destructは以下のような代数的データ型
Inductive T : Type := | C1 : x11 -> x12 -> ... -> T | C2 : x21 -> x22 -> ... -> T ... | Cn : xn1 -> xn2 -> ... -> T.
の値xに対して、
destruct x as [x11 x22 ... | x21 x22 ... | ... | xn1 xn2 ... ]
でパターンマッチングを行うことができますが、このパターンをintros内でも使うことができます。
Goal forall x : bool, negb (negb x) = x. Proof. intros [|]. (* xをintrosしつつ、destruct x相当のことができる *) - (* case x = true *) reflexivity. - (* case x = false *) reflexivity. Qed.
この例だと微妙な感じですが、andやorを分解するとき等に少し便利です。
Goal forall P Q : Prop, (P \/ Q) /\ ~Q -> P. Proof. intros P Q [[HP | HQ] NQ]. (* NQ : ~Q *) (* P \/ Q の部分で分岐する *) - (* case HP : P *) assumption. - (* case HQ : Q *) contradiction. Qed.