# Library CoLoR.Util.Pair.PairLex

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
Lexicographic order on a product and some results concerning it are introduced in this file.

Set Implicit Arguments.

Section LexPair.

Variables (L : Type) (R : Type)
(eqL : relation L) (eqL_Equivalence : Equivalence eqL).

Hint Resolve (Seq_refl L eqL eqL_Equivalence) : sets.
Hint Resolve (Seq_trans L eqL eqL_Equivalence) : sets.
Hint Resolve (Seq_sym L eqL eqL_Equivalence) : sets.

Variables (eqR : relation R) (eqR_Equivalence : Equivalence eqR).

Hint Resolve (Seq_refl R eqR eqR_Equivalence) : sets.
Hint Resolve (Seq_trans R eqR eqR_Equivalence) : sets.
Hint Resolve (Seq_sym R eqR eqR_Equivalence) : sets.

Variable gtL : relation L.

Definition ltL := transp gtL.

Variable gtL_eqL_compat : Proper (eqL ==> eqL ==> impl) gtL.

Definition AccL := Acc ltL.

Instance gtL_morph : Proper (eqL ==> eqL ==> iff) gtL.

Variable gtR : relation R.

Definition ltR := transp gtR.

Variable gtR_eqR_compat: Proper (eqR ==> eqR ==> impl) gtR.

Definition AccR := Acc ltR.

Instance gtR_morph : Proper (eqR ==> eqR ==> iff) gtR.

Definition pair := (L * R)%type.

Definition eqPair (x y : pair) := eqL (fst x) (fst y) /\ eqR (snd x) (snd y).

Reserved Notation "a >lex b" (at level 40).

Inductive LexProd_Gt : relation pair :=
| GtL: forall a a' b b', gtL a a' -> (a, b) >lex (a', b')
| GtR: forall a a' b b', eqL a a' -> gtR b b' -> (a, b) >lex (a', b')
where "a >lex b" := (LexProd_Gt a b).

Definition LexProd_Lt := transp LexProd_Gt.

Notation "a <lex b" := (LexProd_Lt a b) (at level 40).

Definition Acc_LexProd := Acc LexProd_Lt.

Hint Unfold eqPair : sets.

Instance eqPair_Equivalence : Equivalence eqPair.

Instance LexProd_Gt_morph_equiv :
Proper (eqPair ==> eqPair ==> iff) LexProd_Gt.

Lemma LexProd_Gt_morph : forall x1 x2 : pair, eqPair x1 x2 ->
forall x3 x4 : pair, eqPair x3 x4 -> x1 >lex x3 -> x2 >lex x4.

Instance LexProd_Lt_morph : Proper (eqPair ==> eqPair ==> iff) LexProd_Lt.

Instance Acc_LexProd_morph : Proper (eqPair ==> iff) Acc_LexProd.

Proof of the fact that lexicographic order is a strict order.

Section LexProd_StrictOrder.

Variable gtL_so: strict_order gtL.

Hint Resolve (sord_trans gtL_so) : sets.
Hint Resolve (sord_irrefl gtL_so) : sets.
Hint Resolve (so_not_symmetric gtL_so) : sets.
Hint Resolve (so_strict gtL_so gtL_eqL_compat eqL_Equivalence) : sets.

Variable gtR_so: strict_order gtR.

Hint Resolve (sord_trans gtR_so) : sets.
Hint Resolve (sord_irrefl gtR_so) : sets.
Hint Resolve (so_not_symmetric gtR_so) : sets.
Hint Resolve (so_strict gtR_so gtR_eqR_compat eqR_Equivalence) : sets.

Lemma lexprod_irreflex : forall a, a >lex a -> False.

Lemma lexprod_trans : forall a b c, a >lex b -> b >lex c -> a >lex c.

Lemma lexprod_so : strict_order LexProd_Gt.

End LexProd_StrictOrder.

Proof of the fact that lexicographic order is well-founded (if so are the underlying orders)

Section LexProd_WellFounded.

Variables (wf_ltL : well_founded ltL) (wf_ltR : well_founded ltR).

Lemma lexprod_wf : well_founded LexProd_Lt.

End LexProd_WellFounded.

End LexPair.

Module LexicographicOrder (Import A_ord B_ord : Ord).

Module Import A_ext := OrdLemmas A_ord.
Module Import B_ext := OrdLemmas B_ord.

Notation L := A_ord.S.A.
Notation R := B_ord.S.A.
Notation eqL := A_ord.S.eqA.
Notation eqR := B_ord.S.eqA.
Notation gtL := A_ord.gtA.
Notation gtR := B_ord.gtA.
Notation ltL := A_ext.ltA.
Notation ltR := B_ext.ltA.

Definition pair := pair L R.

Definition eqPair (x y : pair) := eqPair eqL eqR x y.

Section Eq_dec.

Variables (eqA_dec : forall x y : L, {eqL x y} + {~eqL x y})
(eqB_dec : forall x y : R, {eqR x y} + {~eqR x y}).

Lemma eqPair_dec : forall x y : pair, {eqPair x y} + {~eqPair x y}.

End Eq_dec.

Definition LexProd_Gt x y := LexProd_Gt eqL gtL gtR x y.

Notation "a >lex b" := (LexProd_Gt a b) (at level 40).

Definition LexProd_Lt := transp LexProd_Gt.

Notation "a <lex b" := (LexProd_Lt a b) (at level 40).

Definition Acc_LexProd := Acc LexProd_Lt.

Hint Unfold eqPair : sets.

Instance eqPair_Equivalence : Equivalence eqPair :=
eqPair_Equivalence A_ord.S.eqA_Equivalence B_ord.S.eqA_Equivalence.

Hint Resolve A_ord.S.eqA_Equivalence B_ord.S.eqA_Equivalence : sets.

Instance LexProd_Gt_morph : Proper (eqPair ==> eqPair ==> iff) LexProd_Gt.

Instance LexProd_Lt_morph : Proper (eqPair ==> eqPair ==> iff) LexProd_Lt.

Instance Acc_LexProd_morph : Proper (eqPair ==> iff) Acc_LexProd.

Proof of the fact that lexicographic order is a strict order.

Module LexProd_StrictOrder
(pA: Poset with Definition A := A_ord.S.A with Module O := A_ord)
(pB: Poset with Definition A := B_ord.S.A with Module O := B_ord).

Hint Resolve pA.gtA_so pB.gtA_so : sets.

Lemma lexprod_irreflex : forall a, a >lex a -> False.

Lemma lexprod_trans : forall a b c, a >lex b -> b >lex c -> a >lex c.

Lemma lexprod_so : strict_order LexProd_Gt.

End LexProd_StrictOrder.

Proof of the fact that lexicographic order is well-founded (if so are the underlaying orders)

Section LexProd_WellFounded.

Variables (wf_ltL : well_founded ltL) (wf_ltR : well_founded ltR).

Lemma lexprod_wf : well_founded LexProd_Lt.

End LexProd_WellFounded.

Module Rel <: Ord.

Module S <: Eqset.
Definition A := pair.
Definition eqA := eqPair.
Definition eqA_dec := eqPair_dec.
Definition eqA_Equivalence := eqPair_Equivalence.
End S.

Definition A := pair.

Definition gtA := LexProd_Gt.

Instance gtA_eqA_compat : Proper (S.eqA ==> S.eqA ==> impl) gtA.

End Rel.

End LexicographicOrder.

Module LexicographicOrderTriple (A_ord B_ord C_ord : Ord).

Import Notations Relation_Operators.

Module Import A_ext := OrdLemmas A_ord.
Module Import B_ext := OrdLemmas B_ord.
Module Import C_ext := OrdLemmas C_ord.

Notation L := A_ord.S.A.
Notation M := B_ord.S.A.
Notation R := C_ord.S.A.
Notation eqL := A_ord.S.eqA.
Notation eqM := B_ord.S.eqA.
Notation eqR := C_ord.S.eqA.
Notation gtL := A_ord.gtA.
Notation gtM := B_ord.gtA.
Notation gtR := C_ord.gtA.
Notation ltL := A_ext.ltA.
Notation ltM := B_ext.ltA.
Notation ltR := C_ext.ltA.

Definition triple := (L * M * R).
Definition fst3 (t : triple) : L := fst (fst t).
Definition snd3 (t : triple) : M := snd (fst t).
Definition trd3 (t : triple) : R := snd t.

Hint Unfold fst3 snd3 trd3.

Module LR_ord := LexicographicOrder A_ord B_ord.
Module Lex3 := LexicographicOrder LR_ord.Rel C_ord.

Definition LexProd3_Gt : relation triple := Lex3.LexProd_Gt.
Definition LexProd3_Lt : relation triple := Lex3.LexProd_Lt.

Notation "a >lex3 b" := (LexProd3_Gt a b) (at level 40).
Notation "a <lex3 b" := (LexProd3_Lt a b) (at level 40).

Section Well_foundedness.

Variables (WF_L : well_founded ltL) (WF_M : well_founded ltM)
(WF_R : well_founded ltR).

Lemma lexprod_wf : well_founded LexProd3_Lt.

End Well_foundedness.

Lemma LexProd3_Gt_inv a b c a' b' c' : (a, b, c) >lex3 (a', b', c') ->
gtL a a' \/ (eqL a a' /\ gtM b b') \/ (eqL a a' /\ eqM b b' /\ gtR c c').

Lemma LexProd3_1 a a' b b' c c' : gtL a a' -> (a, b, c) >lex3 (a', b', c').

Lemma LexProd3_2 a a' b b' c c' :
eqL a a' -> gtM b b' -> (a, b, c) >lex3 (a', b', c').

Lemma LexProd3_3 a a' b b' c c' :
eqL a a' -> eqM b b' -> gtR c c' -> (a, b, c) >lex3 (a', b', c').

Lemma LexProd3_lt a a' b b' c c' :
(a, b, c) >lex3 (a', b', c') -> (a', b', c') <lex3 (a, b, c).

Lemma LexProd3_lt_1 a a' b b' c c' : gtL a' a -> (a, b, c) <lex3 (a', b', c').

Lemma LexProd3_lt_2 a a' b b' c c' :
eqL a' a -> gtM b' b -> (a, b, c) <lex3 (a', b', c').

Lemma LexProd3_lt_3 a a' b b' c c' :
eqL a' a -> eqM b' b -> gtR c' c -> (a, b, c) <lex3 (a', b', c').

End LexicographicOrderTriple.