Make Z.ltb_to_lt a bit stronger

Now it works not just at top-level, but also in, e.g., arguments to
hypotheses.

We had to change some proofs because it no longer moves the hypotheses
it changes to the bottom.

3 files changed, 85 insertions, 45 deletions

diff --git a/src/Reflection/Z/Interpretations128/Relations.v b/src/Reflection/Z/Interpretations128/Relations.v
index 8faa76eab..b7d86bfb9 100644
--- a/src/Reflection/Z/Interpretations128/Relations.v
+++ b/src/Reflection/Z/Interpretations128/Relations.v
@@ -427,24 +427,34 @@ Proof.
   { exact (fun _ _ x => x). }
 Qed.
 
+(* we [match] and [eexact] rather than [eassumption] so that we can backtrack across hypothesis choice, so that we're hypothesis-order-independent *)
 Local Ltac WordW.Rewrites.wordW_util_arith ::=
       solve [ autorewrite with Zshift_to_pow; omega
             | autorewrite with Zshift_to_pow; nia
             | autorewrite with Zshift_to_pow; auto with zarith
-            | eapply Z.le_lt_trans; [ eapply Z.log2_le_mono | eassumption ];
-              autorewrite with Zshift_to_pow; auto using Z.mul_le_mono_nonneg with zarith;
-              solve [ omega
-                    | nia
-                    | etransitivity; [ eapply Z.div_le_mono | eapply Z.div_le_compat_l ];
-                      auto with zarith ]
+            | match goal with
+              | [ H : _ |- _ ]
+                => eapply Z.le_lt_trans; [ eapply Z.log2_le_mono | eexact H ];
+                   autorewrite with Zshift_to_pow; auto using Z.mul_le_mono_nonneg with zarith;
+                   solve [ omega
+                         | nia
+                         | etransitivity; [ eapply Z.div_le_mono | eapply Z.div_le_compat_l ];
+                           auto with zarith ]
+              end
             | apply Z.land_nonneg; WordW.Rewrites.wordW_util_arith
-            | eapply Z.le_lt_trans; [ eapply Z.log2_le_mono | eassumption ];
-              instantiate; apply Z.min_case_strong; intros;
-              first [ etransitivity; [ apply Z.land_upper_bound_l | ]; omega
-                    | etransitivity; [ apply Z.land_upper_bound_r | ]; omega ]
+            | match goal with
+              | [ H : _ |- _ ]
+                => eapply Z.le_lt_trans; [ eapply Z.log2_le_mono | eexact H ];
+                   instantiate; apply Z.min_case_strong; intros;
+                   first [ etransitivity; [ apply Z.land_upper_bound_l | ]; omega
+                         | etransitivity; [ apply Z.land_upper_bound_r | ]; omega ]
+              end
             | rewrite Z.log2_lor by omega;
               apply Z.max_case_strong; intro;
-              (eapply Z.le_lt_trans; [ eapply Z.log2_le_mono; eassumption | assumption ])
+              match goal with
+              | [ H : _ |- _ ]
+                => eapply Z.le_lt_trans; [ eapply Z.log2_le_mono; eexact H | assumption ]
+              end
             | eapply Z.le_lt_trans; [ eapply Z.log2_le_mono, neg_upperbound | ];
               WordW.Rewrites.wordW_util_arith
             | (progress unfold ModularBaseSystemListZOperations.cmovne, ModularBaseSystemListZOperations.cmovl, ModularBaseSystemListZOperations.neg); break_match;
diff --git a/src/Reflection/Z/Interpretations64/Relations.v b/src/Reflection/Z/Interpretations64/Relations.v
index e4f0c482a..0a00ec10e 100644
--- a/src/Reflection/Z/Interpretations64/Relations.v
+++ b/src/Reflection/Z/Interpretations64/Relations.v
@@ -427,24 +427,34 @@ Proof.
   { exact (fun _ _ x => x). }
 Qed.
 
+(* we [match] and [eexact] rather than [eassumption] so that we can backtrack across hypothesis choice, so that we're hypothesis-order-independent *)
 Local Ltac WordW.Rewrites.wordW_util_arith ::=
       solve [ autorewrite with Zshift_to_pow; omega
             | autorewrite with Zshift_to_pow; nia
             | autorewrite with Zshift_to_pow; auto with zarith
-            | eapply Z.le_lt_trans; [ eapply Z.log2_le_mono | eassumption ];
-              autorewrite with Zshift_to_pow; auto using Z.mul_le_mono_nonneg with zarith;
-              solve [ omega
-                    | nia
-                    | etransitivity; [ eapply Z.div_le_mono | eapply Z.div_le_compat_l ];
-                      auto with zarith ]
+            | match goal with
+              | [ H : _ |- _ ]
+                => eapply Z.le_lt_trans; [ eapply Z.log2_le_mono | eexact H ];
+                   autorewrite with Zshift_to_pow; auto using Z.mul_le_mono_nonneg with zarith;
+                   solve [ omega
+                         | nia
+                         | etransitivity; [ eapply Z.div_le_mono | eapply Z.div_le_compat_l ];
+                           auto with zarith ]
+              end
             | apply Z.land_nonneg; WordW.Rewrites.wordW_util_arith
-            | eapply Z.le_lt_trans; [ eapply Z.log2_le_mono | eassumption ];
-              instantiate; apply Z.min_case_strong; intros;
-              first [ etransitivity; [ apply Z.land_upper_bound_l | ]; omega
-                    | etransitivity; [ apply Z.land_upper_bound_r | ]; omega ]
+            | match goal with
+              | [ H : _ |- _ ]
+                => eapply Z.le_lt_trans; [ eapply Z.log2_le_mono | eexact H ];
+                   instantiate; apply Z.min_case_strong; intros;
+                   first [ etransitivity; [ apply Z.land_upper_bound_l | ]; omega
+                         | etransitivity; [ apply Z.land_upper_bound_r | ]; omega ]
+              end
             | rewrite Z.log2_lor by omega;
               apply Z.max_case_strong; intro;
-              (eapply Z.le_lt_trans; [ eapply Z.log2_le_mono; eassumption | assumption ])
+              match goal with
+              | [ H : _ |- _ ]
+                => eapply Z.le_lt_trans; [ eapply Z.log2_le_mono; eexact H | assumption ]
+              end
             | eapply Z.le_lt_trans; [ eapply Z.log2_le_mono, neg_upperbound | ];
               WordW.Rewrites.wordW_util_arith
             | (progress unfold ModularBaseSystemListZOperations.cmovne, ModularBaseSystemListZOperations.cmovl, ModularBaseSystemListZOperations.neg); break_match;
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 04638a0c8..c63a9028d 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1170,29 +1170,50 @@ Module Z.
     refine (proj1 (@reflect_iff_gen _ _ lem b') _);
     cbv beta iota.
 
+  Ltac ltb_to_lt'_hyps_step :=
+    match goal with
+    | [ H : (?x <? ?y) = ?b |- _ ]
+      => ltb_to_lt_with_hyp H (Zlt_cases x y)
+    | [ H : (?x <=? ?y) = ?b |- _ ]
+      => ltb_to_lt_with_hyp H (Zle_cases x y)
+    | [ H : (?x >? ?y) = ?b |- _ ]
+      => ltb_to_lt_with_hyp H (Zgt_cases x y)
+    | [ H : (?x >=? ?y) = ?b |- _ ]
+      => ltb_to_lt_with_hyp H (Zge_cases x y)
+    | [ H : (?x =? ?y) = ?b |- _ ]
+      => ltb_to_lt_with_hyp H (eqb_cases x y)
+    end.
+  Ltac ltb_to_lt'_goal_step :=
+    match goal with
+    | [ |- (?x <? ?y) = ?b ]
+      => ltb_to_lt_in_goal b (Z.ltb_spec0 x y)
+    | [ |- (?x <=? ?y) = ?b ]
+      => ltb_to_lt_in_goal b (Z.leb_spec0 x y)
+    | [ |- (?x >? ?y) = ?b ]
+      => ltb_to_lt_in_goal b (Z.gtb_spec0 x y)
+    | [ |- (?x >=? ?y) = ?b ]
+      => ltb_to_lt_in_goal b (Z.geb_spec0 x y)
+    | [ |- (?x =? ?y) = ?b ]
+      => ltb_to_lt_in_goal b (Z.eqb_spec x y)
+    end.
+  Ltac ltb_to_lt'_step :=
+    first [ ltb_to_lt'_hyps_step
+          | ltb_to_lt'_goal_step ].
+  Ltac ltb_to_lt' := repeat ltb_to_lt'_step.
+
+  Section R_Rb.
+    Local Ltac t := intros ? ? []; split; intro; ltb_to_lt'; omega.
+    Local Notation R_Rb Rb R nR := (forall x y b, Rb x y = b <-> if b then R x y else nR x y).
+    Lemma ltb_lt_iff : R_Rb Z.ltb Z.lt Z.ge. Proof. t. Qed.
+    Lemma leb_le_iff : R_Rb Z.leb Z.le Z.gt. Proof. t. Qed.
+    Lemma gtb_gt_iff : R_Rb Z.gtb Z.gt Z.le. Proof. t. Qed.
+    Lemma geb_ge_iff : R_Rb Z.geb Z.ge Z.lt. Proof. t. Qed.
+    Lemma eqb_eq_iff : R_Rb Z.eqb (@Logic.eq Z) (fun x y => x <> y). Proof. t. Qed.
+  End R_Rb.
+  Hint Rewrite ltb_lt_iff leb_le_iff gtb_gt_iff geb_ge_iff eqb_eq_iff : ltb_to_lt.
   Ltac ltb_to_lt :=
-    repeat match goal with
-           | [ H : (?x <? ?y) = ?b |- _ ]
-             => ltb_to_lt_with_hyp H (Zlt_cases x y)
-           | [ H : (?x <=? ?y) = ?b |- _ ]
-             => ltb_to_lt_with_hyp H (Zle_cases x y)
-           | [ H : (?x >? ?y) = ?b |- _ ]
-             => ltb_to_lt_with_hyp H (Zgt_cases x y)
-           | [ H : (?x >=? ?y) = ?b |- _ ]
-             => ltb_to_lt_with_hyp H (Zge_cases x y)
-           | [ H : (?x =? ?y) = ?b |- _ ]
-             => ltb_to_lt_with_hyp H (eqb_cases x y)
-           | [ |- (?x <? ?y) = ?b ]
-             => ltb_to_lt_in_goal b (Z.ltb_spec0 x y)
-           | [ |- (?x <=? ?y) = ?b ]
-             => ltb_to_lt_in_goal b (Z.leb_spec0 x y)
-           | [ |- (?x >? ?y) = ?b ]
-             => ltb_to_lt_in_goal b (Z.gtb_spec0 x y)
-           | [ |- (?x >=? ?y) = ?b ]
-             => ltb_to_lt_in_goal b (Z.geb_spec0 x y)
-           | [ |- (?x =? ?y) = ?b ]
-             => ltb_to_lt_in_goal b (Z.eqb_spec x y)
-           end.
+    repeat autorewrite with ltb_to_lt in *;
+    cbv beta iota in *.
 
   Ltac compare_to_sgn :=
     repeat match goal with
@@ -3330,4 +3351,3 @@ Ltac Zmod_to_equiv_modulo :=
          | [ |- context T[?x mod ?M = ?y mod ?M] ]
            => let T' := context T[Z.equiv_modulo M x y] in change T'
          end.
-