Support cumulativity in the output for ULift by Copilot · Pull Request #60 · rocq-community/rocq-lean-import

Copilot · 2026-04-05T18:53:29Z

Generalized predeclared API with get_predeclared_ind_as_def for .cumul suffix
declare_ind checks per-instance cumul registrations
to_constr Proj case handles transparent cumulative types
No flag needed — conditioned on Rocqlib.has_ref
Removed SProp cumul definitions (only instance 0 supports cumulativity)
Moved definitions + Register commands to src/ULiftCumulativeRegistration.v (not required by Lean.v, can be Require Imported)
tests/ulift_no_cumul.v: without Register, ULift is an inductive (Fail Check)
tests/ulift_cumul.v: with Require Import ULiftCumulativeRegistration, ULift is transparent
Fixed CI: replaced Unicode → with -> in ULiftCumulativeRegistration.v

Adds support for importing Lean's ULift type using cumulativity instead of an inductive type. When the option is enabled: - ULift is mapped to a transparent definition (ULift_cumul) - ULift.up and ULift.down are mapped to identity functions - ULift.rec is mapped to trivial eliminators - Projections on ULift are replaced by identity Includes registered definitions in Lean.v, option handling in lean.ml, a minimal test dump, and a test file. Agent-Logs-Url: https://github.com/rocq-community/rocq-lean-import/sessions/ba4115fb-a151-49c7-a440-57e98bb41061 Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com>

Agent-Logs-Url: https://github.com/rocq-community/rocq-lean-import/sessions/ba4115fb-a151-49c7-a440-57e98bb41061 Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com>

SkySkimmer · 2026-04-05T19:32:54Z

+  (* Handle ULift with cumulativity *)
+  if ulift_to_cumulativity () && i = 0 && N.equal n ulift_name
+     && Rocqlib.has_ref "lean.ULift.cumul"
+  then begin


there is already an API for predeclared things (get_predeclared_*), use that (generalizing it if necessary)

Done in cae05d6. Generalized the predeclared API with get_predeclared_ind_as_def (for inductives predeclared as definitions using a .cumul suffix), predeclared_ind_as_def_kind type, and get_predeclared_ind_as_def_some/get_predeclared_ind_as_def_any lookup functions, following the same pattern as the existing get_predeclared_ind and get_predeclared_def APIs.

JasonGross · 2026-04-05T23:35:12Z

@copilot please address the PR comments and also @SkySkimmer 's suggestion in the issue to drop the flag and just condition the translation on whether or not the registrations are present

- Remove `Set Lean ULift To Cumulativity` flag; condition on registration presence via `Rocqlib.has_ref` instead - Generalize predeclared API with `get_predeclared_ind_as_def` for inductives predeclared as definitions (with `.cumul` suffix) - Add per-instance cumulative definitions in Lean.v (instances 0-3) - Use the example.out dump from the issue as the test dump - Verify example1 has correct type via convertibility Check Agent-Logs-Url: https://github.com/rocq-community/rocq-lean-import/sessions/c14263e4-2114-4574-8fd3-68315e2e8b4d Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com>

Copilot · 2026-04-05T23:51:21Z

@copilot please address the PR comments and also @SkySkimmer 's suggestion in the issue to drop the flag and just condition the translation on whether or not the registrations are pres...

All three requests addressed in cae05d6:

Dropped the Set Lean ULift To Cumulativity flag — the translation is now conditioned on whether the cumul registrations are present (Rocqlib.has_ref "lean.ULift.cumul")
Used the existing predeclared API, generalized with get_predeclared_ind_as_def for the .cumul suffix pattern
Used the example.out from the issue as the test dump and verified example1 type via Check

SkySkimmer · 2026-04-06T09:19:47Z

+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,


This seems strange, Rocq doesn't have cumulativity between SProp and Set.

Removed all SProp cumul definitions from src/Lean.v in ead0230. Only instance 0 (both r, s non-SProp) supports the cumulative translation; SProp instances (1-3) fall through to normal inductive translation. The cumul definitions and Register commands are now provided at test time only.

JasonGross · 2026-04-06T15:40:33Z

@copilot Drop the manual Set/SProp definitions; those still need translation by inductive. The Register commands should be only in the test time, which should test in one module that without register the check fails, while in another module with register the check succeeds

…no-cumul test - Remove all cumulative ULift definitions/registrations from src/Lean.v (SProp instances 1-3 were incorrect per review, instance 0 moved to test) - Move Register commands to tests/ulift_cumul.v (test-time only) - Add tests/ulift_no_cumul.v: verifies that without Register, ULift is an inductive (Fail Check for bare convertibility) - Update declare_ind to check per-instance cumul registration (not just i=0) - Fix Proj handler to check retyped head instead of global flag: returns identity only when type is not an inductive (transparent cumul case) Agent-Logs-Url: https://github.com/rocq-community/rocq-lean-import/sessions/869afe32-6302-41c3-bca8-7803335da0e9 Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com>

Copilot · 2026-04-06T15:51:43Z

@copilot Drop the manual Set/SProp definitions; those still need translation by inductive. The Register commands should be only in the test time, which should test in one module that ...

Done in ead0230:

Removed all SProp cumul definitions from src/Lean.v
Moved Register commands to tests/ulift_cumul.v (test-time only)
Added tests/ulift_no_cumul.v which verifies that without Register, ULift is an inductive (Fail Check for bare convertibility)
tests/ulift_cumul.v defines + registers cumul defs, imports the same dump, and verifies transparency
Updated declare_ind to check per-instance cumul registration (not global)
Fixed Proj handler to check retyped head instead of global flag

JasonGross · 2026-04-06T23:59:11Z

@copilot Move the definition and register commands to a separate file (not in test-suite) like ULiftCumulativeRegistration.v that is not required by Lean.v and can be Required/Imported.

Move ULift cumulative definitions and Register commands from inline in the test file to a separate src/ULiftCumulativeRegistration.v that is part of the LeanImport package but not required by Lean.v. Users can Require Import it before Lean Import to activate cumulative ULift translation. Agent-Logs-Url: https://github.com/rocq-community/rocq-lean-import/sessions/1dbfd860-3100-4aa9-9319-9ff024615475 Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com>

Copilot · 2026-04-07T00:01:14Z

@copilot Move the definition and register commands to a separate file (not in test-suite) like ULiftCumulativeRegistration.v that is not required by Lean.v and can be Required/`I...

Created src/ULiftCumulativeRegistration.v with the definitions and Register commands in a6b3864. It's part of the LeanImport package (listed in _CoqProject) but not required by Lean.v. The test ulift_cumul.v now does From LeanImport Require Import Lean ULiftCumulativeRegistration. to activate it.

JasonGross · 2026-04-07T00:48:32Z

@copilot fix ci

Replace → with -> and – with - to fix "Undefined token" lexer error in CI where the Unicode arrow is not recognized by the Rocq lexer. Agent-Logs-Url: https://github.com/rocq-community/rocq-lean-import/sessions/3389edcd-4cf8-4004-92c0-4b549d195087 Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com>

Copilot · 2026-04-07T00:51:22Z

@copilot fix ci

Fixed in 231b6e5. The CI failure was a "Lexer: Undefined token" error caused by Unicode → characters in src/ULiftCumulativeRegistration.v — replaced with ASCII ->.

JasonGross · 2026-04-07T20:11:29Z

@SkySkimmer tests pass, I am satisfied with the design. What do you think?

SkySkimmer · 2026-04-07T20:21:40Z

seems ok

* Initial plan * feat: add Set Lean ULift To Cumulativity option Adds support for importing Lean's ULift type using cumulativity instead of an inductive type. When the option is enabled: - ULift is mapped to a transparent definition (ULift_cumul) - ULift.up and ULift.down are mapped to identity functions - ULift.rec is mapped to trivial eliminators - Projections on ULift are replaced by identity Includes registered definitions in Lean.v, option handling in lean.ml, a minimal test dump, and a test file. Agent-Logs-Url: https://github.com/rocq-community/rocq-lean-import/sessions/ba4115fb-a151-49c7-a440-57e98bb41061 Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com> * fix: remove incomplete comment from test file Agent-Logs-Url: https://github.com/rocq-community/rocq-lean-import/sessions/ba4115fb-a151-49c7-a440-57e98bb41061 Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com> * refactor: use predeclared API, drop the flag, use example.out from issue - Remove `Set Lean ULift To Cumulativity` flag; condition on registration presence via `Rocqlib.has_ref` instead - Generalize predeclared API with `get_predeclared_ind_as_def` for inductives predeclared as definitions (with `.cumul` suffix) - Add per-instance cumulative definitions in Lean.v (instances 0-3) - Use the example.out dump from the issue as the test dump - Verify example1 has correct type via convertibility Check Agent-Logs-Url: https://github.com/rocq-community/rocq-lean-import/sessions/c14263e4-2114-4574-8fd3-68315e2e8b4d Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com> * fix: remove SProp cumul defs from Lean.v, move Register to test, add no-cumul test - Remove all cumulative ULift definitions/registrations from src/Lean.v (SProp instances 1-3 were incorrect per review, instance 0 moved to test) - Move Register commands to tests/ulift_cumul.v (test-time only) - Add tests/ulift_no_cumul.v: verifies that without Register, ULift is an inductive (Fail Check for bare convertibility) - Update declare_ind to check per-instance cumul registration (not just i=0) - Fix Proj handler to check retyped head instead of global flag: returns identity only when type is not an inductive (transparent cumul case) Agent-Logs-Url: https://github.com/rocq-community/rocq-lean-import/sessions/869afe32-6302-41c3-bca8-7803335da0e9 Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com> * refactor: move cumul definitions to src/ULiftCumulativeRegistration.v Move ULift cumulative definitions and Register commands from inline in the test file to a separate src/ULiftCumulativeRegistration.v that is part of the LeanImport package but not required by Lean.v. Users can Require Import it before Lean Import to activate cumulative ULift translation. Agent-Logs-Url: https://github.com/rocq-community/rocq-lean-import/sessions/1dbfd860-3100-4aa9-9319-9ff024615475 Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com> * fix: replace Unicode arrow and en-dash in ULiftCumulativeRegistration.v Replace → with -> and – with - to fix "Undefined token" lexer error in CI where the Unicode arrow is not recognized by the Rocq lexer. Agent-Logs-Url: https://github.com/rocq-community/rocq-lean-import/sessions/3389edcd-4cf8-4004-92c0-4b549d195087 Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com>

Initial plan

872f25f

Copilot AI assigned Copilot and JasonGross Apr 5, 2026

Copilot AI linked an issue Apr 5, 2026 that may be closed by this pull request

Supporting cumulativity in the output #59

Closed

Copilot started work on behalf of JasonGross April 5, 2026 18:53 View session

Copilot AI and others added 2 commits April 5, 2026 19:21

fix: remove incomplete comment from test file

7b9f2e4

Agent-Logs-Url: https://github.com/rocq-community/rocq-lean-import/sessions/ba4115fb-a151-49c7-a440-57e98bb41061 Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com>

Copilot AI changed the title ~~[WIP] Add support for cumulativity in output with ULift~~ Support cumulativity in the output for ULift Apr 5, 2026

Copilot AI requested a review from JasonGross April 5, 2026 19:24

Copilot finished work on behalf of JasonGross April 5, 2026 19:24

SkySkimmer reviewed Apr 5, 2026

View reviewed changes

Comment thread tests/ulift_cumul.v

SkySkimmer reviewed Apr 5, 2026

View reviewed changes

Copilot started work on behalf of JasonGross April 5, 2026 23:35 View session

Copilot finished work on behalf of JasonGross April 5, 2026 23:52

SkySkimmer reviewed Apr 6, 2026

View reviewed changes

Copilot started work on behalf of JasonGross April 6, 2026 15:40 View session

Copilot finished work on behalf of JasonGross April 6, 2026 15:53

Copilot started work on behalf of JasonGross April 6, 2026 23:59 View session

Copilot finished work on behalf of JasonGross April 7, 2026 00:02

Copilot started work on behalf of JasonGross April 7, 2026 00:48 View session

Copilot finished work on behalf of JasonGross April 7, 2026 00:52

JasonGross marked this pull request as ready for review April 7, 2026 20:11

JasonGross merged commit c72a3ec into master Apr 7, 2026
1 check passed

JasonGross deleted the copilot/add-cumulativity-support branch April 7, 2026 20:34

ebmoon mentioned this pull request Apr 18, 2026

Fix ULift cumul functions and consolidate ULift tests #61

Merged

Uh oh!

Conversation

Copilot AI commented Apr 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

SkySkimmer Apr 5, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 5, 2026

Choose a reason for hiding this comment

Uh oh!

JasonGross commented Apr 5, 2026

Uh oh!

Copilot AI commented Apr 5, 2026

Uh oh!

SkySkimmer Apr 6, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 6, 2026

Choose a reason for hiding this comment

Uh oh!

JasonGross commented Apr 6, 2026

Uh oh!

Copilot AI commented Apr 6, 2026

Uh oh!

JasonGross commented Apr 6, 2026

Uh oh!

Copilot AI commented Apr 7, 2026

Uh oh!

JasonGross commented Apr 7, 2026

Uh oh!

Copilot AI commented Apr 7, 2026

Uh oh!

JasonGross commented Apr 7, 2026

Uh oh!

SkySkimmer commented Apr 7, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Copilot AI commented Apr 5, 2026 •

edited

Loading