Module Ordered


Constructions of ordered types, for use with the FSet functors for finite sets and the FMap functors for finite maps.

Require Import FSets.
Require Import Coqlib.
Require Import Maps.
Require Import Integers.

Create HintDb ordered_type.

The ordered type of positive numbers

Module OrderedPositive <: OrderedType.

Definition t := positive.
Definition eq (x y: t) := x = y.
Definition lt := Plt.

Lemma eq_refl : forall x : t, eq x x.
Proof (@eq_refl t).
Lemma eq_sym : forall x y : t, eq x y -> eq y x.
Proof (@eq_sym t).
Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Proof (@eq_trans t).
Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Proof Plt_trans.
Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Proof Plt_ne.
Lemma compare : forall x y : t, Compare lt eq x y.
Proof.
  intros. destruct (Pos.compare x y) as [] eqn:E.
  apply EQ. red. apply Pos.compare_eq_iff. assumption.
  apply LT. assumption.
  apply GT. apply Pos.compare_gt_iff. assumption.
Defined.

Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq.

End OrderedPositive.

The ordered type of integers

Module OrderedZ <: OrderedType.

Definition t := Z.
Definition eq (x y: t) := x = y.
Definition lt := Z.lt.

Lemma eq_refl : forall x : t, eq x x.
Proof (@eq_refl t).
Lemma eq_sym : forall x y : t, eq x y -> eq y x.
Proof (@eq_sym t).
Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Proof (@eq_trans t).
Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Proof Z.lt_trans.
Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Proof.
unfold lt, eq, t; intros. lia. Qed.
Lemma compare : forall x y : t, Compare lt eq x y.
Proof.
  intros. destruct (Z.compare x y) as [] eqn:E.
  apply EQ. red. apply Z.compare_eq_iff. assumption.
  apply LT. assumption.
  apply GT. apply Z.compare_gt_iff. assumption.
Defined.

Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := zeq.

End OrderedZ.

The ordered type of machine integers

Module OrderedInt <: OrderedType.

Definition t := int.
Definition eq (x y: t) := x = y.
Definition lt (x y: t) := Int.unsigned x < Int.unsigned y.

Lemma eq_refl : forall x : t, eq x x.
Proof (@eq_refl t).
Lemma eq_sym : forall x y : t, eq x y -> eq y x.
Proof (@eq_sym t).
Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Proof (@eq_trans t).
Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Proof.
  unfold lt; intros. lia.
Qed.
Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Proof.
  unfold lt,eq; intros; red; intros. subst. lia.
Qed.
Lemma compare : forall x y : t, Compare lt eq x y.
Proof.
  intros. destruct (zlt (Int.unsigned x) (Int.unsigned y)).
  apply LT. auto.
  destruct (Int.eq_dec x y).
  apply EQ. auto.
  apply GT.
  assert (Int.unsigned x <> Int.unsigned y).
    red; intros. rewrite <- (Int.repr_unsigned x) in n. rewrite <- (Int.repr_unsigned y) in n. congruence.
  red. lia.
Defined.

Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := Int.eq_dec.

End OrderedInt.

Indexed types (those that inject into positive) are ordered.

Module OrderedIndexed(A: INDEXED_TYPE) <: OrderedType.

Definition t := A.t.
Definition eq (x y: t) := x = y.
Definition lt (x y: t) := Plt (A.index x) (A.index y).

Lemma eq_refl : forall x : t, eq x x.
Proof (@eq_refl t).
Lemma eq_sym : forall x y : t, eq x y -> eq y x.
Proof (@eq_sym t).
Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Proof (@eq_trans t).

Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Proof.
  unfold lt; intros. eapply Plt_trans; eauto.
Qed.

Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Proof.
  unfold lt; unfold eq; intros.
  red; intro. subst y. apply Plt_strict with (A.index x). auto.
Qed.

Lemma compare : forall x y : t, Compare lt eq x y.
Proof.
  intros. case (OrderedPositive.compare (A.index x) (A.index y)); intro.
  apply LT. exact l.
  apply EQ. red; red in e. apply A.index_inj; auto.
  apply GT. exact l.
Defined.

Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }.
Proof.
  intros. case (peq (A.index x) (A.index y)); intros.
  left. apply A.index_inj; auto.
  right; red; unfold eq; intros; subst. congruence.
Defined.

End OrderedIndexed.

The option type is ordered.

Module OrderedOption (A: OrderedType) <: OrderedType.

Definition t := option A.t.

Definition eq (x y: t) :=
  option_rel A.eq x y.

Lemma eq_refl : forall x, eq x x.
Proof.
destruct x; constructor. apply A.eq_refl. Qed.

Lemma eq_sym : forall x y, eq x y -> eq y x.
Proof.
  intros * EQ; inv EQ; constructor.
  now apply A.eq_sym.
Qed.

Lemma eq_trans : forall x y z, eq x y -> eq y z -> eq x z.
Proof.
  intros * EQ1 EQ2; inv EQ1; inv EQ2; constructor.
  eapply A.eq_trans; eauto.
Qed.

Definition lt (x y: t) :=
  match x, y with
  | Some x, Some y => A.lt x y
  | None, Some _ => True
  | _, None => False
  end.

Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Proof.
  intros [] [] [] LT1 LT2; simpl in *; eauto using A.lt_trans.
  now inv LT1.
Qed.

Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Proof.
  intros * LT EQ; inv EQ; simpl in *; auto.
  eapply A.lt_not_eq; eauto.
Qed.

Lemma compare : forall x y : t, Compare lt eq x y.
Proof.
  intros [] [].
  - destruct (A.compare t0 t1); [apply LT|apply EQ|apply GT]; auto.
    now constructor.
  - now apply GT.
  - now apply LT.
  - apply EQ. constructor.
Defined.

Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }.
Proof.
  intros [] []; simpl.
  destruct (A.eq_dec t0 t1).
  1,5:left; constructor; auto.
  all:right; intros * CONTRA; inv CONTRA; eauto.
Defined.

End OrderedOption.

The product of two ordered types is ordered.

Module OrderedPair (A B: OrderedType) <: OrderedType.

Definition t := (A.t * B.t)%type.

Definition eq (x y: t) :=
  A.eq (fst x) (fst y) /\ B.eq (snd x) (snd y).

Lemma eq_refl : forall x : t, eq x x.
Proof.
  intros; split; auto with ordered_type.
Qed.

Lemma eq_sym : forall x y : t, eq x y -> eq y x.
Proof.
  unfold eq; intros. intuition auto with ordered_type.
Qed.

Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Proof.
  unfold eq; intros. intuition eauto with ordered_type.
Qed.

Definition lt (x y: t) :=
  A.lt (fst x) (fst y) \/
  (A.eq (fst x) (fst y) /\ B.lt (snd x) (snd y)).

Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Proof.
  unfold lt; intros.
  elim H; elim H0; intros.

  left. apply A.lt_trans with (fst y); auto.

  left. elim H1; intros.
  case (A.compare (fst x) (fst z)); intro.
  assumption.
  generalize (A.lt_not_eq H2); intro. elim H5.
  apply A.eq_trans with (fst z). auto. auto with ordered_type.
  generalize (@A.lt_not_eq (fst z) (fst y)); intro.
  elim H5. apply A.lt_trans with (fst x); auto.
  apply A.eq_sym; auto.

  left. elim H2; intros.
  case (A.compare (fst x) (fst z)); intro.
  assumption.
  generalize (A.lt_not_eq H1); intro. elim H5.
  apply A.eq_trans with (fst x).
  apply A.eq_sym. auto. auto.
  generalize (@A.lt_not_eq (fst y) (fst x)); intro.
  elim H5. apply A.lt_trans with (fst z); auto.
  apply A.eq_sym; auto.

  right. elim H1; elim H2; intros.
  split. apply A.eq_trans with (fst y); auto.
  apply B.lt_trans with (snd y); auto.
Qed.

Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Proof.
  unfold lt, eq, not; intros.
  elim H0; intros.
  elim H; intro.
  apply (@A.lt_not_eq _ _ H3 H1).
  elim H3; intros.
  apply (@B.lt_not_eq _ _ H5 H2).
Qed.

Lemma compare : forall x y : t, Compare lt eq x y.
Proof.
  intros.
  case (A.compare (fst x) (fst y)); intro.
  apply LT. red. left. auto.
  case (B.compare (snd x) (snd y)); intro.
  apply LT. red. right. tauto.
  apply EQ. red. tauto.
  apply GT. red. right. split. apply A.eq_sym. auto. auto.
  apply GT. red. left. auto.
Defined.

Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }.
Proof.
  unfold eq; intros.
  case (A.eq_dec (fst x) (fst y)); intros.
  case (B.eq_dec (snd x) (snd y)); intros.
  left; auto.
  right; intuition.
  right; intuition.
Defined.

End OrderedPair.