@mei are you volunteering to give me a code review instead? https://github.com/rrika/cumulative/blob/master/src/cumulative_v2.v

EDIT: yeah, it's doing in hours what would've taken me months

@rrika I’m not opposed in general to giving some feedback on Rocq code, but yours looks quite undocumented and cryptic – one thing that helps a lot is stating the main definitions in natural language as comments next to the formal ones. helps with the “what the hell is a_lct supposed to mean”.

there is one general thing that I can give a recommendation on: if at any point you have more than one goal, use some kind of explicit separation between the subgoals (bulletpoints or curly braces).

otherwise, if anything at all ever happens to make a proof not go through, such as a coq update or a refactoring, you’ll find it very hard to figure out what’s even supposed to be happening, let alone what went wrong

you can use the Set Default Goal Selector "!". directive to enforce this, and I very much recommend doing so (this way, if a tactic unexpectedly leaves more than one subgoal, you’ll also get an error immediately instead of having to reconstruct what happened later)

(PS. i’d argue that if you feel like it’d take you months to do what claude is doing for you, then by relying on claude, you’re depriving yourself of a lot of learning experiences you’d encounter along the way if you did it yourself, and stunting your growth as a result)