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 /theories/ZArith/Zmisc.v | |
| 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
Diffstat (limited to 'theories/ZArith/Zmisc.v')
| -rw-r--r-- | theories/ZArith/Zmisc.v | 20 |
1 files changed, 10 insertions, 10 deletions
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. |