14 December, 2010

[Coq] Coq Advent Calender : split (14 of 25)

 Coq でよく使われる tactic の14番目は split です。...そんなに使うかなぁ?

 split はゴールが P /\ Q の形をしている時に、二つのゴール P, Q に分割します。あとはそれぞれを別々に証明すればOKです。

 簡単な例を下記に示します。

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

============================
forall A B C : Prop, A /\ B /\ C -> (A /\ B) /\ C

Sample_of_split < intros A B C abc.
1 subgoal

A : Prop
B : Prop
C : Prop
abc : A /\ B /\ C
============================
(A /\ B) /\ C

Sample_of_split < 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_split < split.
2 subgoals

A : Prop
B : Prop
C : Prop
a : A
b : B
c : C
============================
A /\ B

subgoal 2 is:
C

Sample_of_split < split.
3 subgoals

A : Prop
B : Prop
C : Prop
a : A
b : B
c : C
============================
A

subgoal 2 is:
B
subgoal 3 is:
C

Sample_of_split < assumption.
2 subgoals

A : Prop
B : Prop
C : Prop
a : A
b : B
c : C
============================
B

subgoal 2 is:
C

Sample_of_split < assumption.
1 subgoal

A : Prop
B : Prop
C : Prop
a : A
b : B
c : C
============================
C

Sample_of_split < assumption.
Proof completed.

Sample_of_split < Qed.

No comments: