Questions tagged [lean]

Lean is a theorem prover and programming language, based on the calculus of constructions with inductive types. For version-specific questions, also add the [lean3] or [lean4] tags.

Filter by
Sorted by
Tagged with
2 votes
2 answers
437 views

Lean: dubious noncomputability

In Lean, some definitions must be marked as noncomputable, for example if they depend on the law of the excluded middle or other nonconstructive choice principles. Usually, the reason for ...
user avatar
5 votes
1 answer
97 views

How do I convince the Lean 4 type checker that addition is commutative?

In order to get acquainted with Lean and programming with dependent types I am trying to implement basic operations for a Vector datatype defined following the ...
user avatar
6 votes
1 answer
832 views

In Lean, contradiction tactic failed but actually goal accomplished

I've been playing with Lean, trying to prove the next lemma: lemma l1_cl (A B C : Prop) : ((A → B) → C) → ((A ∧ ¬ B) ∨ C) := ...
user avatar
11 votes
3 answers
587 views

Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?

Question Is CiC stronger than CoC, in terms of proof strength? Context To illustrate the kind of confusion I am in, and what I'd like to learn from the answer, here is part of my inner monologue: If I ...
user avatar
5 votes
2 answers
152 views

How to prove in Lean that sums are distributive?

Assume we are given three types in Lean. constants A B C : Type There is a canonical map of the following form. ...
user avatar
  • 433
2 votes
1 answer
166 views

Lemma about splitting of homogeneous polynomial equations into irreducible equations

Proof assistants, and Lean, are completely new to me. How can I derive the following simple lemma in Lean? How can I let Lean check if the lemma is correctly written? How can I let Lean check if the ...
user avatar
  • 131
12 votes
1 answer
434 views

Lean "nonempty" vs "inhabited"

In the init/logic.lean file of the Lean 3 standard library, nonempty and inhabited are defined. It seems like these two classes ...
user avatar
9 votes
1 answer
488 views

How to define curry in Lean

I just started with Lean and with this nice SE. In the official web book/tutorial, when explaining definitions https://leanprover.github.io/theorem_proving_in_lean/index.html they ask to complete this ...
user avatar
  • 193
16 votes
1 answer
794 views

How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?

This document showed that Lean's impredicative universe of strict propositions breaks normalization (of proofs) in a way that canonicity and logical consistency are unaffected, because the ...
user avatar
  • 4,136
3 votes
2 answers
141 views

Like arbitrary, but for nonempty instead of inhabited

I wrote some code that used a [inhabited ι] assumption, and then used arbitrary ι in the proof. The mathlib linter then ...
user avatar
17 votes
4 answers
772 views

How usable is Lean for constructive mathematics?

In my answer explaining the differences between Lean and Coq, I emphasized that Lean is "essentially classical" mostly due to sociological norms. Nonetheless, even after posting that, I ...
user avatar
  • 3,355
12 votes
0 answers
255 views

How to speed up Lean?

I've recently been writing my first somewhat serious proof in Lean. While doing that, I noticed that Lean gets slower very fast with increasing length of the proof (slower in the sense that whenever I ...
user avatar
  • 421
14 votes
1 answer
458 views

What does the "motive is not type correct" error mean in Lean?

Sometimes, trying to use rw in Lean, we get an error saying motive is not type correct What does this mean? Often ...
user avatar
  • 593
8 votes
2 answers
261 views

Strong induction on ℕ with function α → ℕ

I have the following problem. I have a type $\alpha$, function $f : \alpha \to \mathbb{N}$ and predicate $P : \alpha \to \mathrm{Prop}$ and I want to prove that for all $a : \alpha, P a$. How could ...
user avatar
  • 127
12 votes
2 answers
177 views

Does Lean have a standard ASCII representation?

From Lean 4 tutorial, I learned that In the Lean standard library, you often see Greek letters to denote types, and the Unicode symbol → as a more compact version of -> and you can also type the ...
user avatar
  • 1,310
28 votes
2 answers
560 views

What exactly is setoid hell?

One of the only arguments I've heard about why Lean is better than Coq is that you can construct quotients of built-in structures by default. (In Coq, you apparently have to use Setoids instead of ...
user avatar
7 votes
1 answer
92 views

How does Lean choose which decidability instance to use?

Suppose two separate files define decidability instances for a particular predicate in different ways. If I import both of these files, and attempt to run ...
user avatar
10 votes
1 answer
133 views

Explicit vs implicit universes in lean

I've seen in mathlib several cases where the universes are explicit, that is Type u instead of Type*. Is there any advantage in ...
user avatar
  • 203
4 votes
0 answers
106 views

What would a fully classical and fully univalent ITP and library look like?

Consider two developments in dependent type theory: Lean’s mathlib library (as well many other ITP libraries) is unashamedly fully classical. There is no ...
user avatar
  • 3,355
7 votes
1 answer
100 views

How to quickly look up what constructor/lemma I should use in Lean4?

When writing this answer, I had a hard time finding the lemma I needed to prove 2 ≤ 3. In Agda, when I have a goal, I can press ...
user avatar
  • 4,136
5 votes
1 answer
55 views

Lean: how to use the refine_struct tactic for commutative ring structures?

Suppose I want to make bool (i.e. the type {ff,tt} of boolean values) into a commutative ring. The following works: ...
user avatar
5 votes
1 answer
91 views

How to install Lean-4 stable only?

I followed Lean documentation to install Lean 4 on my Ubuntu Linux (20.04 LTS) using the elan option described there, and updated it to Lean4 ...
user avatar
  • 1,310
12 votes
1 answer
119 views

Lean: problems with visually indistinguishable instances

I will describe a problem which I have in fact solved, but with considerable pain. My question is whether there are better methods for dealing with similar issues. Lean was giving me messages that ...
user avatar
5 votes
2 answers
91 views

How do we resolve metavariables that appear in hypotheses and targets in Lean?

There are two related questions that I expound on below. It might seem like these aren't quite related, but they are both about how to deal with meta-variables that appear when working through a ...
user avatar
  • 333
4 votes
1 answer
66 views

Referencing previous fields when constructing new structure

Let's say I have a simple structure structure foo : Type := (a : ℕ) (b : list (fin a)) when defining the field b I can ...
user avatar
  • 127
18 votes
1 answer
252 views

How hard is computing integrals in Lean?

Are there tools in mathlib which let you give computations of integrals which would roughly follow standard methods for solving them? For now let me restrict attention to some undergrad-level ...
user avatar
  • 928
9 votes
2 answers
96 views

Can Lean simp arguments be ordered?

I want to simplify the expression 0 * 1 * 1 * 1 * 0 using simp only [mul_zero, zero_mul]. I would like ...
user avatar
14 votes
1 answer
134 views

Proof review: Sum of nCk over antidiagonal = Fibonacci

Theorem to prove: The sum of the binomial coefficients over an antidiagonal is a Fibonacci number. More specifically, the $n$th antidiagonal sums to the $n+1$th Fibonacci number, where the ...
user avatar
  • 664
10 votes
1 answer
77 views

Rewriting with context in nested expressions (congruence rules)

I am trying to prove the following example in Lean 4: ...
user avatar
6 votes
3 answers
130 views

Preserve equality with match expression

How can I prove that the matched pattern is equal to the original argument? For example, in the following function, what can I write instead of sorry to prove the ...
user avatar
7 votes
0 answers
96 views

Has there been any work on automated translation of tactic proofs to everyday language?

There are times when I've completed a proof with a lot of backwards reasoning, and I've kind of lost the thread of what I've actually done. It would be nice if there was something that could ...
user avatar
  • 333
6 votes
2 answers
102 views

How to define a recursive sequence in Lean?

Given a recursive sequence of the form $$ f_n = \begin{cases} c_n & n ≤ N\\ F(f_1, f_2, …, f_{n - 1}) & n > N \end{cases} $$ where $c_n$ are constants and $F$ is an arbitrary expression of $...
user avatar
  • 163
9 votes
1 answer
102 views

Representing $\Bbb RP^2$ in Lean: building a type representing a particular set

I need to work with the set of all lines in the Cartesian plane. For my context, the natural way to think of this is that a line can be described by an equation $Ax + By + C = 0$, where $A$ and $B$ ...
user avatar
  • 285
14 votes
2 answers
172 views

What is the difference between refl and rfl in Lean 3?

I already know that refl is called a tactic, and that rfl is a term; can you explain with examples how they technically differ? ...
user avatar
17 votes
1 answer
132 views

How to search for an existing theorem in Lean?

When proving things in a theorem prover, I am often using sizable libraries that I don’t know by heart, so it is crucial to be effective in discovering existing theorems. What are the best approaches ...
user avatar
19 votes
1 answer
144 views

Tutorials for formalizing mathematical definitions/statements in Lean

tl;dr: Are there any good introductions/tutorials on how to formalize definitions and theorem statements in Lean? (in contrast to introductions on formalizing proofs) Some background: I am a phd ...
user avatar
  • 421
13 votes
2 answers
156 views

What is in an olean file?

It seems Lean can produce .olean files from Lean files, and the mathlib project provides an infrastructure to download olean files, which seems to allow the ...
user avatar
11 votes
1 answer
167 views

In Lean, why is the exact tactic necessary when the goal is the same as a hypothesis?

In Lean, when proving basic theorems, one runs into the following kind of thing: ...
user avatar
  • 333
24 votes
1 answer
243 views

What will happen to mathlib when we transition to Lean 4?

Today, there's an exciting large-scale effort to digitize mathematics in Lean's mathematics library mathlib. I understand that a transition to Lean 4 is looming. I'...
user avatar
15 votes
0 answers
113 views

Programming language metatheory in Lean 4?

I'm looking for developments of programming language metatheory done in Lean 4. We have a calculus with a lot of mutually recursive judgements and we want to formalise its denotational semantics. ...
user avatar
10 votes
1 answer
79 views

Is there an official recommendation for editors to input Lean unicode characters?

As mentioned in another question, the way that VSCode and other editors implement unicode characters that cannot be typed directly from most keyboards is an editor feature. As such, different editors ...
user avatar
13 votes
2 answers
111 views

Finding symbols in Lean

There was already a question here of this type but I would like to ask more generally: If I see some strange unicode symbols being used in Lean, is there a recommended way to find out how to type them,...
user avatar
15 votes
2 answers
199 views

Why does apply_instance fail to generate decidable_pred here?

Here is a stripped down version of something that is causing me trouble. ...
user avatar
15 votes
1 answer
96 views

Extends vs including a typeclass argument

In the Lean mathlib, I see some places where a typeclass argument is included in a class definition, such as locally_finite_order. In other places, I see the "<...
user avatar
34 votes
2 answers
732 views

What are the main differences between Coq and Lean?

Coq and Lean are two of the most common proof assistants out there (but the question of course applies to other proof assistants too). What are the main differences between Coq and Lean? Ideally it ...
user avatar
  • 593
22 votes
1 answer
143 views

How to track backwards-incompatible changes in mathlib?

I am trying to update a large body of Lean code to work with the current version of mathlib. This is difficult because there have been a large number of backwards-incompatible changes even since I ...
user avatar
28 votes
1 answer
269 views

In Lean, what do double curly brackets mean?

In Lean, explicit function arguments are enclosed in round brackets and implicit ones in curly brackets, as in this example: ...
user avatar
23 votes
2 answers
230 views

Is there software for interfacing Lean code with LaTeX?

The Natural Number Game suggests the possibility of rewriting mathematics textbooks with embedded interactive Lean code. I'm envisioning something like Google Colab or Mathematica, where you can ...
user avatar
21 votes
1 answer
278 views

What is the difference between `leanprover` and `leanprover-community` GitHub repositories?

I keep bumping into references to "Lean", but then find there are two GitHub repositories for Lean: https://github.com/leanprover and https://github.com/leanprover-community Can someone ...
user avatar
  • 2,676
25 votes
2 answers
292 views

High-performance proof assistants

I mainly work in the field of high-performance computing (HPC). For a 2020 paper I did a Monte Carlo calculation using 24800 CPUs, and one part of the paper was about showing that even up to 24800 ...
user avatar
  • 1,090