From 0f5087bea45be49e105727d6cee4194598474fee Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 5 Jul 2011 04:13:33 +0000
Subject: Back from Oregon commit. powerpc/*: better compilation of some
 comparisons; revised asmgenproof1. common/*: added Mem.storebytes; used to
 give semantics to memcpy builtin.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1679 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 lib/Coqlib.v   | 14 ++++++++++++++
 lib/Integers.v | 10 ++++++++++
 2 files changed, 24 insertions(+)

(limited to 'lib')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 4fc922b..f4d50e8 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -606,6 +606,13 @@ Definition nat_of_Z (z: Z) : nat :=
   | Zneg p => O
   end.
 
+Lemma nat_of_Z_of_nat:
+  forall n, nat_of_Z (Z_of_nat n) = n.
+Proof.
+  intros. unfold Z_of_nat. destruct n. auto.
+  simpl. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. auto.
+Qed.
+
 Lemma nat_of_Z_max:
   forall z, Z_of_nat (nat_of_Z z) = Zmax z 0.
 Proof.
@@ -1133,6 +1140,13 @@ Proof.
   induction 1; intros; simpl. auto. constructor; auto. 
 Qed.
 
+Lemma list_forall2_length:
+  forall l1 l2,
+  list_forall2 l1 l2 -> length l1 = length l2.
+Proof.
+  induction 1; simpl; congruence.
+Qed.
+
 End FORALL2.
 
 Lemma list_forall2_imply:
diff --git a/lib/Integers.v b/lib/Integers.v
index 30f692a..6e7a6cb 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -167,6 +167,11 @@ Definition divu (x y: int) : int :=
 Definition modu (x y: int) : int :=
   repr (Zmod (unsigned x) (unsigned y)).
 
+Definition add_carry (x y cin: int): int :=
+  if zlt (unsigned x + unsigned y + unsigned cin) modulus
+  then zero
+  else one.
+
 (** For bitwise operations, we need to convert between Coq integers [Z]
   and their bit-level representations.  Bit-level representations are
   represented as characteristic functions, that is, functions [f]
@@ -746,6 +751,11 @@ Proof.
   rewrite Zplus_0_r. apply repr_unsigned.
 Qed.
 
+Theorem add_zero_l: forall x, add zero x = x.
+Proof.
+  intros. rewrite add_commut. apply add_zero.
+Qed.
+
 Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z).
 Proof.
   intros; unfold add.
-- 
cgit v1.2.3