Library CoLoR.Util.List.ListPermutation

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
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.