diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-13 09:03:27 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-13 09:03:27 +0000 |
commit | 2b62054dcccae08fdb5b61145e4b84d746e6faf1 (patch) | |
tree | ab7a36991d7c48022f5815b46f97ea656230bd06 /theories/Init/Wf.v | |
parent | 6f9511d66cbca602302d7854b5699e02eb1b026a (diff) |
fichiers prelude Coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@243 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init/Wf.v')
-rwxr-xr-x | theories/Init/Wf.v | 103 |
1 files changed, 103 insertions, 0 deletions
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v new file mode 100755 index 000000000..454ca5dff --- /dev/null +++ b/theories/Init/Wf.v @@ -0,0 +1,103 @@ + +(* $Id$ *) + +(* This module proves the validity of + - well-founded recursion (also called course of values) + - well-founded induction + from a well-founded ordering on a given set *) + +Require Export Logic. +Require Export LogicSyntax. + +(* Well-founded induction principle on Prop *) + +Chapter Well_founded. + + Variable A : Set. + Variable R : A -> A -> Prop. + + (* The accessibility predicate is defined to be non-informative *) + + Inductive Acc : A -> Prop + := Acc_intro : (x:A)((y:A)(R y x)->(Acc y))->(Acc x). + + Lemma Acc_inv : (x:A)(Acc x) -> (y:A)(R y x) -> (Acc y). + Destruct 1; Trivial. + Defined. + + (* the informative elimination : + let Acc_rec F = let rec wf x = F x wf in wf *) + + Section AccRec. + Variable P : A -> Set. + Variable F : (x:A)((y:A)(R y x)->(Acc y))->((y:A)(R y x)->(P y))->(P x). + + Fixpoint Acc_rec [x:A;a:(Acc x)] : (P x) + := (F x (Acc_inv x a) ([y:A][h:(R y x)](Acc_rec y (Acc_inv x a y h)))). + + End AccRec. + + (* A relation is well-founded if every element is accessible *) + + Definition well_founded := (a:A)(Acc a). + + (* well-founded induction on Set and Prop *) + + Hypothesis Rwf : well_founded. + + Theorem well_founded_induction : + (P:A->Set)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a). + Proof. + Intros; Apply (Acc_rec P); Auto. + Save. + + Theorem well_founded_ind : + (P:A->Prop)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a). + Proof. + Intros; Apply (Acc_ind P); Auto. + Qed. + +(* Building fixpoints *) + +Section FixPoint. + +Variable P : A -> Set. +Variable F : (x:A)((y:A)(R y x)->(P y))->(P x). + +Fixpoint Fix_F [x:A;r:(Acc x)] : (P x) := + (F x [y:A][p:(R y x)](Fix_F y (Acc_inv x r y p))). + +Definition fix := [x:A](Fix_F x (Rwf x)). + +(* Proof that well_founded_induction satisfies the fixpoint equation. + It requires an extra property of the functional *) + +Hypothesis F_ext : + (x:A)(f,g:(y:A)(R y x)->(P y)) + ((y:A)(p:(R y x))((f y p)=(g y p)))->(F x f)=(F x g). + +Scheme Acc_inv_dep := Induction for Acc Sort Prop. + +Lemma Fix_F_eq + : (x:A)(r:(Acc x)) + (F x [y:A][p:(R y x)](Fix_F y (Acc_inv x r y p)))=(Fix_F x r). +Intros x r; Elim r using Acc_inv_dep; Auto. +Save. + +Lemma Fix_F_inv : (x:A)(r,s:(Acc x))(Fix_F x r)=(Fix_F x s). +Intro x; Elim (Rwf x); Intros. +Case (Fix_F_eq x0 r); Case (Fix_F_eq x0 s); Intros. +Apply F_ext; Auto. +Save. + + +Lemma fix_eq : (x:A)(fix x)=(F x [y:A][p:(R y x)](fix y)). +Intro; Unfold fix. +Case (Fix_F_eq x). +Apply F_ext; Intros. +Apply Fix_F_inv. +Save. + +End FixPoint. + +End Well_founded. |