[Coq] Coq Advent Calender : left, right (21,22 of 25)

　Coqでよく使われる tactic の21,22番目は left と right です。
　最初に25個と決めて、でもよく考えると12/24で終了すべき。都合が良いのでここで２つ紹介して帳尻を合わせます。

　left は constructor 1 、right は constructor 2 の意味で、実は goal が A \/ B の場合に限らず、コンストラクタが２通りあってどちらかを明示的に指定したい時に使えます。
　大抵そういう場合は左右と対応している訳ですが、例えば nat とかも left が O を指すはず。同様に n:nat に対して destruct n ではなく split とかも使えるはず。単に他人に判りにくいだけですが。

　今回は sumbool について left, right を使う例です。やはり左右に対応しています。

Coq < Lemma Sample_of_left_right : forall n:nat, {n = 0} + {n <> 0}.
1 subgoal
  
  ============================
   forall n : nat, {n = 0} + {n <> 0}

Sample_of_left_right < induction n.
2 subgoals
  
  ============================
   {0 = 0} + {0 <> 0}

subgoal 2 is:
 {S n = 0} + {S n <> 0}

Sample_of_left_right < left.
2 subgoals
  
  ============================
   0 = 0

subgoal 2 is:
 {S n = 0} + {S n <> 0}

Sample_of_left_right < reflexivity.
1 subgoal
  
  n : nat
  IHn : {n = 0} + {n <> 0}
  ============================
   {S n = 0} + {S n <> 0}

Sample_of_left_right < right.
1 subgoal
  
  n : nat
  IHn : {n = 0} + {n <> 0}
  ============================
   S n <> 0

Sample_of_left_right < intro.
1 subgoal
  
  n : nat
  IHn : {n = 0} + {n <> 0}
  H : S n = 0
  ============================
   False

Sample_of_left_right < inversion H.
Proof completed.

Sample_of_left_right < Qed.