some more proofs on integers, preparing for absolute value instruction

2 files changed, 19 insertions, 1 deletions

diff --git a/configure b/configure
index 7331a338..00557673 100755
--- a/configure
+++ b/configure
@@ -541,7 +541,7 @@ missingtools=false
 echo "Testing Coq... " | tr -d '\n'
 coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
 case "$coq_ver" in
-  8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0|8.9.1)
+  8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10+beta2)
         echo "version $coq_ver -- good!";;
   ?*)
         echo "version $coq_ver -- UNSUPPORTED"
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index 3370fae3..e9c62a8d 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -2,6 +2,24 @@ Require Import Coqlib.
 Require Import Integers.
 Require Import Values.
 
+Open Scope Z_scope.
+
+Definition abs_diff (x y : Z) := Z.abs (x - y).
+Definition abs_diff2 (x y : Z) :=
+  if x <=? y then y - x else x - y.
+Lemma abs_diff2_correct :
+  forall x y : Z, (abs_diff x y) = (abs_diff2 x y).
+Proof.
+  intros.
+  unfold abs_diff, abs_diff2.
+  unfold Z.leb.
+  pose proof (Z.compare_spec x y) as Hspec.
+  inv Hspec.
+  - rewrite Z.abs_eq; omega.
+  - rewrite Z.abs_neq; omega.
+  - rewrite Z.abs_eq; omega.
+Qed.
+
 Inductive shift1_4 : Type :=
 | SHIFT1 | SHIFT2 | SHIFT3 | SHIFT4.