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).

Filter by
Sorted by
Tagged with
2 votes
1 answer
26 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 ...
1 vote
1 answer
51 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 ...
5 votes
2 answers
121 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 ...
2 votes
3 answers
76 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. ...
10 votes
3 answers
121 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 ...
-2 votes
1 answer
181 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 ...
5 votes
1 answer
84 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 — ...
3 votes
0 answers
96 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 ...
2 votes
0 answers
86 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
146 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,360
6 votes
1 answer
158 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 ...
7 votes
1 answer
120 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 ...
  • 4,740
4 votes
2 answers
178 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,360
10 votes
1 answer
85 views

Rewriting with context in nested expressions (congruence rules)

I am trying to prove the following example in Lean 4: ...
7 votes
3 answers
139 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 ...
26 votes
1 answer
311 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'...
16 votes
0 answers
133 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. ...
7 votes
2 answers
385 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