diff options
Diffstat (limited to 'backend/NeedDomain.v')
| -rw-r--r-- | backend/NeedDomain.v | 31 |
1 files changed, 16 insertions, 15 deletions
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index 692b4f9b..5d19e8f6 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -16,6 +16,7 @@ Require Import Coqlib. Require Import Maps. Require Import IntvSets. Require Import AST. +Require Import Zbits. Require Import Integers. Require Import Floats. Require Import Values. @@ -300,13 +301,13 @@ Proof. rewrite Int.bits_ror. replace (((i - Int.unsigned amount) mod Int.zwordsize + Int.unsigned amount) mod Int.zwordsize) with i. auto. - apply Int.eqmod_small_eq with Int.zwordsize; auto. - apply Int.eqmod_trans with ((i - Int.unsigned amount) + Int.unsigned amount). - apply Int.eqmod_refl2; omega. - eapply Int.eqmod_trans. 2: apply Int.eqmod_mod; auto. - apply Int.eqmod_add. - apply Int.eqmod_mod; auto. - apply Int.eqmod_refl. + apply eqmod_small_eq with Int.zwordsize; auto. + apply eqmod_trans with ((i - Int.unsigned amount) + Int.unsigned amount). + apply eqmod_refl2; omega. + eapply eqmod_trans. 2: apply eqmod_mod; auto. + apply eqmod_add. + apply eqmod_mod; auto. + apply eqmod_refl. apply Z_mod_lt; auto. apply Z_mod_lt; auto. Qed. @@ -324,7 +325,7 @@ Qed. Lemma eqmod_iagree: forall m x y, - Int.eqmod (two_p (Int.size m)) x y -> + eqmod (two_p (Int.size m)) x y -> iagree (Int.repr x) (Int.repr y) m. Proof. intros. set (p := Z.to_nat (Int.size m)). @@ -333,7 +334,7 @@ Proof. rewrite EQ in H; rewrite <- two_power_nat_two_p in H. red; intros. rewrite ! Int.testbit_repr by auto. destruct (zlt i (Int.size m)). - eapply Int.same_bits_eqmod; eauto. omega. + eapply same_bits_eqmod; eauto. omega. assert (Int.testbit m i = false) by (eapply Int.bits_size_2; omega). congruence. Qed. @@ -343,13 +344,13 @@ Definition complete_mask (m: int) := Int.zero_ext (Int.size m) Int.mone. Lemma iagree_eqmod: forall x y m, iagree x y (complete_mask m) -> - Int.eqmod (two_p (Int.size m)) (Int.unsigned x) (Int.unsigned y). + eqmod (two_p (Int.size m)) (Int.unsigned x) (Int.unsigned y). Proof. intros. set (p := Z.to_nat (Int.size m)). generalize (Int.size_range m); intros RANGE. assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. omega. } rewrite EQ; rewrite <- two_power_nat_two_p. - apply Int.eqmod_same_bits. intros. apply H. omega. + apply eqmod_same_bits. intros. apply H. omega. unfold complete_mask. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by omega. rewrite Int.bits_mone by omega. auto. Qed. @@ -362,7 +363,7 @@ Proof. + assert (Int.unsigned m <> 0). { red; intros; elim n. rewrite <- (Int.repr_unsigned m). rewrite H; auto. } assert (0 < Int.size m). - { apply Int.Zsize_pos'. generalize (Int.unsigned_range m); omega. } + { apply Zsize_pos'. generalize (Int.unsigned_range m); omega. } generalize (Int.size_range m); intros. f_equal. apply Int.bits_size_4. tauto. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by omega. @@ -610,7 +611,7 @@ Proof. unfold modarith; intros. destruct x; simpl in *. - auto. - unfold Val.add; InvAgree. - apply eqmod_iagree. apply Int.eqmod_add; apply iagree_eqmod; auto. + apply eqmod_iagree. apply eqmod_add; apply iagree_eqmod; auto. - inv H; auto. inv H0; auto. destruct w1; auto. Qed. @@ -626,7 +627,7 @@ Lemma mul_sound: Proof. unfold mul, add; intros. destruct x; simpl in *. - auto. -- unfold Val.mul; InvAgree. apply eqmod_iagree. apply Int.eqmod_mult; apply iagree_eqmod; auto. +- unfold Val.mul; InvAgree. apply eqmod_iagree. apply eqmod_mult; apply iagree_eqmod; auto. - inv H; auto. inv H0; auto. destruct w1; auto. Qed. @@ -638,7 +639,7 @@ Proof. intros; destruct x; simpl in *. - auto. - unfold Val.neg; InvAgree. - apply eqmod_iagree. apply Int.eqmod_neg. apply iagree_eqmod; auto. + apply eqmod_iagree. apply eqmod_neg. apply iagree_eqmod; auto. - inv H; simpl; auto. Qed. |