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.

  Lemma lexv_trans n : Transitive eq -> Transitive gt ->
    gt @ eq << gt -> eq @ gt << gt ->
    Transitive (lexv (n:=n) eq gt).

End lexv.

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.