Merge pull request #3636 from FStarLang/gebner_rm_ghost_pull

Remove FStar.Ghost.Pull

ulib/FStar.Cardinality.Cantor.fst

@@ -18,7 +18,7 @@ let no_surj_powerset (a : Type) (f : a -> powerset a) : Lemma (~(is_surj f)) =
 
 let no_inj_powerset (a : Type) (f : powerset a -> a) : Lemma (~(is_inj f)) =
   let aux () : Lemma (requires is_inj f) (ensures False) =
-    let g : a -> powerset a = inverse_of_inj f (fun _ -> false) in
+    let g : a -> GTot (powerset a) = inverse_of_inj f (fun _ -> false) in
     no_surj_powerset a g
   in
   Classical.move_requires aux ()

ulib/FStar.Cardinality.Universes.fst

@@ -6,8 +6,8 @@ open FStar.Cardinality.Cantor
 (* This type is an injection of all powersets of Type u (i.e. Type u -> bool
 functions) into Type (u+1) *)
 noeq
-type type_powerset : (Type u#a -> bool) -> Type u#(max (a+1) b) =
-  | Mk : f:(Type u#a -> bool) -> type_powerset f
+type type_powerset : (Type u#a -> GTot bool) -> Type u#(max (a+1) b) =
+  | Mk : f:(Type u#a -> GTot bool) -> type_powerset f
 
 let aux_inj_type_powerset (f1 f2 : powerset (Type u#a))
   : Lemma (requires type_powerset u#a u#b f1 == type_powerset u#a u#b f2)

ulib/FStar.Functions.fst

@@ -1,21 +1,21 @@
 module FStar.Functions
 
-let inj_comp (#a #b #c : _) (f : a -> b) (g : b -> c)
+let inj_comp (#a #b #c : _) (f : a -> GTot b) (g : b -> GTot c)
   : Lemma (requires is_inj f /\ is_inj g)
           (ensures is_inj (fun x -> g (f x)))
   = ()
 
-let surj_comp (#a #b #c : _) (f : a -> b) (g : b -> c)
+let surj_comp (#a #b #c : _) (f : a -> GTot b) (g : b -> GTot c)
   : Lemma (requires is_surj f /\ is_surj g)
           (ensures is_surj (fun x -> g (f x)))
   = ()
 
-let bij_comp (#a #b #c : _) (f : a -> b) (g : b -> c) :
+let bij_comp (#a #b #c : _) (f : a -> GTot b) (g : b -> GTot c) :
  Lemma (requires is_bij f /\ is_bij g)
        (ensures is_bij (fun x -> g (f x)))
 = ()
 
-let lem_surj (#a #b : _) (f : a -> b) (y : b)
+let lem_surj (#a #b : _) (f : a -> GTot b) (y : b)
   : Lemma (requires is_surj f) (ensures in_image f y)
   = ()
 
@@ -30,11 +30,11 @@ let inverse_of_bij #a #b f =
     assert (g0 (f x) == x)
   in
   Classical.forall_intro aux;
-  Ghost.Pull.pull g0
+  g0
 
 let inverse_of_inj #a #b f def =
   (* f is a bijection into its image, obtain its inverse *)
-  let f' : a -> image_of f = fun x -> f x in
+  let f' : a -> GTot (image_of f) = fun x -> f x in
   let g_partial = inverse_of_bij #a #(image_of f) f' in
   (* extend the inverse to the full domain b *)
   let g : b -> GTot a =
@@ -43,4 +43,4 @@ let inverse_of_inj #a #b f def =
       then g_partial y
       else def
   in
-  Ghost.Pull.pull g
+  g

ulib/FStar.Functions.fsti

@@ -3,51 +3,51 @@ module FStar.Functions
 (* This module contains basic definitions and lemmas
 about functions and sets. *)
 
-let is_inj (#a #b : _) (f : a -> b) : prop =
+let is_inj (#a #b : _) (f : a -> GTot b) : prop =
   forall (x1 x2 : a). f x1 == f x2 ==> x1 == x2
 
-let is_surj (#a #b : _) (f : a -> b) : prop =
+let is_surj (#a #b : _) (f : a -> GTot b) : prop =
   forall (y:b). exists (x:a). f x == y
 
-let is_bij (#a #b : _) (f : a -> b) : prop =
+let is_bij (#a #b : _) (f : a -> GTot b) : prop =
   is_inj f /\ is_surj f
 
-let in_image (#a #b : _) (f : a -> b) (y : b) : prop =
+let in_image (#a #b : _) (f : a -> GTot b) (y : b) : prop =
   exists (x:a). f x == y
 
-let image_of (#a #b : _) (f : a -> b) : Type =
+let image_of (#a #b : _) (f : a -> GTot b) : Type =
   y:b{in_image f y}
 
 (* g inverses f *)
-let is_inverse_of (#a #b : _) (g : b -> a) (f : a -> b)  =
+let is_inverse_of (#a #b : _) (g : b -> GTot a) (f : a -> GTot b)  =
   forall (x:a). g (f x) == x
 
-let powerset (a:Type u#aa) : Type u#aa = a -> bool
+let powerset (a:Type u#aa) : Type u#aa = a -> GTot bool
 
-val inj_comp (#a #b #c : _) (f : a -> b) (g : b -> c)
+val inj_comp (#a #b #c : _) (f : a -> GTot b) (g : b -> GTot c)
   : Lemma (requires is_inj f /\ is_inj g)
           (ensures is_inj (fun x -> g (f x)))
 
-val surj_comp (#a #b #c : _) (f : a -> b) (g : b -> c)
+val surj_comp (#a #b #c : _) (f : a -> GTot b) (g : b -> GTot c)
   : Lemma (requires is_surj f /\ is_surj g)
           (ensures is_surj (fun x -> g (f x)))
 
-val bij_comp (#a #b #c : _) (f : a -> b) (g : b -> c) :
+val bij_comp (#a #b #c : _) (f : a -> GTot b) (g : b -> GTot c) :
  Lemma (requires is_bij f /\ is_bij g)
        (ensures is_bij (fun x -> g (f x)))
 
-val lem_surj (#a #b : _) (f : a -> b) (y : b)
+val lem_surj (#a #b : _) (f : a -> GTot b) (y : b)
   : Lemma (requires is_surj f) (ensures in_image f y)
 
 (* An bijection has a perfect inverse. *)
-val inverse_of_bij (#a #b : _) (f : a -> b)
-  : Ghost (b -> a)
+val inverse_of_bij (#a #b : _) (f : a -> GTot b)
+  : Ghost (b -> GTot a)
           (requires is_bij f)
           (ensures fun g -> is_bij g /\ g `is_inverse_of` f /\ f `is_inverse_of` g)
 
 (* An injective function has an inverse (as long as the domain is non-empty),
 and this inverse is surjective. *)
-val inverse_of_inj (#a #b : _) (f : a -> b{is_inj f}) (def : a)
-  : Ghost (b -> a)
+val inverse_of_inj (#a #b : _) (f : a -> GTot b{is_inj f}) (def : a)
+  : Ghost (b -> GTot a)
           (requires is_inj f)
           (ensures fun g -> is_surj g /\ g `is_inverse_of` f)