All Questions
28
questions
3
votes
1
answer
142
views
Help needed for Lean4 book Interlude exercise
In 3. Interlude of the Functional Programming in Lean book, one of the exercises asks the reader to prove by simp some few theorems, one of them is ...
- 133
0
votes
1
answer
89
views
Using lean4 to prove subset properties
I'm learning Lean4.
I'm trying to prove in lean4 these basic properties of subsets:
$ X \subseteq X $
$ X \subseteq Y , Y \subseteq Z \Rightarrow X \subseteq Z$
$ X \subseteq Y , Y \subseteq X \...
- 3
2
votes
1
answer
136
views
Two steps induction in Lean4: how to obtain 2nd inductive hypothesis?
When trying to solve this example from "The Mechanics of Proof":
...
0
votes
1
answer
161
views
What am I doing wrong when proving the add_right_cancel theorem?
So, as mentioned in my previous two questions, I have been using The Natural Number Game to help me teach myself how to use the mathematical proof assistant Lean4.
I am currently trying to complete ...
- 145
2
votes
2
answers
256
views
How do I prove $\operatorname{succ}(a)$ cannot be equal to $0$ in Lean4?
So I have been using The Natural Number Game (as I have mentioned in my previous post) to learn Lean1. However, I am currently stuck on level 6/9 in the Algorithm world, where I am supposed to prove ...
- 145
1
vote
1
answer
133
views
Need help with induction proof in Lean for $0+d=d$
So I have been trying to learn Lean and have managed to find this resource called the "Natural Number Game" which is supposed to help me learn Lean.
I am learning Lean to help me understand ...
- 145
2
votes
1
answer
169
views
In Lean 4 how to substitute equals in an expression with other variables?
I can use 'subst' to prove that if a=b and a is positive then b is positive:
example (a b : Peano) (h1 : a = b) (h2 : pos a) : pos b := Eq.subst h1 h2
How do I ...
- 31
1
vote
1
answer
146
views
How to see the value under Exists in Lean?
My understanding of dependent typing is that it allows typing functions to constrain their behavior. Say I have a Lean object
...
- 13
0
votes
1
answer
118
views
Shortcut proof by calculation for addition/subtraction, "The Mechanics of Proof", and mathlib4
In Macbeth's book 'The Mechanics of Proof,' the author provides a tactic called addarith to eliminate the need to write calc ...
0
votes
1
answer
166
views
In Lean 4 how to use an implication in a hypothesis?
I am experimenting with my own "natural numbers" (Peano), so I don't want to use Lean 4's natural number tactics (such as add_comm or cancellation). How can the following be proved? It ...
- 31
0
votes
1
answer
233
views
An installation error in "Mathematics in Lean"
I have just started learning Lean 4 using Mathematics in Lean in Visual Studio Code, and I ran into a problem right away. I get the following error message:
...
- 1
2
votes
1
answer
179
views
Verifying a basic function with Lean4
I have this simple structure to represent a person:
structure Person where
age: Nat
lifespan: Nat
deriving Repr
This function takes a Person and either (a) ...
1
vote
0
answers
61
views
Peano Arithmetic in LEAN4 [duplicate]
Kia ora!
I am trying to implement the Peano axioms and prove some simple theorems about the natural numbers in LEAN4. However, I am not sure how to encode the first two (as presented here) axioms in ...
user2426
0
votes
1
answer
154
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 ...
- 479
1
vote
1
answer
276
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.
...
- 479