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.
116
questions
2
votes
1
answer
30
views
What is the precise meaning of "reducible"?
In Lean 4, I've seen the terms "reducible", "semi-reducible" and "irreducible" mentioned a lot. What is the precise meaning and how are these concepts used in code? When ...
- 121
2
votes
0
answers
67
views
How does Lean `simp` tactic work?
The doc at https://leanprover-community.github.io/extras/simp.html says about simp:
all it does is repeatedly replace (or rewrite) subterms of the form A by B, for ...
- 153
1
vote
1
answer
81
views
Lean: what does the syntax `variable [ring R]` mean?
I have written a simple Lean program, inspired by things I found here and there, which compiles as shown in the web editor:
...
- 153
2
votes
1
answer
139
views
(Dis)Advantages of basing a proof assistant on CH correspondence?
Major proof assistants like Lean and Coq are fundamentally based on the Curry-Howard correspondence: propositions are encoded as types, quantified propositions are encoded as dependent types, proofs ...
- 153
1
vote
0
answers
76
views
Lean proofs for graph algorithms
I am new to lean but am interested in proving correctness of graph algorithms. Is there a repository/website that talks about a proof using lean of Dijkstra's shortest path algorithm, for example?
- 111
1
vote
1
answer
103
views
Prove an upper bound on the computation time of the Euclidean algorithm in lean4
I've heard that proof assistants like lean4 can formalize all the usual math.
I'm interested to see how they formalize the complexity estimates of algorithms, since they are not often discussed ...
- 151
3
votes
1
answer
100
views
Programming challenge site for lean4
I recently discovered that Codewars supports lean language.
https://www.codewars.com/
However, lean4 does not seem to be supported.
Do you know of any programming challenge sites that support lean4?
...
- 151
2
votes
4
answers
1k
views
Can we prove every provable statement with Lean?
This question was originally posted on math.stackexchange. People there directed me here.
I just discovered Lean and using computers for stating and proving theorems. The first question that came to ...
- 123
0
votes
1
answer
93
views
increasing the universe level of a type in Lean by force
Given some term
A : Sort u
in Lean, is there a way to artificially increase the universe level and promote A to a term
...
- 712
1
vote
1
answer
76
views
Type of Sets with an Assocaitive Operation in Lean
This is probably a really simple question, but I am no able to find something in the Lean reference manual. I want to define a type of sets equipped with an associative operation.
I have tried the ...
- 712
0
votes
1
answer
59
views
Minimizing proof environment change while proving in Lean
As a matter of (Lean) style, I would like to minimize changing the proof environment, and instead apply lemmas directly (to be "less imperative" and "more functional").
So, can ...
- 183
1
vote
2
answers
161
views
How to parse Lean 3(?) theorem statements to JSON AST
I'd like to take a .lean file, and extract from it all the theorem statements into a fully-elaborated unambiguous textual format that is morally isomorphic to the ...
- 1,062
6
votes
2
answers
108
views
How does one show termination of a function that is structurally recursive over a type T with subterms of type List T?
I've been having a bit of difficulty proving termination of a particular kind of function. I'm quite new to using Lean, so it's possible that what I'm missing is a language feature and not a technique,...
- 133
4
votes
2
answers
287
views
Reasoning about CwFs in a proof assistant
I've been chatting with folks on Mastodon about this but the perspective there is markedly Agda-focused, so I thought I'd ask here for some broader opinions.
What tools/libraries are there for ...
- 768
0
votes
0
answers
123
views
Porting Lean 3 to Lean 4 Process (and the state of general integration in Lean 4)
I found this reference for measure-theoretic integration in Lean. However, I cannot find any integration in the Lean 4 Measure Theory library. Have these not yet been ported, or can they be found ...
- 342
0
votes
2
answers
82
views
Differential Topology and Differential Geometry Porting to Mathlib4
Simple question, but I started working with Lean after Lean 4 came out, so I'm not familiar with Lean 3. To what extent have the Mathlib3 differential topology and differential geometry libraries been ...
- 342
4
votes
1
answer
264
views
Linear types in lean?
Is the LEAN type checker able to count the number of times a parameter is used in a function body?
In Idris2 for comparison I might use (1 x:Nat) which then makes ...
- 147
4
votes
1
answer
222
views
What are the goals of Lean 4?
Porting Mathlib from Lean 3 to Lean 4 is a huge effort, and I'm sure it's not undertaken on a whim. Could you please point me to documentation explaining the motivation for the incompatible changes? ...
- 157
4
votes
1
answer
156
views
Aesop Tactic in Lean
Simple question, but can someone explain the role of the aesop tactic in general, and as it pertains to SimpleGraph?
- 342
4
votes
1
answer
154
views
Graph Theory in Lean
I can't find an implementation of graph theory in Mathlib. Am I overlooking the file, or is it particularly difficult to do this, or has no one been interested in taking this on yet?
If it hasn't been ...
- 342
1
vote
1
answer
43
views
invalid apply tactic, failed to unify
I'm just learning Lean, currently on Advanced Addition world, level 5/13.
I have a hypothesis h that succ (a + d) = succ (b + d)....
- 157
1
vote
1
answer
32
views
inherit_doc attribute Lean 4
This is a rather simple question which I cannot find an answer to in the Lean 4 API or anywhere else online. What does the @[inherit_doc] attribute do?
- 342
4
votes
1
answer
87
views
Auxiliary Typeclasses in Lean
It's a common theme in Mathlib to use some auxiliary typeclass to define the one we actually want to use. For example, to define PseudoMetricSpace we use the ...
- 342
2
votes
1
answer
103
views
Vectors in Lean
In Lean vectors are implemented using
def Vec (a : Type u) (n : Nat) :=
{ l : List a // l.length = n}
I think there is another way to do this without lists:
<...
- 342
3
votes
1
answer
213
views
Type Theory Lean 3 to Lean 4
I'm aware of Lean's type theory. Did the type theory of lean change at all as we moved to Lean 4? Are there any references to this?
- 342
1
vote
2
answers
670
views
Make ChatGPT write formal proof from natural language proof
I know very little about proof assistants, but I played a little with Lean, so I have some basic knowledge of how they work.
I was curious whether I could make ChatGPT convert some natural language ...
- 121
3
votes
2
answers
195
views
How to abstract over function arity in Lean and Coq?
Given types $A, B$ I would like to express the type of all functions $f$ for which there exists an $n \in ℕ$ such that $f$ has type $A^n \to B$. And possibly in such a way, that for $a_1, \dots, a_n : ...
- 224
2
votes
2
answers
102
views
unexpected inductive type occurrence error for recursive inductive type
I want to declare a property that a recursive structure was constructed using a smart constructor. The smart constructor mainly constructs with hash field and the property would allow me to trust the ...
- 315
0
votes
2
answers
40
views
How to create an instance of TotalBLE
I am trying to create an instance of TotalBLE for my comparison function.
...
- 315
1
vote
1
answer
98
views
Unravelling notations in Lean
When one is busy writing a proof in Lean, one sometimes encounters symbols, like + or <=, but one does not know what the ...
- 315
4
votes
1
answer
171
views
Is there a way in LeanProver to declare an inline recursive function, like fix in Coq?
Is there a way to declare an inline recursive function, like fix in Coq?
A relatively minimal example, which has a recursive structure on which we are trying to do ...
- 315
1
vote
1
answer
47
views
How to name the hypothesis resulting from the split tactic for if statements
I am trying to prove the following theorem:
...
- 315
1
vote
1
answer
58
views
How to prove pred_le_pred using tactics
The theorem pred_le_pred is proven in prelude.lean using pattern matching:
...
- 315
3
votes
2
answers
149
views
How to show that an expression of a finite type must be one of the finitely many possible values?
In Lean, how do I prove that a variable, or more generally an expression, ranging over a finite type must be equal to one of the values of the finite type?
In particular, the following should be easy, ...
- 161
0
votes
1
answer
105
views
A chain of coercion in Lean fails to infer the correct type automatically but each separate step does
Context
I have defined two structures corresponding to a group and a subgroup :
...
- 11
2
votes
1
answer
180
views
Setting up Lean 4 on a server
I'm looking at the Lean-in-the-web-browser setup here. It would be really cool if my server at linearlibrary.net could have a page for Lean code of its own.
Unfortunately when I tried to take apart ...
- 127
2
votes
3
answers
383
views
How can I use a dummy variable to prove a lemma in Lean3?
I have the following definition for the operator D:
noncomputable def D: (ℝ → ℝ) → (ℝ → ℝ) := λ f, deriv f
I want to prove that ...
- 21
3
votes
1
answer
68
views
Are there squeeze-versions of ring and abel?
In Lean, it is recommended to use squeeze_simp to generate simp only [a bunch of lemmas] for two reasons:
(1) Otherwise the ...
- 183
4
votes
1
answer
204
views
Error when starting a project in Lean, 'binary package was not provided for 'windows''
after taking a break of half a year I would like to get back to proving things in Lean. I followed the instructions to install a fresh lean project. When I do
...
- 183
2
votes
1
answer
199
views
Is type checking in "Ideal Lean" computably enumerable?
There are actually two type theoretic foundations of Lean given in Mario Carneiro's master's thesis. They are the same, except for how definitional equality is treated:
“algorithmic” definitional ...
- 6,713
4
votes
3
answers
1k
views
Are there computable functions which can't be expressed in Lean?
Lean, unlike e.g. Haskell, makes you prove that recursive definitions of functions will eventually terminate, if the compiler can't do it by using structural recursion, by using ...
- 43
5
votes
1
answer
132
views
Explain all the arguments to this rec eliminator
I defined this inductive type for representing JSON elements
...
- 263
1
vote
1
answer
163
views
How does one translate Lean to Coq (and visa versa)?
I am interested in translated Lean to Coq and visa versa. One first reason is because I want to translate the miniF2F data set in Lean to Coq but lack the expertise to do it. Though in general I'd ...
- 179
0
votes
1
answer
79
views
Well founded recursion through lists
I'm trying out Lean for programming, and I'm struggling with the termination checker. Here's the toy I'm playing with:
...
- 263
1
vote
1
answer
70
views
How do I prove that an element is a within a set in Lean?
Given this code,
inductive Test : Type
| T1 | T2
example : Test.T1 ∈ { t: Test | t = Test.T1 } := begin
sorry
end
How do I prove that ...
- 113
3
votes
1
answer
353
views
Getting an element of a list in Lean
I'm using Lean 4 along with Mathlib.
I'm trying to work with lists, but I can't find a function which obtains the nth entry of a list. It seems pretty hard to find for the most basic function of a ...
- 127
0
votes
1
answer
283
views
Installing relevant packages for Lean's math lib
I'm using the Lean computer proof assistant on my Mac.
I tried to import data.nat.basic from lean's documentation, just like this:
import data.nat.basic
I get this:...
- 127
6
votes
1
answer
210
views
Can we completely erase propositions in the type checker?
Related question on semantic side: How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?
Suppose we have an impredicative universe of ...
- 5,792
3
votes
1
answer
201
views
Equality type and Propositions
I'm writing a library in the Lean computer proof assistant.
Evidently,
X : Type
x : X
y : X
#check x = y
Produces "Prop" and not "Type"; ...
- 155
1
vote
2
answers
80
views
Suppressing notation in Lean
I'm using the Lean computer proof assistant and customizing some notation. Here's the example I'm working with:
...
- 155