Home |
Source |
Case analysis is a core aspect of constructivist logic. Although for many kinds of problems it is a low-level tool, it is ubiquitous among the foundations of all problems formalized in the Coq system. The core idea is: “if I want to prove a property P holds for a term t, I can do so by writing multiple sub-proofs stating that for each form that t can have, P holds.”
destruct allows for case analysis on inductive terms or assumptions. It can be used to split assumptions with conjunctions and disjunctions, as well as existential assumptions. The arguments of destruct are patterns.
(* Simple usage *)
destruct H.
(* Destruct a term and introduce a hypothesis E showing its equivalence to the form it took *)
destruct n eqn:E.
(* Providing names for newly-introduced terms *)
destruct H as [H0 [H1 H2]].
(* Providing only some names for newly-introduced terms *)
destruct H as [H0 [? H1]].
(* Destructing multiple terms/hypotheses *)
destruct x as [| x0 x1], H as [[H1 H0] H2].
(* Providing names for newly-introduced terms in different generated subgoals *)
destruct H as [H1 | H2].Before
n: nat
-------------------------
n = 0 \/ 1 <= ndestruct n as [| n'] eqn:E.After (first goal generated)
n: nat
E: n = 0
-------------------------
1/2
0 = 0 \/ 1 <= 0After (second goal generated)
n, n': nat
E: n = S n'
-------------------------
1/1
S n' = 0 \/ 1 <= S n'Script
Theorem destruct_example1 : forall n : nat,
n = 0 \/ 1 <= n.
Proof.
intros. destruct n as [| n'] eqn:E.
- left. reflexivity.
- right. apply le_n_S, le_0_n.
Qed.Script
Theorem destruct_example2 : forall (P Q R : Prop),
((P /\ Q) /\ R) -> P /\ (Q /\ R).
Proof.
intros P Q R H.
destruct H as [[PTrue QTrue] RTrue]. split.
- apply PTrue.
- split.
-- apply QTrue.
-- apply RTrue.
Qed.Script
Theorem destruct_example3 :
forall (P Q R : Prop),
(P \/ Q) -> P \/ Q \/ R.
Proof.
intros. destruct H as [PTrue | QTrue].
- left. assumption.
- right. left. assumption.
Qed. inversion looks at a given piece of structural evidence and draws conclusions from it. If there are multiple sets of conclusions, inversion will generate a new proof obligation for each one. Informally, inversion is doing a more specific form of the case analysis provided by destruct - where destruct essentially says “I don’t know what this term is, so I’ll prove a property for all of the possible forms of it,” inversion says “I know exactly what terms could construct this hypothesis because of its definition, so I’ll only prove a property for those terms.”
This tactic often generates many trivial equality assumptions that may clutter the assumption space. I recommend almost always following inversion with subst to immediately substitute away these equalities.
(* Standard usage *)
inversion H.Before
n: nat
H: n <= 1
-------------------------
1/1
n = 0 \/ n = 1inversion H.After (first goal generated)
n: nat
H: n <= 1
H0: n = 1
-------------------------
1/2
1 = 0 \/ 1 = 1After (second goal generated)
n: nat
H: n <= 1
m: nat
H1: n <= 0
H0: m = 0
-------------------------
1/1
n = 0 \/ n = 1Script
Theorem inversion_example1 :
forall n, n <= 1 -> n = 0 \/ n = 1.
Proof.
intros. inversion H.
- right. reflexivity.
- inversion H1. left. reflexivity.
Qed.Script
Inductive color : Type :=
| Red | Blue | Green | Cyan | Magenta | Yellow.
Inductive makes_white : color -> color -> color -> Prop :=
| RBG : makes_white Red Blue Green
| CMY : makes_white Cyan Magenta Yellow.
Theorem inversion_example2 :
forall (c1 c2 c3 : color),
makes_white c1 c2 c3 ->
(c1 = Red /\ c2 = Blue /\ c3 = Green) \/
(c1 = Cyan /\ c2 = Magenta /\ c3 = Yellow).
Proof.
intros c1 c2 c3 Hmw. inversion Hmw.
- left. repeat split.
- right. repeat split.
Qed.induction is an extension of destruct that allows for case analysis on inductive terms, gaining an inductive hypothesis for each recursive subterm generated by the term destruction. The arguments of induction are patterns.
If the goal still contains named impliciations, induction can be used before introducing them with intros. In this case, if the argument to induction is not the first impliciation in the chain, all implications before it will be introduced to the goal’s assumption space.
induction can act similarly to inversion under specific circumstances. If you induct over an object that already contains subterms, you can remember the subterm(s) and induct on the root object. Then, by an easy inversion on the hypothesis generated by remember, all cases that don’t match the required form generated by the case analysis will be automatically solved by the principle of explosion.
Sometimes, the automatically-generated induction principles for a type are not sufficient to prove some properties about terms with that type. In this case, it is possible to write a custom induction principle for a type and then use it with the induction tactic.
(* Simple usage *)
induction n.
(* Induct over a term and introduce a hypothesis E showing its equivalence to the form it took *)
induction n eqn:E.
(* Providing names for newly-introduced terms *)
induction n as [| n' IHn' ].
(* Using a custom induction principle *)
induction z using peano_ind.Before
n: nat
-------------------------
n + 0 = ninduction n as [| n' IHn' ].After (first goal generated)
-------------------------
1/2
0 + 0 = 0After (second goal generated)
n': nat
IHn' : n' + 0 = n'
-------------------------
1/1
S n' + 0 = S n'Script
Theorem induction_example1 : forall (n : nat),
n + 0 = n.
Proof.
induction n.
- reflexivity.
- simpl. rewrite IHn. reflexivity.
Qed.Script
Require Import ZArith.
Open Scope Z.
Theorem induction_example2 : forall (x y : Z),
x + y = y + x.
Proof.
induction x using Z.peano_ind.
- intros. simpl. rewrite Z.add_0_r. reflexivity.
- intros. rewrite Z.add_succ_l. rewrite IHx.
rewrite Z.add_comm. rewrite <- Z.add_succ_l.
rewrite Z.add_comm. reflexivity.
- intros. rewrite Z.add_pred_l. rewrite IHx.
rewrite Z.add_comm. rewrite <- Z.add_pred_l.
rewrite Z.add_comm. reflexivity.
Qed.