From 127ff9178265072e05900f31bec0ccb5d02c1911 Mon Sep 17 00:00:00 2001 From: mohring Date: Fri, 9 May 2003 14:40:44 +0000 Subject: ajout inverse relation bien fondee git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4000 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Wellfounded/Inverse_Image.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'theories/Wellfounded') diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v index f29151cae..9afffc95c 100644 --- a/theories/Wellfounded/Inverse_Image.v +++ b/theories/Wellfounded/Inverse_Image.v @@ -33,6 +33,26 @@ Section Inverse_Image. Red; Intros; Apply Acc_inverse_image; Auto. Qed. + Variable F : A -> B -> Prop. + Local RoF : A -> A -> Prop := [x,y] + (EX b : B | (F x b) & (c:B)(F y c)->(R b c)). + +Lemma Acc_inverse_rel : + (b:B)(Acc B R b)->(x:A)(F x b)->(Acc A RoF x). +Induction 1; Intros. +Constructor; Intros. +Case H3; Intros. +Apply (H1 x1); Auto. +Save. + + +Theorem wf_inverse_rel : + (well_founded B R)->(well_founded A RoF). + Red; Constructor; Intros. + Case H0; Intros. + Apply (Acc_inverse_rel x); Auto. +Save. + End Inverse_Image. -- cgit v1.2.3