Home |
Github |
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'
=========================
2/2
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):
Note: this is the case of n <= 1 where
n = 1, hence H0.
n: nat
H: n <= 1
H0: n = 1
=========================
1/2
1 = 0 \/ 1 = 1After (second goal generated):
Note: this is the case of n <= 1 where
n < 1, equivalent to n <= 0, hence
H1.
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. “Induction Principles” - Logical Foundations