I define a `Fixpoint`

that takes as input `n : N`

, and recurses on the quotient obtained by dividing `n`

by some number with `N.div_eucl`

. To do that, I relied on `Program Fixpoint`

using `{wf N.lt n}`

, and then proved all the proof obligations that I concluded with `Defined`

. However, the term I obtain does not compute. I tracked the problem down to having proved the last proof obligation, which is basically `forall n, Acc N.lt n`

, using `exact N.lt_wf_0`

. It turns out that this term, although it is `Defined`

, relies on `Qed`

-ed stuff, which seem to get in the way.

Basically, I'm not sure how to fix this. I guess I could re-proving `forall n, Acc N.lt n`

myself, and make sure to only use transparent terms, but that seems pretty annoying to do. Am I missing an obvious solution here?

you can use Acc_intro_generator

or stdpp's `wf_guard`

wrapper — that only adds `Strategy 100 [wf_guard].`

over `Acc_intro_generator`

Last updated: Jun 23 2024 at 04:03 UTC