State your own theorem

Write binders, a hypothesis and a claim. The proofs are supplied; the statements are yours.

19 minBeginnertheorembindershypothesesnamingstatements you write yourself

0/14 completed in this course

In this course 12 / 14

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. In this exercise you stop before :=: the proofs are supplied, so the whole task is getting the statements right.

A binder lets a theorem talk about arbitrary inputs, and a hypothesis records a relationship the claim may rely on. double_substitute says that equal inputs may be exchanged inside a call to double, so before the colon it needs the two numbers and the equality a = b.

The second theorem needs only a number. Names are part of the interface: the checks under your answer use both theorems by name, so the names, binders and claims all have to match. If a check reports a type mismatch, your statement compiles but says something else.

Worked example

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

-- `rw [h]` replaces `a` by `b` in the goal, using the equation h : a = b.
theorem addFee_respects_eq (a b : Nat) (h : a = b) : addFee a = b + 3 := by
  unfold addFee
  rw [h]

Before the colon, the statement introduces both values and an equality hypothesis; after it, the claim uses all three. Your exercise writes two statements of this kind, and their proofs are supplied.

Takeaway

A theorem statement names a result, introduces its inputs and hypotheses before the colon, and states the claim after it. Getting the statement right is its own skill, separate from proving it.

Exercise 1 of 3

State double_substitute, which uses an equality hypothesis, and double_successor, a claim about every n. Write only the statements; the proofs are supplied when you check.

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