val difference (#a: eqtype) (s1: set a) (s2: set a)
  : set a
let difference (#a: eqtype) (s1: set a) (s2: set a) : set a =
  intro_set (on_dom a (fun x -> s1 x && not (s2 x))) (difference_lists (set_as_list s1) (set_as_list s2))
val difference (#a: eqtype) (s1: set a) (s2: set a)
  : set a
let difference (#a: eqtype) (s1 s2: set a) : set a =
intro_set (on_dom a (fun x -> s1 x && not (s2 x)))
  (difference_lists (set_as_list s1) (set_as_list s2))
FStar.FiniteSet.Base.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.IndefiniteDescription.fsti.checked FStar.Ghost.fsti.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
FStar.FiniteSet.Base.fst
Prims.eqtype FStar.FiniteSet.Base.set FStar.FiniteSet.Base.intro_set FStar.FunctionalExtensionality.on_dom Prims.bool Prims.op_AmpAmp Prims.op_Negation FStar.Ghost.hide Prims.list FStar.FiniteSet.Base.difference_lists FStar.FiniteSet.Base.set_as_list
(*
   Copyright 2008-2021 John Li, Jay Lorch, Rustan Leino, Alex Summers,
   Dan Rosen, Nikhil Swamy, Microsoft Research, and contributors to
   the Dafny Project

   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.

   Includes material from the Dafny project
   (https://github.com/dafny-lang/dafny) which carries this license
   information:

     Created 9 February 2008 by Rustan Leino.
     Converted to Boogie 2 on 28 June 2008.
     Edited sequence axioms 20 October 2009 by Alex Summers.
     Modified 2014 by Dan Rosen.
     Copyright (c) 2008-2014, Microsoft.
     Copyright by the contributors to the Dafny Project
     SPDX-License-Identifier: MIT
*)

(**
This module declares a type and functions used for modeling
finite sets as they're modeled in Dafny.

@summary Type and functions for modeling finite sets
*)
module FStar.FiniteSet.Base

module FLT = FStar.List.Tot
open FStar.FunctionalExtensionality

let has_elements (#a: eqtype) (f: a ^-> bool) (xs: list a): prop =
  forall x. f x == x `FLT.mem` xs

// Finite sets
type set (a: eqtype) = f:(a ^-> bool){exists xs. f `has_elements` xs}

/// We represent the Dafny function [] on sets with `mem`:

let mem (#a: eqtype) (x: a) (s: set a) : bool =
  s x

/// We represent the Dafny function `Set#Card` with `cardinality`:
///
/// function Set#Card<T>(Set T): int;

let rec remove_repeats (#a: eqtype) (xs: list a)
: (ys: list a{list_nonrepeating ys /\ (forall y. FLT.mem y ys <==> FLT.mem y xs)}) =
  match xs with
  | [] -> []
  | hd :: tl -> let tl' = remove_repeats tl in if FLT.mem hd tl then tl' else hd :: tl'

let set_as_list (#a: eqtype) (s: set a): GTot (xs: list a{list_nonrepeating xs /\ (forall x. FLT.mem x xs = mem x s)}) =
  remove_repeats (FStar.IndefiniteDescription.indefinite_description_ghost (list a) (fun xs -> forall x. FLT.mem x xs = mem x s))

[@"opaque_to_smt"]
let cardinality (#a: eqtype) (s: set a) : GTot nat =
  FLT.length (set_as_list s)

let intro_set (#a: eqtype) (f: a ^-> bool) (xs: Ghost.erased (list a))
: Pure (set a)
    (requires f `has_elements` xs)
    (ensures fun _ -> True)
= Classical.exists_intro (fun xs -> f `has_elements` xs) xs;
  f 

/// We represent the Dafny function `Set#Empty` with `empty`:

let emptyset (#a: eqtype): set a = intro_set (on_dom a (fun _ -> false)) []

/// We represent the Dafny function `Set#UnionOne` with `insert`:
///
/// function Set#UnionOne<T>(Set T, T): Set T;

let insert (#a: eqtype) (x: a) (s: set a): set a =
  intro_set (on_dom _ (fun x' -> x = x' || s x')) (x :: set_as_list s)

/// We represent the Dafny function `Set#Singleton` with `singleton`:
///
/// function Set#Singleton<T>(T): Set T;

let singleton (#a: eqtype) (x: a) : set a =
  insert x emptyset

/// We represent the Dafny function `Set#Union` with `union`:
///
/// function Set#Union<T>(Set T, Set T): Set T;

let rec union_lists (#a: eqtype) (xs: list a) (ys: list a) : (zs: list a{forall z. FLT.mem z zs <==> FLT.mem z xs \/ FLT.mem z ys}) =
  match xs with
  | [] -> ys
  | hd :: tl -> hd :: union_lists tl ys

let union (#a: eqtype) (s1: set a) (s2: set a) : (set a) =
  intro_set (on_dom a (fun x -> s1 x || s2 x)) (union_lists (set_as_list s1) (set_as_list s2))

/// We represent the Dafny function `Set#Intersection` with `intersection`:
///
/// function Set#Intersection<T>(Set T, Set T): Set T;

let rec intersect_lists (#a: eqtype) (xs: list a) (ys: list a)
: (zs: list a{forall z. FLT.mem z zs <==> FLT.mem z xs /\ FLT.mem z ys}) =
  match xs with
  | [] -> []
  | hd :: tl -> let zs' = intersect_lists tl ys in if FLT.mem hd ys then hd :: zs' else zs'

let intersection (#a: eqtype) (s1: set a) (s2: set a) : set a =
  intro_set (on_dom a (fun x -> s1 x && s2 x)) (intersect_lists (set_as_list s1) (set_as_list s2))

/// We represent the Dafny function `Set#Difference` with `difference`:
///
/// function Set#Difference<T>(Set T, Set T): Set T;

let rec difference_lists (#a: eqtype) (xs: list a) (ys: list a)
: (zs: list a{forall z. FLT.mem z zs <==> FLT.mem z xs /\ ~(FLT.mem z ys)}) =
  match xs with
  | [] -> []
  | hd :: tl -> let zs' = difference_lists tl ys in if FLT.mem hd ys then zs' else hd :: zs'
val difference (#a: eqtype) (s1: set a) (s2: set a)
  : set a
s1: FStar.FiniteSet.Base.set a -> s2: FStar.FiniteSet.Base.set a -> FStar.FiniteSet.Base.set a