Changeset 4 for Csemantics/Integers.ma
 Timestamp:
 Jun 2, 2010, 7:11:14 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Integers.ma
r3 r4 506 506 rewrite half_modulus_modulus. generalize half_modulus_pos. omega. 507 507 Qed. 508 508 *) 509 naxiom one_not_zero: one ≠ zero. 510 (* 509 511 Theorem one_not_zero: one <> zero. 510 512 Proof. … … 520 522 generalize wordsize_pos wordsize_max_unsigned; unfold max_unsigned; omega. 521 523 Qed. 522 523 (** ** Properties of equality *) 524 525 Theorem eq_sym: 526 forall x y, eq x y = eq y x. 527 Proof. 528 intros; unfold eq. case (zeq (unsigned x) (unsigned y)); intro. 529 rewrite e. rewrite zeq_true. auto. 530 rewrite zeq_false. auto. auto. 531 Qed. 532 533 Theorem eq_spec: forall (x y: int), if eq x y then x = y else x <> y. 534 Proof. 535 intros; unfold eq. case (eq_dec x y); intro. 536 subst y. rewrite zeq_true. auto. 537 rewrite zeq_false. auto. 538 destruct x; destruct y. 539 simpl. red; intro. elim n. apply mkint_eq. auto. 540 Qed. 541 542 Theorem eq_true: forall x, eq x x = true. 543 Proof. 544 intros. generalize (eq_spec x x); case (eq x x); intros; congruence. 545 Qed. 546 547 Theorem eq_false: forall x y, x <> y > eq x y = false. 548 Proof. 549 intros. generalize (eq_spec x y); case (eq x y); intros; congruence. 550 Qed. 551 524 *) 525 (* * ** Properties of equality *) 526 527 ntheorem eq_sym: 528 ∀x,y. eq x y = eq y x. 529 #x y; nwhd in ⊢ (??%%); napply eqZb_elim; #H; 530 ##[ nrewrite > H; nrewrite > (eqZb_z_z …); // 531 ## nrewrite > (eqZb_false … (sym_neq … H)); // 532 ##] nqed. 533 534 ntheorem eq_spec: ∀x,y: int. if eq x y then x = y else (x ≠ y). 535 #x y; nwhd in ⊢ (??%??); nelim (eq_dec x y); #H; 536 ##[ nrewrite > H; nrewrite > (eqZb_z_z …); //; 537 ## nrewrite > (eqZb_false …); //; 538 nelim x in H ⊢ %; nelim y; 539 #x' Px y' Py H; nnormalize; napply (not_to_not … H); napply mk_int_eq; 540 ##] nqed. 541 542 ntheorem eq_true: ∀x. eq x x = true. 543 #x; nlapply (eq_spec x x); nelim (eq x x); //; 544 #H; nnormalize in H; napply False_ind; napply (absurd ? (refl ??) H); 545 nqed. 546 547 ntheorem eq_false: ∀x,y. x ≠ y → eq x y = false. 548 #x y; nlapply (eq_spec x y); nelim (eq x y); //; 549 #H H'; napply False_ind; napply (absurd ? H H'); 550 nqed. 551 (* 552 552 (** ** Modulo arithmetic *) 553 553
Note: See TracChangeset
for help on using the changeset viewer.