The Coq mailing list

[Madhukar <madhukar.yerraguntla AT gmail.com>]

Hi Coq-club,

I am trying to do Xavier Leroy's course exercises [1] but with techniques picked up from CPDT [2] book. Apologies for the longish mail.

In the module on fixpoints and knaster-tarski fixpoint proof, I defined the iterate function using Fix function this way: (in the module they define with structural recursion using accessibility relation on x)

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 nle => iterate x' _ _

         end)

      ).

      - split; auto.

      - now apply iterate_le.

Defined.

While trying to prove the following result, I am stuck at a weird goal imposed by Fix_eq.

Lemma iterate_fix_eq': forall x PRE, (iterate' x PRE) = (F (iterate' x PRE)).

Proof.

  induction x using (well_founded_induction gt_wf). intros; unfold iterate'.

  rewrite (Fix_eq gt_wf (fun (x: A)  => le x (F x) -> A)). 

     - destruct (eq_dec x (F x))  eqn:H_eq'; auto. fold iterate'. apply H; split; auto. (* proves the main result *)

     - intros. destruct (eq_dec x0 (F x0))  eqn:H_eq'; auto. (* stuck here *)

I also have an additional hypothesis for convenience: 

 Hypothesis eq_is_eq: forall x y, eq x y -> x = y.

The goal is: 

• x0: A
• f, g: forall y : A, gt y x0 -> le y (F y) -> A
• H0: forall (y : A) (p : gt y x0), f y p = g y p
• n: ~ eq x0 (F x0)
• H_eq': eq_dec x0 (F x0) = right n 

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

(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))

As you can see, I need to prove that the result of the recursive calls are the same. I am in fact able to prove a modified version of the same goal:

(forall (nle:le x0 (F x0)),  f (F x0) (conj nle n)  = g (F x0) (conj nle n))

My induction hypothesis gives me what I need to prove but the extra `(iterate_le x0 nle) `  arg is throwing me off and I am not able to proceed further since congruence or rewrite isn't working here. Any pointers would be very helpful. Thanks in advance for the help.

[1] https://github.com/xavierleroy/cdf-mech-sem/blob/master/Fixpoints.v

[2] http://adam.chlipala.net/cpdt/cpdt.pdf

Regards,

Madhukar