Library CoLoR.Util.Pair.PairLex

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
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.