The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Madhukar,

I did investigate your question a bit further and I found a solution

you might like better. It involves using "Fix_F" instead of "Fix".

Notice that "Fix" is defined in terms of "Fix_F" anyway in the

StdLib. Using "Fix_F", you get definitional equalities and

you can prove the fixpoint equations "fixpoint' = F fixpoint'"

w/o the assumption "eq x x".

Hence, the extentionality assumption is only required when

manipulating "Fix", and not with "Fix_F".

See below,

Best regards,

Dominique

PS: notice that the proof of iterate'_eq uses *dependent

recursion* on "Acc" via "Acc_inv_dep" instead of having

to assume gt_wf, so this hypothesis can be delayed

further, just before the actual definition of the "fixpoint'".

-----------------

Section KNASTER_TARSKI.

Variable A: Type.

Variable eq: A -> A -> Prop.

Variable eq_dec: forall (x y: A), {eq x y} + {~eq x y}.

Variable le: A -> A -> Prop.

Hypothesis le_trans: forall x y z, le x y -> le y z -> le x z.

Hypothesis eq_le: forall x y, eq x y -> le y x.

Definition gt (x y: A) := le y x /\ ~eq y x.

Variable bot: A.

Hypothesis bot_smallest: forall x, le bot x.

Section FIXPOINT.

Variable F: A -> A.

Hypothesis F_mon: forall x y, le x y -> le (F x) (F y).

Lemma iterate_le:

  forall (x: A) (PRE: le x (F x)), le (F x) (F (F x)).

Proof. intros; apply F_mon, PRE. Qed.

Let P x := le x (F x) -> A.

Local Definition G x (loop : forall y, gt y x -> P y) hx := 

  let x' := F x in 

  match eq_dec x x' with

  | left e   => x

  | right ne => loop x' (conj hx ne) (F_mon _ _ hx)

  end.

Definition iterate' := Fix_F P G.

Lemma iterate'_eq x (a : Acc gt x) PRE : eq (iterate' x a PRE) (F (iterate' x a PRE)).

Proof.

  induction a as [ x ] in PRE |- * using Acc_inv_dep; cbn; unfold G.

  destruct (eq_dec x (F x)); eauto.

Qed.

Hypothesis gt_wf: well_founded gt.

Definition fixpoint' := iterate' bot (gt_wf bot) (bot_smallest (F bot)).

Theorem fixpoint'_eq : eq fixpoint' (F fixpoint').

Proof. apply iterate'_eq. Qed.

End FIXPOINT.

End KNASTER_TARSKI.

Check fixpoint'_eq.

Require Import Extraction.

Extraction Inline G.

Recursive Extraction fixpoint'.

---

De: "Madhukar" <madhukar.yerraguntla AT gmail.com>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Dimanche 29 Janvier 2023 13:26:55
Objet: Re: [Coq-Club] Stuck with weird goal imposed by Fix_eq

Hi Dominique,

Thanks a lot for the clear explanation and the fixed code(bad pun?). I am really grateful for the help. I will get back to you in case of any further questions.

Thanks,

Madhukar

 

On Sun, Jan 29, 2023 at 3:22 PM Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> wrote:

Hi Madhukar,

You are trying to prove fixpoint equations for the Fix operator

and this can sometimes be difficult indeed. 

======================================================

(fun nle : le x0 (F x0) => f (F x0) (conj nle n) (iterate_le x0 nle)) =

(fun nle : le x0 (F x0) => g (F x0) (conj nle n) (iterate_le x0 nle))

Typically that one above is going to get you stuck for a while ...

Indeed, it is an identity between two *functions* and there

is no way out of it, unless assuming FunExt. Which I

guess you do not want to do.

The thing is, the generic fixpoint equation for "Fix"

called "Fix_eq" is *too restrictive* when defining values

in a function space, which is what you do with

| Definition iterate': forall x : A, le x (F x) -> A.

because the output value is in  "P x := le x (F x) -> A"

and "P x" is a space of functions.

To work this out, you have to relax the fixpoint

equation "Fix_eq" to an arbitrary binary relation over 

"P x", ie not just (Coq defined) equality over "P x".

Then you can use this relaxation with extensional

equality for functions, instead of (Coq defined) equality.

Below I suggest such a relaxation "Fix_equiv"

which works in your case, with the noticable

further assumption that eq (from Xavier Leroy's

code assumptions) must be reflexive,

something which is not assumed in XL's code.

I will investage this further but here is some code

that works using "Fix" (and hence "Fix_F") and

"Fix_equiv".

Best regards,

Dominique

-----------

Section Acc_eq.

  Context {X : Type} (R : X -> X -> Prop).

  Inductive Acc_eq : forall {x}, Acc R x -> Acc R x -> Prop := 

    | Acc_eq_intro : forall x H1 H2, (forall y Hy, Acc_eq (H1 y Hy) (H2 y Hy)) -> Acc_eq (Acc_intro x H1) (Acc_intro _ H2).

  Hint Constructors Acc_eq : core.

  Theorem Acc_eq_total : forall {x} (H1 H2 : Acc R x), Acc_eq H1 H2.

  Proof. induction H1 using Acc_inv_dep; intros []; auto. Qed.

End Acc_eq.

Section Fix_equiv.

  (* This one generalizes Fix_eq replacing equality eq/= 

     with an arbitrary (polymorphic) binary relation on P x *)

  Variables (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)

            (P : A -> Type) (E : forall x, P x -> P x -> Prop).

  Infix "~~" := (E _) (at level 70).

  

  Variables (F : forall x, (forall y, R y x -> P y) -> P x)

            (F_ext : forall x (f g : forall y, R y x -> P y),

                       (forall y p, f y p ~~ g y p) -> F x f ~~ F x g).

  Lemma Fix_F_ext x (p q : Acc R x) : Fix_F P F p ~~ Fix_F P F q.

  Proof. induction (Acc_eq_total R p q); eauto. Qed.

  Lemma Fix_F_equiv x r : F x (fun y p => Fix_F P F (Acc_inv r p)) ~~ Fix_F P F r.

  Proof. rewrite Fix_F_eq; apply Fix_F_ext. Qed.

  Hint Resolve Fix_F_ext : core.

  Theorem Fix_equiv x : Fix Rwf P F x ~~ F x (fun y _ => Fix Rwf P F y).

  Proof. unfold Fix; destruct (Rwf x); simpl; auto. Qed.

End Fix_equiv.

(* Compare how Fix_equiv generalizes Fix_eq *)

Check Fix_eq.

Check Fix_equiv.

Section KNASTER_TARSKI.

(** Consider a type [A] equipped with a decidable equality [eq] and a

    transitive ordering [le]. *)

Variable A: Type.

Variable eq: A -> A -> Prop.

Variable eq_dec: forall (x y: A), {eq x y} + {~eq x y}.

Variable le: A -> A -> Prop.

Hypothesis le_trans: forall x y z, le x y -> le y z -> le x z.

Hypothesis eq_le: forall x y, eq x y -> le y x.

(** This is the strict order induced by [le].  We assume it is well-founded:

    all strictly ascending chains are finite. *)

Definition gt (x y: A) := le y x /\ ~eq y x.

Hypothesis gt_wf: well_founded gt.

Section FIXPOINT.

(** Let [F] be a monotonically increasing function from [A] to [A]. *)

Variable F: A -> A.

Hypothesis F_mon: forall x y, le x y -> le (F x) (F y).

Lemma iterate_acc:

  forall (x: A) (acc: Acc gt x) (PRE: le x (F x)) (NEQ: ~eq x (F x)), Acc gt (F x).

Proof.

  intros. apply Acc_inv with x; auto. split; auto.

Defined.

Lemma iterate_le:

  forall (x: A) (PRE: le x (F x)), le (F x) (F (F x)).

Proof. intros; apply F_mon, PRE. Qed.

Let P x := le x (F x) -> A.

Let EQ x (u v : P x) := forall p, eq (u p) (v p).

Let G x (loop : forall y, gt y x -> P y) hx := 

  let x' := F x in 

  match eq_dec x x' with

  | left e   => x

  | right ne => loop x' (conj hx ne) (F_mon _ _ hx)

  end.

Let Fix_G_equiv := Fix_equiv _ _ gt_wf P EQ G.

(* Cannot get rid of that one ... *)

Hypothesis eq_refl : forall x, eq x x.

Let G_ext x (f g : forall y : A, gt y x -> P y) :

       (forall (y : A) (p : gt y x), EQ y (f y p) (g y p)) -> EQ x (G x f) (G x g).

Proof.

  intros H p.

  unfold G.

  destruct (eq_dec x (F x)).

  + apply eq_refl.

  + apply H.

Qed.

Definition iterate' x : P x := Fix gt_wf _ G x. 

Fact iterate'_eq x (PRE : le x (F x)) :

      eq (iterate' x PRE) (G x (fun y _ => iterate' y) PRE).

Proof. apply Fix_G_equiv, G_ext. Qed.

End FIXPOINT.

End KNASTER_TARSKI.