Library basis.ordered_set
Require Import Relations.
Require Import Arith.
Inductive comp : Set :=
| Equivalent : comp
| Less_than : comp
| Greater_than : comp
| Uncomparable : comp.
Module Type S.
Variable A : Set.
Axiom eq_dec : forall e1 e2 : A, {e1 = e2} + {e1 <> e2}.
Parameter o : relation A.
Axiom o_proof : order A o.
Axiom o_dec : forall e1 e2 : A, {o e1 e2} + {~ o e1 e2}.
Axiom o_total : forall e1 e2 : A, {o e1 e2} + {o e2 e1}.
End S.
Module Type ES.
Parameter A : Set.
Parameter eq_A : relation A.
Axiom eq_dec : forall a1 a2 : A, {eq_A a1 a2} + {~eq_A a1 a2}.
Axiom eq_proof : equivalence A eq_A.
Parameter o : relation A.
Axiom o_compat :
forall e1 e1' e2 e2', eq_A e1 e1' -> eq_A e2 e2' -> o e1 e2 -> o e1' e2'.
Axiom o_proof : order A o.
Axiom o_dec : forall e1 e2 : A, {o e1 e2} + {~ o e1 e2}.
Axiom o_total : forall e1 e2 : A, {o e1 e2} + {o e2 e1}.
Add Relation A eq_A
reflexivity proved by (equiv_refl _ _ eq_proof)
symmetry proved by (equiv_sym _ _ eq_proof)
transitivity proved by (equiv_trans _ _ eq_proof) as EQA.
End ES.
Module Nat <: S with Definition A:=nat.
Definition A := nat.
Definition o : relation A := le.
Lemma o_proof : order A o.
Proof.
unfold o; constructor; auto.
unfold reflexive; auto.
unfold transitive; intros n1 n2 n3 H1 H2; apply le_trans with n2; trivial.
unfold antisymmetric; auto with arith.
Qed.
Lemma o_dec : forall e1 e2 : A, {o e1 e2} + {~ o e1 e2}.
Proof.
unfold o.
induction e1; induction e2.
left; trivial.
left; auto with arith.
right; auto with arith.
destruct (IHe1 e2); destruct IHe2; auto with arith.
Defined.
Lemma o_total : forall e1 e2 : A, {o e1 e2} + {o e2 e1}.
Proof.
intros.
unfold o.
change ({e1<=e2}+{e1>=e2}).
apply le_ge_dec.
Qed.
Lemma eq_dec : forall e1 e2 : A, {e1 = e2}+{e1<>e2}.
Proof.
intros; decide equality.
Defined.
End Nat.