Prove an implication

Assume the premise with intro, then prove the conclusion.

14 minBeginnerimplicationintronaming assumptions

0/13 completed in this course

In this course 3 / 13

To prove P → Q you assume P and prove Q. intro h performs the assumption: the premise leaves the goal and enters the context under the name you chose. The state ⊢ P → Q becomes h : P above the line and ⊢ Q below it.

An implication does not claim its premise holds. It promises a way to turn any proof of the premise into a proof of the conclusion. That is why intro is safe: you are not asserting P, you are working under the assumption of it.

You choose the name. hp for a proof of P, hab for a proof of A → B. Lean does not care, but every later line refers to that name, and a proof full of inaccessible names is one you cannot edit. intro also takes several names at once: intro ha hb introduces two premises.

What you introduce is not always what you use. In the worked example the goal is A → B and a proof of B is already in context, so the introduced ha is never touched. intro responds to the shape of the goal, not to where the answer will come from.

Worked example

example (A B : Prop) (hb : B) : A → B := by
  intro ha
  exact hb

After intro ha the goal is ⊢ B, with ha : A and hb : B above the line. Only hb has the right type. Your exercise is the case where the assumption you introduce is the answer.

Takeaway

intro h assumes the premise of an implication and leaves the conclusion as the goal.

Exercise 1 of 2

Prove that P implies P. Name the assumption h.

Suggested steps

Assume the premise under a name
Close what is left

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

Exercise.lean

1theorem exercise (P : Prop) : P → P := by

given

Loading editor…

Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.

P:Prop

⊢P → P

ReadyLn 1, Col 1Lean 4

Draft saved in this browser

Stuck?

Worked example

Knowledge check