Questions tagged [lean4]
Lean 4 is the latest major version of the Lean theorem prover by Microsoft Research. Use this tag for questions specific to Lean 4; if it's about Lean in general, use the tag (lean).
39
questions
0
votes
0
answers
8
views
Using the contrapositive in lean 4
I'm trying to learn lean (version 4) by proving some basic facts about the natural numbers. Please feel free to critique my code if you see have general comments, but I also have a specific question ...
- 101
1
vote
1
answer
44
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 ...
- 305
0
votes
2
answers
33
views
How to create an instance of TotalBLE
I am trying to create an instance of TotalBLE for my comparison function.
...
- 305
1
vote
1
answer
53
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 ...
- 305
4
votes
1
answer
117
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 ...
- 305
1
vote
1
answer
29
views
How to name the hypothesis resulting from the split tactic for if statements
I am trying to prove the following theorem:
...
- 305
1
vote
1
answer
50
views
How to prove pred_le_pred using tactics
The theorem pred_le_pred is proven in prelude.lean using pattern matching:
...
- 305
2
votes
2
answers
139
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, ...
- 151
4
votes
1
answer
122
views
1
vote
0
answers
20
views
How to debug a Lean4 extension
I am interested in debugging the NormCastExt extension to better understand how it works (https://github.com/leanprover/std4/blob/5aa4ab4f0c096e8d0600e3ae41b8577dcf6edb13/Std/Tactic/NormCast/Ext.lean#...
- 217
2
votes
1
answer
89
views
Doing case-by-case proofs about match statements in Lean4
In Lean4, I am stuck in a proof with a goal like this:
...
- 217
4
votes
1
answer
97
views
Tactics for Array/List simplification in lean4
Because there are both Arrays and Lists in Lean4, sometimes you end up with code that has a mixture of Lists and Arrays interspersed with basic operations and conversions between the two. For example,...
- 217
4
votes
1
answer
268
views
Simple Proof about `String.split`
I am new to lean, working on proving a simple lemma in lean4.
lemma String.split_empty (c): String.split "" c = [""]
I tried looking for ...
- 217
4
votes
1
answer
133
views
Lean4 Exercise: Double negation implies law of excluded middle
Been trying to do this exercise from Section 3 of the tutorial for hours and I cannot get it to check. Here's my best attempt below (theorem dne provided by the book):
...
- 43
3
votes
2
answers
108
views
Proving with non-structural recursion in Lean4
I've defined a function (foldMem below) that Lean compiles into a brecOn eliminator. I need to reason with it later on, so I'm ...
- 263
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
2
votes
1
answer
123
views
Definitional vs propositional equality
Theorem Proving in Lean highlights a distinction between definitional and propositional equality when creating recursive functions:
The example above shows that the defining equations for ...
- 263
5
votes
1
answer
128
views
Explain all the arguments to this rec eliminator
I defined this inductive type for representing JSON elements
...
- 263
0
votes
1
answer
145
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 ...
- 169
1
vote
1
answer
167
views
How does Lean4 (or a typical PA) represent lambda functions or in other words arbitrary expressions?
Question:
Say I wanted my language to support various operator symbols, the semantics of which are defined by the user or by axioms.
I'm wondering whether Lean4 (or a typical well-known PA) just ...
2
votes
1
answer
254
views
(In Lean), why cannot structural recursion on propositions be used?
Update: this has been fixed and the fix is available in the latest nightly release of Lean 4.
In Lean 4, structural recursion on functions on types is no issue.
...
- 247
3
votes
1
answer
110
views
How to unfold definitions in Lean / find the right theorems to apply?
After a few days playing around with Lean4, I notice I keep running into the problem of how to find the right theorems to apply. The situation below is one I run into particularly often, so perhaps I ...
- 133
1
vote
1
answer
57
views
Question about default definitions in fields
In Unclarity about Preorder class in Lean4 I asked why the third and fourth field (lt and lt_iff_le_not_le) in the definition of MyPreorder below would both be necessary, as one follows from the other ...
- 133
5
votes
2
answers
153
views
Unclarity about Preorder class in Lean4
I realize the port of Mathlib to Lean4 is not finished yet, but I've run into a definition that I do not quite understand. I'm quite new at using theoremprovers as well as stackexchange, so please be ...
- 133
2
votes
3
answers
169
views
Equality of records with members whose types are dependent (Lean 4)
(Previously, I asked
about converting a term a: A to a term of type B provided that A = B.
...
- 247
10
votes
3
answers
215
views
Given `A = B`, how to prove `a: A` also has type B in Lean 4
I guess my question can be reduced to implementing this function:
def abEq (A B : Type) (a: A) (ab : A = B): B := sorry
I am new to Lean 4 and started learning ...
- 247
-2
votes
1
answer
386
views
A project in Lean which involves "programming"
all,
I have a project in Lean which turns out to involve some features which might better be called programming. So, for that part of the project, I was thinking I would treat Lean like it is Python ...
6
votes
1
answer
133
views
What are the differences between theorem, example, def, etc?
What are all the differences between these keywords that allow for defining top level variables?
What I have noticed so far is that theorems can't be anonymous — ...
- 101
3
votes
0
answers
131
views
Does Lean have a function that reads a file "at compile time"?
Is there some "pure" function that reads a file before the program is type-checked and returns its contents as a string or something, for example if the file ...
- 101
2
votes
0
answers
111
views
Does Lean 4 have syntax to refer to the current thing being defined?
If I am defining a function (using def for example) then is there some way to refer to the function being defined inside its definition without using the name of ...
- 21
4
votes
2
answers
300
views
How to run the main function in lean 4?
I am following the lean 4 tutorial and see a main function as follows:
...
- 1,516
6
votes
1
answer
229
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 ...
- 63
8
votes
1
answer
141
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 ...
- 5,424
4
votes
2
answers
263
views
Non-trivial examples of dependent sum ($\Sigma$-types) in Lean?
I am trying to understand the concept of dependent sum types ($\Sigma$ types) using concrete examples. The example given in Theorem Proving in Lean 4 seems to be a degenerate case rendering the ...
- 1,516
10
votes
1
answer
91
views
Rewriting with context in nested expressions (congruence rules)
I am trying to prove the following example in Lean 4:
...
- 275
7
votes
3
answers
186
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 ...
- 275
29
votes
1
answer
644
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'...
- 931
17
votes
0
answers
150
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.
...
- 1,853
7
votes
2
answers
793
views
How do I install Lean 4?
I want to get started with Lean 4, but I need to install it. The download page links to binaries to download, but I don't know what to do with them. Is there a "best practice" way to install ...
- 228