[Coq] Coq Advent Calender : case (15 of 25)

　Coq でよく使われる tactic の15番目は case です。

　帰納的な型について自動で場合分けをしてくれるという意味では、13番目のinductionと同じですが、inductionと違って単に場合分けを行うだけで帰納法の仮定とかは作ってくれません。

　今回は３値論理を定義してみます。帰納的な bool3 という型を定義し、それらに対する否定、論理積、論理和を定義します。

Coq < Inductive bool3 : Set := yes | maybe | no.
bool3 is defined
bool3_rect is defined
bool3_ind is defined
bool3_rec is defined

Coq < Definition not3(b:bool3) :=
Coq <   match b with
Coq <   | yes => no
Coq <   | maybe => maybe
Coq <   | no => yes
Coq <   end.
not3 is defined

Coq < Definition and3(a b:bool3) :=
Coq <   match a,b with
Coq <   | yes,yes => yes
Coq <   | no, _ => no
Coq <   | _, no => no
Coq <   | _,_ => maybe
Coq <   end.
and3 is defined

Coq < Definition or3(a b:bool3) :=
Coq <   match a,b with
Coq <   | no,no => no
Coq <   | yes,_ => yes
Coq <   | _,yes => yes
Coq <   | _,_ => maybe
Coq <   end.
or3 is defined

Coq <

　では、bool3 における簡単な証明をしてみます。a, b についての場合分けを行うのに case タクティックを使用します。下記の例では case でゴールが増えるのを示したいので個別に case を使っていますが、普通は
case a; case b; reflexivity.
で一行で９通りの場合分けを実施して終了とするでしょう。

Coq < Lemma Sample_of_case : forall a b:bool3,
Coq <   not3 (or3 a b) = and3 (not3 a) (not3 b).
1 subgoal
  
  ============================
   forall a b : bool3, not3 (or3 a b) = and3 (not3 a) (not3 b)

Sample_of_case < intros a b.
1 subgoal
  
  a : bool3
  b : bool3
  ============================
   not3 (or3 a b) = and3 (not3 a) (not3 b)

Sample_of_case < case a.
3 subgoals
  
  a : bool3
  b : bool3
  ============================
   not3 (or3 yes b) = and3 (not3 yes) (not3 b)

subgoal 2 is:
 not3 (or3 maybe b) = and3 (not3 maybe) (not3 b)
subgoal 3 is:
 not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < case b.
5 subgoals
  
  a : bool3
  b : bool3
  ============================
   not3 (or3 yes yes) = and3 (not3 yes) (not3 yes)

subgoal 2 is:
 not3 (or3 yes maybe) = and3 (not3 yes) (not3 maybe)
subgoal 3 is:
 not3 (or3 yes no) = and3 (not3 yes) (not3 no)
subgoal 4 is:
 not3 (or3 maybe b) = and3 (not3 maybe) (not3 b)
subgoal 5 is:
 not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < reflexivity.
4 subgoals
  
  a : bool3
  b : bool3
  ============================
   not3 (or3 yes maybe) = and3 (not3 yes) (not3 maybe)

subgoal 2 is:
 not3 (or3 yes no) = and3 (not3 yes) (not3 no)
subgoal 3 is:
 not3 (or3 maybe b) = and3 (not3 maybe) (not3 b)
subgoal 4 is:
 not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < reflexivity.
3 subgoals
  
  a : bool3
  b : bool3
  ============================
   not3 (or3 yes no) = and3 (not3 yes) (not3 no)

subgoal 2 is:
 not3 (or3 maybe b) = and3 (not3 maybe) (not3 b)
subgoal 3 is:
 not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < reflexivity.
2 subgoals
  
  a : bool3
  b : bool3
  ============================
   not3 (or3 maybe b) = and3 (not3 maybe) (not3 b)

subgoal 2 is:
 not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < case b; reflexivity.
1 subgoal
  
  a : bool3
  b : bool3
  ============================
   not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < case b; reflexivity.
Proof completed.

Sample_of_case < Qed.