在勒柯克，如何构建“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.