# 2.21 Forward Reasoning

Forward reasoning starts from the assumptions in the local context and derives new facts until the goal becomes immediate. This style is useful when the proof has a natural data flow: one hypothesis produces an intermediate result, another hypothesis consumes it, and the final result follows.

## Problem

You have assumptions that can be composed, but the goal is not directly available.

```lean
P Q R : Prop
hp : P
hPQ : P -> Q
hQR : Q -> R
⊢ R
```

The proof should move forward from `hp : P` to `Q`, then from `Q` to `R`.

## Solution

Use `have` to name each intermediate result.

```lean
theorem forward_basic
    (P Q R : Prop)
    (hp : P)
    (hPQ : P -> Q)
    (hQR : Q -> R) :
    R := by
  have hq : Q := hPQ hp
  have hr : R := hQR hq
  exact hr
```

The proof reads in the same order as the mathematical argument.

## Discussion

Forward reasoning is often clearer than directly nesting function applications.

```lean
theorem forward_compact
    (P Q R : Prop)
    (hp : P)
    (hPQ : P -> Q)
    (hQR : Q -> R) :
    R := by
  exact hQR (hPQ hp)
```

The compact version is fine for short proofs. The forward version is better when intermediate facts have meaning or will be reused.

## Forward Reasoning with Conjunctions

A conjunction supplies several facts. Extract them first, then derive consequences.

```lean
theorem forward_with_and
    (P Q R : Prop)
    (h : P ∧ Q)
    (hQR : Q -> R) :
    P ∧ R := by
  have hp : P := h.left
  have hq : Q := h.right
  have hr : R := hQR hq
  exact ⟨hp, hr⟩
```

A shorter version destructures the conjunction directly:

```lean
theorem forward_with_and_rcases
    (P Q R : Prop)
    (h : P ∧ Q)
    (hQR : Q -> R) :
    P ∧ R := by
  rcases h with ⟨hp, hq⟩
  have hr : R := hQR hq
  exact ⟨hp, hr⟩
```

## Forward Reasoning with Existentials

An existential supplies a witness and a proof about that witness.

```lean
theorem forward_with_exists
    (P Q : Nat -> Prop)
    (h : ∃ n : Nat, P n)
    (hPQ : ∀ n : Nat, P n -> Q n) :
    ∃ n : Nat, Q n := by
  rcases h with ⟨n, hnP⟩
  have hnQ : Q n := hPQ n hnP
  exact ⟨n, hnQ⟩
```

The proof keeps the witness `n` fixed and derives the new property for the same witness.

## Forward Reasoning with Disjunctions

A disjunction requires forward reasoning in each branch.

```lean
theorem forward_with_or
    (P Q R : Prop)
    (h : P ∨ Q)
    (hPR : P -> R)
    (hQR : Q -> R) :
    R := by
  cases h with
  | inl hp =>
    have hr : R := hPR hp
    exact hr
  | inr hq =>
    have hr : R := hQR hq
    exact hr
```

Each branch starts with the evidence available in that branch and derives the common conclusion.

## Forward Reasoning with Equality

Equality can be used to transform facts before using them.

```lean
theorem forward_with_eq
    (a b : Nat)
    (hAB : a = b)
    (ha : a + 1 = 5) :
    b + 1 = 5 := by
  have hb : b + 1 = 5 := by
    rw [← hAB]
    exact ha
  exact hb
```

Here the goal is proved by first deriving the exact statement needed.

A more direct version rewrites the hypothesis:

```lean
theorem forward_with_eq_at
    (a b : Nat)
    (hAB : a = b)
    (ha : a + 1 = 5) :
    b + 1 = 5 := by
  rw [hAB] at ha
  exact ha
```

## Forward Reasoning with Negation

Negation is used forward by applying it to a positive proof.

```lean
theorem forward_with_not
    (P Q : Prop)
    (hp : P)
    (hnp : ¬ P) :
    Q := by
  have hf : False := hnp hp
  cases hf
```

The proof derives `False`, then eliminates it.

## Forward Reasoning with Universals

A universal hypothesis becomes useful after it is applied to a specific value.

```lean
theorem forward_with_forall
    (α : Type)
    (P Q : α -> Prop)
    (a : α)
    (hP : ∀ x : α, P x)
    (hPQ : ∀ x : α, P x -> Q x) :
    Q a := by
  have haP : P a := hP a
  have haQ : Q a := hPQ a haP
  exact haQ
```

This pattern is common in formalized mathematics. Instantiate universal facts first, then apply implication facts.

## Combining Several Steps

Forward reasoning scales well when the proof has a chain of dependencies.

```lean
theorem forward_chain
    (P Q R S T : Prop)
    (hp : P)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hRS : R -> S)
    (hST : S -> T) :
    T := by
  have hq : Q := hPQ hp
  have hr : R := hQR hq
  have hs : S := hRS hr
  have ht : T := hST hs
  exact ht
```

This proof is intentionally linear. Each line has one input and one output.

## When to Prefer Forward Reasoning

Forward reasoning is useful when:

* the proof has meaningful intermediate claims
* the same intermediate fact is used more than once
* the goal is distant from the starting assumptions
* the proof should read like a derivation
* debugging requires inspecting each step separately

For very short proofs, direct application may be clearer.

```lean
theorem direct_application
    (P Q : Prop)
    (hp : P)
    (hPQ : P -> Q) :
    Q := by
  exact hPQ hp
```

## Avoiding Useless Intermediate Facts

Do not name every small expression if the name adds no clarity.

Less useful:

```lean
theorem too_many_have
    (P Q : Prop)
    (hp : P)
    (hPQ : P -> Q) :
    Q := by
  have hp' : P := hp
  have hq : Q := hPQ hp'
  exact hq
```

Better:

```lean
theorem enough_have
    (P Q : Prop)
    (hp : P)
    (hPQ : P -> Q) :
    Q := by
  exact hPQ hp
```

Use `have` when the intermediate fact explains the proof or will be reused.

## Forward Reasoning with Reuse

When an intermediate fact is used twice, naming it is appropriate.

```lean
theorem forward_reuse
    (P Q R S : Prop)
    (hp : P)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hQS : Q -> S) :
    R ∧ S := by
  have hq : Q := hPQ hp
  have hr : R := hQR hq
  have hs : S := hQS hq
  exact ⟨hr, hs⟩
```

The proof of `Q` is computed once and reused.

## Common Patterns

Derive a new fact:

```lean
have hq : Q := hPQ hp
```

Derive from a universal:

```lean
have haP : P a := hP a
```

Derive from equality:

```lean
rw [hAB] at ha
```

Derive contradiction:

```lean
have hf : False := hnp hp
```

Use a derived fact:

```lean
exact hQR hq
```

## Common Pitfalls

Do not add intermediate facts that merely rename existing assumptions.

Do not leave large expressions unnamed when they will be reused.

Do not derive facts in an order that hides their dependencies.

Do not use forward reasoning when the goal shape clearly asks for an introduction rule first.

Do not forget that each branch of a case split has its own context.

## Takeaway

Forward reasoning derives consequences from available assumptions. In Lean, the main tool is `have`. Use it to name meaningful intermediate facts, instantiate universal statements, apply implications, transport facts through equalities, and derive contradictions. A good forward proof reads as a sequence of typed transformations from assumptions to goal.