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: Sep 30 2023 at 06:01 UTC