Library Redundancy
Definition redundant (n:nat) (C:comparator_network) (c:comparator) :=
forall s:bin_seq n, apply c (full_apply C s) = full_apply C s.
Lemma redundant_outputs : forall n C c, redundant n C c ->
outputs C n = outputs (C ++ (c::nil)) n.
Lemma outputs_redundant : forall n C c, outputs C n = outputs (C ++ (c::nil)) n ->
redundant n C c.
Lemma SN_redundant : forall n C c C', sorting_network n (C ++ (c::C')) ->
redundant n C c -> sorting_network n (C ++ C').
Redundancy wrt a set of inputs.
This allows us to define a function removing redundant comparators from a network.
Definition red_wrt (n:nat) (I:list (bin_seq n)) (C:comparator_network) (c:comparator) :=
forall s, In s I -> apply c (full_apply C s) = full_apply C s.
Lemma redundant_red_wrt : forall n C c, redundant n C c -> forall I, red_wrt n I C c.
Lemma red_wrt_redundant : forall n C c, red_wrt n (all_bin_seqs n) C c -> redundant n C c.
Lemma red_wrt_dec : forall n I C c, {red_wrt n I C c} + {~red_wrt n I C c}.
Lemma redundant_dec : forall n C c, {redundant n C c} + {~redundant n C c}.
Fixpoint rem_red (n:nat) (C:comparator_network) (I:list (bin_seq n)) :=
match C with
| nil => nil
| c :: C' => match (red_wrt_dec _ I nil c) with
| left _ => rem_red n C' I
| right _ => c :: rem_red n C' (map (apply c (n:=n)) I)
end
end.
Definition remove_red (n:nat) (C:comparator_network) := rem_red n C (all_bin_seqs n).
Lemma rem_red_channels : forall n C I, channels n C -> channels n (rem_red n C I).
Lemma rem_red_standard : forall n C I, standard n C -> standard n (rem_red n C I).
Lemma rem_red_length : forall n C I, length (rem_red n C I) <= length C.
Lemma rem_red_not_redundant : forall n C I C' c C'', rem_red n C I = C' ++ c :: C'' ->
~ red_wrt I C' c.
Lemma rem_red_fixpoint : forall n C I,
(forall C' c C'', C = C' ++ c :: C'' -> ~ red_wrt I C' c) ->
rem_red n C I = C.
Lemma rem_red_apply : forall n C I s, In s I -> full_apply C s = full_apply (rem_red n C I) s.
Lemma rem_red_outputs : forall n C, outputs C n = outputs (remove_red n C) n.
Lemma rem_red_SN : forall n C, sorting_network n C -> sorting_network n (remove_red n C).
Lemma map_ext_str : forall (A B : Type) (f g:A->B), forall l, (forall a, In a l -> f a = g a) -> map f l = map g l.
Lemma rem_red_app : forall n C' C'' I, rem_red n (C'++C'') I = rem_red n C' I ++ rem_red n C'' (map (full_apply C' (n:=n)) I).
Particular case: given a network, its last comparator is redundant.