Lean for All

Day 9: intro and exact🔗

Follow intro, exact and assumption, and predict the goal after each.

How do you prove “if P, then Q”? Assume P, then show Q. The tactic intro does the assuming:

theorem bigger' (n : Nat) : n > 5 → n > 3 := n:Nat⊢ n > 5 → n > 3 n:Nath:n > 5⊢ n > 3 All goals completed! 🐙

Before intro h, and after it:

n : Nat
⊢ n > 5 → n > 3

n : Nat
h : n > 5
⊢ n > 3

The if-part moved above the line, with the name h. Nothing was proved yet: intro only changes the form of the goal.

intro also works on ∀. To prove “for every n, …”, take an arbitrary n and prove the claim for it:

theorem add_zero_all : ∀ n : Nat, n + 0 = n := ⊢ ∀ (n : Nat), n + 0 = n n:Nat⊢ n + 0 = n All goals completed! 🐙 
⊢ ∀ (n : Nat), n + 0 = n

becomes

n : Nat
⊢ n + 0 = n

You do not get to pick n. It stands for any natural number, so whatever follows must work for all of them.

When a hypothesis says exactly the goal, exact finishes the proof:

theorem pick (P Q : Prop) (hp : P) (Variable name `hq` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hq Note: This linter can be disabled with `set_option linter.unusedVariables false`hq : Q) : P := P:PropQ:Prophp:Phq:Q⊢ P All goals completed! 🐙

(P Q : Prop means P and Q are any statements at all.) exact hq would fail: hq says Q, but the goal is P.

assumption does the same job without a name: it looks through the hypotheses for one that is exactly the goal.

theorem pick' (P Q : Prop) (Variable name `hp` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hp Note: This linter can be disabled with `set_option linter.unusedVariables false`hp : P) (hq : Q) : Q := P:PropQ:Prophp:Phq:Q⊢ Q All goals completed! 🐙

intro can take several names at once. Follow this one by hovering over each line:

theorem first (P Q : Prop) : P → Q → P := P:PropQ:Prop⊢ P → Q → P P:PropQ:Prophp:Phq:Q⊢ P All goals completed! 🐙

After intro hp hq you have hp : P and hq : Q, and the goal is P. Then exact hp closes it.

For an auditor: intro and exact are bookkeeping. They never make anything true that was not already given. If a proof is mostly intro and exact, the real content is in the hypotheses, so read those carefully.

Check yourself🔗