Don't emit primitive records for recursive single-constructor inductives by ebmoon · Pull Request #62 · rocq-community/rocq-lean-import

ebmoon · 2026-04-20T18:54:22Z

Summary

The importer's declare_ind coerced every Lean inductive that was single-constructor + no-indices + ≥1 relevant field into a Rocq primitive record, without checking recursion.
A recursive single-constructor inductive cannot admit eta-conversion, and Rocq 9.1+ rejects any primitive-record declaration the kernel can't prove eta for — with "Primitive records must have eta conversion to allow dependent elimination". This blocks imports of Stream/Tree-shaped inductives at declaration time (whether recursion is direct or nested through another type).
This PR adds an is_recursive guard that falls through to the plain Inductive path whenever the inductive occurs in any field type. Non-recursive records keep the primitive-record encoding.

Change

src/lean.ml, inside declare_ind's record-coercion branch, walk the rebuilt constructor's Prod chain and ask Vars.noccurn k t per field, where k starts at npars + 1 (the inductive's Rel index in env_ind_params) and is lifted by one per enclosing binder. The walk stops before the codomain — a constructor's codomain is Ind params… by construction, so testing it would flag every single-constructor inductive as recursive and demote every record.

ebmoon · 2026-04-21T02:09:25Z

Correct fix of this might be the fix for #63

SkySkimmer · 2026-04-21T09:25:52Z

Do Lean recursive records have primitive eta? If not then they're different issues (#63 is a case where Lean has primitive eta but Rocq doesn't, this one may just be an incorrect translation)

ebmoon · 2026-04-21T17:58:55Z

I see. It seems Lean recursive records don't have eta:

https://github.com/leanprover/lean4/blob/master/src/kernel/type_checker.cpp#L800

JasonGross · 2026-04-22T20:11:38Z

Here is a .lean file and the corresponding .out file:

inductive list.{u} (α : Sort u)
  | nil  : list α
  | cons : α → list α → list α
inductive RecInd.{u} (A : Sort u)
  | mk : A → list (RecInd A) → RecInd A

-- Definitional eta does NOT hold for RecInd
-- Propositional eta
theorem RecInd.eta (x : RecInd A) : RecInd.mk x.1 x.2 = x := by
  fail_if_success rfl
  cases x; rfl

.out file

1 #NS 0 list
2 #NS 1 nil
3 #NS 0 α
4 #NS 0 u
1 #UP 4
0 #ES 1
1 #EC 1 1
2 #EV 0
3 #EA 1 2
4 #EP #BI 3 0 3
5 #NS 1 cons
6 #NS 0 a
7 #NS 6 _@
8 #NS 7 test2
9 #NS 8 _hyg
10 #NI 9 8
11 #NI 9 10
5 #EV 1
6 #EA 1 5
7 #EV 2
8 #EA 1 7
9 #EP #BD 11 6 8
10 #EP #BD 10 2 9
11 #EP #BI 3 0 10
2 #US 0
3 #UM 2 1
12 #ES 3
13 #EP #BD 3 0 12
#IND 1 1 13 2 2 4 5 11 4
12 #NS 0 RecInd
13 #NS 12 mk
14 #NS 0 A
15 #NI 9 38
16 #NI 9 40
14 #EC 1 3
15 #EC 12 1
16 #EA 15 5
17 #EA 14 16
18 #EA 15 7
19 #EP #BD 16 17 18
20 #EP #BD 15 2 19
21 #EP #BI 14 0 20
#IND 1 12 13 1 13 21 4
17 #NS 0 Eq
18 #NS 17 refl
19 #NS 0 u_1
4 #UP 19
22 #ES 4
23 #EC 17 4
24 #EA 23 5
25 #EA 24 2
26 #EA 25 2
27 #EP #BD 6 2 26
28 #EP #BI 3 22 27
20 #NS 7 Init
21 #NS 20 Prelude
22 #NS 21 _hyg
23 #NI 22 194
24 #NI 22 196
29 #ES 0
30 #EP #BD 24 5 29
31 #EP #BD 23 2 30
32 #EP #BI 3 22 31
#IND 2 17 32 1 18 28 19
25 #NS 0 PUnit
26 #NS 25 unit
33 #EC 25 1
#IND 0 25 0 1 26 33 4
27 #NS 12 casesOn
28 #NS 0 motive_1
29 #NS 0 t
34 #EA 15 2
35 #EP #BD 29 34 22
30 #NS 0 mk
36 #EV 3
37 #EA 15 36
38 #EA 14 37
39 #EC 13 1
40 #EV 4
41 #EA 39 40
42 #EA 41 5
43 #EA 42 2
44 #EA 36 43
45 #EP #BD 16 38 44
46 #EP #BD 15 7 45
47 #EA 7 5
48 #EP #BD 30 46 47
49 #EP #BD 29 16 48
50 #EP #BI 28 35 49
51 #EP #BI 14 0 50
31 #NS 12 rec
52 #EC 31 4 1
53 #EA 52 36
54 #EA 53 7
55 #EC 25 4
56 #EL #BD 29 38 55
57 #EA 54 56
58 #EA 15 40
59 #EA 14 58
32 #NS 0 a_ih
33 #NS 32 _@
34 #NS 33 test2
35 #NS 34 _hyg
36 #NI 35 40
60 #EA 36 7
61 #EA 60 5
62 #EL #BD 36 55 61
63 #EL #BD 16 59 62
64 #EL #BD 15 36 63
65 #EA 57 64
66 #EC 26 4
67 #EA 65 66
37 #NI 35 8
68 #EA 40 5
38 #NI 35 10
69 #EL #BD 38 55 66
70 #EL #BD 37 68 69
71 #EL #BD 11 59 70
72 #EL #BD 10 37 71
73 #EA 67 72
74 #EA 73 5
75 #EL #BD 30 46 74
76 #EL #BD 29 16 75
77 #EL #BI 28 35 76
78 #EL #BI 14 0 77
#DEF 27 51 78 19 4
39 #NS 17 ndrec
40 #NS 0 u2
5 #UP 40
79 #ES 5
41 #NS 0 motive
42 #NI 22 212
43 #NS 0 u1
6 #UP 43
80 #ES 6
81 #EP #BD 42 5 80
44 #NS 0 m
82 #EA 2 5
45 #NS 0 b
46 #NS 0 h
83 #EC 17 5
84 #EA 83 40
85 #EA 84 36
86 #EA 85 2
87 #EA 36 5
88 #EP #BD 46 86 87
89 #EP #BI 45 36 88
90 #EP #BD 44 82 89
91 #EP #BI 41 81 90
92 #EP #BI 6 2 91
93 #EP #BI 3 79 92
47 #NS 17 rec
94 #EC 47 6 5
95 #EV 5
96 #EA 94 95
97 #EA 96 40
48 #NS 0 x
49 #NS 48 _@
50 #NS 49 Init
51 #NS 50 Prelude
52 #NS 51 _hyg
53 #NI 52 225
54 #NI 52 224
98 #EV 6
99 #EA 83 98
100 #EA 99 95
101 #EA 100 2
102 #EA 95 5
103 #EL #BD 54 101 102
104 #EL #BD 53 95 103
105 #EA 97 104
106 #EA 105 7
107 #EA 106 5
108 #EA 107 2
109 #EL #BD 46 86 108
110 #EL #BI 45 36 109
111 #EL #BD 44 82 110
112 #EL #BI 41 81 111
113 #EL #BI 6 2 112
114 #EL #BI 3 79 113
#DEF 39 93 114 43 40
55 #NS 0 rfl
115 #EC 17 1
116 #EA 115 5
117 #EA 116 2
118 #EA 117 2
119 #EP #BI 6 2 118
120 #EP #BI 3 0 119
121 #EC 18 1
122 #EA 121 5
123 #EA 122 2
124 #EL #BI 6 2 123
125 #EL #BI 3 0 124
#DEF 55 120 125 4
56 #NS 17 symm
126 #EA 115 7
127 #EA 126 5
128 #EA 127 2
129 #EA 115 36
130 #EA 129 5
131 #EA 130 7
132 #EP #BD 46 128 131
133 #EP #BI 45 5 132
134 #EP #BI 6 2 133
135 #EP #BI 3 0 134
136 #EC 47 0 1
137 #EA 136 36
138 #EA 137 7
57 #NI 52 285
58 #NS 46 _@
59 #NS 58 Init
60 #NS 59 Prelude
61 #NS 60 _hyg
62 #NI 61 286
139 #EA 115 40
140 #EA 139 36
141 #EA 140 2
142 #EA 115 95
143 #EA 142 5
144 #EA 143 40
145 #EL #BD 62 141 144
146 #EL #BD 57 36 145
147 #EA 138 146
148 #EC 55 1
149 #EA 148 36
150 #EA 149 7
151 #EA 147 150
152 #EA 151 5
153 #EA 152 2
154 #EL #BD 46 128 153
155 #EL #BI 45 5 154
156 #EL #BI 6 2 155
157 #EL #BI 3 0 156
#DEF 56 135 157 4
63 #NS 12 eta
158 #EC 12 4
159 #EA 158 2
7 #UM 2 4
160 #EC 17 7
161 #EA 158 5
162 #EA 160 161
163 #EC 13 4
164 #EA 163 5
165 #EJ 12 0 2
166 #EA 164 165
167 #EJ 12 1 2
168 #EA 166 167
169 #EA 162 168
170 #EA 169 2
171 #EP #BD 48 159 170
172 #EP #BI 14 22 171
173 #EC 27 0 4
174 #EA 173 5
64 #NS 29 _@
65 #NS 64 test2
66 #NS 65 _hyg
67 #NI 66 99
175 #EA 158 7
176 #EA 160 175
177 #EA 176 5
178 #EA 177 2
179 #EA 158 36
180 #EA 160 179
181 #EA 163 36
182 #EJ 12 0 7
183 #EA 181 182
184 #EJ 12 1 7
185 #EA 183 184
186 #EA 180 185
187 #EA 186 7
188 #EP #BD 46 178 187
189 #EL #BD 67 161 188
190 #EA 174 189
191 #EA 190 2
68 #NI 15 100
69 #NI 16 101
192 #EC 1 7
193 #EA 192 175
70 #NS 58 test2
71 #NS 70 _hyg
72 #NI 71 102
194 #EA 180 7
195 #EA 181 5
196 #EA 195 2
197 #EA 194 196
198 #EC 39 0 7
199 #EA 158 40
200 #EA 198 199
201 #EA 163 40
202 #EA 201 7
203 #EA 202 5
204 #EA 200 203
205 #EA 158 95
206 #EA 160 205
207 #EA 163 95
208 #EA 207 165
209 #EA 208 167
210 #EA 206 209
211 #EA 210 2
212 #EL #BD 48 199 211
213 #EA 204 212
214 #EC 18 7
215 #EA 214 199
216 #EJ 12 0 203
217 #EA 201 216
218 #EJ 12 1 203
219 #EA 217 218
220 #EA 215 219
221 #EA 213 220
222 #EA 221 36
223 #EC 56 7
224 #EA 223 199
225 #EA 224 36
226 #EA 225 203
227 #EA 226 2
228 #EA 222 227
229 #EL #BD 72 197 228
230 #EL #BD 69 193 229
231 #EL #BD 68 5 230
232 #EA 191 231
233 #EA 214 161
234 #EA 233 2
235 #EA 232 234
236 #EL #BD 48 159 235
237 #EL #BI 14 22 236
#DEF 63 172 237 19

JasonGross · 2026-04-22T20:31:40Z

@SkySkimmer Do you have thoughts on this failure?

 File "./rec_single_ctor.v", line 7, characters 0-70:
  - Error:
  - Error at line 126 (for RecInd.casesOn): #DEF 27 51 78 19 4
  - Illegal application: 
  - The term "RecInd_recl" of type
  -  "forall (_UU03b1_ : Type) (P : RecInd _UU03b1_ -> Type),
  -   (forall (a____at___test2__hyg38 : _UU03b1_)
  -      (a____at___test2__hyg40 : list (RecInd _UU03b1_)),
  -    P (RecInd_mk _UU03b1_ a____at___test2__hyg38 a____at___test2__hyg40)) ->
  -   forall r : RecInd _UU03b1_, P r"
  - cannot be applied to the terms
  -  "A" : "Type"
  -  "motive_1" : "RecInd A -> Type"
  -  "fun _ : list (RecInd A) => PUnit" : "list (RecInd A) -> Type"
  -  "fun (a____at___test2__hyg38 : A) (a____at___test2__hyg40 : list (RecInd A))
  -     (_ : PUnit) =>
  -   mk a____at___test2__hyg38 a____at___test2__hyg40"
  -    : "forall (a____at___test2__hyg38 : A)
  -         (a____at___test2__hyg40 : list (RecInd A)),
  -       PUnit ->
  -       motive_1 (RecInd_mk A a____at___test2__hyg38 a____at___test2__hyg40)"
  -  "PUnit_unit" : "PUnit"
  -  "fun (a____at___test2__hyg8 : RecInd A) (_ : list (RecInd A))
  -     (_ : motive_1 a____at___test2__hyg8) (_ : PUnit) =>
  -   PUnit_unit"
  -    : "forall a____at___test2__hyg8 : RecInd A,
  -       list (RecInd A) -> motive_1 a____at___test2__hyg8 -> PUnit -> PUnit"
  -  "t" : "RecInd A"
  - The 3rd term has type "list (RecInd A) -> Type" which should be a subtype of
  -  "forall (a____at___test2__hyg38 : A)
  -     (a____at___test2__hyg40 : list (RecInd A)),
  -   motive_1 (RecInd_mk A a____at___test2__hyg38 a____at___test2__hyg40)".

SkySkimmer · 2026-04-22T20:59:11Z

Seems like it generated a different eliminator than Lean.
Possibly because of nesting? IDK how Lean handles nesting.

SkySkimmer · 2026-04-22T21:03:16Z

For testing this PR you can do an inductive that doesn't use nesting, eg

inductive RecInd.{u} (A : Sort u)
  | mk : A → RecInd A → RecInd A

(this is an empty type but that shouldn't matter for the test)

JasonGross · 2026-05-25T18:37:44Z

@SkySkimmer this now passes CI, what do you think?

SkySkimmer · 2026-05-26T11:41:59Z

-                  else
-                    CErrors.user_err
-                      Pp.(str "cannot project non record " ++ N.pp lean_ind)
+                  let npar = mib.mind_nparams in


move this stuff to a separate function, it's getting too big to stay inline

Are you thinking that we move the entire handling of the Proj case to a separate function, or just the case unfolding?

just the unfolding looks reasonable I think

SkySkimmer · 2026-05-27T07:56:48Z

  let ls = mk_list list char_uinst char chars in
  Constr.(mkApp (mkConstructU ((string, 1), UVars.Instance.empty), [| ls |]))

+let unfold_proj_case env evd ~field ~ind ~indu ~mib ~mip ~args c =


ind is redundant with indu (ind = fst indu)

Suggested change

let unfold_proj_case env evd ~field ~ind ~indu ~mib ~mip ~args c =

let unfold_proj_case env evd ~field ~indu ~mib ~mip ~args c =

and maybe add a comment like "c has type indu applied to args"

SkySkimmer · 2026-05-27T07:58:16Z

+  let (ctx, cty0) = mip.Declarations.mind_nf_lc.(0) in
+  let cty_full =
+    Term.it_mkProd_or_LetIn cty0 ctx
+  in


this function could probably use a reformat now that it is less indented, for instance this letin could be 1 line AFAICT (but it's not the only possible reformat)
not sure how far we have drifted from what ocamlformat would produce, maybe running it but only keeping what it does to this new function would be best

A recursive single-constructor inductive cannot admit eta, so the kernel rejects the primitive-record encoding. The importer's [declare_ind] was coercing every single-constructor, no-index, >=1-relevant-field inductive into a primitive record unconditionally, which made nested-recursive shapes fail at declaration time. Walk the rebuilt constructor Prod chain and check whether the inductive's de Bruijn index (npars+1 in env_ind_params, lifted per binder) occurs in any field type. If so, fall through to the plain Inductive path. The codomain is intentionally skipped: it always mentions the inductive by construction, so testing it there would demote every single-constructor record and break downstream projection uses. Adds tests/rec_single_ctor.v as regression. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Include RecInd.eta theorem in the Lean source and export dump to test that the imported type supports dependent pattern matching, as requested in review. Lean does not grant definitional eta to recursive records. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Remove the auxiliary list inductive from the regression fixture and make RecInd directly recursive through its second constructor field. Regenerate the Lean export with lean4export using explicit names for RecInd and RecInd.eta, and keep the Rocq test focused on the same constructor pattern without list-specific branches.

When an inductive is not declared as a primitive record (e.g., because it is recursive), Lean-side projections (#EJ) can no longer use Rocq primitive projections. Instead, build an inline case/match expression that extracts the appropriate constructor field. This fixes the CI failure where RecInd.eta (which uses projections on the now-non-record RecInd type) could not be imported. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

ind = fst indu, so derive it locally instead of passing both. Also add a doc comment clarifying that c has type indu applied to args. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Pure whitespace/formatting changes, no semantic diff. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Changes made

JasonGross · 2026-06-03T00:00:06Z

@SkySkimmer Updated

SkySkimmer reviewed Apr 20, 2026

View reviewed changes

Comment thread tests/rec_single_ctor.v

JasonGross force-pushed the master-record-fix branch from a33e6b3 to 21a61c0 Compare May 24, 2026 01:36

SkySkimmer previously requested changes May 26, 2026

View reviewed changes

JasonGross requested a review from SkySkimmer May 27, 2026 03:12

SkySkimmer reviewed May 27, 2026

View reviewed changes

ebmoon and others added 8 commits June 2, 2026 23:03

Also prove propositional eta for RecInd directly in Rocq

453df12

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Extract unfold_proj_case from to_constr

75184f9

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Remove redundant ~ind parameter from unfold_proj_case

a426f55

ind = fst indu, so derive it locally instead of passing both. Also add a doc comment clarifying that c has type indu applied to args. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Reformat unfold_proj_case with ocamlformat

fd79d7e

Pure whitespace/formatting changes, no semantic diff. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

JasonGross force-pushed the master-record-fix branch from 0d3ffaa to fd79d7e Compare June 2, 2026 23:03

JasonGross requested a review from SkySkimmer June 2, 2026 23:15

SkySkimmer approved these changes Jun 3, 2026

View reviewed changes

SkySkimmer merged commit 38fb479 into rocq-community:master Jul 1, 2026
1 check passed

	let unfold_proj_case env evd ~field ~ind ~indu ~mib ~mip ~args c =
	let unfold_proj_case env evd ~field ~indu ~mib ~mip ~args c =

Uh oh!

Conversation

ebmoon commented Apr 20, 2026

Summary

Change

Uh oh!

Uh oh!

ebmoon commented Apr 21, 2026

Uh oh!

SkySkimmer commented Apr 21, 2026

Uh oh!

ebmoon commented Apr 21, 2026

Uh oh!

JasonGross commented Apr 22, 2026

Uh oh!

JasonGross commented Apr 22, 2026

Uh oh!

SkySkimmer commented Apr 22, 2026

Uh oh!

SkySkimmer commented Apr 22, 2026

Uh oh!

JasonGross commented May 25, 2026

Uh oh!

SkySkimmer May 26, 2026

Choose a reason for hiding this comment

Uh oh!

JasonGross May 26, 2026

Choose a reason for hiding this comment

Uh oh!

SkySkimmer May 27, 2026

Choose a reason for hiding this comment

Uh oh!

SkySkimmer May 27, 2026

Choose a reason for hiding this comment

Uh oh!

SkySkimmer May 27, 2026

Choose a reason for hiding this comment

Uh oh!

JasonGross commented Jun 3, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants