## Stream: Coq users

### Topic: Yet another Well_founded recursion issue

#### Mycroft92 (Jun 14 2022 at 18:29):

Hi everyone,
I was running through Xavier Leroy's Mechanized semantics course (https://github.com/xavierleroy/cdf-mech-sem) and while working through Knaster Tarski's proof (https://xavierleroy.org/cdf-mech-sem/CDF.Fixpoints.html), I hit a snag.

``````Fixpoint iterate (x: A) (acc: Acc gt x) (PRE: le x (F x)) {struct acc}: A :=
let x' := F x in
match eq_dec x x' with
| left E => x
| right NE => iterate x' (iterate_acc x acc PRE NE) (iterate_le x PRE)
end.
``````

The above function fails with ```Recursive call to iterate has principal argument equal to "iterate_acc x acc PRE NE" instead of a subterm of "acc"```, possibly due to a lower coq version I am running . Is there a way to fix this?

I tried the Fix combinator based approach with

``````Definition iterate : A -> A.
refine
(@Fix A gt gt_wf (fun _ => A)
(fun (x: A)  (iterate: forall (y: A), gt y x -> A) =>
let x' := F x in
match eq_dec x x' with
| left E   => x
| right NE => iterate x' _
end)
).
``````

But I need to prove that ` le x x'` which needs me to push the condition `PRE` into the term and I am not able to figure out a way with `Fix`'s type. Any help is greatly appreciated. Thanks

#### Mycroft92 (Jun 14 2022 at 19:06):

Oops figured out my mistake. I made `iterate_acc` opaque by closing it with `Qed` instead of `Defined` thereby not allowing the term to unravel. However I am interested to know if there's a `Fix` based approach to write the same term.

#### Li-yao (Jun 15 2022 at 18:09):

Change the 4th argument of `Fix` from `(fun _ => A)` to `(fun x => le x (F x) -> A)`

#### Mycroft92 (Jun 16 2022 at 16:37):

Li-yao said:

Change the 4th argument of `Fix` from `(fun _ => A)` to `(fun x => le x (F x) -> A)`

Thanks a lot. In hindsight it looks so easy. This was a solution that helped me learn. Thanks again.

#### Mycroft92 (Jun 16 2022 at 16:42):

This is the final solution that works:

``````Definition iterate': forall x : A, le x (F x) -> A.
refine
(@Fix A gt gt_wf (fun (x: A)  => le x (F x) -> A)
(fun (x: A)
(iterate:
forall y : A, gt y x -> (fun (x: A)  => le x (F x) -> A)  y) =>
let x' := F x in
match eq_dec x x' with
| left E   => fun _ => x
| right NE =>  fun ne => iterate x' _ _
end)
).
- split; auto.
- now apply iterate_le.
Defined.
``````

Last updated: Feb 04 2023 at 21:02 UTC