seq-based set lemmas

Sandbox.fst

module Sandbox
 
#set-options "--ifuel 0 --fuel 0 --z3rlimit 1"


open FStar.Seq
open FStar.Seq.Base


//type vertex_id = UInt32.t


let rec is_set (l: seq UInt32.t)
                  : Tot (bool)
            (decreases length l)= 
if length l = 0 then true else not(mem (head l) (tail l)) && is_set (tail l)

let uint = UInt32.t 

type uint_set = s:seq UInt32.t { is_set s }

#set-options "--fuel 1"
let tail_is_set (s: uint_set) 
  : Lemma (requires length s > 0)
          (ensures is_set (tail s))
          (decreases length s) = ()      

let rec snoc_is_set_lemma (s: uint_set) (x: uint)
  : Lemma (requires ~(mem x s))
          (ensures is_set (snoc s x)) 
          (decreases length s) = 
  if length s = 0 then lemma_tl x s 
  else begin
    Seq.Properties.lemma_mem_snoc (tail s) x;    
    tail_is_set s;
    snoc_is_set_lemma (tail s) x;
    if length (tail s) > 0 then Seq.Properties.lemma_tail_snoc s x;       
    assert (is_set (tail (snoc s x)))
  end

let rec set_union (a b: uint_set)  
  : Tot (l: uint_set{forall x. Seq.mem x l <==> Seq.mem x a \/ Seq.mem x b}) 
        (decreases (length a)) = 
  if length a = 0 then b
  else
  (
    if mem (head a) b then set_union (tail a) b
    else
    (
      let u = set_union (tail a) b in
      if length u = 0 then (Seq.create 1 (head a)) 
      else
      (
        //lemma_tail_snoc (set_union  (tail a) b) (head a);
        snoc_is_set_lemma (set_union  (tail a) b) (head a);
        lemma_mem_snoc (set_union  (tail a) b) (head a);
        snoc (set_union (tail a) b) (head a))
      )
    )

let rec set_subtract (a: uint_set) 
                     (b: seq uint) 
  : Tot (r: uint_set { (forall x. (x `mem` r) <==> ((x `mem` a) && (not (x `mem` b)))) }) 
        (decreases (length a))=  
  if length a = 0 then empty 
  else if mem (head a) b then set_subtract (tail a) b
  else let u = tail a `set_subtract` b in
    lemma_tl (head a) u;    
    if mem (head a) u then u
    else cons (head a) u 

let direct_union (a b c: uint_set)
  : Pure (uint_set) (requires True)
                    (ensures fun r -> (forall x. (mem x r == (mem x a && (not (mem x b || mem x c))))))
  = a `set_subtract` (b `set_union` c)

let wat (a b c: uint_set)
  : Lemma (direct_union a b c == a `set_subtract` (set_union b c)) = ()