From 19dd83cf1b0e57fb13a8d970251822afd6a04ced Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 23 Sep 2003 21:00:49 +0000 Subject: Remplacement de Induction/Destruct par NewInduction/NewDestruct git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4463 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Sets/Constructive_sets.v | 2 +- theories/Sets/Finite_sets.v | 4 ++-- theories/Sets/Image.v | 38 +++++++++++++++++++------------------- theories/Sets/Multiset.v | 14 +++++++------- theories/Sets/Uniset.v | 16 ++++++++-------- 5 files changed, 37 insertions(+), 37 deletions(-) (limited to 'theories/Sets') diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v index 9d24ae433..78ad3d2f2 100755 --- a/theories/Sets/Constructive_sets.v +++ b/theories/Sets/Constructive_sets.v @@ -38,7 +38,7 @@ Qed. Lemma Noone_in_empty: (x: U) ~ (In U (Empty_set U) x). Proof. -Intro x; Red; Induction 1. +Red; NewDestruct 1. Qed. Hints Resolve Noone_in_empty. diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index 1e0c05450..1e7168791 100755 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -59,8 +59,8 @@ Lemma cardinal_invert : [n:nat] (EXT A | (EXT x | X == (Add U A x) /\ ~ (In U A x) /\ (cardinal U A n))) end. Proof. -Induction 1; Simpl; Auto. -Intros; Exists A; Exists x; Auto. +NewInduction 1; Simpl; Auto. +Exists A; Exists x; Auto. Qed. Lemma cardinal_elim : diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index db41d6ac6..d5f42e3f9 100755 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -62,11 +62,11 @@ Split; Red; Intros x0 H'. Elim H'; Intros. Rewrite H0. Elim Add_inv with U X x x1; Auto with sets. -Induction 1; Auto with sets. +NewDestruct 1; Auto with sets. Elim Add_inv with V (Im X f) (f x) x0; Auto with sets. -Induction 1; Intros. -Rewrite H1; Auto with sets. -Induction 1; Auto with sets. +NewDestruct 1 as [x0 H y H0]. +Rewrite H0; Auto with sets. +NewDestruct 1; Auto with sets. Qed. Lemma image_empty: (f: U -> V) (Im (Empty_set U) f) == (Empty_set V). @@ -110,10 +110,10 @@ Unfold injective; Intros f H. Cut (EXT x | ~ ((y: U) (f x) == (f y) -> x == y)). 2: Apply not_all_ex_not with P:=[x:U](y: U) (f x) == (f y) -> x == y; Trivial with sets. -Induction 1; Intros x C; Exists x. +NewDestruct 1 as [x C]; Exists x. Cut (EXT y | ~((f x)==(f y)->x==y)). 2: Apply not_all_ex_not with P:=[y:U](f x)==(f y)->x==y; Trivial with sets. -Induction 1; Intros y D; Exists y. +NewDestruct 1 as [y D]; Exists y. Apply imply_to_and; Trivial with sets. Qed. @@ -140,21 +140,21 @@ Lemma injective_preserves_cardinal: (A: (Ensemble U)) (f: U -> V) (n: nat) (injective f) -> (cardinal ? A n) -> (n': nat) (cardinal ? (Im A f) n') -> n' = n. Proof. -Induction 2; Auto with sets. +NewInduction 2 as [|A n H'0 H'1 x H'2]; Auto with sets. Rewrite (image_empty f). Intros n' CE. Apply cardinal_unicity with V (Empty_set V); Auto with sets. -Intros A0 n0 H'0 H'1 x H'2 n'. -Rewrite (Im_add A0 x f). +Intro n'. +Rewrite (Im_add A x f). Intro H'3. -Elim cardinal_Im_intro with A0 f n0; Trivial with sets. +Elim cardinal_Im_intro with A f n; Trivial with sets. Intros i CI. LApply (H'1 i); Trivial with sets. -Cut ~ (In ? (Im A0 f) (f x)). -Intros. -Apply cardinal_unicity with V (Add ? (Im A0 f) (f x)); Trivial with sets. +Cut ~ (In ? (Im A f) (f x)). +Intros H0 H1. +Apply cardinal_unicity with V (Add ? (Im A f) (f x)); Trivial with sets. Apply card_add; Auto with sets. -Rewrite <- H2; Trivial with sets. +Rewrite <- H1; Trivial with sets. Red; Intro; Apply H'2. Apply In_Image_elim with f; Trivial with sets. Qed. @@ -163,17 +163,17 @@ Lemma cardinal_decreases: (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal U A n) -> (n': nat) (cardinal V (Im A f) n') -> (le n' n). Proof. -Induction 1; Auto with sets. +NewInduction 1 as [|A n H'0 H'1 x H'2]; Auto with sets. Rewrite (image_empty f); Intros. Cut n' = O. Intro E; Rewrite E; Trivial with sets. Apply cardinal_unicity with V (Empty_set V); Auto with sets. -Intros A0 n0 H'0 H'1 x H'2 n'. -Rewrite (Im_add A0 x f). -Elim cardinal_Im_intro with A0 f n0; Trivial with sets. +Intro n'. +Rewrite (Im_add A x f). +Elim cardinal_Im_intro with A f n; Trivial with sets. Intros p C H'3. Apply le_trans with (S p). -Apply card_Add_gen with V (Im A0 f) (f x); Trivial with sets. +Apply card_Add_gen with V (Im A f) (f x); Trivial with sets. Apply le_n_S; Auto with sets. Qed. diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index 68d3ec7a5..37fb47e27 100755 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -42,21 +42,21 @@ Hints Unfold meq multiplicity. Lemma meq_refl : (x:multiset)(meq x x). Proof. -Induction x; Auto. +NewDestruct x; Auto. Qed. Hints Resolve meq_refl. Lemma meq_trans : (x,y,z:multiset)(meq x y)->(meq y z)->(meq x z). Proof. Unfold meq. -Induction x; Induction y; Induction z. +NewDestruct x; NewDestruct y; NewDestruct z. Intros; Rewrite H; Auto. Qed. Lemma meq_sym : (x,y:multiset)(meq x y)->(meq y x). Proof. Unfold meq. -Induction x; Induction y; Auto. +NewDestruct x; NewDestruct y; Auto. Qed. Hints Immediate meq_sym. @@ -83,7 +83,7 @@ Require Plus. (* comm. and ass. of plus *) Lemma munion_comm : (x,y:multiset)(meq (munion x y) (munion y x)). Proof. Unfold meq; Unfold multiplicity; Unfold munion. -Induction x; Induction y; Auto with arith. +NewDestruct x; NewDestruct y; Auto with arith. Qed. Hints Resolve munion_comm. @@ -91,14 +91,14 @@ Lemma munion_ass : (x,y,z:multiset)(meq (munion (munion x y) z) (munion x (munion y z))). Proof. Unfold meq; Unfold munion; Unfold multiplicity. -Induction x; Induction y; Induction z; Auto with arith. +NewDestruct x; NewDestruct y; NewDestruct z; Auto with arith. Qed. Hints Resolve munion_ass. Lemma meq_left : (x,y,z:multiset)(meq x y)->(meq (munion x z) (munion y z)). Proof. Unfold meq; Unfold munion; Unfold multiplicity. -Induction x; Induction y; Induction z. +NewDestruct x; NewDestruct y; NewDestruct z. Intros; Elim H; Auto with arith. Qed. Hints Resolve meq_left. @@ -106,7 +106,7 @@ Hints Resolve meq_left. Lemma meq_right : (x,y,z:multiset)(meq x y)->(meq (munion z x) (munion z y)). Proof. Unfold meq; Unfold munion; Unfold multiplicity. -Induction x; Induction y; Induction z. +NewDestruct x; NewDestruct y; NewDestruct z. Intros; Elim H; Auto. Qed. Hints Resolve meq_right. diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 17b10ae3a..5b28d6c2b 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -54,7 +54,7 @@ Hints Unfold seq. Lemma leb_refl : (b:bool)(leb b b). Proof. -Induction b; Simpl; Auto. +NewDestruct b; Simpl; Auto. Qed. Hints Resolve leb_refl. @@ -70,21 +70,21 @@ Qed. Lemma seq_refl : (x:uniset)(seq x x). Proof. -Induction x; Unfold seq; Auto. +NewDestruct x; Unfold seq; Auto. Qed. Hints Resolve seq_refl. Lemma seq_trans : (x,y,z:uniset)(seq x y)->(seq y z)->(seq x z). Proof. Unfold seq. -Induction x; Induction y; Induction z; Simpl; Intros. +NewDestruct x; NewDestruct y; NewDestruct z; Simpl; Intros. Rewrite H; Auto. Qed. Lemma seq_sym : (x,y:uniset)(seq x y)->(seq y x). Proof. Unfold seq. -Induction x; Induction y; Simpl; Auto. +NewDestruct x; NewDestruct y; Simpl; Auto. Qed. (** uniset union *) @@ -109,7 +109,7 @@ Hints Resolve union_empty_right. Lemma union_comm : (x,y:uniset)(seq (union x y) (union y x)). Proof. Unfold seq; Unfold charac; Unfold union. -Induction x; Induction y; Auto with bool. +NewDestruct x; NewDestruct y; Auto with bool. Qed. Hints Resolve union_comm. @@ -117,14 +117,14 @@ Lemma union_ass : (x,y,z:uniset)(seq (union (union x y) z) (union x (union y z))). Proof. Unfold seq; Unfold union; Unfold charac. -Induction x; Induction y; Induction z; Auto with bool. +NewDestruct x; NewDestruct y; NewDestruct z; Auto with bool. Qed. Hints Resolve union_ass. Lemma seq_left : (x,y,z:uniset)(seq x y)->(seq (union x z) (union y z)). Proof. Unfold seq; Unfold union; Unfold charac. -Induction x; Induction y; Induction z. +NewDestruct x; NewDestruct y; NewDestruct z. Intros; Elim H; Auto. Qed. Hints Resolve seq_left. @@ -132,7 +132,7 @@ Hints Resolve seq_left. Lemma seq_right : (x,y,z:uniset)(seq x y)->(seq (union z x) (union z y)). Proof. Unfold seq; Unfold union; Unfold charac. -Induction x; Induction y; Induction z. +NewDestruct x; NewDestruct y; NewDestruct z. Intros; Elim H; Auto. Qed. Hints Resolve seq_right. -- cgit v1.2.3