Day 4: If … then: hypotheses
Read hypotheses as “if”, and know they are assumptions, not facts.
A hypothesis is a condition the theorem assumes:
theorem bigger (n : Nat) (h : n > 5) : n > 3 := n:Nath:n > 5⊢ n > 3 All goals completed! 🐙
(h : n > 5) reads “if n > 5”. The h is just a name for the assumption, so the proof can refer to it. The whole theorem says:
For every natural number n, if n > 5, then n > 3.
Lean writes “if … then” with an arrow, →. This is the same theorem with everything after the colon:
theorem bigger' : ∀ n : Nat, n > 5 → n > 3 := ⊢ ∀ (n : Nat), n > 5 → n > 3 All goals completed! 🐙
Read P → Q as “if P, then Q” or “P implies Q”.
Several hypotheses chain together. P → Q → R means “if P, then if Q, then R”, which is the same as “if P and Q, then R”. The arrow groups to the right: P → Q → R is P → (Q → R), not (P → Q) → R.
The arrow only goes one way. This is true for every n:
theorem two_even (n : Nat) (h : n = 2) : n % 2 = 0 := n:Nath:n = 2⊢ n % 2 = 0 All goals completed! 🐙
But the reverse, “if n is even then n = 2”, is false (think of 4). Mixing up a statement and its reverse (its converse) is one of the most common reading mistakes.
Most important for auditing: a hypothesis is an assumption, not a fact. Nobody checked that it can be true. Look:
theorem strange (n : Nat) (h1 : n > 5) (h2 : n < 3) : n = 100 := n:Nath1:n > 5h2:n < 3⊢ n = 100 All goals completed! 🐙
Lean accepts it. But no number is both above 5 and below 3, so this theorem applies to no number at all. It says nothing. Such a theorem is called vacuous, and it is exactly the trick to watch for in AI-written proofs.