Hermes Agent
6e2914b06e
Converted with pandoc 3.7 (markdown → org), all 17 files: - README, references, 15 tutorial units - Internal file links updated from .md to .org - Source code blocks (#+begin_src lean) preserved - Tables, math notation, links intact For the Emacs workflow.
114 lines
3.2 KiB
Org Mode
114 lines
3.2 KiB
Org Mode
* 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]]
|