Changeset 10 for C-semantics/Coqlib.ma


Ignore:
Timestamp:
Jul 6, 2010, 11:53:23 AM (10 years ago)
Author:
campbell
Message:

Add binary arithmetic libraries, use for integers and identifiers (but
we're not doing modular arithmetic yet.)
Add a dummy "tree" implementation to make environment lookups executable.
Fix if .. then .. else .. precedence.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Coqlib.ma

    r3 r10  
    1818    library. *)
    1919
    20 include "arithmetics/Z.ma".
     20include "binary/Z.ma".
    2121include "datatypes/sums.ma".
    2222include "datatypes/list.ma".
     
    347347  auto.
    348348Qed.
    349 
    350 (** Properties of powers of two. *)
    351 
    352 Lemma two_power_nat_O : two_power_nat O = 1.
    353 Proof. reflexivity. Qed.
    354 
    355 Lemma two_power_nat_pos : forall n : nat, two_power_nat n > 0.
    356 Proof.
    357   induction n. rewrite two_power_nat_O. omega.
    358   rewrite two_power_nat_S. omega.
    359 Qed.
    360 
    361 Lemma two_power_nat_two_p:
    362   forall x, two_power_nat x = two_p (Z_of_nat x).
    363 Proof.
    364   induction x. auto.
    365   rewrite two_power_nat_S. rewrite inj_S. rewrite two_p_S. omega. omega.
    366 Qed.
    367 
     349*)
     350(* * Properties of powers of two. *)
     351
     352nlemma two_power_nat_O : two_power_nat O = one.
     353//; nqed.
     354
     355nlemma two_power_nat_pos : ∀n:nat. Z_two_power_nat n > 0.
     356//; nqed.
     357
     358nlemma two_power_nat_two_p:
     359  ∀x. Z_two_power_nat x = two_p (Z_of_nat x).
     360#x; ncases x;
     361##[ //;
     362##| nnormalize; #p; nelim p; //; #p' H; nrewrite > (nat_succ_pos …); //;
     363##] nqed.
     364(*
    368365Lemma two_p_monotone:
    369366  forall x y, 0 <= x <= y -> two_p x <= two_p y.
     
    577574(* * Alignment: [align n amount] returns the smallest multiple of [amount]
    578575  greater than or equal to [n]. *)
    579 naxiom align : Z → Z → Z.
    580 (*
     576(*naxiom align : Z → Z → Z.*)
     577
    581578ndefinition align ≝ λn: Z. λamount: Z.
    582579  ((n + amount - 1) / amount) * amount.
    583 
     580(*
    584581Lemma align_le: forall x y, y > 0 -> x <= align x y.
    585582Proof.
Note: See TracChangeset for help on using the changeset viewer.