In Coq, wie ein Element von 'sig' Typ

Question

Mit einer einfachen induktiven Definition eines Typs A konstruieren Gusselement von A zu subsetA, wenn filter übergibt, aber nicht zur Bequemlichkeit Coq, dass es eine gültige Konstruktion für ein Element von "Sig" Typ ist:

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

Fehler:

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"). 

So erwartet Coq einen tatsächlichen Beweis Typ (IstrueB (filter a)), aber was stelle ich ist es Prop geben.

Könnten Sie etwas Licht auf, wie man solche Art zur Verfügung stellen? Danke.

Answer 1

Vor allem gibt es die Standard is_true Wrapper. Sie können es explizit verwenden wie so:

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

oder implizit den Zwang Mechanismus:

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

Als nächstes Nicht-abhängige Muster-mathching auf filter a nicht filter a = true in den true Zweig ausbreitet. Sie haben mindestens drei Möglichkeiten:

1. Verwenden Taktik Ihre cast Funktion zu bauen:

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

2. abhängig Mustervergleich explizit (Suche nach „Konvoi Muster“ auf Stackoverflow oder in 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. Verwenden Sie die Program Einrichtungen:

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