← Back to branch summary

~naesten/coq/trunk

« back to all changes in this revision

Viewing changes to theories/Numbers/Integer/BigZ/ZMake.v

  • Committer: letouzey
  • Date: 2009-11-10 11:19:48 UTC
  • Revision ID: svn-v4:85f007b7-540e-0410-9357-904b9bb8a0f7:trunk:12490
SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMax

 To retrieve the old behavior of spec_sub0 and spec_sub with
 precondition on order, just chain spec_sub with Zmax_r or Zmax_l.
 Idem with spec_pred0 and spec_pred.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Numbers/Integer/BigZ/ZMake.v
191
191
 simpl; generalize (N.spec_compare N.zero x); case N.compare;
192
192
   rewrite N.spec_0; simpl.
193
193
  intros HH; rewrite <- HH; rewrite N.spec_1; ring.
194
 
  intros HH; rewrite N.spec_pred; auto with zarith.
 
194
  intros HH; rewrite N.spec_pred, Zmax_r; auto with zarith.
195
195
 generalize (N.spec_pos x); auto with zarith.
196
196
 Qed.
197
197
 
218
218
   exact (N.spec_add x y).
219
219
 unfold zero; generalize (N.spec_compare x y); case N.compare.
220
220
   rewrite N.spec_0; auto with zarith.
221
 
 intros; rewrite N.spec_sub; try ring; auto with zarith.
222
 
 intros; rewrite N.spec_sub; try ring; auto with zarith.
 
221
 intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
 
222
 intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
223
223
 unfold zero; generalize (N.spec_compare x y); case N.compare.
224
224
   rewrite N.spec_0; auto with zarith.
225
 
 intros; rewrite N.spec_sub; try ring; auto with zarith.
226
 
 intros; rewrite N.spec_sub; try ring; auto with zarith.
227
 
 intros; rewrite N.spec_add; try ring; auto with zarith.
 
225
 intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
 
226
 intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
 
227
 intros; rewrite N.spec_add; auto with zarith.
228
228
 Qed.
229
229
 
230
230
 Definition pred x :=
241
241
 unfold pred, to_Z, minus_one; intros [x | x].
242
242
   generalize (N.spec_compare N.zero x); case N.compare;
243
243
     rewrite N.spec_0; try rewrite N.spec_1; auto with zarith.
244
 
   intros H; exact (N.spec_pred _ H).
 
244
   intros H; rewrite N.spec_pred, Zmax_r; auto with zarith.
245
245
 generalize (N.spec_pos x); auto with zarith.
246
246
 rewrite N.spec_succ; ring.
247
247
 Qed.
268
268
 unfold sub, to_Z; intros [x | x] [y | y].
269
269
 unfold zero; generalize (N.spec_compare x y); case N.compare.
270
270
   rewrite N.spec_0; auto with zarith.
271
 
 intros; rewrite N.spec_sub; try ring; auto with zarith.
272
 
 intros; rewrite N.spec_sub; try ring; auto with zarith.
273
 
 rewrite N.spec_add; ring.
274
 
 rewrite N.spec_add; ring.
 
271
 intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
 
272
 intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
 
273
 rewrite N.spec_add; auto with zarith.
 
274
 rewrite N.spec_add; auto with zarith.
275
275
 unfold zero; generalize (N.spec_compare x y); case N.compare.
276
276
   rewrite N.spec_0; auto with zarith.
277
 
 intros; rewrite N.spec_sub; try ring; auto with zarith.
278
 
 intros; rewrite N.spec_sub; try ring; auto with zarith.
 
277
 intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
 
278
 intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
279
279
 Qed.
280
280
 
281
281
 Definition mul x y :=
398
398
 rewrite N.spec_0; intros H2.
399
399
 change (- Zpos p) with (Zneg p); lazy iota beta.
400
400
 intros H3; rewrite <- H3; auto.
401
 
 rewrite N.spec_succ; rewrite N.spec_sub.
 
401
 rewrite N.spec_succ; rewrite N.spec_sub, Zmax_r.
402
402
 generalize H2; case (N.to_Z r).
403
403
 intros; apply False_ind; auto with zarith.
404
404
 intros p2 _; rewrite He; auto with zarith.
430
430
 rewrite N.spec_0; intros H2.
431
431
 change (- Zpos p1) with (Zneg p1); lazy iota beta.
432
432
 intros H3; rewrite <- H3; auto.
433
 
 rewrite N.spec_succ; rewrite N.spec_sub.
 
433
 rewrite N.spec_succ; rewrite N.spec_sub, Zmax_r.
434
434
 generalize H2; case (N.to_Z r).
435
435
 intros; apply False_ind; auto with zarith.
436
436
 intros p2 _; rewrite He; auto with zarith.