auto の話
Coq.Sets.Ensembles がなんだかうまく使えないなあ,と思った話。ちなみに以下で使う諸定義は http://coq.inria.fr/stdlib/Coq.Sets.Ensembles.html を必要に応じて参照してください。
具体的には何かというと,
Coq < Goal forall x : A, forall X : Ensemble A, In _ (Add _ X x) x. 1 subgoal ============================ forall (x : A) (X : Ensemble A), In A (Add A X x) x Unnamed_thm3 < auto with sets. 1 subgoal ============================ forall (x : A) (X : Ensemble A), In A (Add A X x) x
となってしまうということで,要するに「なんかの集合に x を加えてできる集合には x が属する」という自明に思える主張を auto が証明してくれなくて残念であると言いたいわけです。
どうしてできないか調べてみましょう。debug eauto するとどこまで行ってどこで詰まったかがわかったりします。
Unnamed_thm3 < debug eauto with sets. 1 depth=5 1.1 depth=5 intro 1.1.1 depth=5 intro 1.1.1.1 depth=4 unfold In 1.1.1.1.1 depth=3 unfold Add 1.1.2 depth=4 unfold In 1.1.2.1 depth=4 intro 1.1.2.1.1 depth=3 unfold Add 1.1.2.2 depth=3 unfold Add 1.1.2.2.1 depth=3 intro 1.2 depth=4 unfold In 1.2.1 depth=4 intro 1.2.1.1 depth=4 intro 1.2.1.1.1 depth=3 unfold Add 1.2.1.2 depth=3 unfold Add 1.2.1.2.1 depth=3 intro 1.2.2 depth=3 unfold Add 1.2.2.1 depth=3 intro 1.2.2.1.1 depth=3 intro 1 subgoal ============================ forall (x : A) (X : Ensemble A), In A (Add A X x) x
正確な読み方は知らないんですが,なんとなく In, Add を unfold した後で行き詰まってることが読み取れます。それなら問題の subgoal を見てみましょう。
Unnamed_thm3 < intros; unfold In, Add. 1 subgoal x : A X : Ensemble A ============================ Union A X (Singleton A x) x
ここから先が証明できなかったということでしょう。
右側に入っていることは自明に見えますが,
Unnamed_thm3 < debug eauto with sets. 1 depth=5 1 subgoal x : A X : Ensemble A ============================ Union A X (Singleton A x) x
本当に何もできないようです。本当ですか。
Unnamed_thm3 < Print Hint. Applicable Hints : In the database and_iff_morphism: nothing In the database and_impl_morphism: nothing In the database arith: nothing In the database bool: nothing In the database core: nothing In the database datatypes: nothing In the database decidable_prop: nothing In the database eq_true: nothing In the database equiv_reflexive: nothing In the database equiv_symmetric: nothing In the database extcore: nothing In the database iff_Reflexive: nothing In the database iff_Symmetric: nothing In the database iff_Transitive: nothing In the database iff_iff_iff_impl_morphism: nothing In the database impl_Reflexive: nothing In the database impl_Transitive: nothing In the database not_iff_morphism: nothing In the database not_impl_morphism: nothing In the database or_iff_morphism: nothing In the database or_impl_morphism: nothing In the database ord: nothing In the database pointwise_equivalence: nothing In the database relations: (external) RelationClasses.solve_relation(4) In the database respectful_per: nothing In the database sets: nothing In the database typeclass_instances: nothing In the database v62: nothing In the database zarith: nothing
本当なようです。なんででしょう。
とりあえず人の手で少し助けて証明してみます。Union_intror という Union 型のコンストラクタが,右側の成分に入っていることから Union 全体にも入っていることを示すのに使えます。
Unnamed_thm3 < apply Union_intror; auto with sets. Proof completed.
残りは auto で終わりました。ということは,行き詰まっていたところで Union_intror が適用できることさえ認識されれば,もともとの goal も自動証明できるはずです。
さて,それではなぜ Union_intror が applicable hint とみなされないのでしょうか。それは型を見てみればわかります。
Unnamed_thm3 < Check Union_intror. Union_intror : forall (U : Type) (B C : Ensemble U) (x : U), In U C x -> In U (Union U B C) x
こいつは In を head symbol にもちます。一方,もとの subgoal は Union を head symbol にもっています。auto は head symbol が一致しないものは適用できないとみなすので,Union A X (Singleton x) x という goal に対して Union_intror は適用できないと判断されます。(正確なことは http://coq.inria.fr/refman/Reference-Manual011.html#toc63 などを参照)
実際には In は identity なので,Union_intror の型を適当に簡約してやれば Union が head symbol になるようにできるのですが,そこまでは考慮してくれないようです。
とりあえず,以上の考察をもとに
Unnamed_thm3 < Hint Extern 0 (Union ?U ?B ?C ?e) => change (In _ (Union U B C) e).
とでもごまかしてやれば
Unnamed_thm3 < Restart. 1 subgoal ============================ forall (x : A) (X : Ensemble A), In A (Add A X x) x Unnamed_thm3 < auto with sets. Proof completed.
のようにうまくいくんですが,どうもスマートじゃないなあと思います。