diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-05 13:00:45 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-05 13:00:45 +0000 |
| commit | 0820d3312b7af1fe220a8fd1dea8545c1122775c (patch) | |
| tree | 34c4785b56c52f57990cba8705e59a9b6341b80c | |
| parent | e5f30bae87af1e8f198b4adad69a81e879efead6 (diff) | |
simplification preuve
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2615 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/ZArith/Zdiv.v | 46 |
1 files changed, 10 insertions, 36 deletions
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 75894ffa3..d1837e89b 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -141,8 +141,7 @@ Case (Zgt_bool b `r+r`); (Rewrite POS_xO; Rewrite H0; Split ; [ Ring | Omega ]). Generalize (Zge_cases b `2`). -Case (Zge_bool b `2`); -(Intros; Split; [Ring | Omega ]). +Case (Zge_bool b `2`); (Intros; Split; [Ring | Omega ]). Omega. Save. @@ -151,23 +150,11 @@ Save. Theorem Z_div_mod : (a,b:Z)`b > 0` -> let (q,r) = (Zdiv_eucl a b) in `a = b*q + r` /\ `0<=r<b`. Proof. -Intros a b; Case a; Case b. -Simpl; Omega. -Simpl; Intros; Omega. -Simpl; Intros; Omega. -Simpl; Intros; Omega. +Intros a b; Case a; Case b; Try (Simpl; Intros; Omega). Unfold Zdiv_eucl; Intros; Apply Z_div_mod_POS; Trivial. Intros. -Absurd `(NEG p) > 0`. -Generalize (NEG_lt_ZERO p). -Omega. -Assumption. - -Intros; Absurd `0>0`. -Unfold Zgt; Simpl. -Discriminate. -Assumption. +Absurd `(NEG p) > 0`; [ Generalize (NEG_lt_ZERO p); Omega | Trivial ]. Intros. Generalize (Z_div_mod_POS (POS p) H p0). @@ -177,34 +164,21 @@ Intros z z0. Case z0. Intros [H1 H2]. -Split. -Replace (NEG p0) with `-(POS p0)`. -Rewrite H1. -Ring. -Trivial. -Trivial. +Split; Trivial. +Replace (NEG p0) with `-(POS p0)`; [ Rewrite H1; Ring | Trivial ]. Intros p1 [H1 H2]. -Split. -Replace (NEG p0) with `-(POS p0)`. -Rewrite H1. -Ring. -Trivial. +Split; Trivial. +Replace (NEG p0) with `-(POS p0)`; [ Rewrite H1; Ring | Trivial ]. Generalize (POS_gt_ZERO p1); Omega. Intros p1 [H1 H2]. -Split. -Replace (NEG p0) with `-(POS p0)`. -Rewrite H1. -Ring. -Trivial. +Split; Trivial. +Replace (NEG p0) with `-(POS p0)`; [ Rewrite H1; Ring | Trivial ]. Generalize (NEG_lt_ZERO p1); Omega. - Intros. -Absurd `(NEG p)>0`. -Generalize (NEG_lt_ZERO p); Omega. -Omega. +Absurd `(NEG p)>0`; [ Generalize (NEG_lt_ZERO p); Omega | Omega ]. Save. |