[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.