Library Permutations
Definition permut := list (nat*nat).
Definition dom (P:permut) := map (fst (A:=nat) (B:=nat)) P.
Definition cod (P:permut) := map (snd (A:=nat) (B:=nat)) P.
Fixpoint all_lt n (P:list nat) : Prop :=
match P with
| nil => True
| x :: l => x < n /\ all_lt n l
end.
Lemma all_lt_char : forall n P, (forall x, In x P -> x < n) -> all_lt n P.
Lemma all_lt_In : forall n P i, all_lt n P -> In i P -> i < n.
Lemma all_lt_dec : forall n P, {all_lt n P} + {~all_lt n P}.
Lemma all_lt_remove : forall n P, all_lt n P -> forall H x,
all_lt n (remove H x P).
Definition permutation n (P:permut) :=
NoDup (dom P) /\ all_lt n (dom P) /\ forall i, In i (dom P) <-> In i (cod P).
Lemma permutation_Prop_cod : forall n P, permutation n P -> forall T : nat -> Prop,
(forall i, In i (dom P) -> T i) -> (forall i, In i (cod P) -> T i).
Section Basic_Properties.
Variable n : nat.
Variable P : permut.
Hypothesis HP : permutation n P.
Lemma permutation_all_lt_dom : all_lt n (dom P).
Lemma permutation_all_lt_cod : all_lt n (cod P).
Lemma permutation_in_dom : forall k m, In (k,m) P -> k < n.
Lemma permutation_in_cod : forall k m, In (k,m) P -> m < n.
Lemma permutation_NoDup_dom : NoDup (dom P).
Lemma permutation_NoDup_cod : NoDup (cod P).
Lemma permutation_Permutation : Permutation (dom P) (cod P).
Lemma permutation_In_dom_cod : forall x, In x (dom P) -> In x (cod P).
Lemma permutation_In_cod_dom : forall x, In x (cod P) -> In x (dom P).
End Basic_Properties.
Hint Resolve permutation_all_lt_dom permutation_all_lt_cod
permutation_NoDup_dom permutation_NoDup_cod : core.
Fixpoint val (x:nat) (P:permut) : nat :=
match P with
| nil => x
| (i,j) :: P' => if (eq_nat_dec x i) then j else val x P'
end.
Lemma val_lt_lemma : forall n P i, all_lt n (cod P) -> i < n -> val i P < n.
Lemma val_lt : forall n P i, permutation n P -> i < n -> val i P < n.
Lemma val_not_in : forall P i, ~In i (dom P) -> val i P = i.
Lemma val_in_snd : forall P i, In i (dom P) -> In (i,val i P) P.
Lemma NoDup_val_lemma : forall P:permut, NoDup (dom P) -> NoDup (cod P) ->
forall i j, In (i,j) P -> val i P = j.
Lemma NoDup_val : forall n P, permutation n P ->
forall i j, In (i,j) P -> val i P = j.
Definition equivalent_perm (P Q:permut) := forall i, val i P = val i Q.
Lemma equivalent_perm_refl : forall P, equivalent_perm P P.
Lemma equivalent_perm_sym : forall P Q, equivalent_perm P Q ->
equivalent_perm Q P.
Lemma equivalent_perm_trans : forall P Q R, equivalent_perm P Q ->
equivalent_perm Q R ->
equivalent_perm P Q.
Fixpoint apply_perm (P:permut) (n:nat) (s:bin_seq n) : bin_seq n :=
match P with
| nil => s
| cons (i,j) P' => set (apply_perm P' _ s) i (get s j)
end.
Lemma apply_perm_get_lemma : forall P:permut, forall n,
all_lt n (dom P) -> all_lt n (cod P) ->
forall s:bin_seq n, forall i, i < n ->
get (apply_perm P s) i = get s (val i P).
Lemma apply_perm_get : forall P:permut, forall n, permutation n P ->
forall s:bin_seq n, forall i, i < n ->
get (apply_perm P s) i = get s (val i P).
Lemma apply_perm_equiv : forall P Q:permut, forall n,
permutation n P -> permutation n Q ->
equivalent_perm P Q ->
forall s:bin_seq n, apply_perm P s = apply_perm Q s.
Lemma zeros_apply_perm_count : forall n, forall s:bin_seq n, forall P,
NoDup (dom P) -> NoDup (cod P) ->
all_lt n (dom P) -> all_lt n (cod P) ->
zeros (apply_perm P s) =
zeros s + count_zeros s (cod P)
- count_zeros s (dom P).
Lemma zeros_apply_perm : forall n, forall s:bin_seq n, forall P, permutation n P ->
zeros (apply_perm P s) = zeros s.
Lemma get_perm_set_lemma : forall n P, NoDup (dom P) -> NoDup (cod P) ->
all_lt n (dom P) -> all_lt n (cod P) ->
forall x:bin_seq n, forall i,
get (apply_perm P x) i = get x (val i P).
Lemma get_perm_set : forall n P, permutation n P -> forall x:bin_seq n,
forall i, get (apply_perm P x) i = get x (val i P).
Definition id_permutation : permut := nil.
Lemma id_perm : forall n, permutation n id_permutation.
Lemma id_perm_val : forall i, val i id_permutation = i.
Lemma id_perm_get : forall n, forall s:bin_seq n, forall i,
get (apply_perm id_permutation s) i = get s i.
Lemma id_perm_apply : forall n, forall s:bin_seq n,
apply_perm id_permutation s = s.
Fixpoint inverse_perm (P:permut) : permut :=
match P with
| nil => nil
| (i,j) :: P' => (j,i) :: inverse_perm P'
end.
Lemma inverse_perm_dom : forall P, dom P = cod (inverse_perm P).
Lemma inverse_perm_cod : forall P, cod P = dom (inverse_perm P).
Lemma inverse_perm_perm : forall P n, permutation n P ->
permutation n (inverse_perm P).
Hint Resolve inverse_perm_perm : core.
Lemma inverse_perm_In : forall P i j, In (i,j) P -> In (j,i) (inverse_perm P).
Lemma inverse_inverse_perm : forall P:permut, inverse_perm (inverse_perm P) = P.
Lemma inverse_perm_val_1 : forall n P, permutation n P -> forall i j,
val i P = j -> val j (inverse_perm P) = i.
Lemma inverse_perm_val_2 : forall n P, permutation n P ->
forall i, val (val i P) (inverse_perm P) = i.
Lemma inverse_perm_val_3 : forall n P, permutation n P ->
forall i, val (val i (inverse_perm P)) P = i.
Lemma inverse_perm_bin_seq : forall n P, permutation n P -> forall x:bin_seq n,
x = apply_perm (inverse_perm P) (apply_perm P x).
Applications
Lemma permutation_eq : forall n P, permutation n P -> forall x y:bin_seq n,
apply_perm P x = apply_perm P y -> x = y.
Lemma val_eq : forall n P i j, permutation n P -> i < n -> j < n ->
val i P = val j P -> i = j.
Lemma val_neq : forall n P i j, permutation n P -> i < n -> j < n ->
i <> j -> val i P <> val j P.
Lemma apply_perm_inverse : forall P n, permutation n P -> forall s:bin_seq n,
apply_perm P (apply_perm (inverse_perm P) s) = s.
Section Transpositions.
Definition transposition (i j:nat) := (i,j) :: (j,i) :: nil.
Variables i j : nat.
Variable Hij : i <> j.
Let T := transposition i j.
Lemma transp_perm : forall n, i < n -> j < n -> permutation n T.
Lemma transp_val_i : val i T = j.
Lemma transp_val_j : val j T = i.
Lemma transp_val_neq : forall k, k <> i -> k <> j -> val k T = k.
Lemma transp_get_i : forall n, forall s:bin_seq n, i < n -> j < n ->
get (apply_perm T s) i = get s j.
Lemma transp_get_j : forall n, forall s:bin_seq n, i < n -> j < n ->
get (apply_perm T s) j = get s i.
Lemma transp_get_neq : forall n, forall s:bin_seq n, i < n -> j < n ->
forall k, k <> i -> k <> j -> k < n ->
get (apply_perm T s) k = get s k.
Lemma transp_idemp : forall n, forall s:bin_seq n, i < n -> j < n ->
apply_perm T (apply_perm T s) = s.
Lemma transp_inverse_equiv : equivalent_perm T (inverse_perm T).
End Transpositions.
Lemma transp_sym : forall i j,
equivalent_perm (transposition i j) (transposition j i).
Lemma transp_sym_apply : forall n i j, i <> j -> forall s:bin_seq n,
i < n -> j < n ->
apply_perm (transposition i j) s =
apply_perm (transposition j i) s.