Library hydras.Prelude.Comparable

From Coq Require Import Relations RelationClasses Setoid.
From hydras Require Export MoreOrders STDPP_compat.

Class Compare (A:Type) := compare : A → A → comparison.

Class Comparable {A:Type} (lt: relation A) (cmp : Compare A) :=
{
  comparable_sto :> StrictOrder lt;
  comparable_comp_spec : ∀ (a b : A), CompSpec eq lt a b (compare a b)
}.

#[export] Hint Mode Compare ! : typeclass_instances.
#[export] Hint Mode Comparable ! - - : typeclass_instances.

Section Comparable.

  Context {A: Type}
          {lt: relation A}
          {cmp: Compare A} `{!Comparable lt cmp}.
  #[local] Notation le := (leq lt).

  #[deprecated(note="use StrictOrder_Transitive")]
   Notation lt_trans := StrictOrder_Transitive (only parsing).

  #[deprecated(note="use StrictOrder_Irreflexive")]
   Notation lt_irrefl := StrictOrder_Irreflexive (only parsing).

  Lemma lt_not_gt (a b: A): lt a b → ¬lt b a.

  Lemma lt_not_ge (a b: A): lt a b → ¬ le b a.

  Lemma compare_lt_iff (a b: A):
    compare a b = Lt ↔ lt a b.

  Lemma compare_lt_trans (a b c: A):
    compare a b = Lt → compare b c = Lt → compare a c = Lt.

  Lemma compare_lt_irrefl (a: A): ¬compare a a = Lt.

  Lemma compare_eq_iff (a b: A): compare a b = Eq ↔ a = b.

  Lemma compare_refl (a: A):
    compare a a = Eq.

  Lemma compare_eq_trans (a b c: A):
    compare a b = Eq → compare b c = Eq → compare a c = Eq.

  Lemma compare_gt_iff (a b: A):
    compare a b = Gt ↔ lt b a.

  Lemma compare_gt_irrefl (a: A):
    ¬compare a a = Gt.

  Lemma compare_gt_trans (a b c: A):
    compare a b = Gt → compare b c = Gt → compare a c = Gt.

  Lemma compare_lt_not_gt (a b: A):
    compare a b = Lt → ¬ compare a b = Gt.

  Lemma compare_gt_not_lt (a b: A):
    compare a b = Gt → ¬ compare a b = Lt.

  Lemma le_refl (a: A): le a a.

  Lemma compare_le_iff_refl (a: A):
    le a a ↔ compare a a = Eq.

  Lemma compare_le_iff (a b: A):
    le a b ↔ compare a b = Lt ∨ compare a b = Eq.

  Lemma compare_ge_iff (a b: A):
    le b a ↔ compare a b = Gt ∨ compare a b = Eq.

  Lemma le_trans (a b c: A):
    le a b → le b c → le a c.

  Lemma le_lt_trans (a b c: A):
    le a b → lt b c → lt a c.

  Lemma lt_le_trans (a b c: A):
    lt a b → le b c → lt a c.

  Lemma lt_incl_le (a b: A):
    lt a b → le a b.

  Lemma le_not_gt (a b: A):
    le a b → ¬ lt b a.

  #[using="All"]
  Definition max (a b : A): A :=
  match compare a b with
  | Gt ⇒ a
  | _ ⇒ b
  end.

  Lemma max_dec (a b: A):
    max a b = a ∨ max a b = b.

  Lemma max_comm (a b: A):
    max a b = max b a.

  Lemma max_ge_a (a b: A):
    le b a ↔ max a b = a.

  Lemma max_ge_b (a b: A):
    le a b ↔ max a b = b.

  Lemma max_refl (a: A): max a a = a.

  Lemma le_max_a (a b: A): le a (max a b).

  Lemma le_max_b (a b: A): le b (max a b).

  #[global] Instance max_assoc : Assoc eq max.

  #[using="All"]
  Definition min (a b :A): A :=
  match compare a b with
  | Lt ⇒ a
  | _ ⇒ b
  end.

  Lemma min_max_iff (a b: A):
    min a b = a ↔ max a b = b.

  Lemma min_comm (a b: A):
    min a b = min b a.

  Lemma min_dec (a b: A):
    min a b = a ∨ min a b = b.

  Lemma min_le_ad (a b: A):
    le a b ↔ min a b = a.

  Lemma min_le_b (a b: A):
    le b a ↔ min a b = b.

  Lemma min_refl (a:A):
    min a a = a.


  Lemma le_min_a (a b: A):
    le (min a b) a.

  Lemma le_min_bd (a b: A):
    le (min a b) b.

  #[global] Instance min_assoc: Assoc eq min.


  Lemma compare_trans (a b c: A) (comp_res: comparison):
    compare a b = comp_res → compare b c = comp_res → compare a c = comp_res.

  Lemma compare_reflect (a b: A):
    match compare a b with
    | Lt ⇒ lt a b
    | Eq ⇒ a = b
    | Gt ⇒ lt b a
    end.

  Lemma lt_eq_lt:
    ∀ alpha beta, lt alpha beta ∨ alpha = beta ∨ lt beta alpha.

  Definition lt_eq_lt_dec
             (alpha beta : A) :
    {lt alpha beta} + {alpha = beta} + {lt beta alpha}.
  Defined.

  Lemma LimitNotSucc
        (alpha: A) :
    Limit alpha → ∀ beta, ¬ Successor alpha beta.

End Comparable.

#[local] Ltac compare_trans H1 H2 intropattern :=
  lazymatch type of (H1, H2) with
  | ((?compare ?a ?b = ?comp_res) × (?compare ?b ?c = ?comp_res))%type ⇒
    assert (compare a c = comp_res) as intropattern by
          (apply compare_trans with b;
           [ exact H1 | exact H2 ])
  | ((?compare ?a ?b = ?comp_res) × (?compare ?b ?c = Eq))%type ⇒
    assert (compare a c = comp_res) as intropattern by
          (assert (b = c) as → by (apply compare_eq_iff; exact H2);
           exact H1)
  | ((?compare ?a ?b = Eq) × (?compare ?b ?c = ?comp_res))%type ⇒
    assert (compare a c = comp_res) as intropattern by
          (assert (a = b) as → by (apply compare_eq_iff; exact H1);
           exact H2)
  | ((?compare _ _ = _) × (?compare _ _ = _))%type ⇒ fail "Not a supported case."
  | _ ⇒ fail "Did not find hypotheses talking about compare: did you declare an instance of Comparable?"
  end.

Tactic Notation "compare" "trans" constr(H1) constr(H2) "as" simple_intropattern(intropattern) :=
  compare_trans H1 H2 intropattern.

Ltac compare_destruct_eqn a b H :=
  destruct (compare a b) eqn: H;
  [ apply compare_eq_iff in H as <-
  | apply compare_lt_iff in H
  | apply compare_gt_iff in H
  ].

Tactic Notation "compare" "destruct" constr(a) constr(b) "as" ident(H) :=
  compare_destruct_eqn a b H.