2.22 Backward Reasoning

Backward reasoning starts from the goal and reduces it to simpler subgoals. Instead of building forward from assumptions, you ask: what must be true for this goal to hold? Lean supports this style through tactics like apply, refine, and introduction rules.

Problem

You have a goal that is not directly provable from the current context, but there exists a hypothesis or theorem whose conclusion matches the goal.

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

The goal is R. The hypothesis hQR : Q -> R suggests that proving Q would be enough.

Solution

Use apply to reduce the goal.

theorem backward_basic
    (P Q R : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hp : P) :
    R := by
  apply hQR
  apply hPQ
  exact hp

Step by step:

1. apply hQR changes the goal from R to Q
2. apply hPQ changes the goal from Q to P
3. exact hp closes the goal

Discussion

Backward reasoning follows the structure of implications.

hQR : Q -> R

means:

to prove R, it suffices to prove Q

The tactic apply implements this transformation.

Using apply

If the goal matches the conclusion of a hypothesis:

h : A -> B
⊢ B

then:

apply h

changes the goal to:

⊢ A

Example:

theorem apply_example
    (P Q : Prop)
    (hPQ : P -> Q)
    (hp : P) :
    Q := by
  apply hPQ
  exact hp

Chaining Applications

Multiple implications can be applied in sequence.

theorem apply_chain
    (P Q R S : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hRS : R -> S)
    (hp : P) :
    S := by
  apply hRS
  apply hQR
  apply hPQ
  exact hp

Each apply moves one step backward.

Using refine

The refine tactic allows partial specification of a proof term, leaving holes for subgoals.

theorem refine_example
    (P Q R : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hp : P) :
    R := by
  refine hQR ?hq
  refine hPQ ?hp
  exact hp

The placeholders ?hq and ?hp become new goals.

This is useful when the structure of the proof is known but some pieces must be filled later.

Backward Reasoning with Conjunction

If the goal is a conjunction, use its introduction rule.

theorem backward_and
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P ∧ Q := by
  constructor
  · exact hp
  · exact hq

Here the goal is reduced to two subgoals.

Backward Reasoning with Disjunction

If the goal is a disjunction, choose a side.

theorem backward_or
    (P Q : Prop)
    (hp : P) :
    P ∨ Q := by
  left
  exact hp

The tactic left changes the goal from P ∨ Q to P.

Backward Reasoning with Existentials

To prove an existential, provide a witness.

theorem backward_exists
    (P : Nat -> Prop)
    (a : Nat)
    (ha : P a) :
    ∃ n : Nat, P n := by
  use a
  exact ha

The goal is reduced to proving P a.

Backward Reasoning with Equality

To prove equality, reduce to reflexivity when possible.

theorem backward_eq
    (a : Nat) :
    a = a := by
  rfl

Or rewrite the goal into a simpler form.

theorem backward_eq_rw
    (a b : Nat)
    (hAB : a = b) :
    b = a := by
  rw [hAB]

The goal becomes a = a.

Backward Reasoning with Negation

To prove a negation, assume the proposition and derive False.

theorem backward_not
    (P Q : Prop)
    (hPQ : P -> Q)
    (hnq : ¬ Q) :
    ¬ P := by
  intro hp
  apply hnq
  apply hPQ
  exact hp

The goal ¬ P becomes P -> False.

Combining Forward and Backward Reasoning

Most proofs mix both styles.

theorem mixed_reasoning
    (P Q R : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hp : P) :
    R := by
  apply hQR
  have hq : Q := hPQ hp
  exact hq

The proof starts with backward reasoning, then uses forward reasoning to produce the needed intermediate fact.

Backward Reasoning with Universals

If the goal matches the result of a universal statement, apply it.

theorem backward_forall
    (α : Type)
    (P : α -> Prop)
    (a : α)
    (h : ∀ x : α, P x) :
    P a := by
  exact h a

If the goal is universal, introduce a variable.

theorem backward_forall_intro
    (α : Type)
    (P : α -> Prop) :
    (∀ x : α, P x) -> (∀ x : α, P x) := by
  intro h
  intro x
  exact h x

Using apply with Theorems

You can apply library theorems directly.

theorem backward_add_zero (n : Nat) : n + 0 = n := by
  apply Nat.add_zero

This works because the goal matches the theorem exactly.

When to Prefer Backward Reasoning

Backward reasoning is effective when:

• the goal matches the conclusion of a known theorem
• the proof is naturally goal-driven
• the structure of the proof is determined by the goal
• you want to reduce a complex goal into simpler subgoals

Forward reasoning is better when the structure is determined by the data in the context.

Avoiding Overuse

Too many nested apply calls can make proofs hard to read.

Less readable:

apply hRS
apply hQR
apply hPQ
exact hp

More readable:

have hq : Q := hPQ hp
have hr : R := hQR hq
exact hRS hr

Choose the style that best matches the logical flow.

Common Patterns

Reduce goal:

apply h

Introduce subgoal:

constructor

Choose disjunction side:

left
right

Provide witness:

use a

Introduce assumption:

intro hp

Refine partial proof:

refine h ?_

Common Pitfalls

Do not apply a hypothesis unless its conclusion matches the goal.

Do not create subgoals that are harder than the original goal.

Do not mix too many backward steps without inspecting the intermediate goal.

Do not use apply when a direct exact is clearer.

Do not forget that apply works on the outermost structure of the goal.

Takeaway

Backward reasoning reduces a goal to simpler subgoals using the structure of implications, conjunctions, disjunctions, and quantifiers. The main tool is apply, which turns a goal into the premises required by a hypothesis. Effective proofs often combine backward reasoning to shape the goal and forward reasoning to supply the needed facts.