Library hydras.Prelude.Restriction

From Coq Require Import Wellfounded Ensembles Relations.


Definition restrict {A:Type}(E: Ensemble A)(R: relation A) :=
  fun a b ⇒ E a ∧ R a b ∧ E b.


Section restricted_recursion.

  Variables (A:Type)(E:A→Prop)(R:A→A→Prop).


  Definition well_founded_restriction :=
    ∀ (a:A), E a → Acc (restrict E R) a.

  Definition well_founded_restriction_rect :
    well_founded_restriction →
    ∀ X : A → Type,
      (∀ x : A, E x → (∀ y : A, In _ E y → R y x → X y) → X x) →
      ∀ a : A, In _ E a → X a.

End restricted_recursion.

Section Fix.
  Variables (A:Type)(E: Ensemble A)(R: relation A).
  Hypothesis Hwf : well_founded_restriction A E R.


  Variable P : A → Type.
  Variable F : (∀ x : A, E x → (∀ y : A, In _ E y → R y x → P y) → P x).

  Lemma restriction_fwd : ∀ x y (H: restrict E R x y), E x.

  Definition restrict_build x y (Hx: E x)(Hy : E y)(H : R x y) :=
    conj Hx (conj H Hy) .

  Fixpoint FixR_F (x:A)(Hx : E x)(a: Acc (restrict E R)x ) : P x :=
    F _ Hx (fun (y:A) (h0 : E y) (h : R y x) ⇒
              FixR_F y (restriction_fwd y x
                                        (restrict_build y x h0 Hx h))
                     (Acc_inv a (restrict_build y x h0 Hx h))).
  Lemma FixR_F_eq :
    ∀ (x:A)(Hx : E x) (r: Acc (restrict E R) x) ,
      F _ Hx (fun (y : A)( h0 : E y) (h : R y x) ⇒
                 FixR_F y (restriction_fwd y x (restrict_build y x h0 Hx h))
                        (Acc_inv r (restrict_build y x h0 Hx h)))=
      FixR_F x Hx r.

  Hypothesis Rwf : well_founded_restriction A E R.

  Definition FixR (x:A)(H:E x) := FixR_F x H (Rwf x H).

End Fix.

Arguments FixR [A E R P] _ _ _ _.