Lean for All

Day 13: Rewriting and automation🔗

Follow rw in both directions, and judge what simp, omega and decide really show.

With an equation h : x = y + 1, rw [h] rewrites the goal: every x becomes y + 1.

theorem double (x y : Nat) (h : x = y + 1) : x * 2 = y * 2 + 2 := x:Naty:Nath:x = y + 1⊢ x * 2 = y * 2 + 2 x:Naty:Nath:x = y + 1⊢ (y + 1) * 2 = y * 2 + 2 All goals completed! 🐙 
x y : Nat
h : x = y + 1
⊢ x * 2 = y * 2 + 2

becomes

x y : Nat
h : x = y + 1
⊢ (y + 1) * 2 = y * 2 + 2

rw replaces the left side of the equation by the right side. After rewriting, it also tries rfl, so it sometimes finishes the goal by itself.

To go the other way, right side to left side, write rw [← h]:

theorem move (a b : Nat) (h : a = b) (ha : a > 3) : b > 3 := a:Natb:Nath:a = bha:a > 3⊢ b > 3 a:Natb:Nath:a = bha:a > 3⊢ a > 3 All goals completed! 🐙

With h : a = b, rw [← h] turns every b into a: the goal goes from ⊢ b > 3 to ⊢ a > 3, which is ha. Plain rw [h] would look for a in the goal, find none, and fail.

Some tactics do a lot of work at once. This is called automation:

  • decide: computes the answer for specific numbers.

  • omega: solves arithmetic with +, -, constants and comparisons, using the hypotheses.

  • simp: simplifies the goal using many known facts. It may finish, or leave a simpler goal:

theorem simpler (P : Prop) (hp : P) : P ∧ True := P:Prophp:P⊢ P ∧ True P:Prophp:P⊢ P All goals completed! 🐙

After simp the goal P ∧ True has become P.

Lean still checks everything automation does. Automation does not lower the standard of proof.

Here is the auditor’s point. When automation succeeds, it tells you the goal was easy, not that the theorem is important. Look:

theorem looks_deep (n : Nat) (h1 : n > 10) (h2 : n < 5) : n * n = n + 1000 := n:Nath1:n > 10h2:n < 5⊢ n * n = n + 1000 All goals completed! 🐙

omega succeeds because no number is above 10 and below 5. The hypotheses contradict each other, so any conclusion follows. The statement is vacuous.

A one-line automated proof of a big-sounding claim is a reason to look closer at the hypotheses.

Check yourself🔗