State your own theorem | Proofs about your programs

So far every statement was given and you wrote the proof. Writing the statement is the other half of the work, and often the harder half: a theorem that is easy to prove but says the wrong thing is worse than none.

The shape is theorem name (inputs and hypotheses) : claim. Before the colon you introduce what the claim talks about: values such as (a b : Nat), and hypotheses such as (h : a = b). After the colon comes the claim.

theorem double_pos (n : Nat) (h : 0 < n) : 0 < double n := by
  unfold double
  omega

In this lesson the proofs are supplied when you check, so you write only the statements and stop before :=. The checks under your answer use your theorems by name. If one reports a type mismatch, your statement compiles but says something different.

Worked example

def addFee (n : Nat) : Nat := n + 3

theorem addFee_respects_eq (a b : Nat) (h : a = b) : addFee a = b + 3 := by
  unfold addFee
  rw [h]

Step through the proof1 / 3

At the start of the proof on line 3. Everything above ⊢ may be used; the line below it is what must be proved.

a b:Nat

h:a = b

⊢addFee a = b + 3

Before the colon: two numbers and an equation about them. After it: a claim that uses all three.

Takeaway

A statement introduces its inputs and hypotheses before the colon and makes its claim after it. Getting it right is a skill of its own.

Exercise 1 of 3

State double_substitute, which uses an equality hypothesis, and double_successor, a claim about every n. Write only the statements.

You write only the statements. When you check, each one is proved with the steps below, and the checks confirm it says exactly what was asked.

theorem double_substitute … := by
  unfold double
  omega

theorem double_successor … := by
  unfold double
  omega

Suggested steps

Give double_substitute an equality hypothesis about a and b
After the colon, claim that doubling the first gives the second plus itself
State double_successor for an arbitrary number

These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.

Exercise.lean

1def double (n : Nat) : Nat := n + n

given

Loading editor…

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 statements have to match.
example (a b : Nat) (h : a = b) : double a = b + b := double_substitute a b h
example (n : Nat) : double (n + 1) = n + n + 2 := double_successor n

ReadyLn 1, Col 1Lean 4

Draft saved in this browser

Stuck?

Worked example

Knowledge check