Support cumulativity in the output for ULift

dumps/ulift

@@ -0,0 +1,30 @@
+1 #NS 0 r
+2 #NS 0 s
+3 #NS 0 α
+4 #NS 0 ULift
+5 #NS 4 up
+6 #NS 0 down
+7 #NS 0 self
+8 #NS 4 down
+1 #UP 1
+2 #UP 2
+3 #US 2
+4 #UM 2 1
+5 #US 4
+0 #EV 0
+1 #EV 1
+2 #ES 3
+3 #ES 5
+4 #EC 4 1 2
+5 #EA 4 1
+6 #EP #BD 6 0 5
+7 #EP #BI 3 2 6
+8 #EP #BD 3 2 3
+#IND 1 4 8 1 5 7 1 2
+9 #EA 4 0
+10 #EP #BD 7 9 1
+11 #EP #BI 3 2 10
+12 #EJ 4 0 0
+13 #EL #BD 7 9 12
+14 #EL #BD 3 2 13
+#DEF 8 11 14 1 2

src/Lean.v

@@ -397,3 +397,25 @@ End strings.
 Register Nat_isValidChar as lean.Nat_isValidChar.
 Register Char as lean.Char.
 Register reflective_Char_mk_prim as lean.Char.mk.reflective_prim.
+
+(* Cumulative ULift: using cumulativity instead of an inductive *)
+Definition ULift_cumul@{r s|} (α : Type@{s}) : Type@{max(r,s)} := α.
+Register ULift_cumul as lean.ULift.cumul.
+
+Definition ULift_up_cumul@{r s|} {α : Type@{s}} (a : α) : ULift_cumul@{r s} α := a.
+Register ULift_up_cumul as lean.ULift.up.cumul.
+
+Definition ULift_down_cumul@{r s|} {α : Type@{s}} (a : ULift_cumul@{r s} α) : α := a.
+Register ULift_down_cumul as lean.ULift.down.cumul.
+
+Definition ULift_rec_cumul@{motive r s|} {α : Type@{s}} {P : ULift_cumul@{r s} α → Type@{motive}}
+  (mk : forall (down : α), P (ULift_up_cumul down))
+  (t : ULift_cumul@{r s} α) : P t
+  := mk t.
+Register ULift_rec_cumul as lean.ULift.rec.cumul.
+
+Definition ULift_ind_cumul@{r s|} {α : Type@{s}} {P : ULift_cumul@{r s} α → SProp}
+  (mk : forall (down : α), P (ULift_up_cumul down))
+  (t : ULift_cumul@{r s} α) : P t
+  := mk t.
+Register ULift_ind_cumul as lean.ULift.ind.cumul.

src/lean.ml

@@ -821,6 +821,13 @@ let error_mode = function
   | MissingQuot when skip_missing_quot () -> Skip
   | _ -> error_mode ()
 
+let { Goptions.get = ulift_to_cumulativity } =
+  Goptions.declare_bool_option_and_ref
+    ~key:[ "Lean"; "ULift"; "To"; "Cumulativity" ]
+    ~value:false ()
+
+let ulift_name = N.append_list N.anon [ "ULift" ]
+
 module ZMap = CMap.Make (Z)
 
 let nat_ints = ref ZMap.empty
@@ -1004,6 +1011,10 @@ let rec to_constr =
       ret (mkProd (n, a, b))
     | Proj (lean_ind, field, c) ->
       to_constr env c >>= fun c ->
+      if ulift_to_cumulativity () && N.equal lean_ind ulift_name then
+        (* With cumulativity, ULift is transparent, so projection is identity *)
+        ret c
+      else
       get_uconv >>= fun uconv ->
       (* we retype to get the ind, because otherwise we need the lean
        univs for instantiation
@@ -1209,6 +1220,31 @@ and to_params uconv params =
   (acc, List.rev params)
 
 and declare_ind { name = n; params; ty; ctors; univs } i =
+  (* Handle ULift with cumulativity *)
+  if ulift_to_cumulativity () && i = 0 && N.equal n ulift_name
+     && Rocqlib.has_ref "lean.ULift.cumul"
+  then begin
+    Feedback.msg_info Pp.(str "ULift is predeclared (cumulative)");
+    (* Register ULift type *)
+    let ulift_ref = Rocqlib.lib_ref "lean.ULift.cumul" in
+    let inst = { ref = ulift_ref; algs = [] } in
+    add_declared n i inst;
+    (* Register ULift.up constructor *)
+    let cname = N.append n "up" in
+    let ulift_up_ref = Rocqlib.lib_ref "lean.ULift.up.cumul" in
+    add_declared cname i { ref = ulift_up_ref; algs = [] };
+    (* Register ULift.down *)
+    let dname = N.append n "down" in
+    let ulift_down_ref = Rocqlib.lib_ref "lean.ULift.down.cumul" in
+    add_declared dname i { ref = ulift_down_ref; algs = [] };
+    (* Register eliminator (Type scheme at j=2*i=0, SProp scheme at j=2*i+1=1) *)
+    let nrec = N.append n "rec" in
+    let ulift_rec_ref = Rocqlib.lib_ref "lean.ULift.rec.cumul" in
+    add_declared nrec (2 * i) { ref = ulift_rec_ref; algs = [] };
+    let ulift_ind_ref = Rocqlib.lib_ref "lean.ULift.ind.cumul" in
+    add_declared nrec ((2 * i) + 1) { ref = ulift_ind_ref; algs = [] };
+    inst
+  end else
   let mind, algs, ind_name, cnames, univs, squashy =
     match get_predeclared_ind_some n i with
     | Some (Eq, _, (ind_name, mind)) ->

tests/_CoqProject

@@ -6,4 +6,5 @@
 core.v
 init.v
 anomaly_print_projections.v
-pnni.v
+pnni.v
+ulift_cumul.v

tests/ulift_cumul.v

@@ -0,0 +1,15 @@
+From LeanImport Require Import Lean.
+
+(* Test: ULift imported with cumulativity uses definitions instead of an inductive *)
+Set Lean ULift To Cumulativity.
+Redirect "ulift_cumul.log" Lean Import "../dumps/ulift".
+
+(* Verify ULift_cumul is convertible with the identity type function:
+   α should be accepted where ULift_cumul α is expected *)
+Check (fun (α : Type) (x : α) => (x : ULift_cumul α)).
+
+(* Verify the round trip: ULift_down_cumul (ULift_up_cumul x) = x *)
+Check (fun (α : Type) (x : α) => ULift_down_cumul (ULift_up_cumul x) : α).
+
+(* Verify that the imported ULift_down is well-typed *)
+Check ULift_down.