Changeset 181 for C-semantics

Timestamp:

Oct 13, 2010, 4:27:18 PM (10 years ago)

Author:

campbell

Message:

Sort out some axioms.

Location:

C-semantics

Files:

• Integers.ma (modified) (3 diffs)
• README (modified) (3 diffs)
• extralib.ma (modified) (2 diffs)

C-semantics/Integers.ma

@@ -156 +156 @@
 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)).
@@ -204 +196 @@
 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. *)
 
@@ -744 +732 @@
   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

@@ -10 +10 @@
 
 - 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.
@@ -122 +117 @@
 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
@@ -143 +139 @@
 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

@@ -83 +83 @@
 
 (* 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 ].
@@ -269 +274 @@
 ##| 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 ≝