CoqでHoTTパス誘導を使用するには？コックに

Question

は私が

Definition f (s:Unit) : tt=tt := match s with tt => idpath end. 
Definition g (p:tt=tt) : Unit := match p with idpath => tt end. 

を持っていると私はforall (p:tt=tt), (f o g) p = pを証明したいと思います。

私は、HoTTの本の1.12.1で説明したパス誘導を使用してそれを行いたいと思います。

それはpがidpathである場合のために、我々は

assert((f o g) idpath = idpath). 
simpl. 
reflexivity. 

を証明することができますしかし、どのように私は、全体の証明一緒にパッケージ化するコックにパス誘導を使用しないことは明らかですか？

今までに全体の証明：（？admitの代わりに入れて何）

Require Import HoTT. 
Definition f (s:Unit) : tt=tt := match s with tt => idpath end. 
Definition g (p:tt=tt) : Unit := match p with idpath => tt end. 
Theorem myTheorem : forall (p:tt=tt), (f o g) p = p. 
    assert((f o g) idpath = idpath). 
    simpl. 
    reflexivity. 
admit. 

Answer 1

コックのパス誘導のアナログはmatch構造です。 HoTTの本で説明したように、パス誘導を定義するためにこの方法を使用する方法があります。

Set Implicit Arguments. 

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

この定義のタイプは、我々が

• y : A、
• p : x = y、および
• P : forall y, x = y -> Typeは、

それで十分P y pを、証明したい時はいつでも、と述べていますそのことを示すためにP x eq_reflが成立する。 Jを使用して、g関数が定数であることを示すことができます。 （私はCoqの標準ライブラリによって与えられたものと一致する定義を言い換えています。）

Definition f (s : unit) : tt = tt := match s with tt => eq_refl end. 
Definition g (p : tt = tt) : unit := match p return unit with eq_refl => tt end. 

Definition g_tt p : g p = tt := 
    J (fun y q => match q return unit with eq_refl => tt end = tt) 
    eq_refl p. 

この証明のトリッキーな部分は、他のケースである、JのPパラメータがどうあるべきかを見つけ出すれますパス誘導によって進行する証明。ここでは、私は上記の使用qがtt = y型を持つのに対し、それは、タイプtt = ttの引数を必要とするため、gの定義を展開しなければなりませんでした。いずれにしても、P tt pは定義上はg p = ttに等しいことがわかります。これは私たちが証明したいものです。

p : tt = ttについては、p = eq_reflを表示するようにトリックを行うことができます。以前の結果と組み合わせることで、あなたが望むものを正確に与えることができます。

Definition result (p : tt = tt) : p = eq_refl := 
    J (fun y q => 
     unit_rect (fun z => tt = z -> Prop) 
       (fun u => u = eq_refl) 
       y q) 
    eq_refl p. 

また、要点はPパラメータです。我々は、我々がT ttの要素を見つけることができる時はいつでも（T : unit -> Typeとx : tt用）タイプT xの何かを定義することができると言うunitのための誘導原理を利用します。Jのこの適用の結果は、この場合にunit_rectための計算規則によってだけ

unit_rect (fun z => tt = z -> Prop) 
      (fun u => u = eq_refl) 
      tt p 
= (p = eq_refl) 

あるタイプ

P tt p 

を有するべきであることを想起されたいです。

残念なことに、この種の証明はCoqの戦術的言語で複製するのが難しいです。なぜなら、しばしばPの内容を推測することが困難なためです。この値があなた自身であるべきものを理解し、証明用語を明示的に書き留めるほうが簡単です。

私は理由をよく理解していませんが、matchと校正用語を書き留めた場合、この注釈を理解する上でCoqも非常に優れています。比較：

Definition result' (p : tt = tt) : p = eq_refl := 
    match p with eq_refl => eq_refl end. 

を、これは非常に簡単に見えますが、あなたはそれを印刷しようとすると、コックによって推測実際の用語ははるかに複雑であることがわかります。それを試してみてください！

編集

ああ、私はちょうどあなたがコックの格好いいバージョンを使用しようとしていたことに気づきました。私はそのバージョンがインストールされていないが、私はそれに私のソリューションを適応させることはあまり難しいとは思わないと思う。