2.2 Implication and Functions

Implication is the first logical connective to understand in Lean because it is also the ordinary function type. A proof of P -> Q is a function that receives a proof of P and returns a proof of Q.

Problem

You want to prove a statement of the form:

P -> Q

In Lean, this means you must write a function from proofs of P to proofs of Q.

Solution

Use intro to assume the premise, then prove the conclusion.

theorem implication_identity (P : Prop) : P -> P := by
  intro h
  exact h

After intro h, the proof state is:

h : P
⊢ P

The hypothesis h already has the required type, so exact h closes the goal.

Discussion

An implication has the same shape as a function type:

P -> Q

If P and Q are propositions, this is a logical implication. If P and Q are ordinary data types, this is a computational function. Lean uses the same arrow for both.

For example:

def addOne : Nat -> Nat :=
  fun n => n + 1

and:

theorem prove_implication (P Q : Prop) : P -> Q -> P := by
  intro hp
  intro hq
  exact hp

have the same structural form. The first takes a natural number and returns a natural number. The second takes a proof of P, then a proof of Q, and returns the proof of P.

The theorem can also be written as a term:

theorem prove_implication_term (P Q : Prop) : P -> Q -> P :=
  fun hp => fun hq => hp

The proof is a curried function. It first accepts hp : P, then accepts hq : Q, then returns hp.

Multiple Premises

A statement with several arrows introduces assumptions one at a time.

theorem first_of_two (P Q : Prop) : P -> Q -> P := by
  intro hp
  intro hq
  exact hp

Lean reads this type as:

P -> (Q -> P)

So the proof is a function that takes P and returns another function that takes Q and returns P.

You can introduce both assumptions at once:

theorem first_of_two_short (P Q : Prop) : P -> Q -> P := by
  intro hp hq
  exact hp

This is often clearer when the assumptions are simple.

Using an Implication Hypothesis

If you have a hypothesis:

h : P -> Q

and another hypothesis:

hp : P

then applying h to hp produces a proof of Q.

theorem apply_implication (P Q : Prop) : (P -> Q) -> P -> Q := by
  intro h
  intro hp
  exact h hp

After introducing both hypotheses, the context is:

h : P -> Q
hp : P
⊢ Q

The expression h hp has type Q, so it solves the goal.

Chaining Implications

Implications can be composed.

theorem implication_trans
    (P Q R : Prop) :
    (P -> Q) -> (Q -> R) -> P -> R := by
  intro hpq
  intro hqr
  intro hp
  exact hqr (hpq hp)

The proof proceeds as follows. From hp : P, the function hpq : P -> Q gives hpq hp : Q. Then hqr : Q -> R turns that into hqr (hpq hp) : R.

A more stepwise version uses have:

theorem implication_trans_step
    (P Q R : Prop) :
    (P -> Q) -> (Q -> R) -> P -> R := by
  intro hpq
  intro hqr
  intro hp
  have hq : Q := hpq hp
  have hr : R := hqr hq
  exact hr

This form is longer but easier to inspect.

Applying the Goal Backward

The tactic apply uses an implication in reverse. If the goal is Q and you have a theorem or hypothesis of type P -> Q, then apply changes the goal to P.

theorem apply_backward (P Q : Prop) (h : P -> Q) (hp : P) : Q := by
  apply h
  exact hp

After apply h, Lean knows that proving P is enough to prove Q.

This style is useful when the target conclusion is the result of a known implication.

Implication with Dependent Premises

A later premise may depend on an earlier value.

theorem dependent_implication
    (α : Type)
    (P : α -> Prop)
    (a : α) :
    P a -> P a := by
  intro h
  exact h

Here P is a predicate on values of type α. The proposition P a depends on the chosen value a. The implication rule is the same: introduce the assumption and prove the conclusion.

False Premises

If a premise is impossible, the implication is easy to prove. From False, every proposition follows.

theorem false_implies_anything (P : Prop) : False -> P := by
  intro h
  cases h

The command cases h performs case analysis on a proof of False. Since False has no constructors, there are no cases to consider, so the goal is closed.

Common Patterns

When the goal is an implication:

⊢ P -> Q

use:

intro hp

When the context contains an implication:

h : P -> Q
hp : P
⊢ Q

use:

exact h hp

When the goal matches the conclusion of an implication:

h : P -> Q
⊢ Q

use:

apply h

and then prove P.

Common Pitfalls

Do not try to prove Q directly before introducing the premise of P -> Q. The premise is not available until you use intro.

Do not confuse h : P -> Q with a proof of Q. It is only a way to obtain Q once you provide P.

Do not assume implication is symmetric. From P -> Q, you cannot conclude Q -> P without additional information.

Takeaway

A proof of an implication is a function. To prove P -> Q, assume P and prove Q. To use P -> Q, apply it to a proof of P. This single rule explains intro, function application, and the basic use of apply.