diff options
Diffstat (limited to 'lib/Integers.v')
| -rw-r--r-- | lib/Integers.v | 10 |
1 files changed, 10 insertions, 0 deletions
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. |