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.

のようにうまくいくんですが,どうもスマートじゃないなあと思います。