From 0d7a7f06d2a0eb6b7396914f0551eb903664c331 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 18 Sep 2017 21:54:52 +0200
Subject: [PATCH] Get rid of type class instance finite_countable.

This instance leads to exponential failing searches.
---
 theories/countable.v | 12 ++++++++++++
 theories/finite.v    |  5 ++++-
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/theories/countable.v b/theories/countable.v
index be1886a6..456ef2d4 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -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;
diff --git a/theories/finite.v b/theories/finite.v
index 0a1dff9c..fef53c3b 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -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.
 
-- 
GitLab