Home / Tracks / Proof Strategies / Direct proof

Strategy: Direct proof

Pattern recognition

When you see: a goal of the form P → Q (an implication)

Strategy: Assume P and derive Q.

Tactic: intro h

This is the most fundamental proof strategy. To prove "if P then Q," you assume P is true (giving it a name like h) and then show Q follows. The intro tactic moves the antecedent from the goal into your hypotheses.

Velleman calls this the "direct approach" — you work forwards from what you know towards what you need. It's the default strategy whenever your goal is an implication.

Watch the strategy in action

Here intro transforms the goal by moving the antecedent into the context.

The rule

Goal shape:  P → Q
Action:      intro h
Effect:      h : P appears in context, goal becomes Q
Think:       "Assume P. Now I need to show Q."

Your turn

Prove that implication is transitive: if P → Q and Q → R, then P → R. You will need intro more than once.

theorem imp_trans (P Q R : Prop) (hpq : P → Q) (hqr : Q → R) : P → R := by
  sorry

theorem imp_trans (P Q R : Prop) (hpq : P → Q) (hqr : Q → R) : P → R := by
  intro hp
  exact hqr (hpq hp)

See also: Logic §02 — Implication | Proof Theory §02 — →-Elim