CompDec clean-up (#93)

Clean-up the definition of CompDec, leaving the required minimum (in particular for functional arrays)

2 files changed, 245 insertions, 274 deletions

diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v
index 5f79faf..f8d5b50 100644
--- a/src/classes/SMT_classes.v
+++ b/src/classes/SMT_classes.v
@@ -28,7 +28,7 @@ Definition eqb_to_eq_dec :
   Defined.
 
 
-(** Types with a Boolean equality that reflects in Leibniz equality *)
+(** Types with a Boolean equality that reflects Leibniz equality *)
 Class EqbType T := {
  eqb : T -> T -> bool;
  eqb_spec : forall x y, eqb x y = true <-> x = y
@@ -37,32 +37,65 @@ Class EqbType T := {
 
 (** Types with a decidable equality *)
 Class DecType T := {
- eq_refl : forall x : T, x = x;
- eq_sym : forall x y : T, x = y -> y = x;
- eq_trans : forall x y z : T, x = y -> y = z -> x = z;
  eq_dec : forall x y : T, { x = y } + { x <> y }
 }.
 
 
-Hint Immediate eq_sym.
-Hint Resolve eq_refl eq_trans.
-
 (** Types equipped with Boolean equality are decidable *)
-Instance EqbToDecType T `(EqbType T) : DecType T.
-Proof.
-  destruct H.
-  split; auto.
-  intros; subst; auto.
-  apply (eqb_to_eq_dec _ eqb0); auto.
-Defined.
+Section EqbToDecType.
+  Generalizable Variable T.
+  Context `{ET : EqbType T}.
+
+  Instance EqbToDecType : DecType T.
+  Proof.
+    destruct ET as [eqb0 Heqb0]. split.
+    apply (eqb_to_eq_dec _ eqb0); auto.
+  Defined.
+End EqbToDecType.
+
+
+(** Basic properties on types with Boolean equality *)
+Section EqbTypeProp.
+  Generalizable Variable T.
+  Context `{ET : EqbType T}.
+
+  Lemma eqb_refl x : eqb x x = true.
+  Proof. now rewrite eqb_spec. Qed.
+
+  Lemma eqb_sym x y : eqb x y = true -> eqb y x = true.
+  Proof. rewrite !eqb_spec. now intros ->. Qed.
+
+  Lemma eqb_trans x y z : eqb x y = true -> eqb y z = true -> eqb x z = true.
+  Proof. rewrite !eqb_spec. now intros ->. Qed.
+
+  Lemma eqb_spec_false x y : eqb x y = false <-> x <> y.
+  Proof.
+    split.
+    - intros H1 H2. subst y. rewrite eqb_refl in H1. inversion H1.
+    - intro H. case_eq (eqb x y); auto. intro H1. elim H. now rewrite <- eqb_spec.
+  Qed.
+
+  Lemma reflect_eqb x y : reflect (x = y) (eqb x y).
+  Proof.
+    case_eq (eqb x y); intro H; constructor.
+    - now rewrite eqb_spec in H.
+    - now rewrite eqb_spec_false in H.
+  Qed.
+
+  Lemma eqb_sym2 x y : eqb x y = eqb y x.
+  Proof.
+    case_eq (eqb y x); intro H.
+    - now apply eqb_sym.
+    - rewrite eqb_spec_false in *. auto.
+  Qed.
+End EqbTypeProp.
 
 
 (** Class of types with a partial order *)
 Class OrdType T := {
   lt: T -> T -> Prop;
   lt_trans : forall x y z : T, lt x y -> lt y z -> lt x z;
-  lt_not_eq : forall x y : T, lt x y -> ~ eq x y
-  (* compare : forall x y : T, Compare lt eq x y *)
+  lt_not_eq : forall x y : T, lt x y -> x <> y
 }.
 
 Hint Resolve lt_not_eq lt_trans.
@@ -84,6 +117,29 @@ Class Comparable T {ot:OrdType T} := {
 }.
 
 
+(* A Comparable type is also an EqbType *)
+Section Comparable2EqbType.
+  Generalizable Variable T.
+  Context `{OTT : OrdType T}.
+  Context `{CT : Comparable T}.
+
+  Definition compare2eqb (x y:T) : bool :=
+    match compare x y with
+    | EQ _ => true
+    | _ => false
+    end.
+
+  Lemma compare2eqb_spec x y : compare2eqb x y = true <-> x = y.
+  Proof.
+    unfold compare2eqb.
+    case_eq (compare x y); simpl; intros e He; split; try discriminate;
+      try (intros ->; elim (lt_not_eq _ _ e (eq_refl _))); auto.
+  Qed.
+
+  Instance Comparable2EqbType : EqbType T := Build_EqbType _ _ compare2eqb_spec.
+End Comparable2EqbType.
+
+
 (** Class of inhabited types *)
 Class Inhabited T := {
   default_value : T
@@ -92,53 +148,44 @@ Class Inhabited T := {
 (** * CompDec: Merging all previous classes *)
 
 Class CompDec T := {
-  ty := T;
-  Eqb :> EqbType ty;
-  Decidable := EqbToDecType ty Eqb;
-  Ordered :> OrdType ty;       
-  Comp :> @Comparable ty Ordered;
-  Inh :> Inhabited ty
+  Eqb :> EqbType T;             (* This is redundant since implied by Comp, but it actually allows us to choose a specific equality function *)
+  Ordered :> OrdType T;
+  Comp :> @Comparable T Ordered;
+  Inh :> Inhabited T
 }.
 
 
-Instance ord_of_compdec t `{c: CompDec t} : (OrdType t) := 
-  let (_, _, _, ord, _, _) := c in ord.
+Instance eqbtype_of_compdec t `{c: CompDec t} : (EqbType t) :=
+  let (eqb, _, _, _) := c in eqb.
 
-Instance inh_of_compdec t `{c: CompDec t} : (Inhabited t) := 
-  let (_, _, _, _, _, inh) := c in inh.
+Instance ord_of_compdec t `{c: CompDec t} : (OrdType t) :=
+  let (_, ord, _, _) := c in ord.
+
+Instance inh_of_compdec t `{c: CompDec t} : (Inhabited t) :=
+  let (_, _, _, inh) := c in inh.
 
 Instance comp_of_compdec t `{c: CompDec t} : @Comparable t (ord_of_compdec t).
-destruct c; trivial.
+  destruct c; trivial.
 Defined.
 
-Instance eqbtype_of_compdec t `{c: CompDec t} : EqbType t :=
-  let (_, eqbtype, _, _, _, inh) := c in eqbtype.
-
-Instance dec_of_compdec t `{c: CompDec t} : DecType t :=
-  let (_, _, dec, _, _, inh) := c in dec.
-
-
-Definition type_compdec {ty:Type} (cd : CompDec ty) := ty.
 
 Definition eqb_of_compdec {t} (c : CompDec t) : t -> t -> bool :=
-  match c with
-  | {| ty := ty; Eqb := {| eqb := eqb |} |} => eqb
+  match eqbtype_of_compdec t with
+  | {| eqb := eqb |} => eqb
   end.
 
 
 Lemma compdec_eq_eqb {T:Type} {c : CompDec T} : forall x y : T,
     x = y <-> eqb_of_compdec c x y = true.
 Proof.
-  destruct c. destruct Eqb0.
-  simpl. intros. rewrite eqb_spec0. reflexivity.
+  intros x y. destruct c as [[E HE] O C I]. unfold eqb_of_compdec. simpl. now rewrite HE.
 Qed.
 
 Hint Resolve
      ord_of_compdec
      inh_of_compdec
      comp_of_compdec
-     eqbtype_of_compdec
-     dec_of_compdec : typeclass_instances.
+     eqbtype_of_compdec : typeclass_instances.
 
 
 Record typ_compdec : Type := Typ_compdec {
@@ -146,28 +193,30 @@ Record typ_compdec : Type := Typ_compdec {
   te_compdec : CompDec te_carrier
 }.
 
+
 Section CompDec_from.
 
   Variable T : Type.
+
   Variable eqb' : T -> T -> bool.
+  Variable eqb'_spec : forall x y, eqb' x y = true <-> x = y.
+
   Variable lt' : T -> T -> Prop.
-  Variable d : T.
+  Hypothesis lt'_trans : forall x y z : T, lt' x y -> lt' y z -> lt' x z.
+  Hypothesis lt'_neq : forall x y : T, lt' x y -> x <> y.
 
-  Hypothesis eqb_spec' : forall x y : T, eqb' x y = true <-> x = y.
-  Hypothesis lt_trans': forall x y z : T, lt' x y -> lt' y z -> lt' x z.
-  Hypothesis lt_neq': forall x y : T, lt' x y -> x <> y.
-  
   Variable compare': forall x y : T, Compare lt' eq x y.
-  
+
+  Variable d : T.
+
   Program Instance CompDec_from : (CompDec T) := {|
-    Eqb := {| eqb := eqb' |};
-    Ordered := {| lt := lt'; lt_trans := lt_trans' |};
+    Eqb := {| eqb := eqb'; eqb_spec := eqb'_spec |};
+    Ordered := {| lt := lt'; lt_trans := lt'_trans |};
     Comp := {| compare := compare' |};
     Inh := {| default_value := d |}
   |}.
 
-  
   Definition typ_compdec_from : typ_compdec :=
     Typ_compdec T CompDec_from.
-  
+
 End CompDec_from.
diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v
index 71318df..339d710 100644
--- a/src/classes/SMT_classes_instances.v
+++ b/src/classes/SMT_classes_instances.v
@@ -18,45 +18,37 @@ Require Export SMT_classes.
 
 
 Section Unit.
-
   Let eqb : unit -> unit -> bool := fun _ _ => true.
 
   Let lt : unit -> unit -> Prop := fun _ _ => False.
-  
-  Instance unit_ord : OrdType unit.
+
+  Global Instance unit_ord : OrdType unit.
   Proof. exists lt; unfold lt; trivial.
     intros; contradict H; trivial.
   Defined.
 
-  Instance unit_eqbtype : EqbType unit.
+  Global Instance unit_eqbtype : EqbType unit.
   Proof.
     exists eqb. intros. destruct x, y. unfold eqb. split; trivial.
   Defined.
 
-  Instance unit_comp : @Comparable unit unit_ord.
+  Global Instance unit_comp : @Comparable unit unit_ord.
   Proof.
     split. intros. destruct x, y.
     apply OrderedType.EQ; trivial.
   Defined.
 
-  Instance unit_inh : Inhabited unit := {| default_value := tt |}.
-  
-  Instance unit_compdec : CompDec unit := {|
+  Global Instance unit_inh : Inhabited unit := {| default_value := tt |}.
+
+  Global Instance unit_compdec : CompDec unit := {|
     Eqb := unit_eqbtype;
     Ordered := unit_ord;
     Comp := unit_comp;
     Inh := unit_inh
   |}.
 
-
-  
   Definition unit_typ_compdec := Typ_compdec unit unit_compdec.
 
-
-  Lemma eqb_eq_unit : forall x y, eqb x y <-> x = y.
-  Proof. intros. split; case x; case y; unfold eqb; intros; now auto.
-  Qed.
-  
 End Unit.
 
 
@@ -65,23 +57,17 @@ Section Bool.
   Definition ltb_bool x y := negb x && y.
 
   Definition lt_bool x y := ltb_bool x y = true.
-  
-  Instance bool_ord : OrdType bool.
+
+  Global Instance bool_ord : OrdType bool.
   Proof.
     exists lt_bool.
     intros x y z.
-    case x; case y; case z; intros; simpl; subst; auto. 
+    case x; case y; case z; intros; simpl; subst; auto.
     intros x y.
-    case x; case y; intros; simpl in H; easy. 
+    case x; case y; intros; simpl in H; easy.
   Defined.
 
-  Instance bool_eqbtype : EqbType bool :=
-    {| eqb := Bool.eqb; eqb_spec := eqb_true_iff |}.
-  
-  Instance bool_dec : DecType bool :=
-    EqbToDecType _ bool_eqbtype.
-
-  Instance bool_comp: Comparable bool.
+  Global Instance bool_comp: Comparable bool.
   Proof.
     constructor.
     intros x y.
@@ -99,11 +85,16 @@ Section Bool.
     case x in *; case y in *; auto.
   Defined.
 
-  Instance bool_inh : Inhabited bool := {| default_value := false|}.
+  Global Instance bool_eqbtype : EqbType bool :=
+    {| eqb := Bool.eqb; eqb_spec := eqb_true_iff |}.
+
+  Global Instance bool_dec : DecType bool := EqbToDecType.
+
+  Global Instance bool_inh : Inhabited bool := {| default_value := false|}.
 
-  Instance bool_compdec : CompDec bool := {|
-    Eqb := bool_eqbtype;                                    
-    Ordered := bool_ord;                                    
+  Global Instance bool_compdec : CompDec bool := {|
+    Eqb := bool_eqbtype;
+    Ordered := bool_ord;
     Comp := bool_comp;
     Inh := bool_inh
   |}.
@@ -119,36 +110,32 @@ End Bool.
 
 Section Z.
 
-  Instance Z_ord : OrdType Z.
+  Global Instance Z_ord : OrdType Z.
   Proof.
     exists Z_as_OT.lt.
     exact Z_as_OT.lt_trans.
     exact Z_as_OT.lt_not_eq.
   Defined.
 
-  Instance Z_eqbtype : EqbType Z :=
-    {| eqb := Z.eqb; eqb_spec := Z.eqb_eq |}.
-
-  (* Instance Z_eqbtype : EqbType Z := *)
-  (*   {| eqb := Zeq_bool; eqb_spec := fun x y => symmetry (Zeq_is_eq_bool x y) |}. *)
-  
-  Instance Z_dec : DecType Z :=
-    EqbToDecType _ Z_eqbtype.
 
-  
-  Instance Z_comp: Comparable Z.
+  Global Instance Z_comp: Comparable Z.
   Proof.
     constructor.
     apply Z_as_OT.compare.
   Defined.
 
+  Global Instance Z_eqbtype : EqbType Z :=
+    {| eqb := Z.eqb; eqb_spec := Z.eqb_eq |}.
+
+  Global Instance Z_dec : DecType Z := @EqbToDecType _ Z_eqbtype.
+
+
+  Global Instance Z_inh : Inhabited Z := {| default_value := 0%Z |}.
 
-  Instance Z_inh : Inhabited Z := {| default_value := 0%Z |}.
 
-    
-  Instance Z_compdec : CompDec Z := {|
-    Eqb := Z_eqbtype;                                    
-    Ordered := Z_ord;                                    
+  Global Instance Z_compdec : CompDec Z := {|
+    Eqb := Z_eqbtype;
+    Ordered := Z_ord;
     Comp := Z_comp;
     Inh := Z_inh
   |}.
@@ -202,7 +189,7 @@ Section Z.
 
   Lemma lt_Z_B2P': forall x y, ltP_Z x y <-> Z.lt x y.
   Proof. intros x y; split; intro H.
-         unfold ltP_Z in H. 
+         unfold ltP_Z in H.
          case_eq ((x <? y)%Z ); intros; rewrite H0 in H; try easy.
          now apply Z.ltb_lt in H0.
          apply lt_Z_B2P.
@@ -211,7 +198,7 @@ Section Z.
 
   Lemma le_Z_B2P': forall x y, leP_Z x y <-> Z.le x y.
   Proof. intros x y; split; intro H.
-         unfold leP_Z in H. 
+         unfold leP_Z in H.
          case_eq ((x <=? y)%Z ); intros; rewrite H0 in H; try easy.
          now apply Z.leb_le in H0.
          apply le_Z_B2P.
@@ -220,7 +207,7 @@ Section Z.
 
   Lemma gt_Z_B2P': forall x y, gtP_Z x y <-> Z.gt x y.
   Proof. intros x y; split; intro H.
-         unfold gtP_Z in H. 
+         unfold gtP_Z in H.
          case_eq ((x >? y)%Z ); intros; rewrite H0 in H; try easy.
          now apply Zgt_is_gt_bool in H0.
          apply gt_Z_B2P.
@@ -229,7 +216,7 @@ Section Z.
 
   Lemma ge_Z_B2P': forall x y, geP_Z x y <-> Z.ge x y.
   Proof. intros x y; split; intro H.
-         unfold geP_Z in H. 
+         unfold geP_Z in H.
          case_eq ((x >=? y)%Z ); intros; rewrite H0 in H; try easy.
          rewrite Z.geb_leb in H0. rewrite le_Z_B2P in H0.
          apply le_Z_B2P' in H0. now apply Z.ge_le_iff.
@@ -250,34 +237,33 @@ End Z.
 
 Section Nat.
 
-  Instance Nat_ord : OrdType nat.
+  Global Instance Nat_ord : OrdType nat.
   Proof.
-    
+
     exists Nat_as_OT.lt.
     exact Nat_as_OT.lt_trans.
     exact Nat_as_OT.lt_not_eq.
   Defined.
 
-  Instance Nat_eqbtype : EqbType nat :=
-    {| eqb := Structures.nat_eqb; eqb_spec := Structures.nat_eqb_eq |}.
-  
-  Instance Nat_dec : DecType nat :=
-    EqbToDecType _ Nat_eqbtype.
 
-  
-  Instance Nat_comp: Comparable nat.
+  Global Instance Nat_comp: Comparable nat.
   Proof.
     constructor.
     apply Nat_as_OT.compare.
   Defined.
 
+  Global Instance Nat_eqbtype : EqbType nat :=
+    {| eqb := Structures.nat_eqb; eqb_spec := Structures.nat_eqb_eq |}.
+
+  Global Instance Nat_dec : DecType nat := EqbToDecType.
+
 
-  Instance Nat_inh : Inhabited nat := {| default_value := O%nat |}.
+  Global Instance Nat_inh : Inhabited nat := {| default_value := O%nat |}.
 
-    
-  Instance Nat_compdec : CompDec nat := {|
-    Eqb := Nat_eqbtype;                                    
-    Ordered := Nat_ord;                                    
+
+  Global Instance Nat_compdec : CompDec nat := {|
+    Eqb := Nat_eqbtype;
+    Ordered := Nat_ord;
     Comp := Nat_comp;
     Inh := Nat_inh
   |}.
@@ -287,30 +273,29 @@ End Nat.
 
 Section Positive.
 
-  Instance Positive_ord : OrdType positive.
+  Global Instance Positive_ord : OrdType positive.
   Proof.
     exists Positive_as_OT.lt.
     exact Positive_as_OT.lt_trans.
     exact Positive_as_OT.lt_not_eq.
   Defined.
 
-  Instance Positive_eqbtype : EqbType positive :=
-    {| eqb := Pos.eqb; eqb_spec := Pos.eqb_eq |}.
-  
-  Instance Positive_dec : DecType positive :=
-    EqbToDecType _ Positive_eqbtype.
-
-  Instance Positive_comp: Comparable positive.
+  Global Instance Positive_comp: Comparable positive.
   Proof.
     constructor.
     apply Positive_as_OT.compare.
   Defined.
 
-  Instance Positive_inh : Inhabited positive := {| default_value := 1%positive |}.
+  Global Instance Positive_eqbtype : EqbType positive :=
+    {| eqb := Pos.eqb; eqb_spec := Pos.eqb_eq |}.
+
+  Global Instance Positive_dec : DecType positive := EqbToDecType.
 
-  Instance Positive_compdec : CompDec positive := {|
-    Eqb := Positive_eqbtype;                                    
-    Ordered := Positive_ord;                                    
+  Global Instance Positive_inh : Inhabited positive := {| default_value := 1%positive |}.
+
+  Global Instance Positive_compdec : CompDec positive := {|
+    Eqb := Positive_eqbtype;
+    Ordered := Positive_ord;
     Comp := Positive_comp;
     Inh := Positive_inh
   |}.
@@ -323,8 +308,8 @@ Section BV.
 
   Import BITVECTOR_LIST.
 
-  
-  Instance BV_ord n : OrdType (bitvector n).
+
+  Global Instance BV_ord n : OrdType (bitvector n).
   Proof.
     exists (fun a b => (bv_ult a b)).
     unfold bv_ult, RAWBITVECTOR_LIST.bv_ult.
@@ -342,15 +327,8 @@ Section BV.
     apply H. easy.
   Defined.
 
-  Instance BV_eqbtype n : EqbType (bitvector n) :=
-    {| eqb := @bv_eq n;
-       eqb_spec := @bv_eq_reflect n |}.
 
-  Instance BV_dec n : DecType (bitvector n) :=
-    EqbToDecType _ (BV_eqbtype n).
-
-  
-  Instance BV_comp n: Comparable (bitvector n).
+  Global Instance BV_comp n: Comparable (bitvector n).
   Proof.
     constructor.
     intros x y.
@@ -388,13 +366,19 @@ Section BV.
     now apply RAWBITVECTOR_LIST.rev_neq in H.
   Defined.
 
-  Instance BV_inh n : Inhabited (bitvector n) :=
+  Global Instance BV_eqbtype n : EqbType (bitvector n) :=
+    {| eqb := @bv_eq n;
+       eqb_spec := @bv_eq_reflect n |}.
+
+  Global Instance BV_dec n : DecType (bitvector n) := EqbToDecType.
+
+  Global Instance BV_inh n : Inhabited (bitvector n) :=
     {| default_value := zeros n |}.
 
 
-  Instance BV_compdec n: CompDec (bitvector n) := {|
-    Eqb := BV_eqbtype n;                                    
-    Ordered := BV_ord n;                                    
+  Global Instance BV_compdec n: CompDec (bitvector n) := {|
+    Eqb := BV_eqbtype n;
+    Ordered := BV_ord n;
     Comp := BV_comp n;
     Inh := BV_inh n
   |}.
@@ -405,10 +389,9 @@ End BV.
 
 Section FArray.
 
-  Instance FArray_ord key elt
+  Global Instance FArray_ord key elt
            `{key_ord: OrdType key}
            `{elt_ord: OrdType elt}
-           `{elt_dec: DecType elt}
            `{elt_inh: Inhabited elt}
            `{key_comp: @Comparable key key_ord} : OrdType (farray key elt).
   Proof.
@@ -419,10 +402,30 @@ Section FArray.
     apply lt_farray_not_eq in H.
     apply H.
     rewrite H0.
-    apply eqfarray_refl. auto.
+    apply eqfarray_refl.
   Defined.
 
-  Instance FArray_eqbtype key elt
+
+  Global Instance FArray_comp key elt
+           `{key_ord: OrdType key}
+           `{elt_ord: OrdType elt}
+           `{key_comp: @Comparable key key_ord}
+           `{elt_inh: Inhabited elt}
+           `{elt_comp: @Comparable elt elt_ord} : Comparable (farray key elt).
+  Proof.
+    constructor.
+    intros.
+    destruct (compare_farray key_comp elt_comp x y).
+    - apply OrderedType.LT. auto.
+    - apply OrderedType.EQ.
+      specialize (@eq_equal key elt key_ord key_comp elt_ord elt_comp elt_inh x y).
+      intros.
+      apply H in e.
+      now apply equal_eq in e.
+    - apply OrderedType.GT. auto.
+  Defined.
+
+  Global Instance FArray_eqbtype key elt
            `{key_ord: OrdType key}
            `{elt_ord: OrdType elt}
            `{elt_eqbtype: EqbType elt}
@@ -436,88 +439,48 @@ Section FArray.
     split.
     apply FArray.equal_eq.
     intros. subst. apply eq_equal. apply eqfarray_refl.
-    apply EqbToDecType. auto.
   Defined.
 
-  
-  Instance FArray_dec key elt
+  Global Instance FArray_dec key elt
            `{key_ord: OrdType key}
            `{elt_ord: OrdType elt}
            `{elt_eqbtype: EqbType elt}
            `{key_comp: @Comparable key key_ord}
            `{elt_comp: @Comparable elt elt_ord}
            `{elt_inh: Inhabited elt}
-    : DecType (farray key elt) :=
-    EqbToDecType _ (FArray_eqbtype key elt).
+    : DecType (farray key elt) := EqbToDecType.
 
-  
-  Instance FArray_comp key elt
-           `{key_ord: OrdType key}
-           `{elt_ord: OrdType elt}
-           `{elt_eqbtype: EqbType elt}
-           `{key_comp: @Comparable key key_ord}
-           `{elt_inh: Inhabited elt}
-           `{elt_comp: @Comparable elt elt_ord} : Comparable (farray key elt).
-  Proof.
-    constructor.
-    intros.
-    destruct (compare_farray key_comp (EqbToDecType _ elt_eqbtype) elt_comp x y).
-    - apply OrderedType.LT. auto.
-    - apply OrderedType.EQ.
-      specialize (@eq_equal key elt key_ord key_comp elt_ord elt_comp elt_inh x y).
-      intros.
-      apply H in e.
-      now apply equal_eq in e.
-    - apply OrderedType.GT. auto.
-  Defined.
-
-  Instance FArray_inh key elt
+  Global Instance FArray_inh key elt
            `{key_ord: OrdType key}
            `{elt_inh: Inhabited elt} : Inhabited (farray key elt) :=
     {| default_value := FArray.empty key_ord elt_inh |}.
 
 
-  Program Instance FArray_compdec key elt
+  Global Instance FArray_compdec key elt
           `{key_compdec: CompDec key}
           `{elt_compdec: CompDec elt} :
     CompDec (farray key elt) :=
     {|
       Eqb := FArray_eqbtype key elt;
       Ordered := FArray_ord key elt;
-      (*  Comp := FArray_comp key elt ; *)
+      Comp := FArray_comp key elt ;
       Inh := FArray_inh key elt
     |}.
-  
-  Next Obligation.
-    constructor.
-    destruct key_compdec, elt_compdec.
-    simpl in *.
-    unfold lt_farray.
-    intros. simpl.
-    unfold EqbToDecType. simpl.
-    case_eq (compare x y); intros.
-    apply OrderedType.LT.
-    destruct (compare x y); try discriminate H; auto.
-    apply OrderedType.EQ.
-    destruct (compare x y); try discriminate H; auto.
-    apply OrderedType.GT.
-    destruct (compare y x); try discriminate H; auto; clear H.
-  Defined.
 
 End FArray.
 
 
 Section Int63.
-  
+
   Local Open Scope int63_scope.
 
   Let int_lt x y :=
     if Int63Native.ltb x y then True else False.
-  
-  Instance int63_ord : OrdType int.
+
+  Global Instance int63_ord : OrdType int.
   Proof.
     exists int_lt; unfold int_lt.
-    - intros x y z. 
+    - intros x y z.
       case_eq (x < y); intro;
         case_eq (y < z); intro;
           case_eq (x < z); intro;
@@ -533,15 +496,9 @@ Section Int63.
       rewrite <- Int63Properties.to_Z_eq.
       exact (Z.lt_neq _ _ H).
   Defined.
-  
-  Instance int63_eqbtype : EqbType int :=
-    {| eqb := Int63Native.eqb; eqb_spec := Int63Properties.eqb_spec |}.
 
-  Instance int63_dec : DecType int :=
-    EqbToDecType _ int63_eqbtype.
 
-
-  Instance int63_comp: Comparable int.
+  Global Instance int63_comp: Comparable int.
   Proof.
     constructor.
     intros x y.
@@ -566,16 +523,20 @@ Section Int63.
       rewrite H0. auto.
   Defined.
 
+  Global Instance int63_eqbtype : EqbType int :=
+    {| eqb := Int63Native.eqb; eqb_spec := Int63Properties.eqb_spec |}.
+
+  Global Instance int63_dec : DecType int := EqbToDecType.
+
 
-  Instance int63_inh : Inhabited int := {| default_value := 0 |}.
-    
-  Instance int63_compdec : CompDec int := {|
-    Eqb := int63_eqbtype;                                    
-    Ordered := int63_ord;                                    
+  Global Instance int63_inh : Inhabited int := {| default_value := 0 |}.
+
+  Global Instance int63_compdec : CompDec int := {|
+    Eqb := int63_eqbtype;
+    Ordered := int63_ord;
     Comp := int63_comp;
     Inh := int63_inh
   |}.
-         
 
 End Int63.
 
@@ -586,25 +547,6 @@ Section option.
   Context `{HA : CompDec A}.
 
 
-  Definition option_eqb (x y : option A) : bool :=
-    match x, y with
-    | Some a, Some b => eqb a b
-    | None, None => true
-    | _, _ => false
-    end.
-
-
-  Lemma option_eqb_spec : forall (x y : option A), option_eqb x y = true <-> x = y.
-  Proof.
-    intros [a| ] [b| ]; simpl; split; try discriminate; auto.
-    - intro H. rewrite eqb_spec in H. now subst b.
-    - intros H. inversion H as [H1]. now rewrite eqb_spec.
-  Qed.
-
-
-  Instance option_eqbtype : EqbType (option A) := Build_EqbType _ _ option_eqb_spec.
-
-
   Definition option_lt (x y : option A) : Prop :=
     match x, y with
     | Some a, Some b => lt a b
@@ -631,7 +573,7 @@ Section option.
   Qed.
 
 
-  Instance option_ord : OrdType (option A) :=
+  Global Instance option_ord : OrdType (option A) :=
     Build_OrdType _ _ option_lt_trans option_lt_not_eq.
 
 
@@ -647,15 +589,15 @@ Section option.
     - now apply EQ.
   Defined.
 
+  Global Instance option_comp : Comparable (option A) := Build_Comparable _ _ option_compare.
 
-  Instance option_comp : Comparable (option A) := Build_Comparable _ _ option_compare.
+  Global Instance option_eqbtype : EqbType (option A) := Comparable2EqbType.
 
 
-  Instance option_inh : Inhabited (option A) := Build_Inhabited _ None.
+  Global Instance option_inh : Inhabited (option A) := Build_Inhabited _ None.
 
 
-  Instance option_compdec : CompDec (option A) := {|
-    Eqb := option_eqbtype;
+  Global Instance option_compdec : CompDec (option A) := {|
     Ordered := option_ord;
     Comp := option_comp;
     Inh := option_inh
@@ -670,27 +612,6 @@ Section list.
   Context `{HA : CompDec A}.
 
 
-  Fixpoint list_eqb (xs ys : list A) : bool :=
-    match xs, ys with
-    | nil, nil => true
-    | x::xs, y::ys => eqb x y && list_eqb xs ys
-    | _, _ => false
-    end.
-
-
-  Lemma list_eqb_spec : forall (x y : list A), list_eqb x y = true <-> x = y.
-  Proof.
-    induction x as [ |x xs IHxs]; intros [ |y ys]; simpl; split; try discriminate; auto.
-    - rewrite andb_true_iff. intros [H1 H2]. rewrite eqb_spec in H1. rewrite IHxs in H2. now subst.
-    - intros H. inversion H as [H1]. rewrite andb_true_iff; split.
-      + now rewrite eqb_spec.
-      + subst ys. now rewrite IHxs.
-  Qed.
-
-
-  Instance list_eqbtype : EqbType (list A) := Build_EqbType _ _ list_eqb_spec.
-
-
   Fixpoint list_lt (xs ys : list A) : Prop :=
     match xs, ys with
     | nil, nil => False
@@ -700,6 +621,22 @@ Section list.
     end.
 
 
+  Definition list_compare : forall (x y : list A), Compare list_lt Logic.eq x y.
+  Proof.
+    induction x as [ |x xs IHxs]; intros [ |y ys]; simpl.
+    - now apply EQ.
+    - now apply LT.
+    - now apply GT.
+    - case_eq (compare x y); intros l H.
+      + apply LT. simpl. now left.
+      + case_eq (IHxs ys); intros l1 H1.
+        * apply LT. simpl. right. split; auto. now apply eqb_spec.
+        * apply EQ. now rewrite l, l1.
+        * apply GT. simpl. right. split; auto. now apply eqb_spec.
+      + apply GT. simpl. now left.
+  Defined.
+
+
   Lemma list_lt_trans : forall (x y z : list A),
       list_lt x y -> list_lt y z -> list_lt x z.
   Proof.
@@ -720,39 +657,24 @@ Section list.
     induction x as [ |x xs IHxs]; intros [ |y ys]; simpl; auto.
     - discriminate.
     - intros [H1|[H1 H2]]; intros H; inversion H; subst.
-      + eapply lt_not_eq; eauto.
-      + eapply IHxs; eauto.
+      + now apply (lt_not_eq _ _ H1).
+      + now apply (IHxs _ H2).
   Qed.
 
 
-  Instance list_ord : OrdType (list A) :=
+  Global Instance list_ord : OrdType (list A) :=
     Build_OrdType _ _ list_lt_trans list_lt_not_eq.
 
 
-  Definition list_compare : forall (x y : list A), Compare list_lt Logic.eq x y.
-  Proof.
-    induction x as [ |x xs IHxs]; intros [ |y ys]; simpl.
-    - now apply EQ.
-    - now apply LT.
-    - now apply GT.
-    - case_eq (compare x y); intros l H.
-      + apply LT. simpl. now left.
-      + case_eq (IHxs ys); intros l1 H1.
-        * apply LT. simpl. right. split; auto. now apply eqb_spec.
-        * apply EQ. now rewrite l, l1.
-        * apply GT. simpl. right. split; auto. now apply eqb_spec.
-      + apply GT. simpl. now left.
-  Defined.
-
+  Global Instance list_comp : Comparable (list A) := Build_Comparable _ _ list_compare.
 
-  Instance list_comp : Comparable (list A) := Build_Comparable _ _ list_compare.
+  Global Instance list_eqbtype : EqbType (list A) := Comparable2EqbType.
 
 
-  Instance list_inh : Inhabited (list A) := Build_Inhabited _ nil.
+  Global Instance list_inh : Inhabited (list A) := Build_Inhabited _ nil.
 
 
-  Instance list_compdec : CompDec (list A) := {|
-    Eqb := list_eqbtype;
+  Global Instance list_compdec : CompDec (list A) := {|
     Ordered := list_ord;
     Comp := list_comp;
     Inh := list_inh