State your own theorem
Name it, bind what it talks about, claim something, then prove it.
In this course 9 / 10
Every exercise so far handed you the statement and asked for the proof. Writing the statement is the other half of the work, and frequently the harder half: a theorem that is easy to prove and says the wrong thing is worse than no theorem at all.
The shape is theorem name (binders) : claim := proof. Whatever appears before the colon introduces the things the claim talks about. Everything after it is the claim. := by then opens tactic mode, exactly as in the lessons so far.
A binder lets a theorem talk about an arbitrary input. double_two : double 2 = 4 concerns one number. double_add_self (n : Nat) : double n = n + n concerns every natural number. Supplying an argument, as in double_add_self 7, uses that theorem at seven.
Names are part of the interface, because theorems are referred to by name for the rest of a project’s life. The convention is to describe the statement rather than the proof: double_add_self reads as “double is add self”. The checks under your answer call both of your names, so a typo there is an error like any other.
Worked example
def addZero (n : Nat) : Nat := n + 0
theorem addZero_three : addZero 3 = 3 := by
rfl
theorem addZero_eq (n : Nat) : addZero n = n := by
rfl
#check addZero_eq 7The first theorem fixes the input at three. The second introduces an arbitrary n. Both proofs use rfl because these expressions reduce even when n is unknown; a variable does not always stop computation.
A theorem is a name, binders, a claim and a proof. The binders decide how much the theorem is worth, and the name is how everything else reaches it.
Write and prove two theorems about double: double_two, that doubling two gives four, and double_add_self, that doubling any n gives n + n.
Suggested steps
- State the first theorem, about the number two
- State the second with a binder, so it covers every n
- Give each of them a proof
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:These lines run underneath whatever you write. They are what decides the exercise, so your names and types have to match them.
-- Your theorems are used here by name, so the names and the statements have to match. example : double 2 = 4 := double_two example (k : Nat) : double k = k + k := double_add_self k
Knowledge check
Answer without looking back, then check your reasoning.
correct