Commit 0d7a7f06 authored by Robbert Krebbers's avatar Robbert Krebbers

Get rid of type class instance finite_countable.

This instance leads to exponential failing searches.
parent e7b13437
......@@ -93,6 +93,18 @@ Section inj_countable.
Next Obligation. intros y; simpl; rewrite decode_encode; eauto. Qed.
End inj_countable.
(** ** Unit *)
Program Instance unit_countable : Countable unit :=
{| encode u := 1; decode p := Some () |}.
Next Obligation. by intros []. Qed.
(** ** Bool *)
Program Instance bool_countable : Countable bool := {|
encode b := if b then 1 else 2;
decode p := Some match p return bool with 1 => true | _ => false end
|}.
Next Obligation. by intros []. Qed.
(** ** Option *)
Program Instance option_countable `{Countable A} : Countable (option A) := {|
encode o := match o with None => 1 | Some x => Pos.succ (encode x) end;
......
......@@ -13,7 +13,8 @@ Arguments enum _ {_ _} : assert.
Arguments NoDup_enum : clear implicits.
Arguments NoDup_enum _ {_ _} : assert.
Definition card A `{Finite A} := length (enum A).
Program Instance finite_countable `{Finite A} : Countable A := {|
Program Definition finite_countable `{Finite A} : Countable A := {|
encode := λ x,
Pos.of_nat $ S $ from_option id 0 $ fst <$> list_find (x =) (enum A);
decode := λ p, enum A !! pred (Pos.to_nat p)
......@@ -25,6 +26,8 @@ Next Obligation.
rewrite Nat2Pos.id by done; simpl; rewrite Hi; simpl.
destruct (list_find_Some (x =) xs i y); naive_solver.
Qed.
Hint Immediate finite_countable : typeclass_instances.
Definition find `{Finite A} P `{ x, Decision (P x)} : option A :=
list_find P (enum A) = decode_nat fst.
......
Markdown is supported
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