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).
96
questions
0
votes
1
answer
17
views
In lean 4, how do I give names to variables when using `split`?
Sort of related to In lean 4, how do I refer to variables with names like `a✝`
When I use split to pull apart a match, I get a ...
- 347
0
votes
1
answer
24
views
In lean 4, how do I refer to variables with names like `a✝`
When I have a tactic state that mentions a variable name like a✝, is there a way to refer to it? When I use this variable name in my code, it says it doesn't exist.
...
- 347
0
votes
1
answer
34
views
What do I need to import from MathLib to make `induction a with d hd` work?
I know that I need to import Mathlib to make rewrite [x] at h work. But induction a with d hd...
- 347
2
votes
1
answer
320
views
Why is lean 4 behaving differently on my machine vs in the natural number game?
In the lean 4 version of the natural number game at https://adam.math.hhu.de/#/g/leanprover-community/NNG4/ , I can use tactics like apply x at h and ...
- 347
3
votes
1
answer
80
views
Print the version of lean that is running
In python, I can get the version of python I am using like this:
import sys
print(sys.version)
...
- 347
0
votes
1
answer
41
views
In lean4 why is induction only rewriting the goal, and not the known facts?
When I do induction over a variable $x$ in lean 4, why isn't $x=0$ available as a fact in the base case of the induction? Without this fact, I can't rewrite other facts in order to make the induction ...
- 347
2
votes
1
answer
54
views
Apply `unfold` once, instead of many times, in lean4
I have code that is similar in spirit to this:
...
- 347
1
vote
1
answer
27
views
Case assumption missing from tactic state in lean4
I'm trying to prove a <= max(a, b) by case. I have this:
...
- 347
1
vote
1
answer
157
views
How do I make the rational numbers 0 and 1/2 in lean4?
I'm trying to define a function that in python I would write:
def f(x: bool) -> float:
if x:
return 0.5
return 0.0
In lean 4 I tried writing ...
- 347
2
votes
2
answers
47
views
Shortening a 4-levels-of-match lean4 proof of the CHSH inequality
In the CHSH game, Alice (Bob) is given the value $x$ ($y$) and needs to pick a value $a$ ($b$) such that $a \oplus b = xy$. The CHSH inequality proves they can win at most 75% of the time with ...
- 347
1
vote
1
answer
50
views
Rewriting certain terms in Lean4
I want to prove the following theorem using a single axiom (https://mathworld.wolfram.com/WolframAxiom.html):
...
- 113
1
vote
2
answers
93
views
How to introduce assumption in lean4
This is probably a trivial question, but I've been googling for hours and can't find the syntax I'm looking for.
I'm trying to write a proof of
...
1
vote
1
answer
86
views
How to run lean4 with mathlib manually
I have a file which contents are:
import Mathlib.Data.Rat.Basic
I save it as file.lean in a lean project
and run it like this
...
- 151
2
votes
1
answer
148
views
How to understand the sigma types example from "Theorem Proving in Lean 4"?
In the Lean 4 book called "Theorem Proving in Lean 4" (https://lean-lang.org/theorem_proving_in_lean4/title_page.html), I don't understand a code example about cartesian product types in ...
- 123
2
votes
1
answer
110
views
How to Prove Theorem le_zero in Lean4: If x ≤ 0, then x = 0?
I am playing the Natural Number Game found here and am trying to prove a theorem in Lean4. The theorem states that if a natural number x is less than or equal to 0, ...
- 151
1
vote
1
answer
143
views
how to prove 2+2+a=4+a in lean4?
It should be simple but dig it for a while and still not successful.
theorem example (a : R) : 2 + 2 + a = 4 + a := ...
can someone help to figure out how to do next? many thanks
- 11
1
vote
1
answer
124
views
How to handle data from json files in lean 4?
I don't know how mature or efficient Lean 4.1.0's standard feature support is.
However, I did enjoy an interesting case about benchmarking data processing languages.The challenge is to read a json ...
2
votes
2
answers
93
views
6
votes
1
answer
300
views
Benefits of HoTT compared with dependent type theory like what Lean does?
I am not an expert in type theory, so I wonder what will HoTT bring to theorem proving (ITP/ATP), compared with dependent type theory? More specially, imagine Lean is implemented using HoTT, I would ...
- 161
2
votes
0
answers
105
views
Highschool level linear algebra
I would like to be able to do high-school level linear algebra in Lean/Mathlib. However, it seems pretty hard. I do understand that mathematicians don't care about being able to do this basic stuff ...
- 173
3
votes
1
answer
163
views
0
votes
0
answers
80
views
Is there an algebreic type in lean4?
In lean4 I've seen the Real, Rat, and Int types, but is there an Algebreic type?
Loooking at:
https://leanprover-community.github.io/blog/posts/dedekind-domains-and-class-number-in-lean/
which links ...
- 101
4
votes
2
answers
124
views
How to think about writing Lean theorems
In Lean we make definitions and formulate theorems about the things we have defined. Seemingly, to each definition there exists several simple theorems. Let's go to ...
- 456
2
votes
1
answer
152
views
Understanding Mathlib/MeasureTheory Notation
I want to understand Mathlib/MeasureTheory, and in particular I want to understand Mathlib/MeasureTheory/Integral. I'm having ...
- 456
0
votes
1
answer
39
views
Automatic nightly Lean update?
I recently answered my own question for how to set up a Lean project with Mathlib dependencies. I realize I don't know everything about this. The route I follow starts by navigating to the correct ...
- 456
5
votes
1
answer
118
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 ...
- 173
3
votes
1
answer
349
views
Does lean 4 have built-in dictionary types?
Are there builtin dictionary/map types in Lean 4 prover?
I'd like to use dictionaries in my program and prove properties about it, but I am not sure if there is a dictionary type in Lean 4. A similar ...
- 1,772
1
vote
1
answer
71
views
Where do I prove that a return type is valid?
I am learning Lean 4 by implementing a fixed-length vector type.
Type definition:
...
- 45
4
votes
1
answer
109
views
Why can addition be used in pattern matching Nats but not multiplication
Here's a simple dummy function in Lean 4:
def foo : Nat → Nat
| (m*2) => m
| (m+2) => m
| (m+1) => m
| (0) => 0
Lean has no trouble ...
- 197
1
vote
0
answers
117
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
69
views
Recursive type class for OfNat Even
I'm working my way through Functional Programming in Lean. There's an exercise to create an Even class to represent even natural numbers.
I was able to define ...
- 197
0
votes
1
answer
46
views
proof-based Pos type class
I'm working my way through the chapter on type classes in Functional Programming in Lean. The text demonstrates type-classes by representing positive numbers this way:
...
- 197
1
vote
1
answer
53
views
Typing List.nil
I'm working my way through Functional Programming in Lean and there's an exercise to create a zip function for combining two ...
- 197
3
votes
2
answers
622
views
proof of termination for zip in Lean
I'm making my way through Functional Programming in Lean and there's an exercise to implement zip, which takes two lists and returns a list of tuples the length of ...
- 197
1
vote
1
answer
133
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 ...
- 161
4
votes
1
answer
203
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?
...
- 161
2
votes
3
answers
246
views
2
votes
1
answer
157
views
Dependent replacement in Lean
I'm stuck on proving extensionality results for my dependent structures in Lean 4. It's turning out to be very difficult to show equalities for these dependent structures, since I require a kind of ...
- 381
3
votes
1
answer
122
views
Dependent Equality
I have been using lean for a while and I have noticed that I can't actually prove extensionality for my dependent structures. I was worried at first and then noticed that it was essentially dependent ...
- 381
5
votes
1
answer
398
views
Where is the syntax of Lean 4 documented?
The syntax of Lean 3 is documented in the Lean Reference Manual chapters on expressions, match expressions, declarations, other commands, attributes, and so forth. It's spread out, and I don't think ...
- 151
6
votes
2
answers
139
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,...
- 135
0
votes
0
answers
177
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 ...
- 456
0
votes
2
answers
110
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 ...
- 456
4
votes
1
answer
412
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
237
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?
- 456
4
votes
1
answer
247
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 ...
- 456
1
vote
1
answer
37
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?
- 456
4
votes
1
answer
95
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 ...
- 456
1
vote
1
answer
72
views
Project wide "set_option autoImplicit false" in Lean 4
I want to turn off the autoImplicit option for a whole lake project. Could I achieve that in lakefile.lean? The options ...
- 145
2
votes
0
answers
64
views
Must-read Lean 4 Mathlib Files
I am starting to understand Lean 4, but I feel a bit overwhelmed by the amount of dependencies for most files in Mathlib. To become more familiar, particularly with the module typeclass, I decided to ...
- 456