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

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.

Change the 4th argument of `Fix`

from `(fun _ => A)`

to `(fun x => le x (F x) -> A)`

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.

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: May 24 2024 at 22:02 UTC