Library prelude.AccP
Section restricted_recursion.
Variables (A:Type)(P:A->Prop)(R:A->A->Prop).
Definition restrict (a b:A):Prop :=
P a /\ R a b /\ P b.
Definition well_founded_P := forall (a:A), P a -> Acc restrict a.
Definition P_well_founded_induction_type :
well_founded_P ->
forall X : A -> Type,
(forall x : A, P x -> (forall y : A,P y-> R y x -> X y) -> X x) ->
forall a : A, P a -> X a.
intros W X H a.
pattern a; eapply well_founded_induction_type with (R:=restrict).
unfold well_founded.
split.
unfold well_founded_P in W.
intros; apply W.
case H0.
auto.
intros; apply H.
auto.
intros; apply X0.
unfold restrict; auto.
auto.
Defined.
End restricted_recursion.
Theorem AccElim3 :
forall A B C:Type,
forall (RA:A->A->Prop)
(RB:B->B->Prop)
(RC:C->C->Prop),
forall (P : A -> B -> C -> Prop),
(forall x y z,
(forall (t : A), RA t x ->
forall y' z', Acc RB y' -> Acc RC z' ->
P t y' z') ->
(forall (t : B), RB t y ->
forall z', Acc RC z' -> P x t z') ->
(forall (t : C), RC t z -> P x y t) ->
P x y z) ->
forall x y z, Acc RA x -> Acc RB y -> Acc RC z -> P x y z.
Proof.
intros A B C RA RB RC P H x y z Ax; generalize y z; clear y z.
elim Ax; clear Ax x; intros x _ Hrecx y z Ay; generalize z; clear z.
elim Ay; clear Ay y;
intros y _ Hrecy z Az; elim Az; clear Az z; auto.
Qed.
Theorem accElim3:
forall (A B C:Set)(RA : A -> A ->Prop) (RB : B-> B-> Prop)
(RC : C -> C -> Prop)(P : A -> B -> C -> Prop),
(forall x y z ,
(forall (t : A), RA t x -> P t y z) ->
(forall (t : B), RB t y -> P x t z) ->
(forall (t : C), RC t z -> P x y t) -> P x y z) ->
forall x y z, Acc RA x -> Acc RB y -> Acc RC z -> P x y z.
intros A B C RA RB RC P H x y z Ax Ay Az.
generalize Ax Ay Az.
pattern x, y, z;
eapply AccElim3 with (RA:=RA)(RB:=RB)(RC:=RC) ;eauto.
intros; apply H.
intros;apply H0; auto.
eapply Acc_inv;eauto.
intros;apply H1; auto.
eapply Acc_inv;eauto.
intros;apply H2; auto.
eapply Acc_inv;eauto.
Qed.