Skip to content
Snippets Groups Projects

add Countable instance for decidable Sigma types

Merged Simon Gregersen requested to merge simongregersen/stdpp:countable_sig into master
All threads resolved!
1 file
+ 9
0
Compare changes
  • Side-by-side
  • Inline
+ 9
0
@@ -340,3 +340,12 @@ Next Obligation.
@@ -340,3 +340,12 @@ Next Obligation.
intros T ?? t.
intros T ?? t.
by rewrite <-(right_id_L [] _ (gen_tree_to_list _)), gen_tree_of_to_list.
by rewrite <-(right_id_L [] _ (gen_tree_to_list _)), gen_tree_of_to_list.
Qed.
Qed.
 
 
(** ** Sigma *)
 
Program Instance countable_sig `{Countable A} (P : A Prop)
 
`{!∀ x, Decision (P x), !∀ x, ProofIrrel (P x)} :
 
Countable { x : A | P x } :=
 
inj_countable proj1_sig (λ x, guard (P x) as Hx; Some (x Hx)) _.
 
Next Obligation.
 
intros A ?? P ?? [x Hx]. by erewrite (option_guard_True_pi (P x)).
 
Qed.
Loading