From cc243ad65f5ec970b2d4bfede9543c015a0aae01 Mon Sep 17 00:00:00 2001 From: John Li Date: Fri, 6 Aug 2021 10:25:18 -0700 Subject: [PATCH 1/3] Add FSet cherry-picked from 398283f2a7c3363b07cabc74739d273e493f459c --- examples/steel/arraystructs/FStar.FSet.fst | 66 ++++++++++++++++++++++ 1 file changed, 66 insertions(+) create mode 100644 examples/steel/arraystructs/FStar.FSet.fst diff --git a/examples/steel/arraystructs/FStar.FSet.fst b/examples/steel/arraystructs/FStar.FSet.fst new file mode 100644 index 00000000000..423204acbce --- /dev/null +++ b/examples/steel/arraystructs/FStar.FSet.fst @@ -0,0 +1,66 @@ +module FStar.FSet + +open FStar.List.Tot +open FStar.FunctionalExtensionality + +let has_elements (#a:eqtype) (f: a ^-> bool) (xs: list a): prop = + forall x. f x == x `mem` xs + +// Finite sets +let set (a:eqtype) = f:(a ^-> bool){exists xs. f `has_elements` xs} + +let set_as_list (s: set 'a): GTot (list 'a) = + FStar.IndefiniteDescription.indefinite_description_ghost (list 'a) + (has_elements 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 + +let emptyset #a: set a = intro_set (on_dom a (fun _ -> false)) [] + +let insert x (s: set 'a): set 'a = + intro_set (on_dom _ (fun x' -> x = x' || s x')) (x :: set_as_list s) + +let set_remove (#a:eqtype) x (s: a ^-> bool): (a ^-> bool) = + on_dom _ (fun x' -> not (x = x') && s x') + +let rec list_remove (#a:eqtype) x (xs: list a) = match xs with + | [] -> [] + | x' :: xs -> + if x = x' then list_remove x xs + else x' :: list_remove x xs + +let rec list_remove_spec (#a:eqtype) f x (xs: list a) +: Lemma + (requires f `has_elements` xs) + (ensures set_remove x f `has_elements` list_remove x xs) + (decreases xs) += match xs with + | [] -> () + | x' :: xs -> + let g: (a ^-> bool) = on_dom _ (fun x -> x `mem` xs) in + let f': (a ^-> bool) = on_dom _ (fun x'' -> x'' = x' || g x'') in + assert (f `feq` f'); + assert (g `has_elements` xs); + list_remove_spec g x xs; + assert (set_remove x g `has_elements` list_remove x xs) + +let remove x (s: set 'a): set 'a = + list_remove_spec s x (set_as_list s); + intro_set (set_remove x s) (list_remove x (set_as_list s)) + +let insert_remove x (s: set 'a) +: Lemma (requires s x == true) (ensures insert x (remove x s) == s) + [SMTPat (insert x (remove x s))] += assert (insert x (remove x s) `feq` s) + +let remove_insert x (s: set 'a) +: Lemma (requires s x == false) (ensures remove x (insert x s) == s) + [SMTPat (remove x (insert x s))] += assert (remove x (insert x s) `feq` s) + +let notin (s: set 'a) (x: 'a): prop = s x == false From 40de2ad02cc6e08ce078f5a395d9a25737a3fc0c Mon Sep 17 00:00:00 2001 From: John Li Date: Thu, 26 Aug 2021 12:56:18 -0700 Subject: [PATCH 2/3] move FStar.FSet into ulib cherry-picked from c9db2a8da8a5e1f4f3d1a9e6f206f0b7e980277a --- {examples/steel/arraystructs => ulib}/FStar.FSet.fst | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename {examples/steel/arraystructs => ulib}/FStar.FSet.fst (100%) diff --git a/examples/steel/arraystructs/FStar.FSet.fst b/ulib/FStar.FSet.fst similarity index 100% rename from examples/steel/arraystructs/FStar.FSet.fst rename to ulib/FStar.FSet.fst From fbf89cbbf3ac453a87a8e8a1e672235b9489d147 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Tue, 15 Mar 2022 14:21:39 -0700 Subject: [PATCH 3/3] Adding an interface file and renaming FSet to FiniteSet --- ulib/{FStar.FSet.fst => FStar.FiniteSet.fst} | 26 ++++++++-- ulib/FStar.FiniteSet.fsti | 52 ++++++++++++++++++++ 2 files changed, 74 insertions(+), 4 deletions(-) rename ulib/{FStar.FSet.fst => FStar.FiniteSet.fst} (72%) create mode 100755 ulib/FStar.FiniteSet.fsti diff --git a/ulib/FStar.FSet.fst b/ulib/FStar.FiniteSet.fst similarity index 72% rename from ulib/FStar.FSet.fst rename to ulib/FStar.FiniteSet.fst index 423204acbce..88ea20ad9c1 100644 --- a/ulib/FStar.FSet.fst +++ b/ulib/FStar.FiniteSet.fst @@ -1,4 +1,21 @@ -module FStar.FSet +(* + Copyright 2021 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. + + Author: John Li +*) +module FStar.FiniteSet open FStar.List.Tot open FStar.FunctionalExtensionality @@ -20,6 +37,8 @@ let intro_set (#a:eqtype) (f: a ^-> bool) (xs: Ghost.erased (list a)) = Classical.exists_intro (fun xs -> f `has_elements` xs) xs; f +let mem #a x s = s x + let emptyset #a: set a = intro_set (on_dom a (fun _ -> false)) [] let insert x (s: set 'a): set 'a = @@ -33,7 +52,7 @@ let rec list_remove (#a:eqtype) x (xs: list a) = match xs with | x' :: xs -> if x = x' then list_remove x xs else x' :: list_remove x xs - +module L = FStar.List.Tot let rec list_remove_spec (#a:eqtype) f x (xs: list a) : Lemma (requires f `has_elements` xs) @@ -42,7 +61,7 @@ let rec list_remove_spec (#a:eqtype) f x (xs: list a) = match xs with | [] -> () | x' :: xs -> - let g: (a ^-> bool) = on_dom _ (fun x -> x `mem` xs) in + let g: (a ^-> bool) = on_dom _ (fun x -> x `L.mem` xs) in let f': (a ^-> bool) = on_dom _ (fun x'' -> x'' = x' || g x'') in assert (f `feq` f'); assert (g `has_elements` xs); @@ -63,4 +82,3 @@ let remove_insert x (s: set 'a) [SMTPat (remove x (insert x s))] = assert (remove x (insert x s) `feq` s) -let notin (s: set 'a) (x: 'a): prop = s x == false diff --git a/ulib/FStar.FiniteSet.fsti b/ulib/FStar.FiniteSet.fsti new file mode 100755 index 00000000000..5f0737c27c8 --- /dev/null +++ b/ulib/FStar.FiniteSet.fsti @@ -0,0 +1,52 @@ +(* + Copyright 2021 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. + + Author: John Li, N. Swamy +*) +module FStar.FiniteSet + +val set (a:eqtype) + : Type0 + +val set_as_list (#a:eqtype) (s: set a) + : GTot (list a) + +val mem (#a:eqtype) (x:a) (s:set a) + : bool + +val emptyset (#a:eqtype) + : set a + +val insert (#a:eqtype) (x:a) (s: set a) + : set a + +val remove (#a:eqtype) (x:a) (s: set a) + : set a + +val insert_remove (#a:eqtype) (x:a) (s: set a) + : Lemma + (requires mem x s) + (ensures insert x (remove x s) == s) + [SMTPat (insert x (remove x s))] + +val remove_insert (#a:eqtype) (x:a) (s: set a) + : Lemma + (requires mem x s == false) + (ensures remove x (insert x s) == s) + [SMTPat (remove x (insert x s))] + +let notin (#a:eqtype) (x:a) (s: set a) + : bool + = not (mem x s)