Support cumulativity in the output for ULift

dumps/ulift

@@ -0,0 +1,79 @@
+1 #NS 0 Scratch
+2 #NS 1 MyProd
+3 #NS 2 mk
+4 #NS 0 α
+5 #NS 0 u
+1 #UP 5
+0 #ES 1
+6 #NS 0 β
+7 #NS 0 v
+2 #UP 7
+1 #ES 2
+8 #NS 0 a
+9 #NS 8 _@
+10 #NS 9 Scratch
+11 #NS 10 Basic
+12 #NS 11 _hyg
+13 #NI 12 122
+2 #EV 1
+14 #NI 12 124
+3 #EC 2 1 2
+4 #EV 3
+5 #EA 3 4
+6 #EV 2
+7 #EA 5 6
+8 #EP #BD 14 2 7
+9 #EP #BD 13 2 8
+10 #EP #BI 6 1 9
+11 #EP #BI 4 0 10
+3 #US 0
+4 #UM 3 1
+5 #UM 4 2
+12 #ES 5
+13 #EP #BD 6 1 12
+14 #EP #BD 4 0 13
+#IND 2 2 14 1 3 11 5 7
+15 #NS 0 ULift
+16 #NS 15 up
+17 #NS 0 s
+6 #UP 17
+7 #US 6
+15 #ES 7
+18 #NS 0 down
+16 #EV 0
+19 #NS 0 r
+8 #UP 19
+17 #EC 15 8 6
+18 #EA 17 2
+19 #EP #BD 18 16 18
+20 #EP #BI 4 15 19
+9 #UM 6 8
+10 #US 9
+21 #ES 10
+22 #EP #BD 4 15 21
+#IND 1 15 22 1 16 20 19 17
+20 #NS 1 MyNat
+21 #NS 20 zero
+23 #EC 20 
+22 #NS 20 succ
+23 #NI 12 7
+24 #EP #BD 23 23 23
+25 #ES 3
+#IND 0 20 25 2 21 23 22 24 
+24 #NS 1 example1
+11 #US 3
+26 #EC 2 11 11
+27 #EC 15 3 0
+28 #EA 27 23
+29 #EA 26 28
+30 #EA 29 25
+31 #EC 3 11 11
+32 #EA 31 28
+33 #EA 32 25
+34 #EC 16 3 0
+35 #EA 34 23
+36 #EC 21 
+37 #EA 35 36
+38 #EA 33 37
+39 #EA 38 23
+#DEF 24 30 39 

src/Lean.v

@@ -397,3 +397,94 @@ 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.
+   Instance 0: both r and s non-SProp *)
+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_rec.cumul.ind.
+
+(* Instance 1: r=SProp, s non-SProp *)
+Definition ULift_cumul_inst1@{s|} (α : Type@{s}) : Type@{s} := α.
+Register ULift_cumul_inst1 as lean.ULift_inst1.cumul.
+
+Definition ULift_up_cumul_inst1@{s|} {α : Type@{s}} (a : α) : ULift_cumul_inst1@{s} α := a.
+Register ULift_up_cumul_inst1 as lean.ULift_up_inst1.cumul.
+
+Definition ULift_down_cumul_inst1@{s|} {α : Type@{s}} (a : ULift_cumul_inst1@{s} α) : α := a.
+Register ULift_down_cumul_inst1 as lean.ULift_down_inst1.cumul.
+
+Definition ULift_rec_cumul_inst1@{motive s|} {α : Type@{s}} {P : ULift_cumul_inst1@{s} α → Type@{motive}}
+  (mk : forall (down : α), P (ULift_up_cumul_inst1 down))
+  (t : ULift_cumul_inst1@{s} α) : P t
+  := mk t.
+Register ULift_rec_cumul_inst1 as lean.ULift_rec_inst1.cumul.
+
+Definition ULift_ind_cumul_inst1@{s|} {α : Type@{s}} {P : ULift_cumul_inst1@{s} α → SProp}
+  (mk : forall (down : α), P (ULift_up_cumul_inst1 down))
+  (t : ULift_cumul_inst1@{s} α) : P t
+  := mk t.
+Register ULift_ind_cumul_inst1 as lean.ULift_rec_inst1.cumul.ind.
+
+(* Instance 2: r non-SProp, s=SProp
+   Lean Prop maps to Rocq SProp, but arguments may live in Set by cumulativity,
+   so we use Set as the domain sort. *)
+Definition ULift_cumul_inst2@{r|} (α : Set) : Type@{r} := α.
+Register ULift_cumul_inst2 as lean.ULift_inst2.cumul.
+
+Definition ULift_up_cumul_inst2@{r|} {α : Set} (a : α) : ULift_cumul_inst2@{r} α := a.
+Register ULift_up_cumul_inst2 as lean.ULift_up_inst2.cumul.
+
+Definition ULift_down_cumul_inst2@{r|} {α : Set} (a : ULift_cumul_inst2@{r} α) : α := a.
+Register ULift_down_cumul_inst2 as lean.ULift_down_inst2.cumul.
+
+Definition ULift_rec_cumul_inst2@{motive r|} {α : Set} {P : ULift_cumul_inst2@{r} α → Type@{motive}}
+  (mk : forall (down : α), P (ULift_up_cumul_inst2 down))
+  (t : ULift_cumul_inst2@{r} α) : P t
+  := mk t.
+Register ULift_rec_cumul_inst2 as lean.ULift_rec_inst2.cumul.
+
+Definition ULift_ind_cumul_inst2@{r|} {α : Set} {P : ULift_cumul_inst2@{r} α → SProp}
+  (mk : forall (down : α), P (ULift_up_cumul_inst2 down))
+  (t : ULift_cumul_inst2@{r} α) : P t
+  := mk t.
+Register ULift_ind_cumul_inst2 as lean.ULift_rec_inst2.cumul.ind.
+
+(* Instance 3: both r=SProp, s=SProp *)
+Definition ULift_cumul_inst3@{|} (α : Set) : Set := α.
+Register ULift_cumul_inst3 as lean.ULift_inst3.cumul.
+
+Definition ULift_up_cumul_inst3@{|} {α : Set} (a : α) : ULift_cumul_inst3 α := a.
+Register ULift_up_cumul_inst3 as lean.ULift_up_inst3.cumul.
+
+Definition ULift_down_cumul_inst3@{|} {α : Set} (a : ULift_cumul_inst3 α) : α := a.
+Register ULift_down_cumul_inst3 as lean.ULift_down_inst3.cumul.
+
+Definition ULift_rec_cumul_inst3@{motive|} {α : Set} {P : ULift_cumul_inst3 α → Type@{motive}}
+  (mk : forall (down : α), P (ULift_up_cumul_inst3 down))
+  (t : ULift_cumul_inst3 α) : P t
+  := mk t.
+Register ULift_rec_cumul_inst3 as lean.ULift_rec_inst3.cumul.
+
+Definition ULift_ind_cumul_inst3@{|} {α : Set} {P : ULift_cumul_inst3 α → SProp}
+  (mk : forall (down : α), P (ULift_up_cumul_inst3 down))
+  (t : ULift_cumul_inst3 α) : P t
+  := mk t.
+Register ULift_ind_cumul_inst3 as lean.ULift_rec_inst3.cumul.ind.

src/lean.ml

@@ -688,6 +688,24 @@ let get_predeclared_ind indn n i =
     | exception _ -> None
   else None
 
+(** Like [get_predeclared_ind] but looks for an inductive predeclared as a
+    definition (using a ".cumul" suffix on the registration). Returns the
+    ConstRef of the predeclared definition. *)
+let get_predeclared_ind_as_def indn n i =
+  if N.equal n (N.append_list N.anon indn) then
+    let ind_name = name_for_core n i in
+    let reg = "lean." ^ Id.to_string ind_name ^ ".cumul" in
+    match Rocqlib.lib_ref reg with
+    | ConstRef c -> Some (ind_name, c)
+    | _ ->
+      CErrors.user_err
+        Pp.(
+          str "Bad registration for "
+          ++ str reg
+          ++ str " expected a constant.")
+    | exception _ -> None
+  else None
+
 let get_predeclared_def defn n i =
   if N.equal n (N.append_list N.anon defn) then
     let def_name = name_for_core n i in
@@ -703,6 +721,7 @@ let get_predeclared_def defn n i =
 
 type predeclared_ind_kind = Eq | Nat | Nat_le | Or | And | Fin | UInt32 | Char
 type predeclared_def_kind = UInt32_size | Nat_isValidChar
+type predeclared_ind_as_def_kind = ULift_cumul
 
 let get_predeclared_cnames (k : predeclared_ind_kind) n =
   match k with
@@ -738,6 +757,22 @@ let get_predeclared_ind_some n i =
     CErrors.user_err
       Pp.(str "Multiple predeclared inductive types for " ++ N.pp n)
 
+let get_predeclared_ind_as_def_any n i =
+  List.filter_map
+    (fun (k, h) ->
+      get_predeclared_ind_as_def h n i |> Option.map (fun x -> (k, h, x)))
+    [
+      (ULift_cumul, [ "ULift" ]);
+    ]
+
+let get_predeclared_ind_as_def_some n i =
+  match get_predeclared_ind_as_def_any n i with
+  | [] -> None
+  | [ x ] -> Some x
+  | _ :: _ :: _ ->
+    CErrors.user_err
+      Pp.(str "Multiple predeclared ind-as-def constants for " ++ N.pp n)
+
 let get_predeclared_def_any n i =
   List.filter_map
     (fun (defk, defh) ->
@@ -821,6 +856,11 @@ let error_mode = function
   | MissingQuot when skip_missing_quot () -> Skip
   | _ -> error_mode ()
 
+let ulift_name = N.append_list N.anon [ "ULift" ]
+
+let ulift_to_cumulativity () =
+  Rocqlib.has_ref "lean.ULift.cumul"
+
 module ZMap = CMap.Make (Z)
 
 let nat_ints = ref ZMap.empty
@@ -1004,6 +1044,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 +1253,29 @@ and to_params uconv params =
   (acc, List.rev params)
 
 and declare_ind { name = n; params; ty; ctors; univs } i =
+  (* Handle inductives predeclared as definitions (e.g., ULift with cumulativity).
+     We check if there's a cumul registration, then use per-instance registrations. *)
+  match get_predeclared_ind_as_def_some n 0 with
+  | Some (ULift_cumul, _, _) ->
+    let def_name = name_for_core n i in
+    let cumul_reg nm = "lean." ^ Id.to_string (name_for_core nm i) ^ ".cumul" in
+    Feedback.msg_info Pp.(Id.print def_name ++ str " is predeclared (cumulative)");
+    let ulift_ref = Rocqlib.lib_ref (cumul_reg n) in
+    let inst = { ref = ulift_ref; algs = [] } in
+    add_declared n i inst;
+    (* Register ULift.up constructor *)
+    let cname = N.append n "up" in
+    add_declared cname i { ref = Rocqlib.lib_ref (cumul_reg cname); algs = [] };
+    (* Register ULift.down *)
+    let dname = N.append n "down" in
+    add_declared dname i { ref = Rocqlib.lib_ref (cumul_reg dname); algs = [] };
+    (* Register eliminator (Type scheme at j=2*i, SProp scheme at j=2*i+1) *)
+    let nrec = N.append n "rec" in
+    let rec_base = cumul_reg nrec in
+    add_declared nrec (2 * i) { ref = Rocqlib.lib_ref rec_base; algs = [] };
+    add_declared nrec ((2 * i) + 1) { ref = Rocqlib.lib_ref (rec_base ^ ".ind"); algs = [] };
+    inst
+  | None ->
   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,12 @@
+From LeanImport Require Import Lean.
+
+(* Test: ULift imported with cumulativity uses definitions instead of an inductive.
+   The cumulative definitions are registered in Lean.v, so the import automatically
+   uses cumulativity for ULift. *)
+Redirect "ulift_cumul.log" Lean Import "../dumps/ulift".
+
+(* Verify that the imported Scratch_example1 has the correct type.
+   With cumulativity, ULift is transparent, so ULift_cumul_inst2 Scratch_MyNat
+   is convertible with Scratch_MyNat. *)
+Check Scratch_example1 : Scratch_MyProd (ULift_cumul_inst2 Scratch_MyNat) Type.
+Check Scratch_example1 : Scratch_MyProd Scratch_MyNat Type.