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.

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.

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.

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.

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:

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.

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.

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.

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:

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.

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.

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.

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.

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:

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:

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.

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:

have hq : Q := hPQ hp

Derive from a universal:

have haP : P a := hP a

Derive from equality:

rw [hAB] at ha

Derive contradiction:

have hf : False := hnp hp

Use a derived fact:

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.