+
+
+ExtLib.Core.Any
+ +
+Set Implicit Arguments.
+Set Strict Implicit.
+ +
+
+
++Set Strict Implicit.
+ +
+
+This class should be used when no requirements are needed
+
+
+ExtLib.Core.CmpDec
+ +
+Require Import Coq.Bool.Bool.
+Require Import Coq.Classes.RelationClasses.
+Require Import ExtLib.Tactics.Consider.
+ +
+Set Implicit Arguments.
+Set Strict Implicit.
+ +
+Class CmpDec (T : Type) (equ : T -> T -> Prop) (ltu : T -> T -> Prop) : Type :=
+{ cmp_dec : T -> T -> comparison }.
+ +
+Class CmpDec_Correct T (equ ltu : T -> T -> Prop) (ED : CmpDec equ ltu) : Prop :=
+{ cmp_dec_correct : forall x y : T,
+ match cmp_dec x y with
+ | Eq => equ x y
+ | Lt => ltu x y
+ | Gt => ltu y x
+ end }.
+ +
+Inductive cmp_case (P Q R : Prop) : comparison -> Prop :=
+| CaseEq : P -> cmp_case P Q R Eq
+| CaseLt : Q -> cmp_case P Q R Lt
+| CaseGt : R -> cmp_case P Q R Gt.
+ +
+Section pair.
+ Variable T U : Type.
+ Variables eqt ltt : T -> T -> Prop.
+ Variables equ ltu : U -> U -> Prop.
+ +
+ Definition eq_pair (a b : T * U) : Prop :=
+ eqt (fst a) (fst b) /\ equ (snd a) (snd b).
+ +
+ Definition lt_pair (a b : T * U) : Prop :=
+ ltt (fst a) (fst b) \/ (eqt (fst a) (fst b) /\ ltu (snd a) (snd b)).
+ +
+ Variable cdt : CmpDec eqt ltt.
+ Variable cdu : CmpDec equ ltu.
+ +
+ Instance CmpDec_pair : CmpDec eq_pair lt_pair :=
+ { cmp_dec := fun a b =>
+ let '(al,ar) := a in
+ let '(bl,br) := b in
+ match cmp_dec al bl with
+ | Eq => cmp_dec ar br
+ | x => x
+ end }.
+ +
+ Variable cdtC : CmpDec_Correct cdt.
+ Variable cduC : CmpDec_Correct cdu.
+ Variable Symmetric_eqt : Symmetric eqt.
+ +
+ Instance CmpDec_Correct_pair : CmpDec_Correct CmpDec_pair.
+ Proof.
+ constructor. destruct x; destruct y; unfold eq_pair, lt_pair; simpl in *.
+ generalize (cmp_dec_correct t t0); destruct (cmp_dec t t0); simpl; intros; auto.
+ generalize (cmp_dec_correct u u0); destruct (cmp_dec u u0); simpl; intros; auto.
+ Qed.
+End pair.
+ +
+
++Require Import Coq.Classes.RelationClasses.
+Require Import ExtLib.Tactics.Consider.
+ +
+Set Implicit Arguments.
+Set Strict Implicit.
+ +
+Class CmpDec (T : Type) (equ : T -> T -> Prop) (ltu : T -> T -> Prop) : Type :=
+{ cmp_dec : T -> T -> comparison }.
+ +
+Class CmpDec_Correct T (equ ltu : T -> T -> Prop) (ED : CmpDec equ ltu) : Prop :=
+{ cmp_dec_correct : forall x y : T,
+ match cmp_dec x y with
+ | Eq => equ x y
+ | Lt => ltu x y
+ | Gt => ltu y x
+ end }.
+ +
+Inductive cmp_case (P Q R : Prop) : comparison -> Prop :=
+| CaseEq : P -> cmp_case P Q R Eq
+| CaseLt : Q -> cmp_case P Q R Lt
+| CaseGt : R -> cmp_case P Q R Gt.
+ +
+Section pair.
+ Variable T U : Type.
+ Variables eqt ltt : T -> T -> Prop.
+ Variables equ ltu : U -> U -> Prop.
+ +
+ Definition eq_pair (a b : T * U) : Prop :=
+ eqt (fst a) (fst b) /\ equ (snd a) (snd b).
+ +
+ Definition lt_pair (a b : T * U) : Prop :=
+ ltt (fst a) (fst b) \/ (eqt (fst a) (fst b) /\ ltu (snd a) (snd b)).
+ +
+ Variable cdt : CmpDec eqt ltt.
+ Variable cdu : CmpDec equ ltu.
+ +
+ Instance CmpDec_pair : CmpDec eq_pair lt_pair :=
+ { cmp_dec := fun a b =>
+ let '(al,ar) := a in
+ let '(bl,br) := b in
+ match cmp_dec al bl with
+ | Eq => cmp_dec ar br
+ | x => x
+ end }.
+ +
+ Variable cdtC : CmpDec_Correct cdt.
+ Variable cduC : CmpDec_Correct cdu.
+ Variable Symmetric_eqt : Symmetric eqt.
+ +
+ Instance CmpDec_Correct_pair : CmpDec_Correct CmpDec_pair.
+ Proof.
+ constructor. destruct x; destruct y; unfold eq_pair, lt_pair; simpl in *.
+ generalize (cmp_dec_correct t t0); destruct (cmp_dec t t0); simpl; intros; auto.
+ generalize (cmp_dec_correct u u0); destruct (cmp_dec u u0); simpl; intros; auto.
+ Qed.
+End pair.
+ +
+