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.