The Coq mailing list

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

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.