aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/omega/PreOmega.v118
1 files changed, 104 insertions, 14 deletions
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 7ebc2fb04f..695f000cb1 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -12,12 +12,15 @@ Require Import Arith Max Min BinInt BinNat Znat Nnat.
Local Open Scope Z_scope.
-(** * [Z.div_mod_to_quot_rem]: the tactic for preprocessing [Z.div] and [Z.modulo] *)
+(** * [Z.div_mod_to_equations], [Z.quot_rem_to_equations], [Z.to_euclidean_division_equations]: the tactics for preprocessing [Z.div] and [Z.modulo], [Z.quot] and [Z.rem] *)
-(** This tactic uses the complete specification of [Z.div] and
- [Z.modulo] to remove these functions from the goal without losing
- information. The [Z.div_mod_to_quot_rem_cleanup] tactic removes
- needless hypotheses, which makes tactics like [nia] run faster. *)
+(** These tactic use the complete specification of [Z.div] and
+ [Z.modulo] ([Z.quot] and [Z.rem], respectively) to remove these
+ functions from the goal without losing information. The
+ [Z.euclidean_division_equations_cleanup] tactic removes needless
+ hypotheses, which makes tactics like [nia] run faster. The tactic
+ [Z.to_euclidean_division_equations] combines the handling of both variants
+ of division/quotient and modulo/remainder. *)
Module Z.
Lemma mod_0_r_ext x y : y = 0 -> x mod y = 0.
@@ -25,7 +28,21 @@ Module Z.
Lemma div_0_r_ext x y : y = 0 -> x / y = 0.
Proof. intro; subst; destruct x; reflexivity. Qed.
- Ltac div_mod_to_quot_rem_generalize x y :=
+ Lemma rem_0_r_ext x y : y = 0 -> Z.rem x y = x.
+ Proof. intro; subst; destruct x; reflexivity. Qed.
+ Lemma quot_0_r_ext x y : y = 0 -> Z.quot x y = 0.
+ Proof. intro; subst; destruct x; reflexivity. Qed.
+
+ Lemma rem_bound_pos_pos x y : 0 < y -> 0 <= x -> 0 <= Z.rem x y < y.
+ Proof. intros; apply Z.rem_bound_pos; assumption. Qed.
+ Lemma rem_bound_neg_pos x y : y < 0 -> 0 <= x -> 0 <= Z.rem x y < -y.
+ Proof. rewrite <- Z.rem_opp_r'; intros; apply Z.rem_bound_pos; rewrite ?Z.opp_pos_neg; assumption. Qed.
+ Lemma rem_bound_pos_neg x y : 0 < y -> x <= 0 -> -y < Z.rem x y <= 0.
+ Proof. rewrite <- (Z.opp_involutive x), Z.rem_opp_l', <- Z.opp_lt_mono, and_comm, !Z.opp_nonpos_nonneg; apply rem_bound_pos_pos. Qed.
+ Lemma rem_bound_neg_neg x y : y < 0 -> x <= 0 -> y < Z.rem x y <= 0.
+ Proof. rewrite <- (Z.opp_involutive x), <- (Z.opp_involutive y), Z.rem_opp_l', <- Z.opp_lt_mono, and_comm, !Z.opp_nonpos_nonneg, Z.opp_involutive; apply rem_bound_neg_pos. Qed.
+
+ Ltac div_mod_to_equations_generalize x y :=
pose proof (Z.div_mod x y);
pose proof (Z.mod_pos_bound x y);
pose proof (Z.mod_neg_bound x y);
@@ -36,23 +53,78 @@ Module Z.
set (q := x / y) in *;
set (r := x mod y) in *;
clearbody q r.
- Ltac div_mod_to_quot_rem_step :=
+ Ltac quot_rem_to_equations_generalize x y :=
+ pose proof (Z.quot_rem' x y);
+ pose proof (rem_bound_pos_pos x y);
+ pose proof (rem_bound_pos_neg x y);
+ pose proof (rem_bound_neg_pos x y);
+ pose proof (rem_bound_neg_neg x y);
+ pose proof (quot_0_r_ext x y);
+ pose proof (rem_0_r_ext x y);
+ let q := fresh "q" in
+ let r := fresh "r" in
+ set (q := Z.quot x y) in *;
+ set (r := Z.rem x y) in *;
+ clearbody q r.
+
+ Ltac div_mod_to_equations_step :=
match goal with
- | [ |- context[?x / ?y] ] => div_mod_to_quot_rem_generalize x y
- | [ |- context[?x mod ?y] ] => div_mod_to_quot_rem_generalize x y
- | [ H : context[?x / ?y] |- _ ] => div_mod_to_quot_rem_generalize x y
- | [ H : context[?x mod ?y] |- _ ] => div_mod_to_quot_rem_generalize x y
+ | [ |- context[?x / ?y] ] => div_mod_to_equations_generalize x y
+ | [ |- context[?x mod ?y] ] => div_mod_to_equations_generalize x y
+ | [ H : context[?x / ?y] |- _ ] => div_mod_to_equations_generalize x y
+ | [ H : context[?x mod ?y] |- _ ] => div_mod_to_equations_generalize x y
end.
- Ltac div_mod_to_quot_rem' := repeat div_mod_to_quot_rem_step.
- Ltac div_mod_to_quot_rem_cleanup :=
+ Ltac quot_rem_to_equations_step :=
+ match goal with
+ | [ |- context[Z.quot ?x ?y] ] => quot_rem_to_equations_generalize x y
+ | [ |- context[Z.rem ?x ?y] ] => quot_rem_to_equations_generalize x y
+ | [ H : context[Z.quot ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y
+ | [ H : context[Z.rem ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y
+ end.
+ Ltac div_mod_to_equations' := repeat div_mod_to_equations_step.
+ Ltac quot_rem_to_equations' := repeat quot_rem_to_equations_step.
+ Ltac euclidean_division_equations_cleanup :=
repeat match goal with
+ | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl)
+ | [ H : ?x <> ?x -> _ |- _ ] => clear H
+ | [ H : ?x < ?x -> _ |- _ ] => clear H
| [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H')
| [ H : ?T -> _, H' : ~?T |- _ ] => clear H
| [ H : ~?T -> _, H' : ?T |- _ ] => clear H
+ | [ H : ?A -> ?x = ?x -> _ |- _ ] => specialize (fun a => H a eq_refl)
+ | [ H : ?A -> ?x <> ?x -> _ |- _ ] => clear H
+ | [ H : ?A -> ?x < ?x -> _ |- _ ] => clear H
+ | [ H : ?A -> ?B -> _, 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 -> _, H' : ?x <= 0 |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x (eq_sym pf)))
+ | [ H : ?A -> 0 <= ?x -> _, H' : ?x <= 0 |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl 0 x (eq_sym pf)))
+ | [ H : ?x <= 0 -> _, H' : 0 <= ?x |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x pf))
+ | [ H : ?A -> ?x <= 0 -> _, 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
end.
- Ltac div_mod_to_quot_rem := div_mod_to_quot_rem'; div_mod_to_quot_rem_cleanup.
+ Ltac div_mod_to_equations := div_mod_to_equations'; euclidean_division_equations_cleanup.
+ Ltac quot_rem_to_equations := quot_rem_to_equations'; euclidean_division_equations_cleanup.
+ Ltac to_euclidean_division_equations := div_mod_to_equations'; quot_rem_to_equations'; euclidean_division_equations_cleanup.
End Z.
(** * zify: the Z-ification tactic *)
@@ -453,6 +525,24 @@ Ltac zify_N_op :=
| |- context [ Z.of_N (N.mul ?a ?b) ] =>
pose proof (N2Z.is_nonneg (N.mul a b)); rewrite (N2Z.inj_mul a b) in *
+ (* N.div -> Z.div and a positivity hypothesis *)
+ | H : context [ Z.of_N (N.div ?a ?b) ] |- _ =>
+ pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in *
+ | |- context [ Z.of_N (N.div ?a ?b) ] =>
+ pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in *
+
+ (* N.modulo -> Z.rem / Z.modulo and a positivity hypothesis (N.modulo agrees with Z.modulo on everything except 0; so we pose both the non-zero proof for this agreement, but also replace things with [Z.rem]) *)
+ | H : context [ Z.of_N (N.modulo ?a ?b) ] |- _ =>
+ pose proof (N2Z.is_nonneg (N.modulo a b));
+ pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
+ pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
+ rewrite (N2Z.inj_rem a b) in *
+ | |- context [ Z.of_N (N.div ?a ?b) ] =>
+ pose proof (N2Z.is_nonneg (N.modulo a b));
+ pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
+ pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
+ rewrite (N2Z.inj_rem a b) in *
+
(* atoms of type N : we add a positivity condition (if not already there) *)
| _ : 0 <= Z.of_N ?a |- _ => hide_Z_of_N a
| _ : context [ Z.of_N ?a ] |- _ => pose proof (N2Z.is_nonneg a); hide_Z_of_N a
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:48:06 +0000