Simpler names for guard checker, allow erasure of case predicate and cast annotation, don't erase lambda annotations when no beta by yannl35133 · Pull Request #22081 · rocq-prover/rocq

yannl35133 · 2026-05-28T17:11:03Z

This does some cleanup, rejects a case that I can't reach and accepts cases that were rejected but not sure why.

thomas-lamiaux · 2026-05-28T20:08:52Z

@yannl35133 could you split it between a renaming commit, and the commit doing the extension of the current guard ?

thomas-lamiaux

Why not allow reduction including in cast or products -- though I am pretty sure it is pointless -- as long it is makes the guard more uniform.

Renaming really need to be done in a separate PR though, the changes are though to read

thomas-lamiaux · 2026-05-29T11:51:30Z

       level of the redex stack *)
-    let need_reduce, rs = check_rec_call renv rs c in
-    check_rec_call_state renv need_reduce [] rs (fun () -> None)
+    check_in_stack renv [] rs c


it seems like you did more than renaming, because before this was checking the stack.
Might, just be the git diff that is bad, but this should really be two PR otherwise it is though to follow

Also is there really a point for one line aliases, it just makes the code more complicated to navigate for no reason

because before this was checking the stack

How so? The stack is always empty, and the redex stack is not checked by check_state / check_needreduce, only its needreduce argument. Here, since there is no possibility of reduction, it reports directly to the top of the preexisting redex stack directly.

Also is there really a point for one line aliases, it just makes the code more complicated to navigate for no reason

I kept the same functions as before, just renamed and simplified them. I don't find such aliases too distracting.

For the first point, you are right I got confused.
What I meant is that currently it does:

let need_reduce, rs = check_rec_call renv rs c in check_rec_call_state renv need_reduce [] rs (fun () -> None)

which is the same as

let need_reduce, rs = check_rec_call renv rs c in match need_reduce with | NoNeedReduce -> rs | NeedReduce _ -> need_reduce :: List.tl rs

so it pushed NoNeedReduce and if it figures out it is needed reduction propagates up the stack since there is no redex here to reduce and discard the term. That is no longer seems to be the case with your definition ? Or am I misunderstanding when it is used ?

I don't find such aliases too distracting.

I do, it makes navigating the code awful I spend my time jumping from one part of the code to another. The point of aliasing is to make the code clearer either:

by hiding some recurring small but not trivial piece of code behind a notation

by giving intuition on what is going on by giving a nice name to a piece of code

Here, check_empty_stack could be a name compare to check_in_stack (subterm stack right ?), but ideally we would have a name that reflect the status of the term it is applied to. From this perspective check_not_redex or innert are not bad names to describe some class of term that the stack does not apply to. It also makes it easier to specify or explains.

so it pushed NoNeedReduce and if it figures out it is needed reduction propagates up the stack since there is no redex here to reduce and discard the term. That is no longer seems to be the case with your definition ? Or am I misunderstanding when it is used ?

When it figures out reduction is needed when inside the term, instead of reporting to the specific redex level that got added here, it reports it to the level right above. Thus, the step of transmitting the needreduce to the level right above is happening, but more directly.

Here, check_empty_stack could be a name compare to check_in_stack (subterm stack right ?), but ideally we would have a name that reflect the status of the term it is applied to. From this perspective check_not_redex or innert are not bad names to describe some class of term that the stack does not apply to. It also makes it easier to specify or explains.

check_term is supposed to mean "do the normal checks", check_in_stack means "do the normal checks, but the stack is not trivial" and check_in_redex means "do the checks but you're in a redex so tell me if reduction is needed immediately". I thought those names were rather explicit.

Ok I get now. I still am a bit confused by the names in part by the description of each function 😓
I would prefer names that refer to the meaning rather than the implementation.

What about check_applied_term for check_in_stack instead ?

check_in_redex is rather clear, but I would prefer sth explicit like check_term_need_erasing.
It would be great to keep the prefix check_term to indicate the stack is empty

No idea for check_needreduce. The name is not bad, but I keep understanding you check if you need to reduce like a boolean test, whereas it checks if it needs reduces, if so reduces and check the reduce term. But might, just be me 😅

What do you think ?

2: If you want something explicit, it would be check_term_allowing_erasing, but it's prohibitively long
1: It can be check_term_in_stack, not sure it helps. I don't understand why you don't like the word "stack"
3: Would you prefer enforce_needreduce ? There is purposefully no underscore between need and reduce, since it's referring to the type and not the verbs.

2: If you want something explicit, it would be check_term_allowing_erasing, but it's prohibitively long

What about check_term_erasable / check_erasable_term ?

1: It can be check_term_in_stack, not sure it helps.
I don't understand why you don't like the word "stack"

check_term_in_stack is better, but still I don't like it much as the stack is an implementation detail, it does not reflect the status of the term being checked. I would prefer sth like check_applied_term or check_term_applied that reflect we are checking an applied term.

3: Would you prefer enforce_needreduce ?

maybe it is better 🤷

thomas-lamiaux · 2026-05-29T12:17:46Z

+    check_in_stack renv [] rs c

-  and check_rec_call renv rs c =
+  and check_erasable renv rs c =


Should it be check_need_erasure

No, it doesn't need anything yet. I found a better name because erasability is not the real focus either.

thomas-lamiaux

If we can converge and merge into one or two reviews.
The changes make sense to me.
Maybe add an example in the test-suite.

If we are going to do a cleanup I suggest defining auxiliary functions for the reduction function passed to check_needreduce of Fix,Case,Proj like reduce_fix, reduce_case etc... It would make it easier to follow the check_in_stack function

thomas-lamiaux · 2026-05-29T14:18:56Z

       level of the redex stack *)
-    let need_reduce, rs = check_rec_call renv rs c in
-    check_rec_call_state renv need_reduce [] rs (fun () -> None)
+    check_in_stack renv [] rs c


For the first point, you are right I got confused.
What I meant is that currently it does:

let need_reduce, rs = check_rec_call renv rs c in check_rec_call_state renv need_reduce [] rs (fun () -> None)

which is the same as

let need_reduce, rs = check_rec_call renv rs c in match need_reduce with | NoNeedReduce -> rs | NeedReduce _ -> need_reduce :: List.tl rs

so it pushed NoNeedReduce and if it figures out it is needed reduction propagates up the stack since there is no redex here to reduce and discard the term. That is no longer seems to be the case with your definition ? Or am I misunderstanding when it is used ?

thomas-lamiaux · 2026-05-29T14:21:07Z

       level of the redex stack *)
-    let need_reduce, rs = check_rec_call renv rs c in
-    check_rec_call_state renv need_reduce [] rs (fun () -> None)
+    check_in_stack renv [] rs c


I don't find such aliases too distracting.

I do, it makes navigating the code awful I spend my time jumping from one part of the code to another. The point of aliasing is to make the code clearer either:

by hiding some recurring small but not trivial piece of code behind a notation

by giving intuition on what is going on by giving a nice name to a piece of code

Here, check_empty_stack could be a name compare to check_in_stack (subterm stack right ?), but ideally we would have a name that reflect the status of the term it is applied to. From this perspective check_not_redex or innert are not bad names to describe some class of term that the stack does not apply to. It also makes it easier to specify or explains.

thomas-lamiaux · 2026-06-01T08:43:25Z

I have looking at it again, what do you mean by "rejects a case that I can't reach"

thomas-lamiaux · 2026-06-01T09:59:17Z

+        let rs =
+          if erase_ty then
+            snd (check_in_redex renv rs ty)
+            (* Erase the type annotation *)
+          else
+            check_term renv rs ty
+        in


I don't understand this change ?
It no longer unfolds the lambda if there is an argument in the stack and ty needs unfolding

In a lambda, you will check the body, possibly substituted/in the context extended with the argument.
If a beta-redex happens, you can afford to ignore the needreduce status asked for by checking the type annotation since it's gonna be erased. If there is no beta-redex or if it is fake (SArg argument), then the type is not erased and we need to enforce this.
Also, this didn't change, but nested fixpoints never erase lambda type annotations.

So you are saying we don't need to check the status of the type as it is erased altogether and cannot interact after being substituted. It is a bit weird to me that the guard does not properly do the reductions, but I guess it can be seen as an optimisation. But then as for cast, I don't get why not just use check_term. Do you need to push NeedReduce to get the good indexing of the redex stack or sth ?

thomas-lamiaux · 2026-06-01T15:04:52Z

            let decrArg = recindxs.(i) in
            let nbodies = Array.length bodies in
-            let rs' = Array.fold_left (check_inert_subterm_rec_call renv) (NoNeedReduce::rs) typarray in
+            let rs = push_redex rs in


I find it confusing that push_redex is sometimes used explicitly like here, but indirectly in check_in_redex in let in

I get it, but it's the same as the existing, pushing once to avoid folding the push and pop needlessly.
I could do the same for LetIn and never use check_in_redex, but I'm not sure it would be clearer.

yeah, I guess it makes sense to have this alias

thomas-lamiaux · 2026-06-01T15:05:40Z

-            let rs = check_inert_subterm_rec_call renv rs t in
-            let rs = check_rec_call_stack renv stack rs c in
-            rs
+            let _, rs = check_in_redex renv rs t in


I don't understand why use check_in_redex here if no reduction is performed and the top is discarded

If the top is discarded, it means you accept unapplied recursive calls in this part. In this case, it's because there is an implicit redex in Cast that looks like Cast (c, _, t) ⇝ c, so t is erasable.

My question is why push a NotReduce in the stack to ignore it afterwards

thomas-lamiaux · 2026-06-09T09:38:49Z

-              | [] ->
-                check_rec_call_stack (push_var_renv renv (redex_level rs) (x,a)) [] rs b
-            end
+      | Lambda (na, ty, b) ->


no longer indented properly

yannl35133 requested a review from a team as a code owner May 28, 2026 17:11

yannl35133 added the request: full CI Use this label when you want your next push to trigger a full CI. label May 28, 2026

coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label May 28, 2026

yannl35133 mentioned this pull request May 28, 2026

Do not accept erasable subterm in the types of letin and lambda abstraction #22078

Closed

6 tasks

thomas-lamiaux requested changes May 29, 2026

View reviewed changes

yannl35133 added 3 commits May 29, 2026 15:26

Simpler names for guard checker functions

46b2bd4

Add abstraction to redex levels and simplify how it's handled

511ebb3

Leave pop_argument to deal with an empty stack

9dbdb01

yannl35133 force-pushed the cleaner-redex-stack branch from e43c09d to ff232c8 Compare May 29, 2026 13:51

coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label May 29, 2026

thomas-lamiaux requested changes May 29, 2026

View reviewed changes

thomas-lamiaux self-assigned this May 29, 2026

Allow erasure of case predicate and cast annotation

f13b215

thomas-lamiaux reviewed Jun 1, 2026

View reviewed changes

thomas-lamiaux reviewed Jun 9, 2026

View reviewed changes

yannl35133 added kind: cleanup Code removal, deprecation, refactorings, etc. part: fixpoints About Fixpoint, fix and mutual statements request: full CI Use this label when you want your next push to trigger a full CI. labels Jun 9, 2026

yannl35133 force-pushed the cleaner-redex-stack branch from ff232c8 to f13b215 Compare June 9, 2026 16:34

coqbot-app Bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Jun 9, 2026

yannl35133 mentioned this pull request Jun 9, 2026

Guard fix cleaner #22109

Draft

Conversation

yannl35133 commented May 28, 2026

Uh oh!

thomas-lamiaux commented May 28, 2026

Uh oh!

thomas-lamiaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thomas-lamiaux May 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thomas-lamiaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thomas-lamiaux May 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

thomas-lamiaux commented Jun 1, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

thomas-lamiaux May 29, 2026 •

edited

Loading

thomas-lamiaux May 29, 2026 •

edited

Loading