在勒柯克，如何構建「SIG」型

Question

的元素，類型爲A的一個簡單的歸納定義：

Inductive A: Set := mkA : nat-> A. 

(*get ID of A*) 
Function getId (a: A) : nat := match a with mkA n => n end. 

和子類型的定義：

(* filter that test ID of *A* is 0 *) 
Function filter (a: A) : bool := if (beq_nat (getId a) 0) then true else false. 

(* cast bool to Prop *) 
Definition IstrueB (b : bool) : Prop := if b then True else False. 

(* subtype of *A* that only interests those who pass the filter *) 
Definition subsetA : Set := {a : A | IstrueB (filter a) }. 

我試試這個代碼鑄元件A到subsetA時filter遍，但未能Coq的便利，這是關於「SIG」類型的元素的有效結構：

Definition cast (a: A) : option subsetA := 
match (filter a) with 
| true => Some (exist _ a (IstrueB (filter a))) 
| false => None 
end. 

錯誤：

In environment 
a : A 
The term "IstrueB (filter a)" has type "Prop" 
while it is expected to have type "?P a" 
(unable to find a well-typed instantiation for "?P": cannot ensure that 
"A -> Type" is a subtype of "?X114@{__:=a} -> Prop"). 

所以，勒柯克預計(IstrueB (filter a))類型的實際證明，但我提供有輸入Prop。

請問您如何提供此類型的燈光？謝謝。

Answer 1

首先，有標準is_true包裝。使用強制機制

Definition subsetA : Set := {a : A | is_true (filter a) }. 

或暗示：你可以明確地使用它像這樣

Coercion is_true : bool >-> Sortclass. 
Definition subsetA : Set := { a : A | filter a }. 

下，非依賴filter a圖案mathching不傳播filter a = true到true分支。你至少有三種選擇：

1. 運用戰術，以建立自己的cast功能：

   Definition cast (a: A) : option subsetA. 
       destruct (filter a) eqn:prf. 
       - exact (Some (exist _ a prf)). 
       - exact None. 
   Defined. 
   

2. 使用依賴於模式匹配明確（搜索「護航模式」＃2或CDPT）：

   Definition cast' (a: A) : option subsetA := 
       match (filter a) as fa return (filter a = fa -> option subsetA) with 
       | true => fun prf => Some (exist _ a prf) 
       | false => fun _ => None 
       end eq_refl. 
   

3. 使用Program設施：

   Require Import Coq.Program.Program. 
   
   Program Definition cast'' (a: A) : option subsetA := 
       match filter a with 
       | true => Some (exist _ a _) 
       | false => None 
       end.