# 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. ```lean 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. ```lean 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. ```lean hQR : Q -> R ``` means: ```lean 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: ```lean h : A -> B ⊢ B ``` then: ```lean apply h ``` changes the goal to: ```lean ⊢ A ``` Example: ```lean 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. ```lean 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. ```lean 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. ```lean 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. ```lean 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. ```lean 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. ```lean theorem backward_eq (a : Nat) : a = a := by rfl ``` Or rewrite the goal into a simpler form. ```lean 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`. ```lean 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. ```lean 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. ```lean 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. ```lean 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. ```lean 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: ```lean apply hRS apply hQR apply hPQ exact hp ``` More readable: ```lean 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: ```lean apply h ``` Introduce subgoal: ```lean constructor ``` Choose disjunction side: ```lean left right ``` Provide witness: ```lean use a ``` Introduce assumption: ```lean intro hp ``` Refine partial proof: ```lean 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.