Library Standardization
Definition apply_perm_to_comp (P:permut) (c:comparator) :=
let (x,y) := c in ((val x P),(val y P)).
Definition apply_perm_to_net (P:permut) (S:comparator_network) :=
map (apply_perm_to_comp P) S.
Lemma apply_perm_to_net_inv : forall n P, permutation n P -> forall C,
C = apply_perm_to_net (inverse_perm P) (apply_perm_to_net P C).
Lemma permutation_length : forall S:comparator_network,
forall P, length (apply_perm_to_net P S) = length S.
Lemma permutation_channels : forall n:nat, forall S:comparator_network,
forall P, permutation n P -> channels n S ->
channels n (apply_perm_to_net P S).
Definition permute (i j:nat) (S:comparator_network) : comparator_network :=
apply_perm_to_net (transposition i j) S.
Lemma permute_length : forall i j, forall S:comparator_network,
length S = length (permute i j S).
Lemma permute_channels : forall n:nat, forall S:comparator_network,
forall i j, i <> j -> i < n -> j < n -> channels n S ->
channels n (permute i j S).
Lemma permute_app : forall C C' x y,
permute x y (C++C') = permute x y C ++ permute x y C'.
These two lemmas turned out not to be needed, but who knows?
Lemma apply_perm_transp_red : forall n x y i j,
x < n -> y < n -> i < n -> j < n ->
forall s:bin_seq n, let T := transposition x y in
apply i[<]j (apply_perm T s) =
apply_perm T (apply (apply_perm_to_comp T i[<]j) s).
Opaque apply.
Transparent apply.
Lemma permute_char : forall n x y, x < n -> y < n ->
forall C, forall s s':bin_seq n, channels n C ->
full_apply C (apply_perm (transposition x y) s)
= full_apply C (apply_perm (transposition x y) s') ->
full_apply (permute x y C) s
= full_apply (permute x y C) s'.
Lemma full_apply_permutation : forall n P, permutation n P ->
forall C, channels n C -> forall s:bin_seq n,
full_apply (apply_perm_to_net P C) s =
apply_perm (inverse_perm P)
(full_apply C (apply_perm P s)).
Lemma full_apply_permute : forall n x y, x <> y -> x < n -> y < n ->
forall C, channels n C -> forall s:bin_seq n,
let T := transposition x y in
full_apply (permute x y C) s =
apply_perm T (full_apply C (apply_perm T s)).
Function standardize (S:comparator_network) {measure length S} : comparator_network :=
match S with
| nil => nil
| cons c S' => let (x,y) := c in
match (le_lt_dec x y) with
| left _ => (x[<]y :: standardize S')
| right Hxy => (y[<]x :: standardize (permute x y S'))
end
end.
Lemma standardize_le_lemma : forall S C x y, x <= y -> C = (x[<]y :: S) ->
standardize C = x[<]y :: standardize S.
Lemma standardize_le : forall S x y, x <= y ->
standardize (x[<]y :: S) = x[<]y :: standardize S.
Lemma standardize_gt_lemma : forall S C x y, forall Hxy: x > y, C = (x[<]y :: S) ->
standardize C = y[<]x :: standardize (permute x y S).
Lemma standardize_gt : forall S x y, forall Hxy: x > y,
standardize (x[<]y :: S)
= y[<]x :: standardize (permute x y S).
Lemma standardization_channels : forall n S, channels n S ->
channels n (standardize S).
Lemma channels_standardization : forall n C, channels n (standardize C) ->
channels n C.
Lemma standardization_length : forall S:comparator_network,
length S = length (standardize S).
Theorem standardization : forall n S, channels n S ->
standard n (standardize S).
Lemma standardization_char : forall n C, channels n C -> forall s s':bin_seq n,
full_apply C s = full_apply C s' ->
full_apply (standardize C) s = full_apply (standardize C) s'.
Lemma standardization_sort_lemma : forall C n, channels n C ->
(forall s:bin_seq n, sorted (full_apply C s)) ->
forall s:bin_seq n,
sorted (full_apply (standardize C) s).
Theorem standardization_sort : forall C n, sorting_network n C ->
sorting_network n (standardize C).
Lemma standardize_idemp : forall C, standardize (standardize C) = standardize C.
Lemma standardize_app : forall n C C', standard n C ->
standardize (C ++ C') = C ++ standardize C'.