Prove which branch runs
Use a hypothesis to decide the condition of an if, for every input.
In this course 4 / 8
You wrote clamp in Lean foundations: it returns lo when n < lo, and n otherwise. For concrete numbers, rfl computes which branch runs. For an unknown n, Lean cannot tell, so the proof needs a hypothesis that settles the condition.
After unfold clamp the goal shows the if. Step through the example: simp [h] uses h to decide the condition, picks the branch, and closes the goal.
Without a hypothesis that answers the condition, simp can only rewrite the if into something it cannot finish. It then leaves a goal such as n < lo → lo = n, an implication: “if n < lo, then …”. omega can finish goals of that shape too.
Worked example
def shipping (express : Bool) : Nat :=
if express then 9 else 4
example (express : Bool) (h : express = false) : shipping express = 4 := by
unfold shipping
simp [h]
At the start of the proof on line 4. Everything above ⊢ may be used; the line below it is what must be proved.
The hypothesis says which branch runs, for any input that satisfies it. Your exercise does the same with a comparison instead of a Bool.
To prove what a function with an if returns for every input, unfold it and give simp the hypothesis that settles the condition.
For every lo and n with n < lo, prove that clamp returns the lower bound.
Suggested steps
- Unfold
clampso theifappears - Settle the condition with the hypothesis
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
Knowledge check
Answer without looking back, then check your reasoning.
correct