Library prelude.PartialFix

Require Import Ensembles.
Require Import Relations.
Set Implicit Arguments.
Section partial_fix.


 Variable T : Type.
 Variable D : Ensemble T.
 Variable lt : T -> T -> Prop.
 Hypothesis lt_D : forall x y, lt x y -> D x.
 Hypothesis gt_D : forall x y, lt x y -> D y.
 Hypothesis D_Acc : forall x, D x -> Acc lt x.

Section Acc_iterP.

 Variable P : T-> Type.

 Variable F : forall x:T, (forall y:T, lt y x -> P y) -> D x -> P x.


Fixpoint Acc_iter_partial (x:T) (H:D x) (a:Acc lt x) {struct a} : P x :=
    F (x:=x)
     (fun (y:T) (h: lt y x) =>
          Acc_iter_partial (lt_D h) (Acc_inv a _ h))H .

End Acc_iterP.

Definition partial_fun_induction P F (x:T) Dx :=
  Acc_iter_partial P F Dx (D_Acc (x:=x) Dx).

Section FixPoint.

 Variable P : T -> Type.

 Variable F : forall x:T, (forall y:T, lt y x -> P y) -> D x -> P x.


Definition PFix (x:T)(H:D x) := Acc_iter_partial P F H (D_Acc H).

 Hypothesis
    F_ext :
      forall (x:T) (f g:forall y:T, lt y x -> P y) (Dx: D x),
        (forall (y:T) (p:lt y x), f y p = g y p) -> F f Dx = F g Dx.

Lemma PFix_F_eq :
   forall (x:T)(H:D x)(r:Acc lt x),
    F (fun (y:T) (h: lt y x) =>
      Acc_iter_partial P F (lt_D h) (Acc_inv r y h))H =
      Acc_iter_partial P F H r.
  Proof.
   destruct r using Acc_inv_dep.
   auto.
 Qed.

  Lemma PFix_F_inv : forall (x:T)(H:D x) (r s:Acc lt x),
       Acc_iter_partial P F H r = Acc_iter_partial P F H s .
  Proof.
   intro x.
   intro H.
   generalize H.
   pattern x.
   apply partial_fun_induction.
   intros.
   rewrite <- (PFix_F_eq H2 r).
   rewrite <- (PFix_F_eq H2 s).
   apply F_ext.
   auto.
   auto.
  Qed.

 Lemma PFix_eq : forall (x:T )(H:D x),
             PFix H =
             F (fun (y:T) (h: lt y x) => PFix (lt_D h)) H.
 Proof.
  intro x; unfold PFix in |- *.
  intro;rewrite <- (PFix_F_eq (x:=x)).
  apply F_ext; intros.
  apply PFix_F_inv.
Qed.

End FixPoint.

End partial_fix.