`{x：nat | '}という形式の（サブ）型を扱う最良の方法です。 x> = 13/\ x <= 19} `？

Question

コックは私がこの定義できます：

Definition teenagers : Set := { x : nat | x >= 13 /\ x <= 19 }. 

とも：

Variable Julia:teenagers. 

ではなく：

Example minus_20 : forall x:teenagers, x<20. 

か：

Example Julia_fact1 : Julia > 12. 

を

ジュリア（ティーンエイジャー）のジュリアは12（ナット）と比較できないためです。

Q：私は彼女について有益な何かを書くことができるようにがどのように私はジュリアのサポートタイプがNATであることをコックを知らせる必要がありますか？

Q '：私のティーンエイジャーの定義は終わりのようです。それは建設的であるよりも宣言的であり、私はナットの帰納的性質を失ったようです。その住民をどのように見せてもらえますか？方法がない場合、私はまだナットに従うことができ、プロップと機能することができます。 （初心者ここでは、1週間未満の自己学習Pierce's SF）。

Answer 1

teenagersで使用しているパターンは、 "subType"パターンのインスタンスです。ご承知のとおり、{ x : nat | P x }はnatとは異なります。現在、Coqはこの種の型を効果的に処理するためのサポートをほとんど提供していませんが、 "well-behaved"クラスのPに制限すると、実際には合理的な方法で作業できます。 [これは本当にCoq FAQ BTWになるはず]

長期的には、このパターンに特別なサポートが必要な場合があります。そのようなサポートの良い例は、math-compライブラリsubTypeインターフェイスによって提供されています。このインタフェースを記述

があなたの元の質問を超えているので、私はいくつかのコメントで終了します：あなたのminus_20例で

• 、あなたのティーンエイジャーのデータ型の第一の突起を使用したいです。試してくださいforall x : teenagers, proj1_sig x < 20。コックはあなたがCoercionとして投影を宣言した場合、自動的に、そのような投影を挿入しようとすることができます

  Require Import Omega. 
  
  Definition teenagers : Set := 
      { x : nat | x >= 13 /\ x <= 19 }. 
  
  Coercion teen_to_nat := fun x : teenagers => proj1_sig x. 
  
  Implicit Type t : teenagers. 
  
  Lemma u t : t < 20. 
  Proof. now destruct t; simpl; omega. Qed. 
  

• あなたは正しく{ x : T | P x }がxよりも、コックに同じではありませんが、観測されてきたように。原則として、種類Tのオブジェクトから{ x : T | P x }のオブジェクトに推論を転送することはできません。また、タイプP xのオブジェクトも追加する必要があります。しかしPの広いクラスに対して、あなたはteen_to_nat投影が単射であることを示すことができる、それは次のようになります。そして、

  forall t1 t2, teen_to_nat t1 = teen_to_nat t2 -> t1 = t2. 
  

  、基本型以上の推論は、サブタイプに転送することができます。私は、彼らはよく概念を説明すると思うように私は、数学-COMPにサブタイプのカップル典型的な例を追加しました：：[編集] Inductive subset of an inductive set in Coq

をも参照してください

• サイズのリストをかn.-tuples。長さnのリストは、math-compで1つのリストにサイズの証明を足したもの、つまりn.-tuple T = { s : seq T | size s == n}と表されます。注入性と補間のおかげで、タプル上のすべての通常のリスト関数を使うことができ、うまく動作します。
• バインドされた自然またはordinal：同様に、タイプ'I_n = { x : nat | x < n }は、自然数とほぼ同じですが、バインドされています。