Stream: Coq users

Topic: Fixpoint decreasing through N.div_eucl


view this post on Zulip Rodolphe Lepigre (Oct 27 2023 at 23:37):

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?

view this post on Zulip Gaëtan Gilbert (Oct 28 2023 at 07:31):

you can use Acc_intro_generator

view this post on Zulip Paolo Giarrusso (Oct 28 2023 at 07:47):

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