ex_introの定義を読むにはどうすればよいですか？

Question

私が言うこれは、Mike Nahas's introductory Coq tutorialを読んでいる：に "ex_intro"

引数は次のとおりです。

• 述語
• 証人
• 証人と呼ばれる前提の証明

私はthe definition：

Inductive ex (A:Type) (P:A -> Prop) : Prop := 
    ex_intro : forall x:A, P x -> ex (A:=A) P. 

と私はそれを解析しています。式forall x:A, P x -> ex (A:=A) Pのどの部分が3つの引数（述語、証拠、証明）に対応していますか？

Check ex_intro. 

をあなたが、その後表示されるはずです：

ex_intro 
    : forall (A : Type) (P : A -> Prop) (x : A), P x -> exists x, P x 

これはex_introない取ると言うことがex_introのタイプのためのCoqのインタプリタとクエリを起動すると良いでしょう、マイクは何を意味するのか理解する

Answer 1

3つだけですが4つの引数：

• thiのタイプあなたは定量化していますか？A;
• 述語P : A -> Prop。
• 証人x : A;そして
• P xの証明、xが有効な証人であることを主張します。

これらのすべてを組み合わせると、証明はexists x : A, P xになります。たとえば、@ex_intro nat (fun n => n = 3) 3 eq_reflは、exists n, n = 3という証明です。この場合、AとP -

したがって、あなたが定義に読み取るex_introの実際の型との違いは、前者が、ヘッダに記載されているすべてのパラメータを含むことがあります。

Answer 2

うん、それらの誘導型定義は、読みにくいことができます。

最初の部分である：

Inductive ex (A:Type) (P:A -> Prop) : Prop := 

これは、型自体に関連付けられているものです。だから、あなたがexを参照してくださいいつでも、それはAとし、Pを持つことになりますし、exはタイプPropのものであろう。すぐにAをスキップして、述語であるPに注目しましょう。したがって、例として「素数である自然数がある」とすると、is_primeとなる可能性があります。nat（自然数）を引数とし、natが素数ならばその証明が存在する可能性があります。

この例では、Aはnatとなります。このチュートリアルでは、Aは言及されていません。なぜなら、Coqは常にそれを推論できるからです。述語が与えられると、Coqは述語の引数の型を調べることによってAの型を得ることができる。

ここまで要約すると、この例では、タイプはex nat is_primeとなります。これはプライムであるナットが存在すると言っていますが、ナットは何も言いません。 ex nat is_primeを構築する際には、どちらが必要なのか、「証人」が必要です。そしてそれは、コンストラクタ定義に私たちをリード：

ex_intro : forall x:A, P x -> ex (A:=A) P. 

コンストラクタはex_introという名前です。ここで難しいのは、コンストラクターにその型のすべてのパラメーターがあることです。したがって、ex_introの後にリストされているものになる前に、AとPのタイプのものを含める必要があります。これらのパラメータの後

はex_intro後にリストされているものを来る：x、述語は証人のために保持している証拠である証人、そしてP x、です。この例を使用すると、xは2になり、P xは(is_prime 2)という証明になります。

コンストラクタは、構築中のタイプexのパラメータを指定する必要があります。それは矢印の後に起こっていることです（->）。これらは、コンストラクタの呼び出しで使用されるパラメータと一致する必要はありませんが、通常は行います。これを達成するために、引数Aはではなく、であり、明示的に渡されます。 (A:=A)では、のパラメータAは、コンストラクタの呼び出しでAと等しいはずです。同様に、Pのexは、コンストラクタの呼び出しからPに設定されています。

したがって(prime 2)タイプのproof_that_2_is_primeがある場合は、ex_intro is_prime 2 proof_that_2_is_primeとすることができ、タイプはex nat is_primeとなります。素数である自然数が存在するという私たちの証明です。直接あなたの質問に答えるために

---

：式forall x:A, P x -> ex (A:=A)では、x:Aは証人であるとP xは、証人が真実であることの証明です。式には述語が含まれていません。これは、コンストラクタex_introに渡す必要がある型のパラメータの一部であるためです。チュートリアルのパラメータリストにはAは含まれていません。これはCoqによって推論されるためです。

私はこのディスカッションが私のチュートリアルでは詳細すぎると思った理由を理解してもらいたいと思います。ご質問ありがとうございます。