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.
1.5 KiB
1.5 KiB
Unit 5 — Advanced Tactics
Tutorial 1: Lean 4 Fundamentals · ← Back to README
Goals
- Prove properties by induction with
induction - Use
simp,ring,omegafor automation - Use
rcasesandobtainfor case analysis - Work with
Natarithmetic proofs
Sources
- 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
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← Previous: Unit 4 · Next: Unit 6 — Structures and Type Classes