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.
61 lines
1.5 KiB
Org Mode
61 lines
1.5 KiB
Org Mode
* Unit 5 --- Advanced Tactics
|
||
:PROPERTIES:
|
||
:CUSTOM_ID: unit-5-advanced-tactics
|
||
:END:
|
||
*Tutorial 1: Lean 4 Fundamentals* · [[../README.org][← Back to README]]
|
||
|
||
** Goals
|
||
:PROPERTIES:
|
||
:CUSTOM_ID: goals
|
||
:END:
|
||
- Prove properties by induction with =induction=
|
||
- Use =simp=, =ring=, =omega= for automation
|
||
- Use =rcases= and =obtain= for case analysis
|
||
- Work with =Nat= arithmetic proofs
|
||
|
||
** Sources
|
||
:PROPERTIES:
|
||
:CUSTOM_ID: sources
|
||
:END:
|
||
- TPIL Chapters 5--6 → https://leanprover.github.io/theorem_proving_in_lean4/
|
||
- /Mathematics in Lean/ (MiL), Chapter 1 → https://leanprover-community.github.io/mathematics_in_lean/
|
||
|
||
** Exercises
|
||
:PROPERTIES:
|
||
:CUSTOM_ID: exercises
|
||
:END:
|
||
#+begin_src lean
|
||
open Nat
|
||
|
||
-- 5.1 — Induction on naturals
|
||
theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := by
|
||
sorry
|
||
|
||
theorem add_comm (a b : Nat) : a + b = b + a := by
|
||
sorry
|
||
|
||
theorem mul_comm (a b : Nat) : a * b = b * a := by
|
||
sorry
|
||
|
||
theorem zero_mul (n : Nat) : 0 * n = 0 := by
|
||
sorry
|
||
|
||
-- 5.2 — Induction on lists
|
||
theorem reverse_reverse (xs : List α) : xs.reverse.reverse = xs := by
|
||
sorry
|
||
|
||
theorem length_append (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by
|
||
sorry
|
||
|
||
theorem map_id (xs : List α) : xs.map id = xs := by
|
||
sorry
|
||
|
||
-- 5.3 — Using `simp` and `ring`
|
||
theorem square_sum (a b : Nat) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
|
||
sorry
|
||
#+end_src
|
||
|
||
--------------
|
||
|
||
← [[file:04-quantifiers-and-equality.org][Previous: Unit 4]] · Next: [[file:06-structures-type-classes.org][Unit 6 --- Structures and Type Classes]]
|