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

@@ -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 ()

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))

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 ()

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))

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

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})