在Coq中，如何构造"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元素转换为filter通过时subsetA，但未能方便 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").

因此，Coq期望获得(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上的非依赖模式数学不会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. 显式使用依赖模式匹配(在 Stackoverflow 或 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.