Prove which branch runs
Unfold a function and use a hypothesis to simplify its condition.
In this course 6 / 14
In the previous lesson the checks called your definitions on concrete inputs such as triple 4, and each call computed to a value. A theorem about arbitrary inputs cannot be settled that way. With lo and n unknown, Lean cannot tell which branch of if n < lo then lo else n runs.
if c then a else b returns a when the condition c holds and b otherwise, and both branches must have the same type. clamp lo n returns the lower bound lo when n is below it, and n otherwise: clamp 5 8 is 8 and clamp 5 2 is 5.
The statement below has a hypothesis, (h : n < lo). It is an assumption the theorem is allowed to use: the claim only has to hold for inputs where n < lo is true, and h is the name you use to refer to that fact. The next course is about working with hypotheses; here you only hand one to a tactic.
Two tactics do the work. unfold clamp replaces the call by the body of the definition, so the if appears in the goal. simp is Lean’s simplifier: it rewrites the goal with many known facts until it is closed or can go no further, and simp [h] lets it use h as well. Knowing n < lo, it picks the first branch and closes the equality.
This two-step shape, unfolding the definition and then simplifying with what you know, comes back in almost every later course.
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]The hypothesis identifies the branch for an arbitrary input. Your exercise proves the other branch of a different function, using the same two-step method.
To prove a branch of a function for arbitrary inputs, unfold its definition and use a hypothesis to simplify the condition.
For arbitrary lo and n, use h : n < lo to prove that clamp returns the lower bound.
Suggested steps
- Expose the body of
clamp - Use the hypothesis to select the true branch
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