Use Z.max 0, not an if statement

Leads to fewer match branches

2 files changed, 8 insertions, 19 deletions

diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v
index 087c77497..3c35bdc9e 100644
--- a/src/Compilers/Z/Syntax/Util.v
+++ b/src/Compilers/Z/Syntax/Util.v
@@ -111,9 +111,7 @@ Lemma interpToZ_cast_const_mod {a b} v
   : interpToZ (@cast_const a b v)
     = match b with
       | TZ => interpToZ v
-      | TWord lgsz => if (0 <=? interpToZ v)%Z
-                      then (interpToZ v) mod (2^Z.of_nat (2^lgsz))
-                      else 0
+      | TWord lgsz => Z.max 0 (interpToZ v) mod (2^Z.of_nat (2^lgsz))
       end%Z.
 Proof.
   repeat first [ progress destruct_head base_type
@@ -125,9 +123,7 @@ Lemma cast_const_ZToInterp_mod {a b} v
   : @cast_const a b (ZToInterp v)
     = ZToInterp match a with
                 | TZ => v
-                | TWord lgsz => if (0 <=? v)%Z
-                                then v mod 2^Z.of_nat (2^lgsz)
-                                else 0
+                | TWord lgsz => Z.max 0 v mod 2^Z.of_nat (2^lgsz)
                 end%Z.
 Proof.
   repeat first [ progress destruct_head base_type
@@ -139,9 +135,7 @@ Lemma interpToZ_ZToInterp_mod {a} v
   : @interpToZ a (ZToInterp v)
     = match a with
       | TZ => v
-      | TWord lgsz => if (0 <=? v)%Z
-                      then v mod 2^Z.of_nat (2^lgsz)
-                      else 0
+      | TWord lgsz => Z.max 0 v mod 2^Z.of_nat (2^lgsz)
       end%Z.
 Proof.
   etransitivity; [ apply (@interpToZ_cast_const_mod TZ) | ].
diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v
index afd590fd4..430684070 100644
--- a/src/Util/FixedWordSizesEquality.v
+++ b/src/Util/FixedWordSizesEquality.v
@@ -147,13 +147,11 @@ Proof.
   { apply wordToZ_gen_ZToWord_gen_0. }
 Qed.
 
-Lemma wordToZ_gen_ZToWord_gen_mod_full : forall {sz} w, wordToZ_gen (@ZToWord_gen sz w) = if (0 <=? w)%Z
-                                                                                          then (w mod (2^Z.of_nat sz))%Z
-                                                                                          else 0%Z.
+Lemma wordToZ_gen_ZToWord_gen_mod_full : forall {sz} w, wordToZ_gen (@ZToWord_gen sz w) = (Z.max 0 w mod (2^Z.of_nat sz))%Z.
 Proof.
-  intros; break_match; Z.ltb_to_lt.
-  { apply wordToZ_gen_ZToWord_gen_mod; assumption. }
+  intros; apply Z.max_case_strong; intro.
   { apply wordToZ_gen_ZToWord_gen_neg; omega. }
+  { apply wordToZ_gen_ZToWord_gen_mod; assumption. }
 Qed.
 
 Lemma ZToWord_gen_wordToZ_gen_ZToWord_gen : forall {sz1 sz2} v,
@@ -253,13 +251,10 @@ Proof.
   intros sz w; break_match; apply wordToZ_gen_ZToWord_gen_neg.
 Qed.
 
-Lemma wordToZ_ZToWord_mod_full : forall {sz} w, wordToZ (@ZToWord sz w) = if (0 <=? w)%Z
-                                                                          then (w mod (2^Z.of_nat (2^sz)))%Z
-                                                                          else 0%Z.
+Lemma wordToZ_ZToWord_mod_full : forall {sz} w, wordToZ (@ZToWord sz w) = ((Z.max 0 w) mod (2^Z.of_nat (2^sz)))%Z.
 Proof.
   unfold wordToZ, ZToWord, word_case_dep.
-  intros sz w; set (k := if (_ <=? _)%Z then _ else _);
-    break_match; apply wordToZ_gen_ZToWord_gen_mod_full.
+  intros sz w; break_match; apply wordToZ_gen_ZToWord_gen_mod_full.
 Qed.
 
 Local Ltac wordToZ_word_case_dep_t :=