From 442e82e6ffc6958192f73382d2270e926ead9c80 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Fri, 1 Dec 2017 10:00:05 +0100
Subject: Added simple div_one Theorem variants.

---
 common/Values.v | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

(limited to 'common/Values.v')

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 ->
-- 
cgit