learnxinyminutes-docs/lean4.md
2024-12-09 04:34:00 -07:00

520 lines
14 KiB
Markdown
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

---
name: "Lean 4"
filename: learnlean4.lean
contributors:
- ["Balagopal Komarath", "https://bkomarath.rbgo.in/"]
- ["Ferinko", "https://github.com/Ferinko"]
---
[Lean 4](https://lean-lang.org/) is a dependently typed functional programming
language and an interactive theorem prover.
```lean4
/-
An enumerated data type.
-/
inductive Grade where
| A : Grade
| B : Grade
| F : Grade
deriving Repr
/-
Functions.
-/
def grade (m : Nat) : Grade :=
if 80 <= m then Grade.A
else if 60 <= m then Grade.B
else Grade.F
def highMarks := 80 + 9
def lowMarks := 25 + 25
#eval grade highMarks
#eval grade lowMarks
#check (0 : Nat)
/- #check (0 : Grade) -/ /- This is an error. -/
/-
Types themselves are values.
-/
#check (Nat : Type)
/-
Mathematical propositions are values in Lean. `Prop` is the type of
propositions.
Here are some simple propositions.
-/
#check 0 = 1
#check 1 = 1
#check 2^9 - 2^8 = 2^8
/-
Notice Lean displays `0 = 1 : Prop` to say:
The statement "0 = 1" is a proposition.
We want to distinguish true propositions and false propositions. We do this via
proofs.
Each proposition is a type. `0 = 1` is a type, `1 = 1` is another type.
A proposition is true iff there is a value of that type.
How do we construct a value of type `1 = 1`? We use a constructor that is
defined for that type.
`Eq.refl a` constructs a value of type `a = a`. (reflexivity)
Using this we can prove `1 = 1` as follows.
-/
theorem one_eq_one : 1 = 1 := Eq.refl 1
/-
But there is no way to prove (construct a value of type) `0 = 1`.
The following will fail. As will `Eq.refl 1`
-/
/- theorem zero_eq_one : 0 = 1 := Eq.refl 0 -/
/-
Let us prove an inequality involving variables.
The `calc` primitive allows us to prove equalities using stepwise
calculations. Each step has to be justified by a proof.
-/
theorem plus_squared (a b : Nat) : (a+b)^2 = a^2 + 2*a*b + b^2 :=
calc
(a+b)^2 = (a+b)*(a+b) := Nat.pow_two _
_ = (a+b)*a + (a+b)*b := Nat.mul_add _ _ _
_ = a*a + b*a + (a*b + b*b) := by repeat rw [Nat.add_mul]
_ = a*a + b*a + a*b + b*b := by rw [← Nat.add_assoc]
_ = a*a + a*b + a*b + b*b := by rw [Nat.mul_comm b _]
_ = a^2 + a*b + a*b + b*b := by rw [← Nat.pow_two _]
_ = a^2 + a*b + a*b + b^2 := by rw [← Nat.pow_two _]
_ = a^2 + (a*b + a*b) + b^2 := by rw [Nat.add_assoc (a^_)]
_ = a^2 + 2*(a*b) + b^2 := by rw [← Nat.two_mul _]
_ = a^2 + 2*a*b + b^2 := by rw [Nat.mul_assoc _ _ _]
/-
Underscores can be used when there is no ambiguity in what is to be matched.
For example, in the first step, we want to apply `Nat.pow_two (a+b)`. But,
`(a+b)` is the only pattern here to apply `Nat.pow_two`. So we can omit it.
-/
/-
Let us now prove more "realistic" theorems. Those involving logical connectives.
First, we define even and odd numbers.
-/
def Even (n : Nat) := ∃ k, n = 2*k
def Odd (n : Nat) := ∃ k, n = 2*k + 1
/-
To prove an existential, we can provide specific values if we know them.
-/
theorem zero_even : Even 0 :=
have h : 0 = 2 * 0 := Eq.symm (Nat.mul_zero 2)
Exists.intro 0 h
/-
`Exists.intro v h` proves `∃ x, p x` by substituting `x` by `v` and using the
proof `h` for `p v`.
-/
/-
Now, we will see how to use hypothesis that are existentials to prove
conclusions that are existentials.
The curly braces around parameters `n` and `m` indicate that they are
implicit. Here, Lean will infer them from `hn` and `hm`.
-/
theorem even_mul_even_is_even' {n m : Nat} (hn : Even n) (hm : Even m) : Even (n*m) :=
Exists.elim hn (fun k1 hk1 =>
Exists.elim hm (fun k2 hk2 =>
Exists.intro (k1 * ( 2 * k2)) (
calc
n*m = (2 * k1) * (2 * k2) := by rw [hk1, hk2]
_ = 2 * (k1 * (2 * k2)) := by rw [Nat.mul_assoc]
)
)
)
/-
Most proofs are written using *tactics*. These are commands to Lean that guide
it to construct proofs by itself.
The same theorem, proved using tactics.
-/
theorem even_mul_even_is_even {n m : Nat} (hn : Even n) (hm : Even m) : Even (n*m) := by
have ⟨k1, hk1⟩ := hn
have ⟨k2, hk2⟩ := hm
apply Exists.intro $ k1 * (2 * k2)
calc
n*m = (2 * k1) * (2 * k2) := by rw [hk1, hk2]
_ = 2 * (k1 * (2 * k2)) := by rw [Nat.mul_assoc]
/-
Let us work with implications.
-/
theorem succ_of_even_is_odd' {n : Nat} : Even n → Odd (n+1) :=
fun hn =>
have ⟨k, hk⟩ := hn
Exists.intro k (
calc
n + 1 = 2 * k + 1 := by rw [hk]
)
/-
To prove an implication `p → q`, you have to write a function that takes a proof
of `p` and construct a proof of `q`.
Here, `pn` is proof of `Even n := ∃ k, n = 2 *k`. Eliminating the existential
gets us `k` and a proof `hk` of `n = 2 * k`.
Now, we have to introduce the existential `∃ k, n + 1 = 2 * k + 1`. This `k` is
the same as `k` for `n`. And, the equation is proved by a simple calculation
that substitutes `2 * k` for `n`, which is allowed by `hk`.
-/
/-
Same theorem, now using tactics.
-/
theorem succ_of_even_is_odd {n : Nat} : Even n → Odd (n+1) := by
intro hn
have ⟨k, hk⟩ := hn
apply Exists.intro k
rw [hk]
/-
The following theorem can be proved similarly.
We will use this theorem later.
A `sorry` proves any theorem. It should not be used in real proofs.
-/
theorem succ_of_odd_is_even {n : Nat} : Odd n → Even (n+1) := sorry
/-
We can use theorems by applying them.
-/
example : Odd 1 := by
apply succ_of_even_is_odd
exact zero_even
/-
The two new tactics are:
- `apply p` where `p` is an implication `q → r` and `r` is the goal rewrites
the goal to `q`. More generally, `apply t` will unify the current goal with
the conclusion of `t` and generate goals for each hypothesis of `t`.
- `exact h` solves the goal by stating that the goal is the same as `h`.
-/
/-
Let us see examples of disjunctions.
-/
example : Even 0 Odd 0 := Or.inl zero_even
example : Even 0 Odd 1 := Or.inl zero_even
example : Odd 1 Even 0 := Or.inr zero_even
/-
Here, we always know from `p q` which of `p` and/or `q` is correct. So we can
introduce a proof of the correct side.
-/
/-
Let us see a more "standard" disjunction.
Here, from the hypothesis that `n : Nat`, we cannot determine whether `n` is
even or odd. So we cannot construct `Or` directly.
But, for any specific `n`, we will know which one to construct.
This is exactly what induction allows us to do. We introduce the `induction`
tactic.
The inductive hypothesis is a disjunction. When disjunctions appear at the
hypothesis, we use *proof by exhaustive cases*. This is done using the `cases`
tactic.
-/
theorem even_or_odd {n : Nat} : Even n Odd n := by
induction n
case zero => left ; exact zero_even
case succ n ihn =>
cases ihn with
| inl h => right ; apply (succ_of_even_is_odd h)
| inr h => left ; apply (succ_of_odd_is_even h)
/-
`induction` is not just for natural numbers. It is for any type, since all types
in Lean are inductive.
-/
/-
We now state Collatz conjecture. The proof is left as an exercise to the reader.
-/
def collatz_next (n : Nat) : Nat :=
if n % 2 = 0 then n / 2 else 3 * n + 1
def iter (k : Nat) (f : Nat → Nat) :=
match k with
| Nat.zero => fun x => x
| Nat.succ k' => fun x => f (iter k' f x)
theorem collatz : ∀ n, n > 0 → ∃ k, iter k collatz_next n = 1 := sorry
/-
Now, some "corner cases" in logic.
-/
/-
The proposition `True` is something that can be trivially proved.
`True.intro` is a constructor for proving `True`. Notice that it needs no
inputs.
-/
theorem obvious : True := True.intro
/-
On the other hand, there is no constructor for `False`.
We have to use `sorry`.
-/
theorem impossible : False := sorry
/-
Any `False` in the hypothesis allows us to conclude anything.
Written in term style, we use the eliminator `False.elim`. It takes a proof of
`False`, here `h`, and concludes whatever is the goal.
-/
theorem nonsense (h : False) : 0 = 1 := False.elim h
/-
The `contradiction` tactic uses any `False` in the hypothesis to conclude the
goal.
-/
theorem more_nonsense (h : False) : 1 = 2 := by contradiction
/-
To illustrate constructive vs classical logic, we now prove the contrapositive
theorem.
The forward direction does not require classical logic.
-/
theorem contrapositive_forward' (p q : Prop) : (p → q) → (¬q → ¬p) :=
fun pq => fun hqf => fun hp => hqf (pq hp)
/-
Use the definition `¬q := q → False`. Notice that we have to construct `p →
False` given `p → q` and `q → False`. This is just function composition.
-/
/-
The above proof, using tactics.
-/
theorem contrapositive_forward (p q : Prop) : (p → q) → (¬q → ¬p) := by
intro hpq
intro
intro hp
specialize hpq hp
contradiction
/-
The reverse requires classical logic.
Here, we are required to construct a `q` given values of following types:
- `(q → False) → (p → False)`.
- `p`.
This is impossible without using the law of excluded middle.
-/
theorem contrapositive_reverse' (p q : Prop) : (¬q → ¬p) → (p → q) :=
fun hnqnp =>
Classical.byCases
(fun hq => fun _ => hq)
(fun hnq => fun hp => absurd hp (hnqnp hnq))
/-
Law of excluded middle tells us that we will have a `q` or a `q → False`. In the
first case, it is trivial to construct a `q`, we already have it. In the second
case, we give the `q → False` to obtain a `p → False`. Then, we use the fact
(in constructive logic) that given `p` and `p → False`, we can construct
`False`. Once, we have `False`, we can construct anything, and specifically `q`.
-/
/-
Same proof, using tactics.
-/
theorem contrapositive_reverse (p q : Prop) : (¬q → ¬p) → (p → q) := by
intro hnqnp
intro hp
have emq := Classical.em q
cases emq
case inl _ => assumption
case inr h => specialize hnqnp h ; contradiction
/-
To illustrate how we can define an work with axiomatic systems. Here is a
definition of Groups and some proofs directly translated from "Topics in
Algebra" by Herstein, Second edition.
-/
/-
A `section` introduces a namespace.
-/
section GroupTheory
/-
To define abstract objects like groups, we may use `class`.
-/
class Group (G : Type u) where
op : G → G → G
assoc : ∀ a b c : G, op (op a b) c = op a (op b c)
e : G
identity: ∀ a : G, op a e = a ∧ op e a = a
inverse: ∀ a : G, ∃ b : G, op a b = e ∧ op b a = e
/-
Let us introduce some notation to make this convenient.
-/
open Group
infixl:70 " * " => op
/-
`G` will always stand for a group and variables `a b c` will be elements of that
group in this `section`.
-/
variable [Group G] {a b c : G}
def is_identity (e' : G) := ∀ a : G, (a * e' = a ∧ e' * a = a)
/-
We prove that the identity element is unique.
-/
theorem identity_element_unique : ∀ e' : G, is_identity e' → e' = e := by
intro e'
intro h
specialize h e
have ⟨h1, _⟩ := h
have h' := identity e'
have ⟨_, h2⟩ := h'
exact Eq.trans (Eq.symm h2) h1
/-
Note that we used the `identity` axiom.
-/
/-
Left cancellation. We have to use both `identity` and `inverse` axioms from
`Group`.
-/
theorem left_cancellation : ∀ x y : G, a * x = a * y → x = y := by
have h1 := inverse a
have ⟨ai, a_inv⟩ := h1
have ⟨_, h2⟩ := a_inv
intro x y
intro h3
calc
x = (e : G) * x := Eq.symm (identity x).right
_ = ai * a * x := by rw [h2]
_ = ai * (a * x) := by rw [assoc]
_ = ai * (a * y) := by rw [h3]
_ = ai * a * y := by rw [← assoc]
_ = (e : G) * y := by rw [h2]
_ = y := (identity y).right
end GroupTheory /- Variables `G`, `a`, `b`, `c` are now not in scope. -/
/-
Let us see a mutually recursive definition.
The game of Nim with two heaps.
-/
abbrev between (lower what upper : Nat) : Prop := lower ≤ what ∧ what ≤ upper
mutual
def Alice : Nat → Nat → Prop
| n1, n2 =>
∃ k, (between 1 k n1 ∧ (between 1 k n1 → Bob (n1-k) n2))
(between 1 k n2 ∧ (between 1 k n2 → Bob n1 (n2-k)))
def Bob : Nat → Nat → Prop
| n1, n2 =>
∀ k, (between 1 k n1 → Alice (n1-k) n2)
∧ (between 1 k n2 → Alice n1 (n2-k))
end
example : Bob 0 0 := by
intro k
induction k
case zero =>
constructor
intro ; contradiction
intro ; contradiction
case succ =>
constructor
intro a ; have := a.right ; contradiction
intro a ; have := a.right ; contradiction
/-
We have to convince Lean of termination when a function is defined using just a
`def`. Here's a simple primality checking algorithm that tests all candidate
divisors.
-/
def prime' (n : Nat) : Bool :=
if h : n < 2 then
false
else
@go 2 n (by omega)
where
go (d : Nat) (n : Nat) {_ : n ≥ d} : Bool :=
if h : n = d then /- `h` needed for `omega` below. -/
true
else if n % d = 0 then
false
else
@go (Nat.succ d) n (by omega)
termination_by (n - d)
/-
We have to specify that the recursive function `go` terminates because `n-k`
decreases in each recursive call. This needs the hypothesis `n > k` at the
recursive call site. But the function itself can only assume that `n ≥ k`. We
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` can solve simple equalities and inequalities.
-/
/-
You can also instruct Lean to not check for totality by prefixing `partial` to
`def`.
-/
/-
Or, we can rewrite the function to test the divisors from largest to
smallest. In this case, Lean easily verifies that the function is total.
-/
def prime (n : Nat) : Bool :=
if n < 2 then
true
else
go (n-1) n
where
go d n :=
if d < 2 then
true
else if n % d = 0 then
false
else
go (d-1) n
/-
Now, to Lean, it is obvious that `go` will terminate because `d` decreases in
each recursive call.
-/
#eval prime 57
#eval prime 97
```
For further learning, see:
* [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/)
* [Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/)
* [Lean 4 Manual](https://lean-lang.org/lean4/doc/)