Hatena::Groupcoq

mzpの日記

 | 

2009-11-24

今日のCoq: InductiveなProp

定理の中で使うProp(命題)は、関数的に定義するよりも、Inductiveに定義したほうが証明が楽らしいですよ。

要約

  • Inductiveに定義したPropのほうが使いやすいらしい
  • Inductiveに定義したPropの各名前は、applyできる
  • Inductive Xを定義するとX_indが自動で定義される

前提

こんな簡単なラムダ式があると思ってください。

Inductive type : Set :=
    BoolT : type
  | FunT  : type -> type -> type.

Inductive term : Set :=
    Var     : string -> term
  | Bool    : bool   -> term
  | Lambda  : string -> type -> term -> term
  | Apply   : term  -> term -> term
  | If      : term -> term -> term -> term.

Definition is_value (t : term) :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      true
  | Apply _ _  | If _ _ _ =>
      false
  end.

ダメなPropの例

true/falseを返すかわりに、True/Falseを返すだけのやつ。

Definition value (t : term) : Prop :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      True
  | Apply _ _  | If _ _ _ =>
      False
  end.

イイPropの例

値とは何かを、帰納的(Inductive)に定義している。

Inductive Value  : term -> Prop :=
  | ValVar    : forall s : string, Value (Var s)
  | ValBool   : forall b : bool,   Value (Bool b)
  | ValLambda : forall (x : string) (ty : type) (body : term), Value (Lambda x ty body).

ここで与えたValVarとかいう名前は証明するときに使うので、覚えやすいのにするといいでしょう。

じゃあ、これを使って証明してみよう!(その1)

試しに、こんなんを証明してみましょう。

Theorem is_value_is_Value :
  forall t : term, is_value t = true -> Value t.

ようするに、is_value関数が正しく定義されているか証明したいわけです。

まずは、tについて場合分けします。Inductiveに定義されたデータ型は、inductionを使うよりdestructを使って場合分けしたほうがいいらしいです。

is_value_is_Value < destruct t.
5 subgoals

  s : string
  ============================
   is_value (Var s) = true -> Value (Var s)

subgoal 2 is:
 is_value (Bool b) = true -> Value (Bool b)
subgoal 3 is:
 is_value (Lambda s t t0) = true -> Value (Lambda s t t0)
subgoal 4 is:
 is_value (Apply t1 t2) = true -> Value (Apply t1 t2)
subgoal 5 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

Value (Var s)が登場するまで、適当にintroを使ってやります。

is_value_is_Value < Show 1.

  s : string
  ============================
   is_value (Var s) = true -> Value (Var s)

is_value_is_Value < intro.
5 subgoals

  s : string
  H : is_value (Var s) = true
  ============================
   Value (Var s)

subgoal 2 is:
 is_value (Bool b) = true -> Value (Bool b)
subgoal 3 is:
 is_value (Lambda s t t0) = true -> Value (Lambda s t t0)
subgoal 4 is:
 is_value (Apply t1 t2) = true -> Value (Apply t1 t2)
subgoal 5 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

ここで、さっき定義したValVarが使えます。

is_value_is_Value < Check ValVar.
ValVar
     : forall s : string, Value (Var s)

というわけで、これをapplyすれば証明が完了します。

is_value_is_Value < apply ValVar.
4 subgoals

  b : bool
  ============================
   is_value (Bool b) = true -> Value (Bool b)

subgoal 2 is:
 is_value (Lambda s t t0) = true -> Value (Lambda s t t0)
subgoal 3 is:
 is_value (Apply t1 t2) = true -> Value (Apply t1 t2)
subgoal 4 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

あとは、BoolとLambdaについても同様に証明できます。

is_value_is_Value < intro; apply ValBool.
3 subgoals

  s : string
  t : type
  t0 : term
  ============================
   is_value (Lambda s t t0) = true -> Value (Lambda s t t0)

subgoal 2 is:
 is_value (Apply t1 t2) = true -> Value (Apply t1 t2)
subgoal 3 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

is_value_is_Value < intro; apply ValLambda.
2 subgoals

  t1 : term
  t2 : term
  ============================
   is_value (Apply t1 t2) = true -> Value (Apply t1 t2)

subgoal 2 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

ApplyとIfについては、simplで簡約すると前提がFalseになります。これをintroで仮定に移動させて、discriminateを使ってやれば証明できます。

is_value_is_Value < Show.
2 subgoals

  t1 : term
  t2 : term
  ============================
   is_value (Apply t1 t2) = true -> Value (Apply t1 t2)

subgoal 2 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

is_value_is_Value < simpl.
2 subgoals

  t1 : term
  t2 : term
  ============================
   false = true -> Value (Apply t1 t2)

subgoal 2 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

is_value_is_Value < intro.
2 subgoals

  t1 : term
  t2 : term
  H : false = true
  ============================
   Value (Apply t1 t2)

subgoal 2 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

is_value_is_Value < discriminate.
1 subgoal

  t1 : term
  t2 : term
  t3 : term
  ============================
   is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

is_value_is_Value < simpl;intro; discriminate.
Proof completed.

じゃあ、これを使って証明してみよう!(その2)

じゃあ、逆向きも証明してみましょう。

Theorem Value_is_value :
  forall t : term, Value t -> is_value t = true.

で、これをtについて場合分けしても全然ハッピーになりません。

Inductiveで何かを定義した場合には、xxx_indが自動で定義されます。

Value_is_value < Check Value_ind.
Value_ind
     : forall P : term -> Prop,
       (forall s : string, P (Var s)) ->
       (forall b : bool, P (Bool b)) ->
       (forall (x : string) (ty : type) (body : term), P (Lambda x ty body)) ->
       forall t : term, Value t -> P t

これをapplyすると、いい感じのsubgoalがでてきます。あとはreflexivityだけで証明でいます。

Value_is_value < apply Value_ind.
3 subgoals

  ============================
   forall s : string, is_value (Var s) = true

subgoal 2 is:
 forall b : bool, is_value (Bool b) = true
subgoal 3 is:
 forall (x : string) (ty : type) (body : term),
 is_value (Lambda x ty body) = true
Value_is_value < reflexivity.
2 subgoals

  ============================
   forall b : bool, is_value (Bool b) = true

subgoal 2 is:
 forall (x : string) (ty : type) (body : term),
 is_value (Lambda x ty body) = true

Value_is_value < reflexivity.
1 subgoal

  ============================
   forall (x : string) (ty : type) (body : term),
   is_value (Lambda x ty body) = true

Value_is_value < reflexivity.
Proof completed.
 |