* Unit 4 --- Quantifiers and Equality
:PROPERTIES:
:CUSTOM_ID: unit-4-quantifiers-and-equality
:END:
*Tutorial 1: Lean 4 Fundamentals* · [[../README.org][← Back to README]]

** Goals
:PROPERTIES:
:CUSTOM_ID: goals
:END:
- Use =∀= (forall) and =∃= (exists) quantifiers
- Manipulate equality with =rfl=, =rw=, =calc=
- Combine quantifiers with logical connectives

** Source
:PROPERTIES:
:CUSTOM_ID: source
:END:
/Theorem Proving in Lean 4/ (TPIL), Chapter 4
→ https://leanprover.github.io/theorem_proving_in_lean4/

** Concepts
:PROPERTIES:
:CUSTOM_ID: concepts
:END:
| Concept                | Lean                                                 |
|------------------------+------------------------------------------------------|
| Universal =∀ x, P x=   | =intro x= to prove; =h x= or =apply h= to use        |
| Existential =∃ x, P x= | =⟨x, h⟩= to prove; =rcases h with ⟨x, hx⟩= to use    |
| Equality =a = b=       | =rfl= when definitional; =rw [h]= when propositional |
| =calc= block           | Chain equalities: =calc a = b := h1; _ = c := h2=    |

** Exercises
:PROPERTIES:
:CUSTOM_ID: exercises
:END:
*** Exercise 4.1 --- Universal quantifier
:PROPERTIES:
:CUSTOM_ID: exercise-4.1-universal-quantifier
:END:
#+begin_src lean
-- (a) Prove a simple forall
theorem all_imp (P Q : Nat → Prop) (h : ∀ n, P n → Q n) (x : Nat) (hp : P x) : Q x :=
  by
    sorry

-- (b) Distributing ∀ over ∧
theorem forall_and_distrib (P Q : Nat → Prop) : (∀ n, P n ∧ Q n) ↔ (∀ n, P n) ∧ (∀ n, Q n) :=
  by
    constructor
    · sorry  -- left-to-right
    · sorry  -- right-to-left

-- (c) Prove that if every natural is even, then 42 is even
-- (Use: `Even n := ∃ k, n = 2*k`)
def Even (n : Nat) : Prop := ∃ k, n = 2 * k

theorem all_even_implies_42 : (∀ n, Even n) → Even 42 :=
  by
    sorry
#+end_src

*** Exercise 4.2 --- Existential quantifier
:PROPERTIES:
:CUSTOM_ID: exercise-4.2-existential-quantifier
:END:
#+begin_src lean
-- (a) Prove existence
theorem exists_square (a : Nat) : ∃ n, n = a * a :=
  by
    sorry

-- (b) Distributing ∃ over ∨
theorem exists_or_distrib (P Q : Nat → Prop) : (∃ n, P n ∨ Q n) ↔ (∃ n, P n) ∨ (∃ n, Q n) :=
  by
    constructor
    · sorry
    · sorry

-- (c) Prove: if something is both even and greater than 10, then something is greater than 5
theorem even_and_gt10_implies_gt5 : (∃ n, Even n ∧ n > 10) → (∃ n, n > 5) :=
  by
    sorry
#+end_src

*** Exercise 4.3 --- Equality and rewriting
:PROPERTIES:
:CUSTOM_ID: exercise-4.3-equality-and-rewriting
:END:
#+begin_src lean
-- (a) Prove symmetry and transitivity of equality (without using `symm`/`trans`)
theorem eq_symm {α : Type} (a b : α) (h : a = b) : b = a :=
  by
    sorry

theorem eq_trans {α : Type} (a b c : α) (h1 : a = b) (h2 : b = c) : a = c :=
  by
    sorry

-- (b) Use `calc` to prove a chain of identities
theorem calc_example (a b c d : Nat) (h1 : a = b) (h2 : b = c + 1) (h3 : c + 1 = d) : a = d :=
  by
    sorry

-- (c) Rewrite inside a goal
theorem rewrite_example (a b : Nat) (h : a = b + 1) : a * 2 = (b + 1) * 2 :=
  by
    sorry
#+end_src

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

← [[file:03-propositions-and-proofs.org][Previous: Unit 3]] · Next: [[file:05-advanced-tactics.org][Unit 5 --- Advanced Tactics]]