# 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
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.