diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-08-05 19:04:16 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-08-05 19:04:16 +0000 |
commit | 83c56744d7e232abeb5f23e6d0f23cd0abc14a9c (patch) | |
tree | 6d7d4c2ce3bb159b8f81a4193abde1e3573c28d4 | |
parent | f7351ff222bad0cc906dbee3c06b20babf920100 (diff) |
Expérimentation de NewDestruct et parfois NewInduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1880 85f007b7-540e-0410-9357-904b9bb8a0f7
37 files changed, 233 insertions, 233 deletions
diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v index 52607a4a0..90d1f5940 100644 --- a/contrib/omega/Zcomplements.v +++ b/contrib/omega/Zcomplements.v @@ -18,7 +18,7 @@ Require Wf_nat. Implicit Arguments On. Lemma Zmult_zero : (x,y:Z)`x*y=0` -> `x=0` \/ `y=0`. -Destruct x; Destruct y; Auto. +NewDestruct x; NewDestruct y; Auto. Simpl; Intros; Discriminate H. Simpl; Intros; Discriminate H. Simpl; Intros; Discriminate H. @@ -153,23 +153,23 @@ Save. Section diveucl. Lemma two_or_two_plus_one : (x:Z) { y:Z | `x = 2*y`}+{ y:Z | `x = 2*y+1`}. -Destruct x. +NewDestruct x. Left ; Split with ZERO; Reflexivity. -Destruct p. -Right ; Split with (POS p0); Reflexivity. +NewDestruct p. +Right ; Split with (POS p); Reflexivity. -Left ; Split with (POS p0); Reflexivity. +Left ; Split with (POS p); Reflexivity. Right ; Split with ZERO; Reflexivity. -Destruct p. -Right ; Split with (NEG (add xH p0)). +NewDestruct p. +Right ; Split with (NEG (add xH p)). Rewrite NEG_xI. Rewrite NEG_add. Omega. -Left ; Split with (NEG p0); Reflexivity. +Left ; Split with (NEG p); Reflexivity. Right ; Split with `-1`; Reflexivity. Save. @@ -273,7 +273,7 @@ Save. Theorem Zdiv_eucl : (b:Z)`b > 0` -> (a:Z) { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < b` }. -Destruct a; +NewDestruct a; [ (* a=0 *) Exists `(0,0)`; Omega | (* a = (POS p) *) Intros; Apply Zdiv_eucl_POS; Auto diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v index c2585b3e0..1d9727573 100644 --- a/contrib/omega/Zpower.v +++ b/contrib/omega/Zpower.v @@ -78,7 +78,7 @@ Hints Unfold Zpower_nat : zarith. Lemma Zpower_exp : (x:Z)(n,m:Z) `n >= 0` -> `m >= 0` -> `(Zpower x (n+m))=(Zpower x n)*(Zpower x m)`. -Destruct n; Destruct m; Auto with zarith. +NewDestruct n; NewDestruct m; Auto with zarith. Simpl; Intros; Apply Zred_factor0. Simpl; Auto with zarith. Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith. @@ -313,7 +313,7 @@ Elim (convert p); Simpl; | Intro n; Rewrite (two_power_nat_S n); Unfold 2 Zdiv_rest_aux; Elim (iter_nat n (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`)); - Destruct a; Intros; Apply f_equal with f:=[z:Z]`2*z`; Assumption ]. + NewDestruct a; Intros; Apply f_equal with f:=[z:Z]`2*z`; Assumption ]. Save. Lemma Zdiv_rest_correct2 : @@ -330,33 +330,33 @@ Intros; Apply iter_pos_invariant with Intros q r d; Unfold Zdiv_rest_aux; Elim q; [ Omega - | Destruct p0; - [ Intro; Rewrite POS_xI; Intro; Elim H; Intros; Split; + | NewDestruct p0; + [ Rewrite POS_xI; Intro; Elim H; Intros; Split; [ Rewrite H0; Rewrite Zplus_assoc; Rewrite Zmult_plus_distr_l; Rewrite Zmult_1_n; Rewrite Zmult_assoc; - Rewrite (Zmult_sym (POS p1) `2`); Apply refl_equal + Rewrite (Zmult_sym (POS p0) `2`); Apply refl_equal | Omega ] - | Intro; Rewrite POS_xO; Intro; Elim H; Intros; Split; + | Rewrite POS_xO; Intro; Elim H; Intros; Split; [ Rewrite H0; - Rewrite Zmult_assoc; Rewrite (Zmult_sym (POS p1) `2`); + Rewrite Zmult_assoc; Rewrite (Zmult_sym (POS p0) `2`); Apply refl_equal | Omega ] | Omega ] - | Destruct p0; - [ Intro; Rewrite NEG_xI; Unfold Zminus; Intro; Elim H; Intros; Split; + | NewDestruct p0; + [ Rewrite NEG_xI; Unfold Zminus; Intro; Elim H; Intros; Split; [ Rewrite H0; Rewrite Zplus_assoc; Apply f_equal with f:=[z:Z]`z+r`; Do 2 (Rewrite Zmult_plus_distr_l); Rewrite Zmult_assoc; - Rewrite (Zmult_sym (NEG p1) `2`); + Rewrite (Zmult_sym (NEG p0) `2`); Rewrite <- Zplus_assoc; - Apply f_equal with f:=[z:Z]`2 * (NEG p1) * d + z`; + Apply f_equal with f:=[z:Z]`2 * (NEG p0) * d + z`; Omega | Omega ] - | Intro; Rewrite NEG_xO; Unfold Zminus; Intro; Elim H; Intros; Split; + | Rewrite NEG_xO; Unfold Zminus; Intro; Elim H; Intros; Split; [ Rewrite H0; - Rewrite Zmult_assoc; Rewrite (Zmult_sym (NEG p1) `2`); + Rewrite Zmult_assoc; Rewrite (Zmult_sym (NEG p0) `2`); Apply refl_equal | Omega ] | Omega ] ] diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v index 88e609e3f..93c6eaf53 100644 --- a/contrib/ring/Ring.v +++ b/contrib/ring/Ring.v @@ -69,15 +69,15 @@ Grammar vernac vernac : ast := Definition BoolTheory : (Ring_Theory xorb andb true false [b:bool]b eqb). Split; Simpl. -Destruct n; Destruct m; Reflexivity. -Destruct n; Destruct m; Destruct p; Reflexivity. -Destruct n; Destruct m; Reflexivity. -Destruct n; Destruct m; Destruct p; Reflexivity. -Destruct n; Reflexivity. -Destruct n; Reflexivity. -Destruct n; Reflexivity. -Destruct n; Destruct m; Destruct p; Reflexivity. -Destruct x; Destruct y; Reflexivity Orelse Simpl; Tauto. +NewDestruct n; NewDestruct m; Reflexivity. +NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity. +NewDestruct n; NewDestruct m; Reflexivity. +NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity. +NewDestruct n; Reflexivity. +NewDestruct n; Reflexivity. +NewDestruct n; Reflexivity. +NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity. +NewDestruct x; NewDestruct y; Reflexivity Orelse Simpl; Tauto. Defined. Add Ring bool xorb andb true false [b:bool]b eqb BoolTheory [ true false ]. diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v index 05a6f6850..80d27e630 100644 --- a/contrib/ring/Ring_abstract.v +++ b/contrib/ring/Ring_abstract.v @@ -208,7 +208,7 @@ Proof. Induction x. Intros; Simpl; EAuto. - Destruct y; Intros. + NewDestruct y; Intros. Simpl; Rewrite H; EAuto. diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v index f44f554e0..ae72f4eb4 100644 --- a/contrib/ring/Ring_normalize.v +++ b/contrib/ring/Ring_normalize.v @@ -427,7 +427,7 @@ Save. Remark interp_m_ok : (x:A)(l:varlist) (interp_m x l)==(Amult x (interp_vl l)). Proof. - Destruct l. + NewDestruct l. Simpl; Trivial. Reflexivity. Save. diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v index 8b4a0f95d..1b787f423 100644 --- a/contrib/ring/Ring_theory.v +++ b/contrib/ring/Ring_theory.v @@ -386,7 +386,7 @@ Definition Semi_Ring_Theory_of : (Azero : A)(Aopp : A -> A)(Aeq : A -> A -> bool) (Ring_Theory Aplus Amult Aone Azero Aopp Aeq) ->(Semi_Ring_Theory Aplus Amult Aone Azero Aeq). -Destruct 1. +Intros until 1; Case H. Split; Intros; Simpl; EAuto. Defined. diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v index 9b74e8952..04e2aa16a 100644 --- a/contrib/ring/Setoid_ring_normalize.v +++ b/contrib/ring/Setoid_ring_normalize.v @@ -453,7 +453,7 @@ Save. Remark interp_m_ok : (x:A)(l:varlist) (Aequiv (interp_m x l) (Amult x (interp_vl l))). Proof. - Destruct l;Trivial. + NewDestruct l;Trivial. Save. Lemma canonical_sum_merge_ok : (x,y:canonical_sum) diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v index 6428947ec..a0d587eb3 100644 --- a/contrib/ring/Setoid_ring_theory.v +++ b/contrib/ring/Setoid_ring_theory.v @@ -434,7 +434,7 @@ Implicit Arguments Off. Definition Semi_Setoid_Ring_Theory_of : Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory. -Destruct 1. +NewDestruct 1. Split; Intros; Simpl; EAuto. Defined. diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index ab22eca22..e6b444601 100755 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -22,29 +22,29 @@ Hint constr_between : arith v62 := Constructors between. Lemma bet_eq : (k,l:nat)(l=k)->(between k l). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Hints Resolve bet_eq : arith v62. Lemma between_le : (k,l:nat)(between k l)->(le k l). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Hints Immediate between_le : arith v62. Lemma between_Sk_l : (k,l:nat)(between k l)->(le (S k) l)->(between (S k) l). Proof. -Induction 1. +NewInduction 1. Intros; Absurd (le (S k) k); Auto with arith. -Induction 1; Auto with arith. +Induction H; Auto with arith. Qed. Hints Resolve between_Sk_l : arith v62. Lemma between_restr : (k,l,m:nat)(le k l)->(le l m)->(between k m)->(between l m). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Inductive exists [k:nat] : nat -> Prop @@ -55,7 +55,7 @@ Hint constr_exists : arith v62 := Constructors exists. Lemma exists_le_S : (k,l:nat)(exists k l)->(le (S k) l). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Lemma exists_lt : (k,l:nat)(exists k l)->(lt k l). @@ -78,55 +78,55 @@ Hints Resolve in_int_intro : arith v62. Lemma in_int_lt : (p,q,r:nat)(in_int p q r)->(lt p q). Proof. -Induction 1; Intros. +NewInduction 1; Intros. Apply le_lt_trans with r; Auto with arith. Qed. Lemma in_int_p_Sq : (p,q,r:nat)(in_int p (S q) r)->((in_int p q r) \/ <nat>r=q). Proof. -Induction 1; Intros. +NewInduction 1; Intros. Elim (le_lt_or_eq r q); Auto with arith. Qed. Lemma in_int_S : (p,q,r:nat)(in_int p q r)->(in_int p (S q) r). Proof. -Induction 1;Auto with arith. +NewInduction 1;Auto with arith. Qed. Hints Resolve in_int_S : arith v62. Lemma in_int_Sp_q : (p,q,r:nat)(in_int (S p) q r)->(in_int p q r). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Hints Immediate in_int_Sp_q : arith v62. Lemma between_in_int : (k,l:nat)(between k l)->(r:nat)(in_int k l r)->(P r). Proof. -Induction 1; Intros. +NewInduction 1; Intros. Absurd (lt k k); Auto with arith. Apply in_int_lt with r; Auto with arith. -Elim (in_int_p_Sq k l0 r); Intros; Auto with arith. -Rewrite H4; Trivial with arith. +Elim (in_int_p_Sq k l r); Intros; Auto with arith. +Rewrite H2; Trivial with arith. Qed. Lemma in_int_between : (k,l:nat)(le k l)->((r:nat)(in_int k l r)->(P r))->(between k l). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Lemma exists_in_int : (k,l:nat)(exists k l)->(EX m:nat | (in_int k l m) & (Q m)). Proof. -Induction 1. -Induction 2; Intros p inp Qp; Exists p; Auto with arith. -Intros; Exists l0; Auto with arith. +NewInduction 1. +Case IHexists; Intros p inp Qp; Exists p; Auto with arith. +Exists l; Auto with arith. Qed. Lemma in_int_exists : (k,l,r:nat)(in_int k l r)->(Q r)->(exists k l). Proof. -Induction 1; Intros. +NewInduction 1; Intros. Elim H1; Auto with arith. Qed. @@ -134,23 +134,23 @@ Lemma between_or_exists : (k,l:nat)(le k l)->((n:nat)(in_int k l n)->((P n)\/(Q n))) ->((between k l)\/(exists k l)). Proof. -Induction 1; Intros; Auto with arith. -Elim H1; Intro; Auto with arith. -Elim (H2 m); Auto with arith. +NewInduction 1; Intros; Auto with arith. +Elim IHle; Intro; Auto with arith. +Elim (H0 m); Auto with arith. Qed. Lemma between_not_exists : (k,l:nat)(between k l)-> ((n:nat)(in_int k l n) -> (P n) -> ~(Q n)) -> ~(exists k l). Proof. -Induction 1; Red; Intros. +NewInduction 1; Red; Intros. Absurd (lt k k); Auto with arith. -Absurd (Q l0); Auto with arith. -Elim (exists_in_int k (S l0)); Auto with arith; Intros l' inl' Ql'. -Replace l0 with l'; Auto with arith. +Absurd (Q l); Auto with arith. +Elim (exists_in_int k (S l)); Auto with arith; Intros l' inl' Ql'. +Replace l with l'; Auto with arith. Elim inl'; Intros. -Elim (le_lt_or_eq l' l0); Auto with arith; Intros. -Absurd (exists k l0); Auto with arith. +Elim (le_lt_or_eq l' l); Auto with arith; Intros. +Absurd (exists k l); Auto with arith. Apply in_int_exists with l'; Auto with arith. Qed. @@ -161,7 +161,7 @@ Inductive nth [init:nat] : nat->nat->Prop Lemma nth_le : (init,l,n:nat)(nth init l n)->(le init l). Proof. -Induction 1; Intros; Auto with arith. +NewInduction 1; Intros; Auto with arith. Apply le_trans with (S k); Auto with arith. Qed. @@ -169,7 +169,7 @@ Definition eventually := [n:nat](EX k:nat | (le k n) & (Q k)). Lemma event_O : (eventually O)->(Q O). Proof. -Induction 1; Intros. +NewInduction 1; Intros. Replace O with x; Auto with arith. Qed. diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index 172ccf568..cc4399d2f 100755 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -43,7 +43,7 @@ Proof. Intros m n H. LApply (lt_le_S m n); Auto with arith. Intro H'; LApply (le_lt_or_eq (S m) n); Auto with arith. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Right; Exists (minus n (S (S m))); Simpl. Rewrite (plus_sym m (minus n (S (S m)))). Rewrite (plus_n_Sm (minus n (S (S m))) m). diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 1397326b2..531e0a975 100755 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -14,14 +14,14 @@ Require Gt. Require Decidable. Theorem zerop : (n:nat){n=O}+{lt O n}. -Destruct n; Auto with arith. +NewDestruct n; Auto with arith. Save. Theorem lt_eq_lt_dec : (n,m:nat){(lt n m)}+{n=m}+{(lt m n)}. Proof. -Induction n; Induction m; Auto with arith. -Intros q H'; Elim (H q). -Induction 1; Auto with arith. +NewInduction n; NewInduction m; Auto with arith. +Elim (IHn m). +NewInduction 1; Auto with arith. Auto with arith. Qed. @@ -30,11 +30,11 @@ Proof lt_eq_lt_dec. Lemma le_lt_dec : (n,m:nat) {le n m} + {lt m n}. Proof. -Induction n. +NewInduction n. Auto with arith. -Induction m. +NewInduction m. Auto with arith. -Intros q H'; Elim (H q); Auto with arith. +Elim (IHn m); Auto with arith. Qed. Lemma le_le_S_dec : (n,m:nat) {le n m} + {le (S m) n}. diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 60fdc68ff..2a087a06d 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -32,8 +32,8 @@ Intros. Cut (n:nat)(P n)/\(P (S n)). Intros. Elim (H2 n). Auto with arith. -Induction n0. Auto with arith. -Intros. Elim H2; Auto with arith. +NewInduction n0. Auto with arith. +Intros. Elim IHn0; Auto with arith. Qed. (* 0 <n => n/2 < n *) diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index 8392f17ce..d0bd9afc6 100755 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -21,17 +21,17 @@ Fixpoint eq_nat [n:nat] : nat -> Prop := end. Theorem eq_nat_refl : (n:nat)(eq_nat n n). -Induction n; Simpl; Auto. +NewInduction n; Simpl; Auto. Qed. Hints Resolve eq_nat_refl : arith v62. Theorem eq_eq_nat : (n,m:nat)(n=m)->(eq_nat n m). -Induction 1; Trivial with arith. +NewInduction 1; Trivial with arith. Qed. Hints Immediate eq_eq_nat : arith v62. Theorem eq_nat_eq : (n,m:nat)(eq_nat n m)->(n=m). -Induction n; Induction m; Simpl; Contradiction Orelse Auto with arith. +NewInduction n; NewInduction m; Simpl; Contradiction Orelse Auto with arith. Qed. Hints Immediate eq_nat_eq : arith v62. @@ -40,15 +40,15 @@ Intros; Replace m with n; Auto with arith. Qed. Theorem eq_nat_decide : (n,m:nat){(eq_nat n m)}+{~(eq_nat n m)}. -Induction n. -Destruct m. +NewInduction n. +NewDestruct m. Auto with arith. -Intro; Right; Red; Trivial with arith. -Destruct m. +Intros; Right; Red; Trivial with arith. +NewDestruct m. Right; Red; Auto with arith. Intros. Simpl. -Apply H. +Apply IHn. Defined. Fixpoint beq_nat [n:nat] : nat -> bool := @@ -61,7 +61,7 @@ Fixpoint beq_nat [n:nat] : nat -> bool := Lemma beq_nat_refl : (x:nat)true=(beq_nat x x). Proof. - Induction x; Simpl; Auto. + NewInduction x; Simpl; Auto. Qed. Definition beq_nat_eq : (x,y:nat)true=(beq_nat x y)->x=y. diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index bf73ecb0a..0f1ab8559 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -24,22 +24,22 @@ Hint constr_odd : arith := Constructors odd. Lemma even_or_odd : (n:nat) (even n)\/(odd n). Proof. -Induction n. +NewInduction n. Auto with arith. -Intros n' H. Elim H; Auto with arith. +Elim IHn; Auto with arith. Save. Lemma even_odd_dec : (n:nat) { (even n) }+{ (odd n) }. Proof. -Induction n. +NewInduction n. Auto with arith. -Intros n' H. Elim H; Auto with arith. +Elim IHn; Auto with arith. Save. Lemma not_even_and_odd : (n:nat) (even n) -> (odd n) -> False. Proof. -Induction n. +NewInduction n. Intros. Inversion H0. -Intros. Inversion H0. Inversion H1. Auto with arith. +Intros. Inversion H. Inversion H0. Auto with arith. Save. diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index be420c672..db4494fdf 100755 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -14,12 +14,12 @@ Theorem le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)). Proof. - Induction 1; Auto. + NewInduction 1; Auto. Qed. Theorem le_trans : (n,m,p:nat)(le n m)->(le m p)->(le n p). Proof. - Induction 2; Auto. + NewInduction 2; Auto. Qed. Theorem le_n_Sn : (n:nat)(le n (S n)). @@ -29,14 +29,14 @@ Qed. Theorem le_O_n : (n:nat)(le O n). Proof. - Induction n ; Auto. + NewInduction n ; Auto. Qed. Hints Resolve le_n_S le_n_Sn le_O_n le_n_S le_trans : arith v62. Theorem le_pred_n : (n:nat)(le (pred n) n). Proof. -Induction n ; Auto with arith. +NewInduction n ; Auto with arith. Qed. Hints Resolve le_pred_n : arith v62. @@ -73,7 +73,7 @@ Hints Resolve le_Sn_O : arith v62. Theorem le_Sn_n : (n:nat)~(le (S n) n). Proof. -Induction n; Auto with arith. +NewInduction n; Auto with arith. Qed. Hints Resolve le_Sn_n : arith v62. @@ -110,7 +110,7 @@ Lemma le_elim_rel : (P:nat->nat->Prop) ((p,q:nat)(le p q)->(P p q)->(P (S p) (S q)))-> (n,m:nat)(le n m)->(P n m). Proof. -Induction n; Auto with arith. -Intros n' HRec m Le. +NewInduction n; Auto with arith. +Intros m Le. Elim Le; Auto with arith. Qed. diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index 785685093..7b5e089c3 100755 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -50,17 +50,17 @@ Hints Resolve lt_n_n : arith v62. Lemma S_pred : (n,m:nat)(lt m n)->(n=(S (pred n))). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Lemma lt_pred : (n,p:nat)(lt (S n) p)->(lt n (pred p)). Proof. -Induction 1; Simpl; Auto with arith. +NewInduction 1; Simpl; Auto with arith. Qed. Hints Immediate lt_pred : arith v62. Lemma lt_pred_n_n : (n:nat)(lt O n)->(lt (pred n) n). -Destruct 1; Simpl; Auto with arith. +NewDestruct 1; Simpl; Auto with arith. Save. Hints Resolve lt_pred_n_n : arith v62. @@ -92,14 +92,14 @@ Hints Immediate lt_le_weak : arith v62. Theorem neq_O_lt : (n:nat)(~O=n)->(lt O n). Proof. -Induction n; Auto with arith. +NewInduction n; Auto with arith. Intros; Absurd O=O; Trivial with arith. Qed. Hints Immediate neq_O_lt : arith v62. Theorem lt_O_neq : (n:nat)(lt O n)->(~O=n). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Hints Immediate lt_O_neq : arith v62. @@ -107,35 +107,35 @@ Hints Immediate lt_O_neq : arith v62. Theorem lt_trans : (n,m,p:nat)(lt n m)->(lt m p)->(lt n p). Proof. -Induction 2; Auto with arith. +NewInduction 2; Auto with arith. Qed. Theorem lt_le_trans : (n,m,p:nat)(lt n m)->(le m p)->(lt n p). Proof. -Induction 2; Auto with arith. +NewInduction 2; Auto with arith. Qed. Theorem le_lt_trans : (n,m,p:nat)(le n m)->(lt m p)->(lt n p). Proof. -Induction 2; Auto with arith. +NewInduction 2; Auto with arith. Qed. Hints Resolve lt_trans lt_le_trans le_lt_trans : arith v62. Theorem le_lt_or_eq : (n,m:nat)(le n m)->((lt n m) \/ n=m). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Theorem le_or_lt : (n,m:nat)((le n m)\/(lt m n)). Proof. Intros n m; Pattern n m; Apply nat_double_ind; Auto with arith. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Theorem le_not_lt : (n,m:nat)(le n m) -> ~(lt m n). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Theorem lt_not_le : (n,m:nat)(lt n m) -> ~(le m n). @@ -146,7 +146,7 @@ Hints Immediate le_not_lt lt_not_le : arith v62. Theorem lt_not_sym : (n,m:nat)(lt n m) -> ~(lt m n). Proof. -Induction 1; Auto with arith. +NewInduction 1; Auto with arith. Qed. Theorem nat_total_order: (m,n: nat) ~ m = n -> (lt m n) \/ (lt n m). diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index bc976fbd2..a38329c34 100755 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -28,15 +28,15 @@ Qed. Lemma le_min_l : (n,m:nat)(le (min n m) n). Proof. -Induction n; Intros; Simpl; Auto with arith. +NewInduction n; Intros; Simpl; Auto with arith. Elim m; Intros; Simpl; Auto with arith. Qed. Hints Resolve le_min_l : arith v62. Lemma le_min_r : (n,m:nat)(le (min n m) m). Proof. -Induction n; Simpl; Auto with arith. -Induction m; Simpl; Auto with arith. +NewInduction n; Simpl; Auto with arith. +NewInduction m; Simpl; Auto with arith. Qed. Hints Resolve le_min_r : arith v62. @@ -44,7 +44,7 @@ Hints Resolve le_min_r : arith v62. Lemma min_case : (n,m:nat)(P:nat->Set)(P n)->(P m)->(P (min n m)). Proof. -Induction n; Simpl; Auto with arith. -Induction m; Intros; Simpl; Auto with arith. -Pattern (min n0 n1); Apply H ; Auto with arith. +NewInduction n; Simpl; Auto with arith. +NewInduction m; Intros; Simpl; Auto with arith. +Pattern (min n m); Apply IHn ; Auto with arith. Qed. diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index 3da5916e0..f3f67dea3 100755 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -27,19 +27,19 @@ Fixpoint minus [n:nat] : nat -> nat := Lemma minus_plus_simpl : (n,m,p:nat)((minus n m)=(minus (plus p n) (plus p m))). Proof. - Induction p; Simpl; Auto with arith. + NewInduction p; Simpl; Auto with arith. Qed. Hints Resolve minus_plus_simpl : arith v62. Lemma minus_n_O : (n:nat)(n=(minus n O)). Proof. -Induction n; Simpl; Auto with arith. +NewInduction n; Simpl; Auto with arith. Qed. Hints Resolve minus_n_O : arith v62. Lemma minus_n_n : (n:nat)(O=(minus n n)). Proof. -Induction n; Simpl; Auto with arith. +NewInduction n; Simpl; Auto with arith. Qed. Hints Resolve minus_n_n : arith v62. @@ -84,7 +84,7 @@ Intros; Absurd (lt O O); Auto with arith. Intros p q lepq Hp gtp. Elim (le_lt_or_eq O p); Auto with arith. Auto with arith. -Induction 1; Elim minus_n_O; Auto with arith. +NewInduction 1; Elim minus_n_O; Auto with arith. Qed. Hints Resolve lt_minus : arith v62. @@ -96,7 +96,7 @@ Qed. Hints Immediate lt_O_minus_lt : arith v62. Theorem pred_of_minus : (x:nat)(pred x)=(minus x (S O)). -Induction x; Auto with arith. +NewInduction x; Auto with arith. Save. diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 8955b1ea3..86404aca3 100755 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -26,8 +26,8 @@ Hints Resolve mult_plus_distr : arith v62. Lemma mult_plus_distr_r : (n,m,p:nat) (mult n (plus m p))=(plus (mult n m) (mult n p)). Proof. - Induction n. Trivial. - Intros. Simpl. Rewrite (H m p). Apply sym_eq. Apply plus_permute_2_in_4. + NewInduction n. Trivial. + Intros. Simpl. Rewrite (IHn m p). Apply sym_eq. Apply plus_permute_2_in_4. Qed. Lemma mult_minus_distr : (n,m,p:nat)((mult (minus n m) p)=(minus (mult n p) (mult m p))). @@ -39,7 +39,7 @@ Hints Resolve mult_minus_distr : arith v62. Lemma mult_O_le : (n,m:nat)(m=O)\/(le n (mult m n)). Proof. -Induction m; Simpl; Auto with arith. +NewInduction m; Simpl; Auto with arith. Qed. Hints Resolve mult_O_le : arith v62. @@ -76,16 +76,16 @@ Hints Resolve mult_n_1 : arith v62. Lemma mult_le : (m,n,p:nat) (le n p) -> (le (mult m n) (mult m p)). Proof. - Induction m. Intros. Simpl. Apply le_n. + NewInduction m. Intros. Simpl. Apply le_n. Intros. Simpl. Apply le_plus_plus. Assumption. - Apply H. Assumption. + Apply IHm. Assumption. Qed. Hints Resolve mult_le : arith. Lemma mult_lt : (m,n,p:nat) (lt n p) -> (lt (mult (S m) n) (mult (S m) p)). Proof. - Induction m. Intros. Simpl. Rewrite <- plus_n_O. Rewrite <- plus_n_O. Assumption. - Intros. Exact (lt_plus_plus ? ? ? ? H0 (H ? ? H0)). + NewInduction m. Intros. Simpl. Rewrite <- plus_n_O. Rewrite <- plus_n_O. Assumption. + Intros. Exact (lt_plus_plus ? ? ? ? H (IHm ? ? H)). Qed. Hints Resolve mult_lt : arith. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index b02d5a324..d847a060d 100755 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -12,20 +12,20 @@ Require Decidable. Theorem O_or_S : (n:nat)({m:nat|(S m)=n})+{O=n}. Proof. -Induction n. +NewInduction n. Auto. -Intros p H; Left; Exists p; Auto. +Left; Exists n; Auto. Qed. Theorem eq_nat_dec : (n,m:nat){n=m}+{~(n=m)}. Proof. -Induction n; Induction m; Auto. -Intros q H'; Elim (H q); Auto. +NewInduction n; NewInduction m; Auto. +Elim (IHn m); Auto. Qed. Hints Resolve O_or_S eq_nat_dec : arith. Theorem dec_eq_nat:(x,y:nat)(decidable (x=y)). Intros x y; Unfold decidable; Elim (eq_nat_dec x y); Auto with arith. -Save. +Qed. diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 1b70e1512..69bbd975a 100755 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -32,7 +32,7 @@ Qed. Lemma simpl_plus_l : (n,m,p:nat)((plus n m)=(plus n p))->(m=p). Proof. -Induction n ; Simpl ; Auto with arith. +NewInduction n ; Simpl ; Auto with arith. Qed. Lemma plus_assoc_l : (n,m,p:nat)((plus n (plus m p))=(plus (plus n m) p)). @@ -54,18 +54,18 @@ Hints Resolve plus_assoc_r : arith v62. Lemma simpl_le_plus_l : (p,n,m:nat)(le (plus p n) (plus p m))->(le n m). Proof. -Induction p; Simpl; Auto with arith. +NewInduction p; Simpl; Auto with arith. Qed. Lemma le_reg_l : (n,m,p:nat)(le n m)->(le (plus p n) (plus p m)). Proof. -Induction p; Simpl; Auto with arith. +NewInduction p; Simpl; Auto with arith. Qed. Hints Resolve le_reg_l : arith v62. Lemma le_reg_r : (a,b,c:nat) (le a b)->(le (plus a c) (plus b c)). Proof. -Induction 1 ; Simpl; Auto with arith. +NewInduction 1 ; Simpl; Auto with arith. Qed. Hints Resolve le_reg_r : arith v62. @@ -78,7 +78,7 @@ Qed. Lemma le_plus_l : (n,m:nat)(le n (plus n m)). Proof. -Induction n; Simpl; Auto with arith. +NewInduction n; Simpl; Auto with arith. Qed. Hints Resolve le_plus_l : arith v62. @@ -96,12 +96,12 @@ Hints Resolve le_plus_trans : arith v62. Lemma simpl_lt_plus_l : (n,m,p:nat)(lt (plus p n) (plus p m))->(lt n m). Proof. -Induction p; Simpl; Auto with arith. +NewInduction p; Simpl; Auto with arith. Qed. Lemma lt_reg_l : (n,m,p:nat)(lt n m)->(lt (plus p n) (plus p m)). Proof. -Induction p; Simpl; Auto with arith. +NewInduction p; Simpl; Auto with arith. Qed. Hints Resolve lt_reg_l : arith v62. @@ -138,15 +138,15 @@ Qed. Lemma plus_is_O : (m,n:nat) (plus m n)=O -> m=O /\ n=O. Proof. - Destruct m; Auto. + NewDestruct m; Auto. Intros. Discriminate H. Qed. Lemma plus_is_one : (m,n:nat) (plus m n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}. Proof. - Destruct m; Auto. - Destruct n; Auto. + NewDestruct m; Auto. + NewDestruct n; Auto. Intros. Simpl in H. Discriminate H. Qed. diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index ff502af94..f34c97d23 100755 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -25,12 +25,12 @@ Proof. Red. Cut (n:nat)(a:A)(lt (f a) n)->(Acc A ltof a). Intros H a; Apply (H (S (f a))); Auto with arith. -Induction n. +NewInduction n. Intros; Absurd (lt (f a) O); Auto with arith. -Intros m Hm a ltSma. +Intros a ltSma. Apply Acc_intro. Unfold ltof; Intros b ltfafb. -Apply Hm. +Apply IHn. Apply lt_le_trans with (f a); Auto with arith. Qed. @@ -60,12 +60,12 @@ Theorem induction_ltof1 Proof. Intros P F; Cut (n:nat)(a:A)(lt (f a) n)->(P a). Intros H a; Apply (H (S (f a))); Auto with arith. -Induction n. +NewInduction n. Intros; Absurd (lt (f a) O); Auto with arith. -Intros m Hm a ltSma. +Intros a ltSma. Apply F. Unfold ltof; Intros b ltfafb. -Apply Hm. +Apply IHn. Apply lt_le_trans with (f a); Auto with arith. Qed. @@ -94,12 +94,12 @@ Proof. Red. Cut (n:nat)(a:A)(lt (f a) n)->(Acc A R a). Intros H a; Apply (H (S (f a))); Auto with arith. -Induction n. +NewInduction n. Intros; Absurd (lt (f a) O); Auto with arith. -Intros m Hm a ltSma. +Intros a ltSma. Apply Acc_intro. Intros b ltfafb. -Apply Hm. +Apply IHn. Apply lt_le_trans with (f a); Auto with arith. Save. diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 4f7df44fd..3c82fd8e9 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -57,7 +57,7 @@ Save. Hints Resolve eq_true_false_abs : bool. Lemma not_true_is_false : (b:bool)~b=true->b=false. -Destruct b. +NewDestruct b. Intros. Red in H; Elim H. Reflexivity. @@ -66,7 +66,7 @@ Reflexivity. Save. Lemma not_false_is_true : (b:bool)~b=false->b=true. -Destruct b. +NewDestruct b. Intros. Reflexivity. Intro H; Red in H; Elim H. @@ -98,19 +98,19 @@ Definition eqb : bool->bool->bool := end. Lemma eqb_refl : (x:bool)(Is_true (eqb x x)). -Destruct x; Simpl; Auto with bool. +NewDestruct x; Simpl; Auto with bool. Save. Lemma eqb_eq : (x,y:bool)(Is_true (eqb x y))->x=y. -Destruct x; Destruct y; Simpl; Tauto. +NewDestruct x; NewDestruct y; Simpl; Tauto. Save. Lemma Is_true_eq_true : (x:bool) (Is_true x) -> x=true. -Destruct x; Simpl; Tauto. +NewDestruct x; Simpl; Tauto. Save. Lemma Is_true_eq_true2 : (x:bool) x=true -> (Is_true x). -Destruct x; Simpl; Auto with bool. +NewDestruct x; Simpl; Auto with bool. Save. Lemma eqb_subst : @@ -137,7 +137,7 @@ Trivial with bool. Save. Lemma eqb_prop : (a,b:bool)(eqb a b)=true -> a=b. -Destruct a; Destruct b; Simpl; Intro; +NewDestruct a; NewDestruct b; Simpl; Intro; Discriminate H Orelse Reflexivity. Save. @@ -190,13 +190,13 @@ Save. Lemma negb_orb : (b1,b2:bool) (negb (orb b1 b2)) = (andb (negb b1) (negb b2)). Proof. - Destruct b1; Destruct b2; Simpl; Reflexivity. + NewDestruct b1; NewDestruct b2; Simpl; Reflexivity. Qed. Lemma negb_andb : (b1,b2:bool) (negb (andb b1 b2)) = (orb (negb b1) (negb b2)). Proof. - Destruct b1; Destruct b2; Simpl; Reflexivity. + NewDestruct b1; NewDestruct b2; Simpl; Reflexivity. Qed. Lemma negb_sym : (b,b':bool)(b'=(negb b))->(b=(negb b')). @@ -210,13 +210,13 @@ Induction b; Simpl; Unfold not; Intro; Apply diff_true_false; Auto with bool. Save. Lemma eqb_negb1 : (b:bool)(eqb (negb b) b)=false. -Destruct b. +NewDestruct b. Trivial with bool. Trivial with bool. Save. Lemma eqb_negb2 : (b:bool)(eqb b (negb b))=false. -Destruct b. +NewDestruct b. Trivial with bool. Trivial with bool. Save. @@ -244,10 +244,10 @@ Save. Lemma orb_true_intro : (b1,b2:bool)(b1=true)\/(b2=true)->(orb b1 b2)=true. -Destruct b1; Auto with bool. -Destruct 1; Intros. +NewDestruct b1; Auto with bool. +NewDestruct 1; Intros. Elim diff_true_false; Auto with bool. -Rewrite H0; Trivial with bool. +Rewrite H; Trivial with bool. Save. Hints Resolve orb_true_intro : bool v62. @@ -261,7 +261,7 @@ Trivial with bool. Save. Lemma orb_true_elim : (b1,b2:bool)(orb b1 b2)=true -> {b1=true}+{b2=true}. -Destruct b1; [Auto with bool | Destruct b2; Auto with bool]. +NewDestruct b1; [Auto with bool | NewDestruct b2; Auto with bool]. Save. Lemma orb_false_intro : (b1,b2:bool)(b1=false)->(b2=false)->(orb b1 b2)=false. @@ -271,22 +271,22 @@ Hints Resolve orb_false_intro : bool v62. Lemma orb_b_false : (b:bool)(orb b false)=b. Proof. - Destruct b; Trivial with bool. + NewDestruct b; Trivial with bool. Save. Hints Resolve orb_b_false : bool v62. Lemma orb_false_b : (b:bool)(orb false b)=b. Proof. - Destruct b; Trivial with bool. + NewDestruct b; Trivial with bool. Save. Hints Resolve orb_false_b : bool v62. Lemma orb_false_elim : (b1,b2:bool)(orb b1 b2)=false -> (b1=false)/\(b2=false). Proof. - Destruct b1. + NewDestruct b1. Intros; Elim diff_true_false; Auto with bool. - Destruct b2. + NewDestruct b2. Intros; Elim diff_true_false; Auto with bool. Auto with bool. Save. @@ -294,17 +294,17 @@ Save. Lemma orb_neg_b : (b:bool)(orb b (negb b))=true. Proof. - Destruct b; Reflexivity. + NewDestruct b; Reflexivity. Save. Hints Resolve orb_neg_b : bool v62. Lemma orb_sym : (b1,b2:bool)(orb b1 b2)=(orb b2 b1). -Destruct b1; Destruct b2; Reflexivity. +NewDestruct b1; NewDestruct b2; Reflexivity. Save. Lemma orb_assoc : (b1,b2,b3:bool)(orb b1 (orb b2 b3))=(orb (orb b1 b2) b3). Proof. - Destruct b1; Destruct b2; Destruct b3; Reflexivity. + NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. Save. Hints Resolve orb_sym orb_assoc orb_b_false orb_false_b : bool v62. @@ -332,29 +332,29 @@ Hints Resolve andb_prop2 : bool v62. Lemma andb_true_intro : (b1,b2:bool)(b1=true)/\(b2=true)->(andb b1 b2)=true. Proof. - Destruct b1; Destruct b2; Simpl; Tauto Orelse Auto with bool. + NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool. Save. Hints Resolve andb_true_intro : bool v62. Lemma andb_true_intro2 : (b1,b2:bool)(Is_true b1)->(Is_true b2)->(Is_true (andb b1 b2)). Proof. - Destruct b1; Destruct b2; Simpl; Tauto. + NewDestruct b1; NewDestruct b2; Simpl; Tauto. Save. Hints Resolve andb_true_intro2 : bool v62. Lemma andb_false_intro1 : (b1,b2:bool)(b1=false)->(andb b1 b2)=false. -Destruct b1; Destruct b2; Simpl; Tauto Orelse Auto with bool. +NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool. Save. Lemma andb_false_intro2 : (b1,b2:bool)(b2=false)->(andb b1 b2)=false. -Destruct b1; Destruct b2; Simpl; Tauto Orelse Auto with bool. +NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool. Save. Lemma andb_b_false : (b:bool)(andb b false)=false. -Destruct b; Auto with bool. +NewDestruct b; Auto with bool. Save. Lemma andb_false_b : (b:bool)(andb false b)=false. @@ -362,7 +362,7 @@ Trivial with bool. Save. Lemma andb_b_true : (b:bool)(andb b true)=b. -Destruct b; Auto with bool. +NewDestruct b; Auto with bool. Save. Lemma andb_true_b : (b:bool)(andb true b)=b. @@ -371,22 +371,22 @@ Save. Lemma andb_false_elim : (b1,b2:bool)(andb b1 b2)=false -> {b1=false}+{b2=false}. -Destruct b1; Destruct b2; Simpl; Auto with bool. +NewDestruct b1; NewDestruct b2; Simpl; Auto with bool. Save. Hints Resolve andb_false_elim : bool v62. Lemma andb_neg_b : (b:bool)(andb b (negb b))=false. -Destruct b; Reflexivity. +NewDestruct b; Reflexivity. Save. Hints Resolve andb_neg_b : bool v62. Lemma andb_sym : (b1,b2:bool)(andb b1 b2)=(andb b2 b1). -Destruct b1; Destruct b2; Reflexivity. +NewDestruct b1; NewDestruct b2; Reflexivity. Save. Lemma andb_assoc : (b1,b2,b3:bool)(andb b1 (andb b2 b3))=(andb (andb b1 b2) b3). -Destruct b1; Destruct b2; Destruct b3; Reflexivity. +NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. Save. Hints Resolve andb_sym andb_assoc : bool v62. @@ -463,32 +463,32 @@ Qed. Lemma demorgan1 : (b1,b2,b3:bool) (andb b1 (orb b2 b3)) = (orb (andb b1 b2) (andb b1 b3)). -Destruct b1; Destruct b2; Destruct b3; Reflexivity. +NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. Save. Lemma demorgan2 : (b1,b2,b3:bool) (andb (orb b1 b2) b3) = (orb (andb b1 b3) (andb b2 b3)). -Destruct b1; Destruct b2; Destruct b3; Reflexivity. +NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. Save. Lemma demorgan3 : (b1,b2,b3:bool) (orb b1 (andb b2 b3)) = (andb (orb b1 b2) (orb b1 b3)). -Destruct b1; Destruct b2; Destruct b3; Reflexivity. +NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. Save. Lemma demorgan4 : (b1,b2,b3:bool) (orb (andb b1 b2) b3) = (andb (orb b1 b3) (orb b2 b3)). -Destruct b1; Destruct b2; Destruct b3; Reflexivity. +NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. Save. Lemma absoption_andb : (b1,b2:bool) (andb b1 (orb b1 b2)) = b1. Proof. - Destruct b1; Destruct b2; Simpl; Reflexivity. + NewDestruct b1; NewDestruct b2; Simpl; Reflexivity. Qed. Lemma absoption_orb : (b1,b2:bool) (orb b1 (andb b1 b2)) = b1. Proof. - Destruct b1; Destruct b2; Simpl; Reflexivity. + NewDestruct b1; NewDestruct b2; Simpl; Reflexivity. Qed. diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index f9c5e3976..d0c089c7a 100755 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -17,12 +17,12 @@ Inductive IfProp [A,B:Prop] : bool-> Prop Hints Resolve Iftrue Iffalse : bool v62. Lemma Iftrue_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=true -> A. -Destruct 1; Intros; Auto with bool. +NewDestruct 1; Intros; Auto with bool. Case diff_true_false; Auto with bool. Save. Lemma Iffalse_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=false -> B. -Destruct 1; Intros; Auto with bool. +NewDestruct 1; Intros; Auto with bool. Case diff_true_false; Trivial with bool. Save. @@ -39,11 +39,11 @@ Assumption. Save. Lemma IfProp_or : (A,B:Prop)(b:bool)(IfProp A B b) -> A\/B. -Destruct 1; Auto with bool. +NewDestruct 1; Auto with bool. Save. Lemma IfProp_sum : (A,B:Prop)(b:bool)(IfProp A B b) -> {A}+{B}. -Destruct b; Intro H. +NewDestruct b; Intro H. Left; Inversion H; Auto with bool. Right; Inversion H; Auto with bool. Save. diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index 8a8d09621..4422a03f4 100755 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -15,19 +15,19 @@ Definition zerob : nat->bool := [n:nat]Cases n of O => true | (S _) => false end. Lemma zerob_true_intro : (n:nat)(n=O)->(zerob n)=true. -Destruct n; [Trivial with bool | Intros p H; Inversion H]. +NewDestruct n; [Trivial with bool | Inversion 1]. Save. Hints Resolve zerob_true_intro : bool. Lemma zerob_true_elim : (n:nat)(zerob n)=true->(n=O). -Destruct n; [Trivial with bool | Intros p H; Inversion H]. +NewDestruct n; [Trivial with bool | Inversion 1]. Save. Lemma zerob_false_intro : (n:nat)~(n=O)->(zerob n)=false. -Destruct n; [Destruct 1; Auto with bool | Trivial with bool]. +NewDestruct n; [NewDestruct 1; Auto with bool | Trivial with bool]. Save. Hints Resolve zerob_false_intro : bool. Lemma zerob_false_elim : (n:nat)(zerob n)=false -> ~(n=O). -Destruct n; [Intro H; Inversion H | Auto with bool]. +NewDestruct n; [Intro H; Inversion H | Auto with bool]. Save. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 2c5c0f569..8c3ade1cd 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -150,7 +150,7 @@ Section Logic_lemmas. Proof. Intros. Cut (identity A x y). - Destruct 1; Auto. + NewDestruct 1; Auto. Elim H; Auto. Qed. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index eb7edad11..4882ea29c 100755 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -189,7 +189,7 @@ Lemma False_rect: (C:Type)False->C. Proof. Intros. Cut Empty_set. - Destruct 1. + NewDestruct 1. Elim H. Qed. diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 214c33117..bd55dcd1d 100755 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -29,7 +29,7 @@ Chapter Well_founded. := 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. + NewDestruct 1; Trivial. Defined. (* the informative elimination : diff --git a/theories/IntMap/Addr.v b/theories/IntMap/Addr.v index 088b03845..a74dcf5b8 100644 --- a/theories/IntMap/Addr.v +++ b/theories/IntMap/Addr.v @@ -18,7 +18,7 @@ Inductive ad : Set := Lemma ad_sum : (a:ad) {p:positive | a=(ad_x p)}+{a=ad_z}. Proof. - Destruct a; Auto. + NewDestruct a; Auto. Left; Exists p; Trivial. Qed. @@ -74,15 +74,15 @@ Qed. Lemma ad_xor_comm : (a,a':ad) (ad_xor a a')=(ad_xor a' a). Proof. - Destruct a; Destruct a'; Simpl; Auto. - Induction p; Simpl; Auto. - Destruct p0; Simpl; Trivial; Intros. + NewDestruct a; NewDestruct a'; Simpl; Auto. + Generalize p0; Clear p0; Induction p; Simpl; Auto. + NewDestruct p0; Simpl; Trivial; Intros. Rewrite Hrecp; Trivial. Rewrite Hrecp; Trivial. - Destruct p0; Simpl; Trivial; Intros. + NewDestruct p0; Simpl; Trivial; Intros. Rewrite Hrecp; Trivial. Rewrite Hrecp; Trivial. - Induction p; Simpl; Auto. + Induction p0; Simpl; Auto. Qed. Lemma ad_xor_nilpotent : (a:ad) (ad_xor a a)=ad_z. diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v index c1d07eaa6..7eeeb73f0 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -84,9 +84,9 @@ Qed. Lemma app_eq_nil: (x,y:list) (x^y)=nil -> x=nil /\ y=nil. Proof. - Destruct x;Destruct y;Simpl;Auto. + NewDestruct x;NewDestruct y;Simpl;Auto. Intros H;Discriminate H. - Intros a0 l0 H;Discriminate H. + Intros;Discriminate H. Qed. Lemma app_cons_not_nil: (x,y:list)(a:A)~nil=(x^(cons a y)). @@ -101,7 +101,7 @@ Lemma app_eq_unit:(x,y:list)(a:A) (x^y)=(cons a nil)-> (x=nil)/\ y=(cons a nil) \/ x=(cons a nil)/\ y=nil. Proof. - Destruct x;Destruct y;Simpl. + NewDestruct x;NewDestruct y;Simpl. Intros a H;Discriminate H. Left;Split;Auto. Right;Split;Auto. @@ -442,7 +442,7 @@ i*) Lemma list_eq_dec : ((x,y:A){x=y}+{~x=y})->(x,y:list){x=y}+{~x=y}. Proof. - Induction x; Destruct y; Intros; Auto. + Induction x; NewDestruct y; Intros; Auto. Case (H a a0); Intro e. Case (H0 l0); Intro e'. Left; Rewrite e; Rewrite e'; Trivial. diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 0bee9226e..41ef49eaa 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -17,14 +17,14 @@ Inductive JMeq [A:Set;x:A] : (B:Set)B->Prop := Hints Resolve JMeq_refl. Lemma JMeq_sym : (A,B:Set)(x:A)(y:B)(JMeq x y)->(JMeq y x). -Destruct 1; Trivial. +NewDestruct 1; Trivial. Save. Hints Immediate JMeq_sym. Lemma JMeq_trans : (A,B,C:Set)(x:A)(y:B)(z:C) (JMeq x y)->(JMeq y z)->(JMeq x z). -Destruct 1; Trivial. +NewDestruct 1; Trivial. Save. Axiom JMeq_eq : (A:Set)(x,y:A)(JMeq x y)->(x=y). diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index a9c26fa72..3a1d677db 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -105,12 +105,12 @@ Hints Resolve Rlt_le : real. (**********) Lemma Rle_ge : (r1,r2:R)``r1<=r2`` -> ``r2>=r1``. -Destruct 1; Red; Auto with real. +NewDestruct 1; Red; Auto with real. Save. (**********) Lemma Rge_le : (r1,r2:R)``r1>=r2`` -> ``r2<=r1``. -Destruct 1; Red; Auto with real. +NewDestruct 1; Red; Auto with real. Save. (**********) @@ -1355,7 +1355,7 @@ Save. (**********) Lemma plus_IZR:(z,t:Z)(IZR `z+t`)==``(IZR z)+(IZR t)``. -Destruct z; Destruct t; Intros; Auto with real. +NewDestruct z; NewDestruct t; Intros; Auto with real. Simpl; Intros; Rewrite convert_add; Auto with real. Apply plus_IZR_NEG_POS. Rewrite Zplus_sym; Rewrite Rplus_sym; Apply plus_IZR_NEG_POS. @@ -1406,7 +1406,7 @@ Save. (**********) Lemma eq_IZR_R0:(z:Z)``(IZR z)==0``->`z=0`. -Destruct z; Simpl; Intros; Auto with zarith. +NewDestruct z; Simpl; Intros; Auto with zarith. Case (Rlt_not_eq ``0`` (INR (convert p))); Auto with real. Case (Rlt_not_eq ``-(INR (convert p))`` ``0`` ); Auto with real. Save. diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 104b8b437..01b442a85 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -146,7 +146,7 @@ Proof. Intros. Inversion_clear H. Apply Acc_intro. - Destruct y0;Intros. + NewDestruct y0;Intros. Inversion_clear H;Inversion_clear H1;Apply H0. Apply sp_swap. Apply right_sym;Auto with sets. diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 27c760194..65571855e 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -35,11 +35,11 @@ Require Zsyntax. Lemma inject_nat_complete : (x:Z)`0 <= x` -> (EX n:nat | x=(inject_nat n)). -Destruct x; Intros; +NewDestruct x; Intros; [ Exists O; Auto with arith | Specialize (ZL4 p); Intros Hp; Elim Hp; Intros; - Exists (S x0); Intros; Simpl; - Specialize (bij1 x0); Intro Hx0; + Exists (S x); Intros; Simpl; + Specialize (bij1 x); Intro Hx0; Rewrite <- H0 in Hx0; Apply f_equal with f:=POS; Apply convert_intro; Auto with arith @@ -61,7 +61,7 @@ Save. Lemma inject_nat_complete_inf : (x:Z)`0 <= x` -> { n:nat | (x=(inject_nat n)) }. -Destruct x; Intros; +NewDestruct x; Intros; [ Exists O; Auto with arith | Specialize (ZL4_inf p); Intros Hp; Elim Hp; Intros x0 H0; Exists (S x0); Intros; Simpl; diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index dc9e69e17..cf46b8bdf 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -261,12 +261,12 @@ Save. Lemma Zeven_not_Zodd : (z:Z)(Zeven z) -> ~(Zodd z). Proof. - Destruct z; [ Idtac | Destruct p | Destruct p ]; Compute; Trivial. + NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p ]; Compute; Trivial. Save. Lemma Zodd_not_Zeven : (z:Z)(Zodd z) -> ~(Zeven z). Proof. - Destruct z; [ Idtac | Destruct p | Destruct p ]; Compute; Trivial. + NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p ]; Compute; Trivial. Save. Hints Unfold Zeven Zodd : zarith. @@ -291,22 +291,22 @@ Definition Zdiv2 := Lemma Zeven_div2 : (x:Z) (Zeven x) -> `x = 2*(Zdiv2 x)`. Proof. -Destruct x. +NewDestruct x. Auto with arith. -Destruct p; Auto with arith. -Intros. Absurd (Zeven (POS (xI p0))); Red; Auto with arith. +NewDestruct p; Auto with arith. +Intros. Absurd (Zeven (POS (xI p))); Red; Auto with arith. Intros. Absurd (Zeven `1`); Red; Auto with arith. -Destruct p; Auto with arith. -Intros. Absurd (Zeven (NEG (xI p0))); Red; Auto with arith. +NewDestruct p; Auto with arith. +Intros. Absurd (Zeven (NEG (xI p))); Red; Auto with arith. Intros. Absurd (Zeven `-1`); Red; Auto with arith. Save. Lemma Zodd_div2 : (x:Z) `x >= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)+1`. Proof. -Destruct x. +NewDestruct x. Intros. Absurd (Zodd `0`); Red; Auto with arith. -Destruct p; Auto with arith. -Intros. Absurd (Zodd (POS (xO p0))); Red; Auto with arith. +NewDestruct p; Auto with arith. +Intros. Absurd (Zodd (POS (xO p))); Red; Auto with arith. Intros. Absurd `(NEG p) >= 0`; Red; Auto with arith. Save. diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v index f64093034..678e8b472 100644 --- a/theories/ZArith/fast_integer.v +++ b/theories/ZArith/fast_integer.v @@ -1147,7 +1147,7 @@ Save. Theorem Zmult_Zopp_Zopp: (x,y:Z) (Zmult (Zopp x) (Zopp y)) = (Zmult x y). Proof. -Destruct x; Destruct y; Reflexivity. +NewDestruct x; NewDestruct y; Reflexivity. Save. Theorem weak_Zmult_plus_distr_r: diff --git a/theories/ZArith/zarith_aux.v b/theories/ZArith/zarith_aux.v index 72b66c494..7eb1e37c2 100644 --- a/theories/ZArith/zarith_aux.v +++ b/theories/ZArith/zarith_aux.v @@ -46,7 +46,7 @@ Definition Zabs [z:Z] : Z := (*s Properties of absolu function *) Lemma Zabs_eq : (x:Z) (Zle ZERO x) -> (Zabs x)=x. -Destruct x; Auto with arith. +NewDestruct x; Auto with arith. Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith. Save. |