コックが依存型指定された誘導性の命題

Question

のコンストラクタを区別することはできません私は私がいる問題を示すために、この例のタイプを作成しました：今

Inductive foo : nat -> Prop := 
| foo_1 : forall n, foo n 
| foo_2 : forall n, foo n. 

はっきりfoo_1 0 <> foo_2 0が、私はこれを証明することができないよ：

Lemma bar : foo_1 0 <> foo_2 0. 
Proof. unfold not. intros H. discriminate H. 

これは

Not a discriminable equality.

エラーを返します210はコンテキストをまったく変更しません。奇妙なことに、私がfooをPropからTypeに変更すると、証明は終わりますが、実際のコードでは問題が発生するため、これを行うことはできません。

どうすればこの証拠を得ることができますか？そして、なぜこの問題が最初に問題になっていますか？

Answer 1

短い回答：できません。

私たちも同じようなことを証明するために失敗した場合、のは、単純な例を見てみましょう：

Error: Not a discriminable equality.

さあ、試してみて、見つけるてみましょう：

Inductive baz : Prop := 
| baz1 : baz 
| baz2 : baz. 

Goal baz1 <> baz2. 
    intro H. 
    Fail discriminate H. 
Abort. 

上記は、次のエラーメッセージで失敗します正確にはdiscriminateが失敗します。

すべての最初に、回り道をして、非常に簡単な文を証明してみましょう：

Goal false <> true. 
    intro prf; discriminate. 
Qed. 

我々はまた、代わりに戦術を使用して、それを構築するのではなく、直接その証拠用語を提供することにより、上記の目的を証明することができます。

Goal false <> true. 
    exact (fun prf : false = true => 
    eq_ind false (fun e : bool => if e then False else True) I true prf). 
Qed. 

上記は、discriminateの戦術が単純化したものです。

のは、それに対応しfalse、true、およびbaz1と証明項のbool、baz2、bazを交換し、何が起こるか見てみましょう：以下で失敗し上記

Goal baz1 <> baz2. 
    Fail exact (fun prf : baz1 = baz2 => 
    eq_ind baz1 (fun e : baz => if e then False else True) I baz2 prf). 
Abort. 

：

The command has indeed failed with message:
Incorrect elimination of e in the inductive type baz :
the return type has sort Type while it should be Prop .
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Type
because proofs can be eliminated only to build proofs.

エラーの理由はこの抽象である：

Fail Check (fun e : baz => if e then False else True). 

上記に同じエラーメッセージが表示されます。 なぜそれが簡単か分かります。抽象化のタイプはbaz -> Propで、baz -> Propのタイプは何ですか？提案へ

Check baz -> Prop. (* baz -> Prop : Type *) 

命題の証明から地図Typeに住んで、ないPropで！それ以外の場合は、宇宙の矛盾が発生します。

それを行うためにPropを打破する方法がないのため、私たちの結論は、不平等を証明する方法がないということです - あなただけFalseの証明を構築するために（baz1 = baz2）を書き換え使用することはできません。

別の引数（私はそれが既に@gallaisによって提案されている参照）：それはいくつかの巧妙なトリックを使用してProp内に留まる証明を行うことができたならば、その後、proof irrelevance公理はコックのロジックと矛盾のようになります。

Variable contra : baz1 <> baz2. 
Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2. 
Check contra (proof_irrelevance _ baz1 baz2). (* False *) 

しかし、一貫性があることが知られています（Coq's FAQを参照）。

Universes の章CPDTのセクション「プロップユニバース」を具体的に参照してください。

Answer 2

Coqの根底にある論理は、与えられたPropの2つの証明が等しいことを示す「証明不当性」の公理と互換性があります。結果として、あなたが策定した陳述を証明することは不可能です。

2つのコンストラクタを区別できるようにする場合はPropではなくを誘導Typeにする必要があります。 barは有効な証明として受け入れられます。

Inductive foo : nat -> Type := 
| foo_1 : forall n, foo n 
| foo_2 : forall n, foo n. 

Lemma bar : foo_1 0 <> foo_2 0. 
Proof. unfold not. intros H. discriminate H. Qed.