Changeset 4 for C-semantics/Integers.ma


Ignore:
Timestamp:
Jun 2, 2010, 7:11:14 PM (9 years ago)
Author:
campbell
Message:

Some experimental work on executable Clight semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Integers.ma

    r3 r4  
    506506  rewrite half_modulus_modulus. generalize half_modulus_pos. omega. 
    507507Qed.
    508 
     508*)
     509naxiom one_not_zero: one ≠ zero.
     510(*
    509511Theorem one_not_zero: one <> zero.
    510512Proof.
     
    520522  generalize wordsize_pos wordsize_max_unsigned; unfold max_unsigned; omega.
    521523Qed.
    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
     527ntheorem 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
     534ntheorem 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
     542ntheorem 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);
     545nqed.
     546
     547ntheorem 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');
     550nqed.
     551(*
    552552(** ** Modulo arithmetic *)
    553553
Note: See TracChangeset for help on using the changeset viewer.