From cc1be0bf512b421336e81099aa6906ca47e4257a Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 17 Apr 2002 11:30:23 +0000 Subject: Uniformisation (Qed/Save et Implicits Arguments) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Wellfounded/Disjoint_Union.v | 2 +- theories/Wellfounded/Inclusion.v | 4 ++-- theories/Wellfounded/Inverse_Image.v | 6 +++--- theories/Wellfounded/Lexicographic_Product.v | 14 +++++++------- theories/Wellfounded/Union.v | 6 +++--- 5 files changed, 16 insertions(+), 16 deletions(-) (limited to 'theories/Wellfounded') diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index 5cb4b79d5..ac3233704 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -36,7 +36,7 @@ Proof. Apply Acc_intro;Intros. Inversion_clear H3;Auto with sets. Apply acc_A_sum;Auto with sets. -Save. +Qed. Lemma wf_disjoint_sum: diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index db9cfe227..d2658e717 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -20,7 +20,7 @@ Section WfInclusion. Proof. Induction 2;Intros. Apply Acc_intro;Auto with sets. - Save. + Qed. Hints Resolve Acc_incl. @@ -28,6 +28,6 @@ Section WfInclusion. (inclusion A R1 R2)->(well_founded A R2)->(well_founded A R1). Proof. Unfold well_founded ;Auto with sets. - Save. + Qed. End WfInclusion. diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v index 3e4bca83f..f29151cae 100644 --- a/theories/Wellfounded/Inverse_Image.v +++ b/theories/Wellfounded/Inverse_Image.v @@ -23,15 +23,15 @@ Section Inverse_Image. Apply Acc_intro; Intros. Apply (H1 (f y0)); Try Trivial. Rewrite H2; Trivial. - Save. + Qed. Lemma Acc_inverse_image : (x:A)(Acc B R (f x)) -> (Acc A Rof x). Intros; Apply (Acc_lemma (f x)); Trivial. - Save. + Qed. Theorem wf_inverse_image: (well_founded B R)->(well_founded A Rof). Red; Intros; Apply Acc_inverse_image; Auto. - Save. + Qed. End Inverse_Image. diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index c57a75133..3e8ba318a 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -74,7 +74,7 @@ Proof. Apply acc_A_B_lexprod;Auto with sets;Intros. Red in wfB. Auto with sets. -Save. +Qed. End WfLexicographic_Product. @@ -104,7 +104,7 @@ Proof. (Apply left_lex;Auto with sets). (Apply right_lex;Auto with sets). -Save. +Qed. i*) Lemma Acc_symprod: (x:A)(Acc A leA x)->(y:B)(Acc B leB y) @@ -116,7 +116,7 @@ Proof. Inversion_clear H5;Auto with sets. Apply H1;Auto with sets. Apply Acc_intro;Auto with sets. -Save. +Qed. Lemma wf_symprod: (well_founded A leA)->(well_founded B leB) @@ -125,7 +125,7 @@ Proof. Red. Induction a;Intros. Apply Acc_symprod;Auto with sets. -Save. +Qed. End Wf_Symmetric_Product. @@ -156,7 +156,7 @@ Proof. Apply sp_noswap. Apply left_sym;Auto with sets. -Save. +Qed. Lemma Acc_swapprod: (x,y:A)(Acc A R x)->(Acc A R y) @@ -184,7 +184,7 @@ Proof. Apply right_sym;Auto with sets. Auto with sets. -Save. +Qed. Lemma wf_swapprod: (well_founded A R)->(well_founded A*A SwapProd). @@ -192,6 +192,6 @@ Proof. Red. Induction a;Intros. Apply Acc_swapprod;Auto with sets. -Save. +Qed. End Swap. diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index 576c83cb4..9c013bd11 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -34,7 +34,7 @@ Proof. Elim H4 with x1 ;Auto with sets;Intros. Exists x2;Auto with sets. Apply t_trans with x1 ;Auto with sets. -Save. +Qed. Lemma Acc_union: (commut A R1 R2)->((x:A)(Acc A R2 x)->(Acc A R1 x)) @@ -61,7 +61,7 @@ Proof. Apply Acc_inv with x ;Auto with sets. Apply H0. Apply Acc_intro;Auto with sets. -Save. +Qed. Theorem wf_union: (commut A R1 R2)->(well_founded A R1)->(well_founded A R2) @@ -70,6 +70,6 @@ Proof. Unfold well_founded . Intros. Apply Acc_union;Auto with sets. -Save. +Qed. End WfUnion. -- cgit v1.2.3