16

Coq Proof Assistant を使用して、(小さな) プログラミング言語のモデルを実装しています (Bruno De Fraine、Erik Ernst、Mario Südholt による Featherweight Java の実装を拡張しています)。このタクティックを使用する際に常に頭に浮かぶことの 1 つinductionは、型コンストラクターにラップされた情報をどのように保持するかということです。

次のように実装されたサブタイピング Prop があります。

Inductive sub_type : typ -> typ -> Prop :=
| st_refl : forall t, sub_type t t
| st_trans : forall t1 t2 t3, sub_type t1 t2 -> sub_type t2 t3 -> sub_type t1 t3
| st_extends : forall C D,
    extends C D ->
    sub_type (c_typ C) (c_typ D).

Hint Constructors sub_type.

はextendsJava で見られるクラス拡張メカニズムでtypあり、使用可能な 2 種類の型を表します。

Inductive typ : Set :=
| c_typ : cname -> typ
| r_typ : rname -> typ.

型情報を保存したい場所の例は、次のようinductionな仮説で戦術を使用する場合です。

H: sub_type (c_typ u) (c_typ v)

例えば

u : cname
v : cname
fsv : flds
H : sub_type (c_typ u) (c_typ v)
H0 : fields v fsv
============================
 exists fs : flds, fields u (fsv ++ fs)

usingは、 およびinduction H.に関するすべての情報を破棄します。ケースはuvst_refl

u : cname
v : cname
fsv : flds
t : typ
H0 : fields v fsv
============================
 exists fs : flds, fields u (fsv ++ fs)

ご覧のとおり、 とのコンストラクタに関連する情報、つまり に関連するu情報は失われます。さらに悪いことに、このために Coq はそれを見ることができず、実際にはこの場合は同じでなければなりません。vtypHtuv

Coqinversionでタクティックを使用すると、 とが同じであることがわかります。ただし、およびケースを証明するために生成される誘導仮説が必要なため、この戦術はここでは適用できません。Huvinductionst_transst_extends

コンストラクターにラップされているものに関する情報を破壊することなく、誘導仮説を生成し、等式を導出することの両方を組み合わせた戦術はありinversionますか? inductionまたは、必要な情報を手動で取得する方法はありますか? 両方とも、多くの変換が自動的に適用されることを示しています (特に を使用info inversion H) 。これらにより、私は建設と一緒に戦術を試してみましたが、進歩はありませんでした.info induction Hinversionchangelet ... in

4

3 に答える 3

15

sub_type (c_typ u) (c_typ v)これは、パラメーターが特定の構造 ( ) を持つ従属型 ( ) を持つ仮説を導入する必要がある場合の一般的な問題ですc_typ u。一般的なトリックがあります。これは、構造化されたパラメーターを変数に選択的に書き換え、環境内での同等性を維持することです。

set (t1 := c_typ u) in H; assert (Eq1 : t1 = c_typ u) by reflexivity; clearbody t1.
set (t2 := c_typ u) in H; assert (Eq2 : t2 = c_typ u) by reflexivity; clearbody t2.
induction H. (*often "; try subst" or "; try rewrite Eq1; try rewrite Eq2" *).

Coq 8.2 以降、この一般的な set-assert-clearbody パターンは、組み込みの tactic によって実行されます。remember term as ident in *goal_occurences*

これは、この戦術を使用して証明されたばかげた補題です。

Lemma subtype_r_left_equal :
  forall r1 t2, sub_type (r_typ r1) t2 -> r_typ r1 = t2.
Proof.
  intros.
  remember (r_typ r1) as t1 in H.
  induction H.
  congruence.
  solve [firstorder].
  discriminate.
Qed.

おまけのヒント (経験からですが、かなり前のことなので詳細は覚えていません): 型システムでかなりの構文推論を行っている場合 (これらの種類の機械的証明を行う場合によくあることです)、で判断を入力しておくと便利Setです。タイプ派生を、あなたが推論しているオブジェクトと考えてください。型の派生に等式を導入すると便利だったケースを覚えていますが、これは .NET の型の派生では常に機能するとは限りませんProp。

あなたのProblem.vで、ここに再帰性ケースの証明があります。推移性については、誘導仮説が十分に強力ではないと思われます。これは、問題を単純化した方法の副産物である可能性がありますが、推移性には驚くほど複雑な誘導仮説または補題が必要になることがよくあります。

Fact sub_type_fields: forall u v fsv,
  sub_type (c_typ u) (c_typ v) -> fields v fsv ->
  exists fs, fields u (fsv ++ fs).
Proof.
  intros.
  remember (c_typ u) as t1 in H.
  remember (c_typ v) as t2 in H.
  induction H.
  (* case st_refl *)
  assert (v = u). congruence. subst v t.
  exists nil. rewrite <- app_nil_end. assumption.
  (* case st_trans *)
  subst t1 t3.
  (* case st_extends *)
Admitted.
于 2010-12-23T21:06:33.787 に答える
7

私は同様の問題に遭遇し、Coq 8.3 の「従属誘導」戦術が問題を解決しました。

于 2011-02-04T15:04:13.007 に答える
3

CPDT がこの問題についてコメントしていることは確かでしたが、それがどこにあるのかは完全には明らかではありません。ここにいくつかのリンクがあります：

  1. http://adam.chlipala.net/cpdt/html/Cpdt.Predicates.htmlセクション「暗黙の等価性を持つ述語」は、Coq が「情報を失う」(インダクションではなくデストラクトで) おそらく最も単純なケースを示しています。また、この情報が失われる理由についても説明します。自由変数ではない引数に適用された型を破棄すると、最初にそれらの型が自由変数に置き換えられます (これが、Coq が情報を失う理由です)。

  2. http://adam.chlipala.net/cpdt/html/Cpdt.Universes.htmlセクション「公理を回避する方法」では、Gilles によって説明された「等式のトリック」を含む、公理 K を回避するためのいくつかのトリックを示します。「型ファミリへの非変数引数の誘導をサポートするための一般的な等価ベースのトリックの使用」を検索します

この現象は依存パターンマッチングと密接に関係していると思います。

于 2016-05-01T06:00:32.077 に答える