Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12

1 files changed, 68 insertions, 1 deletions

diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v
index d7c0400..5020185 100644
--- a/src/classes/SMT_classes_instances.v
+++ b/src/classes/SMT_classes_instances.v
@@ -681,4 +681,71 @@ Section list.
 
 End list.
 
-Hint Resolve unit_compdec bool_compdec Z_compdec Nat_compdec Positive_compdec BV_compdec FArray_compdec int63_compdec option_compdec list_compdec : typeclass_instances.
+
+Section prod.
+
+  Generalizable Variables A B.
+  Context `{HA : CompDec A} `{HB : CompDec B}.
+
+
+  Definition prod_lt (x y:A*B) : Prop :=
+    let (a1, b1) := x in
+    let (a2, b2) := y in
+    (lt a1 a2) \/ ((a1 = a2) /\ (lt b1 b2)).
+
+
+  Definition prod_compare : forall (x y:A*B), Compare prod_lt Logic.eq x y.
+  Proof.
+    intros [a1 b1] [a2 b2].
+    case_eq (compare a1 a2); intros l H.
+    - apply LT. simpl. now left.
+    - case_eq (compare b1 b2); intros l1 H1.
+      + apply LT. simpl. now right.
+      + apply EQ. now subst.
+      + apply GT. simpl. now right.
+    - apply GT. simpl. now left.
+  Defined.
+
+
+  Lemma prod_lt_trans : forall (x y z:A*B),
+      prod_lt x y -> prod_lt y z -> prod_lt x z.
+  Proof.
+    intros [a1 b1] [a2 b2] [a3 b3]; simpl.
+    intros [H1|[H1 H4]] [H2|[H2 H3]].
+    - left. eapply lt_trans; eauto.
+    - subst a3. now left.
+    - subst a2. now left.
+    - subst a2 a3. right. split; auto. eapply lt_trans; eauto.
+  Qed.
+
+
+  Lemma prod_lt_not_eq : forall (x y:A*B), prod_lt x y -> x <> y.
+  Proof.
+    intros [a1 b1] [a2 b2]; simpl.
+    intros [H1|[_ H1]] H3; inversion H3 as [[H4 H5]]; clear H3; subst a2 b2;
+      now apply (lt_not_eq _ _ H1).
+  Qed.
+
+
+  Global Instance prod_ord : OrdType (prod A B) :=
+    Build_OrdType _ _ prod_lt_trans prod_lt_not_eq.
+
+
+  Global Instance prod_comp : Comparable (prod A B) := Build_Comparable _ _ prod_compare.
+
+  Global Instance prod_eqbtype : EqbType (prod A B) := Comparable2EqbType.
+
+
+  Global Instance prod_inh : Inhabited (prod A B) :=
+    Build_Inhabited _ (default_value, default_value).
+
+
+  Global Instance prod_compdec : CompDec (prod A B) := {|
+    Ordered := prod_ord;
+    Comp := prod_comp;
+    Inh := prod_inh
+  |}.
+
+End prod.
+
+Hint Resolve unit_compdec bool_compdec Z_compdec Nat_compdec Positive_compdec BV_compdec FArray_compdec int63_compdec option_compdec list_compdec prod_compdec : typeclass_instances.