[lean4/en] Documentation for Lean 4. #4893
Conversation
lean4.html.markdown
Outdated
| Using this we can prove `1 = 1` as follows. | ||
| -/ | ||
|
|
||
| def one_eq_one : 1 = 1 := Eq.refl 1 |
There was a problem hiding this comment.
Style-wise, every theorem should be defined as such; i.e. theorem one_eq_one : 1 = 1 := ....
One can of course view these as noncomputable defs, but that's out of the scope of this intro.
lean4.html.markdown
Outdated
| The following will fail because both sides are not "obviously equal". | ||
| -/ | ||
|
|
||
| /- def pf : 2^9-2^8 = 2^8 := Eq.refl (2^8) -/ |
There was a problem hiding this comment.
'obviously equal' here is definitionally equal; it will work just fine if you feed it the side that reduces.
i.e. theorem pf : 2^9-2^8 = 2^8 := Eq.refl (2 ^ 9 - 2 ^ 8), or theorem pf : 2^9-2^8 = 2^8 := rfl (which constructs the former term).
There was a problem hiding this comment.
I have removed this theorem altogether. You are right, this theorem does not make sense to me after reading your comments.
lean4.html.markdown
Outdated
| let p2 : 2^9-2^8 = 2^8 * 2 - 2^8 := sorry | ||
| let p3 : 2^8 * 2 - 2^8 = 2^8 * (2-1) := sorry | ||
| let p4 : 2^8 * (2-1) = 2^8 := sorry | ||
| Eq.trans (Eq.trans p2 p3) p4 |
There was a problem hiding this comment.
Given the above, either do this symbolically where this proof is needed or use rfl, or quite canonically, decide or mathlib's norm_num.
There was a problem hiding this comment.
Use have instead of let, the data is in Prop which is proof-irrelevant.
lean4.html.markdown
Outdated
| let p4 : 2^8 * (2 - 1) = 2^8 := | ||
| Nat.mul_one (2^8) | ||
| Eq.trans (Eq.trans p2 p3) p4 | ||
|
|
lean4.html.markdown
Outdated
| Eq.trans (Eq.trans p2 p3) p4 | ||
|
|
||
| /- | ||
| For individual steps, we use proofs already available in Lean. For example: |
There was a problem hiding this comment.
Worth noting we're at the liberty to prove whatever it is we so desire.
lean4.html.markdown
Outdated
| specialize h e | ||
| obtain ⟨h1, _⟩ := h | ||
| have h' := identity e' | ||
| obtain ⟨_, h2⟩ := h' |
There was a problem hiding this comment.
Why have we started using obtain instead of the let up until now?
There was a problem hiding this comment.
Are obtain and let interchangeable?
There was a problem hiding this comment.
They're not. obtain is a have + full expressivity of what you call 'rcases patterns'. let is a proof-relevant binder that just happens to be able to deconstruct some simple patterns.
E.g. the former can do things like:
obtain h₁ | h₂ := X```
I would say `obtain` is almost a superset but that's somewhat misleading because `let's` are meant to be used for a different purpose + there's the distinction of whether they keep the data on their rhs around.
So, just think of them as two different features. `obtain` allows you to inspect terms, `let` allows you to introduce new terms.
There was a problem hiding this comment.
I see. I have replaced all let with have in proofs. I think in proofs this is the right thing to do due to proof irrelevance as you mentioned.
Thanks for your comments. They have been very helpful.
lean4.html.markdown
Outdated
| obtain ⟨h1, _⟩ := h | ||
| have h' := identity e' | ||
| obtain ⟨_, h2⟩ := h' | ||
| apply Eq.trans (Eq.symm h2) h1 |
There was a problem hiding this comment.
This should probably say exact now that you introduced it above.
lean4.html.markdown
Outdated
|
|
||
| /- | ||
| Mutually recursive definitions have to be carefully constructed. In particular, | ||
| the hypotheses when recursing should imply well-foundedness. |
There was a problem hiding this comment.
This is misleading. Every definition in Lean has to be well-founded, regardless of whether it's mutually defined.
lean4.html.markdown
Outdated
| /- | ||
| Programming algorithms in Lean is harder. | ||
|
|
||
| This is because we have to convince Lean of termination. Here's a simple |
There was a problem hiding this comment.
This is not true. Lean accepts partial definitions that can be computed with just fine; just can't be unfolded to reason with.
lean4.html.markdown
Outdated
| label the test `n ≤ k` by `h` so that the falsification of this proposition can | ||
| be used by `omega` later to conclude that `n > k`. | ||
|
|
||
| The tactic `omega` is a general-purpose solver for equalities and inequalities. |
There was a problem hiding this comment.
This is also not true. omega is a specific-purpose decision procedure for deciding problems in presburger arithmetic.
- Remove useless theorem `2^9-2^8 = 2^8`. - Rewrite misleading comments. - Use `theorem` and `have` appropriately instead of `def` and `let`.
|
@Ferinko I'm merging this. If there's other issues or parts of your review that weren't addressed or any other things you want to add, it would be nice if you submitted a pull request. |
[language/lang-code](example[python/fr-fr]or[java/en])This documentation contains more comments than the usual tutorials in this repository. Most of it explains theorem proving and not fundamental programming concepts. I think it is still aimed at intermediate to experienced programmers. Please let me know if I should change it.