[Coq] Coq Advent Calender : generalize (20 of 25)

　Coqでよく使われる tactic の20番目は generalize です。

　generalize は intro の逆で、具体的な値の term を、"forall t" のような形に戻します。
　簡単な使用例は下記の様なものです。

Coq < Lemma sample_of_generalize : forall x y, 0 <= x + y + y.
1 subgoal
  
  ============================
   forall x y : nat, 0 <= x + y + y

sample_of_generalize < intros.
1 subgoal
  
  x : nat
  y : nat
  ============================
   0 <= x + y + y

sample_of_generalize < generalize (x + y + y).
1 subgoal
  
  x : nat
  y : nat
  ============================
   forall n : nat, 0 <= n

sample_of_generalize < Require Import Arith.Le.

sample_of_generalize < apply le_O_n.
Proof completed.

sample_of_generalize < Qed.

　単純に generalize で戻せない場合は、generalize dependent t のような形で使います。例えば下記の証明（TAPLの練習問題の証明）で使っています。よほど明らかな場合以外は、generalize dependentの形で使う事が多い様に思います。
　まず証明の前提の定義を幾つか。

Inductive term : Set :=
| TmTrue : term
| TmFalse : term
| TmIf : term -> term -> term -> term
| TmZero : term
| TmSucc : term -> term
| TmPred : term -> term
| TmIszero : term -> term.

Inductive nvalue : term -> Prop :=
| NvZero : nvalue TmZero
| NvSucc : forall t, nvalue t -> nvalue (TmSucc t).

Inductive bvalue : term -> Prop :=
| BvTrue : bvalue TmTrue
| BvFalse : bvalue TmFalse.

Definition value(t:term) : Prop := bvalue t \/ nvalue t.

Inductive eval : term -> term -> Prop :=
| EvIfTrue : forall t2 t3, eval (TmIf TmTrue t2 t3) t2
| EvIfFalse : forall t2 t3, eval (TmIf TmFalse t2 t3) t3
| EvIf : forall t1 t1' t2 t3, eval t1 t1' -> eval (TmIf t1 t2 t3) (TmIf t1' t2 t3)
| EvSucc : forall t1 t1', eval t1 t1' -> eval (TmSucc t1) (TmSucc t1')
| EvPred : forall t1 t1', eval t1 t1' -> eval (TmPred t1) (TmPred t1')
| EvPredZero : eval (TmPred TmZero) TmZero
| EvPredSucc : forall nv, nvalue nv -> eval (TmPred (TmSucc nv)) nv
| EvIszeroZero : eval (TmIszero TmZero) TmTrue
| EvIszeroSucc : forall nv, nvalue nv -> eval (TmIszero (TmSucc nv)) TmFalse
| EvIszero : forall t1 t1', eval t1 t1' -> eval (TmIszero t1) (TmIszero t1').

Notation "t1 --> t2" := (eval t1 t2) (at level 80, no associativity).

Definition normal_form (t : term) : Prop := ~ exists t', eval t t'.

　ここで下記の定理を証明します。intros を下記の様にすると予めdestructした形で intros 可能です。

Coq < Lemma value_is_normal_form : forall v, value v -> normal_form v.
1 subgoal
  
  ============================
   forall v : term, value v -> normal_form v

value_is_normal_form < intros v [bv|nv] [t vEt].
2 subgoals
  
  v : term
  bv : bvalue v
  t : term
  vEt : v --> t
  ============================
   False

subgoal 2 is:
 False

value_is_normal_form < destruct bv; inversion vEt.
1 subgoal
  
  v : term
  nv : nvalue v
  t : term
  vEt : v --> t
  ============================
   False

ここで t をgeneralize dependentします。（generalize t だと、forall t:term, にならずうまくいかない。）

value_is_normal_form < generalize dependent t.
1 subgoal
  
  v : term
  nv : nvalue v
  ============================
   forall t : term, v --> t -> False

value_is_normal_form < induction nv.
2 subgoals
  
  ============================
   forall t : term, TmZero --> t -> False

subgoal 2 is:
 forall t0 : term, TmSucc t --> t0 -> False

value_is_normal_form < intros t zEt.                
2 subgoals
  
  t : term
  zEt : TmZero --> t
  ============================
   False

subgoal 2 is:
 forall t0 : term, TmSucc t --> t0 -> False

value_is_normal_form < inversion zEt.
1 subgoal
  
  t : term
  nv : nvalue t
  IHnv : forall t0 : term, t --> t0 -> False
  ============================
   forall t0 : term, TmSucc t --> t0 -> False

value_is_normal_form < intros t0 stEt0.
1 subgoal
  
  t : term
  nv : nvalue t
  IHnv : forall t0 : term, t --> t0 -> False
  t0 : term
  stEt0 : TmSucc t --> t0
  ============================
   False

value_is_normal_form < inversion stEt0.
1 subgoal
  
  t : term
  nv : nvalue t
  IHnv : forall t0 : term, t --> t0 -> False
  t0 : term
  stEt0 : TmSucc t --> t0
  t1 : term
  t1' : term
  H0 : t --> t1'
  H : t1 = t
  H1 : TmSucc t1' = t0
  ============================
   False

value_is_normal_form < elim (IHnv t1').
1 subgoal
  
  t : term
  nv : nvalue t
  IHnv : forall t0 : term, t --> t0 -> False
  t0 : term
  stEt0 : TmSucc t --> t0
  t1 : term
  t1' : term
  H0 : t --> t1'
  H : t1 = t
  H1 : TmSucc t1' = t0
  ============================
   t --> t1'

value_is_normal_form < exact H0.
Proof completed.

value_is_normal_form < Qed.