val tail_is_subset (#a #f: _) (s: ordset a f {size' s > 0}) : Lemma ((Cons?.tl s) `subset'` s)
let tail_is_subset #a #f (s:ordset a f{size' s > 0})
  : Lemma (Cons?.tl s `subset'` s) = 
  simple_induction (fun (s:ordset a f) -> size' s=0 || subset' (Cons?.tl s) s) s
val tail_is_subset (#a #f: _) (s: ordset a f {size' s > 0}) : Lemma ((Cons?.tl s) `subset'` s)
let tail_is_subset #a #f (s: ordset a f {size' s > 0}) : Lemma ((Cons?.tl s) `subset'` s) =
simple_induction (fun (s: ordset a f) -> size' s = 0 || subset' (Cons?.tl s) s) s
FStar.OrdSet.fst.checked
prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Base.fst.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
FStar.OrdSet.fst
Prims.eqtype FStar.OrdSet.cmp FStar.OrdSet.ordset Prims.b2t Prims.op_GreaterThan FStar.OrdSet.size' FStar.OrdSet.simple_induction Prims.op_BarBar Prims.op_Equality Prims.int FStar.OrdSet.subset' Prims.__proj__Cons__item__tl Prims.unit Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern
(*
   Copyright 2008-2022 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.OrdSet

type ordset a f = l:(list a){sorted f l}

let hasEq_ordset _ _ = ()
    
let rec simple_induction #t #f (p: ordset t f -> Type0) (x: ordset t f)
  : Lemma (requires p [] /\ (forall (l: ordset t f{Cons? l}). p (Cons?.tl l) ==> p l))
          (ensures p x) = match x with
  | [] -> ()
  | ph::pt -> simple_induction p pt;
            assert (p (Cons?.tl (ph::pt)))
  
let rec base_induction #t #f (p: ordset t f -> Type0) (x: ordset t f)
  : Lemma (requires (forall (l: ordset t f{List.Tot.Base.length l < 2}). p l) 
                  /\ (forall (l: ordset t f{Cons? l}). p (Cons?.tl l) ==> p l))
          (ensures p x) 
          (decreases List.Tot.Base.length x) = 
  if List.Tot.Base.length x < 2 then ()
  else match x with
  | ph::pt -> base_induction p pt;
            assert (p (Cons?.tl (ph::pt)))
            
let empty #_ #_ = []

let tail #a #f s = Cons?.tl s <: ordset a f 
let head #_ #_ s = Cons?.hd s

let mem #_ #_ x s = List.Tot.mem x s
 
(* In case snoc-based List implementation is optimized, we use library ones,
   but we additionally supply them with relevant postconditions that come 
   from s being an ordset. *)
let rec last_direct #a #f (s: ordset a f{s <> empty}) 
  : (x:a{mem x s /\ (forall (z:a{mem z s}). f z x)}) 
  = match s with
  | [x] -> x  
  | h::g::t -> last_direct (tail s)

let last_lib #a #f (s: ordset a f{s <> empty}) 
  = snd (List.Tot.Base.unsnoc s)

let last_eq #a #f (s: ordset a f{s <> empty}) 
  : Lemma (last_direct s = last_lib s) = simple_induction 
    (fun p -> if p<>[] then last_direct #a #f p = last_lib p else true) s

let last #a #f s = last_eq s; last_lib s

let rec liat_direct #a #f (s: ordset a f{s <> empty}) : (l:ordset a f{
    (forall x. mem x l = (mem x s && (x <> last s))) /\
    (if tail s <> empty then head s = head l else true)
  }) =  
  match s with
  | [x] -> []
  | h::g::t -> h::(liat_direct #a #f (g::t))

let liat_lib #a #f (s: ordset a f{s <> empty}) = fst (List.Tot.Base.unsnoc s)

let liat_eq #a #f (s:ordset a f {s<>empty})
  : Lemma (liat_direct s = liat_lib s) = simple_induction
    (fun p -> if p<>[] then liat_direct p = liat_lib p else true) s

let liat #a #f s = liat_eq s; liat_lib s
 
let unsnoc #a #f s = 
  liat_eq s;
  last_eq s;
  let l = List.Tot.Base.unsnoc s in
  (fst l, snd l)

let as_list (#a:eqtype) (#f:cmp a) (s:ordset a f) : Tot (l:list a{sorted f l}) = s

val insert': #a:eqtype -> #f:cmp a -> x:a -> s:ordset a f
             -> Tot (l:(ordset a f){let s = as_list s in let l = as_list l in
	                           (Cons? l /\
                                    (head #a #f l = x \/
                                    (Cons? s /\ head #a #f l = head #a #f s)))})
let rec insert' #_ #f x s =
  match s with
  | []     -> [x]
  | hd::tl ->
    if x = hd then hd::tl
    else if f x hd then x::hd::tl
    else hd::(insert' #_ #f x tl)

let rec distinct' #a f l : Tot (ordset a f) = 
  match l with 
  | []  -> []
  | x::t -> insert' x (distinct' f t)

let rec insert_mem (#a:eqtype) #f (x:a) (s:ordset a f) 
  : Lemma (mem x (insert' x s)) 
  = if s<>empty then insert_mem #a #f x (tail s)

let insert_sub (#a:eqtype) #f x (s:ordset a f) test
  : Lemma (mem test (insert' x s) = (mem test s || test = x)) = 
  simple_induction (fun p -> mem test (insert' x p) = (mem test p || test = x)) s

let rec distinct_props #a (f:cmp a) (l: list a) 
  : Lemma (forall x. (mem x (distinct' f l) = List.Tot.Base.mem x l)) = 
  match l with 
  | [] -> ()
  | x::t -> distinct_props f t;
          Classical.forall_intro (insert_sub x (distinct' f t))

let distinct #a f l = distinct_props f l; distinct' f l

let rec union #_ #_ s1 s2 = match s1 with
  | []     -> s2
  | hd::tl -> union tl (insert' hd s2) 

val remove': #a:eqtype -> #f:cmp a -> x:a -> s:ordset a f
             -> Tot (l:(ordset a f){ ((Nil? s ==> Nil? l) /\
                                    (Cons? s ==> head s = x ==> l = tail s) /\
                                    (Cons? s ==> head s =!= x ==> (Cons? l /\ head l = Cons?.hd s)))})
                                    
let rec remove' #a #f x s = match s with
  | [] -> []
  | hd::(tl: ordset a f) ->
    if x = hd then tl
    else hd::(remove' x tl)

let size' (#a:eqtype) (#f:cmp a) (s:ordset a f) = List.Tot.length s

let liat_length #a #f (s:ordset a f{s<>empty}) : Lemma (size' (liat s) = ((size' s) - 1)) 
  = simple_induction (fun p -> if p<>empty then size' (liat p) = ((size' p)-1) else true) s

let rec not_mem_aux (#a:eqtype) (#f:cmp a) (x:a) (s:ordset a f)
  : Lemma (requires (size' s > 0) && (head s <> x) && (f x (head s)))
          (ensures not (mem x s)) = 
  if tail s <> [] then not_mem_aux x (tail s)

let rec subset' #a #f (s1 s2: ordset a f) = match s1, s2 with
  | [], _          -> true
  | hd::tl, hd'::tl' -> if f hd hd' && hd = hd' then subset' #a #f tl tl'
                     else if f hd hd' && not (hd = hd') then false
                     else subset' #a #f s1 tl'
  | _, _           -> false
  
let tail_is_subset #a #f (s:ordset a f{size' s > 0})
val tail_is_subset (#a #f: _) (s: ordset a f {size' s > 0}) : Lemma ((Cons?.tl s) `subset'` s)
s: FStar.OrdSet.ordset a f {FStar.OrdSet.size' s > 0}
  -> FStar.Pervasives.Lemma (ensures FStar.OrdSet.subset' (Cons?.tl s) s)