Library CoLoR.Util.List.ListPermutation

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-28
Some results concerning permutations of lists.

Set Implicit Arguments.



Section Multiplicity.

  Variables
    (A : Type) (eqA : relation A)
    (eqA_dec : forall x y, {eqA x y} + {~eqA x y})
    (eqA_Equivalence : Equivalence eqA).

  Lemma multiplicity_in: forall l x,
    multiplicity (list_contents eqA_dec l) x > 0 ->
    exists x', eqA x' x /\ In x' l.

  Lemma in_multiplicity: forall l a,
    In a l ->
    multiplicity (list_contents eqA_dec l) a > 0.

  Lemma multiplicity_countIn: forall l el,
    multiplicity (list_contents eqA_dec l) el = countIn eqA eqA_dec el l.

  Lemma multiplicity_dropNth_eq: forall l p el el',
    nth_error l p = Some el' ->
    eqA el el' ->
    multiplicity (list_contents eqA_dec (drop_nth l p)) el =
    multiplicity (list_contents eqA_dec l) el - 1.

  Lemma multiplicity_dropNth_neq: forall l p el el',
    nth_error l p = Some el' ->
    ~eqA el el' ->
    multiplicity (list_contents eqA_dec (drop_nth l p)) el =
    multiplicity (list_contents eqA_dec l) el.

End Multiplicity.

Section Permutation.

  Variables
    (A : Type) (eqA : relation A)
    (eqA_dec : forall x y, {eqA x y} + {~eqA x y})
    (eqA_Equivalence : Equivalence eqA).

  Lemma permutation_sym: forall l l',
    permutation eqA_dec l l' -> permutation eqA_dec l' l.

  Lemma permutation_in: forall l l' a, permutation eqA_dec l l' ->
    In a l -> exists a', eqA a' a /\ In a' l'.

  Lemma permutation_drop: forall (l l': list A) a b p,
    eqA a b -> nth_error l' p = Some b ->
    permutation eqA_dec (a :: l) l' -> permutation eqA_dec l (drop_nth l' p).

  Lemma permutation_cons: forall l l' a,
    permutation eqA_dec (a :: l) l' ->
    exists p a',
      nth_error l' p = Some a' /\
      eqA a a' /\
      permutation eqA_dec l (drop_nth l' p).

  Lemma permutation_length: forall (l l': list A),
    permutation eqA_dec l l' ->
    length l = length l'.

  Lemma insert_nth_permut: forall (l: list A) el n,
    permutation eqA_dec (insert_nth l n el) (el::l).

  Lemma insert_nth_permut': forall (l l': list A) el n,
    permutation eqA_dec l l' ->
    permutation eqA_dec (insert_nth l n el) (el::l').

End Permutation.

Section ListSim.

  Variable A : Type.
  Variable B : Type.
  Variable R : A -> B -> Prop.

  Inductive list_sim: list A -> list B -> Prop :=
  | conv_empty:
      list_sim nil nil
  | conv_cons: forall x y xs ys,
      R x y ->
      list_sim xs ys ->
      list_sim (x::xs) (y::ys).

  Lemma list_sim_nth : forall p l l' a, list_sim l l' ->
    nth_error l p = Some a ->
    exists b, nth_error l' p = Some b /\ R a b.

  Lemma list_sim_nth_rev : forall p l l' b, list_sim l l' ->
    nth_error l' p = Some b ->
    exists a, nth_error l p = Some a /\ R a b.

  Lemma list_sim_app : forall l1 l1' l2 l2',
    list_sim l1 l1' -> list_sim l2 l2' -> list_sim (l1 ++ l2) (l1' ++ l2').

  Lemma list_sim_unique : forall l m m',
    (forall x y y', In x l -> In y m -> In y' m' ->
      R x y -> R x y' -> y = y') ->
    list_sim l m -> list_sim l m' -> m = m'.

  Lemma list_sim_insert_nth : forall p l l' a a', nth_error l p = Some a ->
    nth_error l' p = Some a' -> R a a' ->
    list_sim (drop_nth l p) (drop_nth l' p) -> list_sim l l'.

  Lemma list_sim_length : forall l l', list_sim l l' -> length l = length l'.

  Lemma list_sim_tail : forall l l',
    list_sim l l' -> list_sim (tail l) (tail l').

End ListSim.

Section ListSim_iso.

  Variables
    (A : Type) (P eqA : relation A)
    (eqA_dec : forall x y, {eqA x y} + {~eqA x y})
    (eqA_Equivalence : Equivalence eqA)
    (P_eqA_comp : Proper (eqA ==> eqA ==> impl) P).

  Definition list_simA := @list_sim A A P.

  Lemma list_sim_permutation : forall l l' m,
    list_simA l l' -> permutation eqA_dec l m ->
    exists m', list_simA m m' /\ permutation eqA_dec l' m'.

End ListSim_iso.