Coqで既存の型付きコンストラクターの等価性を実装するための型のパターンマッチング

debugcn 投稿 Dev

私は私の名前です

存在記号のあるデータ型に再び小さな問題があるとしましょう。今回は、typeの2つの値がいつext等しいかを定義したいと思います。

Inductive ext (A: Set) :=
| ext_ : forall (X: Set), option X -> ext A.

Fail Definition ext_eq (A: Set) (x y: ext A) : Prop :=
  match x with
  | ext_ _ ox => match y with
                 | ext_ _ oy => (* only when they have the same types *)
                                ox = oy
                 end
  end.

私がやりたいのは、実存型が実際に同じである場合とそうでない場合をどうにかして区別することです。これはJMeqの場合ですか、それともそのような場合の区別を実現する他の方法がありますか？

私はたくさんグーグルで検索しましたが、残念ながら、依存パターンマッチングに関する投稿に出くわしました。

また、を使用して（ブール）スキームを生成しようとしScheme Equality for extましたが、type引数のため、これは成功しませんでした。

ガレ

私がやりたいのは、実存型が実際に同じである場合とそうでない場合をどうにかして区別することです。

Coqの論理は、同型型が等しいという一価公理と互換性があるため、これは不可能です。したがって、(unit * unit)とunitは構文的には異なりますが、Coqのロジックでは区別できません。

考えられる回避策は、関心のあるタイプのコードのデータ型を用意し、それを実存的なものとして保存することです。このようなもの：

Inductive Code : Type :=
  | Nat : Code
  | List : Code -> Code.

Fixpoint meaning (c : Code) := match c with
  | Nat     => nat
  | List c' => list (meaning c')
end.

Inductive ext (A: Set) :=
  | ext_ : forall (c: Code), option (meaning c) -> ext A.

Lemma Code_eq_dec : forall (c d : Code), { c = d } + { c <> d }.
Proof.
intros c; induction c; intros d; destruct d.
- left ; reflexivity.
- right ; inversion 1.
- right ; inversion 1.
- destruct (IHc d).
  + left ; congruence.
  + right; inversion 1; contradiction.
Defined.

Definition ext_eq (A: Set) (x y: ext A) : Prop.
refine(
  match x with | @ext_ _ c ox =>
  match y with | @ext_ _ d oy =>
  match Code_eq_dec c d with
   | left eq   => _
   | right neq => False
  end end end).
subst; exact (ox = oy).
Defined.

ただし、これにより、にパックできるタイプの種類がかなり制限されることは明らかですext。他のより強力な言語（たとえば、誘導再帰を備えている）は、より表現力を与えます。

この記事はインターネットから収集されたものであり、転載の際にはソースを示してください。

侵害の場合は、連絡してください[email protected]