Formal mathematics laboratory
One thing after another
/-- `andThen f g` is the chain "do `f`, then do `g` to the result". Later you will meet it
written `g ∘ f`, read "`g` after `f`". -/
def andThen {α : Type} (f g : α → α) : α → α := fun x => g (f x)/-- The action "add 5". -/
def addFive (n : Nat) : Nat := n + 5/-- The action "double". -/
def double (n : Nat) : Nat := 2 * n/-- Starting at 3: "add 5, then double" goes 3 → 8 → 16, but "double, then add 5" goes
3 → 6 → 11. -/
theorem start_at_three : andThen addFive double 3 = 16 ∧ andThen double addFive 3 = 11 := by
decide/-- For **every** starting number `n`, "add 5, then double" gives exactly 5 more than "double,
then add 5": doubling `n + 5` doubles the 5 as well, giving `2 × n + 10` instead of
`2 × n + 5`. -/
theorem add_then_double (n : Nat) :
andThen addFive double n = andThen double addFive n + 5 := by
unfold andThen addFive double
omega/-- So the two orders **never** give the same result, whatever number you start with. -/
theorem never_agree (n : Nat) : andThen addFive double n ≠ andThen double addFive n := by
rw [add_then_double]
omega/-- But some actions can be done in either order: "add `a`, then add `b`" is the same action as
"add `b`, then add `a`", for every starting number. -/
theorem adding_commutes (a b : Nat) :
andThen (· + a) (· + b) = andThen (· + b) (· + a) := by
funext n
show n + a + b = n + b + a
omega/-- Likewise "multiply by `a`, then by `b`" is the same as "multiply by `b`, then by `a`". This
applies core Lean's `Nat.mul_right_comm`. -/
theorem multiplying_commutes (a b : Nat) :
andThen (· * a) (· * b) = andThen (· * b) (· * a) := by
funext n
exact Nat.mul_right_comm n a b/-- `Undoes u f` says that the action `u` undoes the action `f`: doing `f` and then `u` puts
every thing back exactly as it was. -/
def Undoes {α : Type} (u f : α → α) : Prop := ∀ x, u (f x) = x/-- **The socks-and-shoes rule.** If `uf` undoes `f` and `ug` undoes `g`, then the chain
"`f`, then `g`" is undone by "`ug`, then `uf`" — undo the **last** action first. After `f` and
`g`, undoing `g` takes us back to just after `f`; then undoing `f` takes us back to the
start. -/
theorem socks_and_shoes {α : Type} {f g uf ug : α → α}
(hf : Undoes uf f) (hg : Undoes ug g) : Undoes (andThen ug uf) (andThen f g) := by
intro x
unfold andThen
rw [hg (f x), hf x]/-- The action "halve" on whole numbers (Lean rounds an odd number down). -/
def halve (n : Nat) : Nat := n / 2/-- The action "subtract 5" on whole numbers (Lean stops at 0). -/
def subFive (n : Nat) : Nat := n - 5/-- Halving undoes doubling. -/
theorem halve_undoes_double : Undoes halve double := by
intro n
unfold halve double
omega/-- Subtracting 5 undoes adding 5. -/
theorem subFive_undoes_addFive : Undoes subFive addFive := by
intro n
unfold subFive addFive
omega/-- "Add 5, then double" is undone by "halve, then subtract 5" — the undoing actions in reverse
order. This is the socks-and-shoes rule applied to the two facts above. -/
theorem undo_addFive_then_double : Undoes (andThen halve subFive) (andThen addFive double) :=
socks_and_shoes subFive_undoes_addFive halve_undoes_double/-- Undoing in the original order does **not** work: "subtract 5, then halve" does not undo
"add 5, then double". From 3 the chain reaches 16, and 16 − 5 = 11 is odd, so halving cannot
give back 3. -/
theorem wrong_order_fails : ¬ Undoes (andThen subFive halve) (andThen addFive double) := by
intro h
have h3 := h 3
revert h3
decide/-- The four directions an arrow on a card can point. -/
inductive Dir where
| up | right | down | left
deriving DecidableEq, Repr/-- A quarter turn clockwise (the way clock hands go). -/
def quarterTurn : Dir → Dir
| .up => .right
| .right => .down
| .down => .left
| .left => .up/-- Four quarter turns, one after another, have the same effect as doing nothing: a full
turn. There are only four directions to check. -/
theorem four_quarter_turns (d : Dir) :
quarterTurn (quarterTurn (quarterTurn (quarterTurn d))) = d := by
cases d <;> rfl/-- So a quarter turn is undone by **three more** quarter turns. -/
theorem three_more_turns_undo :
Undoes (andThen quarterTurn (andThen quarterTurn quarterTurn)) quarterTurn := by
intro d
cases d <;> rfl/-- A quarter turn clockwise about the corner `(0, 0)`, acting on a point `(x, y)` of the grid
(with `y` going up): it sends `(x, y)` to `(y, −x)`, so "up" `(0, 1)` goes to "right"
`(1, 0)`. -/
def turnPoint (p : Int × Int) : Int × Int := (p.2, -p.1)/-- Flipping a tile over, left to right: the mirror image in the up–down line through
`(0, 0)`. -/
def flipPoint (p : Int × Int) : Int × Int := (-p.1, p.2)/-- An L-shaped tile, as the grid points it covers: a bar from `(0, 0)` up to `(0, 2)` and a
foot out to `(1, 0)`. -/
def lShape : List (Int × Int) := [(0, 2), (0, 1), (0, 0), (1, 0)]/-- **Turning and flipping do not commute.** "Turn, then flip" moves the L so that it covers
the point `(−1, 0)`; "flip, then turn" leaves that point empty. So the two chains put the
tile in different positions. -/
theorem turn_flip_differ :
((-1, 0) : Int × Int) ∈ lShape.map (andThen turnPoint flipPoint) ∧
((-1, 0) : Int × Int) ∉ lShape.map (andThen flipPoint turnPoint) := by
decide/-- Four quarter turns move every point of the grid back to where it started:
`(x, y) → (y, −x) → (−x, −y) → (−y, x) → (x, y)`. -/
theorem four_turns_points (p : Int × Int) :
turnPoint (turnPoint (turnPoint (turnPoint p))) = p := by
obtain ⟨x, y⟩ := p
simp [turnPoint]/-- A step that can be undone: an action `act`, an action `back`, and a guarantee that `back`
undoes `act`. -/
structure Step (α : Type) where
act : α → α
back : α → α
back_act : ∀ x, back (act x) = x/-- Follow a chain of steps, first to last. -/
def runSteps {α : Type} : List (Step α) → α → α
| [], x => x
| s :: ss, x => runSteps ss (s.act x)/-- Undo a chain of steps: undo all the *later* steps first, and the first step last. -/
def undoSteps {α : Type} : List (Step α) → α → α
| [], x => x
| s :: ss, x => s.back (undoSteps ss x)/-- **Undoing in reverse order works for chains of any length.** Proved by working through the
chain: undoing the rest of the chain takes us back to just after the first step, and undoing
the first step takes us back to the start. -/
theorem undo_run {α : Type} (ss : List (Step α)) (x : α) : undoSteps ss (runSteps ss x) = x := by
induction ss generalizing x with
| nil => rfl
| cons s ss ih =>
simp only [runSteps, undoSteps]
rw [ih, s.back_act]/-- "Add 5", with its undo "subtract 5". -/
def addFiveStep : Step Nat := ⟨addFive, subFive, subFive_undoes_addFive⟩/-- "Double", with its undo "halve". -/
def doubleStep : Step Nat := ⟨double, halve, halve_undoes_double⟩/-- There and back again: the chain add 5, double, add 5 takes 3 to 21, and undoing it in
reverse order (subtract 5, halve, subtract 5) brings 21 back to 3. -/
theorem there_and_back :
runSteps [addFiveStep, doubleStep, addFiveStep] 3 = 21 ∧
undoSteps [addFiveStep, doubleStep, addFiveStep] 21 = 3 := by
decideEach exercise contains a sorry for you to replace. Open it in the Lean web editor, or clone the repository and run lake build.
/-- Starting at 3, check where the two chains end.
Hint: Lean can follow the chains itself — try `decide`. -/
theorem start_at_three : andThen addFive double 3 = 16 ∧ andThen double addFive 3 = 11 := by
sorry/-- Starting at 3: "add 5, then double" goes 3 → 8 → 16, but "double, then add 5" goes
3 → 6 → 11. -/
theorem start_at_three : andThen addFive double 3 = 16 ∧ andThen double addFive 3 = 11 := by
decide/-- Show that four quarter turns do nothing.
Hint: there are only four directions. `cases d <;> rfl` checks each one. -/
theorem four_quarter_turns (d : Dir) :
quarterTurn (quarterTurn (quarterTurn (quarterTurn d))) = d := by
sorry/-- Four quarter turns, one after another, have the same effect as doing nothing: a full
turn. There are only four directions to check. -/
theorem four_quarter_turns (d : Dir) :
quarterTurn (quarterTurn (quarterTurn (quarterTurn d))) = d := by
cases d <;> rfl/-- Prove the socks-and-shoes rule.
Hint: after `intro x` and `unfold andThen`, the goal is `uf (ug (g (f x))) = x`. Rewrite with
`hg (f x)` (taking off the shoes) and then with `hf x` (taking off the socks). -/
theorem socks_and_shoes {α : Type} {f g uf ug : α → α}
(hf : Undoes uf f) (hg : Undoes ug g) : Undoes (andThen ug uf) (andThen f g) := by
sorry/-- **The socks-and-shoes rule.** If `uf` undoes `f` and `ug` undoes `g`, then the chain
"`f`, then `g`" is undone by "`ug`, then `uf`" — undo the **last** action first. After `f` and
`g`, undoing `g` takes us back to just after `f`; then undoing `f` takes us back to the
start. -/
theorem socks_and_shoes {α : Type} {f g uf ug : α → α}
(hf : Undoes uf f) (hg : Undoes ug g) : Undoes (andThen ug uf) (andThen f g) := by
intro x
unfold andThen
rw [hg (f x), hf x]