Library BinarySequences

Require Export Basics.
Require Export Equality.

Inductive bin_seq : nat -> Set :=
  | empty : bin_seq 0
  | zero : forall n:nat, bin_seq n -> bin_seq (S n)
  | one : forall n:nat, bin_seq n -> bin_seq (S n).

Notation "[0] x" := (zero _ x) (at level 0, right associativity).
Notation "[1] x" := (one _ x) (at level 0, right associativity).
Notation "[]" := empty.

Fixpoint get n (s:bin_seq n) (i:nat) : nat :=
  match n with
  | O => 2
  | S k => match i with
           | O => match s with
                  | empty => 2
                  | [0] _ => 0
                  | [1] _ => 1
                  end
           | S j => match s with
                  | empty => 2
                  | zero k S' => get k S' j
                  | one k S' => get k S' j
                  end
           end
  end.


Fixpoint set n (s:bin_seq n) (i:nat) (x:nat) : (bin_seq n) :=
  match s with
  | empty => empty
  | zero _ s' => match i with
                 | 0 => match x with
                        | 0 => [0] s'
                        | _ => [1] s'
                        end
                 | S j => [0] (set _ s' j x)
                 end
  | one _ s' => match i with
                | 0 => match x with
                       | 0 => [0] s'
                       | _ => [1] s'
                       end
                | S j => [1] (set _ s' j x)
                end
  end.


Lemma get_in : forall n:nat, forall x:bin_seq n, forall i,
               i < n -> get x i = 0 \/ get x i = 1.

Lemma get_in_dec : forall n:nat, forall x:bin_seq n, forall i,
                   i < n -> {get x i = 0} + {get x i = 1}.

Lemma get_le : forall n:nat, forall x:bin_seq n, forall i, n <= i -> get x i = 2.

Lemma get_lt : forall n:nat, forall x:bin_seq n, forall i j,
               j < n -> get x i < get x j -> get x i = 0 /\ get x j = 1.

Lemma get_is_lt_0 : forall n:nat, forall x:bin_seq n, forall i,
                    get x i = 0 -> i < n.

Lemma get_is_lt_1 : forall n:nat, forall x:bin_seq n, forall i,
                    get x i = 1 -> i < n.

Lemma get_lt_neq : forall n:nat, forall x:bin_seq n, forall i j,
                   get x i < get x j -> i <> j.

Lemma sign_get : forall n:nat, forall x:bin_seq n, forall i,
                 i < n -> sign (get x i) = get x i.

Lemma bin_seq_get : forall n:nat, forall x y:bin_seq n,
                   (forall i, get x i = get y i) -> x = y.

Lemma bin_seq_get_str : forall n:nat, forall x y:bin_seq n,
                       (forall i, i < n -> get x i = get y i) -> x = y.

Lemma get_set_1 : forall n:nat, forall x:(bin_seq n), forall i j,
                                i < n -> get (set x i j) i = sign j.

Lemma get_set_2 : forall n:nat, forall x:(bin_seq n), forall i j k,
                                i <> k -> get (set x i j) k = get x k.

Lemma set_get : forall n:nat, forall x:bin_seq n, forall i, set x i (get x i) = x.

Lemma set_get_strong : forall n:nat, forall x:bin_seq n, forall i,
                       i < n -> set x i (sign (get x i)) = x.

Lemma set_set_comm : forall n:nat, forall x:bin_seq n, forall i j,
                     i < n -> j < n -> i <> j ->
                     forall k k', set (set x i k) j k' = set (set x j k') i k.

Lemma set_set_del : forall n:nat, forall x:bin_seq n, forall i, i < n ->
                                  forall k k', set (set x i k) i k' = set x i k'.

Fixpoint zeros (n:nat) (s:bin_seq n) : nat :=
  match s with
  | empty => 0
  | [0] s' => S (zeros _ s')
  | [1] s' => zeros _ s'
  end.


Fixpoint ones (n:nat) (s:bin_seq n) : nat :=
  match s with
  | empty => 0
  | [0] s' => ones _ s'
  | [1] s' => S (ones _ s')
  end.


Lemma zeros_le : forall n, forall s:bin_seq n, zeros s <= n.

Lemma ones_le : forall n, forall s:bin_seq n, ones s <= n.

Lemma zeros_set_eq_0 : forall n, forall s:bin_seq n, forall j,
                       get s j = 0 -> zeros (set s j 0) = zeros s.

Lemma zeros_set_eq_1 : forall n, forall s:bin_seq n, forall j,
                       get s j = 1 -> zeros (set s j 1) = zeros s.

Lemma zeros_set_minus : forall n, forall s:bin_seq n, forall j,
                        get s j = 0 -> S (zeros (set s j 1)) = zeros s.

Lemma zeros_set_plus : forall n, forall s:bin_seq n, forall j,
                       get s j = 1 -> zeros (set s j 0) = S (zeros s).

Lemma zeros_gt : forall n s j, (get (n:=n) s j) = 0 -> zeros s > 0.

Fixpoint count_zeros (n:nat) (s:bin_seq n) (l:list nat) :=
  match l with
  | nil => 0
  | i :: l' => match eq_nat_dec (get s i) 0 with
               | left _ => S (count_zeros n s l')
               | right _ => count_zeros n s l'
               end
  end.

Lemma NoDup_count_zeros_set : forall n s l i x, i < n -> ~In i l ->
                              count_zeros n s l = count_zeros n (set s i x) l.

Lemma NoDup_count_zeros : forall l n s, NoDup l -> (forall x, In x l -> x < n) ->
                                        count_zeros n s l <= zeros s.

Lemma count_zeros_remove : forall n s l x, NoDup l -> In x l ->
                           count_zeros n s l =
                                 count_zeros n s (x :: nil) +
                                 count_zeros n s (remove eq_nat_dec x l).

Lemma count_zeros_eq : forall n s l l', Permutation l l' ->
                       count_zeros n s l = count_zeros n s l'.

Fixpoint zero_seq (n:nat) : bin_seq n :=
  match n with
  | O => empty
  | S j => [0] (zero_seq j)
  end.

Notation "[00]" := (zero_seq _).

Fixpoint all_ones (n:nat) (x:bin_seq n) : Prop :=
  match x with
  | [] => True
  | [0] _ => False
  | [1] y => all_ones _ y
  end.

Fixpoint sorted (n:nat) (x:bin_seq n) : Prop :=
  match x with
  | [] => True
  | [0] y => sorted _ y
  | [1] y => all_ones _ y
  end.


Lemma zero_seq_zeros : forall n, zeros (zero_seq n) = n.

Lemma zeros_all_ones : forall n, forall s:bin_seq n, zeros s = 0 -> all_ones s.

Lemma all_ones_char : forall n:nat, forall s:bin_seq n,
                      all_ones s -> forall j, get s j >= 1.

Lemma all_ones_sorted : forall n:nat, forall s:bin_seq n, all_ones s -> sorted s.

Lemma all_ones_zeros : forall n:nat, forall s:bin_seq n, all_ones s -> zeros s = 0.

Lemma all_ones_dec : forall n, forall s:bin_seq n, {all_ones s} + {~all_ones s}.

Lemma sorted_char : forall n:nat, forall s:bin_seq n,
                    (forall i j, i < j -> (get s i) <= (get s j)) -> sorted s.

Lemma sorted_lem : forall n:nat, forall s:bin_seq n, sorted s ->
                   (forall i j, i <= j -> (get s i) <= (get s j)).

Lemma sorted_dec : forall n, forall s:bin_seq n, {sorted s} + {~sorted s}.

Lemma all_sorted_dec : forall n, forall l:list (bin_seq n),
                                 {forall s, In s l -> sorted s} +
                                 {~forall s, In s l -> sorted s}.

Fixpoint all_bin_seqs (n:nat) : (list (bin_seq n)) :=
  match n with
  | O => empty :: nil
  | S k => (map (zero (n:=k)) (all_bin_seqs k)) ++ (map (one (n:=k)) (all_bin_seqs k))
  end.

Lemma all_bin_seqs_lemma : forall n:nat, forall s:bin_seq n, In s (all_bin_seqs n).

Theorem bin_seq_induction : forall n:nat, forall P:bin_seq n -> Prop,
  (forall s:bin_seq n, In s (all_bin_seqs n) -> P s) -> (forall s:bin_seq n, P s).

Lemma bin_seq_inversion_0 : forall s:bin_seq 0, s = [].

Lemma bin_seq_inversion_S : forall n, forall s:bin_seq (S n), exists s':bin_seq n,
                                      s = [0]s' \/ s = [1]s'.

Fixpoint drop (n:nat) (s:bin_seq (S n)) : bin_seq n :=
  match s with
  | [0]s' => s'
  | [1]s' => s'
  end.

Lemma drop_get : forall n s i, get (drop n s) i = get s (S i).

Lemma drop_lemma : forall n s, s = [0](drop n s) \/ s = [1](drop n s).

Lemma drop_0 : forall n s, get s 0 = 0 -> s = [0](drop n s).

Lemma drop_1 : forall n s, get s 0 = 1 -> s = [1](drop n s).


Lemma bin_seq_0_inv : forall n, forall s s':bin_seq n, [0]s = [0]s' -> s = s'.

Lemma bin_seq_1_inv : forall n, forall s s':bin_seq n, [1]s = [1]s' -> s = s'.

Fixpoint co_zero (n:nat) (s:bin_seq n) : bin_seq (S n) :=
  match s with
  | empty => [0][00]
  | [0]s' => [0] (co_zero _ s')
  | [1]s' => [1] (co_zero _ s')
  end.

Fixpoint co_one (n:nat) (s:bin_seq n) : bin_seq (S n) :=
  match s with
  | empty => [1][00]
  | [0]s' => [0] (co_one _ s')
  | [1]s' => [1] (co_one _ s')
  end.


Fixpoint all_co_bin_seqs (n:nat) : (list (bin_seq n)) :=
  match n with
  | O => empty :: nil
  | S k => (map (co_zero (n:=k)) (all_co_bin_seqs k)) ++ (map (co_one (n:=k)) (all_co_bin_seqs k))
  end.

Fixpoint bin_seq_last (n:nat) (s:bin_seq (S n)) : nat :=
  match s with
  | zero 0 _ => 0
  | one 0 _ => 1
  | zero (S k) s' => bin_seq_last _ s'
  | one (S k) s' => bin_seq_last _ s'
  end.

Fixpoint bin_seq_drop (n:nat) (s:bin_seq (S n)) : bin_seq n :=
  match s with
  | zero 0 _ => empty
  | one 0 _ => empty
  | zero (S k) s' => zero (bin_seq_drop k s')
  | one (S k) s' => one (bin_seq_drop k s')
  end.


Lemma bin_seq_alt_char : forall n, forall s:bin_seq (S n),
                         (bin_seq_last s = 0 -> s = co_zero (bin_seq_drop s))
                           /\ (bin_seq_last s = 1 -> s = co_one (bin_seq_drop s)).

Lemma bin_seq_alt_char_0 : forall n, forall s:bin_seq (S n),
                           bin_seq_last s = 0 -> s = co_zero (bin_seq_drop s).

Lemma bin_seq_alt_char_1 : forall n, forall s:bin_seq (S n),
                           bin_seq_last s = 1 -> s = co_one (bin_seq_drop s).

Lemma co_zero_last : forall n, forall s:bin_seq n, bin_seq_last (co_zero s) = 0.

Lemma co_one_last : forall n, forall s:bin_seq n, bin_seq_last (co_one s) = 1.

Lemma zeros_co_one : forall n, forall s:bin_seq n, zeros s = zeros (co_one s).

Lemma co_one_sort_in : forall n, forall s:bin_seq n, sorted s -> sorted (co_one s).

Lemma co_one_sort_out : forall n, forall s:bin_seq n,
                                  sorted (co_one s) -> sorted s.

Lemma bin_seq_last_get : forall n, forall s:bin_seq (S n),
                                   bin_seq_last s = get s n.

Lemma bin_seq_alt_char_all : forall n, forall s:bin_seq (S n),
                             s = co_zero (bin_seq_drop s)
                             \/ s = co_one (bin_seq_drop s).

Lemma all_co_bin_seqs_lemma : forall n:nat, forall s:bin_seq n,
                              In s (all_co_bin_seqs n).

Theorem bin_seq_alt_induction : forall n:nat, forall P:bin_seq n -> Prop,
       (forall s:bin_seq n, In s (all_co_bin_seqs n) -> P s) ->
        forall s:bin_seq n, P s.

Theorem bin_seq_eq_dec : forall n, forall s s':bin_seq n, {s=s'} + {s<>s'}.

Definition sort (n:nat) (s:bin_seq n) : bin_seq n.
Defined.


Lemma sort_zeros : forall n s, zeros (n:=n) s = zeros (sort s).

Lemma co_one_le : forall n, forall s:bin_seq n, forall i,
                  i < n -> (get s i) <= get (co_one s) n.

Lemma co_zero_get : forall n, forall s:bin_seq n, forall i,
                    i < n -> get s i = get (co_zero s) i.

Lemma co_one_get : forall n, forall s:bin_seq n, forall i,
                   i < n -> get s i = get (co_one s) i.

Lemma sorted_sort : forall n, forall s:bin_seq n, sorted (sort s).

Lemma sorted_idemp : forall n, forall s:bin_seq n, sorted s -> s = sort s.

Lemma sorting_char_lemma : forall n, forall s:bin_seq (S n),
                           zeros s < (S n) -> sorted s -> {x | s = co_one x}.

Theorem sorting_char : forall n, forall s s':bin_seq n,
                       zeros s = zeros s' -> sorted s' -> s' = sort s.

Hint Resolve sorted_sort : core.