diff options
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/Omega.v | 55 | ||||
| -rw-r--r-- | plugins/omega/OmegaLemmas.v | 307 | ||||
| -rw-r--r-- | plugins/omega/OmegaPlugin.v | 17 | ||||
| -rw-r--r-- | plugins/omega/OmegaTactic.v | 17 | ||||
| -rw-r--r-- | plugins/omega/PreOmega.v | 558 | ||||
| -rw-r--r-- | plugins/omega/coq_omega.ml | 1914 | ||||
| -rw-r--r-- | plugins/omega/coq_omega.mli | 11 | ||||
| -rw-r--r-- | plugins/omega/g_omega.mlg | 59 | ||||
| -rw-r--r-- | plugins/omega/omega.ml | 708 | ||||
| -rw-r--r-- | plugins/omega/omega_plugin.mlpack | 3 | ||||
| -rw-r--r-- | plugins/omega/plugin_base.dune | 5 |
11 files changed, 3654 insertions, 0 deletions
diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v new file mode 100644 index 0000000000..6c8f23a012 --- /dev/null +++ b/plugins/omega/Omega.v @@ -0,0 +1,55 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(**************************************************************************) +(* *) +(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) +(* *) +(* Pierre Crégut (CNET, Lannion, France) *) +(* *) +(**************************************************************************) + +(* We import what is necessary for Omega *) +Require Export ZArith_base. +Require Export OmegaLemmas. +Require Export PreOmega. + +Declare ML Module "omega_plugin". + +Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l + Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_r + Z.mul_add_distr_l: zarith. + +Require Export Zhints. + +Hint Extern 10 (_ = _ :>nat) => abstract omega: zarith. +Hint Extern 10 (_ <= _) => abstract omega: zarith. +Hint Extern 10 (_ < _) => abstract omega: zarith. +Hint Extern 10 (_ >= _) => abstract omega: zarith. +Hint Extern 10 (_ > _) => abstract omega: zarith. + +Hint Extern 10 (_ <> _ :>nat) => abstract omega: zarith. +Hint Extern 10 (~ _ <= _) => abstract omega: zarith. +Hint Extern 10 (~ _ < _) => abstract omega: zarith. +Hint Extern 10 (~ _ >= _) => abstract omega: zarith. +Hint Extern 10 (~ _ > _) => abstract omega: zarith. + +Hint Extern 10 (_ = _ :>Z) => abstract omega: zarith. +Hint Extern 10 (_ <= _)%Z => abstract omega: zarith. +Hint Extern 10 (_ < _)%Z => abstract omega: zarith. +Hint Extern 10 (_ >= _)%Z => abstract omega: zarith. +Hint Extern 10 (_ > _)%Z => abstract omega: zarith. + +Hint Extern 10 (_ <> _ :>Z) => abstract omega: zarith. +Hint Extern 10 (~ (_ <= _)%Z) => abstract omega: zarith. +Hint Extern 10 (~ (_ < _)%Z) => abstract omega: zarith. +Hint Extern 10 (~ (_ >= _)%Z) => abstract omega: zarith. +Hint Extern 10 (~ (_ > _)%Z) => abstract omega: zarith. + +Hint Extern 10 False => abstract omega: zarith. diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v new file mode 100644 index 0000000000..81bf1fb83d --- /dev/null +++ b/plugins/omega/OmegaLemmas.v @@ -0,0 +1,307 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import BinInt Znat. +Local Open Scope Z_scope. + +(** Factorization lemmas *) + +Theorem Zred_factor0 n : n = n * 1. +Proof. + now Z.nzsimpl. +Qed. + +Theorem Zred_factor1 n : n + n = n * 2. +Proof. + rewrite Z.mul_comm. apply Z.add_diag. +Qed. + +Theorem Zred_factor2 n m : n + n * m = n * (1 + m). +Proof. + rewrite Z.mul_add_distr_l; now Z.nzsimpl. +Qed. + +Theorem Zred_factor3 n m : n * m + n = n * (1 + m). +Proof. + now Z.nzsimpl. +Qed. + +Theorem Zred_factor4 n m p : n * m + n * p = n * (m + p). +Proof. + symmetry; apply Z.mul_add_distr_l. +Qed. + +Theorem Zred_factor5 n m : n * 0 + m = m. +Proof. + now Z.nzsimpl. +Qed. + +Theorem Zred_factor6 n : n = n + 0. +Proof. + now Z.nzsimpl. +Qed. + +(** Other specific variants of theorems dedicated for the Omega tactic *) + +Lemma new_var : forall x : Z, exists y : Z, x = y. +Proof. +intros x; now exists x. +Qed. + +Lemma OMEGA1 x y : x = y -> 0 <= x -> 0 <= y. +Proof. +now intros ->. +Qed. + +Lemma OMEGA2 x y : 0 <= x -> 0 <= y -> 0 <= x + y. +Proof. +Z.order_pos. +Qed. + +Lemma OMEGA3 x y k : k > 0 -> x = y * k -> x = 0 -> y = 0. +Proof. +intros LT -> EQ. apply Z.mul_eq_0 in EQ. destruct EQ; now subst. +Qed. + +Lemma OMEGA4 x y z : x > 0 -> y > x -> z * y + x <> 0. +Proof. +Z.swap_greater. intros Hx Hxy. +rewrite Z.add_move_0_l, <- Z.mul_opp_l. +destruct (Z.lt_trichotomy (-z) 1) as [LT|[->|GT]]. +- intro. revert LT. apply Z.le_ngt, (Z.le_succ_l 0). + apply Z.mul_pos_cancel_r with y; Z.order. +- Z.nzsimpl. Z.order. +- rewrite (Z.mul_lt_mono_pos_r y), Z.mul_1_l in GT; Z.order. +Qed. + +Lemma OMEGA5 x y z : x = 0 -> y = 0 -> x + y * z = 0. +Proof. +now intros -> ->. +Qed. + +Lemma OMEGA6 x y z : 0 <= x -> y = 0 -> 0 <= x + y * z. +Proof. +intros H ->. now Z.nzsimpl. +Qed. + +Lemma OMEGA7 x y z t : + z > 0 -> t > 0 -> 0 <= x -> 0 <= y -> 0 <= x * z + y * t. +Proof. +intros. Z.swap_greater. Z.order_pos. +Qed. + +Lemma OMEGA8 x y : 0 <= x -> 0 <= y -> x = - y -> x = 0. +Proof. +intros H1 H2 H3. rewrite <- Z.opp_nonpos_nonneg in H2. Z.order. +Qed. + +Lemma OMEGA9 x y z t : y = 0 -> x = z -> y + (- x + z) * t = 0. +Proof. +intros. subst. now rewrite Z.add_opp_diag_l. +Qed. + +Lemma OMEGA10 v c1 c2 l1 l2 k1 k2 : + (v * c1 + l1) * k1 + (v * c2 + l2) * k2 = + v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2). +Proof. +rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc. +rewrite <- !Z.add_assoc. f_equal. apply Z.add_shuffle3. +Qed. + +Lemma OMEGA11 v1 c1 l1 l2 k1 : + (v1 * c1 + l1) * k1 + l2 = v1 * (c1 * k1) + (l1 * k1 + l2). +Proof. +rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc. +now rewrite Z.add_assoc. +Qed. + +Lemma OMEGA12 v2 c2 l1 l2 k2 : + l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2). +Proof. +rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc. +apply Z.add_shuffle3. +Qed. + +Lemma OMEGA13 (v l1 l2 : Z) (x : positive) : + v * Zpos x + l1 + (v * Zneg x + l2) = l1 + l2. +Proof. + rewrite Z.add_shuffle1. + rewrite <- Z.mul_add_distr_l, <- Pos2Z.opp_neg, Z.add_opp_diag_r. + now Z.nzsimpl. +Qed. + +Lemma OMEGA14 (v l1 l2 : Z) (x : positive) : + v * Zneg x + l1 + (v * Zpos x + l2) = l1 + l2. +Proof. + rewrite Z.add_shuffle1. + rewrite <- Z.mul_add_distr_l, <- Pos2Z.opp_neg, Z.add_opp_diag_r. + now Z.nzsimpl. +Qed. + +Lemma OMEGA15 v c1 c2 l1 l2 k2 : + v * c1 + l1 + (v * c2 + l2) * k2 = v * (c1 + c2 * k2) + (l1 + l2 * k2). +Proof. + rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc. + apply Z.add_shuffle1. +Qed. + +Lemma OMEGA16 v c l k : (v * c + l) * k = v * (c * k) + l * k. +Proof. + now rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc. +Qed. + +Lemma OMEGA17 x y z : Zne x 0 -> y = 0 -> Zne (x + y * z) 0. +Proof. + unfold Zne, not. intros NE EQ. subst. now Z.nzsimpl. +Qed. + +Lemma OMEGA18 x y k : x = y * k -> Zne x 0 -> Zne y 0. +Proof. + unfold Zne, not. intros. subst; auto. +Qed. + +Lemma OMEGA19 x : Zne x 0 -> 0 <= x + -1 \/ 0 <= x * -1 + -1. +Proof. + unfold Zne. intros Hx. apply Z.lt_gt_cases in Hx. + destruct Hx as [LT|GT]. + - right. change (-1) with (-(1)). + rewrite Z.mul_opp_r, <- Z.opp_add_distr. Z.nzsimpl. + rewrite Z.opp_nonneg_nonpos. now apply Z.le_succ_l. + - left. now apply Z.lt_le_pred. +Qed. + +Lemma OMEGA20 x y z : Zne x 0 -> y = 0 -> Zne (x + y * z) 0. +Proof. + unfold Zne, not. intros H1 H2 H3; apply H1; rewrite H2 in H3; + simpl in H3; rewrite Z.add_0_r in H3; trivial with arith. +Qed. + +Definition fast_Zplus_comm (x y : Z) (P : Z -> Prop) + (H : P (y + x)) := eq_ind_r P H (Z.add_comm x y). + +Definition fast_Zplus_assoc_reverse (n m p : Z) (P : Z -> Prop) + (H : P (n + (m + p))) := eq_ind_r P H (Zplus_assoc_reverse n m p). + +Definition fast_Zplus_assoc (n m p : Z) (P : Z -> Prop) + (H : P (n + m + p)) := eq_ind_r P H (Z.add_assoc n m p). + +Definition fast_Zplus_permute (n m p : Z) (P : Z -> Prop) + (H : P (m + (n + p))) := eq_ind_r P H (Z.add_shuffle3 n m p). + +Definition fast_OMEGA10 (v c1 c2 l1 l2 k1 k2 : Z) (P : Z -> Prop) + (H : P (v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2))) := + eq_ind_r P H (OMEGA10 v c1 c2 l1 l2 k1 k2). + +Definition fast_OMEGA11 (v1 c1 l1 l2 k1 : Z) (P : Z -> Prop) + (H : P (v1 * (c1 * k1) + (l1 * k1 + l2))) := + eq_ind_r P H (OMEGA11 v1 c1 l1 l2 k1). +Definition fast_OMEGA12 (v2 c2 l1 l2 k2 : Z) (P : Z -> Prop) + (H : P (v2 * (c2 * k2) + (l1 + l2 * k2))) := + eq_ind_r P H (OMEGA12 v2 c2 l1 l2 k2). + +Definition fast_OMEGA15 (v c1 c2 l1 l2 k2 : Z) (P : Z -> Prop) + (H : P (v * (c1 + c2 * k2) + (l1 + l2 * k2))) := + eq_ind_r P H (OMEGA15 v c1 c2 l1 l2 k2). +Definition fast_OMEGA16 (v c l k : Z) (P : Z -> Prop) + (H : P (v * (c * k) + l * k)) := eq_ind_r P H (OMEGA16 v c l k). + +Definition fast_OMEGA13 (v l1 l2 : Z) (x : positive) (P : Z -> Prop) + (H : P (l1 + l2)) := eq_ind_r P H (OMEGA13 v l1 l2 x). + +Definition fast_OMEGA14 (v l1 l2 : Z) (x : positive) (P : Z -> Prop) + (H : P (l1 + l2)) := eq_ind_r P H (OMEGA14 v l1 l2 x). +Definition fast_Zred_factor0 (x : Z) (P : Z -> Prop) + (H : P (x * 1)) := eq_ind_r P H (Zred_factor0 x). + +Definition fast_Zopp_eq_mult_neg_1 (x : Z) (P : Z -> Prop) + (H : P (x * -1)) := eq_ind_r P H (Z.opp_eq_mul_m1 x). + +Definition fast_Zmult_comm (x y : Z) (P : Z -> Prop) + (H : P (y * x)) := eq_ind_r P H (Z.mul_comm x y). + +Definition fast_Zopp_plus_distr (x y : Z) (P : Z -> Prop) + (H : P (- x + - y)) := eq_ind_r P H (Z.opp_add_distr x y). + +Definition fast_Zopp_mult_distr_r (x y : Z) (P : Z -> Prop) + (H : P (x * - y)) := eq_ind_r P H (Zopp_mult_distr_r x y). + +Definition fast_Zmult_plus_distr_l (n m p : Z) (P : Z -> Prop) + (H : P (n * p + m * p)) := eq_ind_r P H (Z.mul_add_distr_r n m p). +Definition fast_Zmult_assoc_reverse (n m p : Z) (P : Z -> Prop) + (H : P (n * (m * p))) := eq_ind_r P H (Zmult_assoc_reverse n m p). + +Definition fast_Zred_factor1 (x : Z) (P : Z -> Prop) + (H : P (x * 2)) := eq_ind_r P H (Zred_factor1 x). + +Definition fast_Zred_factor2 (x y : Z) (P : Z -> Prop) + (H : P (x * (1 + y))) := eq_ind_r P H (Zred_factor2 x y). + +Definition fast_Zred_factor3 (x y : Z) (P : Z -> Prop) + (H : P (x * (1 + y))) := eq_ind_r P H (Zred_factor3 x y). + +Definition fast_Zred_factor4 (x y z : Z) (P : Z -> Prop) + (H : P (x * (y + z))) := eq_ind_r P H (Zred_factor4 x y z). + +Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop) + (H : P y) := eq_ind_r P H (Zred_factor5 x y). + +Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop) + (H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x). + +Theorem intro_Z : + forall n:nat, exists y : Z, Z.of_nat n = y /\ 0 <= y * 1 + 0. +Proof. + intros n; exists (Z.of_nat n); split; trivial. + rewrite Z.mul_1_r, Z.add_0_r. apply Nat2Z.is_nonneg. +Qed. + +Register fast_Zplus_assoc_reverse as plugins.omega.fast_Zplus_assoc_reverse. +Register fast_Zplus_assoc as plugins.omega.fast_Zplus_assoc. +Register fast_Zmult_assoc_reverse as plugins.omega.fast_Zmult_assoc_reverse. +Register fast_Zplus_permute as plugins.omega.fast_Zplus_permute. +Register fast_Zplus_comm as plugins.omega.fast_Zplus_comm. +Register fast_Zmult_comm as plugins.omega.fast_Zmult_comm. + +Register OMEGA1 as plugins.omega.OMEGA1. +Register OMEGA2 as plugins.omega.OMEGA2. +Register OMEGA3 as plugins.omega.OMEGA3. +Register OMEGA4 as plugins.omega.OMEGA4. +Register OMEGA5 as plugins.omega.OMEGA5. +Register OMEGA6 as plugins.omega.OMEGA6. +Register OMEGA7 as plugins.omega.OMEGA7. +Register OMEGA8 as plugins.omega.OMEGA8. +Register OMEGA9 as plugins.omega.OMEGA9. +Register fast_OMEGA10 as plugins.omega.fast_OMEGA10. +Register fast_OMEGA11 as plugins.omega.fast_OMEGA11. +Register fast_OMEGA12 as plugins.omega.fast_OMEGA12. +Register fast_OMEGA13 as plugins.omega.fast_OMEGA13. +Register fast_OMEGA14 as plugins.omega.fast_OMEGA14. +Register fast_OMEGA15 as plugins.omega.fast_OMEGA15. +Register fast_OMEGA16 as plugins.omega.fast_OMEGA16. +Register OMEGA17 as plugins.omega.OMEGA17. +Register OMEGA18 as plugins.omega.OMEGA18. +Register OMEGA19 as plugins.omega.OMEGA19. +Register OMEGA20 as plugins.omega.OMEGA20. + +Register fast_Zred_factor0 as plugins.omega.fast_Zred_factor0. +Register fast_Zred_factor1 as plugins.omega.fast_Zred_factor1. +Register fast_Zred_factor2 as plugins.omega.fast_Zred_factor2. +Register fast_Zred_factor3 as plugins.omega.fast_Zred_factor3. +Register fast_Zred_factor4 as plugins.omega.fast_Zred_factor4. +Register fast_Zred_factor5 as plugins.omega.fast_Zred_factor5. +Register fast_Zred_factor6 as plugins.omega.fast_Zred_factor6. + +Register fast_Zmult_plus_distr_l as plugins.omega.fast_Zmult_plus_distr_l. +Register fast_Zopp_plus_distr as plugins.omega.fast_Zopp_plus_distr. +Register fast_Zopp_mult_distr_r as plugins.omega.fast_Zopp_mult_distr_r. +Register fast_Zopp_eq_mult_neg_1 as plugins.omega.fast_Zopp_eq_mult_neg_1. + +Register new_var as plugins.omega.new_var. +Register intro_Z as plugins.omega.intro_Z. diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v new file mode 100644 index 0000000000..3c339c8b8f --- /dev/null +++ b/plugins/omega/OmegaPlugin.v @@ -0,0 +1,17 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* To strictly import the omega tactic *) + +Require ZArith_base. +Require OmegaLemmas. +Require PreOmega. + +Declare ML Module "omega_plugin". diff --git a/plugins/omega/OmegaTactic.v b/plugins/omega/OmegaTactic.v new file mode 100644 index 0000000000..3c339c8b8f --- /dev/null +++ b/plugins/omega/OmegaTactic.v @@ -0,0 +1,17 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* To strictly import the omega tactic *) + +Require ZArith_base. +Require OmegaLemmas. +Require PreOmega. + +Declare ML Module "omega_plugin". diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v new file mode 100644 index 0000000000..695f000cb1 --- /dev/null +++ b/plugins/omega/PreOmega.v @@ -0,0 +1,558 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import Arith Max Min BinInt BinNat Znat Nnat. + +Local Open Scope Z_scope. + +(** * [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] *) + +(** 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. + 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. + + 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); + 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 *; + set (r := x mod y) in *; + clearbody q r. + 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_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 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_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 *) + +(* This tactic searches for nat and N and positive elements in the goal and + translates everything into Z. It is meant as a pre-processor for + (r)omega; for instance a positivity hypothesis is added whenever + - a multiplication is encountered + - an atom is encountered (that is a variable or an unknown construct) + + Recognized relations (can be handled as deeply as allowed by setoid rewrite): + - { eq, le, lt, ge, gt } on { Z, positive, N, nat } + + Recognized operations: + - on Z: Z.min, Z.max, Z.abs, Z.sgn are translated in term of <= < = + - on nat: + * - S O pred min max Pos.to_nat N.to_nat Z.abs_nat + - on positive: Zneg Zpos xI xO xH + * - Pos.succ Pos.pred Pos.min Pos.max Pos.of_succ_nat + - on N: N0 Npos + * - N.pred N.succ N.min N.max N.of_nat Z.abs_N +*) + + + + +(** I) translation of Z.max, Z.min, Z.abs, Z.sgn into recognized equations *) + +Ltac zify_unop_core t thm a := + (* Let's introduce the specification theorem for t *) + pose proof (thm a); + (* Then we replace (t a) everywhere with a fresh variable *) + let z := fresh "z" in set (z:=t a) in *; clearbody z. + +Ltac zify_unop_var_or_term t thm a := + (* If a is a variable, no need for aliasing *) + let za := fresh "z" in + (rename a into za; rename za into a; zify_unop_core t thm a) || + (* Otherwise, a is a complex term: we alias it. *) + (remember a as za; zify_unop_core t thm za). + +Ltac zify_unop t thm a := + (* If a is a scalar, we can simply reduce the unop. *) + (* Note that simpl wasn't enough to reduce [Z.max 0 0] (#5439) *) + let isz := isZcst a in + match isz with + | true => + let u := eval compute in (t a) in + change (t a) with u in * + | _ => zify_unop_var_or_term t thm a + end. + +Ltac zify_unop_nored t thm a := + (* in this version, we don't try to reduce the unop (that can be (Z.add x)) *) + let isz := isZcst a in + match isz with + | true => zify_unop_core t thm a + | _ => zify_unop_var_or_term t thm a + end. + +Ltac zify_binop t thm a b:= + (* works as zify_unop, except that we should be careful when + dealing with b, since it can be equal to a *) + let isza := isZcst a in + match isza with + | true => zify_unop (t a) (thm a) b + | _ => + let za := fresh "z" in + (rename a into za; rename za into a; zify_unop_nored (t a) (thm a) b) || + (remember a as za; match goal with + | H : za = b |- _ => zify_unop_nored (t za) (thm za) za + | _ => zify_unop_nored (t za) (thm za) b + end) + end. + +Ltac zify_op_1 := + match goal with + | x := ?t : Z |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x + | |- context [ Z.max ?a ?b ] => zify_binop Z.max Z.max_spec a b + | H : context [ Z.max ?a ?b ] |- _ => zify_binop Z.max Z.max_spec a b + | |- context [ Z.min ?a ?b ] => zify_binop Z.min Z.min_spec a b + | H : context [ Z.min ?a ?b ] |- _ => zify_binop Z.min Z.min_spec a b + | |- context [ Z.sgn ?a ] => zify_unop Z.sgn Z.sgn_spec a + | H : context [ Z.sgn ?a ] |- _ => zify_unop Z.sgn Z.sgn_spec a + | |- context [ Z.abs ?a ] => zify_unop Z.abs Z.abs_spec a + | H : context [ Z.abs ?a ] |- _ => zify_unop Z.abs Z.abs_spec a + end. + +Ltac zify_op := repeat zify_op_1. + + + + + +(** II) Conversion from nat to Z *) + + +Definition Z_of_nat' := Z.of_nat. + +Ltac hide_Z_of_nat t := + let z := fresh "z" in set (z:=Z.of_nat t) in *; + change Z.of_nat with Z_of_nat' in z; + unfold z in *; clear z. + +Ltac zify_nat_rel := + match goal with + (* I: equalities *) + | x := ?t : nat |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x + | |- (@eq nat ?a ?b) => apply (Nat2Z.inj a b) (* shortcut *) + | H : context [ @eq nat ?a ?b ] |- _ => rewrite <- (Nat2Z.inj_iff a b) in H + | |- context [ @eq nat ?a ?b ] => rewrite <- (Nat2Z.inj_iff a b) + (* II: less than *) + | H : context [ lt ?a ?b ] |- _ => rewrite (Nat2Z.inj_lt a b) in H + | |- context [ lt ?a ?b ] => rewrite (Nat2Z.inj_lt a b) + (* III: less or equal *) + | H : context [ le ?a ?b ] |- _ => rewrite (Nat2Z.inj_le a b) in H + | |- context [ le ?a ?b ] => rewrite (Nat2Z.inj_le a b) + (* IV: greater than *) + | H : context [ gt ?a ?b ] |- _ => rewrite (Nat2Z.inj_gt a b) in H + | |- context [ gt ?a ?b ] => rewrite (Nat2Z.inj_gt a b) + (* V: greater or equal *) + | H : context [ ge ?a ?b ] |- _ => rewrite (Nat2Z.inj_ge a b) in H + | |- context [ ge ?a ?b ] => rewrite (Nat2Z.inj_ge a b) + end. + +Ltac zify_nat_op := + match goal with + (* misc type conversions: positive/N/Z to nat *) + | H : context [ Z.of_nat (Pos.to_nat ?a) ] |- _ => rewrite (positive_nat_Z a) in H + | |- context [ Z.of_nat (Pos.to_nat ?a) ] => rewrite (positive_nat_Z a) + | H : context [ Z.of_nat (N.to_nat ?a) ] |- _ => rewrite (N_nat_Z a) in H + | |- context [ Z.of_nat (N.to_nat ?a) ] => rewrite (N_nat_Z a) + | H : context [ Z.of_nat (Z.abs_nat ?a) ] |- _ => rewrite (Zabs2Nat.id_abs a) in H + | |- context [ Z.of_nat (Z.abs_nat ?a) ] => rewrite (Zabs2Nat.id_abs a) + + (* plus -> Z.add *) + | H : context [ Z.of_nat (plus ?a ?b) ] |- _ => rewrite (Nat2Z.inj_add a b) in H + | |- context [ Z.of_nat (plus ?a ?b) ] => rewrite (Nat2Z.inj_add a b) + + (* min -> Z.min *) + | H : context [ Z.of_nat (min ?a ?b) ] |- _ => rewrite (Nat2Z.inj_min a b) in H + | |- context [ Z.of_nat (min ?a ?b) ] => rewrite (Nat2Z.inj_min a b) + + (* max -> Z.max *) + | H : context [ Z.of_nat (max ?a ?b) ] |- _ => rewrite (Nat2Z.inj_max a b) in H + | |- context [ Z.of_nat (max ?a ?b) ] => rewrite (Nat2Z.inj_max a b) + + (* minus -> Z.max (Z.sub ... ...) 0 *) + | H : context [ Z.of_nat (minus ?a ?b) ] |- _ => rewrite (Nat2Z.inj_sub_max a b) in H + | |- context [ Z.of_nat (minus ?a ?b) ] => rewrite (Nat2Z.inj_sub_max a b) + + (* pred -> minus ... -1 -> Z.max (Z.sub ... -1) 0 *) + | H : context [ Z.of_nat (pred ?a) ] |- _ => rewrite (pred_of_minus a) in H + | |- context [ Z.of_nat (pred ?a) ] => rewrite (pred_of_minus a) + + (* mult -> Z.mul and a positivity hypothesis *) + | H : context [ Z.of_nat (mult ?a ?b) ] |- _ => + pose proof (Nat2Z.is_nonneg (mult a b)); + rewrite (Nat2Z.inj_mul a b) in * + | |- context [ Z.of_nat (mult ?a ?b) ] => + pose proof (Nat2Z.is_nonneg (mult a b)); + rewrite (Nat2Z.inj_mul a b) in * + + (* O -> Z0 *) + | H : context [ Z.of_nat O ] |- _ => change (Z.of_nat O) with Z0 in H + | |- context [ Z.of_nat O ] => change (Z.of_nat O) with Z0 + + (* S -> number or Z.succ *) + | H : context [ Z.of_nat (S ?a) ] |- _ => + let isnat := isnatcst a in + match isnat with + | true => + let t := eval compute in (Z.of_nat (S a)) in + change (Z.of_nat (S a)) with t in H + | _ => rewrite (Nat2Z.inj_succ a) in H + | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), + hide [Z.of_nat (S a)] in this one hypothesis *) + change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H + end + | |- context [ Z.of_nat (S ?a) ] => + let isnat := isnatcst a in + match isnat with + | true => + let t := eval compute in (Z.of_nat (S a)) in + change (Z.of_nat (S a)) with t + | _ => rewrite (Nat2Z.inj_succ a) + | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), + hide [Z.of_nat (S a)] in the goal *) + change (Z.of_nat (S a)) with (Z_of_nat' (S a)) + end + + (* atoms of type nat : we add a positivity condition (if not already there) *) + | _ : 0 <= Z.of_nat ?a |- _ => hide_Z_of_nat a + | _ : context [ Z.of_nat ?a ] |- _ => + pose proof (Nat2Z.is_nonneg a); hide_Z_of_nat a + | |- context [ Z.of_nat ?a ] => + pose proof (Nat2Z.is_nonneg a); hide_Z_of_nat a + end. + +Ltac zify_nat := repeat zify_nat_rel; repeat zify_nat_op; unfold Z_of_nat' in *. + + + + +(* III) conversion from positive to Z *) + +Definition Zpos' := Zpos. +Definition Zneg' := Zneg. + +Ltac hide_Zpos t := + let z := fresh "z" in set (z:=Zpos t) in *; + change Zpos with Zpos' in z; + unfold z in *; clear z. + +Ltac zify_positive_rel := + match goal with + (* I: equalities *) + | x := ?t : positive |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x + | |- (@eq positive ?a ?b) => apply Pos2Z.inj + | H : context [ @eq positive ?a ?b ] |- _ => rewrite <- (Pos2Z.inj_iff a b) in H + | |- context [ @eq positive ?a ?b ] => rewrite <- (Pos2Z.inj_iff a b) + (* II: less than *) + | H : context [ (?a < ?b)%positive ] |- _ => change (a<b)%positive with (Zpos a<Zpos b) in H + | |- context [ (?a < ?b)%positive ] => change (a<b)%positive with (Zpos a<Zpos b) + (* III: less or equal *) + | H : context [ (?a <= ?b)%positive ] |- _ => change (a<=b)%positive with (Zpos a<=Zpos b) in H + | |- context [ (?a <= ?b)%positive ] => change (a<=b)%positive with (Zpos a<=Zpos b) + (* IV: greater than *) + | H : context [ (?a > ?b)%positive ] |- _ => change (a>b)%positive with (Zpos a>Zpos b) in H + | |- context [ (?a > ?b)%positive ] => change (a>b)%positive with (Zpos a>Zpos b) + (* V: greater or equal *) + | H : context [ (?a >= ?b)%positive ] |- _ => change (a>=b)%positive with (Zpos a>=Zpos b) in H + | |- context [ (?a >= ?b)%positive ] => change (a>=b)%positive with (Zpos a>=Zpos b) + end. + +Ltac zify_positive_op := + match goal with + (* Zneg -> -Zpos (except for numbers) *) + | H : context [ Zneg ?a ] |- _ => + let isp := isPcst a in + match isp with + | true => change (Zneg a) with (Zneg' a) in H + | _ => change (Zneg a) with (- Zpos a) in H + end + | |- context [ Zneg ?a ] => + let isp := isPcst a in + match isp with + | true => change (Zneg a) with (Zneg' a) + | _ => change (Zneg a) with (- Zpos a) + end + + (* misc type conversions: nat to positive *) + | H : context [ Zpos (Pos.of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H + | |- context [ Zpos (Pos.of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a) + + (* Pos.add -> Z.add *) + | H : context [ Zpos (?a + ?b) ] |- _ => change (Zpos (a+b)) with (Zpos a + Zpos b) in H + | |- context [ Zpos (?a + ?b) ] => change (Zpos (a+b)) with (Zpos a + Zpos b) + + (* Pos.min -> Z.min *) + | H : context [ Zpos (Pos.min ?a ?b) ] |- _ => rewrite (Pos2Z.inj_min a b) in H + | |- context [ Zpos (Pos.min ?a ?b) ] => rewrite (Pos2Z.inj_min a b) + + (* Pos.max -> Z.max *) + | H : context [ Zpos (Pos.max ?a ?b) ] |- _ => rewrite (Pos2Z.inj_max a b) in H + | |- context [ Zpos (Pos.max ?a ?b) ] => rewrite (Pos2Z.inj_max a b) + + (* Pos.sub -> Z.max 1 (Z.sub ... ...) *) + | H : context [ Zpos (Pos.sub ?a ?b) ] |- _ => rewrite (Pos2Z.inj_sub_max a b) in H + | |- context [ Zpos (Pos.sub ?a ?b) ] => rewrite (Pos2Z.inj_sub_max a b) + + (* Pos.succ -> Z.succ *) + | H : context [ Zpos (Pos.succ ?a) ] |- _ => rewrite (Pos2Z.inj_succ a) in H + | |- context [ Zpos (Pos.succ ?a) ] => rewrite (Pos2Z.inj_succ a) + + (* Pos.pred -> Pos.sub ... -1 -> Z.max 1 (Z.sub ... - 1) *) + | H : context [ Zpos (Pos.pred ?a) ] |- _ => rewrite <- (Pos.sub_1_r a) in H + | |- context [ Zpos (Pos.pred ?a) ] => rewrite <- (Pos.sub_1_r a) + + (* Pos.mul -> Z.mul and a positivity hypothesis *) + | H : context [ Zpos (?a * ?b) ] |- _ => + pose proof (Pos2Z.is_pos (Pos.mul a b)); + change (Zpos (a*b)) with (Zpos a * Zpos b) in * + | |- context [ Zpos (?a * ?b) ] => + pose proof (Pos2Z.is_pos (Pos.mul a b)); + change (Zpos (a*b)) with (Zpos a * Zpos b) in * + + (* xO *) + | H : context [ Zpos (xO ?a) ] |- _ => + let isp := isPcst a in + match isp with + | true => change (Zpos (xO a)) with (Zpos' (xO a)) in H + | _ => rewrite (Pos2Z.inj_xO a) in H + end + | |- context [ Zpos (xO ?a) ] => + let isp := isPcst a in + match isp with + | true => change (Zpos (xO a)) with (Zpos' (xO a)) + | _ => rewrite (Pos2Z.inj_xO a) + end + (* xI *) + | H : context [ Zpos (xI ?a) ] |- _ => + let isp := isPcst a in + match isp with + | true => change (Zpos (xI a)) with (Zpos' (xI a)) in H + | _ => rewrite (Pos2Z.inj_xI a) in H + end + | |- context [ Zpos (xI ?a) ] => + let isp := isPcst a in + match isp with + | true => change (Zpos (xI a)) with (Zpos' (xI a)) + | _ => rewrite (Pos2Z.inj_xI a) + end + + (* xI : nothing to do, just prevent adding a useless positivity condition *) + | H : context [ Zpos xH ] |- _ => hide_Zpos xH + | |- context [ Zpos xH ] => hide_Zpos xH + + (* atoms of type positive : we add a positivity condition (if not already there) *) + | _ : 0 < Zpos ?a |- _ => hide_Zpos a + | _ : context [ Zpos ?a ] |- _ => pose proof (Pos2Z.is_pos a); hide_Zpos a + | |- context [ Zpos ?a ] => pose proof (Pos2Z.is_pos a); hide_Zpos a + end. + +Ltac zify_positive := + repeat zify_positive_rel; repeat zify_positive_op; unfold Zpos',Zneg' in *. + + + + + +(* IV) conversion from N to Z *) + +Definition Z_of_N' := Z.of_N. + +Ltac hide_Z_of_N t := + let z := fresh "z" in set (z:=Z.of_N t) in *; + change Z.of_N with Z_of_N' in z; + unfold z in *; clear z. + +Ltac zify_N_rel := + match goal with + (* I: equalities *) + | x := ?t : N |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x + | |- (@eq N ?a ?b) => apply (N2Z.inj a b) (* shortcut *) + | H : context [ @eq N ?a ?b ] |- _ => rewrite <- (N2Z.inj_iff a b) in H + | |- context [ @eq N ?a ?b ] => rewrite <- (N2Z.inj_iff a b) + (* II: less than *) + | H : context [ (?a < ?b)%N ] |- _ => rewrite (N2Z.inj_lt a b) in H + | |- context [ (?a < ?b)%N ] => rewrite (N2Z.inj_lt a b) + (* III: less or equal *) + | H : context [ (?a <= ?b)%N ] |- _ => rewrite (N2Z.inj_le a b) in H + | |- context [ (?a <= ?b)%N ] => rewrite (N2Z.inj_le a b) + (* IV: greater than *) + | H : context [ (?a > ?b)%N ] |- _ => rewrite (N2Z.inj_gt a b) in H + | |- context [ (?a > ?b)%N ] => rewrite (N2Z.inj_gt a b) + (* V: greater or equal *) + | H : context [ (?a >= ?b)%N ] |- _ => rewrite (N2Z.inj_ge a b) in H + | |- context [ (?a >= ?b)%N ] => rewrite (N2Z.inj_ge a b) + end. + +Ltac zify_N_op := + match goal with + (* misc type conversions: nat to positive *) + | H : context [ Z.of_N (N.of_nat ?a) ] |- _ => rewrite (nat_N_Z a) in H + | |- context [ Z.of_N (N.of_nat ?a) ] => rewrite (nat_N_Z a) + | H : context [ Z.of_N (Z.abs_N ?a) ] |- _ => rewrite (N2Z.inj_abs_N a) in H + | |- context [ Z.of_N (Z.abs_N ?a) ] => rewrite (N2Z.inj_abs_N a) + | H : context [ Z.of_N (Npos ?a) ] |- _ => rewrite (N2Z.inj_pos a) in H + | |- context [ Z.of_N (Npos ?a) ] => rewrite (N2Z.inj_pos a) + | H : context [ Z.of_N N0 ] |- _ => change (Z.of_N N0) with Z0 in H + | |- context [ Z.of_N N0 ] => change (Z.of_N N0) with Z0 + + (* N.add -> Z.add *) + | H : context [ Z.of_N (N.add ?a ?b) ] |- _ => rewrite (N2Z.inj_add a b) in H + | |- context [ Z.of_N (N.add ?a ?b) ] => rewrite (N2Z.inj_add a b) + + (* N.min -> Z.min *) + | H : context [ Z.of_N (N.min ?a ?b) ] |- _ => rewrite (N2Z.inj_min a b) in H + | |- context [ Z.of_N (N.min ?a ?b) ] => rewrite (N2Z.inj_min a b) + + (* N.max -> Z.max *) + | H : context [ Z.of_N (N.max ?a ?b) ] |- _ => rewrite (N2Z.inj_max a b) in H + | |- context [ Z.of_N (N.max ?a ?b) ] => rewrite (N2Z.inj_max a b) + + (* N.sub -> Z.max 0 (Z.sub ... ...) *) + | H : context [ Z.of_N (N.sub ?a ?b) ] |- _ => rewrite (N2Z.inj_sub_max a b) in H + | |- context [ Z.of_N (N.sub ?a ?b) ] => rewrite (N2Z.inj_sub_max a b) + + (* pred -> minus ... -1 -> Z.max (Z.sub ... -1) 0 *) + | H : context [ Z.of_N (N.pred ?a) ] |- _ => rewrite (N.pred_sub a) in H + | |- context [ Z.of_N (N.pred ?a) ] => rewrite (N.pred_sub a) + + (* N.succ -> Z.succ *) + | H : context [ Z.of_N (N.succ ?a) ] |- _ => rewrite (N2Z.inj_succ a) in H + | |- context [ Z.of_N (N.succ ?a) ] => rewrite (N2Z.inj_succ a) + + (* N.mul -> Z.mul and a positivity hypothesis *) + | H : context [ Z.of_N (N.mul ?a ?b) ] |- _ => + pose proof (N2Z.is_nonneg (N.mul a b)); rewrite (N2Z.inj_mul a b) in * + | |- 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 + | |- context [ Z.of_N ?a ] => pose proof (N2Z.is_nonneg a); hide_Z_of_N a + end. + +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. diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml new file mode 100644 index 0000000000..4802608fda --- /dev/null +++ b/plugins/omega/coq_omega.ml @@ -0,0 +1,1914 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(**************************************************************************) +(* *) +(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) +(* *) +(* Pierre Crégut (CNET, Lannion, France) *) +(* *) +(**************************************************************************) + +open CErrors +open Util +open Names +open Constr +open Context +open Nameops +open EConstr +open Tacticals.New +open Tacmach.New +open Tactics +open Logic +open Libnames +open Globnames +open Nametab +open Contradiction +open Tactypes +open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration +module OmegaSolver = Omega.MakeOmegaSolver (Bigint) +open OmegaSolver + +(* Added by JCF, 09/03/98 *) + +let elim_id id = simplest_elim (mkVar id) + +let resolve_id id = apply (mkVar id) + +let display_system_flag = ref false +let display_action_flag = ref false +let old_style_flag = ref false +let letin_flag = ref true + +(* Should we reset all variable labels between two runs of omega ? *) + +let reset_flag = ref true + +(* Coq < 8.5 was not performing such resets, hence omega was slightly + non-deterministic: successive runs of omega on the same problem may + lead to distinct proof-terms. + At the very least, these terms differed on the inner + variable names, but they could even be non-convertible : + the OmegaSolver relies on Hashtbl.iter, it can hence find a different + solution when variable indices differ. *) + +let read f () = !f +let write f x = f:=x + +open Goptions + +let () = + declare_bool_option + { optdepr = false; + optname = "Omega system time displaying flag"; + optkey = ["Omega";"System"]; + optread = read display_system_flag; + optwrite = write display_system_flag } + +let () = + declare_bool_option + { optdepr = false; + optname = "Omega action display flag"; + optkey = ["Omega";"Action"]; + optread = read display_action_flag; + optwrite = write display_action_flag } + +let () = + declare_bool_option + { optdepr = false; + optname = "Omega old style flag"; + optkey = ["Omega";"OldStyle"]; + optread = read old_style_flag; + optwrite = write old_style_flag } + +let () = + declare_bool_option + { optdepr = true; + optname = "Omega automatic reset of generated names"; + optkey = ["Stable";"Omega"]; + optread = read reset_flag; + optwrite = write reset_flag } + +let () = + declare_bool_option + { optdepr = false; + optname = "Omega takes advantage of context variables with body"; + optkey = ["Omega";"UseLocalDefs"]; + optread = read letin_flag; + optwrite = write letin_flag } + +let intref, reset_all_references = + let refs = ref [] in + (fun n -> let r = ref n in refs := (r,n) :: !refs; r), + (fun () -> List.iter (fun (r,n) -> r:=n) !refs) + +let new_identifier = + let cpt = intref 0 in + (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; Id.of_string s) + +let new_identifier_var = + let cpt = intref 0 in + (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; Id.of_string s) + +let new_id = + let cpt = intref 0 in fun () -> incr cpt; !cpt + +let new_var_num = + let cpt = intref 1000 in (fun () -> incr cpt; !cpt) + +let new_var = + let cpt = intref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt) + +let display_var i = Printf.sprintf "X%d" i + +let intern_id,unintern_id,reset_intern_tables = + let cpt = ref 0 in + let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in + (fun (name : Id.t) -> + try Hashtbl.find table name with Not_found -> + let idx = !cpt in + Hashtbl.add table name idx; + Hashtbl.add co_table idx name; + incr cpt; idx), + (fun idx -> + try Hashtbl.find co_table idx with Not_found -> + let v = new_var () in + Hashtbl.add table v idx; Hashtbl.add co_table idx v; v), + (fun () -> cpt := 0; Hashtbl.clear table) + +let mk_then tacs = tclTHENLIST tacs + +let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c]) + +let generalize_tac t = generalize t +let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] +let pf_nf gl c = pf_apply Tacred.simpl gl c + +let rev_assoc k = + let rec loop = function + | [] -> raise Not_found + | (v,k')::_ when Int.equal k k' -> v + | _ :: l -> loop l + in + loop + +let tag_hypothesis, hyp_of_tag, clear_tags = + let l = ref ([]:(Id.t * int) list) in + (fun h id -> l := (h,id):: !l), + (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis"), + (fun () -> l := []) + +let hide_constr,find_constr,clear_constr_tables,dump_tables = + let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in + (fun h id eg b -> l := (h,(id,eg,b)):: !l), + (fun sigma h -> + try List.assoc_f (eq_constr_nounivs sigma) h !l with Not_found -> failwith "find_contr"), + (fun () -> l := []), + (fun () -> !l) + +let reset_all () = + if !reset_flag then begin + reset_all_references (); + reset_intern_tables (); + clear_tags (); + clear_constr_tables () + end + +(* Lazy evaluation is used for Coq constants, because this code + is evaluated before the compiled modules are loaded. + To use the constant Zplus, one must type "Lazy.force coq_Zplus" + This is the right way to access to Coq constants in tactics ML code *) + +let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_monomorphic_global + |> EConstr.of_constr) + + +(* Zarith *) +let coq_xH = gen_constant "num.pos.xH" +let coq_xO = gen_constant "num.pos.xO" +let coq_xI = gen_constant "num.pos.xI" +let coq_Z0 = gen_constant "num.Z.Z0" +let coq_Zpos = gen_constant "num.Z.Zpos" +let coq_Zneg = gen_constant "num.Z.Zneg" +let coq_Z = gen_constant "num.Z.type" +let coq_comparison = gen_constant "core.comparison.type" +let coq_Gt = gen_constant "core.comparison.Gt" +let coq_Zplus = gen_constant "num.Z.add" +let coq_Zmult = gen_constant "num.Z.mul" +let coq_Zopp = gen_constant "num.Z.opp" +let coq_Zminus = gen_constant "num.Z.sub" +let coq_Zsucc = gen_constant "num.Z.succ" +let coq_Zpred = gen_constant "num.Z.pred" +let coq_Z_of_nat = gen_constant "num.Z.of_nat" +let coq_inj_plus = gen_constant "num.Nat2Z.inj_add" +let coq_inj_mult = gen_constant "num.Nat2Z.inj_mul" +let coq_inj_minus1 = gen_constant "num.Nat2Z.inj_sub" +let coq_inj_minus2 = gen_constant "plugins.omega.inj_minus2" +let coq_inj_S = gen_constant "num.Nat2Z.inj_succ" +let coq_inj_eq = gen_constant "plugins.omega.inj_eq" +let coq_inj_neq = gen_constant "plugins.omega.inj_neq" +let coq_inj_le = gen_constant "plugins.omega.inj_le" +let coq_inj_lt = gen_constant "plugins.omega.inj_lt" +let coq_inj_ge = gen_constant "plugins.omega.inj_ge" +let coq_inj_gt = gen_constant "plugins.omega.inj_gt" +let coq_fast_Zplus_assoc_reverse = gen_constant "plugins.omega.fast_Zplus_assoc_reverse" +let coq_fast_Zplus_assoc = gen_constant "plugins.omega.fast_Zplus_assoc" +let coq_fast_Zmult_assoc_reverse = gen_constant "plugins.omega.fast_Zmult_assoc_reverse" +let coq_fast_Zplus_permute = gen_constant "plugins.omega.fast_Zplus_permute" +let coq_fast_Zplus_comm = gen_constant "plugins.omega.fast_Zplus_comm" +let coq_fast_Zmult_comm = gen_constant "plugins.omega.fast_Zmult_comm" +let coq_Zmult_le_approx = gen_constant "plugins.omega.Zmult_le_approx" +let coq_OMEGA1 = gen_constant "plugins.omega.OMEGA1" +let coq_OMEGA2 = gen_constant "plugins.omega.OMEGA2" +let coq_OMEGA3 = gen_constant "plugins.omega.OMEGA3" +let coq_OMEGA4 = gen_constant "plugins.omega.OMEGA4" +let coq_OMEGA5 = gen_constant "plugins.omega.OMEGA5" +let coq_OMEGA6 = gen_constant "plugins.omega.OMEGA6" +let coq_OMEGA7 = gen_constant "plugins.omega.OMEGA7" +let coq_OMEGA8 = gen_constant "plugins.omega.OMEGA8" +let coq_OMEGA9 = gen_constant "plugins.omega.OMEGA9" +let coq_fast_OMEGA10 = gen_constant "plugins.omega.fast_OMEGA10" +let coq_fast_OMEGA11 = gen_constant "plugins.omega.fast_OMEGA11" +let coq_fast_OMEGA12 = gen_constant "plugins.omega.fast_OMEGA12" +let coq_fast_OMEGA13 = gen_constant "plugins.omega.fast_OMEGA13" +let coq_fast_OMEGA14 = gen_constant "plugins.omega.fast_OMEGA14" +let coq_fast_OMEGA15 = gen_constant "plugins.omega.fast_OMEGA15" +let coq_fast_OMEGA16 = gen_constant "plugins.omega.fast_OMEGA16" +let coq_OMEGA17 = gen_constant "plugins.omega.OMEGA17" +let coq_OMEGA18 = gen_constant "plugins.omega.OMEGA18" +let coq_OMEGA19 = gen_constant "plugins.omega.OMEGA19" +let coq_OMEGA20 = gen_constant "plugins.omega.OMEGA20" +let coq_fast_Zred_factor0 = gen_constant "plugins.omega.fast_Zred_factor0" +let coq_fast_Zred_factor1 = gen_constant "plugins.omega.fast_Zred_factor1" +let coq_fast_Zred_factor2 = gen_constant "plugins.omega.fast_Zred_factor2" +let coq_fast_Zred_factor3 = gen_constant "plugins.omega.fast_Zred_factor3" +let coq_fast_Zred_factor4 = gen_constant "plugins.omega.fast_Zred_factor4" +let coq_fast_Zred_factor5 = gen_constant "plugins.omega.fast_Zred_factor5" +let coq_fast_Zred_factor6 = gen_constant "plugins.omega.fast_Zred_factor6" +let coq_fast_Zmult_plus_distr_l = gen_constant "plugins.omega.fast_Zmult_plus_distr_l" +let coq_fast_Zopp_plus_distr = gen_constant "plugins.omega.fast_Zopp_plus_distr" +let coq_fast_Zopp_mult_distr_r = gen_constant "plugins.omega.fast_Zopp_mult_distr_r" +let coq_fast_Zopp_eq_mult_neg_1 = gen_constant "plugins.omega.fast_Zopp_eq_mult_neg_1" +let coq_Zegal_left = gen_constant "plugins.omega.Zegal_left" +let coq_Zne_left = gen_constant "plugins.omega.Zne_left" +let coq_Zlt_left = gen_constant "plugins.omega.Zlt_left" +let coq_Zge_left = gen_constant "plugins.omega.Zge_left" +let coq_Zgt_left = gen_constant "plugins.omega.Zgt_left" +let coq_Zle_left = gen_constant "plugins.omega.Zle_left" +let coq_new_var = gen_constant "plugins.omega.new_var" +let coq_intro_Z = gen_constant "plugins.omega.intro_Z" + +let coq_dec_eq = gen_constant "num.Z.eq_decidable" +let coq_dec_Zne = gen_constant "plugins.omega.dec_Zne" +let coq_dec_Zle = gen_constant "num.Z.le_decidable" +let coq_dec_Zlt = gen_constant "num.Z.lt_decidable" +let coq_dec_Zgt = gen_constant "plugins.omega.dec_Zgt" +let coq_dec_Zge = gen_constant "plugins.omega.dec_Zge" + +let coq_not_Zeq = gen_constant "plugins.omega.not_Zeq" +let coq_not_Zne = gen_constant "plugins.omega.not_Zne" +let coq_Znot_le_gt = gen_constant "plugins.omega.Znot_le_gt" +let coq_Znot_lt_ge = gen_constant "plugins.omega.Znot_lt_ge" +let coq_Znot_ge_lt = gen_constant "plugins.omega.Znot_ge_lt" +let coq_Znot_gt_le = gen_constant "plugins.omega.Znot_gt_le" +let coq_neq = gen_constant "plugins.omega.neq" +let coq_Zne = gen_constant "plugins.omega.Zne" +let coq_Zle = gen_constant "num.Z.le" +let coq_Zlt = gen_constant "num.Z.lt" +let coq_Zge = gen_constant "num.Z.ge" +let coq_Zgt = gen_constant "num.Z.gt" + +(* Peano/Datatypes *) +let coq_nat = gen_constant "num.nat.type" +let coq_O = gen_constant "num.nat.O" +let coq_S = gen_constant "num.nat.S" +let coq_le = gen_constant "num.nat.le" +let coq_lt = gen_constant "num.nat.lt" +let coq_ge = gen_constant "num.nat.ge" +let coq_gt = gen_constant "num.nat.gt" +let coq_plus = gen_constant "num.nat.add" +let coq_minus = gen_constant "num.nat.sub" +let coq_mult = gen_constant "num.nat.mul" +let coq_pred = gen_constant "num.nat.pred" + +(* Compare_dec/Peano_dec/Minus *) +let coq_pred_of_minus = gen_constant "num.nat.pred_of_minus" +let coq_le_gt_dec = gen_constant "num.nat.le_gt_dec" +let coq_dec_eq_nat = gen_constant "num.nat.eq_dec" +let coq_dec_le = gen_constant "num.nat.dec_le" +let coq_dec_lt = gen_constant "num.nat.dec_lt" +let coq_dec_ge = gen_constant "num.nat.dec_ge" +let coq_dec_gt = gen_constant "num.nat.dec_gt" +let coq_not_eq = gen_constant "num.nat.not_eq" +let coq_not_le = gen_constant "num.nat.not_le" +let coq_not_lt = gen_constant "num.nat.not_lt" +let coq_not_ge = gen_constant "num.nat.not_ge" +let coq_not_gt = gen_constant "num.nat.not_gt" + +(* Logic/Decidable *) +let coq_eq_ind_r = gen_constant "core.eq.ind_r" + +let coq_dec_or = gen_constant "core.dec.or" +let coq_dec_and = gen_constant "core.dec.and" +let coq_dec_imp = gen_constant "core.dec.imp" +let coq_dec_iff = gen_constant "core.dec.iff" +let coq_dec_not = gen_constant "core.dec.not" +let coq_dec_False = gen_constant "core.dec.False" +let coq_dec_not_not = gen_constant "core.dec.not_not" +let coq_dec_True = gen_constant "core.dec.True" + +let coq_not_or = gen_constant "core.dec.not_or" +let coq_not_and = gen_constant "core.dec.not_and" +let coq_not_imp = gen_constant "core.dec.not_imp" +let coq_not_iff = gen_constant "core.dec.not_iff" +let coq_not_not = gen_constant "core.dec.dec_not_not" +let coq_imp_simp = gen_constant "core.dec.imp_simp" +let coq_iff = gen_constant "core.iff.type" +let coq_not = gen_constant "core.not.type" +let coq_and = gen_constant "core.and.type" +let coq_or = gen_constant "core.or.type" +let coq_eq = gen_constant "core.eq.type" +let coq_ex = gen_constant "core.ex.type" +let coq_False = gen_constant "core.False.type" +let coq_True = gen_constant "core.True.type" + +(* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *) + +(* For unfold *) +let evaluable_ref_of_constr s c = + let env = Global.env () in + let evd = Evd.from_env env in + match EConstr.kind evd (Lazy.force c) with + | Const (kn,u) when Tacred.is_evaluable env (EvalConstRef kn) -> + EvalConstRef kn + | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant.")) + +let sp_Zsucc = lazy (evaluable_ref_of_constr "Z.succ" coq_Zsucc) +let sp_Zpred = lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred) +let sp_Zminus = lazy (evaluable_ref_of_constr "Z.sub" coq_Zminus) +let sp_Zle = lazy (evaluable_ref_of_constr "Z.le" coq_Zle) +let sp_Zgt = lazy (evaluable_ref_of_constr "Z.gt" coq_Zgt) +let sp_not = lazy (evaluable_ref_of_constr "not" coq_not) + +let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |]) +let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |]) +let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |]) +let mk_gen_eq ty t1 t2 = mkApp (Lazy.force coq_eq, [| ty; t1; t2 |]) +let mk_eq t1 t2 = mk_gen_eq (Lazy.force coq_Z) t1 t2 +let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |]) +let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |]) +let mk_and t1 t2 = mkApp (Lazy.force coq_and, [| t1; t2 |]) +let mk_or t1 t2 = mkApp (Lazy.force coq_or, [| t1; t2 |]) +let mk_not t = mkApp (Lazy.force coq_not, [| t |]) +let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |]) + +let mk_integer n = + let rec loop n = + if n =? one then Lazy.force coq_xH else + mkApp((if n mod two =? zero then Lazy.force coq_xO else Lazy.force coq_xI), + [| loop (n/two) |]) + in + if n =? zero then Lazy.force coq_Z0 + else mkApp ((if n >? zero then Lazy.force coq_Zpos else Lazy.force coq_Zneg), + [| loop (abs n) |]) + +type omega_constant = + | Zplus | Zmult | Zminus | Zsucc | Zopp | Zpred + | Plus | Mult | Minus | Pred | S | O + | Zpos | Zneg | Z0 | Z_of_nat + | Eq | Neq + | Zne | Zle | Zlt | Zge | Zgt + | Z | Nat + | And | Or | False | True | Not | Iff + | Le | Lt | Ge | Gt + | Other of string + +type result = + | Kvar of Id.t + | Kapp of omega_constant * constr list + | Kimp of constr * constr + | Kufo + +(* Nota: Kimp correspond to a binder (Prod), but hopefully we won't + have to bother with term lifting: Kimp will correspond to anonymous + product, for which (Rel 1) doesn't occur in the right term. + Moreover, we'll work on fully introduced goals, hence no Rel's in + the term parts that we manipulate, but rather Var's. + Said otherwise: all constr manipulated here are closed *) + +let destructurate_prop sigma t = + let eq_constr c1 c2 = eq_constr sigma c1 c2 in + let c, args = decompose_app sigma t in + match EConstr.kind sigma c, args with + | _, [_;_;_] when eq_constr (Lazy.force coq_eq) c -> Kapp (Eq,args) + | _, [_;_] when eq_constr c (Lazy.force coq_neq) -> Kapp (Neq,args) + | _, [_;_] when eq_constr c (Lazy.force coq_Zne) -> Kapp (Zne,args) + | _, [_;_] when eq_constr c (Lazy.force coq_Zle) -> Kapp (Zle,args) + | _, [_;_] when eq_constr c (Lazy.force coq_Zlt) -> Kapp (Zlt,args) + | _, [_;_] when eq_constr c (Lazy.force coq_Zge) -> Kapp (Zge,args) + | _, [_;_] when eq_constr c (Lazy.force coq_Zgt) -> Kapp (Zgt,args) + | _, [_;_] when eq_constr c (Lazy.force coq_and) -> Kapp (And,args) + | _, [_;_] when eq_constr c (Lazy.force coq_or) -> Kapp (Or,args) + | _, [_;_] when eq_constr c (Lazy.force coq_iff) -> Kapp (Iff, args) + | _, [_] when eq_constr c (Lazy.force coq_not) -> Kapp (Not,args) + | _, [] when eq_constr c (Lazy.force coq_False) -> Kapp (False,args) + | _, [] when eq_constr c (Lazy.force coq_True) -> Kapp (True,args) + | _, [_;_] when eq_constr c (Lazy.force coq_le) -> Kapp (Le,args) + | _, [_;_] when eq_constr c (Lazy.force coq_lt) -> Kapp (Lt,args) + | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args) + | _, [_;_] when eq_constr c (Lazy.force coq_gt) -> Kapp (Gt,args) + | Const (sp,_), args -> + Kapp (Other (string_of_path (path_of_global (ConstRef sp))),args) + | Construct (csp,_) , args -> + Kapp (Other (string_of_path (path_of_global (ConstructRef csp))), args) + | Ind (isp,_), args -> + Kapp (Other (string_of_path (path_of_global (IndRef isp))),args) + | Var id,[] -> Kvar id + | Prod ({binder_name=Anonymous},typ,body), [] -> Kimp(typ,body) + | Prod ({binder_name=Name _},_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal") + | _ -> Kufo + +let nf = Tacred.simpl + +let destructurate_type env sigma t = + let is_conv = Reductionops.is_conv env sigma in + let c, args = decompose_app sigma (nf env sigma t) in + match EConstr.kind sigma c, args with + | _, [] when is_conv c (Lazy.force coq_Z) -> Kapp (Z,args) + | _, [] when is_conv c (Lazy.force coq_nat) -> Kapp (Nat,args) + | _ -> Kufo + +let destructurate_term sigma t = + let eq_constr c1 c2 = eq_constr sigma c1 c2 in + let c, args = decompose_app sigma t in + match EConstr.kind sigma c, args with + | _, [_;_] when eq_constr c (Lazy.force coq_Zplus) -> Kapp (Zplus,args) + | _, [_;_] when eq_constr c (Lazy.force coq_Zmult) -> Kapp (Zmult,args) + | _, [_;_] when eq_constr c (Lazy.force coq_Zminus) -> Kapp (Zminus,args) + | _, [_] when eq_constr c (Lazy.force coq_Zsucc) -> Kapp (Zsucc,args) + | _, [_] when eq_constr c (Lazy.force coq_Zpred) -> Kapp (Zpred,args) + | _, [_] when eq_constr c (Lazy.force coq_Zopp) -> Kapp (Zopp,args) + | _, [_;_] when eq_constr c (Lazy.force coq_plus) -> Kapp (Plus,args) + | _, [_;_] when eq_constr c (Lazy.force coq_mult) -> Kapp (Mult,args) + | _, [_;_] when eq_constr c (Lazy.force coq_minus) -> Kapp (Minus,args) + | _, [_] when eq_constr c (Lazy.force coq_pred) -> Kapp (Pred,args) + | _, [_] when eq_constr c (Lazy.force coq_S) -> Kapp (S,args) + | _, [] when eq_constr c (Lazy.force coq_O) -> Kapp (O,args) + | _, [_] when eq_constr c (Lazy.force coq_Zpos) -> Kapp (Zneg,args) + | _, [_] when eq_constr c (Lazy.force coq_Zneg) -> Kapp (Zpos,args) + | _, [] when eq_constr c (Lazy.force coq_Z0) -> Kapp (Z0,args) + | _, [_] when eq_constr c (Lazy.force coq_Z_of_nat) -> Kapp (Z_of_nat,args) + | Var id,[] -> Kvar id + | _ -> Kufo + +let recognize_number sigma t = + let eq_constr c1 c2 = eq_constr sigma c1 c2 in + let rec loop t = + match decompose_app sigma t with + | f, [t] when eq_constr f (Lazy.force coq_xI) -> one + two * loop t + | f, [t] when eq_constr f (Lazy.force coq_xO) -> two * loop t + | f, [] when eq_constr f (Lazy.force coq_xH) -> one + | _ -> failwith "not a number" + in + match decompose_app sigma t with + | f, [t] when eq_constr f (Lazy.force coq_Zpos) -> loop t + | f, [t] when eq_constr f (Lazy.force coq_Zneg) -> neg (loop t) + | f, [] when eq_constr f (Lazy.force coq_Z0) -> zero + | _ -> failwith "not a number" + +type constr_path = + | P_APP of int + (* Abstraction and product *) + | P_TYPE + +let context sigma operation path (t : constr) = + let rec loop i p0 t = + match (p0,EConstr.kind sigma t) with + | (p, Cast (c,k,t)) -> mkCast (loop i p c,k,t) + | ([], _) -> operation i t + | ((P_APP n :: p), App (f,v)) -> + let v' = Array.copy v in + v'.(pred n) <- loop i p v'.(pred n); mkApp (f, v') + | (p, Fix ((_,n as ln),(tys,lna,v))) -> + let l = Array.length v in + let v' = Array.copy v in + v'.(n)<- loop (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v'))) + | ((P_TYPE :: p), Prod (n,t,c)) -> + (mkProd (n,loop i p t,c)) + | ((P_TYPE :: p), Lambda (n,t,c)) -> + (mkLambda (n,loop i p t,c)) + | ((P_TYPE :: p), LetIn (n,b,t,c)) -> + (mkLetIn (n,b,loop i p t,c)) + | (p, _) -> + failwith ("abstract_path " ^ string_of_int(List.length p)) + in + loop 1 path t + +let occurrence sigma path (t : constr) = + let rec loop p0 t = match (p0,EConstr.kind sigma t) with + | (p, Cast (c,_,_)) -> loop p c + | ([], _) -> t + | ((P_APP n :: p), App (f,v)) -> loop p v.(pred n) + | (p, Fix((_,n) ,(_,_,v))) -> loop p v.(n) + | ((P_TYPE :: p), Prod (n,term,c)) -> loop p term + | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term + | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term + | (p, _) -> + failwith ("occurrence " ^ string_of_int(List.length p)) + in + loop path t + +let abstract_path sigma typ path t = + let term_occur = ref (mkRel 0) in + let abstract = context sigma (fun i t -> term_occur:= t; mkRel i) path t in + mkLambda (make_annot (Name (Id.of_string "x")) Sorts.Relevant, typ, abstract), !term_occur + +let focused_simpl path = + let open Tacmach.New in + Proofview.Goal.enter begin fun gl -> + let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in + convert_concl_no_check newc DEFAULTcast + end + +let focused_simpl path = focused_simpl path + +type oformula = + | Oplus of oformula * oformula + | Otimes of oformula * oformula + | Oatom of Id.t + | Oz of bigint + | Oufo of constr + +let rec oprint = function + | Oplus(t1,t2) -> + print_string "("; oprint t1; print_string "+"; + oprint t2; print_string ")" + | Otimes (t1,t2) -> + print_string "("; oprint t1; print_string "*"; + oprint t2; print_string ")" + | Oatom s -> print_string (Id.to_string s) + | Oz i -> print_string (string_of_bigint i) + | Oufo f -> print_string "?" + +let rec weight = function + | Oatom c -> intern_id c + | Oz _ -> -1 + | Otimes(c,_) -> weight c + | Oplus _ -> failwith "weight" + | Oufo _ -> -1 + +let rec val_of = function + | Oatom c -> mkVar c + | Oz c -> mk_integer c + | Otimes (t1,t2) -> mkApp (Lazy.force coq_Zmult, [| val_of t1; val_of t2 |]) + | Oplus(t1,t2) -> mkApp (Lazy.force coq_Zplus, [| val_of t1; val_of t2 |]) + | Oufo c -> c + +let compile name kind = + let rec loop accu = function + | Oplus(Otimes(Oatom v,Oz n),r) -> loop ({v=intern_id v; c=n} :: accu) r + | Oz n -> + let id = new_id () in + tag_hypothesis name id; + {kind = kind; body = List.rev accu; constant = n; id = id} + | _ -> anomaly (Pp.str "compile_equation.") + in + loop [] + +let decompile af = + let rec loop = function + | ({v=v; c=n}::r) -> Oplus(Otimes(Oatom (unintern_id v),Oz n),loop r) + | [] -> Oz af.constant + in + loop af.body + +(** Backward compat to emulate the old Refine: normalize the goal conclusion *) +let new_hole env sigma c = + let c = Reductionops.nf_betaiota env sigma c in + Evarutil.new_evar env sigma c + +let clever_rewrite_base_poly typ p result theorem = + let open Tacmach.New in + Proofview.Goal.enter begin fun gl -> + let full = pf_concl gl in + let env = pf_env gl in + let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in + Refine.refine ~typecheck:false begin fun sigma -> + let t = + applist + (mkLambda + (make_annot (Name (Id.of_string "P")) Sorts.Relevant, + mkArrow typ Sorts.Relevant mkProp, + mkLambda + (make_annot (Name (Id.of_string "H")) Sorts.Relevant, + applist (mkRel 1,[result]), + mkApp (Lazy.force coq_eq_ind_r, + [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))), + [abstracted]) + in + let argt = mkApp (abstracted, [|result|]) in + let (sigma, hole) = new_hole env sigma argt in + (sigma, applist (t, [hole])) + end + end + +let clever_rewrite_base p result theorem = + clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem + +let clever_rewrite_base_nat p result theorem = + clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem + +let clever_rewrite_gen p result (t,args) = + let theorem = applist(t, args) in + clever_rewrite_base p result theorem + +let clever_rewrite_gen_nat p result (t,args) = + let theorem = applist(t, args) in + clever_rewrite_base_nat p result theorem + +(** Solve using the term the term [t _] *) +let refine_app gl t = + let open Tacmach.New in + Refine.refine ~typecheck:false begin fun sigma -> + let env = pf_env gl in + let ht = match EConstr.kind sigma (pf_get_type_of gl t) with + | Prod (_, t, _) -> t + | _ -> assert false + in + let (sigma, hole) = new_hole env sigma ht in + (sigma, applist (t, [hole])) + end + +let clever_rewrite p vpath t = + let open Tacmach.New in + Proofview.Goal.enter begin fun gl -> + let full = pf_concl gl in + let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in + let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in + let t' = applist(t, (vargs @ [abstracted])) in + refine_app gl t' + end + +(** simpl_coeffs : + The subterm at location [path_init] in the current goal should + look like [(v1*c1 + (v2*c2 + ... (vn*cn + k)))], and we reduce + via "simpl" each [ci] and the final constant [k]. + The path [path_k] gives the location of constant [k]. + Earlier, the whole was a mere call to [focused_simpl], + leading to reduction inside the atoms [vi], which is bad, + for instance when the atom is an evaluable definition + (see #4132). *) + +let simpl_coeffs path_init path_k = + Proofview.Goal.enter begin fun gl -> + let sigma = project gl in + let rec loop n t = + if Int.equal n 0 then pf_nf gl t + else + (* t should be of the form ((v * c) + ...) *) + match EConstr.kind sigma t with + | App(f,[|t1;t2|]) -> + (match EConstr.kind sigma t1 with + | App (g,[|v;c|]) -> + let c' = pf_nf gl c in + let t2' = loop (pred n) t2 in + mkApp (f,[|mkApp (g,[|v;c'|]);t2'|]) + | _ -> assert false) + | _ -> assert false + in + let n = Pervasives.(-) (List.length path_k) (List.length path_init) in + let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl) + in + convert_concl_no_check newc DEFAULTcast + end + +let rec shuffle p (t1,t2) = + match t1,t2 with + | Oplus(l1,r1), Oplus(l2,r2) -> + if weight l1 > weight l2 then + let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in + (clever_rewrite p [[P_APP 1;P_APP 1]; + [P_APP 1; P_APP 2];[P_APP 2]] + (Lazy.force coq_fast_Zplus_assoc_reverse) + :: tac, + Oplus(l1,t')) + else + let (tac,t') = shuffle (P_APP 2 :: p) (t1,r2) in + (clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]] + (Lazy.force coq_fast_Zplus_permute) + :: tac, + Oplus(l2,t')) + | Oplus(l1,r1), t2 -> + if weight l1 > weight t2 then + let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in + clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] + (Lazy.force coq_fast_Zplus_assoc_reverse) + :: tac, + Oplus(l1, t') + else + [clever_rewrite p [[P_APP 1];[P_APP 2]] + (Lazy.force coq_fast_Zplus_comm)], + Oplus(t2,t1) + | t1,Oplus(l2,r2) -> + if weight l2 > weight t1 then + let (tac,t') = shuffle (P_APP 2 :: p) (t1,r2) in + clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]] + (Lazy.force coq_fast_Zplus_permute) + :: tac, + Oplus(l2,t') + else [],Oplus(t1,t2) + | Oz t1,Oz t2 -> + [focused_simpl p], Oz(Bigint.add t1 t2) + | t1,t2 -> + if weight t1 < weight t2 then + [clever_rewrite p [[P_APP 1];[P_APP 2]] + (Lazy.force coq_fast_Zplus_comm)], + Oplus(t2,t1) + else [],Oplus(t1,t2) + +let shuffle_mult p_init k1 e1 k2 e2 = + let rec loop p = function + | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') -> + if Int.equal v1 v2 then + let tac = + clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; + [P_APP 1; P_APP 1; P_APP 1; P_APP 2]; + [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; + [P_APP 1; P_APP 1; P_APP 2]; + [P_APP 2; P_APP 1; P_APP 2]; + [P_APP 1; P_APP 2]; + [P_APP 2; P_APP 2]] + (Lazy.force coq_fast_OMEGA10) + in + if Bigint.add (Bigint.mult k1 c1) (Bigint.mult k2 c2) =? zero then + let tac' = + clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] + (Lazy.force coq_fast_Zred_factor5) in + tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' :: + loop p (l1,l2) + else tac :: loop (P_APP 2 :: p) (l1,l2) + else if v1 > v2 then + clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; + [P_APP 1; P_APP 1; P_APP 1; P_APP 2]; + [P_APP 1; P_APP 1; P_APP 2]; + [P_APP 2]; + [P_APP 1; P_APP 2]] + (Lazy.force coq_fast_OMEGA11) :: + loop (P_APP 2 :: p) (l1,l2') + else + clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1]; + [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; + [P_APP 1]; + [P_APP 2; P_APP 1; P_APP 2]; + [P_APP 2; P_APP 2]] + (Lazy.force coq_fast_OMEGA12) :: + loop (P_APP 2 :: p) (l1',l2) + | ({c=c1;v=v1}::l1), [] -> + clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; + [P_APP 1; P_APP 1; P_APP 1; P_APP 2]; + [P_APP 1; P_APP 1; P_APP 2]; + [P_APP 2]; + [P_APP 1; P_APP 2]] + (Lazy.force coq_fast_OMEGA11) :: + loop (P_APP 2 :: p) (l1,[]) + | [],({c=c2;v=v2}::l2) -> + clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1]; + [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; + [P_APP 1]; + [P_APP 2; P_APP 1; P_APP 2]; + [P_APP 2; P_APP 2]] + (Lazy.force coq_fast_OMEGA12) :: + loop (P_APP 2 :: p) ([],l2) + | [],[] -> [simpl_coeffs p_init p] + in + loop p_init (e1,e2) + +let shuffle_mult_right p_init e1 k2 e2 = + let rec loop p = function + | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') -> + if Int.equal v1 v2 then + let tac = + clever_rewrite p + [[P_APP 1; P_APP 1; P_APP 1]; + [P_APP 1; P_APP 1; P_APP 2]; + [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; + [P_APP 1; P_APP 2]; + [P_APP 2; P_APP 1; P_APP 2]; + [P_APP 2; P_APP 2]] + (Lazy.force coq_fast_OMEGA15) + in + if Bigint.add c1 (Bigint.mult k2 c2) =? zero then + let tac' = + clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] + (Lazy.force coq_fast_Zred_factor5) + in + tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' :: + loop p (l1,l2) + else tac :: loop (P_APP 2 :: p) (l1,l2) + else if v1 > v2 then + clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] + (Lazy.force coq_fast_Zplus_assoc_reverse) :: + loop (P_APP 2 :: p) (l1,l2') + else + clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1]; + [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; + [P_APP 1]; + [P_APP 2; P_APP 1; P_APP 2]; + [P_APP 2; P_APP 2]] + (Lazy.force coq_fast_OMEGA12) :: + loop (P_APP 2 :: p) (l1',l2) + | ({c=c1;v=v1}::l1), [] -> + clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] + (Lazy.force coq_fast_Zplus_assoc_reverse) :: + loop (P_APP 2 :: p) (l1,[]) + | [],({c=c2;v=v2}::l2) -> + clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1]; + [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; + [P_APP 1]; + [P_APP 2; P_APP 1; P_APP 2]; + [P_APP 2; P_APP 2]] + (Lazy.force coq_fast_OMEGA12) :: + loop (P_APP 2 :: p) ([],l2) + | [],[] -> [simpl_coeffs p_init p] + in + loop p_init (e1,e2) + +let rec shuffle_cancel p = function + | [] -> [focused_simpl p] + | ({c=c1}::l1) -> + let tac = + clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 2]; + [P_APP 2; P_APP 2]; + [P_APP 1; P_APP 1; P_APP 2; P_APP 1]] + (if c1 >? zero then + (Lazy.force coq_fast_OMEGA13) + else + (Lazy.force coq_fast_OMEGA14)) + in + tac :: shuffle_cancel p l1 + +let rec scalar p n = function + | Oplus(t1,t2) -> + let tac1,t1' = scalar (P_APP 1 :: p) n t1 and + tac2,t2' = scalar (P_APP 2 :: p) n t2 in + clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]] + (Lazy.force coq_fast_Zmult_plus_distr_l) :: + (tac1 @ tac2), Oplus(t1',t2') + | Otimes(t1,Oz x) -> + [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]] + (Lazy.force coq_fast_Zmult_assoc_reverse); + focused_simpl (P_APP 2 :: p)], + Otimes(t1,Oz (n*x)) + | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products") + | (Oatom _ as t) -> [], Otimes(t,Oz n) + | Oz i -> [focused_simpl p],Oz(n*i) + | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |])) + +let scalar_norm p_init = + let rec loop p = function + | [] -> [simpl_coeffs p_init p] + | (_::l) -> + clever_rewrite p + [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 1; P_APP 2]; + [P_APP 1; P_APP 2];[P_APP 2]] + (Lazy.force coq_fast_OMEGA16) :: loop (P_APP 2 :: p) l + in + loop p_init + +let norm_add p_init = + let rec loop p = function + | [] -> [simpl_coeffs p_init p] + | _:: l -> + clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] + (Lazy.force coq_fast_Zplus_assoc_reverse) :: + loop (P_APP 2 :: p) l + in + loop p_init + +let scalar_norm_add p_init = + let rec loop p = function + | [] -> [simpl_coeffs p_init p] + | _ :: l -> + clever_rewrite p + [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; + [P_APP 1; P_APP 1; P_APP 1; P_APP 2]; + [P_APP 1; P_APP 1; P_APP 2]; [P_APP 2]; [P_APP 1; P_APP 2]] + (Lazy.force coq_fast_OMEGA11) :: loop (P_APP 2 :: p) l + in + loop p_init + +let rec negate p = function + | Oplus(t1,t2) -> + let tac1,t1' = negate (P_APP 1 :: p) t1 and + tac2,t2' = negate (P_APP 2 :: p) t2 in + clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]] + (Lazy.force coq_fast_Zopp_plus_distr) :: + (tac1 @ tac2), + Oplus(t1',t2') + | Otimes(t1,Oz x) -> + [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]] + (Lazy.force coq_fast_Zopp_mult_distr_r); + focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (neg x)) + | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products") + | (Oatom _ as t) -> + let r = Otimes(t,Oz(negone)) in + [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1)], r + | Oz i -> [focused_simpl p],Oz(neg i) + | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |])) + +let rec transform sigma p t = + let default isnat t' = + try + let v,th,_ = find_constr sigma t' in + [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v + with e when CErrors.noncritical e -> + let v = new_identifier_var () + and th = new_identifier () in + hide_constr t' v th isnat; + [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v + in + try match destructurate_term sigma t with + | Kapp(Zplus,[t1;t2]) -> + let tac1,t1' = transform sigma (P_APP 1 :: p) t1 + and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in + let tac,t' = shuffle p (t1',t2') in + tac1 @ tac2 @ tac, t' + | Kapp(Zminus,[t1;t2]) -> + let tac,t = + transform sigma p + (mkApp (Lazy.force coq_Zplus, + [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in + unfold sp_Zminus :: tac,t + | Kapp(Zsucc,[t1]) -> + let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus, + [| t1; mk_integer one |])) in + unfold sp_Zsucc :: tac,t + | Kapp(Zpred,[t1]) -> + let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus, + [| t1; mk_integer negone |])) in + unfold sp_Zpred :: tac,t + | Kapp(Zmult,[t1;t2]) -> + let tac1,t1' = transform sigma (P_APP 1 :: p) t1 + and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in + begin match t1',t2' with + | (_,Oz n) -> let tac,t' = scalar p n t1' in tac1 @ tac2 @ tac,t' + | (Oz n,_) -> + let sym = + clever_rewrite p [[P_APP 1];[P_APP 2]] + (Lazy.force coq_fast_Zmult_comm) in + let tac,t' = scalar p n t2' in tac1 @ tac2 @ (sym :: tac),t' + | _ -> default false t + end + | Kapp((Zpos|Zneg|Z0),_) -> + (try ([],Oz(recognize_number sigma t)) + with e when CErrors.noncritical e -> default false t) + | Kvar s -> [],Oatom s + | Kapp(Zopp,[t]) -> + let tac,t' = transform sigma (P_APP 1 :: p) t in + let tac',t'' = negate p t' in + tac @ tac', t'' + | Kapp(Z_of_nat,[t']) -> default true t' + | _ -> default false t + with e when catchable_exception e -> default false t + +let shrink_pair p f1 f2 = + match f1,f2 with + | Oatom v,Oatom _ -> + let r = Otimes(Oatom v,Oz two) in + clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zred_factor1), r + | Oatom v, Otimes(_,c2) -> + let r = Otimes(Oatom v,Oplus(c2,Oz one)) in + clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 2]] + (Lazy.force coq_fast_Zred_factor2), r + | Otimes (v1,c1),Oatom v -> + let r = Otimes(Oatom v,Oplus(c1,Oz one)) in + clever_rewrite p [[P_APP 2];[P_APP 1;P_APP 2]] + (Lazy.force coq_fast_Zred_factor3), r + | Otimes (Oatom v,c1),Otimes (v2,c2) -> + let r = Otimes(Oatom v,Oplus(c1,c2)) in + clever_rewrite p + [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2;P_APP 2]] + (Lazy.force coq_fast_Zred_factor4),r + | t1,t2 -> + begin + oprint t1; print_newline (); oprint t2; print_newline (); + flush Pervasives.stdout; CErrors.user_err Pp.(str "shrink.1") + end + +let reduce_factor p = function + | Oatom v -> + let r = Otimes(Oatom v,Oz one) in + [clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor0)],r + | Otimes(Oatom v,Oz n) as f -> [],f + | Otimes(Oatom v,c) -> + let rec compute = function + | Oz n -> n + | Oplus(t1,t2) -> Bigint.add (compute t1) (compute t2) + | _ -> CErrors.user_err Pp.(str "condense.1") + in + [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c)) + | t -> oprint t; CErrors.user_err Pp.(str "reduce_factor.1") + +let rec condense p = function + | Oplus(f1,(Oplus(f2,r) as t)) -> + if Int.equal (weight f1) (weight f2) then begin + let shrink_tac,t = shrink_pair (P_APP 1 :: p) f1 f2 in + let assoc_tac = + clever_rewrite p + [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]] + (Lazy.force coq_fast_Zplus_assoc) in + let tac_list,t' = condense p (Oplus(t,r)) in + (assoc_tac :: shrink_tac :: tac_list), t' + end else begin + let tac,f = reduce_factor (P_APP 1 :: p) f1 in + let tac',t' = condense (P_APP 2 :: p) t in + (tac @ tac'), Oplus(f,t') + end + | Oplus(f1,Oz n) -> + let tac,f1' = reduce_factor (P_APP 1 :: p) f1 in tac,Oplus(f1',Oz n) + | Oplus(f1,f2) -> + if Int.equal (weight f1) (weight f2) then begin + let tac_shrink,t = shrink_pair p f1 f2 in + let tac,t' = condense p t in + tac_shrink :: tac,t' + end else begin + let tac,f = reduce_factor (P_APP 1 :: p) f1 in + let tac',t' = condense (P_APP 2 :: p) f2 in + (tac @ tac'),Oplus(f,t') + end + | Oz _ as t -> [],t + | t -> + let tac,t' = reduce_factor p t in + let final = Oplus(t',Oz zero) in + let tac' = clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor6) in + tac @ [tac'], final + +let rec clear_zero p = function + | Oplus(Otimes(Oatom v,Oz n),r) when n =? zero -> + let tac = + clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] + (Lazy.force coq_fast_Zred_factor5) in + let tac',t = clear_zero p r in + tac :: tac',t + | Oplus(f,r) -> + let tac,t = clear_zero (P_APP 2 :: p) r in tac,Oplus(f,t) + | t -> [],t + +let replay_history tactic_normalisation = + let aux = Id.of_string "auxiliary" in + let aux1 = Id.of_string "auxiliary_1" in + let aux2 = Id.of_string "auxiliary_2" in + let izero = mk_integer zero in + let rec loop t : unit Proofview.tactic = + match t with + | HYP e :: l -> + begin + try + tclTHEN + (Id.List.assoc (hyp_of_tag e.id) tactic_normalisation) + (loop l) + with Not_found -> loop l end + | NEGATE_CONTRADICT (e2,e1,b) :: l -> + let eq1 = decompile e1 + and eq2 = decompile e2 in + let id1 = hyp_of_tag e1.id + and id2 = hyp_of_tag e2.id in + let k = if b then negone else one in + let p_initial = [P_APP 1;P_TYPE] in + let tac= shuffle_mult_right p_initial e1.body k e2.body in + tclTHENLIST [ + generalize_tac + [mkApp (Lazy.force coq_OMEGA17, [| + val_of eq1; + val_of eq2; + mk_integer k; + mkVar id1; mkVar id2 |])]; + mk_then tac; + (intros_using [aux]); + resolve_id aux; + reflexivity + ] + | CONTRADICTION (e1,e2) :: l -> + let eq1 = decompile e1 + and eq2 = decompile e2 in + let p_initial = [P_APP 2;P_TYPE] in + let tac = shuffle_cancel p_initial e1.body in + let solve_le = + let not_sup_sup = mkApp (Lazy.force coq_eq, + [| + Lazy.force coq_comparison; + Lazy.force coq_Gt; + Lazy.force coq_Gt |]) + in + tclTHENS + (tclTHENLIST [ + unfold sp_Zle; + simpl_in_concl; + intro; + (absurd not_sup_sup) ]) + [ assumption ; reflexivity ] + in + let theorem = + mkApp (Lazy.force coq_OMEGA2, [| + val_of eq1; val_of eq2; + mkVar (hyp_of_tag e1.id); + mkVar (hyp_of_tag e2.id) |]) + in + Proofview.tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) solve_le + | DIVIDE_AND_APPROX (e1,e2,k,d) :: l -> + let id = hyp_of_tag e1.id in + let eq1 = val_of(decompile e1) + and eq2 = val_of(decompile e2) in + let kk = mk_integer k + and dd = mk_integer d in + let rhs = mk_plus (mk_times eq2 kk) dd in + let state_eg = mk_eq eq1 rhs in + let tac = scalar_norm_add [P_APP 3] e2.body in + tclTHENS + (cut state_eg) + [ tclTHENS + (tclTHENLIST [ + (intros_using [aux]); + (generalize_tac + [mkApp (Lazy.force coq_OMEGA1, + [| eq1; rhs; mkVar aux; mkVar id |])]); + (clear [aux;id]); + (intros_using [id]); + (cut (mk_gt kk dd)) ]) + [ tclTHENS + (cut (mk_gt kk izero)) + [ tclTHENLIST [ + (intros_using [aux1; aux2]); + (generalize_tac + [mkApp (Lazy.force coq_Zmult_le_approx, + [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]); + (clear [aux1;aux2;id]); + (intros_using [id]); + (loop l) ]; + tclTHENLIST [ + (unfold sp_Zgt); + simpl_in_concl; + reflexivity ] ]; + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] + ]; + tclTHEN (mk_then tac) reflexivity ] + + | NOT_EXACT_DIVIDE (e1,k) :: l -> + let c = floor_div e1.constant k in + let d = Bigint.sub e1.constant (Bigint.mult c k) in + let e2 = {id=e1.id; kind=EQUA;constant = c; + body = map_eq_linear (fun c -> c / k) e1.body } in + let eq2 = val_of(decompile e2) in + let kk = mk_integer k + and dd = mk_integer d in + let tac = scalar_norm_add [P_APP 2] e2.body in + tclTHENS + (cut (mk_gt dd izero)) + [ tclTHENS (cut (mk_gt kk dd)) + [tclTHENLIST [ + (intros_using [aux2;aux1]); + (generalize_tac + [mkApp (Lazy.force coq_OMEGA4, + [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]); + (clear [aux1;aux2]); + unfold sp_not; + (intros_using [aux]); + resolve_id aux; + mk_then tac; + assumption ] ; + tclTHENLIST [ + unfold sp_Zgt; + simpl_in_concl; + reflexivity ] ]; + tclTHENLIST [ + unfold sp_Zgt; + simpl_in_concl; + reflexivity ] ] + | EXACT_DIVIDE (e1,k) :: l -> + let id = hyp_of_tag e1.id in + let e2 = map_eq_afine (fun c -> c / k) e1 in + let eq1 = val_of(decompile e1) + and eq2 = val_of(decompile e2) in + let kk = mk_integer k in + let state_eq = mk_eq eq1 (mk_times eq2 kk) in + if e1.kind == DISE then + let tac = scalar_norm [P_APP 3] e2.body in + tclTHENS + (cut state_eq) + [tclTHENLIST [ + (intros_using [aux1]); + (generalize_tac + [mkApp (Lazy.force coq_OMEGA18, + [| eq1;eq2;kk;mkVar aux1; mkVar id |])]); + (clear [aux1;id]); + (intros_using [id]); + (loop l) ]; + tclTHEN (mk_then tac) reflexivity ] + else + let tac = scalar_norm [P_APP 3] e2.body in + tclTHENS (cut state_eq) + [ + tclTHENS + (cut (mk_gt kk izero)) + [tclTHENLIST [ + (intros_using [aux2;aux1]); + (generalize_tac + [mkApp (Lazy.force coq_OMEGA3, + [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]); + (clear [aux1;aux2;id]); + (intros_using [id]); + (loop l) ]; + tclTHENLIST [ + unfold sp_Zgt; + simpl_in_concl; + reflexivity ] ]; + tclTHEN (mk_then tac) reflexivity ] + | (MERGE_EQ(e3,e1,e2)) :: l -> + let id = new_identifier () in + tag_hypothesis id e3; + let id1 = hyp_of_tag e1.id + and id2 = hyp_of_tag e2 in + let eq1 = val_of(decompile e1) + and eq2 = val_of (decompile (negate_eq e1)) in + let tac = + clever_rewrite [P_APP 3] [[P_APP 1]] + (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: + scalar_norm [P_APP 3] e1.body + in + tclTHENS + (cut (mk_eq eq1 (mk_inv eq2))) + [tclTHENLIST [ + (intros_using [aux]); + (generalize_tac [mkApp (Lazy.force coq_OMEGA8, + [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]); + (clear [id1;id2;aux]); + (intros_using [id]); + (loop l) ]; + tclTHEN (mk_then tac) reflexivity] + + | STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l -> + let id = new_identifier () + and id2 = hyp_of_tag orig.id in + tag_hypothesis id e.id; + let eq1 = val_of(decompile def) + and eq2 = val_of(decompile orig) in + let vid = unintern_id v in + let theorem = + mkApp (Lazy.force coq_ex, [| + Lazy.force coq_Z; + mkLambda + (make_annot (Name vid) Sorts.Relevant, + Lazy.force coq_Z, + mk_eq (mkRel 1) eq1) |]) + in + let mm = mk_integer m in + let p_initial = [P_APP 2;P_TYPE] in + let tac = + clever_rewrite (P_APP 1 :: P_APP 1 :: P_APP 2 :: p_initial) + [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: + shuffle_mult_right p_initial + orig.body m ({c= negone;v= v}::def.body) in + tclTHENS + (cut theorem) + [tclTHENLIST [ + (intros_using [aux]); + (elim_id aux); + (clear [aux]); + (intros_using [vid; aux]); + (generalize_tac + [mkApp (Lazy.force coq_OMEGA9, + [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]); + mk_then tac; + (clear [aux]); + (intros_using [id]); + (loop l) ]; + tclTHEN (exists_tac eq1) reflexivity ] + | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> + let id1 = new_identifier () + and id2 = new_identifier () in + tag_hypothesis id1 e1; tag_hypothesis id2 e2; + let id = hyp_of_tag e.id in + let tac1 = norm_add [P_APP 2;P_TYPE] e.body in + let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in + let eq = val_of(decompile e) in + tclTHENS + (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id]))) + [tclTHENLIST [ mk_then tac1; (intros_using [id1]); (loop act1) ]; + tclTHENLIST [ mk_then tac2; (intros_using [id2]); (loop act2) ]] + | SUM(e3,(k1,e1),(k2,e2)) :: l -> + let id = new_identifier () in + tag_hypothesis id e3; + let id1 = hyp_of_tag e1.id + and id2 = hyp_of_tag e2.id in + let eq1 = val_of(decompile e1) + and eq2 = val_of(decompile e2) in + if k1 =? one && e2.kind == EQUA then + let tac_thm = + match e1.kind with + | EQUA -> Lazy.force coq_OMEGA5 + | INEQ -> Lazy.force coq_OMEGA6 + | DISE -> Lazy.force coq_OMEGA20 + in + let kk = mk_integer k2 in + let p_initial = + if e1.kind == DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in + let tac = shuffle_mult_right p_initial e1.body k2 e2.body in + tclTHENLIST [ + (generalize_tac + [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]); + mk_then tac; + (intros_using [id]); + (loop l) + ] + else + let kk1 = mk_integer k1 + and kk2 = mk_integer k2 in + let p_initial = [P_APP 2;P_TYPE] in + let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in + tclTHENS (cut (mk_gt kk1 izero)) + [tclTHENS + (cut (mk_gt kk2 izero)) + [tclTHENLIST [ + (intros_using [aux2;aux1]); + (generalize_tac + [mkApp (Lazy.force coq_OMEGA7, [| + eq1;eq2;kk1;kk2; + mkVar aux1;mkVar aux2; + mkVar id1;mkVar id2 |])]); + (clear [aux1;aux2]); + mk_then tac; + (intros_using [id]); + (loop l) ]; + tclTHENLIST [ + unfold sp_Zgt; + simpl_in_concl; + reflexivity ] ]; + tclTHENLIST [ + unfold sp_Zgt; + simpl_in_concl; + reflexivity ] ] + | CONSTANT_NOT_NUL(e,k) :: l -> + tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl + | CONSTANT_NUL(e) :: l -> + tclTHEN (resolve_id (hyp_of_tag e)) reflexivity + | CONSTANT_NEG(e,k) :: l -> + tclTHENLIST [ + (generalize_tac [mkVar (hyp_of_tag e)]); + unfold sp_Zle; + simpl_in_concl; + unfold sp_not; + (intros_using [aux]); + resolve_id aux; + reflexivity + ] + | _ -> Proofview.tclUNIT () + in + loop + +let normalize sigma p_initial t = + let (tac,t') = transform sigma p_initial t in + let (tac',t'') = condense p_initial t' in + let (tac'',t''') = clear_zero p_initial t'' in + tac @ tac' @ tac'' , t''' + +let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) = + let p_initial = [P_APP pos ;P_TYPE] in + let (tac,t') = normalize sigma p_initial t in + let shift_left = + tclTHEN + (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]) + (tclTRY (clear [id])) + in + if not (List.is_empty tac) then + let id' = new_identifier () in + ((id',(tclTHENLIST [ shift_left; mk_then tac; (intros_using [id']) ])) + :: tactic, + compile id' flag t' :: defs) + else + (tactic,defs) + +let destructure_omega env sigma tac_def (id,c) = + if String.equal (atompart_of_id id) "State" then + tac_def + else + try match destructurate_prop sigma c with + | Kapp(Eq,[typ;t1;t2]) + when begin match destructurate_type env sigma typ with Kapp(Z,[]) -> true | _ -> false end -> + let t = mk_plus t1 (mk_inv t2) in + normalize_equation sigma + id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def + | Kapp(Zne,[t1;t2]) -> + let t = mk_plus t1 (mk_inv t2) in + normalize_equation sigma + id DISE (Lazy.force coq_Zne_left) 1 t t1 t2 tac_def + | Kapp(Zle,[t1;t2]) -> + let t = mk_plus t2 (mk_inv t1) in + normalize_equation sigma + id INEQ (Lazy.force coq_Zle_left) 2 t t1 t2 tac_def + | Kapp(Zlt,[t1;t2]) -> + let t = mk_plus (mk_plus t2 (mk_integer negone)) (mk_inv t1) in + normalize_equation sigma + id INEQ (Lazy.force coq_Zlt_left) 2 t t1 t2 tac_def + | Kapp(Zge,[t1;t2]) -> + let t = mk_plus t1 (mk_inv t2) in + normalize_equation sigma + id INEQ (Lazy.force coq_Zge_left) 2 t t1 t2 tac_def + | Kapp(Zgt,[t1;t2]) -> + let t = mk_plus (mk_plus t1 (mk_integer negone)) (mk_inv t2) in + normalize_equation sigma + id INEQ (Lazy.force coq_Zgt_left) 2 t t1 t2 tac_def + | _ -> tac_def + with e when catchable_exception e -> tac_def + +let reintroduce id = + (* [id] cannot be cleared if dependent: protect it by a try *) + tclTHEN (tclTRY (clear [id])) (intro_using id) + + +open Proofview.Notations + +let coq_omega = + Proofview.Goal.enter begin fun gl -> + clear_constr_tables (); + let hyps_types = Tacmach.New.pf_hyps_types gl in + let destructure_omega = Tacmach.New.pf_apply destructure_omega gl in + let tactic_normalisation, system = + List.fold_left destructure_omega ([],[]) hyps_types in + let prelude,sys = + List.fold_left + (fun (tac,sys) (t,(v,th,b)) -> + if b then + let id = new_identifier () in + let i = new_id () in + tag_hypothesis id i; + (tclTHENLIST [ + (simplest_elim (applist (Lazy.force coq_intro_Z, [t]))); + (intros_using [v; id]); + (elim_id id); + (clear [id]); + (intros_using [th;id]); + tac ]), + {kind = INEQ; + body = [{v=intern_id v; c=one}]; + constant = zero; id = i} :: sys + else + (tclTHENLIST [ + (simplest_elim (applist (Lazy.force coq_new_var, [t]))); + (intros_using [v;th]); + tac ]), + sys) + (Proofview.tclUNIT (),[]) (dump_tables ()) + in + let system = system @ sys in + if !display_system_flag then display_system display_var system; + if !old_style_flag then begin + try + let _ = simplify (new_id,new_var_num,display_var) false system in + Proofview.tclUNIT () + with UNSOLVABLE -> + let _,path = depend [] [] (history ()) in + if !display_action_flag then display_action display_var path; + (tclTHEN prelude (replay_history tactic_normalisation path)) + end else begin + try + let path = simplify_strong (new_id,new_var_num,display_var) system in + if !display_action_flag then display_action display_var path; + tclTHEN prelude (replay_history tactic_normalisation path) + with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system") + end + end + +let coq_omega = coq_omega + +let nat_inject = + Proofview.Goal.enter begin fun gl -> + let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in + let rec explore p t : unit Proofview.tactic = + Proofview.tclEVARMAP >>= fun sigma -> + try match destructurate_term sigma t with + | Kapp(Plus,[t1;t2]) -> + tclTHENLIST [ + (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2)) + ((Lazy.force coq_inj_plus),[t1;t2])); + (explore (P_APP 1 :: p) t1); + (explore (P_APP 2 :: p) t2) + ] + | Kapp(Mult,[t1;t2]) -> + tclTHENLIST [ + (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2)) + ((Lazy.force coq_inj_mult),[t1;t2])); + (explore (P_APP 1 :: p) t1); + (explore (P_APP 2 :: p) t2) + ] + | Kapp(Minus,[t1;t2]) -> + let id = new_identifier () in + tclTHENS + (tclTHEN + (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1]))) + (intros_using [id])) + [ + tclTHENLIST [ + (clever_rewrite_gen p + (mk_minus (mk_inj t1) (mk_inj t2)) + ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id])); + (loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]); + (explore (P_APP 1 :: p) t1); + (explore (P_APP 2 :: p) t2) ]; + (tclTHEN + (clever_rewrite_gen p (mk_integer zero) + ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id])) + (loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])])) + ] + | Kapp(S,[t']) -> + let rec is_number t = + try match destructurate_term sigma t with + Kapp(S,[t]) -> is_number t + | Kapp(O,[]) -> true + | _ -> false + with e when catchable_exception e -> false + in + let rec loop p t : unit Proofview.tactic = + try match destructurate_term sigma t with + Kapp(S,[t]) -> + (tclTHEN + (clever_rewrite_gen p + (mkApp (Lazy.force coq_Zsucc, [| mk_inj t |])) + ((Lazy.force coq_inj_S),[t])) + (loop (P_APP 1 :: p) t)) + | _ -> explore p t + with e when catchable_exception e -> explore p t + in + if is_number t' then focused_simpl p else loop p t + | Kapp(Pred,[t]) -> + let t_minus_one = + mkApp (Lazy.force coq_minus, [| t; + mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in + tclTHEN + (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one + ((Lazy.force coq_pred_of_minus),[t])) + (explore p t_minus_one) + | Kapp(O,[]) -> focused_simpl p + | _ -> Proofview.tclUNIT () + with e when catchable_exception e -> Proofview.tclUNIT () + + and loop = function + | [] -> Proofview.tclUNIT () + | (i,t)::lit -> + Proofview.tclEVARMAP >>= fun sigma -> + begin try match destructurate_prop sigma t with + Kapp(Le,[t1;t2]) -> + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]); + (explore [P_APP 1; P_TYPE] t1); + (explore [P_APP 2; P_TYPE] t2); + (reintroduce i); + (loop lit) + ] + | Kapp(Lt,[t1;t2]) -> + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]); + (explore [P_APP 1; P_TYPE] t1); + (explore [P_APP 2; P_TYPE] t2); + (reintroduce i); + (loop lit) + ] + | Kapp(Ge,[t1;t2]) -> + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]); + (explore [P_APP 1; P_TYPE] t1); + (explore [P_APP 2; P_TYPE] t2); + (reintroduce i); + (loop lit) + ] + | Kapp(Gt,[t1;t2]) -> + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]); + (explore [P_APP 1; P_TYPE] t1); + (explore [P_APP 2; P_TYPE] t2); + (reintroduce i); + (loop lit) + ] + | Kapp(Neq,[t1;t2]) -> + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]); + (explore [P_APP 1; P_TYPE] t1); + (explore [P_APP 2; P_TYPE] t2); + (reintroduce i); + (loop lit) + ] + | Kapp(Eq,[typ;t1;t2]) -> + if is_conv typ (Lazy.force coq_nat) then + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]); + (explore [P_APP 2; P_TYPE] t1); + (explore [P_APP 3; P_TYPE] t2); + (reintroduce i); + (loop lit) + ] + else loop lit + | _ -> loop lit + with e when catchable_exception e -> loop lit end + in + let hyps_types = Tacmach.New.pf_hyps_types gl in + loop (List.rev hyps_types) + end + +let dec_binop = function + | Zne -> coq_dec_Zne + | Zle -> coq_dec_Zle + | Zlt -> coq_dec_Zlt + | Zge -> coq_dec_Zge + | Zgt -> coq_dec_Zgt + | Le -> coq_dec_le + | Lt -> coq_dec_lt + | Ge -> coq_dec_ge + | Gt -> coq_dec_gt + | _ -> raise Not_found + +let not_binop = function + | Zne -> coq_not_Zne + | Zle -> coq_Znot_le_gt + | Zlt -> coq_Znot_lt_ge + | Zge -> coq_Znot_ge_lt + | Zgt -> coq_Znot_gt_le + | Le -> coq_not_le + | Lt -> coq_not_lt + | Ge -> coq_not_ge + | Gt -> coq_not_gt + | _ -> raise Not_found + +(** A decidability check : for some [t], could we build a term + of type [decidable t] (i.e. [t\/~t]) ? Otherwise, we raise + [Undecidable]. Note that a successful check implies that + [t] has type Prop. +*) + +exception Undecidable + +let rec decidability env sigma t = + match destructurate_prop sigma t with + | Kapp(Or,[t1;t2]) -> + mkApp (Lazy.force coq_dec_or, [| t1; t2; + decidability env sigma t1; decidability env sigma t2 |]) + | Kapp(And,[t1;t2]) -> + mkApp (Lazy.force coq_dec_and, [| t1; t2; + decidability env sigma t1; decidability env sigma t2 |]) + | Kapp(Iff,[t1;t2]) -> + mkApp (Lazy.force coq_dec_iff, [| t1; t2; + decidability env sigma t1; decidability env sigma t2 |]) + | Kimp(t1,t2) -> + (* This is the only situation where it's not obvious that [t] + is in Prop. The recursive call on [t2] will ensure that. *) + mkApp (Lazy.force coq_dec_imp, + [| t1; t2; decidability env sigma t1; decidability env sigma t2 |]) + | Kapp(Not,[t1]) -> + mkApp (Lazy.force coq_dec_not, [| t1; decidability env sigma t1 |]) + | Kapp(Eq,[typ;t1;t2]) -> + begin match destructurate_type env sigma typ with + | Kapp(Z,[]) -> mkApp (Lazy.force coq_dec_eq, [| t1;t2 |]) + | Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |]) + | _ -> raise Undecidable + end + | Kapp(op,[t1;t2]) -> + (try mkApp (Lazy.force (dec_binop op), [| t1; t2 |]) + with Not_found -> raise Undecidable) + | Kapp(False,[]) -> Lazy.force coq_dec_False + | Kapp(True,[]) -> Lazy.force coq_dec_True + | _ -> raise Undecidable + +let fresh_id avoid id gl = + fresh_id_in_env avoid id (Proofview.Goal.env gl) + +let onClearedName id tac = + (* We cannot ensure that hyps can be cleared (because of dependencies), *) + (* so renaming may be necessary *) + tclTHEN + (tclTRY (clear [id])) + (Proofview.Goal.enter begin fun gl -> + let id = fresh_id Id.Set.empty id gl in + tclTHEN (introduction id) (tac id) + end) + +let onClearedName2 id tac = + tclTHEN + (tclTRY (clear [id])) + (Proofview.Goal.enter begin fun gl -> + let id1 = fresh_id Id.Set.empty (add_suffix id "_left") gl in + let id2 = fresh_id Id.Set.empty (add_suffix id "_right") gl in + tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] + end) + +let destructure_hyps = + Proofview.Goal.enter begin fun gl -> + let type_of = Tacmach.New.pf_unsafe_type_of gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let decidability = decidability env sigma in + let rec loop = function + | [] -> (tclTHEN nat_inject coq_omega) + | LocalDef (i,body,typ) :: lit when !letin_flag -> + Proofview.tclEVARMAP >>= fun sigma -> + begin + try + match destructurate_type env sigma typ with + | Kapp(Nat,_) | Kapp(Z,_) -> + let hid = fresh_id Id.Set.empty (add_suffix i.binder_name "_eqn") gl in + let hty = mk_gen_eq typ (mkVar i.binder_name) body in + tclTHEN + (assert_by (Name hid) hty reflexivity) + (loop (LocalAssum (make_annot hid Sorts.Relevant, hty) :: lit)) + | _ -> loop lit + with e when catchable_exception e -> loop lit + end + | decl :: lit -> (* variable without body (or !letin_flag isn't set) *) + let i = NamedDecl.get_id decl in + Proofview.tclEVARMAP >>= fun sigma -> + begin try match destructurate_prop sigma (NamedDecl.get_type decl) with + | Kapp(False,[]) -> elim_id i + | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit + | Kapp(Or,[t1;t2]) -> + (tclTHENS + (elim_id i) + [ onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t1)::lit))); + onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t2)::lit))) ]) + | Kapp(And,[t1;t2]) -> + tclTHEN + (elim_id i) + (onClearedName2 i (fun i1 i2 -> + loop (LocalAssum (make_annot i1 Sorts.Relevant,t1) :: + LocalAssum (make_annot i2 Sorts.Relevant,t2) :: lit))) + | Kapp(Iff,[t1;t2]) -> + tclTHEN + (elim_id i) + (onClearedName2 i (fun i1 i2 -> + loop (LocalAssum (make_annot i1 Sorts.Relevant,mkArrow t1 Sorts.Relevant t2) :: + LocalAssum (make_annot i2 Sorts.Relevant,mkArrow t2 Sorts.Relevant t1) :: lit))) + | Kimp(t1,t2) -> + (* t1 and t2 might be in Type rather than Prop. + For t1, the decidability check will ensure being Prop. *) + if Termops.is_Prop sigma (type_of t2) + then + let d1 = decidability t1 in + tclTHENLIST [ + (generalize_tac [mkApp (Lazy.force coq_imp_simp, + [| t1; t2; d1; mkVar i|])]); + (onClearedName i (fun i -> + (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_not t1) t2) :: lit)))) + ] + else + loop lit + | Kapp(Not,[t]) -> + begin match destructurate_prop sigma t with + Kapp(Or,[t1;t2]) -> + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); + (onClearedName i (fun i -> + (loop (LocalAssum (make_annot i Sorts.Relevant,mk_and (mk_not t1) (mk_not t2)) :: lit)))) + ] + | Kapp(And,[t1;t2]) -> + let d1 = decidability t1 in + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_not_and, + [| t1; t2; d1; mkVar i |])]); + (onClearedName i (fun i -> + (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_not t1) (mk_not t2)) :: lit)))) + ] + | Kapp(Iff,[t1;t2]) -> + let d1 = decidability t1 in + let d2 = decidability t2 in + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_not_iff, + [| t1; t2; d1; d2; mkVar i |])]); + (onClearedName i (fun i -> + (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_and t1 (mk_not t2)) + (mk_and (mk_not t1) t2)) :: lit)))) + ] + | Kimp(t1,t2) -> + (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok. + For t1, being decidable implies being Prop. *) + let d1 = decidability t1 in + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_not_imp, + [| t1; t2; d1; mkVar i |])]); + (onClearedName i (fun i -> + (loop (LocalAssum (make_annot i Sorts.Relevant,mk_and t1 (mk_not t2)) :: lit)))) + ] + | Kapp(Not,[t]) -> + let d = decidability t in + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); + (onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t) :: lit)))) + ] + | Kapp(op,[t1;t2]) -> + (try + let thm = not_binop op in + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]); + (onClearedName i (fun _ -> loop lit)) + ] + with Not_found -> loop lit) + | Kapp(Eq,[typ;t1;t2]) -> + if !old_style_flag then begin + match destructurate_type env sigma typ with + | Kapp(Nat,_) -> + tclTHENLIST [ + (simplest_elim + (mkApp + (Lazy.force coq_not_eq, [|t1;t2;mkVar i|]))); + (onClearedName i (fun _ -> loop lit)) + ] + | Kapp(Z,_) -> + tclTHENLIST [ + (simplest_elim + (mkApp + (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|]))); + (onClearedName i (fun _ -> loop lit)) + ] + | _ -> loop lit + end else begin + match destructurate_type env sigma typ with + | Kapp(Nat,_) -> + (tclTHEN + (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) + decl)) + (loop lit)) + | Kapp(Z,_) -> + (tclTHEN + (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) + decl)) + (loop lit)) + | _ -> loop lit + end + | _ -> loop lit + end + | _ -> loop lit + with + | Undecidable -> loop lit + | e when catchable_exception e -> loop lit + end + in + let hyps = Proofview.Goal.hyps gl in + loop hyps + end + +let destructure_goal = + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let decidability = decidability env sigma in + let rec loop t = + Proofview.tclEVARMAP >>= fun sigma -> + let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in + Proofview.V82.wrap_exceptions prop >>= fun prop -> + match prop with + | Kapp(Not,[t]) -> + (tclTHEN + (tclTHEN (unfold sp_not) intro) + destructure_hyps) + | Kimp(a,b) -> (tclTHEN intro (loop b)) + | Kapp(False,[]) -> destructure_hyps + | _ -> + let goal_tac = + try + let dec = decidability t in + tclTHEN + (Proofview.Goal.enter begin fun gl -> + refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |])) + end) + intro + with Undecidable -> Tactics.elim_type (Lazy.force coq_False) + | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + in + tclTHEN goal_tac destructure_hyps + in + (loop concl) + end + +let destructure_goal = destructure_goal + +let omega_solver = + Proofview.tclUNIT () >>= fun () -> (* delay for [check_required_library] *) + Coqlib.check_required_library ["Coq";"omega";"Omega"]; + reset_all (); + destructure_goal diff --git a/plugins/omega/coq_omega.mli b/plugins/omega/coq_omega.mli new file mode 100644 index 0000000000..a657826caa --- /dev/null +++ b/plugins/omega/coq_omega.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val omega_solver : unit Proofview.tactic diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg new file mode 100644 index 0000000000..85081b24a3 --- /dev/null +++ b/plugins/omega/g_omega.mlg @@ -0,0 +1,59 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(**************************************************************************) +(* *) +(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) +(* *) +(* Pierre Crégut (CNET, Lannion, France) *) +(* *) +(**************************************************************************) + + +DECLARE PLUGIN "omega_plugin" + +{ + +open Ltac_plugin +open Names +open Coq_omega +open Stdarg + +let eval_tactic name = + let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in + let kn = KerName.make (ModPath.MPfile dp) (Label.make name) in + let tac = Tacenv.interp_ltac kn in + Tacinterp.eval_tactic tac + +let omega_tactic l = + let tacs = List.map + (function + | "nat" -> eval_tactic "zify_nat" + | "positive" -> eval_tactic "zify_positive" + | "N" -> eval_tactic "zify_N" + | "Z" -> eval_tactic "zify_op" + | s -> CErrors.user_err Pp.(str ("No Omega knowledge base for type "^s))) + (Util.List.sort_uniquize String.compare l) + in + Tacticals.New.tclTHEN + (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs)) + (omega_solver) + +} + +TACTIC EXTEND omega +| [ "omega" ] -> { omega_tactic [] } +END + +TACTIC EXTEND omega' +| [ "omega" "with" ne_ident_list(l) ] -> + { omega_tactic (List.map Names.Id.to_string l) } +| [ "omega" "with" "*" ] -> { omega_tactic ["nat";"positive";"N";"Z"] } +END + diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml new file mode 100644 index 0000000000..7bca7c7099 --- /dev/null +++ b/plugins/omega/omega.ml @@ -0,0 +1,708 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(**************************************************************************) +(* *) +(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) +(* *) +(* Pierre Crégut (CNET, Lannion, France) *) +(* *) +(* 13/10/2002 : modified to cope with an external numbering of equations *) +(* and hypothesis. Its use for Omega is not more complex and it makes *) +(* things much simpler for the reflexive version where we should limit *) +(* the number of source of numbering. *) +(**************************************************************************) + +module type INT = sig + type bigint + val equal : bigint -> bigint -> bool + val less_than : bigint -> bigint -> bool + val add : bigint -> bigint -> bigint + val sub : bigint -> bigint -> bigint + val mult : bigint -> bigint -> bigint + val euclid : bigint -> bigint -> bigint * bigint + val neg : bigint -> bigint + val zero : bigint + val one : bigint + val to_string : bigint -> string +end + +let debug = ref false + +module MakeOmegaSolver (I:INT) = struct + +type bigint = I.bigint +let (=?) = I.equal +let (<?) = I.less_than +let (<=?) x y = I.less_than x y || x = y +let (>?) x y = I.less_than y x +let (>=?) x y = I.less_than y x || x = y +let (+) = I.add +let (-) = I.sub +let ( * ) = I.mult +let (/) x y = fst (I.euclid x y) +let (mod) x y = snd (I.euclid x y) +let zero = I.zero +let one = I.one +let two = one + one +let negone = I.neg one +let abs x = if I.less_than x zero then I.neg x else x +let string_of_bigint = I.to_string +let neg = I.neg + +(* To ensure that polymorphic (<) is not used mistakenly on big integers *) +(* Warning: do not use (=) either on big int *) +let (<) = ((<) : int -> int -> bool) +let (>) = ((>) : int -> int -> bool) +let (<=) = ((<=) : int -> int -> bool) +let (>=) = ((>=) : int -> int -> bool) + +let pp i = print_int i; print_newline (); flush stdout + +let push v l = l := v :: !l + +let rec pgcd x y = if y =? zero then x else pgcd y (x mod y) + +let pgcd_l = function + | [] -> failwith "pgcd_l" + | x :: l -> List.fold_left pgcd x l + +let floor_div a b = + match a >=? zero , b >? zero with + | true,true -> a / b + | false,false -> a / b + | true, false -> (a-one) / b - one + | false,true -> (a+one) / b - one + +type coeff = {c: bigint ; v: int} + +type linear = coeff list + +type eqn_kind = EQUA | INEQ | DISE + +type afine = { + (* a number uniquely identifying the equation *) + id: int ; + (* a boolean true for an eq, false for an ineq (Sigma a_i x_i >= 0) *) + kind: eqn_kind; + (* the variables and their coefficient *) + body: coeff list; + (* a constant *) + constant: bigint } + +type state_action = { + st_new_eq : afine; + st_def : afine; (* /!\ this represents [st_def = st_var] *) + st_orig : afine; + st_coef : bigint; + st_var : int } + +type action = + | DIVIDE_AND_APPROX of afine * afine * bigint * bigint + | NOT_EXACT_DIVIDE of afine * bigint + | FORGET_C of int + | EXACT_DIVIDE of afine * bigint + | SUM of int * (bigint * afine) * (bigint * afine) + | STATE of state_action + | HYP of afine + | FORGET of int * int + | FORGET_I of int * int + | CONTRADICTION of afine * afine + | NEGATE_CONTRADICT of afine * afine * bool + | MERGE_EQ of int * afine * int + | CONSTANT_NOT_NUL of int * bigint + | CONSTANT_NUL of int + | CONSTANT_NEG of int * bigint + | SPLIT_INEQ of afine * (int * action list) * (int * action list) + | WEAKEN of int * bigint + +exception UNSOLVABLE + +exception NO_CONTRADICTION + +let display_eq print_var (l,e) = + let _ = + List.fold_left + (fun not_first f -> + print_string + (if f.c <? zero then "- " else if not_first then "+ " else ""); + let c = abs f.c in + if c =? one then + Printf.printf "%s " (print_var f.v) + else + Printf.printf "%s %s " (string_of_bigint c) (print_var f.v); + true) + false l + in + if e >? zero then + Printf.printf "+ %s " (string_of_bigint e) + else if e <? zero then + Printf.printf "- %s " (string_of_bigint (abs e)) + +let rec trace_length l = + let action_length accu = function + | SPLIT_INEQ (_,(_,l1),(_,l2)) -> + accu + one + trace_length l1 + trace_length l2 + | _ -> accu + one in + List.fold_left action_length zero l + +let operator_of_eq = function + | EQUA -> "=" | DISE -> "!=" | INEQ -> ">=" + +let kind_of = function + | EQUA -> "equation" | DISE -> "disequation" | INEQ -> "inequation" + +let display_system print_var l = + List.iter + (fun { kind=b; body=e; constant=c; id=id} -> + Printf.printf "E%d: " id; + display_eq print_var (e,c); + Printf.printf "%s 0\n" (operator_of_eq b)) + l; + print_string "------------------------\n\n" + +let display_inequations print_var l = + List.iter (fun e -> display_eq print_var e;print_string ">= 0\n") l; + print_string "------------------------\n\n" + +let sbi = string_of_bigint + +let rec display_action print_var = function + | act :: l -> begin match act with + | DIVIDE_AND_APPROX (e1,e2,k,d) -> + Printf.printf + "Inequation E%d is divided by %s and the constant coefficient is \ + rounded by subtracting %s.\n" e1.id (sbi k) (sbi d) + | NOT_EXACT_DIVIDE (e,k) -> + Printf.printf + "Constant in equation E%d is not divisible by the pgcd \ + %s of its other coefficients.\n" e.id (sbi k) + | EXACT_DIVIDE (e,k) -> + Printf.printf + "Equation E%d is divided by the pgcd \ + %s of its coefficients.\n" e.id (sbi k) + | WEAKEN (e,k) -> + Printf.printf + "To ensure a solution in the dark shadow \ + the equation E%d is weakened by %s.\n" e (sbi k) + | SUM (e,(c1,e1),(c2,e2)) -> + Printf.printf + "We state %s E%d = %s %s E%d + %s %s E%d.\n" + (kind_of e1.kind) e (sbi c1) (kind_of e1.kind) e1.id (sbi c2) + (kind_of e2.kind) e2.id + | STATE { st_new_eq = e } -> + Printf.printf "We define a new equation E%d: " e.id; + display_eq print_var (e.body,e.constant); + print_string (operator_of_eq e.kind); print_string " 0" + | HYP e -> + Printf.printf "We define E%d: " e.id; + display_eq print_var (e.body,e.constant); + print_string (operator_of_eq e.kind); print_string " 0\n" + | FORGET_C e -> Printf.printf "E%d is trivially satisfiable.\n" e + | FORGET (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2 + | FORGET_I (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2 + | MERGE_EQ (e,e1,e2) -> + Printf.printf "E%d and E%d can be merged into E%d.\n" e1.id e2 e + | CONTRADICTION (e1,e2) -> + Printf.printf + "Equations E%d and E%d imply a contradiction on their \ + constant factors.\n" e1.id e2.id + | NEGATE_CONTRADICT(e1,e2,b) -> + Printf.printf + "Equations E%d and E%d state that their body is at the same time \ + equal and different\n" e1.id e2.id + | CONSTANT_NOT_NUL (e,k) -> + Printf.printf "Equation E%d states %s = 0.\n" e (sbi k) + | CONSTANT_NEG(e,k) -> + Printf.printf "Equation E%d states %s >= 0.\n" e (sbi k) + | CONSTANT_NUL e -> + Printf.printf "Inequation E%d states 0 != 0.\n" e + | SPLIT_INEQ (e,(e1,l1),(e2,l2)) -> + Printf.printf "Equation E%d is split in E%d and E%d\n\n" e.id e1 e2; + display_action print_var l1; + print_newline (); + display_action print_var l2; + print_newline () + end; display_action print_var l + | [] -> + flush stdout + +let default_print_var v = Printf.sprintf "X%d" v (* For debugging *) + +(*""*) +let add_event, history, clear_history = + let accu = ref [] in + (fun (v:action) -> if !debug then display_action default_print_var [v]; push v accu), + (fun () -> !accu), + (fun () -> accu := []) + +let nf_linear = List.sort (fun x y -> Pervasives.(-) y.v x.v) + +let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x)) + +let map_eq_linear f = + let rec loop = function + | x :: l -> let c = f x.c in if c=?zero then loop l else {v=x.v; c=c} :: loop l + | [] -> [] + in + loop + +let map_eq_afine f e = + { id = e.id; kind = e.kind; body = map_eq_linear f e.body; + constant = f e.constant } + +let negate_eq = map_eq_afine (fun x -> neg x) + +let rec sum p0 p1 = match (p0,p1) with + | ([], l) -> l | (l, []) -> l + | (((x1::l1) as l1'), ((x2::l2) as l2')) -> + if x1.v = x2.v then + let c = x1.c + x2.c in + if c =? zero then sum l1 l2 else {v=x1.v;c=c} :: sum l1 l2 + else if x1.v > x2.v then + x1 :: sum l1 l2' + else + x2 :: sum l1' l2 + +let sum_afine new_eq_id eq1 eq2 = + { kind = eq1.kind; id = new_eq_id (); + body = sum eq1.body eq2.body; constant = eq1.constant + eq2.constant } + +exception FACTOR1 + +let rec chop_factor_1 = function + | x :: l -> + if abs x.c =? one then x,l else let (c',l') = chop_factor_1 l in (c',x::l') + | [] -> raise FACTOR1 + +exception CHOPVAR + +let rec chop_var v = function + | f :: l -> if f.v = v then f,l else let (f',l') = chop_var v l in (f',f::l') + | [] -> raise CHOPVAR + +let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) = + if e = [] then begin + match eq_flag with + | EQUA -> + if x =? zero then [] else begin + add_event (CONSTANT_NOT_NUL(id,x)); raise UNSOLVABLE + end + | DISE -> + if x <> zero then [] else begin + add_event (CONSTANT_NUL id); raise UNSOLVABLE + end + | INEQ -> + if x >=? zero then [] else begin + add_event (CONSTANT_NEG(id,x)); raise UNSOLVABLE + end + end else + let gcd = pgcd_l (List.map (fun f -> abs f.c) e) in + if eq_flag=EQUA && x mod gcd <> zero then begin + add_event (NOT_EXACT_DIVIDE (eq,gcd)); raise UNSOLVABLE + end else if eq_flag=DISE && x mod gcd <> zero then begin + add_event (FORGET_C eq.id); [] + end else if gcd <> one then begin + let c = floor_div x gcd in + let d = x - c * gcd in + let new_eq = {id=id; kind=eq_flag; constant=c; + body=map_eq_linear (fun c -> c / gcd) e} in + add_event (if eq_flag=EQUA || eq_flag = DISE then EXACT_DIVIDE(eq,gcd) + else DIVIDE_AND_APPROX(eq,new_eq,gcd,d)); + [new_eq] + end else [eq] + +let eliminate_with_in new_eq_id {v=v;c=c_unite} eq2 + ({body=e1; constant=c1} as eq1) = + try + let (f,_) = chop_var v e1 in + let coeff = if c_unite=?one then neg f.c else if c_unite=? negone then f.c + else failwith "eliminate_with_in" in + let res = sum_afine new_eq_id eq1 (map_eq_afine (fun c -> c * coeff) eq2) in + add_event (SUM (res.id,(one,eq1),(coeff,eq2))); res + with CHOPVAR -> eq1 + +let omega_mod a b = a - b * floor_div (two * a + b) (two * b) +let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = + let e = original.body in + let sigma = new_var_id () in + if e == [] then begin + display_system print_var [original] ; failwith "TL" + end; + let smallest,var = + List.fold_left (fun (v,p) c -> if v >? (abs c.c) then abs c.c,c.v else (v,p)) + (abs (List.hd e).c, (List.hd e).v) (List.tl e) + in + let m = smallest + one in + let new_eq = + { constant = omega_mod original.constant m; + body = {c= neg m;v=sigma} :: + map_eq_linear (fun a -> omega_mod a m) original.body; + id = new_eq_id (); kind = EQUA } in + let definition = + { constant = neg (floor_div (two * original.constant + m) (two * m)); + body = map_eq_linear (fun a -> neg (floor_div (two * a + m) (two * m))) + original.body; + id = new_eq_id (); kind = EQUA } in + add_event (STATE {st_new_eq = new_eq; st_def = definition; + st_orig = original; st_coef = m; st_var = sigma}); + let new_eq = List.hd (normalize new_eq) in + let eliminated_var, def = chop_var var new_eq.body in + let other_equations = + Util.List.map_append + (fun e -> + normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l1 in + let inequations = + Util.List.map_append + (fun e -> + normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l2 in + let original' = eliminate_with_in new_eq_id eliminated_var new_eq original in + let mod_original = map_eq_afine (fun c -> c / m) original' in + add_event (EXACT_DIVIDE (original',m)); + List.hd (normalize mod_original),other_equations,inequations + +let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e,other,ineqs) = + if !debug then display_system print_var (e::other); + try + let v,def = chop_factor_1 e.body in + (Util.List.map_append + (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) other, + Util.List.map_append + (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) ineqs) + with FACTOR1 -> + eliminate_one_equation new_ids (banerjee_step new_ids e other ineqs) + +let rec banerjee ((_,_,print_var) as new_ids) (sys_eq,sys_ineq) = + let rec fst_eq_1 = function + (eq::l) -> + if List.exists (fun x -> abs x.c =? one) eq.body then eq,l + else let (eq',l') = fst_eq_1 l in (eq',eq::l') + | [] -> raise Not_found in + match sys_eq with + [] -> if !debug then display_system print_var sys_ineq; sys_ineq + | (e1::rest) -> + let eq,other = try fst_eq_1 sys_eq with Not_found -> (e1,rest) in + if eq.body = [] then + if eq.constant =? zero then begin + add_event (FORGET_C eq.id); banerjee new_ids (other,sys_ineq) + end else begin + add_event (CONSTANT_NOT_NUL(eq.id,eq.constant)); raise UNSOLVABLE + end + else + banerjee new_ids + (eliminate_one_equation new_ids (eq,other,sys_ineq)) + +type kind = INVERTED | NORMAL + +let redundancy_elimination new_eq_id system = + let normal = function + ({body=f::_} as e) when f.c <? zero -> negate_eq e, INVERTED + | e -> e,NORMAL in + let table = Hashtbl.create 7 in + List.iter + (fun e -> + let ({body=ne} as nx) ,kind = normal e in + if ne = [] then + if nx.constant <? zero then begin + add_event (CONSTANT_NEG(nx.id,nx.constant)); raise UNSOLVABLE + end else add_event (FORGET_C nx.id) + else + try + let (optnormal,optinvert) = Hashtbl.find table ne in + let final = + if kind = NORMAL then begin + match optnormal with + Some v -> + let kept = + if v.constant <? nx.constant + then begin add_event (FORGET (v.id,nx.id));v end + else begin add_event (FORGET (nx.id,v.id));nx end in + (Some(kept),optinvert) + | None -> Some nx,optinvert + end else begin + match optinvert with + Some v -> + let _kept = + if v.constant >? nx.constant + then begin add_event (FORGET_I (v.id,nx.id));v end + else begin add_event (FORGET_I (nx.id,v.id));nx end in + (optnormal,Some(if v.constant >? nx.constant then v else nx)) + | None -> optnormal,Some nx + end in + begin match final with + (Some high, Some low) -> + if high.constant <? low.constant then begin + add_event(CONTRADICTION (high,negate_eq low)); + raise UNSOLVABLE + end + | _ -> () end; + Hashtbl.remove table ne; + Hashtbl.add table ne final + with Not_found -> + Hashtbl.add table ne + (if kind = NORMAL then (Some nx,None) else (None,Some nx))) + system; + let accu_eq = ref [] in + let accu_ineq = ref [] in + Hashtbl.iter + (fun p0 p1 -> match (p0,p1) with + | (e, (Some x, Some y)) when x.constant =? y.constant -> + let id=new_eq_id () in + add_event (MERGE_EQ(id,x,y.id)); + push {id=id; kind=EQUA; body=x.body; constant=x.constant} accu_eq + | (e, (optnorm,optinvert)) -> + begin match optnorm with + Some x -> push x accu_ineq | _ -> () end; + begin match optinvert with + Some x -> push (negate_eq x) accu_ineq | _ -> () end) + table; + !accu_eq,!accu_ineq + +exception SOLVED_SYSTEM + +let select_variable system = + let table = Hashtbl.create 7 in + let push v c= + try let r = Hashtbl.find table v in r := max !r (abs c) + with Not_found -> Hashtbl.add table v (ref (abs c)) in + List.iter (fun {body=l} -> List.iter (fun f -> push f.v f.c) l) system; + let vmin,cmin = ref (-1), ref zero in + let var_cpt = ref 0 in + Hashtbl.iter + (fun v ({contents = c}) -> + incr var_cpt; + if c <? !cmin || !vmin = (-1) then begin vmin := v; cmin := c end) + table; + if !var_cpt < 1 then raise SOLVED_SYSTEM; + !vmin + +let classify v system = + List.fold_left + (fun (not_occ,below,over) eq -> + try let f,eq' = chop_var v eq.body in + if f.c >=? zero then (not_occ,((f.c,eq) :: below),over) + else (not_occ,below,((neg f.c,eq) :: over)) + with CHOPVAR -> (eq::not_occ,below,over)) + ([],[],[]) system + +let product new_eq_id dark_shadow low high = + List.fold_left + (fun accu (a,eq1) -> + List.fold_left + (fun accu (b,eq2) -> + let eq = + sum_afine new_eq_id (map_eq_afine (fun c -> c * b) eq1) + (map_eq_afine (fun c -> c * a) eq2) in + add_event(SUM(eq.id,(b,eq1),(a,eq2))); + match normalize eq with + | [eq] -> + let final_eq = + if dark_shadow then + let delta = (a - one) * (b - one) in + add_event(WEAKEN(eq.id,delta)); + {id = eq.id; kind=INEQ; body = eq.body; + constant = eq.constant - delta} + else eq + in final_eq :: accu + | (e::_) -> failwith "Product dardk" + | [] -> accu) + accu high) + [] low + +let fourier_motzkin (new_eq_id,_,print_var) dark_shadow system = + let v = select_variable system in + let (ineq_out, ineq_low,ineq_high) = classify v system in + let expanded = ineq_out @ product new_eq_id dark_shadow ineq_low ineq_high in + if !debug then display_system print_var expanded; expanded + +let simplify ((new_eq_id,new_var_id,print_var) as new_ids) dark_shadow system = + if List.exists (fun e -> e.kind = DISE) system then + failwith "disequation in simplify"; + clear_history (); + List.iter (fun e -> add_event (HYP e)) system; + let system = Util.List.map_append normalize system in + let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in + let simp_eq,simp_ineq = redundancy_elimination new_eq_id ineqs in + let system = (eqs @ simp_eq,simp_ineq) in + let rec loop1a system = + let sys_ineq = banerjee new_ids system in + loop1b sys_ineq + and loop1b sys_ineq = + let simp_eq,simp_ineq = redundancy_elimination new_eq_id sys_ineq in + if simp_eq = [] then simp_ineq else loop1a (simp_eq,simp_ineq) + in + let rec loop2 system = + try + let expanded = fourier_motzkin new_ids dark_shadow system in + loop2 (loop1b expanded) + with SOLVED_SYSTEM -> + if !debug then display_system print_var system; system + in + loop2 (loop1a system) + +let rec depend relie_on accu = function + | act :: l -> + begin match act with + | DIVIDE_AND_APPROX (e,_,_,_) -> + if Int.List.mem e.id relie_on then depend relie_on (act::accu) l + else depend relie_on accu l + | EXACT_DIVIDE (e,_) -> + if Int.List.mem e.id relie_on then depend relie_on (act::accu) l + else depend relie_on accu l + | WEAKEN (e,_) -> + if Int.List.mem e relie_on then depend relie_on (act::accu) l + else depend relie_on accu l + | SUM (e,(_,e1),(_,e2)) -> + if Int.List.mem e relie_on then + depend (e1.id::e2.id::relie_on) (act::accu) l + else + depend relie_on accu l + | STATE {st_new_eq=e;st_orig=o} -> + if Int.List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l + else depend relie_on accu l + | HYP e -> + if Int.List.mem e.id relie_on then depend relie_on (act::accu) l + else depend relie_on accu l + | FORGET_C _ -> depend relie_on accu l + | FORGET _ -> depend relie_on accu l + | FORGET_I _ -> depend relie_on accu l + | MERGE_EQ (e,e1,e2) -> + if Int.List.mem e relie_on then + depend (e1.id::e2::relie_on) (act::accu) l + else + depend relie_on accu l + | NOT_EXACT_DIVIDE (e,_) -> depend (e.id::relie_on) (act::accu) l + | CONTRADICTION (e1,e2) -> + depend (e1.id::e2.id::relie_on) (act::accu) l + | CONSTANT_NOT_NUL (e,_) -> depend (e::relie_on) (act::accu) l + | CONSTANT_NEG (e,_) -> depend (e::relie_on) (act::accu) l + | CONSTANT_NUL e -> depend (e::relie_on) (act::accu) l + | NEGATE_CONTRADICT (e1,e2,_) -> + depend (e1.id::e2.id::relie_on) (act::accu) l + | SPLIT_INEQ _ -> failwith "depend" + end + | [] -> relie_on, accu + +let negation (eqs,ineqs) = + let diseq,_ = List.partition (fun e -> e.kind = DISE) ineqs in + let normal = function + | ({body=f::_} as e) when f.c <? zero -> negate_eq e, INVERTED + | e -> e,NORMAL in + let table = Hashtbl.create 7 in + List.iter (fun e -> + let {body=ne;constant=c} ,kind = normal e in + Hashtbl.add table (ne,c) (kind,e)) diseq; + List.iter (fun e -> + assert (e.kind = EQUA); + let {body=ne;constant=c},kind = normal e in + try + let (kind',e') = Hashtbl.find table (ne,c) in + add_event (NEGATE_CONTRADICT (e,e',kind=kind')); + raise UNSOLVABLE + with Not_found -> ()) eqs + +exception FULL_SOLUTION of action list * int list + +let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = + clear_history (); + List.iter (fun e -> add_event (HYP e)) system; + (* Initial simplification phase *) + let rec loop1a system = + negation system; + let sys_ineq = banerjee new_ids system in + loop1b sys_ineq + and loop1b sys_ineq = + let dise,ine = List.partition (fun e -> e.kind = DISE) sys_ineq in + let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in + if simp_eq = [] then dise @ simp_ineq + else loop1a (simp_eq,dise @ simp_ineq) + in + let rec loop2 system = + try + let expanded = fourier_motzkin new_ids false system in + loop2 (loop1b expanded) + with SOLVED_SYSTEM -> if !debug then display_system print_var system; system + in + let rec explode_diseq = function + | (de::diseq,ineqs,expl_map) -> + let id1 = new_eq_id () + and id2 = new_eq_id () in + let e1 = + {id = id1; kind=INEQ; body = de.body; constant = de.constant -one} in + let e2 = + {id = id2; kind=INEQ; body = map_eq_linear neg de.body; + constant = neg de.constant - one} in + let new_sys = + List.map (fun (what,sys) -> ((de.id,id1,true)::what, e1::sys)) + ineqs @ + List.map (fun (what,sys) -> ((de.id,id2,false)::what,e2::sys)) + ineqs + in + explode_diseq (diseq,new_sys,(de.id,(de,id1,id2))::expl_map) + | ([],ineqs,expl_map) -> ineqs,expl_map + in + try + let system = Util.List.map_append normalize system in + let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in + let dise,ine = List.partition (fun e -> e.kind = DISE) ineqs in + let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in + let system = (eqs @ simp_eq,simp_ineq @ dise) in + let system' = loop1a system in + let diseq,ineq = List.partition (fun e -> e.kind = DISE) system' in + let first_segment = history () in + let sys_exploded,explode_map = explode_diseq (diseq,[[],ineq],[]) in + let all_solutions = + List.map + (fun (decomp,sys) -> + clear_history (); + try let _ = loop2 sys in raise NO_CONTRADICTION + with UNSOLVABLE -> + let relie_on,path = depend [] [] (history ()) in + let dc,_ = List.partition (fun (_,id,_) -> Int.List.mem id relie_on) decomp in + let red = List.map (fun (x,_,_) -> x) dc in + (red,relie_on,decomp,path)) + sys_exploded + in + let max_count sys = + let tbl = Hashtbl.create 7 in + let augment x = + try incr (Hashtbl.find tbl x) + with Not_found -> Hashtbl.add tbl x (ref 1) in + let eq = ref (-1) and c = ref 0 in + List.iter (function + | ([],r_on,_,path) -> raise (FULL_SOLUTION (path,r_on)) + | (l,_,_,_) -> List.iter augment l) sys; + Hashtbl.iter (fun x v -> if !v > !c then begin eq := x; c := !v end) tbl; + !eq + in + let rec solve systems = + try + let id = max_count systems in + let rec sign = function + | ((id',_,b)::l) -> if id=id' then b else sign l + | [] -> failwith "solve" in + let s1,s2 = + List.partition (fun (_,_,decomp,_) -> sign decomp) systems in + let remove_int (dep,ro,dc,pa) = + (Util.List.except Int.equal id dep,ro,dc,pa) + in + let s1' = List.map remove_int s1 in + let s2' = List.map remove_int s2 in + let (r1,relie1) = solve s1' + and (r2,relie2) = solve s2' in + let (eq,id1,id2) = Int.List.assoc id explode_map in + [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], + eq.id :: Util.List.union Int.equal relie1 relie2 + with FULL_SOLUTION (x0,x1) -> (x0,x1) + in + let act,relie_on = solve all_solutions in + snd(depend relie_on act first_segment) + with UNSOLVABLE -> snd (depend [] [] (history ())) + +end diff --git a/plugins/omega/omega_plugin.mlpack b/plugins/omega/omega_plugin.mlpack new file mode 100644 index 0000000000..df7f1047f2 --- /dev/null +++ b/plugins/omega/omega_plugin.mlpack @@ -0,0 +1,3 @@ +Omega +Coq_omega +G_omega diff --git a/plugins/omega/plugin_base.dune b/plugins/omega/plugin_base.dune new file mode 100644 index 0000000000..f512501c78 --- /dev/null +++ b/plugins/omega/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name omega_plugin) + (public_name coq.plugins.omega) + (synopsis "Coq's omega plugin") + (libraries coq.plugins.ltac)) |