Library CoLoR.Util.List.ListLex

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Solange Coupet-Grimal and William Delobel, 2006-01-09
  • Adam Koprowski, 2007-06-01 added Decidability section
Definition and properties of lexicographic order on lists of elements of a setoid. In particular, proofs that lex 'transmits' strict partial order property, and is a lifting.


Module LexOrder (ES : Eqset).

  Section Lex.

    Variable r : relation ES.A.

    Inductive lex : relation (list ES.A) :=
      | lex1 : forall h h' (l l' : list ES.A),
        r h h' -> length l = length l' -> lex (h::l) (h'::l')
      | lex2 : forall (h : ES.A) (l l' : list ES.A),
        lex l l' -> lex (h::l) (h::l').

    Lemma lex_length : forall ss ts : list ES.A,
      lex ss ts -> length ss = length ts.

    Lemma SPO_to_lex_SPO : forall (ss : list ES.A),
      (forall s, In s ss ->
        (forall t u, r s t -> r t u -> r s u) /\ (r s s -> False)) ->
      (forall ts us : list ES.A, lex ss ts -> lex ts us -> lex ss us)
      /\ (lex ss ss -> False).

    Lemma irrefl_to_lex_irrefl : forall (ss : list ES.A),
      (forall s, In s ss -> r s s -> False) -> lex ss ss -> False.

    Lemma lex_lifting_aux : forall n (l : list ES.A),
      length l = n -> Accs r l -> Restricted_acc (Accs r) lex l.

    Section Lex_and_one_less.

      Lemma one_less2lex : forall l l', one_less r l l' -> lex l l'.

    End Lex_and_one_less.

  End Lex.

  Lemma lex_lifting : forall (r : relation ES.A) (l : list ES.A),
    Accs r l -> Restricted_acc (Accs r) (lex r) l.

  Section Decidability.

    Import Peano_dec.

    Variable eqA_dec : forall a b : ES.A, {a = b} + {~a = b}.

    Lemma lex_dec : forall R l l',
      (forall a b, In a l -> In b l' -> {R a b} + {~R a b}) ->
      {lex R l l'} + {~lex R l l'}.

  End Decidability.

  Section Homomorphism.

    Variable R : relation ES.A.
    Variable f : ES.A -> ES.A.

    Lemma lex_homomorphic : forall l l',
      (forall x x', In x l -> In x' l' -> R x x' -> R (f x) (f x')) ->
      lex R l l' -> lex R (map f l) (map f l').

  End Homomorphism.

End LexOrder.