<URL:http://www.morikita.co.jp/books/book/3287>
計算で可能なことは計算でやったほうが証明が簡単になるというのはポアンカレ原理というらしい。 でも検索しても出てこないなぁ。 1902年ということなので、「科学と仮説」という本に載っているのかな。
それはそれとして、読んでいて気がついたこと:
elim. と apply: XXX_ind と同じ結果になるかどうか、について少し調べてみた。
違う結果になる、と思った原因は以下の経験があったからであり、(SSReflectではなく) Coq の elim と apply nat_ind の話だった。
Goal forall n, n + 0 = n. intro n. elim n. (* subgoal: 0 + 0 = 0 subgoal: forall n0 : nat, n0 + 0 = n0 -> S n0 + 0 = S n0 *) Abort. Goal forall n, n + 0 = n. intro n. apply nat_ind. (* subgoal: n + 0 = 0 subgoal: forall n0 : nat, n + 0 = n0 -> n + 0 = S n0 *) Abort.
ただし、これは SSReflect でも似た挙動になる。
From mathcomp Require Import all_ssreflect. Goal forall n, n + 0 = n. move=> n. elim: n. (* subgoal: 0 + 0 = 0 subgoal: forall n : nat, n + 0 = n -> n.+1 + 0 = n.+1 *) Abort. Goal forall n, n + 0 = n. move=> n. apply: nat_ind. (* subgoal: n + 0 = 0 subgoal: forall n0 : nat, n + 0 = n0 -> n + 0 = n0.+1 *) Abort.
しかし、これは elim: n と apply: nat_ind. の比較になっていて、 記述されていた elim. と apply: nat_ind. の比較になっていない。 elim. をするには move=> n する前の状態でなければならないので、 その状態だと以下のように同じになる。
From mathcomp Require Import all_ssreflect. Goal forall n, n + 0 = n. elim. (* subgoal: 0 + 0 = 0 subgoal: forall n : nat, n + 0 = n -> n.+1 + 0 = n.+1 *) Abort. Goal forall n, n + 0 = n. apply: nat_ind. (* subgoal: 0 + 0 = 0 subgoal: forall n : nat, n + 0 = n -> n.+1 + 0 = n.+1 *)
Coq の elim や induction は引数が必要なので、SSReflect の elim. 相当のことはできないが、 apply については同じ結果になる。
Goal forall n, n + 0 = n. apply nat_ind. (* subgoal: 0 + 0 = 0 subgoal: forall n : nat, n + 0 = n -> S n + 0 = S n *)
ただし、以下のように定義した関数 f を使った状態では、 Coq の apply と SSReflect の apply: は異なる結果になる。
Coq では以下のようになり、これは証明できない。
Definition f z := forall n, n + z = n. Goal f 0. apply nat_ind. (* subgoal: f 0 subgoal: forall n : nat, f n -> f (S n) *)
SSReflect では以下のようになり、うまくいく。
From mathcomp Require Import all_ssreflect. Definition f z := forall n, n + z = n. Goal f 0. apply: nat_ind. (* subgoal: 0 + 0 = 0 subgoal: forall n : nat, n + 0 = n -> n.+1 + 0 = n.+1 *)
この違いは apply と apply: で nat_ind の P の探しかたが違うことに起因する。
nat_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P n.+1) -> forall n : nat, P n
Coq の apply には、補題の結論が P x であり、ゴールの結論が g y という形の場合は P を g、x を y にマッチさせるという仕掛けが入っている。
それに対して SSReflect の apply: t は、以下のような refine を順に試して最初にうまくいったものを使う、となっている。
refine t refine (t _) refine (t _ _) ...
この f 0 については、_ が 3つの場合と 4 つの場合に成功する。
From mathcomp Require Import all_ssreflect. Definition f z := forall n, n + z = n. Goal f 0. refine (nat_ind _ _ _). (* subgoal: 0 + 0 = 0 subgoal: forall n : nat, n + 0 = n -> n.+1 + 0 = n.+1 *) Abort. Goal f 0. refine (nat_ind _ _ _ _). (* subgoal: f 0 subgoal: forall n : nat, f n -> f n.+1 *) Abort.
この場合には _ が少ない 3つのほうが証明がうまくいくケースであったが、 複数の可能性がある場合に、常に少ない方が証明がうまくいくものであるかはわからない。
Canonical Structure をちゃんと調べたことがなかったので、少し調べた。
マニュアルは (あと、昨日読んだ本も) 意味のある、でも少し複雑な例で説明されているので、 意味はないけれど単純な例を自分で作ってみた。
Structure struct_type := struct_cstr { type_field : Type; nat_field : nat }.
Definition struct_val1 := struct_cstr bool 1.
Definition struct_val2 := struct_cstr bool 2.
Definition f (x : struct_type) (y : type_field x) := nat_field x.
Compute f struct_val1 true.
Fail Compute f _ true.
(* ここの _ は引数 x を推論させる指定だが、これは推論できない。
手がかりは type_field x が bool であるということだけだが、
それを満たす x は struct_val1 でも struct_val2 でも、
あるいは struct_cstr bool N で作った何でもいいので推論できないのは当然 *)
Compute f _ (true : type_field struct_val1). (* = 1 *)
Compute f _ (true : type_field struct_val2). (* = 2 *)
(* 第2引数yのところを cast の形で
type_field struct_val1 とか type_field struct_val2 と書いておくと、
推論してくれる *)
Goal type_field struct_val1 = type_field struct_val2.
Proof. exact (@eq_refl Type bool). Qed.
(* type_field struct_val1 と type_field struct_val2 は結局のところ
bool なので、convertible である。
convertible なものは Gallina では同じものとして扱われる、
というのは推論が終わってからの話で、
推論中は convertible なものであっても違う扱いになることがあるのだな。 *)
Canonical Structure struct_val1' := struct_val1.
(* type_field x が bool であるときに x を struct_val1 であると
推論するように設定する *)
Compute f _ true. (* = 1 *)
(* Canonical Structure の設定により、_ は struct_val1 と推論され、
struct_val1 の nat_field の 1 が返ってくる *)
Definition f1 := f _ true.
Print f1. (* f1 = f struct_val1' true *)
(* 推論の結果、実際に埋められるものは Canonical Structure で := の左に
書いた識別子が使われるようだ。
わざわざ識別子を指定させるのはここで使うためなのだな。 *)
Fail Compute f _ 0.
(*
The term "0" has type "nat" while it is expected to have type
"type_field ?x".
*)
(* type_field x が nat であるときに x がなんであるかは設定していないので、
ここでは失敗する *)
Canonical Structure struct_val2' := struct_val2.
(*
struct_val2' is defined
Ignoring canonical projection to S by nat_field in struct_val2': redundant
with struct_val1' [redundant-canonical-projection,typechecker]
Ignoring canonical projection to bool by type_field in struct_val2':
redundant with struct_val1' [redundant-canonical-projection,typechecker]
*)
(* type_field x が bool であるときの x を以前とは異なる struct_val2 と設定してみようとすると、
無視されると警告される
*)
Compute f _ true. (* = 1 *)
(* 警告にあったように無視され、f _ true の _ は struct_val1 に推論され、1 が返ってくる。
もし、struct_val2 に推論されるなら、2 が返ってくるはずである。 *)
なお、Canonical Structure struct_val1' := struct_val1. を Canonical struct_val1' := struct_val1. とか、 Canonical struct_val1. と書けるようにするのは SSReflect の機能の模様。
なら、Canonical struct_val1 って書くと、何で埋めるのか、 と疑問に思ってやってみると、以下のように struct_val1 そのものが埋められる模様。
From mathcomp Require Import ssreflect.
Structure struct_type := struct_cstr { type_field : Type; nat_field : nat }.
Definition struct_val1 := struct_cstr bool 1.
Definition f (x : struct_type) (y : type_field x) := nat_field x.
Canonical struct_val1.
Definition f1 := f _ true.
Print f1. (* f1 = f struct_val1 true *)
では、Canonical struct_cstr bool 1. とかするとどうなるか、というと、 これは syntax error だった。
[latest]