diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | contrib/subtac/FixSub.v | 18 |
2 files changed, 19 insertions, 1 deletions
@@ -994,7 +994,7 @@ JPROVERVO= CCVO= -SUBTACVO= +SUBTACVO=contrib/subtac/FixSub.vo RTAUTOVO = \ contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v new file mode 100644 index 0000000000..4279c17f57 --- /dev/null +++ b/contrib/subtac/FixSub.v @@ -0,0 +1,18 @@ +Require Import Coq.Init.Wf. + +Section FixPoint. + +Variable A : Set. +Variable R : A -> A -> Prop. +Hypothesis Rwf : well_founded R. +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. + |