Library Prune
Pre-permutations
These are permutations in list form, which can be transformed into "our" permutations.Section Pre_permutations.
Fixpoint make_permutation_rec (n:nat) (l:list nat) : permut :=
match n, l with
| _, nil => nil
| O, _ => nil
| S k, x::l' => (k,x) :: make_permutation_rec k l'
end.
Definition make_permutation (l:list nat) : permut :=
rev (make_permutation_rec (length l) (rev l)).
Lemma make_permutation_dom : forall k l,
dom (make_permutation (k::l)) = (till_n (length l)).
Lemma make_permutation_cod : forall l, cod (make_permutation l) = l.
Variable n:nat.
Variable l:list nat.
Definition pre_permutation := NoDup l /\ all_lt n l /\ length l = n.
Lemma pre_permutation_dec : {pre_permutation} + {~pre_permutation}.
Lemma pre_permutation_In : pre_permutation -> forall i, i < n -> In i l.
Lemma pre_permutation_lemma : pre_permutation ->
permutation n (make_permutation l).
End Pre_permutations.
Hint Resolve pre_permutation_lemma : core.
Section Prune.
The oracle will give indication as to what networks are subsumed by others.
Prune then verifies this, ignoring wrong information.
Definition Oracle := list (OCN * OCN * (list nat)).
Definition BTree := BinaryTree OCN.
Fixpoint run_oracle (n:nat) (O:Oracle) : bool * (BTree * (list OCN)) :=
match O with
| nil => (true,(nought,nil))
| (C,C',P) :: O' => match (pre_permutation_dec n P) with
| right _ => (false,(nought,nil))
| left A => match (subsumption_dec n (OCN_to_CN n C) (OCN_to_CN n C')
(make_permutation P)
(pre_permutation_lemma _ _ A)) with
| right _ => (false,(nought,nil))
| left _ => let (b,Tl) := (run_oracle n O') in
let (T,l) := Tl in
(b,(BT_add OCN_compare C T,C'::l))
end
end
end.
Definition oracle_ok n O := fst (run_oracle n O) = true.
Lemma run_lemma : forall n X O, oracle_ok n (X :: O) ->
oracle_ok n O.
Lemma oracle_perm : forall n O, oracle_ok n O ->
forall C C' P, In (C,C',P) O -> pre_permutation n P.
Lemma oracle_subs : forall n O, oracle_ok n O ->
forall C C' P HP, In (C,C',P) O -> subsumption n (OCN_to_CN n C) (OCN_to_CN n C') _ (pre_permutation_lemma n P HP).
Lemma run_3rd : forall n O, oracle_ok n O -> snd (snd (run_oracle n O)) = map (snd (B:=OCN)) (map (fst (B:=list nat)) O).
Lemma oracle_filter_in : forall n C C' P O, oracle_ok n O -> In (C,C',P) O -> BT_In C (fst (snd (run_oracle n O))).
Lemma oracle_filter_wf : forall n O, BT_wf OCN_compare (fst (snd (run_oracle n O))).
Definition OCN_eq_dec := list_eq_dec eq_nat_dec.
Fixpoint oracle_test (F:BTree) (R:list OCN) :=
match F with
| nought => true
| _ => match R with
| nil => false
| C' :: R' => let (C,F') := (BT_split F nil) in
match (OCN_eq_dec C C') with
| left _ => oracle_test F' R'
| right _ => oracle_test F R'
end
end
end.
Lemma oracle_test_in_lemma : forall R F, BT_wf OCN_compare F -> oracle_test F R = true ->
forall C, BT_In C F -> In C R.
Lemma oracle_test_in : forall n O, oracle_ok n O ->
forall R, oracle_test (fst (snd (run_oracle n O))) R = true ->
forall C C' P, In (C,C',P) O -> In C R.
Definition Prune (O:Oracle) (R:list OCN) (n:nat)
: list OCN :=
match (run_oracle n O) with
| (false,_) => R
| (true,XY) => let (X,Y) := XY in
let R' := remove_all OCN_eq_dec Y R in
match (oracle_test X R') with
| false => R
| true => R'
end
end.
Lemma Prune_nil : forall O n, Prune O nil n = nil.
Lemma Prune_in : forall O R n C, In C (Prune O R n) -> In C R.
Lemma Prune_standard : forall O R n, (forall C, In C R -> standard n (OCN_to_CN n C)) ->
forall C, In C (Prune O R n) -> standard n (OCN_to_CN n C).
Lemma Prune_NoDup : forall O R n, NoDup R -> NoDup (Prune O R n).
Theorem Prune_complete : forall O R n, size_complete R n ->
(forall C, In C R -> standard n (OCN_to_CN n C)) ->
(forall C C' c C'', In C R -> OCN_to_CN n C = C' ++ c :: C'' -> ~ redundant n C' c) ->
(forall C C', In C R -> In C' R -> length C = length C') ->
size_complete (Prune O R n) n.
Lemma Prune_SN : forall O R n m C, sorting_network n (OCN_to_CN n C) -> In C R ->
(forall C', In C' R -> length C' = m /\ standard n (OCN_to_CN n C')) ->
exists C', In C' (Prune O R n) /\ sorting_network n (OCN_to_CN n C').
End Prune.
Lemma SN_0 : sorting_network 0 nil.
Lemma SN_1 : sorting_network 1 nil.
Lemma nil_not_SN : forall n, n > 1 -> ~sorting_network n nil.
Inductive Answer : Set :=
| yes : nat -> nat -> Answer
| no : forall n k:nat, forall R:list OCN,
NoDup R ->
(forall C, In C R -> length C = k) ->
(forall C, In C R -> standard n (OCN_to_CN n C)) -> Answer
| maybe : Answer.
Lemma GP_start_0 : NoDup (nil :: nil (A:=OCN)).
Lemma GP_start_1 : forall C:OCN, In C (nil :: nil) -> length C = 0.
Lemma GP_start_2 : forall n C, In C (nil :: nil) -> standard n (OCN_to_CN n C).
Lemma GP_it_0 : forall n O R, NoDup R -> NoDup (Prune O (OGenerate R n) n).
Lemma GP_it_1 : forall n O k R, NoDup R -> (forall C, In C R -> length C = k) ->
forall C, In C (Prune O (OGenerate R n) n) -> length C = S k.
Lemma GP_it_2 : forall n X R, NoDup R ->
(forall C, In C R -> standard n (OCN_to_CN n C)) ->
(forall C, In C (Prune X (OGenerate R n) n) -> standard n (OCN_to_CN n C)).
Lemma GP_SC : forall R n, (forall C, In C R -> standard n (OCN_to_CN n C)) ->
forall C, In C (map (OCN_to_CN n) R) -> channels n C.
Fixpoint Generate_and_Prune (m n:nat) (O:list Oracle) :=
match n with
| 0 => match m with
| 0 => yes 0 0
| 1 => yes 1 0
| _ => no m 0 (nil :: nil) GP_start_0 GP_start_1 (GP_start_2 m)
end
| S k => match O with
| nil => maybe
| X::O' => let GP := (Generate_and_Prune m k O') in
match GP with
| maybe => maybe
| yes p q => yes p q
| no p q R HR0 HR1 HR2 => let H0 := GP_it_0 p X _ HR0 in
let H1 := GP_it_1 p X _ _ HR0 HR1 in
let H2 := GP_it_2 p X _ HR0 HR2 in
let GP' := Prune X (OGenerate R p) p in
match (exists_SN_dec p (map (OCN_to_CN p) GP') (GP_SC GP' p H2)) with
| left _ => yes p (S q)
| right _ => no p (S q) GP' H0 H1 H2
end
end
end
end.
Lemma GP_yes_no_OK : forall m n O,
(forall p q, Generate_and_Prune m n O = yes p q -> p = m) /\
(forall p q R HR0 HR1 HR2, Generate_and_Prune m n O = no p q R HR0 HR1 HR2 -> p = m /\ q = n).
Lemma GP_yes_OK : forall m n O p q, Generate_and_Prune m n O = yes p q -> p = m.
Lemma GP_yes_weak : forall m n O p q, Generate_and_Prune m n O = yes p q ->
exists C, sorting_network p C /\ length C = q.
Lemma GP_no_OK_1 : forall m n O p q R HR0 HR1 HR2, Generate_and_Prune m n O = no p q R HR0 HR1 HR2 -> p = m.
Lemma GP_no_OK_2 : forall m n O p q R HR0 HR1 HR2, Generate_and_Prune m n O = no p q R HR0 HR1 HR2 -> q = n.
Lemma GP_yes_le : forall m n O p q, Generate_and_Prune m n O = yes p q -> q <= n.
Lemma GP_channels_0 : forall n O, Generate_and_Prune 0 n O = yes 0 0
\/ Generate_and_Prune 0 n O = maybe.
Lemma GP_channels_1 : forall n O, Generate_and_Prune 1 n O = yes 1 0
\/ Generate_and_Prune 1 n O = maybe.
Lemma GP_channels : forall m n O R HR0 HR1 HR2, Generate_and_Prune m n O = no m n R HR0 HR1 HR2 -> m > 1.
Lemma OCN_to_CN_inv : forall n C, standard n C -> exists O, OCN_to_CN n O = C.
Lemma nat_to_comp_inj : forall n c c', nat_to_comp n c = nat_to_comp n c' ->
c < length (all_st_comps n) -> c' < length (all_st_comps n) ->
c = c'.
Lemma OCN_to_CN_inj : forall n C C', OCN_ok C n -> OCN_ok C' n -> OCN_to_CN n C = OCN_to_CN n C' -> C = C'.
Lemma OCN_standard_ok : forall C n,
standard n (OCN_to_CN n C) -> OCN_ok C n.
Lemma GP_non_red : forall m n O R HR0 HR1 HR2, Generate_and_Prune m n O = no m n R HR0 HR1 HR2 ->
forall C, In C R ->
forall C' c C'', OCN_to_CN m C = C' ++ (c :: C'') -> ~redundant m C' c.
Lemma GP_no_SN : forall m n O R HR0 HR1 HR2, Generate_and_Prune m n O = no m n R HR0 HR1 HR2 ->
forall C, In C R -> ~ sorting_network m (OCN_to_CN m C).
Lemma GP_complete : forall m n O R HR0 HR1 HR2, Generate_and_Prune m n O = no m n R HR0 HR1 HR2 ->
size_complete R m.
Theorem GP_no : forall m n O R HR0 HR1 HR2, Generate_and_Prune m n O = no m n R HR0 HR1 HR2 ->
forall C, sorting_network m C -> length C > n.
Lemma GP_has_SN : forall m n O, Generate_and_Prune m n O <> maybe ->
forall k, (forall C, sorting_network m C -> length C >= k) ->
forall C, sorting_network m C -> length C = k ->
n >= k -> Generate_and_Prune m n O = yes m k.
Fixpoint Generate_it (n m:nat) : list OCN :=
match m with
| O => nil :: nil
| S k => Generate (Generate_it n k) n
end.
Lemma Generate_has_all : forall R n k, standard n (OCN_to_CN n R) -> length R = k -> In R (Generate_it n k).
Lemma Generate_it_length : forall k R n, In R (Generate_it n k) -> length R = k.
Lemma Generate_it_standard : forall k R n, In R (Generate_it n k) -> standard n (OCN_to_CN n R).
Fixpoint Nil (n:nat) : list Oracle :=
match n with
| O => nil
| S k => nil :: Nil k
end.
Lemma exists_SN_dec_str : forall m l, (forall C, In C l -> channels m C) ->
{C | In C l & sorting_network m C} +
{forall C, In C l -> ~sorting_network m C}.
Lemma SN_size_dec : forall n k, {exists C, sorting_network n C /\ length C = k}
+ {forall C, length C = k -> ~sorting_network n C}.
Fixpoint dummy_net (n:nat) : comparator_network :=
match n with
| O => nil
| S k => 0[<]1 :: dummy_net k
end.
Lemma dummy_length : forall n, length (dummy_net n) = n.
Lemma dummy_standard : forall n k, 1 < k -> standard k (dummy_net n).
Lemma minimal_SN : forall n, (exists C, sorting_network n C) ->
exists C, sorting_network n C /\
forall C', sorting_network n C' -> length C <= length C'.
Lemma GP_yes_str : forall m n O p q, Generate_and_Prune m n O = yes p q ->
forall C, sorting_network p C -> length C >= q.
Theorem GP_yes : forall m n O k, Generate_and_Prune m n O = yes m k ->
(forall C, sorting_network m C -> length C >= k) /\
exists C, sorting_network m C /\ length C = k.