# Changeset 181

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

Sort out some axioms.

Location:
C-semantics
Files:
3 edited

Unmodified
Added
Removed
• ## C-semantics/Integers.ma

 r15 ndefinition neg : int → int ≝ λx. repr (- unsigned x). (* ndefinition zero_ext : Z → int → int ≝ λn,x. repr (modZ (unsigned x) (two_p n)). ndefinition sign_ext : Z → int → int ≝ λn,x. repr (let p ≝ two_p n in let y ≝ modZ (unsigned x) p in if Zltb y (two_p (n-1)) then y else y - p). *) nlet rec zero_ext (n:Z) (x:int) on x : int ≝ repr (modZ (unsigned x) (two_p n)). ndefinition Z_shift_add ≝ λb: bool. λx: Z. if b then 2 * x + 1 else 2 * x. (* Definition Z_bin_decomp (x: Z) : bool * Z := match x with | Z0 => (false, 0) | Zpos p => match p with | xI q => (true, Zpos q) | xO q => (false, Zpos q) | xH => (true, 0) end | Zneg p => match p with | xI q => (true, Zneg q - 1) | xO q => (false, Zneg q) | xH => (true, -1) end end. *) naxiom bits_of_Z : nat → Z → Z → bool. naxiom Z_of_bits : nat → (Z → bool) → Z. (* Fixpoint bits_of_Z (n: nat) (x: Z) {struct n}: Z -> bool := match n with | O => (fun i: Z => false) | S m => let (b, y) := Z_bin_decomp x in let f := bits_of_Z m y in (fun i: Z => if zeq i 0 then b else f (i - 1)) end. Fixpoint Z_of_bits (n: nat) (f: Z -> bool) {struct n}: Z := match n with | O => 0 | S m => Z_shift_add (f 0) (Z_of_bits m (fun i => f (i + 1))) end. *) ndefinition Z_bin_decomp : Z → bool × Z ≝ λx.match x with [ OZ ⇒ 〈false, OZ〉 | pos p ⇒ match p with [ p1 q ⇒ 〈true, pos q〉 | p0 q ⇒ 〈false, pos q〉 | one ⇒ 〈true, OZ〉 ] | neg p ⇒ match p with [ p1 q ⇒ 〈true, Zpred (neg q)〉 | p0 q ⇒ 〈false, neg q〉 | one ⇒ 〈true, neg one〉 ] ]. nlet rec bits_of_Z (n:nat) (x:Z) on n : Z → bool ≝ match n with [ O ⇒ λi:Z. false | S m ⇒ match Z_bin_decomp x with [ mk_pair b y ⇒ let f ≝ bits_of_Z m y in λi:Z. if eqZb i 0 then b else f (Zpred i) ] ]. nlet rec Z_of_bits (n:nat) (f:Z → bool) on n : Z ≝ match n with [ O ⇒ OZ | S m ⇒ Z_shift_add (f OZ) (Z_of_bits m (λi. f (Zsucc i))) ]. (* * Bitwise logical ``and'', ``or'' and ``xor'' operations. *) apply eqmod_refl. red; exists (-1); ring. Qed. Theorem unsigned_range: forall i, 0 <= unsigned i < modulus. Proof. destruct i; simpl. auto. Qed. Hint Resolve unsigned_range: ints. Theorem unsigned_range_2: forall i, 0 <= unsigned i <= max_unsigned. Proof. intro; unfold max_unsigned. generalize (unsigned_range i). omega. Qed. Hint Resolve unsigned_range_2: ints. *) ntheorem unsigned_range: ∀i. 0 ≤ unsigned i ∧ unsigned i < modulus. #i; ncases i; #i' H; ncases H; /2/; nqed. ntheorem unsigned_range_2: ∀i. 0 ≤ unsigned i ∧ unsigned i ≤ max_unsigned. #i; nrewrite > (?:max_unsigned = modulus - 1); //; (* unfold *) nlapply (unsigned_range i); *; #Hz Hm; @; ##[ //; ##| nrewrite < (Zpred_Zsucc (unsigned i)); nrewrite < (Zpred_Zplus_neg_O modulus); napply monotonic_Zle_Zpred; /2/; ##] nqed. naxiom signed_range: ∀i. min_signed ≤ signed i ∧ signed i ≤ max_signed. (* #i; nwhd in ⊢ (?(??%)(?%?)); nlapply (unsigned_range i); *; nletin n ≝ (unsigned i); #H1 H2; napply (Zltb_elim_Type0); #H3; ##[ @; ##[ napply (transitive_Zle ? OZ); //; ##| nrewrite < (Zpred_Zsucc n); nrewrite < (Zpred_Zplus_neg_O half_modulus); napply monotonic_Zle_Zpred; /2/; ##] ##| @; ##[ nrewrite > half_modulus_modulus; Theorem signed_range: forall i, min_signed <= signed i <= max_signed.
• ## C-semantics/README

 r178 - The memory model is executable; some small tests can be found in test/memorymodel.ma.  Note that the handling of integer values is axiomatised, so conversions are not yet evaluated. test/memorymodel.ma. - The C syntax has been ported, minus a few lemmas that are not used by the semantics. - The Clight syntax file has been ported, minus a few lemmas that are not used by the semantics. - Most of the small-step C semantics has been ported, although a few of the underlying arithmetic functions are only present as axioms. - Nonetheless, this is sufficient to animate the semantics of several simple C programs in test. - The small-step inductively defined Clight semantics has been ported. - A collection of definitions and lemmas that probably ought to be in matita's standard library can be found in extralib.ma. - Some of the machine integers (i.e., integers modulo) results are given as axioms in Integers.ma.  Implementing them should be routine now that - Some of the theory about machine integers (i.e., integers modulo) are given as axioms in Integers.ma.  Proving them should be routine now that we have a binary representation of integers.  The CompCert version is given as a functor on the word size - we don't have an equivalent of this yet. Integers.ma Most of the operations have been ported, although some have been left as axioms because the underlying operation is not present.  The use of the Coq module system to abstract over the word size has been left out for now. The operations have been ported, although the results about them generally have not.  The equality results have been left axiomatised because they require proof irrelevance because each integer carries a proof that it is in range.  The use of the Coq module system to abstract over the word size has been left out for now. Maps.ma Values.ma The definitions about values which don't rely on arithmetics operations that haven't been ported yet are done.  The other definitions and most of the lemmas still remain to be done. The definitions about operations relevant to the Clight semantics have been ported.  The other definitions and most of the lemmas still remain to be done.
• ## C-semantics/extralib.ma

 r173 (* should be proved in nat.ma, but it's not! *) naxiom eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ]. nlemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ]. #n; nelim n; ##[ #m; ncases m; //; ##| #n' IH m; ncases m; ##[ /2/; ##| #m'; nwhd in match (eqb (S n') (S m')) in ⊢ %; nlapply (IH m'); ncases (eqb n' m'); /2/; ##] ##] nqed. nlemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ]. ##| napply Hnlt; napply (Zltb_false_to_not_Zlt … Hb) ##] nqed. nlemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc. #x y; ncases x; ncases y; /2/; #n m; napply (pos_cases … n); napply (pos_cases … m); ##[ //; ##| #n'; /2/; ##| #m'; #H; napply False_ind; nnormalize in H; napply (absurd … (not_le_succ_one m')); /2/; ##| #n' m'; #H; nnormalize in H; nrewrite > (Zsucc_neg_succ n'); nrewrite > (Zsucc_neg_succ m'); /2/; ##] nqed. nlemma monotonic_Zle_Zpred: monotonic Z Zle Zpred. #x y; ncases x; ncases y; ##[ ##1,2,7,8,9: /2/; ##| ##3,4: #m; nnormalize; *; ##| #m n; napply (pos_cases … n); napply (pos_cases … m); ##[ ##1,2: /2/; ##| #n'; nnormalize; #H; napply False_ind; napply (absurd … (not_le_succ_one n')); /2/; ##| #n' m'; nrewrite > (Zpred_pos_succ n'); nrewrite > (Zpred_pos_succ m'); /2/; ##] ##| #m n; nnormalize; *; ##] nqed. nlemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m). #n; ncases n; //; #n'; #a b H; ##[ napply (pos_elim … n'); ##[ nrewrite < (Zsucc_Zplus_pos_O a); nrewrite < (Zsucc_Zplus_pos_O b); /2/; ##| #n'' H; nrewrite > (?:pos (succ n'') = Zsucc (pos n'')); //; nrewrite > (Zplus_Zsucc …); nrewrite > (Zplus_Zsucc …); /2/; ##] ##| napply (pos_elim … n'); ##[ nrewrite < (Zpred_Zplus_neg_O a); nrewrite < (Zpred_Zplus_neg_O b); /2/; ##| #n'' H; nrewrite > (?:neg (succ n'') = Zpred (neg n'')); //; nrewrite > (Zplus_Zpred …); nrewrite > (Zplus_Zpred …); /2/; ##] ##] nqed. nlemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n). /2/; nqed. nlet rec Z_times (x:Z) (y:Z) : Z ≝
Note: See TracChangeset for help on using the changeset viewer.