04 December, 2010

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

 Coq でよく使われる tactic の4つ目は 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 <

No comments: