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.

関連記事