Streicher_K_ Axiomの使い方

Question

誰かに簡単な例を教えてもらえますかStreicher_K_公理Coq.Logic.EqdepFactsから？

はたぶん単純な事実を示すために：私もある、Streicher_K_でそれを証明する方法を見つけ試行錯誤によって

Variable A:Type. 
Variable x:A. 
Axiom SK:Streicher_K_on_ A x (fun p:x=x => (eq_refl x) = p). 

Lemma single_proof : forall (y:A)(u v:x = y), u = v. 
intros. 
destruct u. 
apply (SK). 
reflexivity. 
Qed. 

：

Lemma single_proof : forall (A:Type)(x y:A) (u v:x = y), u = v. 

私はStreicher_K_on_でそれを証明するために管理しましたさらに簡単に：

Axiom SK:Streicher_K_ A. 

しかし、問題は私はなぜこれがうまくいくのかわかりません。私は基本的な型チェックを理解していません。

Answer 1

Kとその多くの同等のステートメント

公理Kの文が一目で把握することが少し難しいです。追加のパラメータがあるため、標準ライブラリで理解することはさらに困難です。幸いなことに、それはあなたが証明しようとしていたものを一般化し、次の代替、と等価であり、私たちは、実際に必要なものが多いです。

UIP : forall (T : Type) (x y : T) (p q : x = y), p = q 

（「UIPは」の略で、「アイデンティティ証明の単一性。」）

Coq標準ライブラリには、EqdepTheoryモジュールがあり、これらの2つのステートメントとそれ以外のいくつかの同様のものがこの等価性を示しています。それは、人はそれらのいずれかを想定しながら、私たちは自由にこれらのステートメントのいずれかを使用することができますeq_rect_eq：

Require Import Coq.Logic.EqdepFacts. 

Module Ax : EqdepElimination. 

Axiom eq_rect_eq : 
    forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), 
     x = eq_rect p Q x p h. 

End Ax. 

Module Export UIPM := EqdepTheory Ax. 

このスニペットの後、我々は、例えば、

Check UIP. 

を実行することができますしかし、どのように我々は何かを証明しませんK？

あなたはUIPを証明するためにKを使う方法についても困惑したようです。答えは次の文章の中にあります。

Definition J (A : Type) (x : A) (P : forall y, x = y -> Prop) : 
    P x eq_refl -> forall y (p : x = y), P y p := 
    fun H y p => 
    match p with 
    | eq_refl => H 
    end. 

一見、KとJはかなり似ています。

J : forall (A : Type) (x : A) (P : forall y : A, x = y -> Prop), 
    P x eq_refl -> forall (y : A) (p : x = y), P y p 

K : forall (A : Type) (x : A) (P :    x = x -> Prop), 
    P eq_refl -> forall   (p : x = x), P p 

（私は読みやすくするためKの代わりStreicher_Kを書きました。）一つの違いは、Jが右辺に関しては一般的なものであり等式x = yの述語Pによってパラメータ化されていることであるy：さんが自分のタイプを比較してみましょう。 Kも述語がPですが、一致度はx = xのみとみなされます。

Jは、上記のようにCoqの理論で証明されていますが、Kは理論に余分な公理を加えることによってのみ証明できます。 Kで使用される述語PがJで使用されるものよりも具体的であるが、match文がCoqでどのようにタイプされたかの結果であることを考えると、これは驚くように見えるかもしれない。

KとJを組み合わせることで、UIPの証明に到達することができます。 Jは、私たちは、任意の等式にこれを一般化することができ、

Definition UIP_refl (A : Type) (x : A) (p : x = x) : eq_refl = p := 
    Streicher_K A x (fun q => eq_refl = q) eq_refl p. 

その後：Jの定義は、パターンを使用していることを

Definition UIP (A : Type) (x y : A) (p q : x = y) : p = q := 
    J A x (fun y p => forall q : x = y, p = q) (UIP_refl A x) y p q. 

はお知らせのは最初だけ再帰等式のために働くことを、それの特殊なバージョンを証明してみましょうマッチング。 Coqはdestruct (SK).を呼び出したときに、あなたの証明にパターンマッチングを使用していました。