[Coq] Coq Advent Calender : destruct (4 of 25)

　Coq でよく使われる tactic の４つ目は destruct です。

　destruct は基本的にはある項を場合分けする時使うのですが、仮定の中にある /\ とか \/ とか exists とかを分解するのに使うのに便利です。（それ以外のときは induction とか case_eq とか使う事が多い様にも思います。）
　下記の例では仮定 abc を分解して仮定 a, b, c を作っています。　

Coq < Lemma Sample_of_destruct : forall A B C:Prop,
Coq < A /\ (B /\ C) -> (A /\ B) /\ C.
1 subgoal
  
  ============================
   forall A B C : Prop, A /\ B /\ C -> (A /\ B) /\ C

Sample_of_destruct < intros A B C abc.
1 subgoal
  
  A : Prop
  B : Prop
  C : Prop
  abc : A /\ B /\ C
  ============================
   (A /\ B) /\ C

Sample_of_destruct < destruct abc as [a [b c]].
1 subgoal
  
  A : Prop
  B : Prop
  C : Prop
  a : A
  b : B
  c : C
  ============================
   (A /\ B) /\ C

Sample_of_destruct < split; [split|]; assumption.
Proof completed.

Sample_of_destruct < Qed.
intros A B C abc.
destruct abc as (a, (b, c)).
split; [ split | idtac ]; assumption.

Sample_of_destruct is defined

Coq <