diff options
| author | coq | 2006-02-22 17:37:43 +0000 |
|---|---|---|
| committer | coq | 2006-02-22 17:37:43 +0000 |
| commit | 41797f79e59eee357d6bcce7385021c680b5de52 (patch) | |
| tree | 5434a54e35aa7ade0e97156405d675ddb1ef568f | |
| parent | 3b132fb78a258f09818cbd68f582a51ec3b589ce (diff) | |
Add vernacular file for subtac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8079 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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. + |