Changeset 181


Ignore:
Timestamp:
Oct 13, 2010, 4:27:18 PM (9 years ago)
Author:
campbell
Message:

Sort out some axioms.

Location:
C-semantics
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Integers.ma

    r15 r181  
    156156ndefinition neg : int → int ≝ λx. repr (- unsigned x).
    157157
    158 (*
    159 ndefinition zero_ext : Z → int → int ≝
    160 λn,x. repr (modZ (unsigned x) (two_p n)).
    161 ndefinition sign_ext : Z → int → int ≝
    162 λn,x. repr (let p ≝ two_p n in
    163         let y ≝ modZ (unsigned x) p in
    164         if Zltb y (two_p (n-1)) then y else y - p).
    165 *)
    166158nlet rec zero_ext (n:Z) (x:int) on x : int ≝
    167159  repr (modZ (unsigned x) (two_p n)).
     
    204196ndefinition Z_shift_add ≝ λb: bool. λx: Z.
    205197  if b then 2 * x + 1 else 2 * x.
    206 (*
    207 Definition Z_bin_decomp (x: Z) : bool * Z :=
    208   match x with
    209   | Z0 => (false, 0)
    210   | Zpos p =>
    211       match p with
    212       | xI q => (true, Zpos q)
    213       | xO q => (false, Zpos q)
    214       | xH => (true, 0)
    215       end
    216   | Zneg p =>
    217       match p with
    218       | xI q => (true, Zneg q - 1)
    219       | xO q => (false, Zneg q)
    220       | xH => (true, -1)
    221       end
    222   end.
    223 *)
    224 naxiom bits_of_Z : nat → Z → Z → bool.
    225 naxiom Z_of_bits : nat → (Z → bool) → Z.
    226 (*
    227 Fixpoint bits_of_Z (n: nat) (x: Z) {struct n}: Z -> bool :=
    228   match n with
    229   | O =>
    230       (fun i: Z => false)
    231   | S m =>
    232       let (b, y) := Z_bin_decomp x in
    233       let f := bits_of_Z m y in
    234       (fun i: Z => if zeq i 0 then b else f (i - 1))
    235   end.
    236 
    237 Fixpoint Z_of_bits (n: nat) (f: Z -> bool) {struct n}: Z :=
    238   match n with
    239   | O => 0
    240   | S m => Z_shift_add (f 0) (Z_of_bits m (fun i => f (i + 1)))
    241   end.
    242 *)
     198
     199ndefinition Z_bin_decomp : Z → bool × Z ≝
     200λx.match x with
     201[ OZ ⇒ 〈false, OZ〉
     202| pos p ⇒
     203  match p with
     204  [ p1 q ⇒ 〈true, pos q〉
     205  | p0 q ⇒ 〈false, pos q〉
     206  | one ⇒ 〈true, OZ〉
     207  ]
     208| neg p ⇒
     209  match p with
     210  [ p1 q ⇒ 〈true, Zpred (neg q)〉
     211  | p0 q ⇒ 〈false, neg q〉
     212  | one ⇒ 〈true, neg one〉
     213  ]
     214].
     215
     216nlet rec bits_of_Z (n:nat) (x:Z) on n : Z → bool ≝
     217match n with
     218[ O ⇒ λi:Z. false
     219| S m ⇒
     220    match Z_bin_decomp x with [ mk_pair b y ⇒
     221      let f ≝ bits_of_Z m y in
     222      λi:Z. if eqZb i 0 then b else f (Zpred i) ]
     223].
     224
     225nlet rec Z_of_bits (n:nat) (f:Z → bool) on n : Z ≝
     226match n with
     227[ O ⇒ OZ
     228| S m ⇒ Z_shift_add (f OZ) (Z_of_bits m (λi. f (Zsucc i)))
     229].
     230
    243231(* * Bitwise logical ``and'', ``or'' and ``xor'' operations. *)
    244232
     
    744732  apply eqmod_refl. red; exists (-1); ring.
    745733Qed.
    746 
    747 Theorem unsigned_range:
    748   forall i, 0 <= unsigned i < modulus.
    749 Proof.
    750   destruct i; simpl. auto.
    751 Qed.
    752 Hint Resolve unsigned_range: ints.
    753 
    754 Theorem unsigned_range_2:
    755   forall i, 0 <= unsigned i <= max_unsigned.
    756 Proof.
    757   intro; unfold max_unsigned.
    758   generalize (unsigned_range i). omega.
    759 Qed.
    760 Hint Resolve unsigned_range_2: ints.
    761734*)
     735
     736ntheorem unsigned_range: ∀i. 0 ≤ unsigned i ∧ unsigned i < modulus.
     737#i; ncases i; #i' H; ncases H; /2/;
     738nqed.
     739
     740ntheorem unsigned_range_2:
     741  ∀i. 0 ≤ unsigned i ∧ unsigned i ≤ max_unsigned.
     742#i; nrewrite > (?:max_unsigned = modulus - 1); //; (* unfold *)
     743nlapply (unsigned_range i); *; #Hz Hm; @;
     744##[ //;
     745##| nrewrite < (Zpred_Zsucc (unsigned i));
     746    nrewrite < (Zpred_Zplus_neg_O modulus);
     747    napply monotonic_Zle_Zpred;
     748    /2/;
     749##] nqed.
     750
    762751naxiom signed_range:
    763752  ∀i. min_signed ≤ signed i ∧ signed i ≤ max_signed.
    764753(*
     754#i; nwhd in ⊢ (?(??%)(?%?));
     755nlapply (unsigned_range i); *; nletin n ≝ (unsigned i); #H1 H2;
     756napply (Zltb_elim_Type0); #H3;
     757##[ @; ##[ napply (transitive_Zle ? OZ); //;
     758       ##| nrewrite < (Zpred_Zsucc n);
     759           nrewrite < (Zpred_Zplus_neg_O half_modulus);
     760           napply monotonic_Zle_Zpred; /2/;
     761       ##]
     762##| @; ##[ nrewrite > half_modulus_modulus;
     763
    765764Theorem signed_range:
    766765  forall i, min_signed <= signed i <= max_signed.
  • C-semantics/README

    r178 r181  
    1010
    1111- The memory model is executable; some small tests can be found in
    12   test/memorymodel.ma.  Note that the handling of integer values is
    13   axiomatised, so conversions are not yet evaluated.
     12  test/memorymodel.ma.
    1413
    15 - The C syntax has been ported, minus a few lemmas that are not used by
    16   the semantics.
     14- The Clight syntax file has been ported, minus a few lemmas that are not used
     15  by the semantics.
    1716
    18 - Most of the small-step C semantics has been ported, although a few of the
    19   underlying arithmetic functions are only present as axioms.
    20 
    21 - Nonetheless, this is sufficient to animate the semantics of several simple C
    22   programs in test.
     17- The small-step inductively defined Clight semantics has been ported.
    2318
    2419- A collection of definitions and lemmas that probably ought to be in
    2520  matita's standard library can be found in extralib.ma.
    2621
    27 - Some of the machine integers (i.e., integers modulo) results are
    28   given as axioms in Integers.ma.  Implementing them should be routine now that
     22- Some of the theory about machine integers (i.e., integers modulo) are
     23  given as axioms in Integers.ma.  Proving them should be routine now that
    2924  we have a binary representation of integers.  The CompCert version is given
    3025  as a functor on the word size - we don't have an equivalent of this yet.
     
    122117Integers.ma
    123118
    124   Most of the operations have been ported, although some have been left as
    125   axioms because the underlying operation is not present.  The use of the
    126   Coq module system to abstract over the word size has been left out for
    127   now.
     119  The operations have been ported, although the results about them generally
     120  have not.  The equality results have been left axiomatised because they
     121  require proof irrelevance because each integer carries a proof that it is
     122  in range.  The use of the Coq module system to abstract over the word size
     123  has been left out for now.
    128124
    129125Maps.ma
     
    143139Values.ma
    144140
    145   The definitions about values which don't rely on arithmetics operations that
    146   haven't been ported yet are done.  The other definitions and most of the
    147   lemmas still remain to be done.
     141  The definitions about operations relevant to the Clight semantics have been
     142  ported.  The other definitions and most of the lemmas still remain to be done.
    148143
    149144
  • C-semantics/extralib.ma

    r173 r181  
    8383
    8484(* should be proved in nat.ma, but it's not! *)
    85 naxiom eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
     85nlemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
     86#n; nelim n;
     87##[ #m; ncases m; //;
     88##| #n' IH m; ncases m; ##[ /2/; ##| #m'; nwhd in match (eqb (S n') (S m')) in ⊢ %;
     89  nlapply (IH m'); ncases (eqb n' m'); /2/; ##]
     90##] nqed.
    8691
    8792nlemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
     
    269274##| napply Hnlt; napply (Zltb_false_to_not_Zlt … Hb)
    270275##] nqed.
     276
     277nlemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc.
     278#x y; ncases x; ncases y; /2/;
     279#n m; napply (pos_cases … n); napply (pos_cases … m);
     280##[ //;
     281##| #n'; /2/;
     282##| #m'; #H; napply False_ind; nnormalize in H; napply (absurd … (not_le_succ_one m')); /2/;
     283##| #n' m'; #H; nnormalize in H;
     284    nrewrite > (Zsucc_neg_succ n'); nrewrite > (Zsucc_neg_succ m'); /2/;
     285##] nqed.
     286
     287nlemma monotonic_Zle_Zpred: monotonic Z Zle Zpred.
     288#x y; ncases x; ncases y;
     289##[ ##1,2,7,8,9: /2/;
     290##| ##3,4: #m; nnormalize; *;
     291##| #m n; napply (pos_cases … n); napply (pos_cases … m);
     292  ##[ ##1,2: /2/;
     293  ##| #n'; nnormalize; #H; napply False_ind; napply (absurd … (not_le_succ_one n')); /2/;
     294  ##| #n' m'; nrewrite > (Zpred_pos_succ n'); nrewrite > (Zpred_pos_succ m'); /2/;
     295  ##]
     296##| #m n; nnormalize; *;
     297##] nqed.
     298
     299nlemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m).
     300#n; ncases n; //; #n'; #a b H;
     301##[ napply (pos_elim … n');
     302  ##[ nrewrite < (Zsucc_Zplus_pos_O a); nrewrite < (Zsucc_Zplus_pos_O b); /2/;
     303  ##| #n'' H; nrewrite > (?:pos (succ n'') = Zsucc (pos n'')); //;
     304      nrewrite > (Zplus_Zsucc …); nrewrite > (Zplus_Zsucc …); /2/;
     305  ##]
     306##| napply (pos_elim … n');
     307  ##[ nrewrite < (Zpred_Zplus_neg_O a); nrewrite < (Zpred_Zplus_neg_O b); /2/;
     308  ##| #n'' H; nrewrite > (?:neg (succ n'') = Zpred (neg n'')); //;
     309      nrewrite > (Zplus_Zpred …); nrewrite > (Zplus_Zpred …); /2/;
     310  ##]
     311##] nqed.
     312
     313nlemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n).
     314/2/; nqed.
    271315
    272316nlet rec Z_times (x:Z) (y:Z) : Z ≝
Note: See TracChangeset for help on using the changeset viewer.