Theorem Proving in Lean 4

https://leanprover.github.io/theorem_proving_in_lean4/
Admin
Theorem Proving in Lean 4 is a comprehensive guide to formal theorem proving using the Lean 4 proof...
Tokens:123,752
Snippets:1,295
Trust Score:8.3
Update:4 months ago
Show doc for...
Tokens:
Raw
### Example using `simp` for algebraic expansion

Source: https://leanprover.github.io/theorem_proving_in_lean4/Quantifiers-and-Equality

A concise example using `simp` to prove the algebraic identity.

```Lean
variable (x y : Nat)
example : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
by
  x:Nat
  y:Nat
  ⊢ (x + y) * (x + y) = x * x + y * x + x * y + y * y
  simp [Nat.mul_add, Nat.add_mul, Nat.add_assoc]
-- All goals completed! 🐙
```

--------------------------------

### Example demonstrating function extensionality

Source: https://leanprover.github.io/theorem_proving_in_lean4/Axioms-and-Computation

This example shows how `extfun_app` can be used to demonstrate that extensionally equal functions are equal in the `extfun` type.

```Lean
example (f₁ f₂ : (x : α) → β x) (h : ∀ x, f₁ x = f₂ x) :=
  calc f₁ =
    _ = extfun_app (.mk _ f₁) :=
      rfl
    _ = extfun_app (.mk _ f₂) :=
      by
        rw [Quot.sound]
        trivial
    _ = f₂ :=
      rfl
```

--------------------------------

### Example using `simp` with `List.reverse_append`

Source: https://leanprover.github.io/theorem_proving_in_lean4/Tactics

An example demonstrating the use of `simp` with the `List.reverse_append` lemma.

```Lean
example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) :
    p ((mk_symm ys).reverse ++ xs.reverse) :=
  by simp only [List.reverse_append] at h
```

--------------------------------

### Custom Infix Notation Example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Interacting-with-Lean

An example of defining a custom infix notation using the 'notation' command.

```Lean
def `declaration uses 'sorry'`wobble : α → β → γ := sorry
``notation:65 lhs:65 " ~ " rhs:65 => wobble lhs rhs
```

--------------------------------

### And.intro example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Propositions-and-Proofs

This example demonstrates the use of `And.intro` to construct a proof of `p ∧ q` from proofs of `p` and `q`. It also shows the equivalent anonymous constructor notation `⟨hp, hq⟩`.

```Lean
variable (p q : Prop)
example (hp : p) (hq : q) : p ∧ q := And.intro hp hq

#check fun hp hq => ⟨hp, hq⟩ : p → q → p ∧ q
```

--------------------------------

### Proposition Composition Example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Propositions-and-Proofs

An example demonstrating function composition with propositions, analogous to the previous chapter's example with types. It also shows the use of numeric Unicode subscripts for hypotheses.

```Lean
variable (p q r s : Prop)
theorem t2 (h₁ : q → r) (h₂ : p → q) : p → r := fun h₃ : p => show r from h₁ (h₂ h₃)
```

--------------------------------

### Example using `rw` for algebraic expansion

Source: https://leanprover.github.io/theorem_proving_in_lean4/Quantifiers-and-Equality

A concise example using `rw` to prove the algebraic identity.

```Lean
variable (x y : Nat)
example : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
by
  x:Nat
  y:Nat
  ⊢ (x + y) * (x + y) = x * x + y * x + x * y + y * y
  rw [Nat.mul_add, Nat.add_mul, Nat.add_mul, ←Nat.add_assoc]
-- All goals completed! 🐙
```

--------------------------------

### Example: Proving \forall y : \alpha, p y from \forall x : \alpha, p x ∧ q x

Source: https://leanprover.github.io/theorem_proving_in_lean4/Quantifiers-and-Equality

An example demonstrating how to prove a universal quantification from a conjunction of two predicates.

```Lean
example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ y : α, p y := fun h : ∀ x : α, p x ∧ q x => fun y : α => show p y from (h y).left
```

--------------------------------

### Unsound function example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Induction-and-Recursion

Example demonstrating how `sorry` can be used to prove `False`, leading to an unsound definition.

```Lean
def `declaration uses 'sorry'`unsound (x : Nat) : False :=
  unsound (x + 1)
decreasing_by sorry
-- All goals completed! 🐙
-- unsound 0 : False
#check unsound 0

-- `unsound 0` is a proof of `False`
'unsound' depends on axioms: [sorryAx]
#print axioms unsound
```

--------------------------------

### And.left and And.right examples

Source: https://leanprover.github.io/theorem_proving_in_lean4/Propositions-and-Proofs

These examples demonstrate the use of `And.left` and `And.right` to extract proofs of `p` and `q` respectively from a proof of `p ∧ q`.

```Lean
variable (p q : Prop)
example (h : p ∧ q) : p := And.left h
example (h : p ∧ q) : q := And.right h
```

--------------------------------

### Example: Proving \forall x : \alpha, p x from \forall x : \alpha, p x ∧ q x (using different variable names)

Source: https://leanprover.github.io/theorem_proving_in_lean4/Quantifiers-and-Equality

An example showing the equivalence of variable renaming in universal quantification proofs.

```Lean
example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ x : α, p x := fun h : ∀ x : α, p x ∧ q x => fun z : α => show p z from And.left (h z)
```

--------------------------------

### Tail Function Examples

Source: https://leanprover.github.io/theorem_proving_in_lean4/Induction-and-Recursion

Demonstrates defining the 'tail' function with parameters placed before and after the type signature.

```Lean
set_option linter.unusedVariables false
def tail1 {α : Type u} : List α → List α |
  [] => []
  | a :: as => as
def tail2 : {α : Type u} → List α → List α |
  α, [] => []
  | α, a :: as => as
```

--------------------------------

### List namespace examples

Source: https://leanprover.github.io/theorem_proving_in_lean4/Dependent-Type-Theory

Provides examples of definitions within the 'List' namespace, such as 'nil', 'cons', and 'map', and demonstrates how to check their types.

```Lean
List.nil.{u} {α : Type u} : List α
#check List.nil
List.cons.{u} {α : Type u} (head : α) (tail : List α) : List α
#check List.cons
List.map.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List β
#check List.map
```

--------------------------------

### Example using `simp` with a hypothesis

Source: https://leanprover.github.io/theorem_proving_in_lean4/Tactics

An example demonstrating the use of `simp` with a hypothesis `h`.

```Lean
example (xs ys : List Nat) (p : List Nat → Prop) (h : p (mk_symm ys ++ xs.reverse)) :
    p (mk_symm ys ++ xs.reverse) :=
  by simp at h
```

--------------------------------

### Equality Proof Example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Quantifiers-and-Equality

An example demonstrating a proof involving equality in Lean 4, using `have` and `trans`.

```Lean
example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := have h1 : (x + y) * (x + y) = (x + y) * x + (x + y) * y := Nat.mul_add (x + y) x y have h2 : (x + y) * (x + y) = x * x + y * x + (x * y + y * y) := (Nat.add_mul x y x) ▸ (Nat.add_mul x y y) ▸ h1 h2.trans (Nat.add_assoc (x * x + y * x) (x * y) (y * y)).symm
```

--------------------------------

### Division function example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Induction-and-Recursion

An example of defining a division function using recursion and proving its correctness with Lean's `by` tactic.

```Lean
example (x y : Nat) : div x y = if 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 :=
by
  unfold div
  conv =>
    lhs
    unfold div
  simp

```

--------------------------------

### Basic tactic example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Tactics

An example demonstrating the use of basic tactics like `apply Eq.trans`, `apply Eq.symm`, and `repeat assumption`.

```Lean
example : ∀ a b c : Nat, a = b → a = c → c = b := by
⊢ ∀ (a b c : Nat), a = b → a = c → c = b
intros
a✝ : a = b
b✝ : a = c
⊢ c = b
apply Eq.trans
apply Eq.symm a✝
assumption
All goals completed! 🐙 
```

--------------------------------

### Example using `calc` with divisibility

Source: https://leanprover.github.io/theorem_proving_in_lean4/Quantifiers-and-Equality

An example demonstrating the use of `calc` with the `divides` relation, including infix notation.

```Lean
example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) :=
calc divides x y := h₁
_ = z := h₂
_ | 2*z := divides_mul ..
-- All goals completed! 🐙
```

--------------------------------

### Basic Pattern Matching Example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Induction-and-Recursion

Demonstrates basic pattern matching on two lists of natural numbers.

```Lean
def bar : List Nat → List Nat → Nat |
  [], [] => 0
  | a :: as, [] => a
  | [], b :: bs => b
  | a :: as, b :: bs => a + b
```

--------------------------------

### Example using `simp` with a negated theorem

Source: https://leanprover.github.io/theorem_proving_in_lean4/Tactics

An example demonstrating the use of `simp` with a negated theorem `[-reverse_mk_symm]`.

```Lean
example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) :
    p ((mk_symm ys).reverse ++ xs.reverse) :=
  by simp [-reverse_mk_symm] at h
```

--------------------------------

### Checking And Type

Source: https://leanprover.github.io/theorem_proving_in_lean4/Interacting-with-Lean

Examples of using `#check` with the `And` type and its `intro` constructor.

```Lean
-- examples with And `And (a b : Prop) : Prop`
#check And
```

```Lean
`And.intro {a b : Prop} (left : a) (right : b) : a ∧ b`
#check And.intro
```

```Lean
`@And.intro : ∀ {a b : Prop}, a → b → a ∧ b`
#check @And.intro
```

--------------------------------

### Revert tactic example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Tactics

Demonstrates the `revert` tactic, which is an inverse to `intro`.

```Lean
example (x : Nat) : x = x := by
x : Nat
⊢ x = x
revert x
⊢ ∀ (x : Nat), x = x
intro y
y : Nat
⊢ y = y
rfl
All goals completed! 🐙 
```

--------------------------------

### Dependent Pattern Matching Example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Induction-and-Recursion

An example demonstrating dependent pattern matching for the `zipWith` function on `Vect` in Lean4. This illustrates a complex recursive definition requiring careful handling of types and indices.

```Lean4
def Vect.zipWith.match_1.{u_1, u_2, u_3} : {α : Type u_1} → {β : Type u_2} → (motive : (x : Nat) → Vect α x → Vect β x → Sort u_3) → (x : Nat) → (x_1 : Vect α x) → (x_2 : Vect β x) → (Unit → motive 0 nil nil) → ((n : Nat) → (a : α) → (as : Vect α n) → (b : β) → (bs : Vect β n) → motive n.succ (cons a as) (cons b bs)) → motive x x_1 x_2 := fun {α} {β} motive x x_1 x_2 h_1 h_2 => Nat.casesOn (motive := fun x => (x_3 : Vect α x) → (x_4 : Vect β x) → motive x x_3 x_4) x (fun x x_3 => casesOn (motive := fun a x_4 => Nat.zero = a → x ≍ x_4 → motive Nat.zero x x_3) x (fun h h_3 => ⋯ ▸ casesOn (motive := fun a x => Nat.zero = a → x_3 ≍ x → motive Nat.zero nil x_3) x_3 (fun h h_4 => ⋯ ▸ h_1 ()) (fun a {n} a_1 h => False.elim ⋯) ⋯ ⋯) (fun a {n} a_1 h => False.elim ⋯) ⋯ ⋯) (fun n x x_3 => casesOn (motive := fun a x_4 => n.succ = a → x ≍ x_4 → motive n.succ x x_3) x (fun h => False.elim ⋯) (fun a {n_1} a_1 h => n.elimOffset n_1 1 h fun x_4 => Eq.ndrec (motive := fun {n_2} => (a_2 : Vect α n_2) → x ≍ cons a a_2 → motive n.succ x x_3) (fun a_2 h => ⋯ ▸ casesOn (motive := fun a_3 x => n.succ = a_3 → x_3 ≍ x → motive n.succ (cons a a_2) x_3) x_3 (fun h => False.elim ⋯) (fun a_3 {n_2} a_4 h => n.elimOffset n_2 1 h fun x => Eq.ndrec (motive := fun {n_3} => (a_5 : Vect β n_3) → x_3 ≍ cons a_3 a_5 → motive n.succ (cons a a_2) x_3) (fun a_5 h => ⋯ ▸ h_2 n a a_2 a_3 a_5) x a_4) ⋯ ⋯) x_4 a_1) ⋯ ⋯) x_1 x_2
```

```Lean4
def Vect.zipWith.match_1.{u_1, u_2, u_3} : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (x : Nat) → Vect α x → Vect β x → Sort u_3) →
      (x : Nat) →
        (x_1 : Vect α x) →
          (x_2 : Vect β x) →
            (Unit → motive 0 nil nil) →
              ((n : Nat) →
                  (a : α) → (as : Vect α n) → (b : β) → (bs : Vect β n) → motive n.succ (cons a as) (cons b bs)) →
                motive x x_1 x_2 := 
fun {α} {β} motive x x_1 x_2 h_1 h_2 =>
  Nat.casesOn (motive := fun x => (x_3 : Vect α x) → (x_4 : Vect β x) → motive x x_3 x_4) x
    (fun x x_3 =>
      casesOn (motive := fun a x_4 => Nat.zero = a → x ≍ x_4 → motive Nat.zero x x_3) x
        (fun h h_3 =>
          ⋯ ▸
            casesOn (motive := fun a x => Nat.zero = a → x_3 ≍ x → motive Nat.zero nil x_3) x_3
              (fun h h_4 => ⋯ ▸ h_1 ()) (fun a {n} a_1 h => False.elim ⋯) ⋯ ⋯)
        (fun a {n} a_1 h => False.elim ⋯) ⋯ ⋯)
    (fun n x x_3 =>
      casesOn (motive := fun a x_4 => n.succ = a → x ≍ x_4 → motive n.succ x x_3) x (fun h => False.elim ⋯)
        (fun a {n_1} a_1 h =>
          n.elimOffset n_1 1 h fun x_4 =>
            Eq.ndrec (motive := fun {n_2} => (a_2 : Vect α n_2) → x ≍ cons a a_2 → motive n.succ x x_3)
              (fun a_2 h =>
                ⋯ ▸
                  casesOn (motive := fun a_3 x => n.succ = a_3 → x_3 ≍ x → motive n.succ (cons a a_2) x_3) x_3
                    (fun h => False.elim ⋯)
                    (fun a_3 {n_2} a_4 h =>
                      n.elimOffset n_2 1 h fun x =>
                        Eq.ndrec (motive := fun {n_3} =>
                          (a_5 : Vect β n_3) → x_3 ≍ cons a_3 a_5 → motive n.succ (cons a a_2) x_3)
                          (fun a_5 h => ⋯ ▸ h_2 n a a_2 a_3 a_5) x a_4)
                    ⋯ ⋯)
              x_4 a_1)
        ⋯ ⋯)
```

--------------------------------

### Section with variables and definitions

Source: https://leanprover.github.io/theorem_proving_in_lean4/Interacting-with-Lean

An example demonstrating the use of sections, variables, and attributes in Lean.

```Lean
section
variable (x y : Nat)
def double := x + x
#check double y
double y : Nat
#check double (2 * x)
double (2 * x) : Nat
attribute [local simp] Nat.add_assoc Nat.add_comm Nat.add_left_comm
theorem t1 : double (x + y) = double x + double y :=
by
  simp [double]
-- All goals completed!
#check t1 y
t1 y : ∀ (y_1 : Nat), double (y + y_1) = double y + double y_1
#check t1 (2 * x)
t1 (2 * x) : ∀ (y : Nat), double (2 * x + y) = double (2 * x) + double y
theorem t2 : double (x * y) = double x * y :=
by
  simp [double, Nat.add_mul]
-- All goals completed!
end
```

--------------------------------

### Using the `show` tactic

Source: https://leanprover.github.io/theorem_proving_in_lean4/Tactics

An example demonstrating the use of the `show` tactic to rewrite a goal.

```Lean
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
by
  apply Iff.intro
  intro h
  cases h with | inl hq =>
    show (p ∧ q) ∨ (p ∧ r)
    exact Or.inl ⟨h.left, hq⟩
  | inr hr =>
    show (p ∧ q) ∨ (p ∧ r)
    exact Or.inr ⟨h.left, hr⟩
  intro h
  cases h with | inl hpq =>
    show p ∧ (q ∨ r)
    exact ⟨hpq.left, Or.inl hpq.right⟩
  | inr hpr =>
    show p ∧ (q ∨ r)
    exact ⟨hpr.left, Or.inr hpr.right⟩
```

--------------------------------

### Named Arguments Example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Interacting-with-Lean

Demonstrates the use of named arguments in a function definition and its application.

```Lean
def sum (xs : List Nat) := xs.foldl (init := 0) (·+·) ```10
#eval sum [1, 2, 3, 4]
````
```

--------------------------------

### Example with metavariable unification

Source: https://leanprover.github.io/theorem_proving_in_lean4/Tactics

Shows how the assumption tactic can unify metavariables in the conclusion.

```Lean
variable (x y z w : Nat)
example (h₁ : x = y) (h₂ : y = z) (h₃ : z = w) : x = w :=
by
x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ x = w
apply Eq.trans h₁
x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ x = ?b
x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ ?b = w
assumption
x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ ?b = w      -- solves x = ?b with h₁
apply Eq.trans h₂
x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ y = ?h₂.b
x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ ?h₂.b = w
assumption
x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ ?h₂.b = w      -- solves y = ?h₂.b with h₂
assumption
All goals completed! 🐙      -- solves z = w with h₃
```

--------------------------------

### Structural recursion example: addition

Source: https://leanprover.github.io/theorem_proving_in_lean4/Induction-and-Recursion

Definition of addition using the equation compiler, demonstrating structural recursion.

```Lean
open Nat
def add : Nat → Nat → Nat
  | m, zero => m
  | m, succ n => succ (add m n)
```

--------------------------------

### Specialized Equality Example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Quantifiers-and-Equality

An example specializing the transitivity and symmetry of equality.

```Lean
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)
example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```

--------------------------------

### Infix, Non-associative, and Prefix/Postfix Notations

Source: https://leanprover.github.io/theorem_proving_in_lean4/Interacting-with-Lean

Examples of defining different types of notations with precedences.

```Lean
infixl:65 " + " => HAdd.hAdd  -- left-associative
``infix:50 " = " => Eq         -- non-associative
``infixr:80 " ^ " => HPow.hPow  -- right-associative
``prefix:100 "-" => Neg.neg
``postfix:max "⁻¹" => Inv.inv
```

--------------------------------

### Setting Options

Source: https://leanprover.github.io/theorem_proving_in_lean4/Interacting-with-Lean

Syntax for setting Lean options to control behavior, with examples for pretty printing.

```lean
set_option <name> <value>
```

```lean
pp.explicit  : display implicit arguments
pp.universes : display hidden universe parameters
pp.notation  : display output using defined notations
```

```lean
set_option pp.explicit true 
set_option pp.universes true 
set_option pp.notation false 
```

```lean
@Eq.{1} Nat (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))) (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) : Prop
```

```lean
@Eq.{1} Nat
  (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat)
    (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
    (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
  (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) : Prop
```

```lean
@Eq.{1} (Nat → Nat) (fun x => @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))) fun x => @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x (@OfNat.ofNat.{0} Nat (nat_lit 3) (instOfNatNat (nat_lit 3)))
```

```lean
@Eq.{1} (Nat → Nat)
  (fun x =>
    @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x
      (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
  fun x =>
  @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x
    (@OfNat.ofNat.{0} Nat (nat_lit 3) (instOfNatNat (nat_lit 3)))
```

```lean
(fun x => @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))) (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))) : Nat
```

```lean
(fun x =>
    @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x
      (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
  (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))) : Nat
```

```lean
set_option pp.all true
set_option pp.all false
```

--------------------------------

### Namespace and Open Command Example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Interacting-with-Lean

Demonstrates the use of `namespace` to prepend a prefix to identifiers and `open` to create aliases.

```Lean
namespace Foo
def bar : Nat := 1
end Foo
open Foo

-- Check the aliased name
#check bar
```

```Lean
#check Foo.bar
```

--------------------------------

### Example using intros tactic

Source: https://leanprover.github.io/theorem_proving_in_lean4/Tactics

Demonstrates the intros tactic to automatically introduce variables and hypotheses.

```Lean
example : ∀ a b c : Nat, a = b → a = c → c = b :=
by
⊢ ∀ (a b c : Nat), a = b → a = c → c = b
intros a b c h₁ h₂
⊢ c = b
apply Eq.trans h₁
⊢ c = ?b
apply Eq.trans h₂
⊢ ?b = b
assumption
All goals completed! 🐙
```

--------------------------------

### Axiom Example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Propositions-and-Proofs

An example of an axiom `and_commut` which asserts a proof for the commutativity of conjunction.

```Lean
axiom and_commut (p q : Prop) : Proof (Implies (And p q) (And q p))
variable (p q : Prop)
and_commut p q : Proof (Implies (p ∧ q) (q ∧ p))
```

--------------------------------

### Example of `Nat.below 3`

Source: https://leanprover.github.io/theorem_proving_in_lean4/Induction-and-Recursion

Reducing the expression `@Nat.below C (3 : Nat)` to understand its structure.

```Lean
#reduce @Nat.below C (3 : Nat)
```

--------------------------------

### Existential Quantifier Example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Quantifiers-and-Equality

An example demonstrating the use of the existential quantifier (Exists) and its introduction.

```Lean
theorem gex4 : ∀ (g : Nat → Nat → Nat),
  @Eq Nat
      (g (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))
        (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))))
      (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) →
    @Exists Nat fun x => @Eq Nat (g x x) (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) :=
fun g hg =>
  @Exists.intro Nat (fun x => @Eq Nat (g x x) (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))))
    (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) hg
```

--------------------------------

### Splitting Conjunctions

Source: https://leanprover.github.io/theorem_proving_in_lean4/Tactics

An example demonstrating how to split conjunctions using tactics in Lean 4.

```Lean
example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r :=
by
constructor
left
assumption
right
constructor
left
assumption
right
constructor
left
assumption
right
assumption
```

--------------------------------

### Multiple alternatives with intro

Source: https://leanprover.github.io/theorem_proving_in_lean4/Tactics

Shows how to provide multiple alternatives using `intro` with pattern matching, similar to `match` expressions, for existential quantifiers with disjunctions.

```Lean
example (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x :=
by
  intro | ⟨w, Or.inl h⟩ =>
  exact ⟨w, Or.inr h⟩
  | ⟨w, Or.inr h⟩ =>
  exact ⟨w, Or.inl h⟩
```

--------------------------------

### Example Calculational Proof

Source: https://leanprover.github.io/theorem_proving_in_lean4/Quantifiers-and-Equality

An example demonstrating a calculational proof for a theorem involving equality.

```Lean
variable (a b c d e : Nat) 
theorem T (h1 : a = b) (h2 : b = c + 1) (h3 : c = d) (h4 : e = 1 + d) : a = e := calc a = b := h1
    _ = c + 1 := h2
    _ = d + 1 := congrArg Nat.succ h3
    _ = 1 + d := Nat.add_comm d 1
    _ = e := Eq.symm h4
```

--------------------------------

### Example Structure Declaration: Point

Source: https://leanprover.github.io/theorem_proving_in_lean4/Structures-and-Records

A simple example of a structure declaration for a 2D point.

```Lean
structure Point (α : Type u) where mk :: x : α y : α
```

--------------------------------

### Boolean Logic Functions

Source: https://leanprover.github.io/theorem_proving_in_lean4/Induction-and-Recursion

Examples of boolean 'and', 'or', and 'cond' functions using pattern matching.

```Lean
set_option linter.unusedVariables false
namespace Hidden
def and : Bool → Bool → Bool | true, a => a | false, _ => false
def or : Bool → Bool → Bool | true, _ => true | false, a => a
def cond : Bool → α → α → α | true, x, y => x | false, x, y => y
end Hidden
```

--------------------------------

### Equivalent Definitions using Match

Source: https://leanprover.github.io/theorem_proving_in_lean4/Induction-and-Recursion

Demonstrates different ways to define the same function, including using match expressions.

```Lean
def bar₁ : Nat × Nat → Nat | (m, n) => m + n 
def bar₂ (p : Nat × Nat) : Nat := match p with | (m, n) => m + n 
def bar₃ : Nat × Nat → Nat := fun (m, n) => m + n 
def bar₄ (p : Nat × Nat) : Nat := let (m, n) := p; m + n
```

--------------------------------

### Proof of p ∧ q → q ∧ p

Source: https://leanprover.github.io/theorem_proving_in_lean4/Propositions-and-Proofs

This example shows how to prove `p ∧ q → q ∧ p` using `And.intro`, `And.left`, and `And.right`.

```Lean
variable (p q : Prop)
example (h : p ∧ q) : q ∧ p := And.intro (And.right h) (And.left h)
```

--------------------------------

### Logical equivalence introduction

Source: https://leanprover.github.io/theorem_proving_in_lean4/Propositions-and-Proofs

Shows how to construct a proof of logical equivalence (p ↔ q) using Iff.intro from proofs of the forward (p → q) and backward (q → p) implications.

```Lean
variable (p q : Prop)
theorem and_swap : p ∧ q ↔ q ∧ p := Iff.intro (fun h : p ∧ q => show q ∧ p from And.intro (And.right h) (And.left h)) (fun h : q ∧ p => show p ∧ q from And.intro (And.right h) (And.left h))
```

--------------------------------

### Output Parameters Example 1

Source: https://leanprover.github.io/theorem_proving_in_lean4/Type-Classes

Demonstrates the use of output parameters in a heterogeneous polymorphic multiplication.

```Lean
namespace Ex 
class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where hMul : α → β → γ 
export HMul (hMul)
instance : HMul Nat Nat Nat where hMul := Nat.mul
instance : HMul Nat (Array Nat) (Array Nat) where hMul a bs := bs.map (fun b => hMul a b)
```
12
#eval hMul 4 3
```
```
```
#[8, 12, 16]
#eval hMul 4 #[2, 3, 4]
```

end Ex 
```

--------------------------------

### Proof of a property using induction

Source: https://leanprover.github.io/theorem_proving_in_lean4/Induction-and-Recursion

Proof of the property `f b1 b2 b3 b4 b5 = (b1 || b2 || b3 || b4 || b5)` using induction and the `simp_all` tactic.

```Lean
theorem f_or : f b1 b2 b3 b4 b5 = (b1 || b2 || b3 || b4 || b5) :=
by
b1:Bool
b2:Bool
b3:Bool
b4:Bool
b5:Bool
⊢ f b1 b2 b3 b4 b5 = (b1 || b2 || b3 || b4 || b5)
fun_cases f
case1
b2:Bool
b3:Bool
b4:Bool
b5:Bool
⊢ true = (true || b2 || b3 || b4 || b5)
case2
b1:Bool
b3:Bool
b4:Bool
b5:Bool
x✝:b1 = true → False
⊢ true = (b1 || true || b3 || b4 || b5)
case3
b1:Bool
b2:Bool
b4:Bool
b5:Bool
x✝¹:b1 = true → False
x✝:b2 = true → False
⊢ true = (b1 || b2 || true || b4 || b5)
case4
b1:Bool
b2:Bool
b3:Bool
b5:Bool
x✝²:b1 = true → False
x✝¹:b2 = true → False
x✝:b3 = true → False
⊢ true = (b1 || b2 || b3 || true || b5)
case5
b1:Bool
b2:Bool
b3:Bool
b4:Bool
b5:Bool
x✝³:b1 = true → False
x✝²:b2 = true → False
x✝¹:b3 = true → False
x✝:b4 = true → False
⊢ b5 = (b1 || b2 || b3 || b4 || b5)
<;>
case1
b2:Bool
b3:Bool
b4:Bool
b5:Bool
⊢ true = (true || b2 || b3 || b4 || b5)
case2
b1:Bool
b3:Bool
b4:Bool
b5:Bool
x✝:b1 = true → False
⊢ true = (b1 || true || b3 || b4 || b5)
case3
b1:Bool
b2:Bool
b4:Bool
b5:Bool
x✝¹:b1 = true → False
x✝:b2 = true → False
⊢ true = (b1 || b2 || true || b4 || b5)
case4
b1:Bool
b2:Bool
b3:Bool
b5:Bool
x✝²:b1 = true → False
x✝¹:b2 = true → False
x✝:b3 = true → False
⊢ true = (b1 || b2 || b3 || true || b5)
case5
b1:Bool
b2:Bool
b3:Bool
b4:Bool
b5:Bool
x✝³:b1 = true → False
x✝²:b2 = true → False
x✝¹:b3 = true → False
x✝:b4 = true → False
⊢ b5 = (b1 || b2 || b3 || b4 || b5)
simp_all
All goals completed! 🐙
```

--------------------------------

### Example Theorems for Point Structure

Source: https://leanprover.github.io/theorem_proving_in_lean4/Structures-and-Records

Example theorems demonstrating the properties of the Point structure's constructor.

```Lean
open Point
example (a b : α) : x (mk a b) = a := rfl
```

```Lean
open Point
example (a b : α) : y (mk a b) = b := rfl
```

--------------------------------

### Sum Type Example using `Sum.casesOn`

Source: https://leanprover.github.io/theorem_proving_in_lean4/Inductive-Types

An example demonstrating the use of `Sum.casesOn` to define a function on the sum type.

```Lean
def sum_example (s : Sum Nat Nat) : Nat := Sum.casesOn (motive := fun _ => Nat) s (fun n => 2 * n) (fun n => 2 * n + 1)
```

```Lean
#eval sum_example (Sum.inl 3)
```

```Lean
#eval sum_example (Sum.inr 3)
```

--------------------------------

### Logical equivalence introduction (concise)

Source: https://leanprover.github.io/theorem_proving_in_lean4/Propositions-and-Proofs

A concise version of constructing a proof for logical equivalence using anonymous constructor notation.

```Lean
variable (p q : Prop)
theorem and_swap : p ∧ q ↔ q ∧ p := ⟨ fun h => ⟨h.right, h.left⟩, fun h => ⟨h.right, h.left⟩ ⟩
```

--------------------------------

### Product Type Example using `Prod.casesOn`

Source: https://leanprover.github.io/theorem_proving_in_lean4/Inductive-Types

An example demonstrating the use of `Prod.casesOn` to define a function on the product type.

```Lean
def prod_example (p : Bool × Nat) : Nat := Prod.casesOn (motive := fun _ => Nat) p (fun b n => cond b (2 * n) (2 * n + 1))
```

```Lean
#eval prod_example (true, 3)
```

```Lean
#eval prod_example (false, 3)
```

--------------------------------

### Example of #guard_msgs capturing all messages

Source: https://leanprover.github.io/theorem_proving_in_lean4/Interacting-with-Lean

This example demonstrates #guard_msgs capturing both an error and a warning when evaluating an expression that uses 'sorry'.

```Lean
/- error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.  To attempt to evaluate anyway despite the risks, use the '#eval!' command. --- warning: declaration uses 'sorry' -/ `❌️ Docstring on `#guard_msgs` does not match generated message:  - error: aborting evaluation since the expression depends on the - 'sorry' axiom, which can lead to runtime instability and crashes. + warning: declaration uses 'sorry' + --- + error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.   - To attempt to evaluate anyway despite the risks, use the '#eval!' - command. - --- - warning: declaration uses 'sorry' + To attempt to evaluate anyway despite the risks, use the '#eval!' command. `#guard_msgs in `declaration uses 'sorry'``aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.  To attempt to evaluate anyway despite the risks, use the '#eval!' command.`#eval (sorry : Nat)``
```

--------------------------------

### Example using `calc` for algebraic expansion

Source: https://leanprover.github.io/theorem_proving_in_lean4/Quantifiers-and-Equality

Demonstrates using `calc` to prove an algebraic identity for `(x + y) * (x + y)`.

```Lean
variable (x y : Nat)
example : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
calc (x + y) * (x + y) = (x + y) * x + (x + y) * y :=
  by
    x:Nat
    y:Nat
    ⊢ (x + y) * (x + y) = (x + y) * x + (x + y) * y
  rw [Nat.mul_add]
-- All goals completed! 🐙
_ = x * x + y * x + (x + y) * y :=
  by
    x:Nat
    y:Nat
    ⊢ (x + y) * (x + y) = (x + y) * x + (x + y) * y
  rw [Nat.mul_add]
-- All goals completed! 🐙
_ = x * x + y * x + (x * y + y * y) :=
  by
    x:Nat
    y:Nat
    ⊢ (x + y) * (x + y) = (x + y) * x + (x + y) * y
  rw [Nat.mul_add]
-- All goals completed! 🐙
_ = x * x + y * x + x * y + y * y :=
  by
    x:Nat
    y:Nat
    ⊢ (x + y) * (x + y) = (x + y) * x + (x + y) * y
  rw [←Nat.add_assoc]
-- All goals completed! 🐙
```

--------------------------------

### Example of #guard_msgs for a type error

Source: https://leanprover.github.io/theorem_proving_in_lean4/Interacting-with-Lean

This example demonstrates how to use #guard_msgs to check for a specific type error when defining a variable.

```Lean
/- error: Type mismatch   "Not a number" has type   String but is expected to have type   Nat -/ #guard_msgs in def x : Nat := "Not a number"
```

--------------------------------

### Sample Term and Evaluation

Source: https://leanprover.github.io/theorem_proving_in_lean4/Induction-and-Recursion

A sample `Term` and an evaluation of `numConsts` on it.

```Lean
def sample := app "f" [app "g" [const "x"], const "y"]

#eval numConsts sample
```

--------------------------------

### Output Parameters Example 2

Source: https://leanprover.github.io/theorem_proving_in_lean4/Type-Classes

Extends the heterogeneous polymorphic multiplication to include Int and demonstrates chaining instances.

```Lean
namespace Ex 
class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where hMul : α → β → γ 
export HMul (hMul)
instance : HMul Nat Nat Nat where hMul := Nat.mul
instance : HMul Int Int Int where hMul := Int.mul
instance [HMul α β γ] : HMul α (Array β) (Array γ) where hMul a bs := bs.map (fun b => hMul a b)
```
12
#eval hMul 4 3
```
```
```
#[8, 12, 16]
#eval hMul 4 #[2, 3, 4]
```
```
```
#[-6, 2, -8]
#eval hMul (-2) #[3, -1, 4]
```
```
```
#[#[4, 6], #[0, 8]]
#eval hMul 2 #[#[2, 3], #[0, 4]]
```

end Ex 
```

--------------------------------

### More natural example of mixing term-style and tactic-style proofs

Source: https://leanprover.github.io/theorem_proving_in_lean4/Tactics

A more natural example of mixing term-style and tactic-style proofs.

```Lean
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
by
  apply Iff.intro
  intro h
  cases h with | inl hq =>
    exact Or.inl ⟨h.left, hq⟩
  | inr hr =>
    exact Or.inr ⟨h.left, hr⟩
  intro h
  cases h with | inl hpq =>
    exact ⟨hpq.left, Or.inl hpq.right⟩
  | inr hpr =>
    exact ⟨hpr.left, Or.inr hpr.right⟩
```

--------------------------------

### CoeSort Example

Source: https://leanprover.github.io/theorem_proving_in_lean4/Type-Classes

This example demonstrates how to define a coercion for Semigroup to its carrier type, allowing `a : S` instead of `a : S.carrier`.

```Lean
structure Semigroup where
  carrier : Type u
  mul : carrier → carrier → carrier
  mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)

instance (S : Semigroup) : Mul S.carrier where
  mul a b := S.mul a b

instance : CoeSort Semigroup (Type u) where
  coe s := s.carrier

example (S : Semigroup) (a b c : S) : (a * b) * c = a * (b * c) :=
  Semigroup.mul_assoc _ a b c
```
Tokens:
Raw