Commit 057543ba authored by Simon Gregersen's avatar Simon Gregersen
Browse files

add Countable instance for decidable Sigma types

parent f7c9c556
...@@ -340,3 +340,21 @@ Next Obligation. ...@@ -340,3 +340,21 @@ 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.
(** ** Decidable Sigma *)
Section sigma.
Context `{Countable A} (P : A Prop).
Context `{ x, Decision (P x)} `{ x, ProofIrrel (P x)}.
Program Instance countable_sig : Countable { x : A | P x } :=
{| encode := λ x, encode (`x);
decode := λ p, x decode p;
match decide (P x) return option { x | P x } with
| left H => Some (x H)
| right _ => None
end |}.
Next Obligation.
intros []. rewrite decode_encode; simpl. by erewrite decide_left.
Qed.
End sigma.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment