20 December, 2010

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

No comments: