# 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:

```lean
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.

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

After `intro h`, the proof state is:

```lean
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:

```lean
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:

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

and:

```lean
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:

```lean
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.

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

Lean reads this type as:

```lean
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:

```lean
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:

```lean
h : P -> Q
```

and another hypothesis:

```lean
hp : P
```

then applying `h` to `hp` produces a proof of `Q`.

```lean
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:

```lean
h : P -> Q
hp : P
⊢ Q
```

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

## Chaining Implications

Implications can be composed.

```lean
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`:

```lean
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`.

```lean
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.

```lean
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.

```lean
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:

```lean
⊢ P -> Q
```

use:

```lean
intro hp
```

When the context contains an implication:

```lean
h : P -> Q
hp : P
⊢ Q
```

use:

```lean
exact h hp
```

When the goal matches the conclusion of an implication:

```lean
h : P -> Q
⊢ Q
```

use:

```lean
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`.