Require Export Standardization.
Require Export Redundancy.

Definition OCN := list nat.

Definition nat_to_comp n c := nth c (all_st_comps n) (0,0).

Lemma nat_to_comp_ok : forall n c, comp_standard n (nat_to_comp n c) ->
                       nth_ok c (all_st_comps n) (0,0) = true.

Lemma nat_to_comp_inv : forall c n, comp_standard n c ->
                        exists k, c = nat_to_comp n k /\ k < length (all_st_comps n).

Definition OCN_to_CN (n:nat) (C:OCN) :=
  map (nat_to_comp n) C.

Definition OCN_ok (C:OCN) (n:nat) :=
  forall c, In c C -> nth_ok c (all_st_comps n) (0,0) = true.

Lemma OCN_standard : forall C n,
      OCN_ok C n -> standard n (OCN_to_CN n C).

Fixpoint OCN_compare (C C':OCN) :=
  match C, C' with
  | nil, nil => Eq
  | (_::_), nil => Gt
  | nil, (_::_) => Lt
  | (c::cs), (c'::cs') => match nat_compare c c' with
                          | Lt => Lt
                          | Gt => Gt
                          | Eq => OCN_compare cs cs'
                          end
  end.

Lemma OCN_compare_eq : forall C, OCN_compare C C = Eq.

Lemma OCN_compare_sym_Lt : forall C C', OCN_compare C C' = Lt -> OCN_compare C' C = Gt.

Lemma OCN_compare_sym_Gt : forall C C', OCN_compare C C' = Gt -> OCN_compare C' C = Lt.

Lemma eq_OCN_compare : forall C C', OCN_compare C C' = Eq -> C = C'.

Lemma OCN_compare_trans : forall C C' C'', OCN_compare C C' = Lt -> OCN_compare C' C'' = Lt ->
                                          OCN_compare C C'' = Lt.

Definition size_complete (R:list OCN) (n:nat) := forall k:nat,
          (exists C:comparator_network, sorting_network n C /\ length C = k) ->
           exists C' C'':comparator_network, In C' (map (OCN_to_CN n) R) /\ standard n (C'++C'')
                      /\ (forall C1 c C2, (C'++C'') = (C1++c::C2) -> ~redundant n C1 c)
                      /\ sorting_network n (C'++C'') /\ length (C'++C'') <= k.

Lemma empty_complete : forall n, size_complete (nil::nil) n.

Lemma complete_size : forall R n k, size_complete R n ->
                     (forall C, In C R -> length C = k) ->
                      forall S, sorting_network n S -> length S >= k.

Fixpoint till_n' (n:nat) : (list nat) :=
  match n with
  | O => nil
  | S k => till_n' k ++ (k :: nil)
  end.

Lemma till_n'_lemma : forall n i:nat, i<n -> In i (till_n' n).

Lemma till_n'_lt : forall n i:nat, In i (till_n' n) -> i < n.

Lemma till_n'_length: forall n, length (till_n' n) = n.

Lemma till_n'_char : forall n m, m < n -> forall x, nth m (till_n' n) x = m.

Lemma till_n'_NoDup : forall n, NoDup (till_n' n).

Definition add_to_all (cc:list nat) (C:OCN) :=
  map (fun c => (C ++ (c :: nil))) cc.

Fixpoint Generate (R:list OCN) (n:nat) : list OCN :=
  match R with
  | nil => nil
  | cons C R' => (add_to_all (till_n' (length (all_st_comps n))) C) ++ Generate R' n
  end.

Lemma add_to_all_standard : forall C n cc, OCN_ok C n ->
                           (forall c, In c cc -> c < length (all_st_comps n)) ->
                            forall C', In C' (add_to_all cc C) -> OCN_ok C' n.

Lemma add_to_all_In : forall l C S, In S (add_to_all l C) -> exists c, In c l /\ S = C ++ c :: nil.

Lemma add_to_all_NoDup : forall l, NoDup l -> forall C, NoDup (add_to_all l C).

Lemma Generate_length : forall n k R, (forall C, In C R -> length C = k) ->
                        forall C, In C (Generate R n) -> length C = S k.

Lemma Generate_channels : forall R m, m <= 1 -> Generate R m = nil.

Lemma Generate_OK : forall R n, (forall C, In C R -> OCN_ok C n) ->
                    forall C, In C (Generate R n) -> OCN_ok C n.

Lemma Generate_standard : forall R n, (forall C, In C R -> OCN_ok C n) ->
                    forall C, In C (Generate R n) -> standard n (OCN_to_CN n C).

Lemma Generate_extend : forall R n C c, In C R -> comp_standard n c ->
                                        In ((OCN_to_CN n C) ++ (c :: nil)) (map (OCN_to_CN n) (Generate R n)).

Lemma Generate_in : forall R n C c, In (C ++ c :: nil) (Generate R n) -> In C R.

Lemma in_Generate : forall R n C, In C (Generate R n) -> exists S x, C = S ++ x :: nil /\ In S R.

Lemma Generate_NoDup : forall R n, NoDup R -> NoDup (Generate R n).

Theorem Generate_complete : forall R n, size_complete R n ->
                           (forall C, In C R -> ~sorting_network n (OCN_to_CN n C)) ->
                                      size_complete (Generate R n) n.

Fixpoint filter_non_redundant (n:nat) (R:list OCN) :=
  match R with
  | nil => nil
  | (C :: R') => match last_redundant_dec n (OCN_to_CN n C) with
                 | left _ => filter_non_redundant n R'
                 | right _ => C :: filter_non_redundant n R'
                 end
  end.

Lemma filtered_in : forall n R C, In C (filter_non_redundant n R) -> ~last_redundant n (OCN_to_CN n C).

Lemma filtered_in_str : forall n R C, In C (map (OCN_to_CN n) R) -> ~last_redundant n C ->
                                      In C (map (OCN_to_CN n) (filter_non_redundant n R)).

Lemma filtered_in_src : forall n R C, In C (filter_non_redundant n R) -> In C R.

Lemma filtered_NoDup : forall n R, NoDup R -> NoDup (filter_non_redundant n R).

Definition OGenerate (R:list OCN) (n:nat) : list OCN :=
           filter_non_redundant n (Generate R n).

Theorem OGenerate_complete : forall R n, size_complete R n ->
                            (forall C, In C R -> ~sorting_network n (OCN_to_CN n C)) ->
                                       size_complete (OGenerate R n) n.

Hint Resolve OCN_compare_eq eq_OCN_compare OCN_compare_trans OCN_compare_sym_Gt : core.