Apply an implication
An implication is a function on proofs. apply works backwards from the goal.
In this course 5 / 13
A hypothesis hpq : P → Q is a function from proofs of P to proofs of Q. Given hp : P, the application hpq hp is a proof of Q, so exact hpq hp closes the goal in one line. Nothing unusual is happening: this is function application, and proofs are values.
apply runs the same idea backwards. apply hpq says: the goal is Q, and hpq produces a Q out of a P, so it is enough to prove P. The goal ⊢ Q is replaced by ⊢ P. This is how proofs are normally found: start from what you want and work back to what you have.
Backward steps chain. In the worked example apply g turns ⊢ C into ⊢ B, then apply f turns that into ⊢ A, and a hypothesis finishes. Each line peels off one implication, and the panel shows the goal getting closer to something you already hold. A function with two premises, P → Q → R, leaves two goals after apply, one for each premise.
Use exact when you can already write the finished term and apply when you are still looking for the argument. Both end up producing the same proof term; the difference is which end you start from.
Worked example
example (A B C : Prop) (f : A → B) (g : B → C) (ha : A) : C := by
apply g
apply f
exact haWatch the goal shrink: ⊢ C, then ⊢ B, then ⊢ A, then nothing. Your exercise is a single link of this chain.
Implications are functions on proofs. exact f a applies one forwards; apply f works backwards from the goal.
Prove Q from hpq : P → Q and hp : P.
Suggested steps
- Reduce the goal Q to its premise P
- Close the new goal with hp
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