従属型のインスタンス間の等価性の証明

Question

代数構造（たとえばすべてのモノイドのクラス）に対応するクラスを正式化しようとすると、必要なすべてのモデルをモデル化する製品タイプとしてmonoid (a:Type)タイプを作成するのが自然な設計です（要素e:a、オペレータapp : a -> a -> a、モノイド法が満たされていることの証明など）。その際、マップmonoid: Type -> Typeを作成しています。このアプローチの潜在的な欠点は、モノタイプm:monoid a（サポートタイプがaのモノイド）とm':monoid b（モノイドサポートタイプb）が与えられていると、タイプが不正であるため、同等性m = m'を書くことはできません。別の設計では、タイプmonoidを作成することになります。サポートタイプは別のフィールドa:Typeであるため、m m':monoidを指定すると、m = m'かどうかを尋ねるのは常に意味があります。何らかの形で、mとm'が同じサポート（a m = a m）を持ち、演算子が等価（等価の公理のおかげで達成できるかもしれないapp m = app m'）であり、証明フィールドが問題ではないと主張したいと思います何らかの証明が無関係な公理を持っているなど）、m = m'。それは悪い型付けされているため、残念ながら、私たちはイベント我々が持っていると仮定し、問題を単純化するために...

を平等app m = app m'を表現することはできません。

Inductive myType : Type := 
| make : forall (a:Type), a -> myType. 
. 

私は、フォームの結果を持っているしたいと思います：

forall (a b:Type) (x:a) (y:b), a = b -> x = y -> make a x = make b y. 

この文は入力できないので、入力できません。

私は公理は私が2種類aとbが同じであることを証明することができますがあり、私はxとyがあまりにも確かに同じであることを示すことができるかもしれないが、私は私があると結論することが可能なツールを持っていると思いますmake a x = make b y。どんな提案も大歓迎です。

Answer 1

これを証明する低技術の方法は、提供された等価性を使用して手動の型キャストを挿入することです。つまり、仮定がx = yである代わりに、仮定は(CAST q x) = yです。以下では、キャストを明示的にマッチとして記述していますが、それを行う関数を定義することでより見栄えを良くすることもできます。

Inductive myType : Type := 
| make : forall (a:Type), a -> myType. 

Lemma ex : forall (a b:Type) (x:a) (y:b) (q: a = b), (match q in _ = T return T with eq_refl => x end) = y -> make a x = make b y. 
Proof. 
    destruct q. 
    intros q. 
    congruence. 
Qed. 

もJMeqとして知られる「異種の平等を」、使用することで、この機械のほとんどを非表示にするよりよい方法があります。詳細な紹介についてはthe Equality chapter of CPDTをお勧めします。この特定の定理はあなたがこのスタイルで形式化を行う場合は、平等に関する公理なしでコックに証明することができない目標を発生する可能性があり、公理なし証明することができるが、あなたの例では、一般的に

Require Import Coq.Logic.JMeq. 

Infix "==" := JMeq (at level 70, no associativity). 

Inductive myType : Type := 
| make : forall (a:Type), a -> myType. 

Lemma ex : forall (a b:Type) (x:a) (y:b), a = b -> x == y -> make a x = make b y. 
Proof. 
    intros. 
    rewrite H0. 
    reflexivity. 
Qed. 

になります。特に、この種の従属レコードの注入性は証明できません。 JMEqライブラリは、異種同値性についての公理JMeq_eqを自動的に使用するため、非常に便利です。