From e97fd5e3c425a531b0eda1e4818f3f0977ecdfd3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Sat, 13 Apr 2024 09:22:39 -0700
Subject: [PATCH 1/4] Add a proof the cardinality of Type(u+1) is greater than
 Type(u)

This also adds an FStar.Functions module with some reusable definitions
about functions and sets. It also splits the proof between the
set-theoretic results on functions (due to Cantor, potentially useful
without referring to universes) and the result about universes which
uses an indexed inductive type.
---
 ulib/FStar.Cardinality.Cantor.fst     | 24 +++++++++++++++++
 ulib/FStar.Cardinality.Cantor.fsti    | 13 +++++++++
 ulib/FStar.Cardinality.Universes.fst  | 38 +++++++++++++++++++++++++++
 ulib/FStar.Cardinality.Universes.fsti |  8 ++++++
 ulib/FStar.Functions.fst              | 29 ++++++++++++++++++++
 ulib/FStar.Functions.fsti             | 34 ++++++++++++++++++++++++
 6 files changed, 146 insertions(+)
 create mode 100644 ulib/FStar.Cardinality.Cantor.fst
 create mode 100644 ulib/FStar.Cardinality.Cantor.fsti
 create mode 100644 ulib/FStar.Cardinality.Universes.fst
 create mode 100644 ulib/FStar.Cardinality.Universes.fsti
 create mode 100644 ulib/FStar.Functions.fst
 create mode 100644 ulib/FStar.Functions.fsti

diff --git a/ulib/FStar.Cardinality.Cantor.fst b/ulib/FStar.Cardinality.Cantor.fst
new file mode 100644
index 00000000000..4f2ee440157
--- /dev/null
+++ b/ulib/FStar.Cardinality.Cantor.fst
@@ -0,0 +1,24 @@
+module FStar.Cardinality.Cantor
+
+open FStar.Functions
+
+let no_surj_powerset (a : Type) (f : a -> powerset a) : Lemma (~(is_surj f)) =
+  let aux () : Lemma (requires is_surj f) (ensures False) =
+    (* Cantor's proof: given a supposed surjective f,
+    we define a set s that cannot be in the image of f. Namely,
+    the set of x:a such that x is not in f(x).  *)
+    let s : powerset a = fun x -> not (f x x) in
+    let aux (x : a) : Lemma (requires f x == s) (ensures False) =
+      // We have f x == s, which means that f x x == not (f x x), contradiction
+      assert (f x x) // this triggers the SMT appropriately
+    in
+    Classical.forall_intro (Classical.move_requires aux)
+  in
+  Classical.move_requires aux ()
+
+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
+    no_surj_powerset a g
+  in
+  Classical.move_requires aux ()
diff --git a/ulib/FStar.Cardinality.Cantor.fsti b/ulib/FStar.Cardinality.Cantor.fsti
new file mode 100644
index 00000000000..af749e8bedc
--- /dev/null
+++ b/ulib/FStar.Cardinality.Cantor.fsti
@@ -0,0 +1,13 @@
+module FStar.Cardinality.Cantor
+
+(* Cantor's theorem: there is no surjection from a set to its
+powerset, and therefore also no injection from the powerset to the
+set. *)
+
+open FStar.Functions
+
+val no_surj_powerset (a : Type) (f : a -> powerset a)
+  : Lemma (~(is_surj f))
+
+val no_inj_powerset (a : Type) (f : powerset a -> a)
+  : Lemma (~(is_inj f))
diff --git a/ulib/FStar.Cardinality.Universes.fst b/ulib/FStar.Cardinality.Universes.fst
new file mode 100644
index 00000000000..e37e2a2cc51
--- /dev/null
+++ b/ulib/FStar.Cardinality.Universes.fst
@@ -0,0 +1,38 @@
+module FStar.Cardinality.Universes
+
+open FStar.Functions
+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#(a+1) =
+  | Mk : f:(Type u#a -> bool) -> type_powerset f
+
+let aux_inj_type_powerset (f1 f2 : powerset (Type u#a))
+  : Lemma (requires type_powerset f1 == type_powerset f2)
+          (ensures f1 == f2)
+=
+  assert (type_powerset f1 == type_powerset f2);
+  let xx1 : type_powerset f1 = Mk f1 in
+  let xx2 : type_powerset f2 = coerce_eq () xx1 in
+  assert (xx1 === xx2);
+  assert (f1 == f2)
+  
+let inj_type_powerset () : Lemma (is_inj type_powerset) =
+  Classical.forall_intro_2 (fun f1 -> Classical.move_requires (aux_inj_type_powerset f1))
+ 
+ (* The general structure of this proof is:
+   1- We know there is an injection of powerset(Type(u)) into Type(u+1) (see type_powerset above)
+   2- We know there is NO injection from powerset(Type(u)) into Type(u) (see no_inj_powerset)
+   3- Therefore, there cannot be an injection from Type(u+1) into Type(u), otherwise we would
+      compose it with the first injection and obtain the second impossible injection.
+*)
+let no_inj_universes (f : Type u#(a+1) -> Type u#a) : Lemma (~(is_inj f)) =
+  let aux () : Lemma (requires is_inj f) (ensures False) =
+    let comp : powerset (Type u#a) -> Type u#a = fun x -> f (type_powerset x) in
+    inj_type_powerset ();
+    inj_comp type_powerset f;
+    no_inj_powerset _ comp
+  in
+  Classical.move_requires aux ()
diff --git a/ulib/FStar.Cardinality.Universes.fsti b/ulib/FStar.Cardinality.Universes.fsti
new file mode 100644
index 00000000000..7f267802c8c
--- /dev/null
+++ b/ulib/FStar.Cardinality.Universes.fsti
@@ -0,0 +1,8 @@
+module FStar.Cardinality.Universes
+
+open FStar.Functions
+open FStar.Cardinality.Cantor
+
+(* Prove that there can be no injection from Type (u+1) into Type u *)
+val no_inj_universes (f : Type u#(a+1) -> Type u#a)
+  : Lemma (~(is_inj f))
diff --git a/ulib/FStar.Functions.fst b/ulib/FStar.Functions.fst
new file mode 100644
index 00000000000..f2b866904a7
--- /dev/null
+++ b/ulib/FStar.Functions.fst
@@ -0,0 +1,29 @@
+module FStar.Functions
+
+let inj_comp (#a #b #c : _) (f : a -> b) (g : b -> 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)
+  : Lemma (requires is_surj f /\ is_surj g)
+          (ensures is_surj (fun x -> g (f x)))
+  = ()
+
+let lem_surj (#a #b : _) (f : a -> b) (y : b)
+  : Lemma (requires is_surj f) (ensures in_image f y)
+  = ()
+
+let inverse_of_inj (#a #b : _) (f : a -> b{is_inj f}) (def : a) : GTot (g : (b -> a){is_surj g}) =
+  (* Construct the inverse from indefinite description + choice. *)
+  let g0 (y:b) : GTot (x:a{in_image f y ==> f x == y})  =
+    FStar.IndefiniteDescription.indefinite_description_tot a
+      (fun (x:a) -> (in_image f y ==> f x == y))
+  in
+  let g : (b -> a) = Ghost.Pull.pull g0 in
+  (* Prove it's surjective *)
+  let aux (x:a) : Lemma (exists (y:b). g y == x) =
+    assert (in_image f (f x))
+  in
+  Classical.forall_intro aux;
+  g
diff --git a/ulib/FStar.Functions.fsti b/ulib/FStar.Functions.fsti
new file mode 100644
index 00000000000..365df75b9a7
--- /dev/null
+++ b/ulib/FStar.Functions.fsti
@@ -0,0 +1,34 @@
+module FStar.Functions
+
+(* This module contains basic definitions and lemmas
+about functions and sets. *)
+
+let is_inj (#a #b : _) (f : a -> b) : prop =
+  forall (x1 x2 : a). f x1 == f x2 ==> x1 == x2
+
+let is_surj (#a #b : _) (f : a -> b) : prop =
+  forall (y:b). exists (x:a). f x == y
+
+let in_image (#a #b : _) (f : a -> b) (y : b) : prop =
+  exists (x:a). f x == y
+
+let image_of (#a #b : _) (f : a -> b) : Type =
+  y:b{in_image f y}
+
+let powerset (a:Type u#aa) : Type u#aa = a -> bool
+
+val inj_comp (#a #b #c : _) (f : a -> b) (g : b -> 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)
+  : Lemma (requires is_surj f /\ is_surj g)
+          (ensures is_surj (fun x -> g (f x)))
+
+val lem_surj (#a #b : _) (f : a -> b) (y : b)
+  : Lemma (requires is_surj f) (ensures in_image f y)
+
+(* 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)
+  : GTot (g : (b -> a){is_surj g})

From 6115829fbc150c8a487eea944b7da857f3260658 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Sat, 13 Apr 2024 09:32:00 -0700
Subject: [PATCH 2/4] snap

---
 ocaml/fstar-lib/generated/FStar_Cardinality_Cantor.ml    | 1 +
 ocaml/fstar-lib/generated/FStar_Cardinality_Universes.ml | 8 ++++++++
 ocaml/fstar-lib/generated/FStar_Functions.ml             | 6 ++++++
 3 files changed, 15 insertions(+)
 create mode 100644 ocaml/fstar-lib/generated/FStar_Cardinality_Cantor.ml
 create mode 100644 ocaml/fstar-lib/generated/FStar_Cardinality_Universes.ml
 create mode 100644 ocaml/fstar-lib/generated/FStar_Functions.ml

diff --git a/ocaml/fstar-lib/generated/FStar_Cardinality_Cantor.ml b/ocaml/fstar-lib/generated/FStar_Cardinality_Cantor.ml
new file mode 100644
index 00000000000..e8306abedb2
--- /dev/null
+++ b/ocaml/fstar-lib/generated/FStar_Cardinality_Cantor.ml
@@ -0,0 +1 @@
+open Prims
\ No newline at end of file
diff --git a/ocaml/fstar-lib/generated/FStar_Cardinality_Universes.ml b/ocaml/fstar-lib/generated/FStar_Cardinality_Universes.ml
new file mode 100644
index 00000000000..83ef61cc385
--- /dev/null
+++ b/ocaml/fstar-lib/generated/FStar_Cardinality_Universes.ml
@@ -0,0 +1,8 @@
+open Prims
+type 'dummyV0 type_powerset =
+  | Mk of (unit -> Prims.bool) 
+let (uu___is_Mk : (unit -> Prims.bool) -> unit type_powerset -> Prims.bool) =
+  fun uu___ -> fun projectee -> true
+let (__proj__Mk__item__f :
+  (unit -> Prims.bool) -> unit type_powerset -> unit -> Prims.bool) =
+  fun uu___ -> fun projectee -> match projectee with | Mk f -> f
\ No newline at end of file
diff --git a/ocaml/fstar-lib/generated/FStar_Functions.ml b/ocaml/fstar-lib/generated/FStar_Functions.ml
new file mode 100644
index 00000000000..7d68ef4d935
--- /dev/null
+++ b/ocaml/fstar-lib/generated/FStar_Functions.ml
@@ -0,0 +1,6 @@
+open Prims
+type ('a, 'b, 'f) is_inj = unit
+type ('a, 'b, 'f) is_surj = unit
+type ('a, 'b, 'f, 'y) in_image = unit
+type ('a, 'b, 'f) image_of = 'b
+type 'a powerset = 'a -> Prims.bool
\ No newline at end of file

From 3e4a5950e24add3463ae24d5875d29177093e6c6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Sun, 14 Apr 2024 10:03:18 -0700
Subject: [PATCH 3/4] FStar.Functions: More facts

---
 ulib/FStar.Functions.fst  | 28 ++++++++++++++++++++--------
 ulib/FStar.Functions.fsti | 17 ++++++++++++++++-
 2 files changed, 36 insertions(+), 9 deletions(-)

diff --git a/ulib/FStar.Functions.fst b/ulib/FStar.Functions.fst
index f2b866904a7..1c342526748 100644
--- a/ulib/FStar.Functions.fst
+++ b/ulib/FStar.Functions.fst
@@ -14,16 +14,28 @@ let lem_surj (#a #b : _) (f : a -> b) (y : b)
   : Lemma (requires is_surj f) (ensures in_image f y)
   = ()
 
-let inverse_of_inj (#a #b : _) (f : a -> b{is_inj f}) (def : a) : GTot (g : (b -> a){is_surj g}) =
+let inverse_of_bij #a #b f =
   (* Construct the inverse from indefinite description + choice. *)
-  let g0 (y:b) : GTot (x:a{in_image f y ==> f x == y})  =
-    FStar.IndefiniteDescription.indefinite_description_tot a
-      (fun (x:a) -> (in_image f y ==> f x == y))
+  let g0 (y:b) : GTot (x:a{f x == y})  =
+    FStar.IndefiniteDescription.indefinite_description_ghost a
+      (fun (x:a) -> f x == y)
   in
-  let g : (b -> a) = Ghost.Pull.pull g0 in
   (* Prove it's surjective *)
-  let aux (x:a) : Lemma (exists (y:b). g y == x) =
-    assert (in_image f (f x))
+  let aux (x:a) : Lemma (exists (y:b). g0 y == x) =
+    assert (g0 (f x) == x)
   in
   Classical.forall_intro aux;
-  g
+  Ghost.Pull.pull 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 g_partial = inverse_of_bij #a #(image_of f) f' in
+  (* extend the inverse to the full domain b *)
+  let g : b -> GTot a =
+    fun (y:b) ->
+      if FStar.StrongExcludedMiddle.strong_excluded_middle (in_image f y)
+      then g_partial y
+      else def
+  in
+  Ghost.Pull.pull g
diff --git a/ulib/FStar.Functions.fsti b/ulib/FStar.Functions.fsti
index 365df75b9a7..503603e5d38 100644
--- a/ulib/FStar.Functions.fsti
+++ b/ulib/FStar.Functions.fsti
@@ -9,12 +9,19 @@ let is_inj (#a #b : _) (f : a -> b) : prop =
 let is_surj (#a #b : _) (f : a -> b) : prop =
   forall (y:b). exists (x:a). f x == y
 
+let is_bij (#a #b : _) (f : a -> b) : prop =
+  is_inj f /\ is_surj f
+
 let in_image (#a #b : _) (f : a -> b) (y : b) : prop =
   exists (x:a). f x == y
 
 let image_of (#a #b : _) (f : a -> b) : Type =
   y:b{in_image f y}
 
+(* g inverses f *)
+let is_inverse_of (#a #b : _) (g : b -> a) (f : a -> b)  =
+  forall (x:a). g (f x) == x
+
 let powerset (a:Type u#aa) : Type u#aa = a -> bool
 
 val inj_comp (#a #b #c : _) (f : a -> b) (g : b -> c)
@@ -28,7 +35,15 @@ val surj_comp (#a #b #c : _) (f : a -> b) (g : b -> c)
 val lem_surj (#a #b : _) (f : a -> 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)
+          (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)
-  : GTot (g : (b -> a){is_surj g})
+  : Ghost (b -> a)
+          (requires is_inj f)
+          (ensures fun g -> is_surj g /\ g `is_inverse_of` f)

From f13d4034e27855948a6ac2212e3b50aad9871b90 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Sun, 14 Apr 2024 10:24:37 -0700
Subject: [PATCH 4/4] snap

---
 ocaml/fstar-lib/generated/FStar_Functions.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/ocaml/fstar-lib/generated/FStar_Functions.ml b/ocaml/fstar-lib/generated/FStar_Functions.ml
index 7d68ef4d935..eb068c194ea 100644
--- a/ocaml/fstar-lib/generated/FStar_Functions.ml
+++ b/ocaml/fstar-lib/generated/FStar_Functions.ml
@@ -1,6 +1,8 @@
 open Prims
 type ('a, 'b, 'f) is_inj = unit
 type ('a, 'b, 'f) is_surj = unit
+type ('a, 'b, 'f) is_bij = unit
 type ('a, 'b, 'f, 'y) in_image = unit
 type ('a, 'b, 'f) image_of = 'b
+type ('a, 'b, 'g, 'f) is_inverse_of = unit
 type 'a powerset = 'a -> Prims.bool
\ No newline at end of file