Reorder Z.euclidean_division_equations_cleanup

Fixes #18770

We first destruct, then clear, then specialize.  The reasoning is:
- `destruct` before `clear` because the `clear` is not going to make much of
  a difference to `destruct`, but the `destruct` might expose more
  opportunities for `clear`ing
- `clear` between `destruct` and `specialize` so that we don't waste a
  bunch of time modifying the goal (via `specialize`) on hypotheses that
  we would anyway want to `clear`

doc/changelog/11-standard-library/18818-faster-zify.rst

@@ -0,0 +1,7 @@
+- **Fixed:**
+  :g:`Z.euclidean_division_equations_cleanup` has been reordered so that
+  :tacn:`zify` (and :tacn:`lia`, :tacn:`nia`, etc) are no longer as slow when the
+  context contains many assumptions of the form :g:`0 <= ... < ...`
+  (`#18818 <https://github.com/coq/coq/pull/18818>`_,
+  fixes `#18770 <https://github.com/coq/coq/issues/18770>`_,
+  by Jason Gross).

theories/omega/PreOmega.v

@@ -97,45 +97,50 @@ Module Z.
   Ltac quot_rem_to_equations' := repeat quot_rem_to_equations_step.
   Ltac divide_to_equations' := repeat divide_to_equations_step.
   Ltac euclidean_division_equations_cleanup :=
-    repeat match goal with
-           | [ H : ?x = ?x -> ?Q |- _ ] => specialize (H eq_refl)
-           | [ H : ?x <> ?x -> _ |- _ ] => clear H
-           | [ H : ?x < ?x -> _ |- _ ] => clear H
-           | [ H : ?T -> ?Q, H' : ?T |- _ ] => specialize (H H')
-           | [ H : ?T -> _, H' : ~?T |- _ ] => clear H
-           | [ H : ~?T -> _, H' : ?T |- _ ] => clear H
-           | [ H : ?A -> ?x = ?x -> ?Q |- _ ] => specialize (fun a => H a eq_refl)
-           | [ H : ?A -> ?x <> ?x -> _ |- _ ] => clear H
-           | [ H : ?A -> ?x < ?x -> _ |- _ ] => clear H
-           | [ H : ?A -> ?B -> ?Q, H' : ?B |- _ ] => specialize (fun a => H a H')
-           | [ H : ?A -> ?B -> _, H' : ~?B |- _ ] => clear H
-           | [ H : ?A -> ~?B -> _, H' : ?B |- _ ] => clear H
-           | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
-           | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
-           | [ H : ?A -> 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
-           | [ H : ?A -> ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
-           | [ H : 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H
-           | [ H : ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H
-           | [ H : ?A -> 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H
-           | [ H : ?A -> ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H
-           | [ H : 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H
-           | [ H : ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H
-           | [ H : ?A -> 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H
-           | [ H : ?A -> ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H
-           | [ H : 0 <= ?x -> ?Q, H' : ?x <= 0 |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x (eq_sym pf)))
-           | [ H : ?A -> 0 <= ?x -> ?Q, H' : ?x <= 0 |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl 0 x (eq_sym pf)))
-           | [ H : ?x <= 0 -> ?Q, H' : 0 <= ?x |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x pf))
-           | [ H : ?A -> ?x <= 0 -> ?Q, H' : 0 <= ?x |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl x 0 pf))
-           | [ H : ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H
-           | [ H : ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H
-           | [ H : ?A -> ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H
-           | [ H : ?A -> ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H
-           | [ H : ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H
-           | [ H : ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H
-           | [ H : ?A -> ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H
-           | [ H : ?A -> ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H
-           | [ H : 0 <= ?x < _ |- _ ] => destruct H
-           end.
+    repeat
+      (repeat match goal with
+         | [ H : 0 <= ?x < _ |- _ ] => destruct H
+         end;
+       repeat match goal with
+         | [ H : ?x <> ?x -> _ |- _ ] => clear H
+         | [ H : ?x < ?x -> _ |- _ ] => clear H
+         | [ H : ?T -> _, H' : ~?T |- _ ] => clear H
+         | [ H : ~?T -> _, H' : ?T |- _ ] => clear H
+         | [ H : ?A -> ?x <> ?x -> _ |- _ ] => clear H
+         | [ H : ?A -> ?x < ?x -> _ |- _ ] => clear H
+         | [ H : ?A -> ?B -> _, H' : ~?B |- _ ] => clear H
+         | [ H : ?A -> ~?B -> _, H' : ?B |- _ ] => clear H
+         | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
+         | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
+         | [ H : ?A -> 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
+         | [ H : ?A -> ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
+         | [ H : 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H
+         | [ H : ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H
+         | [ H : ?A -> 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H
+         | [ H : ?A -> ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H
+         | [ H : 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H
+         | [ H : ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H
+         | [ H : ?A -> 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H
+         | [ H : ?A -> ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H
+         | [ H : ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H
+         | [ H : ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H
+         | [ H : ?A -> ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H
+         | [ H : ?A -> ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H
+         | [ H : ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H
+         | [ H : ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H
+         | [ H : ?A -> ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H
+         | [ H : ?A -> ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H
+         end;
+       repeat match goal with
+         | [ H : ?x = ?x -> ?Q |- _ ] => specialize (H eq_refl)
+         | [ H : ?T -> ?Q, H' : ?T |- _ ] => specialize (H H')
+         | [ H : ?A -> ?x = ?x -> ?Q |- _ ] => specialize (fun a => H a eq_refl)
+         | [ H : ?A -> ?B -> ?Q, H' : ?B |- _ ] => specialize (fun a => H a H')
+         | [ H : 0 <= ?x -> ?Q, H' : ?x <= 0 |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x (eq_sym pf)))
+         | [ H : ?A -> 0 <= ?x -> ?Q, H' : ?x <= 0 |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl 0 x (eq_sym pf)))
+         | [ H : ?x <= 0 -> ?Q, H' : 0 <= ?x |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x pf))
+         | [ H : ?A -> ?x <= 0 -> ?Q, H' : 0 <= ?x |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl x 0 pf))
+         end).
   (** poses [x = y \/ x <> y] unless that is redundant or contradictory *)
   Ltac euclidean_division_equations_pose_eq_fact x y :=
     assert_fails constr_eq x y;