# Library CoLoR.Util.Relation.Lexico

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2006-10-25
lexicographic ordering

Set Implicit Arguments.

## Lexicographic quasi-ordering on pairs.

Section lex.

We assume given a set A equipped with two relations gtA and eqA satisfying some compatibility condition, and a set B equipped with a relation gtB.

Variables (A B : Type) (gtA eqA : relation A) (gtB : relation B).

Definition of the lexicographic relation.

Inductive lex : relation (prod A B) :=
| lex1 a a' b b' : gtA a a' -> lex (a,b) (a',b')
| lex2 a a' b b' : eqA a a' -> gtB b b' -> lex (a,b) (a',b').

Lemma lex_intro : forall a a' b b',
gtA a a' \/ (eqA a a' /\ gtB b b') -> lex (a,b) (a',b').

We now prove that lex is wellfounded if both gtA and gtB are wellfounded, eqA is transitive and gtA absorbs eqA.

Variables (WF_gtA : WF gtA) (WF_gtB : WF gtB)
(eqA_trans : Transitive eqA) (Hcomp : eqA @ gtA << gtA).

Lemma SN_compat : forall a, SN gtA a -> forall a', eqA a a' -> SN gtA a'.

Lemma lex_SN_eq : forall a b,
SN lex (a,b) -> forall a', eqA a a' -> SN lex (a',b).

Lemma lex_SN :
forall a, SN gtA a -> forall b, SN gtB b -> SN lex (a, b).

Lemma WF_lex : WF lex.

End lex.

symprod is included in lex.

Lemma symprod_lex A (gtA : relation A) :
symprod gtA gtA << lex gtA Logic.eq gtA.

lex is monotone wrt inclusion.

Instance lex_incl A B : Proper (incl ==> incl ==> incl ==> incl) (@lex A B).

Instance lex_same A B : Proper (same ==> same ==> same ==> same) (@lex A B).

## Type of n-tuples of elements of A.

Fixpoint prodn n A : Type :=
match n with
| 0 => unit
| S n' => prod A (prodn n' A)
end.

Fixpoint projn n {A} : prodn n A -> forall i, i<n -> A :=
match n as n return prodn n A -> forall i, i<n -> A with
| 0 => fun xs i (hi : i<0) => False_rect _ (lt_n_0 hi)
| S n' => fun xs i =>
match i as i return i<S n' -> A with
| 0 => fun _ => fst xs
| S i' => fun hi => projn (snd xs) (lt_S_n hi)
end
end.

## Lexicographic order on tuples.

Fixpoint lexn {n A} (eqA gtA : relation A) :=
match n as n return relation (prodn n A) with
| 0 => empty_rel
| S n' => lex gtA eqA (lexn eqA gtA)
end.

Section lexn.

Variables (A : Type) (eqA gt : relation A).

Equivalent definition.

Lemma lexn_eq : forall n (xs ys : prodn n A), lexn eqA gt xs ys <->
(exists i (hi : i<n), gt (projn xs hi) (projn ys hi)
/\ forall j, j<i -> forall hj : j<n, eqA (projn xs hj) (projn ys hj)).

Wellfoundedness.

Variables (gt_wf : WF gt) (eqA_trans : Transitive eqA)
(Hcomp : eqA @ gt << gt).

Lemma lexn_wf n : WF (lexn (n:=n) eqA gt).

End lexn.

Monotony wrt incl.

Instance lexn_incl A : forall n, Proper (incl ==> incl ==> incl) (@lexn n A).

## Convert of vector of size n into an n-tuple.

Fixpoint prod_of_vec n A (v : vector A n) :=
match v in vector _ n return prodn n A with
| Vnil => tt
| Vcons x v' => (x, prod_of_vec v')
end.

Lemma projn_prod_of_vec : forall A n (xs : vector A n) i (hi : i<n),
projn (prod_of_vec xs) hi = Vnth xs hi.

## Lexicographic order on vectors of fixed length.

Definition lexv {n A} (eq gt : relation A) : relation (vector A n) :=
fun v w => lexn eq gt (prod_of_vec v) (prod_of_vec w).

Section lexv.

Variables (A : Type) (eq gt : relation A).

Equivalent definition.

Lemma lexv_eq : forall n (xs ys : vector A n), lexv eq gt xs ys <->
(exists i (hi : i<n), gt (Vnth xs hi) (Vnth ys hi)
/\ forall j, j<i -> forall hj : j<n, eq (Vnth xs hj) (Vnth ys hj)).

Wellfoundedness.

Section wf.

Variables (gt_wf : WF gt) (eq_trans : Transitive eq)
(Hcomp : eq @ gt << gt).

Lemma lexv_wf n : WF (lexv (n:=n) eq gt).

End wf.

lexv eq gt absorbs Vforall2 eq.

Lemma lexv_forall2_l : eq @ gt << gt -> Transitive eq ->
forall n, Vforall2 eq (n:=n) @ lexv eq gt << lexv eq gt.

Lemma lexv_forall2_r : gt @ eq << gt -> Transitive eq ->
forall n, lexv eq gt @ Vforall2 eq (n:=n) << lexv eq gt.

lexv eq gt is invariant by Vforall2 eq.

Global Instance lexv_forall2 n : Transitive eq -> Symmetric eq ->
Proper (eq ==> eq ==> impl) gt ->
Proper (Vforall2 eq ==> Vforall2 eq ==> impl) (lexv (n:=n) eq gt).

Transitivity.
Monotony wrt incl.

Instance lexv_incl n A : Proper (incl ==> incl ==> incl) (@lexv n A).

Vrel1 is included in lexv.

Lemma Vrel1_lexv n A (gt : relation A) :
Vrel1 (n:=n) gt << lexv Logic.eq gt.

lexv (opt eq) (opt gt) absorbs Vforall2_opt eq.

Section Vforall2_opt.

Variables (A : Type) (eq gt : relation A).

Lemma lexv_forall2_opt_l : eq @ gt << gt -> Transitive eq -> forall n,
Vforall2_opt (n:=n) eq @ lexv (opt eq) (opt gt)
<< lexv (opt eq) (opt gt).

Lemma lexv_forall2_opt_r : gt @ eq << gt -> Transitive eq -> forall n,
lexv (opt eq) (opt gt) @ Vforall2_opt (n:=n) eq
<< lexv (opt eq) (opt gt).

End Vforall2_opt.

Monotony of lexv wrt arguments.

Lemma lexv_mon_arg A (eq gt : relation A) n (ts us : vector A n)
p (ts' us' : vector A p) :
lexv eq gt ts us -> lexv eq gt (Vapp ts ts') (Vapp us us').

Monotony of Rof lexv (Vopt_filter M) when M is sorted.

Lemma lexv_opt_filter_sorted_mon_arg A (eq gt : relation A)
n (ks : vector nat n) (ks_sorted : sorted ks) p (ts : vector A p)
q (us : vector A q) p' (ts' : vector A p') q' (us' : vector A q') :
lexv (opt eq) (opt gt) (Vopt_filter ks ts) (Vopt_filter ks us) ->
lexv (opt eq) (opt gt) (Vopt_filter ks (Vapp ts ts'))
(Vopt_filter ks (Vapp us us')).

## Lexicographic order on lists of bounded length.

Section lexl.

Variables (m : nat) (A : Type) (eq gt : relation A).

Inductive lexl : relation (list A) :=
| lexl_intro : forall (xs ys : list A) i
(im : i < m) (ix : i < length xs) (iy : i < length ys),
gt (ith ix) (ith iy)
-> (forall j (ji : j < i) (jx : j < length xs) (jy : j < length ys),
eq (ith jx) (ith jy))
-> lexl xs ys.

Variables (gt_wf : WF gt) (eq_trans : Transitive eq)
(Hcomp : eq @ gt << gt).

Lemma lexl_wf : WF lexl.

End lexl.

Instance lexl_incl m A : Proper (incl ==> incl ==> incl) (@lexl m A).

## Lexicographic ordering on dependent pairs.

Section lexd.

Variables (A : Type) (B : A -> Type).

Section def.

Variables (gtA : relation A) (gtB : forall a : A, relation (B a)).

Inductive lexd : relation (sigT B) :=
| lexdl a a' (b : B a) (b' : B a') : gtA a a' -> lexd (existT b) (existT b')
| lexdr a (b b' : B a) : gtB b b' -> lexd (existT b) (existT b').

End def.

Lemma lexd_incl : forall gt1 gt1', gt1 << gt1'
-> forall gt2 gt2', (forall a, gt2 a << gt2' a)
-> lexd gt1 gt2 << lexd gt1' gt2'.

End lexd.