今日の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.
