diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-12-01 10:00:05 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-12-01 10:00:05 +0100 |
| commit | 442e82e6ffc6958192f73382d2270e926ead9c80 (patch) | |
| tree | 24409429d6ab33acaa16d30bac07558d5204b7aa /common | |
| parent | d4070c456e71b6edfc9b65e5ec837370fea8e9d0 (diff) | |
| download | compcert-442e82e6ffc6958192f73382d2270e926ead9c80.tar.gz compcert-442e82e6ffc6958192f73382d2270e926ead9c80.zip | |
Added simple div_one Theorem variants.
Diffstat (limited to 'common')
| -rw-r--r-- | common/Values.v | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/common/Values.v b/common/Values.v index 802d827b..a20dd567 100644 --- a/common/Values.v +++ b/common/Values.v @@ -1181,6 +1181,16 @@ Proof. simpl. rewrite H0. decEq. decEq. symmetry. apply Int.divs_pow2. auto. Qed. +Theorem divs_one: + forall s , divs (Vint s) (Vint Int.one) = Some (Vint s). +Proof. + intros. + unfold divs. rewrite Int.eq_false; try discriminate. + simpl. rewrite (Int.eq_false Int.one Int.mone); try discriminate. + rewrite andb_false_intro2; auto. f_equal. f_equal. + rewrite Int.divs_one; auto. replace Int.zwordsize with 32; auto. omega. +Qed. + Theorem divu_pow2: forall x n logn y, Int.is_power2 n = Some logn -> @@ -1194,6 +1204,13 @@ Proof. decEq. symmetry. apply Int.divu_pow2. auto. Qed. +Theorem divu_one: + forall s, divu (Vint s) (Vint Int.one) = Some (Vint s). +Proof. + intros. simpl. rewrite Int.eq_false; try discriminate. + f_equal. f_equal. apply Int.divu_one. +Qed. + Theorem modu_pow2: forall x n logn y, Int.is_power2 n = Some logn -> @@ -1524,6 +1541,16 @@ Proof. rewrite Int64.repr_unsigned. auto. Qed. +Theorem divls_one: + forall n, divls (Vlong n) (Vlong Int64.one) = Some (Vlong n). +Proof. + intros. unfold divls. rewrite Int64.eq_false; try discriminate. + rewrite (Int64.eq_false Int64.one Int64.mone); try discriminate. + rewrite andb_false_intro2; auto. + simpl. f_equal. f_equal. apply Int64.divs_one. + replace Int64.zwordsize with 64; auto. omega. +Qed. + Theorem divlu_pow2: forall x n logn y, Int64.is_power2' n = Some logn -> @@ -1537,6 +1564,13 @@ Proof. decEq. symmetry. apply Int64.divu_pow2'. auto. Qed. +Theorem divlu_one: + forall n, divlu (Vlong n) (Vlong Int64.one) = Some (Vlong n). +Proof. + intros. unfold divlu. rewrite Int64.eq_false; try discriminate. + simpl. f_equal. f_equal. apply Int64.divu_one. +Qed. + Theorem modlu_pow2: forall x n logn y, Int64.is_power2 n = Some logn -> |