* 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]]