diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-23 21:12:43 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-23 21:12:43 +0000 |
commit | 123817e082cea45d26b13461caa39807c38ed8a6 (patch) | |
tree | 23b98ea170c538c5ebd54cd00e0f280384dab859 | |
parent | 19dd83cf1b0e57fb13a8d970251822afd6a04ced (diff) |
Remplacement de Induction/Destruct par NewInduction/NewDestruct
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4464 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-x | theories/Relations/Operators_Properties.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Finite_sets_facts.v | 12 |
2 files changed, 12 insertions, 14 deletions
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index d7cb7a7eb..0ca819b84 100755 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -39,9 +39,9 @@ Lemma clos_rt_idempotent: (incl (clos_refl_trans A (clos_refl_trans A R)) (clos_refl_trans A R)). Red. -Induction 1; Auto with sets. +NewInduction 1; Auto with sets. Intros. -Apply rt_trans with y0; Auto with sets. +Apply rt_trans with y; Auto with sets. Qed. Lemma clos_refl_trans_ind_left: (A:Set)(R:A->A->Prop)(M:A)(P:A->Prop) @@ -72,9 +72,8 @@ Section Clos_Refl_Sym_Trans. Lemma clos_rt_clos_rst: (inclusion A (clos_refl_trans A R) (clos_refl_sym_trans A R)). Red. -Induction 1; Auto with sets. -Intros. -Apply rst_trans with y0; Auto with sets. +NewInduction 1; Auto with sets. +Apply rst_trans with y; Auto with sets. Qed. Lemma clos_rst_is_equiv: (equivalence A (clos_refl_sym_trans A R)). @@ -90,9 +89,8 @@ Qed. (incl (clos_refl_sym_trans A (clos_refl_sym_trans A R)) (clos_refl_sym_trans A R)). Red. -Induction 1; Auto with sets. -Intros. -Apply rst_trans with y0; Auto with sets. +NewInduction 1; Auto with sets. +Apply rst_trans with y; Auto with sets. Qed. End Clos_Refl_Sym_Trans. diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v index 0f11b389a..4e7b6931f 100755 --- a/theories/Sets/Finite_sets_facts.v +++ b/theories/Sets/Finite_sets_facts.v @@ -42,15 +42,15 @@ Variable U: Type. Lemma finite_cardinal : (X: (Ensemble U)) (Finite U X) -> (EX n:nat |(cardinal U X n)). Proof. -Induction 1. +NewInduction 1 as [|A _ [n H]]. Exists O; Auto with sets. -Induction 2; Intros n H3; Exists (S n); Auto with sets. +Exists (S n); Auto with sets. Qed. Lemma cardinal_finite: (X: (Ensemble U)) (n: nat) (cardinal U X n) -> (Finite U X). Proof. -Induction 1; Auto with sets. +NewInduction 1; Auto with sets. Qed. Theorem Add_preserves_Finite: @@ -89,7 +89,7 @@ Intros A H'; Elim H'; Auto with sets. Intros X H'0. Rewrite (less_than_empty U X H'0); Auto with sets. Intros; Elim Included_Add with U X A0 x; Auto with sets. -Induction 1; Intro A'; Induction 1; Intros H5 H6. +NewDestruct 1 as [A' [H5 H6]]. Rewrite H5; Auto with sets. Qed. @@ -110,8 +110,8 @@ Hints Resolve cardinalO_empty. Lemma inh_card_gt_O: (X: (Ensemble U)) (Inhabited U X) -> (n: nat) (cardinal U X n) -> (gt n O). Proof. -Induction 1. -Intros x H' n H'0. +NewInduction 1 as [x H']. +Intros n H'0. Elim (gt_O_eq n); Auto with sets. Intro H'1; Generalize H'; Generalize H'0. Rewrite <- H'1; Intro H'2. |