Library CoLoR.Util.List.SortUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Leo Ducas, 2007-08-06
auxiliary lemmas on Coq's sort and lelistA predicates and on Coq's multiplicity function

Set Implicit Arguments.

lelistA and sort

Lemma sort_incl_aux : forall B (T S : relation B) a l,
  T << S -> lelistA T a l -> lelistA S a l.

Lemma sort_incl : forall B (T S : relation B) l,
  T << S -> sort T l -> sort S l.

Lemma sort_transitive : forall B (a : B) L rel,
  transitive rel -> sort rel (a::L) -> forall x, In x L -> rel a x.

Lemma lelistA_map A (R : relation A) B (S : relation B) (f : A->B)
      (f_mon : Proper (R ==> S) f) a :
  forall l, lelistA R a l -> lelistA S (f a) (map f l).

Lemma sort_map A (R : relation A) B (S : relation B) (f : A->B)
      (f_mon : Proper (R ==> S) f) :
  forall l, sort R l -> sort S (map f l).

Lemma nodup_lelistA_strict : forall B a S (mb : list B)
  (HL : nodup (a::mb)), lelistA (S%) a mb -> lelistA S a mb.

Lemma nodup_sort_strict : forall B S (mb : list B)
  (HL : nodup mb), sort (S%) mb -> sort S mb.


Section multiplicity.

  Variables (B : Type) (B_eq_dec : forall x y : B, {x=y}+{x<>y}).

  Lemma In_multiplicity : forall mb a, In a mb ->
    multiplicity (list_contents B_eq_dec mb) a >= 1.

  Lemma multiplicity_nodup : forall mb,
    (forall a, multiplicity (list_contents B_eq_dec mb) a <= 1) -> nodup mb.

End multiplicity.


Section Sorted.

  Variables (A : Type) (lt : relation A) (lt_trans : Transitive lt) (d : A).

  Lemma Sorted_nth_S : forall l i, Sorted lt l ->
    i < length l -> S i < length l -> lt (nth i l d) (nth (S i) l d).

  Lemma HdRel_nth : forall l i n, Sorted lt l ->
    HdRel lt n l -> i < length l -> lt n (nth i l d).

  Lemma Sorted_nth : forall j l i, Sorted lt l ->
    i < length l -> j < length l -> i < j -> lt (nth i l d) (nth j l d).

End Sorted.