Proof By Induction

Induction Principle

• Prove P(n) for all natural numbers:

  • Base case: prove P(0).

  • Inductive case: prove P(n') ⇒ P(S n').

  • Creates proof chain: P(0) ⇒ P(1) ⇒ P(2) ⇒ … for all numbers.

induction Tactic Syntax

• Induction n as [| n' IHn'] splits into:
  • Base case (n=0).
  • Inductive case (n=S n').
  • IHn' is inductive hypothesis (assumes property holds for n').

plusnO Induction Proof

• Theorem: forall n, n = n + 0.
  • Base: 0 = 0 + 0 (reflexivity).
  • Inductive: assume n' = n' + 0, prove S n' = S n' + 0.
  • Reflexivity completes.

Inductive Hypothesis Power

• Creates proof chain:
  • Base proves for 0.
  • Inductive case proves if true for k, then true for k+1.
  • Thus true for all natural numbers.

plus_assoc Proof

• Theorem: n + (m + p) = (n + m) + p.
  • Induct on n.
  • Base: 0 + (m + p) = (0 + m) + p (reflexivity).
  • Inductive: assumes, proves S n' + (m + p).
  • Reflexivity.

minusnn Proof

• Theorem: minus n n = 0.
  • Induct on n.
  • Base: minus 0 0 = 0 (simpl).
  • Inductive: assumes, proves minus (S n') (S n') = 0.

Helper Lemma plusnSm

• Lemma: forall n m, S (n + m) = n + S m.
  • Essential for commutativity proof.
  • Allows moving successor from outside to inside addition.

plus_comm Proof

• Theorem: n + m = m + n.
  • Induct on n.
  • Base: 0 + m = m + 0 (rewrite plusnO).
  • Inductive: assumes, proves S n' + m = m + S n'.

Helper Lemma Strategy

• Complex proofs require helper lemmas:
  • Identify needed facts.
  • Prove as separate lemmas.
  • Use in main proof.

assert Tactic

• Introduces intermediate subgoal during proof.
  • Syntax: assert (H: proposition). { prove proposition }
  • Useful for complex proofs.

plus_rearrange with assert

• Theorem: (n + m) + (p + q) = (m + n) + (p + q).
  • Use assert for commutativity lemma.

plus_swap Proof

• Theorem: n + (m + p) = m + (n + p).
  • Combine associativity and commutativity.

Choosing Induction Variable

• Induct on variable driving recursion.
  • Pattern matches on first argument (n).
  • Look at function definitions.

Induction vs Case Analysis

• Case analysis (destruct): finite cases, independent proofs.
  • Induction: recursive data types, properties for all natural numbers.

Induction Proof Structure

• Theorem name: forall n, property.
  • Proof structure:
  • intros n.
  • induction n as [| n' IHn'].
  • Base case: simpl, reflexivity.
  • Inductive case: simpl, rewrite IHn', reflexivity.

Common Induction Patterns

• Direct induction: apply IH directly.
  • Induction with lemmas: need helper lemmas.
  • Induction with rewriting: combine IH with other theorems.