diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /contrib/subtac/FixSub.v | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
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. |