From 0219dc26914219765300bf2eae792bed49b73562 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 9 Jul 2018 12:57:39 -0400 Subject: Add Z.div_mod_to_quot_rem tactic, put it in zify The various (micr)omega tactics now support `Z.div` and `Z.modulo`. I briefly looked into supporting `Nat.div` and `Nat.modulo`, but the conversions between `Z.div` and `Nat.div` are defined in `ZArith.Zdiv`, which depends on `Omega`, which depends on `PreOmega`, which is where `zify` is defined. --- plugins/omega/PreOmega.v | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 94a3d40441..387f258bdd 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -12,6 +12,38 @@ 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] *) + +(** This tactic uses the complete specification of [Z.div] and + [Z.modulo] to remove these functions from the goal without losing + information. *) + +Module Z. + Lemma div_mod_cases x y + : ((x = y * (x/y) + x mod y /\ (0 <= x mod y < y \/ y < x mod y <= 0)) + \/ (y = 0 /\ x / y = 0 /\ x mod y = 0)). + Proof. + destruct (Z.eq_dec y 0); subst; + [ right | left; auto using Z.div_mod, Z.mod_bound_or ]. + destruct x; cbv; repeat esplit. + Qed. + + Ltac div_mod_to_quot_rem_generalize x y := + pose proof (div_mod_cases x y); + let q := fresh "q" in + let r := fresh "r" in + set (q := x / y) in *; + set (r := x mod y) in *; + clearbody q r. + Ltac div_mod_to_quot_rem_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 + end. + Ltac div_mod_to_quot_rem := repeat div_mod_to_quot_rem_step. +End Z. (** * zify: the Z-ification tactic *) @@ -423,4 +455,4 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. (** The complete Z-ification tactic *) -Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op. +Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem. -- cgit v1.2.3 From 7bc08910ad7451d5e45102653d33e89aed5ae12b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 16 Jul 2018 20:08:02 -0400 Subject: Don't pose any disjunctions in div_mod_to_quot_rem Disjunctions seem to have a negative performance impact, so let's try implications instead. --- plugins/omega/PreOmega.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'plugins') diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 387f258bdd..1e0922e1ca 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -19,17 +19,17 @@ Local Open Scope Z_scope. information. *) Module Z. - Lemma div_mod_cases x y - : ((x = y * (x/y) + x mod y /\ (0 <= x mod y < y \/ y < x mod y <= 0)) - \/ (y = 0 /\ x / y = 0 /\ x mod y = 0)). - Proof. - destruct (Z.eq_dec y 0); subst; - [ right | left; auto using Z.div_mod, Z.mod_bound_or ]. - destruct x; cbv; repeat esplit. - Qed. + Lemma mod_0_r_ext x y : y = 0 -> x mod y = 0. + Proof. intro; subst; destruct x; reflexivity. Qed. + 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 := - pose proof (div_mod_cases 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); + pose proof (div_0_r_ext x y); + pose proof (mod_0_r_ext x y); let q := fresh "q" in let r := fresh "r" in set (q := x / y) in *; -- cgit v1.2.3 From 0c99020482e96ceb05799c47ffbcaef0e89b4b1f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 3 Dec 2018 16:45:49 -0500 Subject: Don't bundle Z.div_mod_quot_rem into zify Alas, I have not had time to work on imrpoving the performance of nia, and there has been a request to include this tactic (which is useful on its own) without bundling it into `zify`. So that is what we do here. I leave the definition of it in `PreOmega` in case we want to eventually include it in `zify`/`nia`. --- plugins/omega/PreOmega.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 1e0922e1ca..08bfec84bc 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -455,4 +455,4 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. (** The complete Z-ification tactic *) -Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem. +Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op. -- cgit v1.2.3 From a10076e834720c05e55397c9e26b9d7a8786298b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 3 Dec 2018 18:10:03 -0500 Subject: Move cleanup from the test-suite to Z.div_mod_to_quot_rem_cleanup Also fold it into `Z.div_mod_to_quot_rem` Note that the test-suite file is a bit slow. On my machine, it is ``` real 2m32.983s user 2m32.544s sys 0m0.492s ``` --- plugins/omega/PreOmega.v | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) (limited to 'plugins') diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 08bfec84bc..7ebc2fb04f 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -16,7 +16,8 @@ Local Open Scope Z_scope. (** This tactic uses the complete specification of [Z.div] and [Z.modulo] to remove these functions from the goal without losing - information. *) + information. The [Z.div_mod_to_quot_rem_cleanup] tactic removes + needless hypotheses, which makes tactics like [nia] run faster. *) Module Z. Lemma mod_0_r_ext x y : y = 0 -> x mod y = 0. @@ -42,7 +43,16 @@ Module Z. | [ 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 end. - Ltac div_mod_to_quot_rem := repeat div_mod_to_quot_rem_step. + Ltac div_mod_to_quot_rem' := repeat div_mod_to_quot_rem_step. + Ltac div_mod_to_quot_rem_cleanup := + repeat match goal with + | [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H') + | [ H : ?T -> _, H' : ~?T |- _ ] => clear H + | [ H : ~?T -> _, H' : ?T |- _ ] => clear H + | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H + | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H + end. + Ltac div_mod_to_quot_rem := div_mod_to_quot_rem'; div_mod_to_quot_rem_cleanup. End Z. (** * zify: the Z-ification tactic *) -- cgit v1.2.3 From d69ec6e2e0931a87d2ec3b3f47d1969b365d91f7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 5 Dec 2018 16:05:13 -0500 Subject: Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, Z.to_euclidean_division_equations --- plugins/omega/PreOmega.v | 118 +++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 104 insertions(+), 14 deletions(-) (limited to 'plugins') 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 -- cgit v1.2.3