[Coq] Coq Advent Calender : elim (17 of 25)

　Coq でよく使われる tactic の17番目は elim です。

　elim はほとんど induction と同じ事が出来ます。例えばこんな感じ。帰納法の仮定を自分で intro する必要があるのが違います。

Coq < Lemma Sample_of_elim : forall n, n + 0 = n.
1 subgoal
  
  ============================
   forall n : nat, n + 0 = n

Sample_of_elim < intros.
1 subgoal
  
  n : nat
  ============================
   n + 0 = n

Sample_of_elim < elim n.
2 subgoals
  
  n : nat
  ============================
   0 + 0 = 0

subgoal 2 is:
 forall n0 : nat, n0 + 0 = n0 -> S n0 + 0 = S n0

Sample_of_elim < 

　ただこうやって帰納法で使うときはinductionする方が多い様にも思います。（golfだとelimが有利なのかな？）

　下記の様にゴールが False で、仮定が ~P の形をしている時は、私は習慣で他のタクティックではなく elim を使います。こんな感じ。

Coq < Lemma Sample_of_elim' : forall P, ~~(P \/ ~P).
1 subgoal
  
  ============================
   forall P : Prop, ~ ~ (P \/ ~ P)

Sample_of_elim' < intros.
1 subgoal
  
  P : Prop
  ============================
   ~ ~ (P \/ ~ P)

Sample_of_elim' < intro npnp.
1 subgoal
  
  P : Prop
  npnp : ~ (P \/ ~ P)
  ============================
   False

Sample_of_elim' < elim npnp.
1 subgoal
  
  P : Prop
  npnp : ~ (P \/ ~ P)
  ============================
   P \/ ~ P

Sample_of_elim' < right.
1 subgoal
  
  P : Prop
  npnp : ~ (P \/ ~ P)
  ============================
   ~ P

Sample_of_elim' < intro p.
1 subgoal
  
  P : Prop
  npnp : ~ (P \/ ~ P)
  p : P
  ============================
   False

Sample_of_elim' < elim npnp.
1 subgoal
  
  P : Prop
  npnp : ~ (P \/ ~ P)
  p : P
  ============================
   P \/ ~ P

Sample_of_elim' < left.
1 subgoal
  
  P : Prop
  npnp : ~ (P \/ ~ P)
  p : P
  ============================
   P

Sample_of_elim' < exact p.   
Proof completed.

Sample_of_elim' < Qed.
intros.
intro npnp.
elim npnp.
right.
intro p.
elim npnp.
left.
exact p.

Sample_of_elim' is defined

Coq <