val mem_elt_lt_hd (#a: eqtype) (#f: cmp a) (x: a) (s: mset a f {Cons? s})
    : Lemma (requires f x (fst (hd s)) /\ x <> fst (hd s)) (ensures mem x s == 0)
val mem_elt_lt_hd (#a: eqtype) (#f: cmp a) (x: a) (s: mset a f {Cons? s})
    : Lemma (requires f x (fst (hd s)) /\ x <> fst (hd s)) (ensures mem x s == 0)
let rec mem_elt_lt_hd (#a:eqtype) (#f:cmp a) (x:a) (s:mset a f{Cons? s})
  : Lemma
      (requires f x (fst (hd s)) /\ x <> fst (hd s))
      (ensures mem x s == 0)
  = match s with
    | [_] -> ()
    | _ -> mem_elt_lt_hd x (tl s)
module Zeta.MultiSet

open FStar.List.Tot


/// We represet a multiset with a sorted associative list
///   where the second component of each list element is the
///   cardinality of the first component in the set
///
/// The list is sorted on the first component of its elements


let rec sorted (#a:eqtype) (f:cmp a) (l:list (a & pos)) : Type0 =
  match l with
  | [] -> True
  | [_] -> True
  | (x, _)::(y, card_y)::tl ->
    f x y /\
    x =!= y /\
    sorted f ((y, card_y)::tl)

let mset a f = l:list (a & pos){sorted f l}


/// We will use this function, rather than pattern matching to get better implicit inference

let tl (#a:eqtype) (#f:cmp a) (s:mset a f{Cons? s}) : mset a f = tl s

let empty #_ #_ = []

let create #_ #_ x m = [x, m]

let rec mem #_ #_ x s =
  match s with
  | [] -> 0
  | (y, n)::_ -> if x = y then n else mem x (tl s)


let mem_empty (#a: eqtype) (f: cmp a) (x:a)
  : Lemma (mem x (empty #_ #f) == 0)
  = ()

/// We define an auxiliary add function that
///   maintains some invariants on the returned multiset,
///   so as to typecheck the body (the recursive call case)

private let rec add (#a:eqtype) (#f:cmp a) (s:mset a f) (x:a)
  : s':mset a f{
      Cons? s' /\
      (fst (hd s') == x \/ (Cons? s /\ fst (hd s') == fst (hd s)))}
  = match s with
    | [] -> [x, 1]
    | (y, n)::_ ->
      if x = y then (y, n + 1)::(tl s)
      else if f x y then (x, 1)::s
      else (y, n)::(add (tl s) x)

let add_elem = add

let rec seq2mset_aux (#a:eqtype) (#f:cmp a) (s:Seq.seq a)
  : Tot (mset a f) (decreases (Seq.length s))
  = if Seq.length s = 0 then empty
    else
      let ms = seq2mset_aux (Seq.tail s) in
      add_elem ms (Seq.index s 0)

let seq2mset = seq2mset_aux

let zero_length_implies_empty (#a:eqtype) (#f: cmp a) (s: Seq.seq a)
  : Lemma (ensures (Seq.length s = 0 ==> seq2mset #a #f s == empty))
  = ()

/// Again defining an auxiliary function to maintain some invariants on the return type

let rec union_aux (#a:eqtype) (#f:cmp a) (s1 s2:mset a f) :
  s:mset a f{
    ((Cons? s1 /\ Cons? s2) ==>
     (Cons? s /\ (let x1 = fst (hd s1) in
                 let x2 = fst (hd s2) in
                 if f x1 x2 then fst (hd s) == x1
                 else fst (hd s) == x2))) /\
    (Nil? s1 ==> s == s2) /\
    (Nil? s2 ==> s == s1)} =
  match s1, s2 with
  | [], _ -> s2
  | _, [] -> s1
  | (x1, n1)::_, (x2, n2)::_ ->
    if x1 = x2
    then (x1, n1 + n2)::(union_aux (tl s1) (tl s2))
    else if f x1 x2
    then (x1, n1)::(union_aux (tl s1) s2)
    else (x2, n2)::(union_aux s1 (tl s2))

let union = union_aux

let rec size #_ #_ s =
  match s with
  | [] -> 0
  | (_, n)::_ -> n + size (tl s)


/// A helper lemma saying that
///   an element that is less than (per f) the hd of the mset, is not in the mset
/
prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
Zeta.MultiSet.fst
x: a -> s: Zeta.MultiSet.mset a f {Cons? s}
  -> FStar.Pervasives.Lemma
      (requires
        f x (FStar.Pervasives.Native.fst (FStar.List.Tot.Base.hd s)) /\
        x <> FStar.Pervasives.Native.fst (FStar.List.Tot.Base.hd s))
      (ensures Zeta.MultiSet.mem x s == 0)
Prims.eqtype Zeta.MultiSet.cmp Zeta.MultiSet.mset Prims.b2t Prims.uu___is_Cons FStar.Pervasives.Native.tuple2 Prims.pos Prims.list Zeta.MultiSet.mem_elt_lt_hd Zeta.MultiSet.tl Prims.unit Prims.l_and FStar.Pervasives.Native.fst FStar.List.Tot.Base.hd Prims.op_disEquality Prims.squash Prims.eq2 Prims.int Zeta.MultiSet.mem Prims.Nil FStar.Pervasives.pattern
let rec mem_elt_lt_hd (#a: eqtype) (#f: cmp a) (x: a) (s: mset a f {Cons? s})
    : Lemma (requires f x (fst (hd s)) /\ x <> fst (hd s)) (ensures mem x s == 0) =
  
match s with
| [_] -> ()
| _ -> mem_elt_lt_hd x (tl s)