Library order

Require Import ssreflect ssrbool eqtype ssrfun seq.
Require Import Arith_ext.

This file provides:

a section that proves some facts about total orders
a module type for orders
a section that defines an order for pairs
a section that defines the lexicographic order
functors to instantiate order for pairs and lexicographic order

Section total_order_facts.

Variable A : eqType.
Variable ltA : A -> A -> bool.
Notation "x < y" := (ltA x y).
Variable ltA_trans : forall n m p, m < n -> n m < p.
Variable ltA_irr : forall a, a < a = false.
Variable ltA_total : forall m n, (m != n) = (m < n) || (n < m).

Lemma flip : forall a b, a b < a = false.

Lemma flip' : forall a b, a a = b \/ b < a.

Lemma lt_neq : forall a b, a a == b = false.

Lemma tri' : forall a b, a forall a, a < n' \/ a = n' \/ n' < a /\ a < n \/ a = n \/ n < a.

End total_order_facts.

Module Type ORDER.
Parameter A : eqType.
Parameter ltA : A -> A -> bool.
Notation "x < y" := (ltA x y). Parameter ltA_trans : forall n m p, m < n -> n m < p.
Parameter ltA_total : forall m n, (m != n) = (m < n) || (n < m).
Parameter ltA_irr : forall a, a < a = false.
End ORDER.

Require Import ssrnat.

Module NatOrder <: ORDER.
Definition A := nat_eqType.
Definition ltA : A -> A -> bool := ltn.
Lemma ltA_trans : forall n m p, m < n -> n m < p.
Lemma ltA_total : forall m n, (m != n) = (m < n) || (n < m).
Lemma ltA_irr : forall a, a < a = false.
End NatOrder.

Section order_pair.

Variable A : eqType.
Variable ltA : A -> A -> bool.
Notation "x < y" := (ltA x y) : section_ordered_sequence_of_pairs.
Open Local Scope section_ordered_sequence_of_pairs.
Variable ltA_trans : forall n m p, m < n -> n m < p.
Variable ltA_irr : forall a, a < a = false.
Variable ltA_total : forall m n, (m != n) = (m < n) || (n < m).
Variable B : eqType.
Variable ltB : B -> B -> bool.
Notation "x << y" := (ltB x y) (at level 70) : section_ordered_sequence_of_pairs.
Variable ltB_trans : forall n m p, m << n -> n < m << p.
Variable ltB_irr : forall a, a << a = false.
Variable ltB_total : forall m n, (m != n) = (m << n) || (n << m).

Definition lt_pair : prod_eqType A B -> prod_eqType A B -> bool :=
 fun x => fun y => (x.1 < y.1) || ( (x.1 == y.1) && (x.2 << y.2) ).

Lemma lt_pair_trans : forall (n m p : prod_eqType A B),
 lt_pair m n -> lt_pair n p -> lt_pair m p.

Lemma lt_pair_total : forall (m n : prod_eqType A B),
 (m != n) = lt_pair m n || lt_pair n m.

Lemma lt_pair_irr : forall (m:prod_eqType A B), lt_pair m m = false.

End order_pair.

Module PairOrder (O1 O2:ORDER) : ORDER.
Definition A := prod_eqType O1.A O2.A.
Definition ltA : A -> A -> bool := lt_pair O1.ltA O2.ltA.
Notation "x < y" := (ltA x y).
Lemma ltA_trans : forall n m p, m < n -> n m < p.
Lemma ltA_total : forall m n, (m != n) = (m < n) || (n < m).
Lemma ltA_irr : forall a, a < a = false.
End PairOrder.

Module pair_nat_order := PairOrder NatOrder NatOrder.

given an order ltA (over an eqtype A), define the lexicographic order lex (over the type seq A)

Section lexicographic_order.
Variable A : eqType.
Variable ltA : A -> A -> bool.
Notation "x < y" := (ltA x y).
Variable ltA_trans : forall n m p, m < n -> n m < p.
Variable ltA_irr : forall a, a < a = false.
Variable ltA_total : forall m n, (m != n) = (m < n) || (n < m).

Fixpoint lex (l l':seq A) {struct l} : bool :=
 match l with
 | [::] => match l' with
 | [::] => false
 | _ => true
 end
 | h :: t => match l' with
 | [::] => false
 | h' :: t' =>
 if h < h' then true else
 if h == h' then lex t t' else
 false
 end
 end.

Lemma lex_seq0 : forall (n : seq A), ~ lex n [::].

Lemma lex_app : forall l a b, lex a b -> lex (l ++ a) (l ++ b).

Lemma lex_trans : forall n m p, lex m n -> lex n p -> lex m p.

Lemma lex_total : forall m n, ~~ (m == n) = lex m n || lex n m.

Lemma lex_irr : forall n, lex n n = false.

End lexicographic_order.

Module LexOrder (O:ORDER) : ORDER with Definition A := seq_eqType O.A.
Definition A := seq_eqType O.A.
Definition ltA : A -> A -> bool := lex _ O.ltA.
Notation "x < y" := (ltA x y).
Lemma ltA_trans : forall n m p, m < n -> n m < p.
Lemma ltA_total : forall m n, (m != n) = (m < n) || (n < m).
Lemma ltA_irr : forall a, a < a = false.
End LexOrder.

Module seq_nat_order := LexOrder NatOrder.
Module seq_pair_of_nats_order := LexOrder pair_nat_order.

Require Import ZArith_ext.

Module ZOrder <: ORDER.
Definition A := Z_eqType.
Definition ltA : A -> A -> bool := Zlt_bool.
Lemma ltA_trans : forall n m p, ltA m n -> ltA n p -> ltA m p.
Lemma ltA_total : forall m n, (m != n) = (ltA m n) || (ltA n m).
Lemma ltA_irr : forall a, ltA a a = false.
End ZOrder.

Require Import machine_int.
Import MachineInt.

Module Int32Order <: ORDER.
Definition A := int_32_eqType.
Definition ltA : A -> A -> bool := @lt_n 32%nat.
Lemma ltA_trans : forall n m p, ltA m n -> ltA n p -> ltA m p.
Lemma ltA_total : forall m n, (m != n) = (ltA m n) || (ltA n m).
Lemma ltA_irr : forall a, ltA a a = false.
End Int32Order.

Require Import Ascii.

Definition eq_ascii (a b : ascii) : bool :=
 match ascii_dec a b with left _ => true| right _ => false end.

Lemma eq_asciiP : Equality.axiom eq_ascii.

Canonical Structure ascii_eqMixin := EqMixin eq_asciiP.
Canonical Structure ascii_eqType := Eval hnf in EqType _ ascii_eqMixin.

Definition lt_ascii (a b : ascii) : bool := ltn (nat_of_ascii a) (nat_of_ascii b).

Module AsciiOrder <: ORDER.
Definition A := ascii_eqType.
Definition ltA : A -> A -> bool := lt_ascii.
Lemma ltA_trans : forall n m p, ltA m n -> ltA n p -> ltA m p.
Lemma ltA_total : forall m n, (m != n) = (ltA m n) || (ltA n m).
Lemma ltA_irr : forall a, ltA a a = false.
End AsciiOrder.

Module lex_ascii := LexOrder AsciiOrder.

Require Import String_ext.

Definition lt_string (a b : string) : bool := lex_ascii.ltA (string2asciis a) (string2asciis b).

Module StringOrder : ORDER.
Definition A := string_eqType.
Definition ltA : A -> A -> bool := lt_string.
Lemma ltA_trans : forall n m p, ltA m n -> ltA n p -> ltA m p.
Lemma ltA_total : forall m n, (m != n) = (ltA m n) || (ltA n m).
Lemma ltA_irr : forall a, ltA a a = false.
End StringOrder.