diff options
Diffstat (limited to 'contrib/subtac/FixSub.v')
-rw-r--r-- | contrib/subtac/FixSub.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v new file mode 100644 index 00000000..bbf722db --- /dev/null +++ b/contrib/subtac/FixSub.v @@ -0,0 +1,22 @@ +Require Import Wf. + +Section Well_founded. +Variable A : Set. +Variable R : A -> A -> Prop. +Hypothesis Rwf : well_founded R. + +Section FixPoint. + +Variable P : A -> Set. + +Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. + +Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x := + F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y) + (Acc_inv r (proj1_sig y) (proj2_sig y))). + +Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x). + +End FixPoint. + +End Well_founded. |