Require Import Coq.Classes.RelationClasses.

Set Implicit Arguments.
Set Strict Implicit.

Fixpoint guard A (R : A -> A -> Prop) (n : nat) (wfR : well_founded R)
  {struct n}: well_founded R :=
  match n with
    | 0 => wfR
    | S n => fun x => Acc_intro x (fun y _ => guard n (guard n wfR) y)
  end.

Section setoid_fix.
  Variables (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R).
  Variables (P : A -> Type)
            (F : forall x : A, (forall y : A, R y x -> P y) -> P x).
  Variable r : forall x : A, P x -> P x -> Prop.
  Hypothesis Hstep : forall (x : A) (f g : forall y : A, R y x -> P y),
                       (forall (y : A) (p : R y x), r (f y p) (g y p)) ->
                       r (@F x f) (@F x g).

  Lemma Fix_F_equiv_inv
  : forall (x : A) (r' s' : Acc R x),
      r (Fix_F _ F r') (Fix_F _ F s').
  Proof.
(* Goal: forall (x : A) (r' s' : @Acc A R x), @r x (@Fix_F A R P F x r') (@Fix_F A R P F x s') *)
    intro x; induction (Rwf x); intros.
(* Goal: @r x (@Fix_F A R P F x r') (@Fix_F A R P F x s') *)
    rewrite <- (Fix_F_eq _ F r'); rewrite <- (Fix_F_eq _ F s'); intros.
(* Goal: @r x (@F x (fun (y : A) (p : R y x) => @Fix_F A R P F y (@Acc_inv A R x r' y p))) (@F x (fun (y : A) (p : R y x) => @Fix_F A R P F y (@Acc_inv A R x s' y p))) *)
    eapply Hstep.
(* Goal: forall (y : A) (p : R y x), @r y (@Fix_F A R P F y (@Acc_inv A R x r' y p)) (@Fix_F A R P F y (@Acc_inv A R x s' y p)) *)
    eauto.
  Qed.

  Theorem Fix_equiv
  : forall x : A,
      r (Fix Rwf P F x) (@F x (fun (y : A) (_ : R y x) => Fix Rwf P F y)).
  Proof.
(* Goal: forall x : A, @r x (@Fix A R Rwf P F x) (@F x (fun (y : A) (_ : R y x) => @Fix A R Rwf P F y)) *)
    intro x; unfold Fix.
(* Goal: @r x (@Fix_F A R P F x (Rwf x)) (@F x (fun (y : A) (_ : R y x) => @Fix_F A R P F y (Rwf y))) *)
    rewrite <- Fix_F_eq.
(* Goal: @r x (@F x (fun (y : A) (p : R y x) => @Fix_F A R P F y (@Acc_inv A R x (Rwf x) y p))) (@F x (fun (y : A) (_ : R y x) => @Fix_F A R P F y (Rwf y))) *)
    apply Hstep; intros.
(* Goal: @r y (@Fix_F A R P F y (@Acc_inv A R x (Rwf x) y p)) (@Fix_F A R P F y (Rwf y)) *)
    apply Fix_F_equiv_inv.
  Qed.
End setoid_fix.