[lean4/en] Documentation for Lean 4 (#4893)

1 files changed, 519 insertions, 0 deletions

diff --git a/lean4.html.markdown b/lean4.html.markdown
new file mode 100644
index 00000000..4d427cec
--- /dev/null
+++ b/lean4.html.markdown
@@ -0,0 +1,519 @@
+---
+language: "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/)