Basics - Proof By Case Analysis

destruct Tactic

Splits proof into cases based on type constructors. Syntax: destruct n as [| n'] eqn:E. 'as' names variables in each constructor case; eqn saves case equation. Essential for exhaustive case analysis on inductive types.

Case Analysis for Nat

destruct n splits into two cases: n = O (zero) and n = S n' (successor). n' is the inner value. Must prove property holds for both cases to prove for all natural numbers.

Case Analysis for Bool

destruct b splits into b = true and b = false. No 'as' pattern needed because constructors have no inner values. Each case simplifies directly for reflexivity.

Exhaustive Case Analysis Principle

For safety verification, case analysis must cover all constructors exhaustively. Rocq forces handling every constructor; you cannot miss a case. Proves safety through impossibility - if property holds in all cases, it always holds.

Boolean AND Exchange Proof

Theorem andb3_exchange: forall b c d, andb (andb b c) d = andb (andb b d) c. Requires nested destruct on b, then c, then d. Total 8 cases.

Multiple Case Analysis

For multiple variables, nested destruct explores all combinations. Example: andb_commutative requires destruct b then destruct c for 4 total cases. Each case simplifies to reflexivity.

Bullet Styles for Subgoals

Organize proof cases: - (single dash), + (plus sign), * (asterisk), or { and } braces. Use different levels for nested cases. Improves readability.

Comments in Proofs

Add comments to clarify what each case represents. Example: - (* n = 0 ) ( Base case *) reflexivity. Makes proofs easier to understand, review, and debug.

Case Analysis Limitations

Cannot prove n = n + 0 for all n because simpl cannot reduce n + 0 (n is variable). Base case (n=0) works but successor case requires knowing S n' = S (n' + 0), which needs the result for n'. Requires induction.

When to Use Case Analysis

Use for finite types with independent cases: booleans (2 cases), small enumerations, base cases of recursive proofs. Each case provable independently without dependency on other cases.

When to Use Induction

Use when proving case n requires knowing result for case n-1. Successor case depends on inductive hypothesis. Natural numbers require induction, not just case analysis, for many theorems.

Proof Strategies Summary

reflexivity: identical sides. simpl: evaluate/reduce expressions. rewrite: use equations/hypotheses. destruct: case analysis on finite types. induction: recursive/infinite types