コック：私はちょうどコックを使用して開始セット

Question

の内容に関する命題。

命題myPropをどのように定義すれば、H、myProp Hというセットがtrueの場合、となるでしょうか？

具体的には、Hのサブセットがnatであることをどのように表現できますか？またはどのように私は単にのlet HがNATのサブセットで述べることができますか？

Answer 1

あなたは型理論であり、そのサブセットの概念は、集合論のように 同じように正確に存在しません。 NATのサブセットがちょうど自然数を超える命題としてそれを記述することによって行われているように何かを記述

。タイプnat -> Propの何か。

文はHがNATのサブセットが書かれていることがしてみましょう：

Variable H : nat -> Prop. 

は今の自然数上の述語は自然数に適用することができます。

あなたは均一性を持っていると自然数の完全なサブセットについて話をしたい場合は、それは（ランダムに名を選択）で表される

Definition all_nat n := True. 

があなたのmyProp述語に注意を向けると、それだけで適用されます自然数の述語については、natのサブセットについての部分を削除することができます。これは、常に満たされます。

Definition myProp (H : nat -> Prop) := forall x, H (2 * x) -> H x. 

私は本当にあなたの最初の提案以下の記述を持つようにしたい場合は、私が

Definition myProp' (H : nat -> Prop) := 
    (forall x, H x -> all_nat x) /\ 
    (forall x, H (2 * x) -> H x). 

を書くでしょう。しかし論理積の最初の部分はall_natの場合は本当に役に立たないです。それは、natの別の意味のあるサブセットのすべてのサブセットを考慮する他の場合には便利です。