summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Integers.v128
1 files changed, 107 insertions, 21 deletions
diff --git a/lib/Integers.v b/lib/Integers.v
index 9844ed1..a76049b 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -1398,6 +1398,16 @@ Proof.
unfold z; auto.
Qed.
+Lemma Z_of_bits_equal:
+ forall f x,
+ (forall i, 0 <= i < Z_of_nat wordsize -> f i = bits_of_Z wordsize (unsigned x) i) ->
+ repr (Z_of_bits wordsize f 0) = x.
+Proof.
+ intros. transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)) 0)).
+ f_equal. apply Z_of_bits_exten; intros. apply H. omega.
+ apply eqm_repr_eq. apply Z_of_bits_of_Z.
+Qed.
+
(** ** Properties of bitwise and, or, xor *)
Lemma bitwise_binop_commut:
@@ -1427,9 +1437,7 @@ Lemma bitwise_binop_idem:
forall x,
bitwise_binop f x x = x.
Proof.
- unfold bitwise_binop; intros.
- apply eqm_repr_eq. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
- apply eqm_refl2. apply Z_of_bits_exten. auto.
+ unfold bitwise_binop; intros. apply Z_of_bits_equal; intros. auto.
Qed.
Theorem and_commut: forall x y, and x y = and y x.
@@ -1440,21 +1448,27 @@ Proof (bitwise_binop_assoc andb andb_assoc).
Theorem and_zero: forall x, and x zero = zero.
Proof.
- intros. unfold and, bitwise_binop.
- apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
- apply eqm_refl2. apply Z_of_bits_exten. intros.
+ intros. unfold and, bitwise_binop. apply Z_of_bits_equal; intros.
rewrite unsigned_zero. rewrite bits_of_Z_zero. apply andb_b_false.
Qed.
+Corollary and_zero_l: forall x, and zero x = zero.
+Proof.
+ intros. rewrite and_commut. apply and_zero.
+Qed.
+
Theorem and_mone: forall x, and x mone = x.
Proof.
- intros. unfold and, bitwise_binop.
- apply eqm_repr_eq. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
- apply eqm_refl2. apply Z_of_bits_exten; intros.
+ intros. unfold and, bitwise_binop. apply Z_of_bits_equal; intros.
rewrite unsigned_mone. rewrite bits_of_Z_mone. apply andb_b_true.
omega.
Qed.
+Corollary and_mone_l: forall x, and mone x = x.
+Proof.
+ intros. rewrite and_commut. apply and_mone.
+Qed.
+
Theorem and_idem: forall x, and x x = x.
Proof.
intros. apply (bitwise_binop_idem andb). destruct a; auto.
@@ -1468,21 +1482,27 @@ Proof (bitwise_binop_assoc orb orb_assoc).
Theorem or_zero: forall x, or x zero = x.
Proof.
- intros. unfold or, bitwise_binop.
- apply eqm_repr_eq. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
- apply eqm_refl2. apply Z_of_bits_exten. intros.
+ intros. unfold or, bitwise_binop. apply Z_of_bits_equal; intros.
rewrite unsigned_zero. rewrite bits_of_Z_zero. apply orb_b_false.
Qed.
+Corollary or_zero_l: forall x, or zero x = x.
+Proof.
+ intros. rewrite or_commut. apply or_zero.
+Qed.
+
Theorem or_mone: forall x, or x mone = mone.
Proof.
- intros. unfold or, bitwise_binop.
- apply eqm_repr_eq. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
- apply eqm_refl2. apply Z_of_bits_exten. intros.
+ intros. unfold or, bitwise_binop. apply Z_of_bits_equal; intros.
rewrite unsigned_mone. rewrite bits_of_Z_mone. apply orb_b_true.
omega.
Qed.
+Corollary or_mone_l: forall x, or mone x = mone.
+Proof.
+ intros. rewrite or_commut. apply or_mone.
+Qed.
+
Theorem or_idem: forall x, or x x = x.
Proof.
intros. apply (bitwise_binop_idem orb). destruct a; auto.
@@ -1499,6 +1519,49 @@ Proof.
apply demorgan1.
Qed.
+Corollary and_or_distrib_l:
+ forall x y z,
+ and (or x y) z = or (and x z) (and y z).
+Proof.
+ intros. rewrite (and_commut (or x y)). rewrite and_or_distrib. f_equal; apply and_commut.
+Qed.
+
+Theorem or_and_distrib:
+ forall x y z,
+ or x (and y z) = and (or x y) (or x z).
+Proof.
+ intros; unfold and, or, bitwise_binop.
+ repeat rewrite unsigned_repr; auto with ints.
+ decEq; apply Z_of_bits_exten; intros.
+ repeat rewrite bits_of_Z_of_bits; repeat rewrite Zplus_0_r; auto.
+ apply orb_andb_distrib_r.
+Qed.
+
+Corollary or_and_distrib_l:
+ forall x y z,
+ or (and x y) z = and (or x z) (or y z).
+Proof.
+ intros. rewrite (or_commut (and x y)). rewrite or_and_distrib. f_equal; apply or_commut.
+Qed.
+
+Theorem and_or_absorb: forall x y, and x (or x y) = x.
+Proof.
+ intros; unfold and, or, bitwise_binop. apply Z_of_bits_equal; intros.
+ rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits.
+ assert (forall a b, a && (a || b) = a) by (destruct a; destruct b; auto).
+ auto.
+ omega.
+Qed.
+
+Theorem or_and_absorb: forall x y, or x (and x y) = x.
+Proof.
+ intros; unfold and, or, bitwise_binop. apply Z_of_bits_equal; intros.
+ rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits.
+ assert (forall a b, a || (a && b) = a) by (destruct a; destruct b; auto).
+ auto.
+ omega.
+Qed.
+
Theorem xor_commut: forall x y, xor x y = xor y x.
Proof (bitwise_binop_commut xorb xorb_comm).
@@ -1510,17 +1573,18 @@ Qed.
Theorem xor_zero: forall x, xor x zero = x.
Proof.
- intros. unfold xor, bitwise_binop.
- apply eqm_repr_eq. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
- apply eqm_refl2. apply Z_of_bits_exten. intros.
+ intros. unfold xor, bitwise_binop. apply Z_of_bits_equal; intros.
rewrite unsigned_zero. rewrite bits_of_Z_zero. apply xorb_false.
Qed.
+Corollary xor_zero_l: forall x, xor zero x = x.
+Proof.
+ intros. rewrite xor_commut. apply xor_zero.
+Qed.
+
Theorem xor_idem: forall x, xor x x = zero.
Proof.
- intros. unfold xor, bitwise_binop.
- apply eqm_repr_eq. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
- apply eqm_refl2. apply Z_of_bits_exten. intros.
+ intros. unfold xor, bitwise_binop. apply Z_of_bits_equal; intros.
rewrite unsigned_zero. rewrite bits_of_Z_zero. apply xorb_nilpotent.
Qed.
@@ -1530,6 +1594,28 @@ Proof. rewrite xor_commut. apply xor_zero. Qed.
Theorem xor_one_one: xor one one = zero.
Proof. apply xor_idem. Qed.
+Theorem xor_zero_equal: forall x y, xor x y = zero -> x = y.
+Proof.
+ unfold xor, bitwise_binop; intros.
+ set (ux := unsigned x) in *. set (uy := unsigned y) in *.
+ set (fx := bits_of_Z wordsize ux) in *.
+ set (fy := bits_of_Z wordsize uy) in *.
+ assert (forall i, 0 <= i < Z_of_nat wordsize -> fx i = fy i).
+ intros.
+ assert (bits_of_Z wordsize (unsigned (repr (Z_of_bits wordsize (fun i => xorb (fx i) (fy i)) 0))) i = false).
+ rewrite H. rewrite unsigned_zero. apply bits_of_Z_zero.
+ rewrite unsigned_repr in H1; auto with ints.
+ rewrite bits_of_Z_of_bits in H1; auto.
+ destruct (fx i); destruct (fy i); simpl in H1; congruence.
+ rewrite <- (repr_unsigned x); fold ux.
+ rewrite <- (repr_unsigned y); fold uy.
+ apply eqm_samerepr.
+ eapply eqm_trans. apply eqm_sym. apply Z_of_bits_of_Z.
+ eapply eqm_trans. 2: apply Z_of_bits_of_Z.
+ fold fx; fold fy. apply eqm_refl2.
+ apply Z_of_bits_exten. intros; apply H0; omega.
+Qed.
+
Theorem and_xor_distrib:
forall x y z,
and x (xor y z) = xor (and x y) (and x z).