Section RBag.


  Context {A:Type}.
  Context {eqdec:EqDec A eq}.

  Definition rbag := list A.

  Definition bunion := (@app A).


  Notation "X ≅ Y" := (ldeqA X Y) (at level 70) : rbag_scope.   Notation "b1 ⊎ b2" := (bunion b1 b2) (right associativity, at level 70) : rbag_scope.
  Global Instance bunion_proper : Proper (ldeqA ==> ldeqA ==> ldeqA) bunion.

  Lemma bunion_nil_r:
    ∀ (l:list A),
      (l ⊎ nil) = l.

  Lemma bunion_nil_l:
    ∀ (l:list A),
      (nil ⊎ l) = l.

  Lemma bunion_assoc:
    ∀ (l1 l2 l3:list A),
      ((l1 ⊎ l2) ⊎ l3) = (l1 ⊎ (l2 ⊎ l3)).

  Lemma bunion_comm (l1 l2: list A) :
    (l1 ⊎ l2) ≅ (l2 ⊎ l1).

  Lemma bunion_Forall P (l1 l2 : list A) :
    Forall P l1 → Forall P l2 → Forall P (bunion l1 l2).

  Fixpoint remove_one (x : A) (l : list A) : list A :=
    match l with
      | nil ⇒ nil
      | y::tl ⇒ if (x == y) then tl else y::(remove_one x tl)
    end.



  Global Instance remove_one_proper : Proper (eq ==> ldeqA ==> ldeqA) remove_one.

  Fixpoint bminus (d x:list A) {struct d} : list A :=
    match d with
      | nil ⇒ x
      | d1 :: d' ⇒ bminus d' (remove_one d1 x)
    end.

  Notation "b1 ⊖ b2" := (bminus b2 b1) (right associativity, at level 70) : rbag_scope.
  Lemma bminus_over_app_delta :
    ∀ (d1 d2:list A), ∀ (s:list A),
      ((s ⊖ d1) ⊖ d2) = (s ⊖ (d1 ++ d2)).

  Lemma bminus_to_nil:
    ∀ (d:list A), (nil ⊖ d) = nil.

  Lemma bminus_nil_to_self:
    ∀ (x:list A), (x ⊖ nil) = x.

  Global Instance bminus_proper_lem : Proper (eq ==> ldeqA ==> ldeqA) bminus.

  Lemma remove_one_comm:
    ∀ (x1 x2:A), ∀ x:list A,
      (remove_one x1 (remove_one x2 x)) = (remove_one x2 (remove_one x1 x)).

  Lemma remove_one_not_first:
    ∀ (x1 x2:A), ∀ s:list A,
      x1 ≠ x2 → (remove_one x1 (x2 :: s)) = x2 :: (remove_one x1 s).

  Global Instance bminus_proper : Proper (ldeqA ==> ldeqA ==> ldeqA) bminus.


  Lemma bminus_self : ∀ (x:list A), (x ⊖ x) = nil.

  Lemma bminus_naught : ∀ (x:list A), (x ⊖ nil) = x.


  Lemma bminus_cons :
    ∀ (a:A) (x y:list A), ((a :: x) ⊖ (a :: y)) = (x ⊖ y).


  Lemma bunion_bminus :
    ∀ (x y: list A), ((y ⊎ x) ⊖ y) = x.

  Lemma remove_one_consed:
    ∀ (x:list A), ∀ (a:A),
      (remove_one a (a :: x)) = x.

  Lemma remove_one_In (a x:A) (l1 l2:list A) :
    In x (bminus l1 (remove_one a l2)) → In x (bminus l1 l2).

  Lemma remove_one_sublist l a : sublist (remove_one a l) l.

  Lemma bminus_sublist (l1 l2:list A) :
    sublist (bminus l1 l2) l2.

  Lemma bminus_Forall (l1 l2:list A) p :
    Forall p l2 → Forall p (bminus l1 l2).

  Lemma bminus_NoDup (l1 l2:list A) : NoDup l2 → NoDup (bminus l1 l2).


  Lemma pick_an_a:
    ∀ (l:list A) (a:A),
      ({l':list A | a::l' ≅ l}) + {remove_one a l ≅ l}.


  Global Instance filter_proper : ∀ (p:A → bool), Proper (ldeqA ==> ldeqA) (filter p).

  Section MBag.

    Fixpoint mult (l:list A) (a:A) : nat :=
      match l with
        | nil ⇒ O
        | b :: l' ⇒ if (equiv_dec a b) then S (mult l' a) else (mult l' a)
      end.

    Definition mult_equiv l l' := (∀ a, mult l a = mult l' a).

    Notation "X ≅# Y" := (mult_equiv X Y) (at level 70) : rbag_scope.

    Global Instance mult_proper : Proper (ldeqA ==> eq ==> eq) mult.

    Lemma bags_equal_same_mult1:
      ∀ (l1 l2:list A),
        l1 ≅ l2 → l1 ≅# l2.

    Fixpoint groupby (l:list A) : list (A×nat)
      := match l with
           | nil ⇒ nil
           | (a::ls) ⇒ let rest := groupby ls in
                        match lookup equiv_dec rest a with
                          | None ⇒ (a,1)::rest
                          | Some x ⇒ update_first equiv_dec rest a (S x)
                        end
         end.

    Lemma groupby_noDup l : NoDup (domain (groupby l)).

    Fixpoint rep (a:A) n : list A :=
      match n with
        | 0 ⇒ nil
        | S m ⇒ a::(rep a m)
      end.

    Fixpoint smush (l:list (A×nat)) : list A
      := match l with
           | nil ⇒ nil
           | ((d,n)::ls) ⇒ rep d n ++ smush ls
         end.

    Global Instance smush_perm_proper : Proper ((@Permutation (A×nat)) ==> ldeqA) smush.

    Lemma smush1 a n x : smush ((a,S n)::x) = a::(smush ((a,n)::x)).

    Lemma smush_groupby l : Permutation (smush (groupby l)) l.

    Lemma pick_an_a_or_absent:
      ∀ (l:list A) (a:A),
        (mult l a = 0) ∨ (∃ l':list A, a::l' ≅ l).

    Lemma lookup_none_mult0 l d : lookup equiv_dec (groupby l) d = None → mult l d = 0.

    Lemma lookup_update_eq {B:Type }{l a} {n n':B} : lookup equiv_dec (update_first equiv_dec l a n') a = Some n → n = n'.

    Lemma groupby_domain {l a} : In a (domain (groupby l)) ↔ In a l.

    Lemma lookup_update_eq_in {B:Type}{l:list (A×B)} {a} {n:B} :
      In a (domain l) →
      lookup equiv_dec (update_first equiv_dec l a n) a = Some n.

    Lemma lookup_update_neq {B:Type }{l a a'} {n:B} : a≠a' → lookup equiv_dec (update_first equiv_dec l a n) a' = lookup equiv_dec l a'.

    Lemma groupby_mult_in {l d n} : In (d, n) (groupby l) → mult l d = n.

    Lemma groupby_mult_in_pos {l d n} : In (d, n) (groupby l) → n ≠ 0.

    Lemma mult_in_groupby {l d n} : mult l d = S n → In (d, S n) (groupby l).

    Lemma mult_nin_groupby {l d} : mult l d = 0 → ¬ In d (domain (groupby l)).

    Lemma bags_same_mult_has_equal :
      ∀ (l1 l2:list A),
        (∀ (a:A), (mult l1 a) = (mult l2 a)) → (l1 ≅ l2).

  End MBag.

  Definition bmin (l1 l2:list A) :=
    l1 ⊖ (l1 ⊖ l2).
  Notation "b1 min-b b2" := (bmin b1 b2) (right associativity, at level 70) : rbag_scope.

  Definition bmax (l1 l2:list A) :=
    l1 ⊎ (l2 ⊖ l1).
  Notation "b1 max-b b2" := (bmax b1 b2) (right associativity, at level 70) : rbag_scope.


  Definition bcount (l:list A) := length l.

  Fixpoint bdistinct (l:list A) :=
    match l with
      | nil ⇒ nil
      | x :: l' ⇒
        let dl' := bdistinct l' in
        match mult dl' x with
          | O ⇒ x :: dl'
          | _ ⇒ dl'
        end
    end.

  Lemma bdistinct_sublist l : sublist (bdistinct l) l.

  Lemma bdistinct_Forall {P} {l} :
      Forall P l → Forall P (bdistinct l).

  Lemma bdistinct_at_most_one:
    ∀ (l:list A), ∀ (x:A),
      (mult (bdistinct l) x) = 0 ∨ (mult (bdistinct l) x) = 1.


  Global Instance bdistinct_proper : Proper (ldeqA ==> ldeqA) bdistinct.

  Lemma bdistinct_exactly_zero:
    ∀ (l:list A), ∀ (x:A),
      (mult l x) = 0 → (mult (bdistinct l) x) = 0.

  Lemma bdistinct_exactly_zero_back:
    ∀ (l:list A), ∀ (x:A),
      (mult (bdistinct l) x) = 0 → (mult l x) = 0.

  Lemma bdistinct_exactly_one:
    ∀ (l:list A), ∀ (x:A),
      (mult l x) ≠ 0 → (mult (bdistinct l) x) = 1.

  Lemma bdistinct_exactly_one_back:
    ∀ (l:list A), ∀ (x:A),
      (mult (bdistinct l) x) = 1 → (mult l x) ≠ 0.

  Lemma bdistinct_exactly_one_back_diff:
    ∀ (l:list A), ∀ (x:A),
      (mult (bdistinct l) x) = 1 → (mult l x) ≥ 1.

  Lemma exist_or_zero:
    ∀ (s:list A), ∀ (x:A),
      (∃ (rs:list A), (x::rs) ≅ s) ∨ (mult s x) = 0.

  Lemma bdistinct_mult:
    ∀ (l:list A), ∀ (x:A),
      mult (bdistinct l) x = min (mult l x) 1.

  Lemma mult_pos_equiv_in:
    ∀ l,
    ∀ x,
      mult l x > 0 ↔ In x l.

  Lemma bdistinct_same_elemts:
    ∀ l,
    ∀ x,
      In x l → In x (bdistinct l).

  Lemma bdistinct_nil {l:list A} :
    bdistinct l = nil → l = nil.

  Lemma bdistinct_NoDup (l : list A) :
    NoDup (bdistinct l).

  Lemma NoDup_bdistinct {l:list A} :
    NoDup l → bdistinct l = l.

  Lemma bdistinct_idem {l:list A} :
    bdistinct (bdistinct l) = bdistinct l.

  Lemma bdistinct_equivlist (l : list A) :
    equivlist l (bdistinct l).


  Lemma fold_right_bdistinct (f : A → A → A)
        (assoc:∀ x y z : A, f x (f y z) = f (f x y) z)
        (comm:∀ x y : A, f x y = f y x)
        (idem:∀ x : A, f x x = x) (l:list A) (unit:A) :
    fold_right f unit l = fold_right f unit (bdistinct l).

  Lemma fold_right_equivlist (f : A → A → A)
  (assoc:∀ x y z : A, f x (f y z) = f (f x y) z)
  (comm:∀ x y : A, f x y = f y x)
  (idem:∀ x : A, f x x = x) (l1 l2:list A) (unit:A) :
    equivlist l1 l2 →
    fold_right f unit l1 = fold_right f unit l2.

  Lemma bunion_mult:
    ∀ (s t:list A), ∀ (x:A), mult (s ⊎ t) x = (mult s x) + (mult t x).

  Lemma remove_one_mult:
    ∀ (s:list A), ∀ (x:A), mult (remove_one x s) x = pred (mult s x).

  Lemma mult_on_remove:
    ∀ (s:list A), ∀ (a x:A),
      x ≠ a → mult (remove_one a s) x = mult s x.

  Lemma bminus_mult:
    ∀ (s t:list A), ∀ (x:A), mult (s ⊖ t) x = (mult s x) - (mult t x).

  Lemma bmin_on_nil_r:
    ∀ (s:list A), (s min-b nil) = nil.

  Lemma bmin_on_nil_l:
    ∀ (s:list A), (nil min-b s) = nil.

  Lemma bmax_on_nil_r:
    ∀ (s:list A), (s max-b nil) = s.

  Lemma bmax_on_nil_l:
    ∀ (s:list A), (nil max-b s) = s.

    Lemma bmin_Forall P (l1 l2 : list A) :
    Forall P l1 → Forall P l2 → Forall P (bmin l1 l2).

  Lemma bmax_Forall P (l1 l2 : list A) :
    Forall P l1 → Forall P l2 → Forall P (bmax l1 l2).

  Lemma minus_min:
    ∀ (n n0:nat), n0 - (n0 - n) = min n0 n.

  Lemma minus_max:
    ∀ (n n0:nat), n0 + (n - n0) = max n0 n.

  Lemma bmin_mult:
    ∀ (s t:list A), ∀ (x:A), (mult (s min-b t) x) = min (mult s x) (mult t x).

  Lemma bmax_mult:
    ∀ (s t:list A), ∀ (x:A), (mult (s max-b t) x) = max (mult s x) (mult t x).

  Lemma bmin_comm:
    ∀ (s t:list A), (s min-b t) ≅ (t min-b s).

  Lemma bmax_comm:
    ∀ (s t:list A), (s max-b t) ≅ (t max-b s).


  Lemma select_not_select:
    ∀ (p:A → bool), ∀ (s:list A),
      ((filter p s) ⊎ (filter (fun x ⇒ negb (p x)) s)) ≅ s.

  Lemma bdistinct_over_bunion_empty_r:
    ∀ (l1 l2:list A), ∀ (x:A),
      (mult (bdistinct (l1 ⊎ l2)) x = 0) → (mult (bdistinct l2) x = 0).

  Lemma bdistinct_over_bunion_empty_l:
    ∀ (l1 l2:list A), ∀ (x:A),
      (mult (bdistinct (l1 ⊎ l2)) x = 0) → (mult (bdistinct l1) x = 0).

  Lemma bdistinct_over_bunion_singleton2:
    ∀ (l1 l2:list A), ∀ (x:A),
      (mult (bdistinct l2) x = 0) → (mult (bdistinct l1) x = 1) → (mult (bdistinct (l1 ⊎ l2)) x = 1).

  Lemma bdistinct_over_bunion:
    ∀ (l1 l2:list A),
      (bdistinct (l1 ⊎ l2)) ≅ ((bdistinct l1) max-b (bdistinct l2)).

  Lemma bmin_zero:
    ∀ (l1 l2:list A), ∀ (x:A),
      mult (l1 min-b l2) x = 0 → (mult l1 x = 0) ∨ (mult l2 x = 0).

  Lemma bmin_zero_back:
    ∀ (l1 l2:list A), ∀ (x:A),
      (mult l1 x = 0) ∨ (mult l2 x = 0) → mult (l1 min-b l2) x = 0.

  Lemma bdistinct_over_bmin:
    ∀ (l2 l1:list A),
      (bdistinct (l1 min-b l2)) ≅ ((bdistinct l1) min-b (bdistinct l2)).

  Lemma split_select:
    ∀ (p:A → bool), ∀ (s:list A),
      ∃ (sp nsp:list A),
        (sp ⊎ nsp) ≅ s ∧
        (filter p sp) = sp ∧
        (filter p nsp) = nil.

  Lemma mult_filter_true l {p a} :
    p a = true →
    mult (filter p l) a = mult l a.

  Lemma mult_filter_false l {p a} :
    p a = false →
    mult (filter p l) a = 0.


  Definition bminus_delta2 (Q dQm dQp:list A) :=
    (Q min-b dQm) ⊖ dQp.

  Definition bplus_delta2 (Q dQm dQp:list A) :=
    dQp ⊖ (Q min-b dQm).

  Definition apply_deltas (Q dQm dQp: list A) :=
    (Q ⊖ dQm) ⊎ dQp.

  Lemma theorem2_a:
    ∀ (Q dQm dQp: list A),
      (apply_deltas Q dQm dQp) ≅
      (apply_deltas Q (bminus_delta2 Q dQm dQp) (bplus_delta2 Q dQm dQp)).

  Lemma theorem2_b:
    ∀ (Q dQm dQp: list A),
      ((bminus_delta2 Q dQm dQp) ⊖ Q) ≅ nil.

  Lemma theorem2_c:
    ∀ (Q dQm dQp: list A),
      ((bminus_delta2 Q dQm dQp) min-b (bplus_delta2 Q dQm dQp)) ≅ nil.

  Lemma remove_one_bminus r s a:
    ((remove_one a s) ⊖ r) = (s ⊖ (a :: r)).

  Lemma remove_bminus_comm r s a:
    ((remove_one a s) ⊖ r) = (remove_one a (s ⊖ r)).

  Lemma filter_remove_one_false s {p a} : p a = false →
      (filter p (remove_one a s)) = filter p s.

  Lemma filter_remove_one s {p a} :
      (filter p (remove_one a s)) = remove_one a (filter p s).

  Lemma bunion_filter (s:list A) (ds:list A) (p:A → bool):
      (filter p (s ⊎ ds)) = ((filter p s) ⊎ (filter p ds)).

  Lemma bminus_filter (p:A → bool) (s ds:list A) : (filter p (s ⊖ ds)) = ((filter p s) ⊖ (filter p ds)).

End RBag.

Section NumMinMax.

  Definition bnummin (l:list Z) :=
    match l with
    | nil ⇒ 0
    | x0 :: l' ⇒
      fold_right (fun x y ⇒ Zmin x y) x0 l'
    end.

  Definition bnummax (l:list Z) :=
    match l with
    | nil ⇒ 0
    | x0 :: l' ⇒
      fold_right (fun x y ⇒ Zmax x y) x0 l'
    end.

End NumMinMax.