Formal mathematics laboratory
Function machines in sequence
/-- "Do `f`, then `g`": the function that sends `a` to `g (f a)`. It can only be formed when the
outputs of `f` (of type `β`) are inputs that `g` accepts. -/
def andThen {α β γ : Type} (f : α → β) (g : β → γ) : α → γ := fun a => g (f a)/-- Our `andThen f g` is the function Lean's library writes `g ∘ f`, read "`g` after `f`".
They agree by definition, so `rfl` proves it. -/
theorem and_then_eq_comp {α β γ : Type} (f : α → β) (g : β → γ) : andThen f g = g ∘ f := rfl/-- "Add 3, then double" sends `x` to `2(x + 3) = 2x + 6`. -/
theorem add_then_double (x : Int) : andThen (fun n => n + 3) (fun n => 2 * n) x = 2 * x + 6 := by
show 2 * (x + 3) = 2 * x + 6
omega/-- "Double, then add 3" sends `x` to `2x + 3`. -/
theorem double_then_add (x : Int) : andThen (fun n => 2 * n) (fun n => n + 3) x = 2 * x + 3 := by
show 2 * x + 3 = 2 * x + 3
rfl/-- **Order matters**: "add 3, then double" and "double, then add 3" are different functions.
One input is enough to tell them apart: at `0` they give `6` and `3`. -/
theorem order_matters :
andThen (fun n : Int => n + 3) (fun n => 2 * n) ≠ andThen (fun n : Int => 2 * n) (fun n => n + 3) := by
intro h
have h0 := congrFun h 0
rw [add_then_double, double_then_add] at h0
omega/-- **When can "add `a`" and "multiply by `m`" be swapped?** "Add `a`, then multiply by `m`" gives
`m(x + a) = mx + ma`, while "multiply by `m`, then add `a`" gives `mx + a`. They agree for every
`x` exactly when `ma = a`, that is, when `a = 0` or `m = 1`. -/
theorem add_mul_swap_iff (a m : Int) :
(∀ x, andThen (fun n => n + a) (fun n => m * n) x = andThen (fun n => m * n) (fun n => n + a) x)
↔ a = 0 ∨ m = 1 := by
constructor
· intro h
-- At `x = 0` the two chains give `m · a` and `a`.
have h0 : m * (0 + a) = m * 0 + a := h 0
have hma : (m - 1) * a = 0 := by
rw [Int.sub_mul, Int.one_mul]
rw [Int.zero_add, Int.mul_zero, Int.zero_add] at h0
omega
cases Int.mul_eq_zero.mp hma with
| inl hm => exact Or.inr (by omega)
| inr ha => exact Or.inl ha
· intro h x
show m * (x + a) = m * x + a
cases h with
| inl ha => rw [ha, Int.add_zero, Int.add_zero]
| inr hm => rw [hm, Int.one_mul, Int.one_mul]/-- Doing nothing first changes nothing: "identity, then `f`" is `f`. -/
theorem id_and_then {α β : Type} (f : α → β) : andThen id f = f := rfl/-- Doing nothing afterwards changes nothing: "`f`, then identity" is `f`. -/
theorem and_then_id {α β : Type} (f : α → β) : andThen f id = f := rfl/-- `g` **undoes** `f` if doing `f` and then `g` always gives back the input: `g (f a) = a`. -/
def Undoes {α β : Type} (g : β → α) (f : α → β) : Prop := ∀ a, g (f a) = a/-- "Subtract 3" undoes "add 3" … -/
theorem sub_undoes_add : Undoes (fun x : Int => x - 3) (fun x => x + 3) := by
intro a
show a + 3 - 3 = a
omega/-- … and "add 3" undoes "subtract 3". Each undoes the other: they are **inverse** functions. -/
theorem add_undoes_sub : Undoes (fun x : Int => x + 3) (fun x => x - 3) := by
intro a
show a - 3 + 3 = a
omega/-- On the rational numbers, "halve" undoes "double" and "double" undoes "halve": `x ↦ 2x` and
`x ↦ x / 2` are inverse functions of `ℚ`. -/
theorem halve_undoes_double :
Undoes (fun x : Rat => x / 2) (fun x => 2 * x) ∧ Undoes (fun x : Rat => 2 * x) (fun x => x / 2) := by
constructor
· intro a
show 2 * a / 2 = a
grind
· intro a
show 2 * (a / 2) = a
grind/-- On the integers, halving *with rounding down* (Lean's `y / 2`) still undoes doubling:
`(2x) / 2 = x`. This applies core Lean's `Int.mul_ediv_cancel_left`. -/
theorem int_halve_undoes_double : Undoes (fun y : Int => y / 2) (fun x => 2 * x) :=
fun x => Int.mul_ediv_cancel_left x (by decide)/-- … but on the integers doubling does **not** undo halving: `1` is halved (rounding down) to
`0`, and doubling `0` gives `0`, not `1`. So `x ↦ 2x` has no inverse function `ℤ → ℤ`: odd
numbers are never outputs, so nothing can be sent back to them. -/
theorem int_double_not_undoes_halve : ¬ Undoes (fun x : Int => 2 * x) (fun y => y / 2) := by
intro h
have h1 : 2 * (1 / 2 : Int) = 1 := h 1
exact absurd h1 (by decide)/-- **Socks and shoes.** If `f'` undoes `f` and `g'` undoes `g`, then "`f`, then `g`" is undone by
"`g'`, then `f'`": undo the **last** step **first**. The calculation:
`f' (g' (g (f a))) = f' (f a) = a`. -/
theorem undo_chain {α β γ : Type} {f : α → β} {g : β → γ} {f' : β → α} {g' : γ → β}
(hf : Undoes f' f) (hg : Undoes g' g) : Undoes (andThen g' f') (andThen f g) := by
intro a
calc andThen g' f' (andThen f g a) = f' (g' (g (f a))) := rfl
_ = f' (f a) := by rw [hg (f a)]
_ = a := hf a/-- Celsius to Fahrenheit: multiply by `9/5`, then add `32`. -/
def toFahrenheit : Rat → Rat := andThen (fun c => 9 / 5 * c) (fun x => x + 32)/-- Fahrenheit to Celsius: subtract `32`, then multiply by `5/9` — the undoing steps, in reverse
order. -/
def toCelsius : Rat → Rat := andThen (fun f => f - 32) (fun x => 5 / 9 * x)/-- A warm day: `30 °C` is `86 °F`, and converting back gives `30 °C` again. Lean checks the
fraction arithmetic exactly (`decide +kernel` evaluates both sides). -/
theorem thirty_degrees : toFahrenheit 30 = 86 ∧ toCelsius 86 = 30 := by
decide +kernel/-- `toCelsius` undoes `toFahrenheit` for **every** temperature. This is the socks-and-shoes rule
`undo_chain` applied to the two steps: `× 5/9` undoes `× 9/5`, and `− 32` undoes `+ 32`. -/
theorem to_celsius_undoes : Undoes toCelsius toFahrenheit := by
apply undo_chain
· intro c
show 5 / 9 * (9 / 5 * c) = c
grind
· intro x
show x + 32 - 32 = x
grind/-- Undoing the steps in the **wrong** order fails: "multiply by `5/9`, then subtract `32`" does
not undo `toFahrenheit`. At `0 °C`: `toFahrenheit 0 = 32`, and `5/9 · 32 − 32 = −128/9 ≠ 0`. -/
theorem wrong_order_fails :
¬ Undoes (andThen (fun x : Rat => 5 / 9 * x) (fun x => x - 32)) toFahrenheit := by
intro h
have h0 := h 0
revert h0
decide +kernel/-- If `f` can be undone, then different inputs always give different outputs: from
`f a = f b`, apply the undoing function `g` to both sides to get `a = g (f a) = g (f b) = b`. -/
theorem injective_of_undoes {α β : Type} {f : α → β} {g : β → α} (h : Undoes g f) (a b : α)
(hab : f a = f b) : a = b :=
calc a = g (f a) := (h a).symm
_ = g (f b) := by rw [hab]
_ = b := h b/-- The same fact from core Lean's library, where "`g` undoes `f`" is called
`Function.LeftInverse g f` (it is defined exactly like our `Undoes g f`) and "never sends two
inputs to the same output" is `Function.Injective f`. This applies
`Function.LeftInverse.injective`. -/
theorem injective_of_undoes_library {α β : Type} {f : α → β} {g : β → α} (h : Undoes g f) :
Function.Injective f :=
Function.LeftInverse.injective h/-- **Squaring on ℤ cannot be undone**: `2² = (−2)² = 4`, so an undoing function would have to
send `4` back to both `2` and `−2`. -/
theorem square_cannot_be_undone : ¬ ∃ g : Int → Int, Undoes g (fun x => x * x) := by
intro ⟨g, hg⟩
have h : (2 : Int) = -2 := injective_of_undoes hg 2 (-2) (by decide)
exact absurd h (by decide)Each exercise contains a sorry for you to replace. Open it in the Lean web editor, or clone the repository and run lake build.
/-- Show that "add 3" undoes "subtract 3".
Hint: `intro a`, then `show a - 3 + 3 = a` to unfold the definitions, and finish with `omega`. -/
theorem add_undoes_sub : Undoes (fun x : Int => x + 3) (fun x => x - 3) := by
sorry/-- … and "add 3" undoes "subtract 3". Each undoes the other: they are **inverse** functions. -/
theorem add_undoes_sub : Undoes (fun x : Int => x + 3) (fun x => x - 3) := by
intro a
show a - 3 + 3 = a
omega/-- Socks and shoes: "`f`, then `g`" is undone by "`g'`, then `f'`".
Hint: `intro a`. The goal unfolds to `f' (g' (g (f a))) = a`. Rewrite with `hg (f a)`, which says
`g' (g (f a)) = f a`, and finish with `hf a`. You may need `show f' (g' (g (f a))) = a` first. -/
theorem undo_chain {α β γ : Type} {f : α → β} {g : β → γ} {f' : β → α} {g' : γ → β}
(hf : Undoes f' f) (hg : Undoes g' g) : Undoes (andThen g' f') (andThen f g) := by
sorry/-- **Socks and shoes.** If `f'` undoes `f` and `g'` undoes `g`, then "`f`, then `g`" is undone by
"`g'`, then `f'`": undo the **last** step **first**. The calculation:
`f' (g' (g (f a))) = f' (f a) = a`. -/
theorem undo_chain {α β γ : Type} {f : α → β} {g : β → γ} {f' : β → α} {g' : γ → β}
(hf : Undoes f' f) (hg : Undoes g' g) : Undoes (andThen g' f') (andThen f g) := by
intro a
calc andThen g' f' (andThen f g a) = f' (g' (g (f a))) := rfl
_ = f' (f a) := by rw [hg (f a)]
_ = a := hf a