Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Reorder Z.euclidean_division_equations_cleanup #18818

Merged
merged 1 commit into from
Mar 21, 2024
Merged

Reorder Z.euclidean_division_equations_cleanup #18818

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
7 changes: 7 additions & 0 deletions doc/changelog/11-standard-library/18818-faster-zify.rst
View file
Open in desktop
@@ -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).
83 changes: 44 additions & 39 deletions theories/omega/PreOmega.v
View file
Open in desktop
Expand Up @@ -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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this repeat here because specialize in the old version actually trigger more clear later, whereas in the new version there is no such opportunity without this repeat?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not just more clear but also more destruct, yes. I'm not 100% sure that it gets used in practice, but I expect it to be relatively cheap to run the final iteration, and I think it's better to not have to manually track whether or not specialize can reveal more opportunities for clear and destruct

(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;
Expand Down