diff options
| author | Frédéric Besson | 2019-03-28 15:24:33 +0100 |
|---|---|---|
| committer | Frédéric Besson | 2019-09-16 16:02:38 +0200 |
| commit | dfff69ef604e02703575cb1cb15b2f77eda5f0f4 (patch) | |
| tree | a18ae2078ecd8c3e7f46ae947b9d4ba8499b0704 | |
| parent | 3d7de72f45ae2f8bcedbe1db0eb8870e58757b45 (diff) | |
Re-implementation of zify
The logic is implemented in OCaml. By induction over the terms,
guided by registered Coq terms in ZifyInst.v, it generates a rewriting
lemma. The rewriting is only performed if there is some progress. If
the rewriting fails (due to dependencies), a novel hypothesis is
generated.
This PR fixes #5155, fixes #8898, fixes #7886, fixes #10707, fixes #9848
ans fixes #10755.
The zify plugin is placed in the micromega directory.
(Though the reason is unclear, having it in a separate directory is
bad for efficiency.) efficiency impact.
There are also a few improvements of lia/lra that are piggybacked.
- more aggressive pruning of useless hypotheses
- slightly optimised conjunctive normal form
- applies exfalso if conclusion is not in Prop
- removal of Timeout in test-suite
37 files changed, 4620 insertions, 872 deletions
diff --git a/Makefile.common b/Makefile.common index dd23d7dd2f..2d1200c071 100644 --- a/Makefile.common +++ b/Makefile.common @@ -155,13 +155,14 @@ LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo SSRCMO:=plugins/ssr/ssreflect_plugin.cmo LTAC2CMO:=user-contrib/Ltac2/ltac2_plugin.cmo +ZIFYCMO:=plugins/micromega/zify_plugin.cmo PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(MICROMEGACMO) \ $(RINGCMO) \ $(EXTRACTIONCMO) \ $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \ $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \ - $(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) $(LTAC2CMO) + $(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) $(LTAC2CMO) $(ZIFYCMO) ifeq ($(HASNATDYNLINK)-$(BEST),false-opt) STATICPLUGINS:=$(PLUGINSCMO) diff --git a/doc/changelog/04-tactics/09856-zify.rst b/doc/changelog/04-tactics/09856-zify.rst new file mode 100644 index 0000000000..6b9143c77b --- /dev/null +++ b/doc/changelog/04-tactics/09856-zify.rst @@ -0,0 +1,7 @@ +- Reimplementation of the :tacn:`zify` tactic. The tactic is more efficient and copes with dependent hypotheses. + It can also be extended by redefining the tactic ``zify_post_hook``. + (`#9856 <https://github.com/coq/coq/pull/9856>`_ fixes + `#8898 <https://github.com/coq/coq/issues/8898>`_, + `#7886 <https://github.com/coq/coq/issues/7886>`_, + `#9848 <https://github.com/coq/coq/issues/9848>`_ and + `#5155 <https://github.com/coq/coq/issues/5155>`_, by Frédéric Besson). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index e56b36caad..238106b2e7 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -9,9 +9,11 @@ Short description of the tactics -------------------------------- The Psatz module (``Require Import Psatz.``) gives access to several -tactics for solving arithmetic goals over :math:`\mathbb{Z}`, :math:`\mathbb{Q}`, and :math:`\mathbb{R}` [#]_. -It also possible to get the tactics for integers by a ``Require Import Lia``, -rationals ``Require Import Lqa`` and reals ``Require Import Lra``. +tactics for solving arithmetic goals over :math:`\mathbb{Q}`, +:math:`\mathbb{R}`, and :math:`\mathbb{Z}` but also :g:`nat` and +:g:`N`. It also possible to get the tactics for integers by a +``Require Import Lia``, rationals ``Require Import Lqa`` and reals +``Require Import Lra``. + :tacn:`lia` is a decision procedure for linear integer arithmetic; + :tacn:`nia` is an incomplete proof procedure for integer non-linear @@ -23,7 +25,7 @@ rationals ``Require Import Lqa`` and reals ``Require Import Lra``. ``n`` is an optional integer limiting the proof search depth, is an incomplete proof procedure for non-linear arithmetic. It is based on John Harrison’s HOL Light - driver to the external prover `csdp` [#]_. Note that the `csdp` driver is + driver to the external prover `csdp` [#csdp]_. Note that the `csdp` driver is generating a *proof cache* which makes it possible to rerun scripts even without `csdp`. @@ -78,7 +80,7 @@ closed under the following rules: \end{array}` The following theorem provides a proof principle for checking that a -set of polynomial inequalities does not have solutions [#]_. +set of polynomial inequalities does not have solutions [#fnpsatz]_. .. _psatz_thm: @@ -111,32 +113,21 @@ and checked to be :math:`-1`. The deductive power of :tacn:`lra` overlaps with the one of :tacn:`field` tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`. - `lia`: a tactic for linear integer arithmetic --------------------------------------------- .. tacn:: lia :name: lia - This tactic offers an alternative to the :tacn:`omega` tactic. Roughly - speaking, the deductive power of lia is the combined deductive power of - :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear goals - that :tacn:`omega` does not solve, such as the following so-called *omega - nightmare* :cite:`TheOmegaPaper`. - -.. coqdoc:: - - Goal forall x y, - 27 <= 11 * x + 13 * y <= 45 -> - -10 <= 7 * x - 9 * y <= 4 -> False. + This tactic solves linear goals over :g:`Z` by searching for *linear* refutations and cutting planes. + :tacn:`lia` provides support for :g:`Z`, :g:`nat`, :g:`positive` and :g:`N` by pre-processing via the :tacn:`zify` tactic. -The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` is under evaluation. High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ Over :math:`\mathbb{R}`, *positivstellensatz* refutations are a complete proof -principle [#]_. However, this is not the case over :math:`\mathbb{Z}`. Actually, +principle [#mayfail]_. However, this is not the case over :math:`\mathbb{Z}`. Actually, *positivstellensatz* refutations are not even sufficient to decide linear *integer* arithmetic. The canonical example is :math:`2 * x = 1 -> \mathtt{False}` which is a theorem of :math:`\mathbb{Z}` but not a theorem of :math:`{\mathbb{R}}`. To remedy this @@ -249,21 +240,55 @@ cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running :tacn:`ring` we obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. -.. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with - the ``zify`` tactic. -.. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by - pre-processing the goal with the ``Z.div_mod_to_equations`` tactic (you may - need to manually run ``zify`` first). -.. [#] Support for :g:`Z.quot` and :g:`Z.rem` may be obtained by pre-processing - the goal with the ``Z.quot_rem_to_equations`` tactic (you may need to manually - run ``zify`` first). -.. [#] Note that support for :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and - :g:`Z.rem` may be simultaneously obtained by pre-processing the goal with the - ``Z.to_euclidean_division_equations`` tactic (you may need to manually run - ``zify`` first). -.. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp -.. [#] Variants deal with equalities and strict inequalities. -.. [#] In practice, the oracle might fail to produce such a refutation. +`zify`: pre-processing of arithmetic goals +------------------------------------------ + +.. tacn:: zify + :name: zify + + This tactic is internally called by :tacn:`lia` to support additional types e.g., :g:`nat`, :g:`positive` and :g:`N`. + By requiring the module ``ZifyBool``, the boolean type :g:`bool` and some comparison operators are also supported. + :tacn:`zify` can also be extended by rebinding the tactic `Zify.zify_post_hook` that is run immediately after :tacn:`zify`. + + + To support :g:`Z.div` and :g:`Z.modulo`: ``Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations``. + + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``. + + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations``. + + +.. cmd:: Show Zify InjTyp + :name: Show Zify InjTyp + + This command shows the list of types that can be injected into :g:`Z`. + +.. cmd:: Show Zify BinOp + :name: Show Zify BinOp + + This command shows the list of binary operators processed by :tacn:`zify`. + +.. cmd:: Show Zify BinRel + :name: Show Zify BinRel + + This command shows the list of binary relations processed by :tacn:`zify`. + + +.. cmd:: Show Zify UnOp + :name: Show Zify UnOp + + This command shows the list of unary operators processed by :tacn:`zify`. + +.. cmd:: Show Zify CstOp + :name: Show Zify CstOp + + This command shows the list of constants processed by :tacn:`zify`. + +.. cmd:: Show Zify Spec + :name: Show Zify Spec + + This command shows the list of operators over :g:`Z` that are compiled using their specification e.g., :g:`Z.min`. + +.. [#csdp] Sources and binaries can be found at https://projects.coin-or.org/Csdp +.. [#fnpsatz] Variants deal with equalities and strict inequalities. +.. [#mayfail] In practice, the oracle might fail to produce such a refutation. .. comment in original TeX: .. %% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 46175e37ed..bc4d8b95ab 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -42,6 +42,10 @@ plugins/micromega/Tauto.v plugins/micromega/VarMap.v plugins/micromega/ZCoeff.v plugins/micromega/ZMicromega.v +plugins/micromega/ZifyInst.v +plugins/micromega/ZifyBool.v +plugins/micromega/ZifyClasses.v +plugins/micromega/Zify.v plugins/nsatz/Nsatz.v plugins/omega/Omega.v plugins/omega/OmegaLemmas.v diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v index 8c7b601aba..7e04fe0220 100644 --- a/plugins/micromega/Lia.v +++ b/plugins/micromega/Lia.v @@ -23,9 +23,6 @@ Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". -Ltac preprocess := - zify ; unfold Z.succ in * ; unfold Z.pred in *. - Ltac zchange checker := intros __wit __varmap __ff ; change (@Tauto.eval_bf _ (Zeval_formula (@find Z Z0 __varmap)) __ff) ; @@ -39,11 +36,17 @@ Ltac zchecker_abstract checker := Ltac zchecker := zchecker_no_abstract ZTautoChecker_sound. -Ltac zchecker_ext := zchecker_no_abstract ZTautoCheckerExt_sound. +(*Ltac zchecker_ext := zchecker_no_abstract ZTautoCheckerExt_sound.*) + +Ltac zchecker_ext := + intros __wit __varmap __ff ; + exact (ZTautoCheckerExt_sound __ff __wit + (@eq_refl bool true <: @eq bool (ZTautoCheckerExt __ff __wit) true) + (@find Z Z0 __varmap)). -Ltac lia := preprocess; xlia zchecker_ext. +Ltac lia := zify; xlia zchecker_ext. -Ltac nia := preprocess; xnlia zchecker. +Ltac nia := zify; xnlia zchecker. (* Local Variables: *) diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 1050bae303..80e0f3a536 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -55,7 +55,8 @@ Extract Constant Rinv => "fun x -> 1 / x". extraction is only performed as a test in the test suite. *) (*Extraction "micromega.ml" Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula - ZMicromega.cnfZ ZMicromega.Zeval_const ZMicromega.bound_problem_fr QMicromega.cnfQ + Tauto.abst_form + ZMicromega.cnfZ ZMicromega.bound_problem_fr ZMicromega.Zeval_const QMicromega.cnfQ List.map simpl_cone (*map_cone indexes*) denorm Qpower vm_add normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v index 3c72d3268f..4a02d1d01e 100644 --- a/plugins/micromega/QMicromega.v +++ b/plugins/micromega/QMicromega.v @@ -172,9 +172,9 @@ Qed. Require Import Coq.micromega.Tauto. -Definition Qnormalise := @cnf_normalise Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool. +Definition Qnormalise := @cnf_normalise Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool Qle_bool. -Definition Qnegate := @cnf_negate Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool. +Definition Qnegate := @cnf_negate Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool Qle_bool. Definition qunsat := check_inconsistent 0 Qeq_bool Qle_bool. @@ -204,7 +204,7 @@ Proof. unfold eval_nformula. unfold RingMicromega.eval_nformula. destruct t. apply (check_inconsistent_sound Qsor QSORaddon) ; auto. - - unfold qdeduce. apply (nformula_plus_nformula_correct Qsor QSORaddon). + - unfold qdeduce. intros. revert H. apply (nformula_plus_nformula_correct Qsor QSORaddon);auto. - intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now eapply (cnf_normalise_correct Qsor QSORaddon);eauto. - intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now eapply (cnf_negate_correct Qsor QSORaddon);eauto. - intros t w0. diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index 30bbac44d0..d8282a1127 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -432,8 +432,8 @@ Qed. Require Import Coq.micromega.Tauto. -Definition Rnormalise := @cnf_normalise Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool. -Definition Rnegate := @cnf_negate Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool. +Definition Rnormalise := @cnf_normalise Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool Qle_bool. +Definition Rnegate := @cnf_negate Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool Qle_bool. Definition runsat := check_inconsistent 0%Q Qeq_bool Qle_bool. @@ -467,7 +467,9 @@ Proof. apply Reval_nformula_dec. - destruct t. apply (check_inconsistent_sound Rsor QSORaddon) ; auto. - - unfold rdeduce. apply (nformula_plus_nformula_correct Rsor QSORaddon). + - unfold rdeduce. + intros. revert H. + eapply (nformula_plus_nformula_correct Rsor QSORaddon); eauto. - now apply (cnf_normalise_correct Rsor QSORaddon). - intros. now eapply (cnf_negate_correct Rsor QSORaddon); eauto. - intros t w0. diff --git a/plugins/micromega/Refl.v b/plugins/micromega/Refl.v index 63b4d5e8f8..cd759029fa 100644 --- a/plugins/micromega/Refl.v +++ b/plugins/micromega/Refl.v @@ -99,8 +99,6 @@ Proof. apply IHl; auto. Qed. - - Lemma make_conj_app : forall A eval l1 l2, @make_conj A eval (l1 ++ l2) <-> @make_conj A eval l1 /\ @make_conj A eval l2. Proof. induction l1. @@ -114,34 +112,41 @@ Proof. tauto. Qed. +Infix "+++" := rev_append (right associativity, at level 60) : list_scope. + +Lemma make_conj_rapp : forall A eval l1 l2, @make_conj A eval (l1 +++ l2) <-> @make_conj A eval (l1++l2). +Proof. + induction l1. + - simpl. tauto. + - intros. + simpl rev_append at 1. + rewrite IHl1. + rewrite make_conj_app. + rewrite make_conj_cons. + simpl app. + rewrite make_conj_cons. + rewrite make_conj_app. + tauto. +Qed. + Lemma not_make_conj_cons : forall (A:Type) (t:A) a eval (no_middle_eval : (eval t) \/ ~ (eval t)), - ~ make_conj eval (t ::a) -> ~ (eval t) \/ (~ make_conj eval a). + ~ make_conj eval (t ::a) <-> ~ (eval t) \/ (~ make_conj eval a). Proof. intros. - simpl in H. - destruct a. - tauto. + rewrite make_conj_cons. tauto. Qed. Lemma not_make_conj_app : forall (A:Type) (t:list A) a eval (no_middle_eval : forall d, eval d \/ ~ eval d) , - ~ make_conj eval (t ++ a) -> (~ make_conj eval t) \/ (~ make_conj eval a). + ~ make_conj eval (t ++ a) <-> (~ make_conj eval t) \/ (~ make_conj eval a). Proof. induction t. - simpl. - tauto. - intros. - simpl ((a::t)++a0)in H. - destruct (@not_make_conj_cons _ _ _ _ (no_middle_eval a) H). - left ; red ; intros. - apply H0. - rewrite make_conj_cons in H1. - tauto. - destruct (IHt _ _ no_middle_eval H0). - left ; red ; intros. - apply H1. - rewrite make_conj_cons in H2. - tauto. - right ; auto. + - simpl. + tauto. + - intros. + simpl ((a::t)++a0). + rewrite !not_make_conj_cons by auto. + rewrite IHt by auto. + tauto. Qed. diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index cddc140f51..c1edf579cf 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -707,6 +707,8 @@ Definition padd := Padd cO cplus ceqb. Definition pmul := Pmul cO cI cplus ctimes ceqb. +Definition popp := Popp copp. + Definition normalise (f : Formula C) : NFormula := let (lhs, op, rhs) := f in let lhs := norm lhs in @@ -733,7 +735,6 @@ let (lhs, op, rhs) := f in | OpLt => (psub lhs rhs, NonStrict) end. - Lemma eval_pol_sub : forall env lhs rhs, eval_pol env (psub lhs rhs) == eval_pol env lhs - eval_pol env rhs. Proof. intros. @@ -755,6 +756,12 @@ Proof. (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)). Qed. +Lemma eval_pol_opp : forall env e, eval_pol env (popp e) == - eval_pol env e. +Proof. + intros. + apply (Popp_ok (SORsetoid sor) Rops_wd + (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon)). +Qed. Lemma eval_pol_norm : forall env lhs, eval_pexpr env lhs == eval_pol env (norm lhs). @@ -766,16 +773,18 @@ Qed. Theorem normalise_sound : forall (env : PolEnv) (f : Formula C), - eval_formula env f -> eval_nformula env (normalise f). + eval_formula env f <-> eval_nformula env (normalise f). Proof. -intros env f H; destruct f as [lhs op rhs]; simpl in *. +intros env f; destruct f as [lhs op rhs]; simpl in *. destruct op; simpl in *; rewrite eval_pol_sub ; rewrite <- eval_pol_norm ; rewrite <- eval_pol_norm. -now apply <- (Rminus_eq_0 sor). -intros H1. apply -> (Rminus_eq_0 sor) in H1. now apply H. -now apply -> (Rle_le_minus sor). -now apply -> (Rle_le_minus sor). -now apply -> (Rlt_lt_minus sor). -now apply -> (Rlt_lt_minus sor). +- symmetry. + now apply (Rminus_eq_0 sor). +- rewrite (Rminus_eq_0 sor). + tauto. +- now apply (Rle_le_minus sor). +- now apply (Rle_le_minus sor). +- now apply (Rlt_lt_minus sor). +- now apply (Rlt_lt_minus sor). Qed. Theorem negate_correct : @@ -784,92 +793,173 @@ Theorem negate_correct : Proof. intros env f; destruct f as [lhs op rhs]; simpl. destruct op; simpl in *; rewrite eval_pol_sub ; rewrite <- eval_pol_norm ; rewrite <- eval_pol_norm. -symmetry. rewrite (Rminus_eq_0 sor). +- symmetry. rewrite (Rminus_eq_0 sor). split; intro H; [symmetry; now apply -> (Req_dne sor) | symmetry in H; now apply <- (Req_dne sor)]. -rewrite (Rminus_eq_0 sor). split; intro; now apply (Rneq_symm sor). -rewrite <- (Rlt_lt_minus sor). now rewrite <- (Rle_ngt sor). -rewrite <- (Rlt_lt_minus sor). now rewrite <- (Rle_ngt sor). -rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor). -rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor). +- rewrite (Rminus_eq_0 sor). split; intro; now apply (Rneq_symm sor). +- rewrite <- (Rlt_lt_minus sor). now rewrite <- (Rle_ngt sor). +- rewrite <- (Rlt_lt_minus sor). now rewrite <- (Rle_ngt sor). +- rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor). +- rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor). Qed. (** Another normalisation - this is used for cnf conversion **) -Definition xnormalise (t:Formula C) : list (NFormula) := - let (lhs,o,rhs) := t in - let lhs := norm lhs in - let rhs := norm rhs in +Definition xnormalise (f:NFormula) : list (NFormula) := + let (e,o) := f in + match o with + | Equal => (e , Strict) :: (popp e, Strict) :: nil + | NonEqual => (e , Equal) :: nil + | Strict => (popp e, NonStrict) :: nil + | NonStrict => (popp e, Strict) :: nil + end. + +Definition xnegate (t:NFormula) : list (NFormula) := + let (e,o) := t in match o with - | OpEq => - (psub lhs rhs, Strict)::(psub rhs lhs , Strict)::nil - | OpNEq => (psub lhs rhs,Equal) :: nil - | OpGt => (psub rhs lhs,NonStrict) :: nil - | OpLt => (psub lhs rhs,NonStrict) :: nil - | OpGe => (psub rhs lhs , Strict) :: nil - | OpLe => (psub lhs rhs ,Strict) :: nil + | Equal => (e,Equal) :: nil + | NonEqual => (e,Strict)::(popp e,Strict)::nil + | Strict => (e,Strict) :: nil + | NonStrict => (e,NonStrict) :: nil end. -Import Coq.micromega.Tauto. -Definition cnf_normalise {T : Type} (t:Formula C) (tg : T) : cnf NFormula T := - List.map (fun x => (x,tg)::nil) (xnormalise t). +Import Coq.micromega.Tauto. +Definition cnf_of_list {T : Type} (l:list NFormula) (tg : T) : cnf NFormula T := + List.fold_right (fun x acc => + if check_inconsistent x then acc else ((x,tg)::nil)::acc) + (cnf_tt _ _) l. Add Ring SORRing : (SORrt sor). -Lemma cnf_normalise_correct : forall (T : Type) env t tg, eval_cnf (Annot:=T) eval_nformula env (cnf_normalise t tg) -> eval_formula env t. +Lemma cnf_of_list_correct : + forall (T : Type) env l tg, + eval_cnf (Annot:=T) eval_nformula env (cnf_of_list l tg) <-> + make_conj (fun x : NFormula => eval_nformula env x -> False) l. Proof. - unfold cnf_normalise, xnormalise ; simpl ; intros T env t tg. - unfold eval_cnf, eval_clause. - destruct t as [lhs o rhs]; case_eq o ; unfold eval_tt; - simpl; - repeat rewrite eval_pol_sub ; repeat rewrite <- eval_pol_norm in * ; - generalize (eval_pexpr env lhs); - generalize (eval_pexpr env rhs) ; intros z1 z2 ; intros. - - apply (SORle_antisymm sor). - + rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto. - + rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto. - - now rewrite <- (Rminus_eq_0 sor). - - rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). auto. - - rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). auto. - - rewrite (Rlt_nge sor). rewrite (Rle_le_minus sor). auto. - - rewrite (Rlt_nge sor). rewrite (Rle_le_minus sor). auto. + unfold cnf_of_list. + intros T env l tg. + set (F := (fun (x : NFormula) (acc : list (list (NFormula * T))) => + if check_inconsistent x then acc else ((x, tg) :: nil) :: acc)). + set (G := ((fun x : NFormula => eval_nformula env x -> False))). + induction l. + - compute. + tauto. + - rewrite make_conj_cons. + simpl. + unfold F at 1. + destruct (check_inconsistent a) eqn:EQ. + + rewrite IHl. + unfold G. + destruct a. + specialize (check_inconsistent_sound _ _ EQ env). + simpl. + tauto. + + + rewrite <- eval_cnf_cons_iff with (1:= fun env (term:Formula Z) => True) . + simpl. + unfold eval_tt. simpl. + rewrite IHl. + unfold G at 2. + tauto. Qed. -Definition xnegate (t:Formula C) : list (NFormula) := - let (lhs,o,rhs) := t in - let lhs := norm lhs in - let rhs := norm rhs in - match o with - | OpEq => (psub lhs rhs,Equal) :: nil - | OpNEq => (psub lhs rhs ,Strict)::(psub rhs lhs,Strict)::nil - | OpGt => (psub lhs rhs,Strict) :: nil - | OpLt => (psub rhs lhs,Strict) :: nil - | OpGe => (psub lhs rhs,NonStrict) :: nil - | OpLe => (psub rhs lhs,NonStrict) :: nil - end. +Definition cnf_normalise {T: Type} (t: Formula C) (tg: T) : cnf NFormula T := + let f := normalise t in + if check_inconsistent f then cnf_ff _ _ + else cnf_of_list (xnormalise f) tg. -Definition cnf_negate {T : Type} (t:Formula C) (tg:T) : cnf NFormula T := - List.map (fun x => (x,tg)::nil) (xnegate t). +Definition cnf_negate {T: Type} (t: Formula C) (tg: T) : cnf NFormula T := + let f := normalise t in + if check_inconsistent f then cnf_tt _ _ + else cnf_of_list (xnegate f) tg. + +Lemma eq0_cnf : forall x, + (0 < x -> False) /\ (0 < - x -> False) <-> x == 0. +Proof. + split ; intros. + + apply (SORle_antisymm sor). + * now rewrite (Rle_ngt sor). + * rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). + setoid_replace (0 - x) with (-x) by ring. + tauto. + + split; intro. + * rewrite (SORlt_le_neq sor) in H0. + apply (proj2 H0). + now rewrite H. + * rewrite (SORlt_le_neq sor) in H0. + apply (proj2 H0). + rewrite H. ring. +Qed. + +Lemma xnormalise_correct : forall env f, + (make_conj (fun x => eval_nformula env x -> False) (xnormalise f)) <-> eval_nformula env f. +Proof. + intros env f. + destruct f as [e o]; destruct o eqn:Op; cbn - [psub]; + repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc; + repeat rewrite eval_pol_opp; + generalize (eval_pol env e) as x; intro. + - apply eq0_cnf. + - unfold not. tauto. + - symmetry. rewrite (Rlt_nge sor). + rewrite (Rle_le_minus sor). + setoid_replace (0 - x) with (-x) by ring. + tauto. + - rewrite (Rle_ngt sor). + symmetry. + rewrite (Rlt_lt_minus sor). + setoid_replace (0 - x) with (-x) by ring. + tauto. +Qed. + + +Lemma xnegate_correct : forall env f, + (make_conj (fun x => eval_nformula env x -> False) (xnegate f)) <-> ~ eval_nformula env f. +Proof. + intros env f. + destruct f as [e o]; destruct o eqn:Op; cbn - [psub]; + repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc; + repeat rewrite eval_pol_opp; + generalize (eval_pol env e) as x; intro. + - tauto. + - rewrite eq0_cnf. + rewrite (Req_dne sor). + tauto. + - tauto. + - tauto. +Qed. + + +Lemma cnf_normalise_correct : forall (T : Type) env t tg, eval_cnf (Annot:=T) eval_nformula env (cnf_normalise t tg) <-> eval_formula env t. +Proof. + intros T env t tg. + unfold cnf_normalise. + rewrite normalise_sound. + generalize (normalise t) as f;intro. + destruct (check_inconsistent f) eqn:U. + - destruct f as [e op]. + assert (US := check_inconsistent_sound _ _ U env). + rewrite eval_cnf_ff with (1:= eval_nformula). + tauto. + - intros. rewrite cnf_of_list_correct. + now apply xnormalise_correct. +Qed. -Lemma cnf_negate_correct : forall (T : Type) env t (tg:T), eval_cnf eval_nformula env (cnf_negate t tg) -> ~ eval_formula env t. +Lemma cnf_negate_correct : forall (T : Type) env t (tg:T), eval_cnf eval_nformula env (cnf_negate t tg) <-> ~ eval_formula env t. Proof. - unfold cnf_negate, xnegate ; simpl ; intros T env t tg. - unfold eval_cnf, eval_clause. - destruct t as [lhs o rhs]; case_eq o ; unfold eval_tt; simpl; - repeat rewrite eval_pol_sub ; repeat rewrite <- eval_pol_norm in * ; - generalize (eval_pexpr env lhs); - generalize (eval_pexpr env rhs) ; intros z1 z2 ; intros ; intuition. + intros T env t tg. + rewrite normalise_sound. + unfold cnf_negate. + generalize (normalise t) as f;intro. + destruct (check_inconsistent f) eqn:U. - - apply H0. - rewrite H1 ; ring. - - apply H1. apply (SORle_antisymm sor). - + rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto. - + rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto. - - apply H0. now rewrite (Rle_le_minus sor) in H1. - - apply H0. now rewrite (Rle_le_minus sor) in H1. - - apply H0. now rewrite (Rlt_lt_minus sor) in H1. - - apply H0. now rewrite (Rlt_lt_minus sor) in H1. + destruct f as [e o]. + assert (US := check_inconsistent_sound _ _ U env). + rewrite eval_cnf_tt with (1:= eval_nformula). + tauto. + - rewrite cnf_of_list_correct. + apply xnegate_correct. Qed. Lemma eval_nformula_dec : forall env d, (eval_nformula env d) \/ ~ (eval_nformula env d). diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v index d6ccf582ae..02dd29ef14 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -223,32 +223,59 @@ Section S. end end. - (* Definition or_clause_cnf (t:clause) (f:cnf) : cnf := - List.map (fun x => (t++x)) f. *) - - Definition or_clause_cnf (t:clause) (f:cnf) : cnf := - List.fold_right (fun e acc => + Definition xor_clause_cnf (t:clause) (f:cnf) : cnf := + List.fold_left (fun acc e => match or_clause t e with | None => acc | Some cl => cl :: acc - end) nil f. + end) f nil . + + Definition or_clause_cnf (t: clause) (f:cnf) : cnf := + match t with + | nil => f + | _ => xor_clause_cnf t f + end. Fixpoint or_cnf (f : cnf) (f' : cnf) {struct f}: cnf := match f with | nil => cnf_tt - | e :: rst => (or_cnf rst f') ++ (or_clause_cnf e f') + | e :: rst => (or_cnf rst f') +++ (or_clause_cnf e f') end. Definition and_cnf (f1 : cnf) (f2 : cnf) : cnf := - f1 ++ f2. + f1 +++ f2. (** TX is Prop in Coq and EConstr.constr in Ocaml. AF i s unit in Coq and Names.Id.t in Ocaml *) Definition TFormula (TX: Type) (AF: Type) := @GFormula Term TX Annot AF. + + Definition is_cnf_tt (c : cnf) : bool := + match c with + | nil => true + | _ => false + end. + + Definition is_cnf_ff (c : cnf) : bool := + match c with + | nil::nil => true + | _ => false + end. + + Definition and_cnf_opt (f1 : cnf) (f2 : cnf) : cnf := + if is_cnf_ff f1 || is_cnf_ff f2 + then cnf_ff + else and_cnf f1 f2. + + Definition or_cnf_opt (f1 : cnf) (f2 : cnf) : cnf := + if is_cnf_tt f1 || is_cnf_tt f2 + then cnf_tt + else if is_cnf_ff f2 + then f1 else or_cnf f1 f2. + Fixpoint xcnf {TX AF: Type} (pol : bool) (f : TFormula TX AF) {struct f}: cnf := match f with | TT => if pol then cnf_tt else cnf_ff @@ -257,9 +284,10 @@ Section S. | A x t => if pol then normalise x t else negate x t | N e => xcnf (negb pol) e | Cj e1 e2 => - (if pol then and_cnf else or_cnf) (xcnf pol e1) (xcnf pol e2) - | D e1 e2 => (if pol then or_cnf else and_cnf) (xcnf pol e1) (xcnf pol e2) - | I e1 _ e2 => (if pol then or_cnf else and_cnf) (xcnf (negb pol) e1) (xcnf pol e2) + (if pol then and_cnf_opt else or_cnf_opt) (xcnf pol e1) (xcnf pol e2) + | D e1 e2 => (if pol then or_cnf_opt else and_cnf_opt) (xcnf pol e1) (xcnf pol e2) + | I e1 _ e2 + => (if pol then or_cnf_opt else and_cnf_opt) (xcnf (negb pol) e1) (xcnf pol e2) end. Section CNFAnnot. @@ -269,8 +297,6 @@ Section S. For efficiency, this is a separate function. *) - - Fixpoint radd_term (t : Term' * Annot) (cl : clause) : clause + list Annot := match cl with | nil => (* if t is unsat, the clause is empty BUT t is needed. *) @@ -301,56 +327,616 @@ Section S. end end. - Definition ror_clause_cnf t f := - List.fold_right (fun e '(acc,tg) => + Definition xror_clause_cnf t f := + List.fold_left (fun '(acc,tg) e => match ror_clause t e with | inl cl => (cl :: acc,tg) - | inr l => (acc,tg++l) - end) (nil,nil) f . + | inr l => (acc,tg+++l) + end) f (nil,nil). + + Definition ror_clause_cnf t f := + match t with + | nil => (f,nil) + | _ => xror_clause_cnf t f + end. - Fixpoint ror_cnf f f' := + Fixpoint ror_cnf (f f':list clause) := match f with | nil => (cnf_tt,nil) | e :: rst => let (rst_f',t) := ror_cnf rst f' in let (e_f', t') := ror_clause_cnf e f' in - (rst_f' ++ e_f', t ++ t') + (rst_f' +++ e_f', t +++ t') + end. + + Definition annot_of_clause (l : clause) : list Annot := + List.map snd l. + + Definition annot_of_cnf (f : cnf) : list Annot := + List.fold_left (fun acc e => annot_of_clause e +++ acc ) f nil. + + + Definition ror_cnf_opt f1 f2 := + if is_cnf_tt f1 + then (cnf_tt , nil) + else if is_cnf_tt f2 + then (cnf_tt, nil) + else if is_cnf_ff f2 + then (f1,nil) + else ror_cnf f1 f2. + + + Definition ocons {A : Type} (o : option A) (l : list A) : list A := + match o with + | None => l + | Some e => e ::l end. - Fixpoint rxcnf {TX AF: Type}(polarity : bool) (f : TFormula TX AF) := + Definition ratom (c : cnf) (a : Annot) : cnf * list Annot := + if is_cnf_ff c || is_cnf_tt c + then (c,a::nil) + else (c,nil). (* t is embedded in c *) + + Fixpoint rxcnf {TX AF: Type}(polarity : bool) (f : TFormula TX AF) : cnf * list Annot := match f with | TT => if polarity then (cnf_tt,nil) else (cnf_ff,nil) | FF => if polarity then (cnf_ff,nil) else (cnf_tt,nil) | X p => if polarity then (cnf_ff,nil) else (cnf_ff,nil) - | A x t => ((if polarity then normalise x t else negate x t),nil) + | A x t => ratom (if polarity then normalise x t else negate x t) t | N e => rxcnf (negb polarity) e | Cj e1 e2 => - let (e1,t1) := rxcnf polarity e1 in - let (e2,t2) := rxcnf polarity e2 in + let '(e1,t1) := rxcnf polarity e1 in + let '(e2,t2) := rxcnf polarity e2 in if polarity - then (e1 ++ e2, t1 ++ t2) - else let (f',t') := ror_cnf e1 e2 in - (f', t1 ++ t2 ++ t') + then (and_cnf_opt e1 e2, t1 +++ t2) + else let (f',t') := ror_cnf_opt e1 e2 in + (f', t1 +++ t2 +++ t') | D e1 e2 => - let (e1,t1) := rxcnf polarity e1 in - let (e2,t2) := rxcnf polarity e2 in + let '(e1,t1) := rxcnf polarity e1 in + let '(e2,t2) := rxcnf polarity e2 in if polarity - then let (f',t') := ror_cnf e1 e2 in - (f', t1 ++ t2 ++ t') - else (e1 ++ e2, t1 ++ t2) - | I e1 _ e2 => - let (e1 , t1) := (rxcnf (negb polarity) e1) in - let (e2 , t2) := (rxcnf polarity e2) in + then let (f',t') := ror_cnf_opt e1 e2 in + (f', t1 +++ t2 +++ t') + else (and_cnf_opt e1 e2, t1 +++ t2) + | I e1 a e2 => + let '(e1 , t1) := (rxcnf (negb polarity) e1) in if polarity - then let (f',t') := ror_cnf e1 e2 in - (f', t1 ++ t2 ++ t') - else (and_cnf e1 e2, t1 ++ t2) + then + if is_cnf_ff e1 + then + rxcnf polarity e2 + else (* compute disjunction *) + let '(e2 , t2) := (rxcnf polarity e2) in + let (f',t') := ror_cnf_opt e1 e2 in + (f', t1 +++ t2 +++ t') (* record the hypothesis *) + else + let '(e2 , t2) := (rxcnf polarity e2) in + (and_cnf_opt e1 e2, t1 +++ t2) end. + + Section Abstraction. + Variable TX : Type. + Variable AF : Type. + + Class to_constrT : Type := + { + mkTT : TX; + mkFF : TX; + mkA : Term -> Annot -> TX; + mkCj : TX -> TX -> TX; + mkD : TX -> TX -> TX; + mkI : TX -> TX -> TX; + mkN : TX -> TX + }. + + Context {to_constr : to_constrT}. + + Fixpoint aformula (f : TFormula TX AF) : TX := + match f with + | TT => mkTT + | FF => mkFF + | X p => p + | A x t => mkA x t + | Cj f1 f2 => mkCj (aformula f1) (aformula f2) + | D f1 f2 => mkD (aformula f1) (aformula f2) + | I f1 o f2 => mkI (aformula f1) (aformula f2) + | N f => mkN (aformula f) + end. + + + Definition is_X (f : TFormula TX AF) : option TX := + match f with + | X p => Some p + | _ => None + end. + + Definition is_X_inv : forall f x, + is_X f = Some x -> f = X x. + Proof. + destruct f ; simpl ; congruence. + Qed. + + + Variable needA : Annot -> bool. + + Definition abs_and (f1 f2 : TFormula TX AF) + (c : TFormula TX AF -> TFormula TX AF -> TFormula TX AF) := + match is_X f1 , is_X f2 with + | Some _ , _ | _ , Some _ => X (aformula (c f1 f2)) + | _ , _ => c f1 f2 + end. + + Definition abs_or (f1 f2 : TFormula TX AF) + (c : TFormula TX AF -> TFormula TX AF -> TFormula TX AF) := + match is_X f1 , is_X f2 with + | Some _ , Some _ => X (aformula (c f1 f2)) + | _ , _ => c f1 f2 + end. + + Definition mk_arrow (o : option AF) (f1 f2: TFormula TX AF) := + match o with + | None => I f1 None f2 + | Some _ => if is_X f1 then f2 else I f1 o f2 + end. + + + Fixpoint abst_form (pol : bool) (f : TFormula TX AF) := + match f with + | TT => if pol then TT else X mkTT + | FF => if pol then X mkFF else FF + | X p => X p + | A x t => if needA t then A x t else X (mkA x t) + | Cj f1 f2 => + let f1 := abst_form pol f1 in + let f2 := abst_form pol f2 in + if pol then abs_and f1 f2 Cj + else abs_or f1 f2 Cj + | D f1 f2 => + let f1 := abst_form pol f1 in + let f2 := abst_form pol f2 in + if pol then abs_or f1 f2 D + else abs_and f1 f2 D + | I f1 o f2 => + let f1 := abst_form (negb pol) f1 in + let f2 := abst_form pol f2 in + if pol + then abs_or f1 f2 (mk_arrow o) + else abs_and f1 f2 (mk_arrow o) + | N f => let f := abst_form (negb pol) f in + match is_X f with + | Some a => X (mkN a) + | _ => N f + end + end. + + + + + Lemma if_same : forall {A: Type} (b:bool) (t:A), + (if b then t else t) = t. + Proof. + destruct b ; reflexivity. + Qed. + + Lemma is_cnf_tt_cnf_ff : + is_cnf_tt cnf_ff = false. + Proof. + reflexivity. + Qed. + + Lemma is_cnf_ff_cnf_ff : + is_cnf_ff cnf_ff = true. + Proof. + reflexivity. + Qed. + + + Lemma is_cnf_tt_inv : forall f1, + is_cnf_tt f1 = true -> f1 = cnf_tt. + Proof. + unfold cnf_tt. + destruct f1 ; simpl ; try congruence. + Qed. + + Lemma is_cnf_ff_inv : forall f1, + is_cnf_ff f1 = true -> f1 = cnf_ff. + Proof. + unfold cnf_ff. + destruct f1 ; simpl ; try congruence. + destruct c ; simpl ; try congruence. + destruct f1 ; try congruence. + reflexivity. + Qed. + + + Lemma if_cnf_tt : forall f, (if is_cnf_tt f then cnf_tt else f) = f. + Proof. + intros. + destruct (is_cnf_tt f) eqn:EQ. + apply is_cnf_tt_inv in EQ;auto. + reflexivity. + Qed. + + Lemma or_cnf_opt_cnf_ff : forall f, + or_cnf_opt cnf_ff f = f. + Proof. + intros. + unfold or_cnf_opt. + rewrite is_cnf_tt_cnf_ff. + simpl. + destruct (is_cnf_tt f) eqn:EQ. + apply is_cnf_tt_inv in EQ. + congruence. + destruct (is_cnf_ff f) eqn:EQ1. + apply is_cnf_ff_inv in EQ1. + congruence. + reflexivity. + Qed. + + Lemma abs_and_pol : forall f1 f2 pol, + and_cnf_opt (xcnf pol f1) (xcnf pol f2) = + xcnf pol (abs_and f1 f2 (if pol then Cj else D)). + Proof. + unfold abs_and; intros. + destruct (is_X f1) eqn:EQ1. + apply is_X_inv in EQ1. + subst. + simpl. + rewrite if_same. reflexivity. + destruct (is_X f2) eqn:EQ2. + apply is_X_inv in EQ2. + subst. + simpl. + rewrite if_same. + unfold and_cnf_opt. + rewrite orb_comm. reflexivity. + destruct pol ; simpl; auto. + Qed. + + Lemma abs_or_pol : forall f1 f2 pol, + or_cnf_opt (xcnf pol f1) (xcnf pol f2) = + xcnf pol (abs_or f1 f2 (if pol then D else Cj)). + Proof. + unfold abs_or; intros. + destruct (is_X f1) eqn:EQ1. + apply is_X_inv in EQ1. + subst. + destruct (is_X f2) eqn:EQ2. + apply is_X_inv in EQ2. + subst. + simpl. + rewrite if_same. + reflexivity. + simpl. + rewrite if_same. + destruct pol ; simpl; auto. + destruct pol ; simpl ; auto. + Qed. + + Variable needA_all : forall a, needA a = true. + + Lemma xcnf_true_mk_arrow_l : forall o t f, + xcnf true (mk_arrow o (X t) f) = xcnf true f. + Proof. + destruct o ; simpl; auto. + intros. rewrite or_cnf_opt_cnf_ff. reflexivity. + Qed. + + Lemma or_cnf_opt_cnf_ff_r : forall f, + or_cnf_opt f cnf_ff = f. + Proof. + unfold or_cnf_opt. + intros. + rewrite is_cnf_tt_cnf_ff. + rewrite orb_comm. + simpl. + apply if_cnf_tt. + Qed. + + Lemma xcnf_true_mk_arrow_r : forall o t f, + xcnf true (mk_arrow o f (X t)) = xcnf false f. + Proof. + destruct o ; simpl; auto. + - intros. + destruct (is_X f) eqn:EQ. + apply is_X_inv in EQ. subst. reflexivity. + simpl. + apply or_cnf_opt_cnf_ff_r. + - intros. + apply or_cnf_opt_cnf_ff_r. + Qed. + + + + Lemma abst_form_correct : forall f pol, + xcnf pol f = xcnf pol (abst_form pol f). + Proof. + induction f;intros. + - simpl. destruct pol ; reflexivity. + - simpl. destruct pol ; reflexivity. + - simpl. reflexivity. + - simpl. rewrite needA_all. + reflexivity. + - simpl. + specialize (IHf1 pol). + specialize (IHf2 pol). + rewrite IHf1. + rewrite IHf2. + destruct pol. + + + apply abs_and_pol; auto. + + + apply abs_or_pol; auto. + - simpl. + specialize (IHf1 pol). + specialize (IHf2 pol). + rewrite IHf1. + rewrite IHf2. + destruct pol. + + + apply abs_or_pol; auto. + + + apply abs_and_pol; auto. + - simpl. + specialize (IHf (negb pol)). + destruct (is_X (abst_form (negb pol) f)) eqn:EQ1. + + apply is_X_inv in EQ1. + rewrite EQ1 in *. + simpl in *. + destruct pol ; auto. + + simpl. congruence. + - simpl. + specialize (IHf1 (negb pol)). + specialize (IHf2 pol). + destruct pol. + + + simpl in *. + unfold abs_or. + destruct (is_X (abst_form false f1)) eqn:EQ1; + destruct (is_X (abst_form true f2)) eqn:EQ2 ; simpl. + * apply is_X_inv in EQ1. + apply is_X_inv in EQ2. + rewrite EQ1 in *. + rewrite EQ2 in *. + rewrite IHf1. rewrite IHf2. + simpl. reflexivity. + * apply is_X_inv in EQ1. + rewrite EQ1 in *. + rewrite IHf1. + simpl. + rewrite xcnf_true_mk_arrow_l. + rewrite or_cnf_opt_cnf_ff. + congruence. + * apply is_X_inv in EQ2. + rewrite EQ2 in *. + rewrite IHf2. + simpl. + rewrite xcnf_true_mk_arrow_r. + rewrite or_cnf_opt_cnf_ff_r. + congruence. + * destruct o ; simpl ; try congruence. + rewrite EQ1. + simpl. congruence. + + simpl in *. + unfold abs_and. + destruct (is_X (abst_form true f1)) eqn:EQ1; + destruct (is_X (abst_form false f2)) eqn:EQ2 ; simpl. + * apply is_X_inv in EQ1. + apply is_X_inv in EQ2. + rewrite EQ1 in *. + rewrite EQ2 in *. + rewrite IHf1. rewrite IHf2. + simpl. reflexivity. + * apply is_X_inv in EQ1. + rewrite EQ1 in *. + rewrite IHf1. + simpl. reflexivity. + * apply is_X_inv in EQ2. + rewrite EQ2 in *. + rewrite IHf2. + simpl. unfold and_cnf_opt. + rewrite orb_comm. reflexivity. + * destruct o; simpl. + rewrite EQ1. simpl. + congruence. + congruence. + Qed. + + End Abstraction. + + End CNFAnnot. + Lemma radd_term_term : forall a' a cl, radd_term a a' = inl cl -> add_term a a' = Some cl. + Proof. + induction a' ; simpl. + - intros. + destruct (deduce (fst a) (fst a)). + destruct (unsat t). congruence. + inversion H. reflexivity. + inversion H ;reflexivity. + - intros. + destruct (deduce (fst a0) (fst a)). + destruct (unsat t). congruence. + destruct (radd_term a0 a') eqn:RADD; try congruence. + inversion H. subst. + apply IHa' in RADD. + rewrite RADD. + reflexivity. + destruct (radd_term a0 a') eqn:RADD; try congruence. + inversion H. subst. + apply IHa' in RADD. + rewrite RADD. + reflexivity. + Qed. + + Lemma radd_term_term' : forall a' a cl, add_term a a' = Some cl -> radd_term a a' = inl cl. + Proof. + induction a' ; simpl. + - intros. + destruct (deduce (fst a) (fst a)). + destruct (unsat t). congruence. + inversion H. reflexivity. + inversion H ;reflexivity. + - intros. + destruct (deduce (fst a0) (fst a)). + destruct (unsat t). congruence. + destruct (add_term a0 a') eqn:RADD; try congruence. + inversion H. subst. + apply IHa' in RADD. + rewrite RADD. + reflexivity. + destruct (add_term a0 a') eqn:RADD; try congruence. + inversion H. subst. + apply IHa' in RADD. + rewrite RADD. + reflexivity. + Qed. + + Lemma xror_clause_clause : forall a f, + fst (xror_clause_cnf a f) = xor_clause_cnf a f. + Proof. + unfold xror_clause_cnf. + unfold xor_clause_cnf. + assert (ACC: fst (@nil clause,@nil Annot) = nil). + reflexivity. + intros. + set (F1:= (fun '(acc, tg) (e : clause) => + match ror_clause a e with + | inl cl => (cl :: acc, tg) + | inr l => (acc, tg +++ l) + end)). + set (F2:= (fun (acc : list clause) (e : clause) => + match or_clause a e with + | Some cl => cl :: acc + | None => acc + end)). + revert ACC. + generalize (@nil clause,@nil Annot). + generalize (@nil clause). + induction f ; simpl ; auto. + intros. + apply IHf. + unfold F1 , F2. + destruct p ; simpl in * ; subst. + clear. + revert a0. + induction a; simpl; auto. + intros. + destruct (radd_term a a1) eqn:RADD. + apply radd_term_term in RADD. + rewrite RADD. + auto. + destruct (add_term a a1) eqn:RADD'. + apply radd_term_term' in RADD'. + congruence. + reflexivity. + Qed. + + Lemma ror_clause_clause : forall a f, + fst (ror_clause_cnf a f) = or_clause_cnf a f. + Proof. + unfold ror_clause_cnf,or_clause_cnf. + destruct a ; auto. + apply xror_clause_clause. + Qed. + + Lemma ror_cnf_cnf : forall f1 f2, fst (ror_cnf f1 f2) = or_cnf f1 f2. + Proof. + induction f1 ; simpl ; auto. + intros. + specialize (IHf1 f2). + destruct(ror_cnf f1 f2). + rewrite <- ror_clause_clause. + destruct(ror_clause_cnf a f2). + simpl. + rewrite <- IHf1. + reflexivity. + Qed. + + Lemma ror_opt_cnf_cnf : forall f1 f2, fst (ror_cnf_opt f1 f2) = or_cnf_opt f1 f2. + Proof. + unfold ror_cnf_opt, or_cnf_opt. + intros. + destruct (is_cnf_tt f1). + - simpl ; auto. + - simpl. destruct (is_cnf_tt f2) ; simpl ; auto. + destruct (is_cnf_ff f2) eqn:EQ. + reflexivity. + apply ror_cnf_cnf. + Qed. + + Lemma ratom_cnf : forall f a, + fst (ratom f a) = f. + Proof. + unfold ratom. + intros. + destruct (is_cnf_ff f || is_cnf_tt f); auto. + Qed. + + + + Lemma rxcnf_xcnf : forall {TX AF:Type} (f:TFormula TX AF) b, + fst (rxcnf b f) = xcnf b f. + Proof. + induction f ; simpl ; auto. + - destruct b; simpl ; auto. + - destruct b; simpl ; auto. + - destruct b ; simpl ; auto. + - intros. rewrite ratom_cnf. reflexivity. + - intros. + specialize (IHf1 b). + specialize (IHf2 b). + destruct (rxcnf b f1). + destruct (rxcnf b f2). + simpl in *. + subst. destruct b ; auto. + rewrite <- ror_opt_cnf_cnf. + destruct (ror_cnf_opt (xcnf false f1) (xcnf false f2)). + reflexivity. + - intros. + specialize (IHf1 b). + specialize (IHf2 b). + rewrite <- IHf1. + rewrite <- IHf2. + destruct (rxcnf b f1). + destruct (rxcnf b f2). + simpl in *. + subst. destruct b ; auto. + rewrite <- ror_opt_cnf_cnf. + destruct (ror_cnf_opt (xcnf true f1) (xcnf true f2)). + reflexivity. + - intros. + specialize (IHf1 (negb b)). + specialize (IHf2 b). + rewrite <- IHf1. + rewrite <- IHf2. + destruct (rxcnf (negb b) f1). + destruct (rxcnf b f2). + simpl in *. + subst. + destruct b;auto. + generalize (is_cnf_ff_inv (xcnf (negb true) f1)). + destruct (is_cnf_ff (xcnf (negb true) f1)). + + intros. + rewrite H by auto. + unfold or_cnf_opt. + simpl. + destruct (is_cnf_tt (xcnf true f2)) eqn:EQ;auto. + apply is_cnf_tt_inv in EQ; auto. + destruct (is_cnf_ff (xcnf true f2)) eqn:EQ1. + apply is_cnf_ff_inv in EQ1. congruence. + reflexivity. + + + rewrite <- ror_opt_cnf_cnf. + destruct (ror_cnf_opt (xcnf (negb true) f1) (xcnf true f2)). + intros. + reflexivity. + Qed. + Variable eval : Env -> Term -> Prop. @@ -364,8 +950,9 @@ Section S. - Variable deduce_prop : forall env t t' u, - eval' env t -> eval' env t' -> deduce t t' = Some u -> eval' env u. + Variable deduce_prop : forall t t' u, + deduce t t' = Some u -> forall env, + eval' env t -> eval' env t' -> eval' env u. @@ -377,14 +964,55 @@ Section S. Definition eval_cnf (env : Env) (f:cnf) := make_conj (eval_clause env) f. - Lemma eval_cnf_app : forall env x y, eval_cnf env (x++y) -> eval_cnf env x /\ eval_cnf env y. + Lemma eval_cnf_app : forall env x y, eval_cnf env (x+++y) <-> eval_cnf env x /\ eval_cnf env y. Proof. unfold eval_cnf. intros. - rewrite make_conj_app in H ; auto. + rewrite make_conj_rapp. + rewrite make_conj_app ; auto. + tauto. Qed. + Lemma eval_cnf_ff : forall env, eval_cnf env cnf_ff <-> False. + Proof. + unfold cnf_ff, eval_cnf,eval_clause. + simpl. tauto. + Qed. + + Lemma eval_cnf_tt : forall env, eval_cnf env cnf_tt <-> True. + Proof. + unfold cnf_tt, eval_cnf,eval_clause. + simpl. tauto. + Qed. + + + Lemma eval_cnf_and_opt : forall env x y, eval_cnf env (and_cnf_opt x y) <-> eval_cnf env (and_cnf x y). + Proof. + unfold and_cnf_opt. + intros. + destruct (is_cnf_ff x) eqn:F1. + { apply is_cnf_ff_inv in F1. + simpl. subst. + unfold and_cnf. + rewrite eval_cnf_app. + rewrite eval_cnf_ff. + tauto. + } + simpl. + destruct (is_cnf_ff y) eqn:F2. + { apply is_cnf_ff_inv in F2. + simpl. subst. + unfold and_cnf. + rewrite eval_cnf_app. + rewrite eval_cnf_ff. + tauto. + } + tauto. + Qed. + + + Definition eval_opt_clause (env : Env) (cl: option clause) := match cl with | None => True @@ -392,57 +1020,50 @@ Section S. end. - Lemma add_term_correct : forall env t cl , eval_opt_clause env (add_term t cl) -> eval_clause env (t::cl). + Lemma add_term_correct : forall env t cl , eval_opt_clause env (add_term t cl) <-> eval_clause env (t::cl). Proof. induction cl. - (* BC *) simpl. - case_eq (deduce (fst t) (fst t)) ; auto. - intros *. - case_eq (unsat t0) ; auto. - unfold eval_clause. - rewrite make_conj_cons. - intros. intro. - apply unsat_prop with (1:= H) (env := env). - apply deduce_prop with (3:= H0) ; tauto. + case_eq (deduce (fst t) (fst t)) ; try tauto. + intros. + generalize (@deduce_prop _ _ _ H env). + case_eq (unsat t0) ; try tauto. + { intros. + generalize (@unsat_prop _ H0 env). + unfold eval_clause. + rewrite make_conj_cons. + simpl; intros. + tauto. + } - (* IC *) simpl. - case_eq (deduce (fst t) (fst a)). - intro u. - case_eq (unsat u). - simpl. intros. - unfold eval_clause. - intro. - apply unsat_prop with (1:= H) (env:= env). - repeat rewrite make_conj_cons in H2. - apply deduce_prop with (3:= H0); tauto. - intro. - case_eq (add_term t cl) ; intros. - simpl in H2. - rewrite H0 in IHcl. - simpl in IHcl. - unfold eval_clause in *. - intros. - repeat rewrite make_conj_cons in *. - tauto. - rewrite H0 in IHcl ; simpl in *. - unfold eval_clause in *. + case_eq (deduce (fst t) (fst a)); intros. - repeat rewrite make_conj_cons in *. - tauto. - case_eq (add_term t cl) ; intros. - simpl in H1. - unfold eval_clause in *. - repeat rewrite make_conj_cons in *. - rewrite H in IHcl. - simpl in IHcl. - tauto. - simpl in *. - rewrite H in IHcl. - simpl in IHcl. - unfold eval_clause in *. - repeat rewrite make_conj_cons in *. - tauto. + generalize (@deduce_prop _ _ _ H env). + case_eq (unsat t0); intros. + { + generalize (@unsat_prop _ H0 env). + simpl. + unfold eval_clause. + repeat rewrite make_conj_cons. + tauto. + } + destruct (add_term t cl) ; simpl in * ; try tauto. + { + intros. + unfold eval_clause in *. + repeat rewrite make_conj_cons in *. + tauto. + } + { + unfold eval_clause in *. + repeat rewrite make_conj_cons in *. + tauto. + } + destruct (add_term t cl) ; simpl in *; + unfold eval_clause in * ; + repeat rewrite make_conj_cons in *; tauto. Qed. @@ -455,80 +1076,84 @@ Section S. Hint Resolve no_middle_eval_tt : tauto. - Lemma or_clause_correct : forall cl cl' env, eval_opt_clause env (or_clause cl cl') -> eval_clause env cl \/ eval_clause env cl'. + Lemma or_clause_correct : forall cl cl' env, eval_opt_clause env (or_clause cl cl') <-> eval_clause env cl \/ eval_clause env cl'. Proof. induction cl. - - simpl. tauto. + - simpl. unfold eval_clause at 2. simpl. tauto. - intros *. simpl. assert (HH := add_term_correct env a cl'). - case_eq (add_term a cl'). + assert (eval_tt env a \/ ~ eval_tt env a) by (apply no_middle_eval'). + destruct (add_term a cl'); simpl in *. + - intros. - apply IHcl in H0. - rewrite H in HH. - simpl in HH. + rewrite IHcl. unfold eval_clause in *. - destruct H0. - * - repeat rewrite make_conj_cons in *. + rewrite !make_conj_cons in *. tauto. - * apply HH in H0. - apply not_make_conj_cons in H0 ; auto with tauto. + + unfold eval_clause in *. repeat rewrite make_conj_cons in *. tauto. - + - intros. - rewrite H in HH. - simpl in HH. - unfold eval_clause in *. - assert (HH' := HH Coq.Init.Logic.I). - apply not_make_conj_cons in HH'; auto with tauto. - repeat rewrite make_conj_cons in *. - tauto. Qed. - Lemma or_clause_cnf_correct : forall env t f, eval_cnf env (or_clause_cnf t f) -> (eval_clause env t) \/ (eval_cnf env f). + Lemma or_clause_cnf_correct : forall env t f, eval_cnf env (or_clause_cnf t f) <-> (eval_clause env t) \/ (eval_cnf env f). Proof. unfold eval_cnf. unfold or_clause_cnf. intros until t. - set (F := (fun (e : clause) (acc : list clause) => + set (F := (fun (acc : list clause) (e : clause) => match or_clause t e with | Some cl => cl :: acc | None => acc end)). - induction f;auto. - simpl. - intros. - destruct f. - - simpl in H. - simpl in IHf. - unfold F in H. - revert H. - intros. - apply or_clause_correct. - destruct (or_clause t a) ; simpl in * ; auto. - - - unfold F in H at 1. - revert H. - assert (HH := or_clause_correct t a env). - destruct (or_clause t a); simpl in HH ; - rewrite make_conj_cons in * ; intuition. - rewrite make_conj_cons in *. - tauto. + intro f. + assert ( make_conj (eval_clause env) (fold_left F f nil) <-> (eval_clause env t \/ make_conj (eval_clause env) f) /\ make_conj (eval_clause env) nil). + { + generalize (@nil clause) as acc. + induction f. + - simpl. + intros ; tauto. + - intros. + simpl fold_left. + rewrite IHf. + rewrite make_conj_cons. + unfold F in *; clear F. + generalize (or_clause_correct t a env). + destruct (or_clause t a). + + + rewrite make_conj_cons. + simpl. tauto. + + simpl. tauto. + } + destruct t ; auto. + - unfold eval_clause ; simpl. tauto. + - unfold xor_clause_cnf. + unfold F in H. + rewrite H. + unfold make_conj at 2. tauto. Qed. - Lemma eval_cnf_cons : forall env a f, (~ make_conj (eval_tt env) a) -> eval_cnf env f -> eval_cnf env (a::f). + Lemma eval_cnf_cons : forall env a f, (~ make_conj (eval_tt env) a /\ eval_cnf env f) <-> eval_cnf env (a::f). + Proof. + intros. + unfold eval_cnf in *. + rewrite make_conj_cons ; eauto. + unfold eval_clause at 2. + tauto. + Qed. + + Lemma eval_cnf_cons_iff : forall env a f, ((~ make_conj (eval_tt env) a) /\ eval_cnf env f) <-> eval_cnf env (a::f). Proof. intros. unfold eval_cnf in *. rewrite make_conj_cons ; eauto. + unfold eval_clause. + tauto. Qed. - Lemma or_cnf_correct : forall env f f', eval_cnf env (or_cnf f f') -> (eval_cnf env f) \/ (eval_cnf env f'). + + Lemma or_cnf_correct : forall env f f', eval_cnf env (or_cnf f f') <-> (eval_cnf env f) \/ (eval_cnf env f'). Proof. induction f. unfold eval_cnf. @@ -536,17 +1161,49 @@ Section S. tauto. (**) intros. - simpl in H. - destruct (eval_cnf_app _ _ _ H). - clear H. - destruct (IHf _ H0). - destruct (or_clause_cnf_correct _ _ _ H1). - left. - apply eval_cnf_cons ; auto. - right ; auto. - right ; auto. + simpl. + rewrite eval_cnf_app. + rewrite <- eval_cnf_cons_iff. + rewrite IHf. + rewrite or_clause_cnf_correct. + unfold eval_clause. + tauto. Qed. + Lemma or_cnf_opt_correct : forall env f f', eval_cnf env (or_cnf_opt f f') <-> eval_cnf env (or_cnf f f'). + Proof. + unfold or_cnf_opt. + intros. + destruct (is_cnf_tt f) eqn:TF. + { simpl. + apply is_cnf_tt_inv in TF. + subst. + rewrite or_cnf_correct. + rewrite eval_cnf_tt. + tauto. + } + destruct (is_cnf_tt f') eqn:TF'. + { simpl. + apply is_cnf_tt_inv in TF'. + subst. + rewrite or_cnf_correct. + rewrite eval_cnf_tt. + tauto. + } + { simpl. + destruct (is_cnf_ff f') eqn:EQ. + apply is_cnf_ff_inv in EQ. + subst. + rewrite or_cnf_correct. + rewrite eval_cnf_ff. + tauto. + tauto. + } + Qed. + + + + Variable normalise_correct : forall env t tg, eval_cnf env (normalise t tg) -> eval env t. Variable negate_correct : forall env t tg, eval_cnf env (negate t tg) -> ~ eval env t. @@ -554,16 +1211,16 @@ Section S. Lemma xcnf_correct : forall (f : @GFormula Term Prop Annot unit) pol env, eval_cnf env (xcnf pol f) -> eval_f (fun x => x) (eval env) (if pol then f else N f). Proof. induction f. - (* TT *) + - (* TT *) unfold eval_cnf. simpl. destruct pol ; simpl ; auto. - (* FF *) + - (* FF *) unfold eval_cnf. destruct pol; simpl ; auto. unfold eval_clause ; simpl. tauto. - (* P *) + - (* P *) simpl. destruct pol ; intros ;simpl. unfold eval_cnf in H. @@ -575,7 +1232,7 @@ Section S. unfold eval_cnf in H;simpl in H. unfold eval_clause in H ; simpl in H. tauto. - (* A *) + - (* A *) simpl. destruct pol ; simpl. intros. @@ -583,49 +1240,54 @@ Section S. (* A 2 *) intros. eapply negate_correct ; eauto. - auto. - (* Cj *) + - (* Cj *) destruct pol ; simpl. - (* pol = true *) + + (* pol = true *) intros. + rewrite eval_cnf_and_opt in H. unfold and_cnf in H. - destruct (eval_cnf_app _ _ _ H). - clear H. + rewrite eval_cnf_app in H. + destruct H. split. - apply (IHf1 _ _ H0). - apply (IHf2 _ _ H1). - (* pol = false *) + apply (IHf1 _ _ H). + apply (IHf2 _ _ H0). + + (* pol = false *) intros. - destruct (or_cnf_correct _ _ _ H). - generalize (IHf1 false env H0). + rewrite or_cnf_opt_correct in H. + rewrite or_cnf_correct in H. + destruct H as [H | H]. + generalize (IHf1 false env H). simpl. tauto. - generalize (IHf2 false env H0). + generalize (IHf2 false env H). simpl. tauto. - (* D *) + - (* D *) simpl. destruct pol. - (* pol = true *) + + (* pol = true *) intros. - destruct (or_cnf_correct _ _ _ H). - generalize (IHf1 _ env H0). + rewrite or_cnf_opt_correct in H. + rewrite or_cnf_correct in H. + destruct H as [H | H]. + generalize (IHf1 _ env H). simpl. tauto. - generalize (IHf2 _ env H0). + generalize (IHf2 _ env H). simpl. tauto. - (* pol = true *) - unfold and_cnf. + + (* pol = true *) intros. - destruct (eval_cnf_app _ _ _ H). - clear H. + rewrite eval_cnf_and_opt in H. + unfold and_cnf. + rewrite eval_cnf_app in H. + destruct H as [H0 H1]. simpl. generalize (IHf1 _ _ H0). generalize (IHf2 _ _ H1). simpl. tauto. - (**) + - (**) simpl. destruct pol ; simpl. intros. @@ -633,25 +1295,29 @@ Section S. intros. generalize (IHf _ _ H). tauto. - (* I *) + - (* I *) simpl; intros. destruct pol. - simpl. + + simpl. intro. - destruct (or_cnf_correct _ _ _ H). - generalize (IHf1 _ _ H1). + rewrite or_cnf_opt_correct in H. + rewrite or_cnf_correct in H. + destruct H as [H | H]. + generalize (IHf1 _ _ H). simpl in *. tauto. - generalize (IHf2 _ _ H1). + generalize (IHf2 _ _ H). auto. - (* pol = false *) - unfold and_cnf in H. - simpl in H. - destruct (eval_cnf_app _ _ _ H). - generalize (IHf1 _ _ H0). - generalize (IHf2 _ _ H1). - simpl. - tauto. + + (* pol = false *) + rewrite eval_cnf_and_opt in H. + unfold and_cnf in H. + simpl in H. + rewrite eval_cnf_app in H. + destruct H as [H0 H1]. + generalize (IHf1 _ _ H0). + generalize (IHf2 _ _ H1). + simpl. + tauto. Qed. diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index c0d22486b5..47c77ea927 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -23,6 +23,7 @@ Require Import ZCoeff. Require Import Refl. Require Import ZArith. (*Declare ML Module "micromega_plugin".*) +Open Scope Z_scope. Ltac flatten_bool := repeat match goal with @@ -32,10 +33,70 @@ Ltac flatten_bool := Ltac inv H := inversion H ; try subst ; clear H. +Lemma eq_le_iff : forall x, 0 = x <-> (0 <= x /\ x <= 0). +Proof. + intros. + split ; intros. + - subst. + compute. intuition congruence. + - destruct H. + apply Z.le_antisymm; auto. +Qed. + +Lemma lt_le_iff : forall x, + 0 < x <-> 0 <= x - 1. +Proof. + split ; intros. + - apply Zlt_succ_le. + ring_simplify. + auto. + - apply Zle_lt_succ in H. + ring_simplify in H. + auto. +Qed. + +Lemma le_0_iff : forall x y, + x <= y <-> 0 <= y - x. +Proof. + split ; intros. + - apply Zle_minus_le_0; auto. + - apply Zle_0_minus_le; auto. +Qed. + +Lemma le_neg : forall x, + ((0 <= x) -> False) <-> 0 < -x. +Proof. + intro. + rewrite lt_le_iff. + split ; intros. + - apply Znot_le_gt in H. + apply Zgt_le_succ in H. + rewrite le_0_iff in H. + ring_simplify in H; auto. + - assert (C := (Z.add_le_mono _ _ _ _ H H0)). + ring_simplify in C. + compute in C. + apply C ; reflexivity. +Qed. + +Lemma eq_cnf : forall x, + (0 <= x - 1 -> False) /\ (0 <= -1 - x -> False) <-> x = 0. +Proof. + intros. + rewrite Z.eq_sym_iff. + rewrite eq_le_iff. + rewrite (le_0_iff x 0). + rewrite !le_neg. + rewrite !lt_le_iff. + replace (- (x - 1) -1) with (-x) by ring. + replace (- (-1 - x) -1) with x by ring. + split ; intros (H1 & H2); auto. +Qed. -Require Import EnvRing. -Open Scope Z_scope. + + +Require Import EnvRing. Lemma Zsor : SOR 0 1 Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt. Proof. @@ -211,83 +272,213 @@ Proof. apply (eval_pol_norm Zsor ZSORaddon). Qed. -Definition xnormalise (t:Formula Z) : list (NFormula Z) := +Definition Zunsat := check_inconsistent 0 Zeq_bool Z.leb. + +Definition Zdeduce := nformula_plus_nformula 0 Z.add Zeq_bool. + +Lemma Zunsat_sound : forall f, + Zunsat f = true -> forall env, eval_nformula env f -> False. +Proof. + unfold Zunsat. + intros. + destruct f. + eapply check_inconsistent_sound with (1 := Zsor) (2 := ZSORaddon) in H; eauto. +Qed. + +Definition xnnormalise (t : Formula Z) : NFormula Z := let (lhs,o,rhs) := t in - let lhs := normZ lhs in - let rhs := normZ rhs in - match o with - | OpEq => - ((psub lhs (padd rhs (Pc 1))),NonStrict)::((psub rhs (padd lhs (Pc 1))),NonStrict)::nil - | OpNEq => (psub lhs rhs,Equal) :: nil - | OpGt => (psub rhs lhs,NonStrict) :: nil - | OpLt => (psub lhs rhs,NonStrict) :: nil - | OpGe => (psub rhs (padd lhs (Pc 1)),NonStrict) :: nil - | OpLe => (psub lhs (padd rhs (Pc 1)),NonStrict) :: nil - end. + let lhs := normZ lhs in + let rhs := normZ rhs in + match o with + | OpEq => (psub rhs lhs, Equal) + | OpNEq => (psub rhs lhs, NonEqual) + | OpGt => (psub lhs rhs, Strict) + | OpLt => (psub rhs lhs, Strict) + | OpGe => (psub lhs rhs, NonStrict) + | OpLe => (psub rhs lhs, NonStrict) + end. + +Lemma xnnormalise_correct : + forall env f, + eval_nformula env (xnnormalise f) <-> Zeval_formula env f. +Proof. + intros. + rewrite Zeval_formula_compat. + unfold xnnormalise. + destruct f as [lhs o rhs]. + destruct o eqn:O ; cbn ; rewrite ?eval_pol_sub; + rewrite <- !eval_pol_norm ; simpl in *; + unfold eval_expr; + generalize ( eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) + (fun x : N => x) (pow_N 1 Z.mul) env lhs); + generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) + (fun x : N => x) (pow_N 1 Z.mul) env rhs); intros. + - split ; intros. + + assert (z0 + (z - z0) = z0 + 0) by congruence. + rewrite Z.add_0_r in H0. + rewrite <- H0. + ring. + + subst. + ring. + - split ; repeat intro. + subst. apply H. ring. + apply H. + assert (z0 + (z - z0) = z0 + 0) by congruence. + rewrite Z.add_0_r in H1. + rewrite <- H1. + ring. + - split ; intros. + + apply Zle_0_minus_le; auto. + + apply Zle_minus_le_0; auto. + - split ; intros. + + apply Zle_0_minus_le; auto. + + apply Zle_minus_le_0; auto. + - split ; intros. + + apply Zlt_0_minus_lt; auto. + + apply Zlt_left_lt in H. + apply H. + - split ; intros. + + apply Zlt_0_minus_lt ; auto. + + apply Zlt_left_lt in H. + apply H. +Qed. + +Definition xnormalise (f: NFormula Z) : list (NFormula Z) := + let (e,o) := f in + match o with + | Equal => (psub e (Pc 1),NonStrict) :: (psub (Pc (-1)) e, NonStrict) :: nil + | NonStrict => ((psub (Pc (-1)) e,NonStrict)::nil) + | Strict => ((psub (Pc 0)) e, NonStrict)::nil + | NonEqual => (e, Equal)::nil + end. + +Lemma eval_pol_Pc : forall env z, + eval_pol env (Pc z) = z. +Proof. + reflexivity. +Qed. + +Ltac iff_ring := + match goal with + | |- ?F 0 ?X <-> ?F 0 ?Y => replace X with Y by ring ; tauto + end. + + +Lemma xnormalise_correct : forall env f, + (make_conj (fun x => eval_nformula env x -> False) (xnormalise f)) <-> eval_nformula env f. +Proof. + intros. + destruct f as [e o]; destruct o eqn:Op; cbn - [psub]; + repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc; + generalize (eval_pol env e) as x; intro. + - apply eq_cnf. + - unfold not. tauto. + - rewrite le_neg. + iff_ring. + - rewrite le_neg. + rewrite lt_le_iff. + iff_ring. +Qed. + Require Import Coq.micromega.Tauto BinNums. -Definition normalise {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T := - List.map (fun x => (x,tg)::nil) (xnormalise t). +Definition cnf_of_list {T: Type} (tg : T) (l : list (NFormula Z)) := + List.fold_right (fun x acc => + if Zunsat x then acc else ((x,tg)::nil)::acc) + (cnf_tt _ _) l. + +Lemma cnf_of_list_correct : + forall {T : Type} (tg:T) (f : list (NFormula Z)) env, + eval_cnf eval_nformula env (cnf_of_list tg f) <-> + make_conj (fun x : NFormula Z => eval_nformula env x -> False) f. +Proof. + unfold cnf_of_list. + intros. + set (F := (fun (x : NFormula Z) (acc : list (list (NFormula Z * T))) => + if Zunsat x then acc else ((x, tg) :: nil) :: acc)). + set (E := ((fun x : NFormula Z => eval_nformula env x -> False))). + induction f. + - compute. + tauto. + - rewrite make_conj_cons. + simpl. + unfold F at 1. + destruct (Zunsat a) eqn:EQ. + + rewrite IHf. + unfold E at 1. + specialize (Zunsat_sound _ EQ env). + tauto. + + + rewrite <- eval_cnf_cons_iff with (1:= fun env (term:Formula Z) => True) . + rewrite IHf. + simpl. + unfold E at 2. + unfold eval_tt. simpl. + tauto. +Qed. +Definition normalise {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T := + let f := xnnormalise t in + if Zunsat f then cnf_ff _ _ + else cnf_of_list tg (xnormalise f). Lemma normalise_correct : forall (T: Type) env t (tg:T), eval_cnf eval_nformula env (normalise t tg) <-> Zeval_formula env t. Proof. - unfold normalise, xnormalise; cbn -[padd]; intros T env t tg. - rewrite Zeval_formula_compat. - unfold eval_cnf, eval_clause. - destruct t as [lhs o rhs]; case_eq o; cbn -[padd]; - repeat rewrite eval_pol_sub; - repeat rewrite eval_pol_add; - repeat rewrite <- eval_pol_norm ; simpl in *; - unfold eval_expr; - generalize ( eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) - (fun x : N => x) (pow_N 1 Z.mul) env lhs); - generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) - (fun x : N => x) (pow_N 1 Z.mul) env rhs) ; intros z1 z2 ; intros ; subst; - intuition (auto with zarith). + intros. + rewrite <- xnnormalise_correct. + unfold normalise. + generalize (xnnormalise t) as f;intro. + destruct (Zunsat f) eqn:U. + - assert (US := Zunsat_sound _ U env). + rewrite eval_cnf_ff with (1:= eval_nformula). + tauto. + - rewrite cnf_of_list_correct. + apply xnormalise_correct. Qed. -Definition xnegate (t:RingMicromega.Formula Z) : list (NFormula Z) := - let (lhs,o,rhs) := t in - let lhs := normZ lhs in - let rhs := normZ rhs in +Definition xnegate (f:NFormula Z) : list (NFormula Z) := + let (e,o) := f in match o with - | OpEq => (psub lhs rhs,Equal) :: nil - | OpNEq => ((psub lhs (padd rhs (Pc 1))),NonStrict)::((psub rhs (padd lhs (Pc 1))),NonStrict)::nil - | OpGt => (psub lhs (padd rhs (Pc 1)),NonStrict) :: nil - | OpLt => (psub rhs (padd lhs (Pc 1)),NonStrict) :: nil - | OpGe => (psub lhs rhs,NonStrict) :: nil - | OpLe => (psub rhs lhs,NonStrict) :: nil + | Equal => (e,Equal) :: nil + | NonEqual => (psub e (Pc 1),NonStrict) :: (psub (Pc (-1)) e, NonStrict) :: nil + | NonStrict => (e,NonStrict)::nil + | Strict => (psub e (Pc 1),NonStrict)::nil end. Definition negate {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T := - List.map (fun x => (x,tg)::nil) (xnegate t). + let f := xnnormalise t in + if Zunsat f then cnf_tt _ _ + else cnf_of_list tg (xnegate f). -Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env t. -Proof. +Lemma xnegate_correct : forall env f, + (make_conj (fun x => eval_nformula env x -> False) (xnegate f)) <-> ~ eval_nformula env f. Proof. - Opaque padd. - intros T env t tg. - rewrite Zeval_formula_compat. - unfold negate, xnegate ; simpl. - unfold eval_cnf,eval_clause. - destruct t as [lhs o rhs]; case_eq o; unfold eval_tt ; simpl; - repeat rewrite eval_pol_sub; - repeat rewrite eval_pol_add; - repeat rewrite <- eval_pol_norm ; simpl in *; - unfold eval_expr; - generalize ( eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) - (fun x : N => x) (pow_N 1 Z.mul) env lhs); - generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) - (fun x : N => x) (pow_N 1 Z.mul) env rhs) ; intros z1 z2 ; intros ; subst; - intuition (auto with zarith). - Transparent padd. + intros. + destruct f as [e o]; destruct o eqn:Op; cbn - [psub]; + repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc; + generalize (eval_pol env e) as x; intro. + - tauto. + - rewrite eq_cnf. + destruct (Z.eq_decidable x 0);tauto. + - rewrite lt_le_iff. + tauto. + - tauto. Qed. -Definition Zunsat := check_inconsistent 0 Zeq_bool Z.leb. - -Definition Zdeduce := nformula_plus_nformula 0 Z.add Zeq_bool. +Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env t. +Proof. + intros. + rewrite <- xnnormalise_correct. + unfold negate. + generalize (xnnormalise t) as f;intro. + destruct (Zunsat f) eqn:U. + - assert (US := Zunsat_sound _ U env). + rewrite eval_cnf_tt with (1:= eval_nformula). + tauto. + - rewrite cnf_of_list_correct. + apply xnegate_correct. +Qed. Definition cnfZ (Annot TX AF : Type) (f : TFormula (Formula Z) Annot TX AF) := rxcnf Zunsat Zdeduce normalise negate true f. @@ -1221,7 +1412,8 @@ Proof. unfold eval_nformula. unfold RingMicromega.eval_nformula. destruct t. apply (check_inconsistent_sound Zsor ZSORaddon) ; auto. - - unfold Zdeduce. apply (nformula_plus_nformula_correct Zsor ZSORaddon). + - unfold Zdeduce. intros. revert H. + apply (nformula_plus_nformula_correct Zsor ZSORaddon); auto. - intros env t tg. rewrite normalise_correct ; auto. @@ -1513,10 +1705,8 @@ Fixpoint xhyps_of_pt (base:nat) (acc : list nat) (pt:ZArithProof) : list nat := Definition hyps_of_pt (pt : ZArithProof) : list nat := xhyps_of_pt 0 nil pt. - Open Scope Z_scope. - (** To ease bindings from ml code **) Definition make_impl := Refl.make_impl. Definition make_conj := Refl.make_conj. diff --git a/plugins/micromega/Zify.v b/plugins/micromega/Zify.v new file mode 100644 index 0000000000..57d812b0fd --- /dev/null +++ b/plugins/micromega/Zify.v @@ -0,0 +1,90 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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 ZifyClasses. +Require Export ZifyInst. +Require Import InitialRing. + +(** From PreOmega *) + +(** 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. + +(* end from PreOmega *) + +Ltac applySpec S := + let t := type of S in + match t with + | @BinOpSpec _ _ ?Op _ => + let Spec := (eval unfold S, BSpec in (@BSpec _ _ Op _ S)) in + repeat + match goal with + | H : context[Op ?X ?Y] |- _ => zify_binop Op Spec X Y + | |- context[Op ?X ?Y] => zify_binop Op Spec X Y + end + | @UnOpSpec _ _ ?Op _ => + let Spec := (eval unfold S, USpec in (@USpec _ _ Op _ S)) in + repeat + match goal with + | H : context[Op ?X] |- _ => zify_unop Op Spec X + | |- context[Op ?X ] => zify_unop Op Spec X + end + end. + +(** [zify_post_hook] is there to be redefined. *) +Ltac zify_post_hook := idtac. + +Ltac zify := zify_tac ; (iter_specs applySpec) ; zify_post_hook. diff --git a/plugins/micromega/ZifyBool.v b/plugins/micromega/ZifyBool.v new file mode 100644 index 0000000000..ec37c2003f --- /dev/null +++ b/plugins/micromega/ZifyBool.v @@ -0,0 +1,255 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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 Bool ZArith. +Require Import ZifyClasses. +Open Scope Z_scope. +(* Instances of [ZifyClasses] for dealing with boolean operators. + Various encodings of boolean are possible. One objective is to + have an encoding that is terse but also lia friendly. + *) + +(** [Z_of_bool] is the injection function for boolean *) +Definition Z_of_bool (b : bool) : Z := if b then 1 else 0. + +(** [bool_of_Z] is a compatible reverse operation *) +Definition bool_of_Z (z : Z) : bool := negb (Z.eqb z 0). + +Lemma Z_of_bool_bound : forall x, 0 <= Z_of_bool x <= 1. +Proof. + destruct x ; simpl; compute; intuition congruence. +Qed. + +Instance Inj_bool_Z : InjTyp bool Z := + { inj := Z_of_bool ; pred :=(fun x => 0 <= x <= 1) ; cstr := Z_of_bool_bound}. +Add InjTyp Inj_bool_Z. + +(** Boolean operators *) + +Instance Op_andb : BinOp andb := + { TBOp := Z.min ; + TBOpInj := ltac: (destruct n,m; reflexivity)}. +Add BinOp Op_andb. + +Instance Op_orb : BinOp orb := + { TBOp := Z.max ; + TBOpInj := ltac:(destruct n,m; reflexivity)}. +Add BinOp Op_orb. + +Instance Op_negb : UnOp negb := + { TUOp := fun x => 1 - x ; TUOpInj := ltac:(destruct x; reflexivity)}. +Add UnOp Op_negb. + +Instance Op_eq_bool : BinRel (@eq bool) := + {TR := @eq Z ; TRInj := ltac:(destruct n,m; simpl ; intuition congruence) }. +Add BinRel Op_eq_bool. + +Instance Op_true : CstOp true := + { TCst := 1 ; TCstInj := eq_refl }. + +Instance Op_false : CstOp false := + { TCst := 0 ; TCstInj := eq_refl }. + + +(** Comparisons are encoded using the predicates [isZero] and [isLeZero].*) + +Definition isZero (z : Z) := Z_of_bool (Z.eqb z 0). + +Definition isLeZero (x : Z) := Z_of_bool (Z.leb x 0). + +(* Some intermediate lemma *) + +Lemma Z_eqb_isZero : forall n m, + Z_of_bool (n =? m) = isZero (n - m). +Proof. + intros ; unfold isZero. + destruct ( n =? m) eqn:EQ. + - simpl. rewrite Z.eqb_eq in EQ. + rewrite EQ. rewrite Z.sub_diag. + reflexivity. + - + destruct (n - m =? 0) eqn:EQ'. + rewrite Z.eqb_neq in EQ. + rewrite Z.eqb_eq in EQ'. + apply Zminus_eq in EQ'. + congruence. + reflexivity. +Qed. + +Lemma Z_leb_sub : forall x y, x <=? y = ((x - y) <=? 0). +Proof. + intros. + destruct (x <=?y) eqn:B1 ; + destruct (x - y <=?0) eqn:B2 ; auto. + - rewrite Z.leb_le in B1. + rewrite Z.leb_nle in B2. + rewrite Z.le_sub_0 in B2. tauto. + - rewrite Z.leb_nle in B1. + rewrite Z.leb_le in B2. + rewrite Z.le_sub_0 in B2. tauto. +Qed. + +Lemma Z_ltb_leb : forall x y, x <? y = (x +1 <=? y). +Proof. + intros. + destruct (x <?y) eqn:B1 ; + destruct (x + 1 <=?y) eqn:B2 ; auto. + - rewrite Z.ltb_lt in B1. + rewrite Z.leb_nle in B2. + apply Zorder.Zlt_le_succ in B1. + unfold Z.succ in B1. + tauto. + - rewrite Z.ltb_nlt in B1. + rewrite Z.leb_le in B2. + apply Zorder.Zle_lt_succ in B2. + unfold Z.succ in B2. + apply Zorder.Zplus_lt_reg_r in B2. + tauto. +Qed. + + +(** Comparison over Z *) + +Instance Op_Zeqb : BinOp Z.eqb := + { TBOp := fun x y => isZero (Z.sub x y) ; TBOpInj := Z_eqb_isZero}. + +Instance Op_Zleb : BinOp Z.leb := + { TBOp := fun x y => isLeZero (x-y) ; + TBOpInj := + ltac: (intros;unfold isLeZero; + rewrite Z_leb_sub; + auto) }. +Add BinOp Op_Zleb. + +Instance Op_Zgeb : BinOp Z.geb := + { TBOp := fun x y => isLeZero (y-x) ; + TBOpInj := ltac:( + intros; + unfold isLeZero; + rewrite Z.geb_leb; + rewrite Z_leb_sub; + auto) }. +Add BinOp Op_Zgeb. + +Instance Op_Zltb : BinOp Z.ltb := + { TBOp := fun x y => isLeZero (x+1-y) ; + TBOpInj := ltac:( + intros; + unfold isLeZero; + rewrite Z_ltb_leb; + rewrite <- Z_leb_sub; + reflexivity) }. + +Instance Op_Zgtb : BinOp Z.gtb := + { TBOp := fun x y => isLeZero (y-x+1) ; + TBOpInj := ltac:( + intros; + unfold isLeZero; + rewrite Z.gtb_ltb; + rewrite Z_ltb_leb; + rewrite Z_leb_sub; + rewrite Z.add_sub_swap; + reflexivity) }. +Add BinOp Op_Zgtb. + +(** Comparison over nat *) + + +Lemma Z_of_nat_eqb_iff : forall n m, + (n =? m)%nat = (Z.of_nat n =? Z.of_nat m). +Proof. + intros. + rewrite Nat.eqb_compare. + rewrite Z.eqb_compare. + rewrite Nat2Z.inj_compare. + reflexivity. +Qed. + +Lemma Z_of_nat_leb_iff : forall n m, + (n <=? m)%nat = (Z.of_nat n <=? Z.of_nat m). +Proof. + intros. + rewrite Nat.leb_compare. + rewrite Z.leb_compare. + rewrite Nat2Z.inj_compare. + reflexivity. +Qed. + +Lemma Z_of_nat_ltb_iff : forall n m, + (n <? m)%nat = (Z.of_nat n <? Z.of_nat m). +Proof. + intros. + rewrite Nat.ltb_compare. + rewrite Z.ltb_compare. + rewrite Nat2Z.inj_compare. + reflexivity. +Qed. + +Instance Op_nat_eqb : BinOp Nat.eqb := + { TBOp := fun x y => isZero (Z.sub x y) ; + TBOpInj := ltac:( + intros; simpl; + rewrite <- Z_eqb_isZero; + f_equal; apply Z_of_nat_eqb_iff) }. +Add BinOp Op_nat_eqb. + +Instance Op_nat_leb : BinOp Nat.leb := + { TBOp := fun x y => isLeZero (x-y) ; + TBOpInj := ltac:( + intros; + rewrite Z_of_nat_leb_iff; + unfold isLeZero; + rewrite Z_leb_sub; + auto) }. +Add BinOp Op_nat_leb. + +Instance Op_nat_ltb : BinOp Nat.ltb := + { TBOp := fun x y => isLeZero (x+1-y) ; + TBOpInj := ltac:( + intros; + rewrite Z_of_nat_ltb_iff; + unfold isLeZero; + rewrite Z_ltb_leb; + rewrite <- Z_leb_sub; + reflexivity) }. +Add BinOp Op_nat_ltb. + +(** Injected boolean operators *) + +Lemma Z_eqb_ZSpec_ok : forall x, x <> isZero x. +Proof. + intros. + unfold isZero. + destruct (x =? 0) eqn:EQ. + - apply Z.eqb_eq in EQ. + simpl. congruence. + - apply Z.eqb_neq in EQ. + simpl. auto. +Qed. + +Instance Z_eqb_ZSpec : UnOpSpec isZero := + {| UPred := fun n r => n <> r ; USpec := Z_eqb_ZSpec_ok |}. +Add Spec Z_eqb_ZSpec. + +Lemma leZeroSpec_ok : forall x, x <= 0 /\ isLeZero x = 1 \/ x > 0 /\ isLeZero x = 0. +Proof. + intros. + unfold isLeZero. + destruct (x <=? 0) eqn:EQ. + - apply Z.leb_le in EQ. + simpl. intuition congruence. + - simpl. + apply Z.leb_nle in EQ. + apply Zorder.Znot_le_gt in EQ. + tauto. +Qed. + +Instance leZeroSpec : UnOpSpec isLeZero := + {| UPred := fun n r => (n<=0 /\ r = 1) \/ (n > 0 /\ r = 0) ; USpec := leZeroSpec_ok|}. +Add Spec leZeroSpec. diff --git a/plugins/micromega/ZifyClasses.v b/plugins/micromega/ZifyClasses.v new file mode 100644 index 0000000000..d3f7f91074 --- /dev/null +++ b/plugins/micromega/ZifyClasses.v @@ -0,0 +1,232 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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) *) +(************************************************************************) +Set Primitive Projections. + +(** An alternative to [zify] in ML parametrised by user-provided classes instances. + + The framework has currently several limitations that are in place for simplicity. + For instance, we only consider binary operators of type [Op: S -> S -> S]. + Another limitation is that our injection theorems e.g. [TBOpInj], + are using Leibniz equality; the payoff is that there is no need for morphisms... + *) + +(** An injection [InjTyp S T] declares an injection + from source type S to target type T. +*) +Class InjTyp (S : Type) (T : Type) := + mkinj { + (* [inj] is the injection function *) + inj : S -> T; + pred : T -> Prop; + (* [cstr] states that [pred] holds for any injected element. + [cstr (inj x)] is introduced in the goal for any leaf + term of the form [inj x] + *) + cstr : forall x, pred (inj x) + }. + +(** [BinOp Op] declares a source operator [Op: S1 -> S2 -> S3]. + *) +Class BinOp {S1 S2 S3:Type} {T:Type} (Op : S1 -> S2 -> S3) {I1 : InjTyp S1 T} {I2 : InjTyp S2 T} {I3 : InjTyp S3 T} := + mkbop { + (* [TBOp] is the target operator after injection of operands. *) + TBOp : T -> T -> T; + (* [TBOpInj] states the correctness of the injection. *) + TBOpInj : forall (n:S1) (m:S2), inj (Op n m) = TBOp (inj n) (inj m) + }. + +(** [Unop Op] declares a source operator [Op : S1 -> S2]. *) +Class UnOp {S1 S2 T:Type} (Op : S1 -> S2) {I1 : InjTyp S1 T} {I2 : InjTyp S2 T} := + mkuop { + (* [TUOp] is the target operator after injection of operands. *) + TUOp : T -> T; + (* [TUOpInj] states the correctness of the injection. *) + TUOpInj : forall (x:S1), inj (Op x) = TUOp (inj x) + }. + +(** [CstOp Op] declares a source constant [Op : S]. *) +Class CstOp {S T:Type} (Op : S) {I : InjTyp S T} := + mkcst { + (* [TCst] is the target constant. *) + TCst : T; + (* [TCstInj] states the correctness of the injection. *) + TCstInj : inj Op = TCst + }. + +(** In the framework, [Prop] is mapped to [Prop] and the injection is phrased in + terms of [=] instead of [<->]. +*) + +(** [BinRel R] declares the injection of a binary relation. *) +Class BinRel {S:Type} {T:Type} (R : S -> S -> Prop) {I : InjTyp S T} := + mkbrel { + TR : T -> T -> Prop; + TRInj : forall n m : S, R n m <-> TR (@inj _ _ I n) (inj m) + }. + +(** [PropOp Op] declares morphisms for [<->]. + This will be used to deal with e.g. [and], [or],... *) +Class PropOp (Op : Prop -> Prop -> Prop) := + mkprop { + op_iff : forall (p1 p2 q1 q2:Prop), (p1 <-> q1) -> (p2 <-> q2) -> (Op p1 p2 <-> Op q1 q2) + }. + +Class PropUOp (Op : Prop -> Prop) := + mkuprop { + uop_iff : forall (p1 q1 :Prop), (p1 <-> q1) -> (Op p1 <-> Op q1) + }. + + + +(** Once the term is injected, terms can be replaced by their specification. + NB1: The Ltac code is currently limited to (Op: Z -> Z -> Z) + NB2: This is not sufficient to cope with [Z.div] or [Z.mod] + *) +Class BinOpSpec {S T: Type} (Op : T -> T -> T) {I : InjTyp S T} := + mkbspec { + BPred : T -> T -> T -> Prop; + BSpec : forall x y, BPred x y (Op x y) + }. + +Class UnOpSpec {S T: Type} (Op : T -> T) {I : InjTyp S T} := + mkuspec { + UPred : T -> T -> Prop; + USpec : forall x, UPred x (Op x) + }. + +(** After injections, e.g. nat -> Z, + the fact that Z.of_nat x * Z.of_nat y is positive is lost. + This information can be recovered using instance of the [Saturate] class. +*) +Class Saturate {T: Type} (Op : T -> T -> T) := + mksat { + (** Given [Op x y], + - [PArg1] is the pre-condition of x + - [PArg2] is the pre-condition of y + - [PRes] is the pos-condition of (Op x y) *) + PArg1 : T -> Prop; + PArg2 : T -> Prop; + PRes : T -> Prop; + (** [SatOk] states the correctness of the reasoning *) + SatOk : forall x y, PArg1 x -> PArg2 y -> PRes (Op x y) + }. +(* The [ZifyInst.saturate] iterates over all the instances + and for every pattern of the form + [H1 : PArg1 ?x , H2 : PArg2 ?y , T : context[Op ?x ?y] |- _ ] + [H1 : PArg1 ?x , H2 : PArg2 ?y |- context[Op ?x ?y] ] + asserts (SatOK x y H1 H2) *) + +(** The rest of the file is for internal use by the ML tactic. + There are data-structures and lemmas used to inductively construct + the injected terms. *) + +(** The data-structures [injterm] and [injected_prop] + are used to store source and target expressions together + with a correctness proof. *) + +Record injterm {S T: Type} {I : S -> T} := + mkinjterm { source : S ; target : T ; inj_ok : I source = target}. + +Record injprop := + mkinjprop { + source_prop : Prop ; target_prop : Prop ; + injprop_ok : source_prop <-> target_prop}. + +(** Lemmas for building [injterm] and [injprop]. *) + +Definition mkprop_op (Op : Prop -> Prop -> Prop) (POp : PropOp Op) + (p1 :injprop) (p2: injprop) : injprop := + {| source_prop := (Op (source_prop p1) (source_prop p2)) ; + target_prop := (Op (target_prop p1) (target_prop p2)) ; + injprop_ok := (op_iff (source_prop p1) (source_prop p2) (target_prop p1) (target_prop p2) + (injprop_ok p1) (injprop_ok p2)) + |}. + + +Definition mkuprop_op (Op : Prop -> Prop) (POp : PropUOp Op) + (p1 :injprop) : injprop := + {| source_prop := (Op (source_prop p1)) ; + target_prop := (Op (target_prop p1)) ; + injprop_ok := (uop_iff (source_prop p1) (target_prop p1) (injprop_ok p1)) + |}. + + +Lemma mkapp2 (S1 S2 S3 T : Type) (Op : S1 -> S2 -> S3) + {I1 : InjTyp S1 T} {I2 : InjTyp S2 T} {I3 : InjTyp S3 T} + (B : @BinOp S1 S2 S3 T Op I1 I2 I3) + (t1 : @injterm S1 T inj) (t2 : @injterm S2 T inj) + : @injterm S3 T inj. +Proof. + apply (mkinjterm _ _ inj (Op (source t1) (source t2)) (TBOp (target t1) (target t2))). + (rewrite <- inj_ok; + rewrite <- inj_ok; + apply TBOpInj). +Defined. + +Lemma mkapp (S1 S2 T : Type) (Op : S1 -> S2) + {I1 : InjTyp S1 T} + {I2 : InjTyp S2 T} + (B : @UnOp S1 S2 T Op I1 I2 ) + (t1 : @injterm S1 T inj) + : @injterm S2 T inj. +Proof. + apply (mkinjterm _ _ inj (Op (source t1)) (TUOp (target t1))). + (rewrite <- inj_ok; apply TUOpInj). +Defined. + +Lemma mkapp0 (S T : Type) (Op : S) + {I : InjTyp S T} + (B : @CstOp S T Op I) + : @injterm S T inj. +Proof. + apply (mkinjterm _ _ inj Op TCst). + (apply TCstInj). +Defined. + +Lemma mkrel (S T : Type) (R : S -> S -> Prop) + {Inj : InjTyp S T} + (B : @BinRel S T R Inj) + (t1 : @injterm S T inj) (t2 : @injterm S T inj) + : @injprop. +Proof. + apply (mkinjprop (R (source t1) (source t2)) (TR (target t1) (target t2))). + (rewrite <- inj_ok; rewrite <- inj_ok;apply TRInj). +Defined. + +(** Registering constants for use by the plugin *) +Register target_prop as ZifyClasses.target_prop. +Register mkrel as ZifyClasses.mkrel. +Register target as ZifyClasses.target. +Register mkapp2 as ZifyClasses.mkapp2. +Register mkapp as ZifyClasses.mkapp. +Register mkapp0 as ZifyClasses.mkapp0. +Register op_iff as ZifyClasses.op_iff. +Register uop_iff as ZifyClasses.uop_iff. +Register TR as ZifyClasses.TR. +Register TBOp as ZifyClasses.TBOp. +Register TUOp as ZifyClasses.TUOp. +Register TCst as ZifyClasses.TCst. +Register mkprop_op as ZifyClasses.mkprop_op. +Register mkuprop_op as ZifyClasses.mkuprop_op. +Register injprop_ok as ZifyClasses.injprop_ok. +Register inj_ok as ZifyClasses.inj_ok. +Register source as ZifyClasses.source. +Register source_prop as ZifyClasses.source_prop. +Register inj as ZifyClasses.inj. +Register TRInj as ZifyClasses.TRInj. +Register TUOpInj as ZifyClasses.TUOpInj. +Register not as ZifyClasses.not. +Register mkinjterm as ZifyClasses.mkinjterm. +Register eq_refl as ZifyClasses.eq_refl. +Register mkinjprop as ZifyClasses.mkinjprop. +Register iff_refl as ZifyClasses.iff_refl. +Register source_prop as ZifyClasses.source_prop. +Register injprop_ok as ZifyClasses.injprop_ok. +Register iff as ZifyClasses.iff. diff --git a/plugins/micromega/ZifyInst.v b/plugins/micromega/ZifyInst.v new file mode 100644 index 0000000000..3c44113604 --- /dev/null +++ b/plugins/micromega/ZifyInst.v @@ -0,0 +1,445 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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) *) +(************************************************************************) + +(* Instances of [ZifyClasses] for emulating the existing zify. + Each instance is registered using a Add 'class' 'name_of_instance'. + *) + +Require Import Arith Max Min BinInt BinNat Znat Nnat. +Require Import ZifyClasses. +Declare ML Module "zify_plugin". +Open Scope Z_scope. + +(** Propositional logic *) +Instance PropAnd : PropOp and. +Proof. + constructor. + tauto. +Defined. +Add PropOp PropAnd. + +Instance PropOr : PropOp or. +Proof. + constructor. + tauto. +Defined. +Add PropOp PropOr. + +Instance PropArrow : PropOp (fun x y => x -> y). +Proof. + constructor. + intros. + tauto. +Defined. +Add PropOp PropArrow. + +Instance PropIff : PropOp iff. +Proof. + constructor. + intros. + tauto. +Defined. +Add PropOp PropIff. + +Instance PropNot : PropUOp not. +Proof. + constructor. + intros. + tauto. +Defined. +Add PropUOp PropNot. + + +Instance Inj_Z_Z : InjTyp Z Z := + mkinj _ _ (fun x => x) (fun x => True ) (fun _ => I). +Add InjTyp Inj_Z_Z. + +(** Support for nat *) + +Instance Inj_nat_Z : InjTyp nat Z := + mkinj _ _ Z.of_nat (fun x => 0 <= x ) Nat2Z.is_nonneg. +Add InjTyp Inj_nat_Z. + +(* zify_nat_rel *) +Instance Op_ge : BinRel ge := + {| TR := Z.ge; TRInj := Nat2Z.inj_ge |}. +Add BinRel Op_ge. + +Instance Op_lt : BinRel lt := + {| TR := Z.lt; TRInj := Nat2Z.inj_lt |}. +Add BinRel Op_lt. + +Instance Op_gt : BinRel gt := + {| TR := Z.gt; TRInj := Nat2Z.inj_gt |}. +Add BinRel Op_gt. + +Instance Op_le : BinRel le := + {| TR := Z.le; TRInj := Nat2Z.inj_le |}. +Add BinRel Op_le. + +Instance Op_eq_nat : BinRel (@eq nat) := + {| TR := @eq Z ; TRInj := fun x y : nat => iff_sym (Nat2Z.inj_iff x y) |}. +Add BinRel Op_eq_nat. + +(* zify_nat_op *) +Instance Op_plus : BinOp Nat.add := + {| TBOp := Z.add; TBOpInj := Nat2Z.inj_add |}. +Add BinOp Op_plus. + +Instance Op_sub : BinOp Nat.sub := + {| TBOp := fun n m => Z.max 0 (n - m) ; TBOpInj := Nat2Z.inj_sub_max |}. +Add BinOp Op_sub. + +Instance Op_mul : BinOp Nat.mul := + {| TBOp := Z.mul ; TBOpInj := Nat2Z.inj_mul |}. +Add BinOp Op_mul. + +Instance Op_min : BinOp Nat.min := + {| TBOp := Z.min ; TBOpInj := Nat2Z.inj_min |}. +Add BinOp Op_min. + +Instance Op_max : BinOp Nat.max := + {| TBOp := Z.max ; TBOpInj := Nat2Z.inj_max |}. +Add BinOp Op_max. + +Instance Op_pred : UnOp Nat.pred := + {| TUOp := fun n => Z.max 0 (n - 1) ; TUOpInj := Nat2Z.inj_pred_max |}. +Add UnOp Op_pred. + +Instance Op_S : UnOp S := + {| TUOp := fun x => Z.add x 1 ; TUOpInj := Nat2Z.inj_succ |}. +Add UnOp Op_S. + +Instance Op_O : CstOp O := + {| TCst := Z0 ; TCstInj := eq_refl (Z.of_nat 0) |}. + +Instance Op_Z_abs_nat : UnOp Z.abs_nat := + { TUOp := Z.abs ; TUOpInj := Zabs2Nat.id_abs }. +Add UnOp Op_Z_abs_nat. + +(** Support for positive *) + +Instance Inj_pos_Z : InjTyp positive Z := + {| inj := Zpos ; pred := (fun x => 0 < x ) ; cstr := Pos2Z.pos_is_pos |}. +Add InjTyp Inj_pos_Z. + +Instance Op_pos_to_nat : UnOp Pos.to_nat := + {TUOp := (fun x => x); TUOpInj := positive_nat_Z}. +Add UnOp Op_pos_to_nat. + +Instance Inj_N_Z : InjTyp N Z := + mkinj _ _ Z.of_N (fun x => 0 <= x ) N2Z.is_nonneg. +Add InjTyp Inj_N_Z. + + +Instance Op_N_to_nat : UnOp N.to_nat := + { TUOp := fun x => x ; TUOpInj := N_nat_Z }. +Add UnOp Op_N_to_nat. + +(* zify_positive_rel *) + +Instance Op_pos_ge : BinRel Pos.ge := + {| TR := Z.ge; TRInj := fun x y => iff_refl (Z.pos x >= Z.pos y) |}. +Add BinRel Op_pos_ge. + +Instance Op_pos_lt : BinRel Pos.lt := + {| TR := Z.lt; TRInj := fun x y => iff_refl (Z.pos x < Z.pos y) |}. +Add BinRel Op_pos_lt. + +Instance Op_pos_gt : BinRel Pos.gt := + {| TR := Z.gt; TRInj := fun x y => iff_refl (Z.pos x > Z.pos y) |}. +Add BinRel Op_pos_gt. + +Instance Op_pos_le : BinRel Pos.le := + {| TR := Z.le; TRInj := fun x y => iff_refl (Z.pos x <= Z.pos y) |}. +Add BinRel Op_pos_le. + +Instance Op_eq_pos : BinRel (@eq positive) := + {| TR := @eq Z ; TRInj := fun x y => iff_sym (Pos2Z.inj_iff x y) |}. +Add BinRel Op_eq_pos. + +(* zify_positive_op *) + + +Program Instance Op_Z_of_N : UnOp Z.of_N := + { TUOp := (fun x => x) ; TUOpInj := fun x => eq_refl (Z.of_N x) }. +Add UnOp Op_Z_of_N. + +Instance Op_Z_neg : UnOp Z.neg := + { TUOp := Z.opp ; TUOpInj := (fun x => eq_refl (Zneg x))}. +Add UnOp Op_Z_neg. + +Instance Op_Z_pos : UnOp Z.pos := + { TUOp := (fun x => x) ; TUOpInj := (fun x => eq_refl (Z.pos x))}. +Add UnOp Op_Z_pos. + +Instance Op_pos_succ : UnOp Pos.succ := + { TUOp := fun x => x + 1; TUOpInj := Pos2Z.inj_succ }. +Add UnOp Op_pos_succ. + +Instance Op_pos_pred : UnOp Pos.pred := + { TUOp := fun x => Z.max 1 (x - 1) ; + TUOpInj := ltac : + (intros; + rewrite <- Pos.sub_1_r; + apply Pos2Z.inj_sub_max) }. +Add UnOp Op_pos_pred. + +Instance Op_pos_of_succ_nat : UnOp Pos.of_succ_nat := + { TUOp := fun x => x + 1 ; TUOpInj := Zpos_P_of_succ_nat }. +Add UnOp Op_pos_of_succ_nat. + +Program Instance Op_pos_add : BinOp Pos.add := + { TBOp := Z.add ; TBOpInj := ltac: (reflexivity) }. +Add BinOp Op_pos_add. + +Instance Op_pos_sub : BinOp Pos.sub := + { TBOp := fun n m => Z.max 1 (n - m) ;TBOpInj := Pos2Z.inj_sub_max }. +Add BinOp Op_pos_sub. + +Instance Op_pos_mul : BinOp Pos.mul := + { TBOp := Z.mul ; TBOpInj := ltac: (reflexivity) }. +Add BinOp Op_pos_mul. + +Instance Op_pos_min : BinOp Pos.min := + { TBOp := Z.min ; TBOpInj := Pos2Z.inj_min }. +Add BinOp Op_pos_min. + +Instance Op_pos_max : BinOp Pos.max := + { TBOp := Z.max ; TBOpInj := Pos2Z.inj_max }. +Add BinOp Op_pos_max. + +Instance Op_xO : UnOp xO := + { TUOp := fun x => 2 * x ; TUOpInj := ltac: (reflexivity) }. +Add UnOp Op_xO. + +Instance Op_xI : UnOp xI := + { TUOp := fun x => 2 * x + 1 ; TUOpInj := ltac: (reflexivity) }. +Add UnOp Op_xI. + +Instance Op_xH : CstOp xH := + { TCst := 1%Z ; TCstInj := ltac:(reflexivity)}. +Add CstOp Op_xH. + +Instance Op_Z_of_nat : UnOp Z.of_nat:= + { TUOp := fun x => x ; TUOpInj := ltac:(reflexivity) }. +Add UnOp Op_Z_of_nat. + +(* zify_N_rel *) +Instance Op_N_ge : BinRel N.ge := + {| TR := Z.ge ; TRInj := N2Z.inj_ge |}. +Add BinRel Op_N_ge. + +Instance Op_N_lt : BinRel N.lt := + {| TR := Z.lt ; TRInj := N2Z.inj_lt |}. +Add BinRel Op_N_lt. + +Instance Op_N_gt : BinRel N.gt := + {| TR := Z.gt ; TRInj := N2Z.inj_gt |}. +Add BinRel Op_N_gt. + +Instance Op_N_le : BinRel N.le := + {| TR := Z.le ; TRInj := N2Z.inj_le |}. +Add BinRel Op_N_le. + +Instance Op_eq_N : BinRel (@eq N) := + {| TR := @eq Z ; TRInj := fun x y : N => iff_sym (N2Z.inj_iff x y) |}. +Add BinRel Op_eq_N. + +(* zify_N_op *) +Instance Op_N_of_nat : UnOp N.of_nat := + { TUOp := fun x => x ; TUOpInj := nat_N_Z }. +Add UnOp Op_N_of_nat. + +Instance Op_Z_abs_N : UnOp Z.abs_N := + { TUOp := Z.abs ; TUOpInj := N2Z.inj_abs_N }. +Add UnOp Op_Z_abs_N. + +Instance Op_N_pos : UnOp N.pos := + { TUOp := fun x => x ; TUOpInj := ltac:(reflexivity)}. +Add UnOp Op_N_pos. + +Instance Op_N_add : BinOp N.add := + {| TBOp := Z.add ; TBOpInj := N2Z.inj_add |}. +Add BinOp Op_N_add. + +Instance Op_N_min : BinOp N.min := + {| TBOp := Z.min ; TBOpInj := N2Z.inj_min |}. +Add BinOp Op_N_min. + +Instance Op_N_max : BinOp N.max := + {| TBOp := Z.max ; TBOpInj := N2Z.inj_max |}. +Add BinOp Op_N_max. + +Instance Op_N_mul : BinOp N.mul := + {| TBOp := Z.mul ; TBOpInj := N2Z.inj_mul |}. +Add BinOp Op_N_mul. + +Instance Op_N_sub : BinOp N.sub := + {| TBOp := fun x y => Z.max 0 (x - y) ; TBOpInj := N2Z.inj_sub_max|}. +Add BinOp Op_N_sub. + +Instance Op_N_div : BinOp N.div := + {| TBOp := Z.div ; TBOpInj := N2Z.inj_div|}. +Add BinOp Op_N_div. + + + +Instance Op_N_mod : BinOp N.modulo := + {| TBOp := Z.rem ; TBOpInj := N2Z.inj_rem|}. +Add BinOp Op_N_mod. + +Instance Op_N_pred : UnOp N.pred := + { TUOp := fun x => Z.max 0 (x - 1) ; + TUOpInj := + ltac:(intros; rewrite N.pred_sub; apply N2Z.inj_sub_max) }. +Add UnOp Op_N_pred. + +Instance Op_N_succ : UnOp N.succ := + {| TUOp := fun x => x + 1 ; TUOpInj := N2Z.inj_succ |}. +Add UnOp Op_N_succ. + +(** Support for Z - injected to itself *) + +(* zify_Z_rel *) +Instance Op_Z_ge : BinRel Z.ge := + {| TR := Z.ge ; TRInj := fun x y => iff_refl (x>= y)|}. +Add BinRel Op_Z_ge. + +Instance Op_Z_lt : BinRel Z.lt := + {| TR := Z.lt ; TRInj := fun x y => iff_refl (x < y)|}. +Add BinRel Op_Z_lt. + +Instance Op_Z_gt : BinRel Z.gt := + {| TR := Z.gt ;TRInj := fun x y => iff_refl (x > y)|}. +Add BinRel Op_Z_gt. + +Instance Op_Z_le : BinRel Z.le := + {| TR := Z.le ;TRInj := fun x y => iff_refl (x <= y)|}. +Add BinRel Op_Z_le. + +Instance Op_eqZ : BinRel (@eq Z) := + { TR := @eq Z ; TRInj := fun x y => iff_refl (x = y) }. +Add BinRel Op_eqZ. + +Instance Op_Z_add : BinOp Z.add := + { TBOp := Z.add ; TBOpInj := ltac:(reflexivity) }. +Add BinOp Op_Z_add. + +Instance Op_Z_min : BinOp Z.min := + { TBOp := Z.min ; TBOpInj := ltac:(reflexivity) }. +Add BinOp Op_Z_min. + +Instance Op_Z_max : BinOp Z.max := + { TBOp := Z.max ; TBOpInj := ltac:(reflexivity) }. +Add BinOp Op_Z_max. + +Instance Op_Z_mul : BinOp Z.mul := + { TBOp := Z.mul ; TBOpInj := ltac:(reflexivity) }. +Add BinOp Op_Z_mul. + +Instance Op_Z_sub : BinOp Z.sub := + { TBOp := Z.sub ; TBOpInj := ltac:(reflexivity) }. +Add BinOp Op_Z_sub. + +Instance Op_Z_div : BinOp Z.div := + { TBOp := Z.div ; TBOpInj := ltac:(reflexivity) }. +Add BinOp Op_Z_div. + +Instance Op_Z_mod : BinOp Z.modulo := + { TBOp := Z.modulo ; TBOpInj := ltac:(reflexivity) }. +Add BinOp Op_Z_mod. + +Instance Op_Z_rem : BinOp Z.rem := + { TBOp := Z.rem ; TBOpInj := ltac:(reflexivity) }. +Add BinOp Op_Z_rem. + +Instance Op_Z_quot : BinOp Z.quot := + { TBOp := Z.quot ; TBOpInj := ltac:(reflexivity) }. +Add BinOp Op_Z_quot. + +Instance Op_Z_succ : UnOp Z.succ := + { TUOp := fun x => x + 1 ; TUOpInj := ltac:(reflexivity) }. +Add UnOp Op_Z_succ. + +Instance Op_Z_pred : UnOp Z.pred := + { TUOp := fun x => x - 1 ; TUOpInj := ltac:(reflexivity) }. +Add UnOp Op_Z_pred. + +Instance Op_Z_opp : UnOp Z.opp := + { TUOp := Z.opp ; TUOpInj := ltac:(reflexivity) }. +Add UnOp Op_Z_opp. + +Instance Op_Z_abs : UnOp Z.abs := + { TUOp := Z.abs ; TUOpInj := ltac:(reflexivity) }. +Add UnOp Op_Z_abs. + +Instance Op_Z_sgn : UnOp Z.sgn := + { TUOp := Z.sgn ; TUOpInj := ltac:(reflexivity) }. +Add UnOp Op_Z_sgn. + +Instance Op_Z_pow_pos : BinOp Z.pow_pos := + { TBOp := Z.pow ; TBOpInj := ltac:(reflexivity) }. +Add BinOp Op_Z_pow_pos. + +Lemma of_nat_to_nat_eq : forall x, Z.of_nat (Z.to_nat x) = Z.max 0 x. +Proof. + destruct x. + - reflexivity. + - rewrite Z2Nat.id. + reflexivity. + compute. congruence. + - reflexivity. +Qed. + +Instance Op_Z_to_nat : UnOp Z.to_nat := + { TUOp := fun x => Z.max 0 x ; TUOpInj := of_nat_to_nat_eq }. +Add UnOp Op_Z_to_nat. + +(** Specification of derived operators over Z *) + +Instance ZmaxSpec : BinOpSpec Z.max := + {| BPred := fun n m r => n < m /\ r = m \/ m <= n /\ r = n ; BSpec := Z.max_spec|}. +Add Spec ZmaxSpec. + +Instance ZminSpec : BinOpSpec Z.min := + {| BPred := fun n m r : Z => n < m /\ r = n \/ m <= n /\ r = m ; + BSpec := Z.min_spec|}. +Add Spec ZminSpec. + +Instance ZsgnSpec : UnOpSpec Z.sgn := + {| UPred := fun n r : Z => 0 < n /\ r = 1 \/ 0 = n /\ r = 0 \/ n < 0 /\ r = - (1) ; + USpec := Z.sgn_spec|}. +Add Spec ZsgnSpec. + +Instance ZabsSpec : UnOpSpec Z.abs := + {| UPred := fun n r: Z => 0 <= n /\ r = n \/ n < 0 /\ r = - n ; + USpec := Z.abs_spec|}. +Add Spec ZabsSpec. + +(** Saturate positivity constraints *) + +Instance SatProd : Saturate Z.mul := + {| + PArg1 := fun x => 0 <= x; + PArg2 := fun y => 0 <= y; + PRes := fun r => 0 <= r; + SatOk := Z.mul_nonneg_nonneg + |}. +Add Saturate SatProd. + +Instance SatProdPos : Saturate Z.mul := + {| + PArg1 := fun x => 0 < x; + PArg2 := fun y => 0 < y; + PRes := fun r => 0 < r; + SatOk := Z.mul_pos_pos + |}. +Add Saturate SatProdPos. diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 5cc2c2e061..ceb651abed 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -27,7 +27,7 @@ open Context open Tactypes (** - * Debug flag + * Debug flag *) let debug = false @@ -39,7 +39,7 @@ let max_depth = max_int (* Search limit for provers over Q R *) let lra_proof_depth = ref max_depth - + (* Search limit for provers over Z *) let lia_enum = ref true let lia_proof_depth = ref max_depth @@ -50,10 +50,8 @@ let get_lia_option () = let get_lra_option () = !lra_proof_depth - - let () = - + let int_opt l vref = { optdepr = false; @@ -63,7 +61,7 @@ let () = optwrite = (fun x -> vref := (match x with None -> max_depth | Some v -> v)) } in - let lia_enum_opt = + let lia_enum_opt = { optdepr = false; optname = "Lia Enum"; @@ -90,6 +88,7 @@ let () = optwrite = (fun x -> Certificate.dump_file := x) } in + let () = declare_bool_option solver_opt in let () = declare_stringopt_option dump_file_opt in let () = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in @@ -97,7 +96,7 @@ let () = let () = declare_bool_option lia_enum_opt in () - + (** * Initialize a tag type to the Tag module declaration (see Mutils). *) @@ -167,8 +166,8 @@ struct let logic_dir = ["Coq";"Logic";"Decidable"] - let mic_modules = - [ + let mic_modules = + [ ["Coq";"Lists";"List"]; ["Coq"; "micromega";"ZMicromega"]; ["Coq"; "micromega";"Tauto"]; @@ -419,7 +418,7 @@ struct | _ -> raise ParseError (* Access the Micromega module *) - + (* parse/dump/print from numbers up to expressions and formulas *) let rec parse_nat sigma term = @@ -437,15 +436,15 @@ struct | Mc.S p -> EConstr.mkApp(Lazy.force coq_S,[| dump_nat p |]) let rec parse_positive sigma term = - let (i,c) = get_left_construct sigma term in + let (i,c) = get_left_construct sigma term in match i with - | 1 -> Mc.XI (parse_positive sigma c.(0)) - | 2 -> Mc.XO (parse_positive sigma c.(0)) - | 3 -> Mc.XH - | i -> raise ParseError + | 1 -> Mc.XI (parse_positive sigma c.(0)) + | 2 -> Mc.XO (parse_positive sigma c.(0)) + | 3 -> Mc.XH + | i -> raise ParseError let rec dump_positive x = - match x with + match x with | Mc.XH -> Lazy.force coq_xH | Mc.XO p -> EConstr.mkApp(Lazy.force coq_xO,[| dump_positive p |]) | Mc.XI p -> EConstr.mkApp(Lazy.force coq_xI,[| dump_positive p |]) @@ -453,14 +452,14 @@ struct let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x) let dump_n x = - match x with + match x with | Mc.N0 -> Lazy.force coq_N0 | Mc.Npos p -> EConstr.mkApp(Lazy.force coq_Npos,[| dump_positive p|]) (** [is_ground_term env sigma term] holds if the term [term] is an instance of the typeclass [DeclConstant.GT term] i.e. built from user-defined constants and functions. - NB: This mechanism is used to customise the reification process to decide + NB: This mechanism can be used to customise the reification process to decide what to consider as a constant (see [parse_constant]) *) @@ -468,10 +467,10 @@ struct match EConstr.kind evd t with | Const _ | Construct _ -> (* Restrict typeclass resolution to trivial cases *) begin - let typ = Retyping.get_type_of env evd t in - try - ignore (Typeclasses.resolve_one_typeclass env evd (EConstr.mkApp(Lazy.force coq_DeclaredConstant,[| typ;t|]))) ; true - with Not_found -> false + let typ = Retyping.get_type_of env evd t in + try + ignore (Typeclasses.resolve_one_typeclass env evd (EConstr.mkApp(Lazy.force coq_DeclaredConstant,[| typ;t|]))) ; true + with Not_found -> false end | _ -> false @@ -485,12 +484,12 @@ struct let parse_z sigma term = - let (i,c) = get_left_construct sigma term in + let (i,c) = get_left_construct sigma term in match i with - | 1 -> Mc.Z0 - | 2 -> Mc.Zpos (parse_positive sigma c.(0)) - | 3 -> Mc.Zneg (parse_positive sigma c.(0)) - | i -> raise ParseError + | 1 -> Mc.Z0 + | 2 -> Mc.Zpos (parse_positive sigma c.(0)) + | 3 -> Mc.Zneg (parse_positive sigma c.(0)) + | i -> raise ParseError let dump_z x = match x with @@ -512,7 +511,7 @@ struct | _ -> raise ParseError - let rec pp_Rcst o cst = + let rec pp_Rcst o cst = match cst with | Mc.C0 -> output_string o "C0" | Mc.C1 -> output_string o "C1" @@ -526,9 +525,9 @@ struct | Mc.COpp t -> Printf.fprintf o "(- %a)" pp_Rcst t - let rec dump_Rcst cst = + let rec dump_Rcst cst = match cst with - | Mc.C0 -> Lazy.force coq_C0 + | Mc.C0 -> Lazy.force coq_C0 | Mc.C1 -> Lazy.force coq_C1 | Mc.CQ q -> EConstr.mkApp(Lazy.force coq_CQ, [| dump_q q |]) | Mc.CZ z -> EConstr.mkApp(Lazy.force coq_CZ, [| dump_z z |]) @@ -682,7 +681,7 @@ struct type gl = { env : Environ.env; sigma : Evd.evar_map } - let is_convertible gl t1 t2 = + let is_convertible gl t1 t2 = Reductionops.is_conv gl.env gl.sigma t1 t2 let parse_zop gl (op,args) = @@ -778,7 +777,7 @@ struct | e::l -> if EConstr.eq_constr evd e v then n - else _get_rank l (n+1) in + else _get_rank l (n+1) in _get_rank env.vars 1 let elements env = env.vars @@ -810,7 +809,7 @@ struct let parse_variable env term = let (env,n) = Env.compute_rank_add env term in - (Mc.PEX n , env) in + (Mc.PEX n , env) in let rec parse_expr env term = let combine env op (t1,t2) = @@ -826,12 +825,12 @@ struct match EConstr.kind gl.sigma t with | Const c -> ( match assoc_ops gl.sigma t ops_spec with - | Binop f -> combine env f (args.(0),args.(1)) + | Binop f -> combine env f (args.(0),args.(1)) | Opp -> let (expr,env) = parse_expr env args.(0) in (Mc.PEopp expr, env) | Power -> begin - try + try let (expr,env) = parse_expr env args.(0) in let power = (parse_exp expr args.(1)) in (power , env) @@ -844,9 +843,9 @@ struct then (Printf.printf "unknown op: %s\n" s; flush stdout;); let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env) ) - | _ -> parse_variable env term + | _ -> parse_variable env term ) - | _ -> parse_variable env term in + | _ -> parse_variable env term in parse_expr env term let zop_spec = @@ -920,14 +919,18 @@ struct Therefore, there is a specific parser for constant over R *) - let rconst_assoc = - [ + let rconst_assoc = + [ coq_Rplus , (fun x y -> Mc.CPlus(x,y)) ; - coq_Rminus , (fun x y -> Mc.CMinus(x,y)) ; - coq_Rmult , (fun x y -> Mc.CMult(x,y)) ; + coq_Rminus , (fun x y -> Mc.CMinus(x,y)) ; + coq_Rmult , (fun x y -> Mc.CMult(x,y)) ; (* coq_Rdiv , (fun x y -> Mc.CMult(x,Mc.CInv y)) ;*) ] + + + + let rconstant gl term = let sigma = gl.sigma in @@ -950,12 +953,12 @@ struct f a b with ParseError -> - match op with - | op when EConstr.eq_constr sigma op (Lazy.force coq_Rinv) -> + match op with + | op when EConstr.eq_constr sigma op (Lazy.force coq_Rinv) -> let arg = rconstant args.(0) in if Mc.qeq_bool (Mc.q_of_Rcst arg) {Mc.qnum = Mc.Z0 ; Mc.qden = Mc.XH} then raise ParseError (* This is a division by zero -- no semantics *) - else Mc.CInv(arg) + else Mc.CInv(arg) | op when EConstr.eq_constr sigma op (Lazy.force coq_Rpower) -> Mc.CPow(rconstant args.(0) , Mc.Inr (parse_more_constant nconstant gl args.(1))) | op when EConstr.eq_constr sigma op (Lazy.force coq_IQR) -> @@ -963,18 +966,19 @@ struct | op when EConstr.eq_constr sigma op (Lazy.force coq_IZR) -> Mc.CZ (parse_more_constant zconstant gl args.(0)) | _ -> raise ParseError - end + end | _ -> raise ParseError in rconstant term + let rconstant gl term = if debug then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env gl.env gl.sigma term ++ fnl ()); let res = rconstant gl term in - if debug then - (Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ; + if debug then + (Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ; res @@ -1034,20 +1038,26 @@ struct (** * This is the big generic function for formula parsers. *) - + + let is_prop env sigma term = + let sort = Retyping.get_sort_of env sigma term in + Sorts.is_prop sort + let parse_formula gl parse_atom env tg term = let sigma = gl.sigma in + let is_prop term = is_prop gl.env gl.sigma term in + let parse_atom env tg t = try let (at,env) = parse_atom env t gl in (Mc.A(at,(tg,t)), env,Tag.next tg) - with e when CErrors.noncritical e -> (Mc.X(t),env,tg) in + with ParseError -> + if is_prop t + then (Mc.X(t),env,tg) + else raise ParseError + in - let is_prop term = - let sort = Retyping.get_sort_of gl.env gl.sigma term in - Sorts.is_prop sort in - let rec xparse_formula env tg term = match EConstr.kind sigma term with | App(l,rst) -> @@ -1106,7 +1116,7 @@ struct doit (doit env f1) f2 | N f -> doit env f in - + doit (Env.empty gl) form) let var_env_of_formula form = @@ -1118,7 +1128,7 @@ struct ISet.union (vars_of_expr e1) (vars_of_expr e2) | Mc.PEopp e | Mc.PEpow(e,_)-> vars_of_expr e in - + let vars_of_atom {Mc.flhs ; Mc.fop; Mc.frhs} = ISet.union (vars_of_expr flhs) (vars_of_expr frhs) in Mc.( @@ -1129,10 +1139,10 @@ struct | N f -> doit f in doit form) - - + + type 'cst dump_expr = (* 'cst is the type of the syntactic constants *) { interp_typ : EConstr.constr; @@ -1169,12 +1179,12 @@ let dump_qexpr = lazy dump_mul = Lazy.force coq_Qmult; dump_pow = Lazy.force coq_Qpower; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))); - dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) qop_table + dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) qop_table } -let rec dump_Rcst_as_R cst = +let rec dump_Rcst_as_R cst = match cst with - | Mc.C0 -> Lazy.force coq_R0 + | Mc.C0 -> Lazy.force coq_R0 | Mc.C1 -> Lazy.force coq_R1 | Mc.CQ q -> EConstr.mkApp(Lazy.force coq_IQR, [| dump_q q |]) | Mc.CZ z -> EConstr.mkApp(Lazy.force coq_IZR, [| dump_z z |]) @@ -1201,18 +1211,11 @@ let dump_rexpr = lazy dump_mul = Lazy.force coq_Rmult; dump_pow = Lazy.force coq_Rpower; dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n))); - dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) rop_table + dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) rop_table } - - -(** [make_goal_of_formula depxr vars props form] where - - vars is an environment for the arithmetic variables occurring in form - - props is an environment for the propositions occurring in form - @return a goal where all the variables and propositions of the formula are quantified -*) let prodn n env b = let rec prodrec = function @@ -1222,17 +1225,29 @@ let prodn n env b = in prodrec (n,env,b) +(** [make_goal_of_formula depxr vars props form] where + - vars is an environment for the arithmetic variables occurring in form + - props is an environment for the propositions occurring in form + @return a goal where all the variables and propositions of the formula are quantified + +*) + let make_goal_of_formula gl dexpr form = let vars_idx = List.mapi (fun i v -> (v, i+1)) (ISet.elements (var_env_of_formula form)) in (* List.iter (fun (v,i) -> Printf.fprintf stdout "var %i has index %i\n" v i) vars_idx ;*) - + let props = prop_env_of_formula gl form in - let vars_n = List.map (fun (_,i) -> (Names.Id.of_string (Printf.sprintf "__x%i" i)) , dexpr.interp_typ) vars_idx in - let props_n = List.mapi (fun i _ -> (Names.Id.of_string (Printf.sprintf "__p%i" (i+1))) , EConstr.mkProp) (Env.elements props) in + let fresh_var str i = Names.Id.of_string (str^(string_of_int i)) in + + let fresh_prop str i = + Names.Id.of_string (str^(string_of_int i)) in + + let vars_n = List.map (fun (_,i) -> fresh_var "__x" i, dexpr.interp_typ) vars_idx in + let props_n = List.mapi (fun i _ -> fresh_prop "__p" (i+1) , EConstr.mkProp) (Env.elements props) in let var_name_pos = List.map2 (fun (idx,_) (id,_) -> id,idx) vars_idx vars_n in @@ -1251,16 +1266,16 @@ let make_goal_of_formula gl dexpr form = | Mc.PEpow(e,n) -> EConstr.mkApp(dexpr.dump_pow, [| dump_expr e; dexpr.dump_pow_arg n|]) in dump_expr e in - + let mkop op e1 e2 = try EConstr.mkApp(List.assoc op dexpr.dump_op, [| e1; e2|]) with Not_found -> EConstr.mkApp(Lazy.force coq_Eq,[|dexpr.interp_typ ; e1 ;e2|]) in - + let dump_cstr i { Mc.flhs ; Mc.fop ; Mc.frhs } = mkop fop (dump_expr i flhs) (dump_expr i frhs) in - + let rec xdump pi xi f = match f with | Mc.TT -> Lazy.force coq_True @@ -1271,16 +1286,16 @@ let make_goal_of_formula gl dexpr form = | Mc.N(x) -> EConstr.mkArrow (xdump pi xi x) Sorts.Relevant (Lazy.force coq_False) | Mc.A(x,_) -> dump_cstr xi x | Mc.X(t) -> let idx = Env.get_rank props t in - EConstr.mkRel (pi+idx) in - + EConstr.mkRel (pi+idx) in + let nb_vars = List.length vars_n in - let nb_props = List.length props_n in + let nb_props = List.length props_n in (* Printf.fprintf stdout "NBProps : %i\n" nb_props ;*) - + let subst_prop p = let idx = Env.get_rank props p in - EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx)) in + EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx)) in let form' = Mc.mapX subst_prop form in @@ -1288,13 +1303,13 @@ let make_goal_of_formula gl dexpr form = (prodn nb_vars (List.map (fun (x,y) -> Name.Name x,y) vars_n) (xdump (List.length vars_n) 0 form)), List.rev props_n, List.rev var_name_pos,form') - + (** * Given a conclusion and a list of affectations, rebuild a term prefixed by * the appropriate letins. * TODO: reverse the list of bindings! *) - + let set l concl = let rec xset acc = function | [] -> acc @@ -1306,7 +1321,7 @@ let make_goal_of_formula gl dexpr form = xset concl l end (** - * MODULE END: M + * MODULE END: M *) open M @@ -1317,14 +1332,14 @@ let coq_Branch = let coq_Elt = lazy (gen_constant_in_modules "VarMap" [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Elt") -let coq_Empty = +let coq_Empty = lazy (gen_constant_in_modules "VarMap" [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty") -let coq_VarMap = +let coq_VarMap = lazy (gen_constant_in_modules "VarMap" [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t") - + let rec dump_varmap typ m = match m with @@ -1337,9 +1352,9 @@ let rec dump_varmap typ m = let vm_of_list env = match env with | [] -> Mc.Empty - | (d,_)::_ -> + | (d,_)::_ -> List.fold_left (fun vm (c,i) -> - Mc.vm_add d (CamlToCoq.positive i) c vm) Mc.Empty env + Mc.vm_add d (CamlToCoq.positive i) c vm) Mc.Empty env let rec dump_proof_term = function | Micromega.DoneProof -> Lazy.force coq_doneProof @@ -1347,12 +1362,12 @@ let rec dump_proof_term = function EConstr.mkApp(Lazy.force coq_ratProof, [| dump_psatz coq_Z dump_z cone; dump_proof_term rst|]) | Micromega.CutProof(cone,prf) -> EConstr.mkApp(Lazy.force coq_cutProof, - [| dump_psatz coq_Z dump_z cone ; - dump_proof_term prf|]) + [| dump_psatz coq_Z dump_z cone ; + dump_proof_term prf|]) | Micromega.EnumProof(c1,c2,prfs) -> EConstr.mkApp (Lazy.force coq_enumProof, - [| dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ; - dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |]) + [| dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ; + dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |]) let rec size_of_psatz = function @@ -1369,8 +1384,8 @@ let rec size_of_pf = function | Micromega.CutProof(p,a) -> (size_of_pf a) + (size_of_psatz p) | Micromega.EnumProof(p1,p2,l) -> (size_of_psatz p1) + (size_of_psatz p2) + (List.fold_left (fun acc p -> size_of_pf p + acc) 0 l) -let dump_proof_term t = - if debug then Printf.printf "dump_proof_term %i\n" (size_of_pf t) ; +let dump_proof_term t = + if debug then Printf.printf "dump_proof_term %i\n" (size_of_pf t) ; dump_proof_term t @@ -1384,7 +1399,7 @@ let rec pp_proof_term o = function | Micromega.CutProof(cone,rst) -> Printf.fprintf o "C[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst | Micromega.EnumProof(c1,c2,rst) -> Printf.fprintf o "EP[%a,%a,%a]" - (pp_psatz pp_z) c1 (pp_psatz pp_z) c2 + (pp_psatz pp_z) c1 (pp_psatz pp_z) c2 (pp_list "[" "]" pp_proof_term) rst let rec parse_hyps gl parse_arith env tg hyps = @@ -1392,10 +1407,14 @@ let rec parse_hyps gl parse_arith env tg hyps = | [] -> ([],env,tg) | (i,t)::l -> let (lhyps,env,tg) = parse_hyps gl parse_arith env tg l in - try - let (c,env,tg) = parse_formula gl parse_arith env tg t in - ((i,c)::lhyps, env,tg) - with e when CErrors.noncritical e -> (lhyps,env,tg) + if is_prop gl.env gl.sigma t + then + try + let (c,env,tg) = parse_formula gl parse_arith env tg t in + ((i,c)::lhyps, env,tg) + with ParseError -> (lhyps,env,tg) + else (lhyps,env,tg) + let parse_goal gl parse_arith (env:Env.t) hyps term = let (f,env,tg) = parse_formula gl parse_arith env (Tag.from 0) term in @@ -1408,8 +1427,8 @@ let parse_goal gl parse_arith (env:Env.t) hyps term = type ('synt_c, 'prf) domain_spec = { typ : EConstr.constr; (* is the type of the interpretation domain - Z, Q, R*) coeff : EConstr.constr ; (* is the type of the syntactic coeffs - Z , Q , Rcst *) - dump_coeff : 'synt_c -> EConstr.constr ; - proof_typ : EConstr.constr ; + dump_coeff : 'synt_c -> EConstr.constr ; + proof_typ : EConstr.constr ; dump_proof : 'prf -> EConstr.constr } @@ -1465,7 +1484,7 @@ let pre_processZ mt f = Mc.bound_problem_fr tag_of_var mt f (** Naive topological sort of constr according to the subterm-ordering *) -(* An element is minimal x is minimal w.r.t y if +(* An element is minimal x is minimal w.r.t y if x <= y or (x and y are incomparable) *) (** @@ -1473,7 +1492,7 @@ let pre_processZ mt f = * witness. *) -let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*) = +let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*) = (* let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *) let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in @@ -1490,7 +1509,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* ("__wit", cert, cert_typ) ] (Tacmach.New.pf_concl gl)) - ] + ] end @@ -1511,7 +1530,7 @@ type ('option,'a,'prf,'model) prover = { } - + (** * Given a prover and a disjunction of atoms, find a proof of any of * the atoms. Returns an (optional) pair of a proof and a prover @@ -1545,7 +1564,13 @@ let witness_list prover l = | Prf w -> Prf (w::l) in xwitness_list l -let witness_list_tags = witness_list +let witness_list_tags p g = witness_list p g +(* let t1 = System.get_time () in + let res = witness_list p g in + let t2 = System.get_time () in + Feedback.msg_info Pp.(str "Witness generation "++int (List.length g) ++ str " "++System.fmt_time_difference t1 t2) ; + res + *) (** * Prune the proof object, according to the 'diff' between two cnf formulas. @@ -1593,6 +1618,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = if debug then begin Printf.printf "CNFRES\n"; flush stdout; + Printf.printf "CNFOLD %a\n" pp_cnf_tag cnf_ff; List.iter (fun (cl,(prf,prover)) -> let hyps_idx = prover.hyps prf in let hyps = selecti hyps_idx cl in @@ -1619,37 +1645,27 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = * variables. See the Tag module in mutils.ml for more. *) -let abstract_formula hyps f = - Mc.( - let rec xabs f = - match f with - | X c -> X c - | A(a,(t,term)) -> if TagSet.mem t hyps then A(a,(t,term)) else X(term) - | Cj(f1,f2) -> - (match xabs f1 , xabs f2 with - | X a1 , X a2 -> X (EConstr.mkApp(Lazy.force coq_and, [|a1;a2|])) - | f1 , f2 -> Cj(f1,f2) ) - | D(f1,f2) -> - (match xabs f1 , xabs f2 with - | X a1 , X a2 -> X (EConstr.mkApp(Lazy.force coq_or, [|a1;a2|])) - | f1 , f2 -> D(f1,f2) ) - | N(f) -> - (match xabs f with - | X a -> X (EConstr.mkApp(Lazy.force coq_not, [|a|])) - | f -> N f) - | I(f1,hyp,f2) -> - (match xabs f1 , hyp, xabs f2 with - | X a1 , Some _ , af2 -> af2 - | X a1 , None , X a2 -> X (EConstr.mkArrow a1 Sorts.Relevant a2) - | af1 , _ , af2 -> I(af1,hyp,af2) - ) - | FF -> FF - | TT -> TT - in xabs f) + + +let abstract_formula : TagSet.t -> 'a formula -> 'a formula = + fun hyps f -> + let to_constr = Mc.({ + mkTT = Lazy.force coq_True; + mkFF = Lazy.force coq_False; + mkA = (fun a (tg, t) -> t); + mkCj = (let coq_and = Lazy.force coq_and in + fun x y -> EConstr.mkApp(coq_and,[|x;y|])); + mkD = (let coq_or = Lazy.force coq_or in + fun x y -> EConstr.mkApp(coq_or,[|x;y|])); + mkI = (fun x y -> EConstr.mkArrow x Sorts.Relevant y); + mkN = (let coq_not = Lazy.force coq_not in + (fun x -> EConstr.mkApp(coq_not,[|x|]))) + }) in + Mc.abst_form to_constr (fun (t,_) -> TagSet.mem t hyps) true f (* [abstract_wrt_formula] is used in contexts whre f1 is already an abstraction of f2 *) -let rec abstract_wrt_formula f1 f2 = +let rec abstract_wrt_formula f1 f2 = Mc.( match f1 , f2 with | X c , _ -> X c @@ -1669,13 +1685,13 @@ let rec abstract_wrt_formula f1 f2 = exception CsdpNotFound - + (** * This is the core of Micromega: apply the prover, analyze the result and * prune unused fomulas, and finally modify the proof state. *) -let formula_hyps_concl hyps concl = +let formula_hyps_concl hyps concl = List.fold_right (fun (id,f) (cc,ids) -> match f with @@ -1684,6 +1700,14 @@ let formula_hyps_concl hyps concl = hyps (concl,[]) +(* let time str f x = + let t1 = System.get_time () in + let res = f x in + let t2 = System.get_time () in + Feedback.msg_info (Pp.str str ++ Pp.str " " ++ System.fmt_time_difference t1 t2) ; + res + *) + let micromega_tauto pre_process cnf spec prover env (polys1: (Names.Id.t * 'cst formula) list) (polys2: 'cst formula) gl = (* Express the goal as one big implication *) @@ -1691,34 +1715,36 @@ let micromega_tauto pre_process cnf spec prover env (polys1: (Names.Id.t * 'cst let mt = CamlToCoq.positive (max_tag ff) in (* Construction of cnf *) - let pre_ff = (pre_process mt ff) in + let pre_ff = pre_process mt (ff:'a formula) in let (cnf_ff,cnf_ff_tags) = cnf pre_ff in match witness_list_tags prover cnf_ff with | Model m -> Model m | Unknown -> Unknown | Prf res -> (*Printf.printf "\nList %i" (List.length `res); *) - let hyps = List.fold_left + let deps = List.fold_left (fun s (cl,(prf,p)) -> let tags = ISet.fold (fun i s -> let t = fst (snd (List.nth cl i)) in if debug then (Printf.fprintf stdout "T : %i -> %a" i Tag.pp t) ; (*try*) TagSet.add t s (* with Invalid_argument _ -> s*)) (p.hyps prf) TagSet.empty in - TagSet.union s tags) (List.fold_left (fun s i -> TagSet.add i s) TagSet.empty (List.map fst cnf_ff_tags)) (List.combine cnf_ff res) in + TagSet.union s tags) (List.fold_left (fun s (i,_) -> TagSet.add i s) TagSet.empty cnf_ff_tags) (List.combine cnf_ff res) in - let ff' = abstract_formula hyps ff in + let ff' = abstract_formula deps ff in - let pre_ff' = pre_process mt ff' in - let cnf_ff',_ = cnf pre_ff' in + let pre_ff' = pre_process mt ff' in + let (cnf_ff',_) = cnf pre_ff' in if debug then begin output_string stdout "\n"; Printf.printf "TForm : %a\n" pp_formula ff ; flush stdout; + Printf.printf "CNF : %a\n" pp_cnf_tag cnf_ff ; flush stdout; Printf.printf "TFormAbs : %a\n" pp_formula ff' ; flush stdout; Printf.printf "TFormPre : %a\n" pp_formula pre_ff ; flush stdout; Printf.printf "TFormPreAbs : %a\n" pp_formula pre_ff' ; flush stdout; + Printf.printf "CNF : %a\n" pp_cnf_tag cnf_ff' ; flush stdout; end; (* Even if it does not work, this does not mean it is not provable @@ -1730,6 +1756,7 @@ let micromega_tauto pre_process cnf spec prover env (polys1: (Names.Id.t * 'cst | None -> failwith "abstraction is wrong" | Some res -> () end ; *) + let res' = compact_proofs cnf_ff res cnf_ff' in let (ff',res',ids) = (ff',res', Mc.ids_of_formula ff') in @@ -1749,12 +1776,22 @@ let micromega_tauto pre_process cnf spec prover env (polys1: (Names.Id.t * 'cst (** * Parse the proof environment, and call micromega_tauto *) - let fresh_id avoid id gl = Tactics.fresh_id_in_env avoid id (Proofview.Goal.env gl) +let clear_all_no_check = + Proofview.Goal.enter begin fun gl -> + let concl = Tacmach.New.pf_concl gl in + let env = Environ.reset_with_named_context Environ.empty_named_context_val (Tacmach.New.pf_env gl) in + (Refine.refine ~typecheck:false begin fun sigma -> + Evarutil.new_evar env sigma ~principal:true concl + end) + end + + + let micromega_gen - parse_arith + parse_arith pre_process cnf spec dumpexpr prover tac = @@ -1771,52 +1808,48 @@ let micromega_gen if debug then Feedback.msg_debug (Pp.str "Env " ++ (Env.pp gl0 env)) ; - + match micromega_tauto pre_process cnf spec prover env hyps concl gl0 with | Unknown -> flush stdout ; Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") | Model(m,e) -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") | Prf (ids,ff',res') -> let (arith_goal,props,vars,ff_arith) = make_goal_of_formula gl0 dumpexpr ff' in - let intro (id,_) = Tactics.introduction id in + let intro (id,_) = Tactics.introduction id in let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in - let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in + (* let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in*) let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in - let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in + let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in - let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; + let tac_arith = Tacticals.New.tclTHENLIST [ clear_all_no_check ;intro_props ; intro_vars ; micromega_order_change spec res' (EConstr.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env' ff_arith ] in let goal_props = List.rev (Env.elements (prop_env_of_formula gl0 ff')) in - let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in - - let arith_args = goal_props @ goal_vars in + let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in - let kill_arith = - Tacticals.New.tclTHEN - (Tactics.keep []) - ((*Tactics.tclABSTRACT None*) - (Tacticals.New.tclTHEN tac_arith tac)) in + let arith_args = goal_props @ goal_vars in - Tacticals.New.tclTHENS - (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal) - [ - kill_arith; - (Tacticals.New.tclTHENLIST - [(Tactics.generalize (List.map EConstr.mkVar ids)); - Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args)) - ] ) - ] + let kill_arith = Tacticals.New.tclTHEN tac_arith tac in +(* +(*tclABSTRACT fails in certain corner cases.*) +Tacticals.New.tclTHEN + clear_all_no_check + (Abstract.tclABSTRACT ~opaque:false None (Tacticals.New.tclTHEN tac_arith tac)) in *) + + Tacticals.New.tclTHEN + (Tactics.assert_by (Names.Name goal_name) arith_goal + ((*Proofview.tclTIME (Some "kill_arith")*) kill_arith)) + ((*Proofview.tclTIME (Some "apply_arith") *) + (Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args@(List.map EConstr.mkVar ids))))) with - | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout") | CsdpNotFound -> flush stdout ; - Tacticals.New.tclFAIL 0 (Pp.str + Tacticals.New.tclFAIL 0 (Pp.str (" Skipping what remains of this tactic: the complexity of the goal requires " - ^ "the use of a specialized external tool called csdp. \n\n" + ^ "the use of a specialized external tool called csdp. \n\n" ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) | x -> begin if debug then Tacticals.New.tclFAIL 0 (Pp.str (Printexc.get_backtrace ())) @@ -1824,13 +1857,13 @@ let micromega_gen end end -let micromega_order_changer cert env ff = +let micromega_order_changer cert env ff = (*let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *) let coeff = Lazy.force coq_Rcst in let dump_coeff = dump_Rcst in let typ = Lazy.force coq_R in let cert_typ = (EConstr.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in - + let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[| coeff|])) in let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in let vm = dump_varmap (typ) (vm_of_list env) in @@ -1843,7 +1876,7 @@ let micromega_order_changer cert env ff = ("__ff", ff, EConstr.mkApp(Lazy.force coq_Formula, [|formula_typ |])); ("__varmap", vm, EConstr.mkApp (gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|])); + [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|])); ("__wit", cert, cert_typ) ] (Tacmach.New.pf_concl gl))); @@ -1870,68 +1903,62 @@ let micromega_genr prover tac = let (hyps,concl,env) = parse_goal gl0 parse_arith (Env.empty gl0) hyps concl in let env = Env.elements env in let spec = Lazy.force spec in - + let hyps' = List.map (fun (n,f) -> (n, Mc.map_bformula (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in let concl' = Mc.map_bformula (Micromega.map_Formula Micromega.q_of_Rcst) concl in - + match micromega_tauto (fun _ x -> x) Mc.cnfQ spec prover env hyps' concl' gl0 with | Unknown | Model _ -> flush stdout ; Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") | Prf (ids,ff',res') -> - let (ff,ids) = formula_hyps_concl - (List.filter (fun (n,_) -> List.mem n ids) hyps) concl in + let (ff,ids) = formula_hyps_concl + (List.filter (fun (n,_) -> List.mem n ids) hyps) concl in + let ff' = abstract_wrt_formula ff' ff in let (arith_goal,props,vars,ff_arith) = make_goal_of_formula gl0 (Lazy.force dump_rexpr) ff' in - let intro (id,_) = Tactics.introduction id in + let intro (id,_) = Tactics.introduction id in let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in - let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in - - let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; + let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in + + let tac_arith = Tacticals.New.tclTHENLIST [ clear_all_no_check ; intro_props ; intro_vars ; micromega_order_changer res' env' ff_arith ] in let goal_props = List.rev (Env.elements (prop_env_of_formula gl0 ff')) in - let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in - + let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in + let arith_args = goal_props @ goal_vars in - let kill_arith = - Tacticals.New.tclTHEN + let kill_arith = Tacticals.New.tclTHEN tac_arith tac in + (* Tacticals.New.tclTHEN (Tactics.keep []) - ((*Tactics.tclABSTRACT None*) - (Tacticals.New.tclTHEN tac_arith tac)) in + (Tactics.tclABSTRACT None*) Tacticals.New.tclTHENS (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal) [ kill_arith; (Tacticals.New.tclTHENLIST - [(Tactics.generalize (List.map EConstr.mkVar ids)); - Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args)) + [(Tactics.generalize (List.map EConstr.mkVar ids)); + (Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args))) ] ) ] with - | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout") | CsdpNotFound -> flush stdout ; - Tacticals.New.tclFAIL 0 (Pp.str + Tacticals.New.tclFAIL 0 (Pp.str (" Skipping what remains of this tactic: the complexity of the goal requires " - ^ "the use of a specialized external tool called csdp. \n\n" + ^ "the use of a specialized external tool called csdp. \n\n" ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) end - - -let micromega_genr prover = (micromega_genr prover) - - let lift_ratproof prover l = match prover l with | Unknown | Model _ -> Unknown @@ -1966,7 +1993,7 @@ let csdp_cache = ".csdp.cache" *) let require_csdp = - if System.is_in_system_path "csdp" + if System.is_in_system_path "csdp" then lazy () else lazy (raise CsdpNotFound) @@ -2028,9 +2055,9 @@ let xhyps_of_cone base acc prf = match e with | Mc.PsatzC _ | Mc.PsatzZ | Mc.PsatzSquare _ -> acc | Mc.PsatzIn n -> let n = (CoqToCaml.nat n) in - if n >= base - then ISet.add (n-base) acc - else acc + if n >= base + then ISet.add (n-base) acc + else acc | Mc.PsatzMulC(_,c) -> xtract c acc | Mc.PsatzAdd(e1,e2) | Mc.PsatzMulE(e1,e2) -> xtract e1 (xtract e2 acc) in @@ -2059,8 +2086,8 @@ let hyps_of_pt pt = | Mc.RatProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c) | Mc.CutProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c) | Mc.EnumProof(c1,c2,l) -> - let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in - List.fold_left (fun s x -> xhyps (base + 1) x s) s l in + let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in + List.fold_left (fun s x -> xhyps (base + 1) x s) s l in xhyps 0 pt ISet.empty @@ -2075,10 +2102,10 @@ let compact_pt pt f = | Mc.RatProof(c,pt) -> Mc.RatProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt ) | Mc.CutProof(c,pt) -> Mc.CutProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt ) | Mc.EnumProof(c1,c2,l) -> Mc.EnumProof(compact_cone c1 (translate (ofset)), compact_cone c2 (translate (ofset)), - Mc.map (fun x -> compact_pt (ofset+1) x) l) in + Mc.map (fun x -> compact_pt (ofset+1) x) l) in compact_pt 0 pt -(** +(** * Definition of provers. * Instantiates the type ('a,'prf) prover defined above. *) @@ -2099,15 +2126,15 @@ module CacheQ = PHashtable(struct let hash = Hashtbl.hash end) -let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s) +let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s) let memo_nlia = CacheZ.memo ".nia.cache" (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s) let memo_nra = CacheQ.memo ".nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s) - + let linear_prover_Q = { name = "linear prover"; - get_option = get_lra_option ; + get_option = get_lra_option ; prover = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o ) l) ; hyps = hyps_of_cone ; compact = compact_cone ; @@ -2118,7 +2145,7 @@ let linear_prover_Q = { let linear_prover_R = { name = "linear prover"; - get_option = get_lra_option ; + get_option = get_lra_option ; prover = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o ) l) ; hyps = hyps_of_cone ; compact = compact_cone ; @@ -2186,11 +2213,26 @@ let nlinear_Z = { pp_f = fun o x -> pp_pol pp_z o (fst x) } -(** +(** * Functions instantiating micromega_gen with the appropriate theories and * solvers *) +let exfalso_if_concl_not_Prop = + Proofview.Goal.enter begin fun gl -> + Tacmach.New.( + if is_prop (pf_env gl) (project gl) (pf_concl gl) + then Tacticals.New.tclIDTAC + else Tactics.elim_type (Lazy.force coq_False) + ) + end + +let micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac = + Tacticals.New.tclTHEN exfalso_if_concl_not_Prop (micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac) + +let micromega_genr prover tac = + Tacticals.New.tclTHEN exfalso_if_concl_not_Prop (micromega_genr prover tac) + let lra_Q = micromega_gen parse_qarith (fun _ x -> x) Mc.cnfQ qq_domain_spec dump_qexpr linear_prover_Q @@ -2232,26 +2274,13 @@ let xnlia = micromega_gen parse_zarith (fun _ x -> x) Mc.cnfZ zz_domain_spec dump_zexpr nlinear_Z -let nra = +let nra = micromega_genr nlinear_prover_R let nqa = micromega_gen parse_qarith (fun _ x -> x) Mc.cnfQ qq_domain_spec dump_qexpr nlinear_prover_R -(** Let expose [is_ground_tac] *) - -let is_ground_tac t = - Proofview.Goal.enter begin fun gl -> - let sigma = Tacmach.New.project gl in - let env = Tacmach.New.pf_env gl in - if is_ground_term env sigma t - then Tacticals.New.tclIDTAC - else Tacticals.New.tclFAIL 0 (Pp.str "Not ground") - end - - - (* Local Variables: *) (* coding: utf-8 *) (* End: *) diff --git a/plugins/micromega/coq_micromega.mli b/plugins/micromega/coq_micromega.mli index 7567e7c322..844ff5b1a6 100644 --- a/plugins/micromega/coq_micromega.mli +++ b/plugins/micromega/coq_micromega.mli @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val is_ground_tac : EConstr.constr -> unit Proofview.tactic +(*val is_ground_tac : EConstr.constr -> unit Proofview.tactic*) val psatz_Z : int -> unit Proofview.tactic -> unit Proofview.tactic val psatz_Q : int -> unit Proofview.tactic -> unit Proofview.tactic val psatz_R : int -> unit Proofview.tactic -> unit Proofview.tactic diff --git a/plugins/micromega/g_micromega.mlg b/plugins/micromega/g_micromega.mlg index ffc803af44..bcf546f059 100644 --- a/plugins/micromega/g_micromega.mlg +++ b/plugins/micromega/g_micromega.mlg @@ -22,6 +22,8 @@ open Ltac_plugin open Stdarg open Tacarg + + } DECLARE PLUGIN "micromega_plugin" @@ -30,11 +32,6 @@ TACTIC EXTEND RED | [ "myred" ] -> { Tactics.red_in_concl } END -TACTIC EXTEND ISGROUND -| [ "is_ground" constr(t) ] -> { Coq_micromega.is_ground_tac t } -END - - TACTIC EXTEND PsatzZ | [ "psatz_Z" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Z i (Tacinterp.tactic_of_value ist t)) diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg new file mode 100644 index 0000000000..424a7d7c54 --- /dev/null +++ b/plugins/micromega/g_zify.mlg @@ -0,0 +1,52 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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) *) +(************************************************************************) + +{ + +open Ltac_plugin +open Stdarg +open Tacarg + + +} + +DECLARE PLUGIN "zify_plugin" + +VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF +| ["Add" "InjTyp" constr(t) ] -> { Zify.InjTable.register t } +| ["Add" "BinOp" constr(t) ] -> { Zify.BinOp.register t } +| ["Add" "UnOp" constr(t) ] -> { Zify.UnOp.register t } +| ["Add" "CstOp" constr(t) ] -> { Zify.CstOp.register t } +| ["Add" "BinRel" constr(t) ] -> { Zify.BinRel.register t } +| ["Add" "PropOp" constr(t) ] -> { Zify.PropOp.register t } +| ["Add" "PropUOp" constr(t) ] -> { Zify.PropOp.register t } +| ["Add" "Spec" constr(t) ] -> { Zify.Spec.register t } +| ["Add" "BinOpSpec" constr(t) ] -> { Zify.Spec.register t } +| ["Add" "UnOpSpec" constr(t) ] -> { Zify.Spec.register t } +| ["Add" "Saturate" constr(t) ] -> { Zify.Saturate.register t } +END + +TACTIC EXTEND ITER +| [ "iter_specs" tactic(t)] -> { Zify.iter_specs t } +END + +TACTIC EXTEND TRANS +| [ "zify_tac" ] -> { Zify.zify_tac } +| [ "saturate" ] -> { Zify.saturate } +END + +VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF +|[ "Show" "Zify" "InjTyp" ] -> { Zify.InjTable.print () } +|[ "Show" "Zify" "BinOp" ] -> { Zify.BinOp.print () } +|[ "Show" "Zify" "UnOp" ] -> { Zify.UnOp.print () } +|[ "Show" "Zify" "CstOp"] -> { Zify.CstOp.print () } +|[ "Show" "Zify" "BinRel"] -> { Zify.BinRel.print () } +|[ "Show" "Zify" "Spec"] -> { Zify.Spec.print () } +END diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index cd620bd4a9..f508b3dc56 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -67,12 +67,26 @@ let rec nth n0 l default = | [] -> default | _::t0 -> nth m t0 default) +(** val rev_append : 'a1 list -> 'a1 list -> 'a1 list **) + +let rec rev_append l l' = + match l with + | [] -> l' + | a::l0 -> rev_append l0 (a::l') + (** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **) let rec map f = function | [] -> [] | a::t0 -> (f a)::(map f t0) +(** val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1 **) + +let rec fold_left f l a0 = + match l with + | [] -> a0 + | b::t0 -> fold_left f t0 (f a0 b) + (** val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 **) let rec fold_right f a0 = function @@ -1061,15 +1075,24 @@ let rec or_clause unsat deduce cl1 cl2 = | Some cl' -> or_clause unsat deduce cl cl' | None -> None) -(** val or_clause_cnf : +(** val xor_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf **) -let or_clause_cnf unsat deduce t0 f = - fold_right (fun e acc -> +let xor_clause_cnf unsat deduce t0 f = + fold_left (fun acc e -> match or_clause unsat deduce t0 e with | Some cl -> cl::acc - | None -> acc) [] f + | None -> acc) f [] + +(** val or_clause_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, + 'a2) cnf -> ('a1, 'a2) cnf **) + +let or_clause_cnf unsat deduce t0 f = + match t0 with + | [] -> f + | _::_ -> xor_clause_cnf unsat deduce t0 f (** val or_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, @@ -1079,45 +1102,78 @@ let rec or_cnf unsat deduce f f' = match f with | [] -> cnf_tt | e::rst -> - app (or_cnf unsat deduce rst f') (or_clause_cnf unsat deduce e f') + rev_append (or_cnf unsat deduce rst f') (or_clause_cnf unsat deduce e f') (** val and_cnf : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf **) let and_cnf = - app + rev_append type ('term, 'annot, 'tX, 'aF) tFormula = ('term, 'tX, 'annot, 'aF) gFormula +(** val is_cnf_tt : ('a1, 'a2) cnf -> bool **) + +let is_cnf_tt = function +| [] -> true +| _::_ -> false + +(** val is_cnf_ff : ('a1, 'a2) cnf -> bool **) + +let is_cnf_ff = function +| [] -> false +| c0::l -> + (match c0 with + | [] -> (match l with + | [] -> true + | _::_ -> false) + | _::_ -> false) + +(** val and_cnf_opt : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf **) + +let and_cnf_opt f1 f2 = + if if is_cnf_ff f1 then true else is_cnf_ff f2 + then cnf_ff + else and_cnf f1 f2 + +(** val or_cnf_opt : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, + 'a2) cnf -> ('a1, 'a2) cnf **) + +let or_cnf_opt unsat deduce f1 f2 = + if if is_cnf_tt f1 then true else is_cnf_tt f2 + then cnf_tt + else if is_cnf_ff f2 then f1 else or_cnf unsat deduce f1 f2 + (** val xcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) -let rec xcnf unsat deduce normalise0 negate0 pol0 = function +let rec xcnf unsat deduce normalise1 negate0 pol0 = function | TT -> if pol0 then cnf_tt else cnf_ff | FF -> if pol0 then cnf_ff else cnf_tt | X _ -> cnf_ff -| A (x, t0) -> if pol0 then normalise0 x t0 else negate0 x t0 +| A (x, t0) -> if pol0 then normalise1 x t0 else negate0 x t0 | Cj (e1, e2) -> if pol0 - then and_cnf (xcnf unsat deduce normalise0 negate0 pol0 e1) - (xcnf unsat deduce normalise0 negate0 pol0 e2) - else or_cnf unsat deduce (xcnf unsat deduce normalise0 negate0 pol0 e1) - (xcnf unsat deduce normalise0 negate0 pol0 e2) + then and_cnf_opt (xcnf unsat deduce normalise1 negate0 pol0 e1) + (xcnf unsat deduce normalise1 negate0 pol0 e2) + else or_cnf_opt unsat deduce (xcnf unsat deduce normalise1 negate0 pol0 e1) + (xcnf unsat deduce normalise1 negate0 pol0 e2) | D (e1, e2) -> if pol0 - then or_cnf unsat deduce (xcnf unsat deduce normalise0 negate0 pol0 e1) - (xcnf unsat deduce normalise0 negate0 pol0 e2) - else and_cnf (xcnf unsat deduce normalise0 negate0 pol0 e1) - (xcnf unsat deduce normalise0 negate0 pol0 e2) -| N e -> xcnf unsat deduce normalise0 negate0 (negb pol0) e + then or_cnf_opt unsat deduce (xcnf unsat deduce normalise1 negate0 pol0 e1) + (xcnf unsat deduce normalise1 negate0 pol0 e2) + else and_cnf_opt (xcnf unsat deduce normalise1 negate0 pol0 e1) + (xcnf unsat deduce normalise1 negate0 pol0 e2) +| N e -> xcnf unsat deduce normalise1 negate0 (negb pol0) e | I (e1, _, e2) -> if pol0 - then or_cnf unsat deduce - (xcnf unsat deduce normalise0 negate0 (negb pol0) e1) - (xcnf unsat deduce normalise0 negate0 pol0 e2) - else and_cnf (xcnf unsat deduce normalise0 negate0 (negb pol0) e1) - (xcnf unsat deduce normalise0 negate0 pol0 e2) + then or_cnf_opt unsat deduce + (xcnf unsat deduce normalise1 negate0 (negb pol0) e1) + (xcnf unsat deduce normalise1 negate0 pol0 e2) + else and_cnf_opt (xcnf unsat deduce normalise1 negate0 (negb pol0) e1) + (xcnf unsat deduce normalise1 negate0 pol0 e2) (** val radd_term : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) @@ -1153,19 +1209,28 @@ let rec ror_clause unsat deduce cl1 cl2 = | Inl cl' -> ror_clause unsat deduce cl cl' | Inr l -> Inr l) -(** val ror_clause_cnf : +(** val xror_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list * 'a2 list **) -let ror_clause_cnf unsat deduce t0 f = - fold_right (fun e pat -> +let xror_clause_cnf unsat deduce t0 f = + fold_left (fun pat e -> let acc,tg = pat in (match ror_clause unsat deduce t0 e with | Inl cl -> (cl::acc),tg - | Inr l -> acc,(app tg l))) ([],[]) f + | Inr l -> acc,(rev_append tg l))) f ([],[]) + +(** val ror_clause_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, + 'a2) clause list -> ('a1, 'a2) clause list * 'a2 list **) + +let ror_clause_cnf unsat deduce t0 f = + match t0 with + | [] -> f,[] + | _::_ -> xror_clause_cnf unsat deduce t0 f (** val ror_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list list -> + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list -> ('a1, 'a2) cnf * 'a2 list **) let rec ror_cnf unsat deduce f f' = @@ -1174,37 +1239,159 @@ let rec ror_cnf unsat deduce f f' = | e::rst -> let rst_f',t0 = ror_cnf unsat deduce rst f' in let e_f',t' = ror_clause_cnf unsat deduce e f' in - (app rst_f' e_f'),(app t0 t') + (rev_append rst_f' e_f'),(rev_append t0 t') + +(** val ror_cnf_opt : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, + 'a2) cnf -> ('a1, 'a2) cnf * 'a2 list **) + +let ror_cnf_opt unsat deduce f1 f2 = + if is_cnf_tt f1 + then cnf_tt,[] + else if is_cnf_tt f2 + then cnf_tt,[] + else if is_cnf_ff f2 then f1,[] else ror_cnf unsat deduce f1 f2 + +(** val ratom : ('a1, 'a2) cnf -> 'a2 -> ('a1, 'a2) cnf * 'a2 list **) + +let ratom c a = + if if is_cnf_ff c then true else is_cnf_tt c then c,(a::[]) else c,[] (** val rxcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list **) -let rec rxcnf unsat deduce normalise0 negate0 polarity = function +let rec rxcnf unsat deduce normalise1 negate0 polarity = function | TT -> if polarity then cnf_tt,[] else cnf_ff,[] | FF -> if polarity then cnf_ff,[] else cnf_tt,[] | X _ -> cnf_ff,[] -| A (x, t0) -> (if polarity then normalise0 x t0 else negate0 x t0),[] +| A (x, t0) -> ratom (if polarity then normalise1 x t0 else negate0 x t0) t0 | Cj (e1, e2) -> - let e3,t1 = rxcnf unsat deduce normalise0 negate0 polarity e1 in - let e4,t2 = rxcnf unsat deduce normalise0 negate0 polarity e2 in + let e3,t1 = rxcnf unsat deduce normalise1 negate0 polarity e1 in + let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in if polarity - then (app e3 e4),(app t1 t2) - else let f',t' = ror_cnf unsat deduce e3 e4 in f',(app t1 (app t2 t')) + then (and_cnf_opt e3 e4),(rev_append t1 t2) + else let f',t' = ror_cnf_opt unsat deduce e3 e4 in + f',(rev_append t1 (rev_append t2 t')) | D (e1, e2) -> - let e3,t1 = rxcnf unsat deduce normalise0 negate0 polarity e1 in - let e4,t2 = rxcnf unsat deduce normalise0 negate0 polarity e2 in + let e3,t1 = rxcnf unsat deduce normalise1 negate0 polarity e1 in + let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in if polarity - then let f',t' = ror_cnf unsat deduce e3 e4 in f',(app t1 (app t2 t')) - else (app e3 e4),(app t1 t2) -| N e -> rxcnf unsat deduce normalise0 negate0 (negb polarity) e + then let f',t' = ror_cnf_opt unsat deduce e3 e4 in + f',(rev_append t1 (rev_append t2 t')) + else (and_cnf_opt e3 e4),(rev_append t1 t2) +| N e -> rxcnf unsat deduce normalise1 negate0 (negb polarity) e | I (e1, _, e2) -> - let e3,t1 = rxcnf unsat deduce normalise0 negate0 (negb polarity) e1 in - let e4,t2 = rxcnf unsat deduce normalise0 negate0 polarity e2 in + let e3,t1 = rxcnf unsat deduce normalise1 negate0 (negb polarity) e1 in if polarity - then let f',t' = ror_cnf unsat deduce e3 e4 in f',(app t1 (app t2 t')) - else (and_cnf e3 e4),(app t1 t2) + then if is_cnf_ff e3 + then rxcnf unsat deduce normalise1 negate0 polarity e2 + else let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in + let f',t' = ror_cnf_opt unsat deduce e3 e4 in + f',(rev_append t1 (rev_append t2 t')) + else let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in + (and_cnf_opt e3 e4),(rev_append t1 t2) + +type ('term, 'annot, 'tX) to_constrT = { mkTT : 'tX; mkFF : 'tX; + mkA : ('term -> 'annot -> 'tX); + mkCj : ('tX -> 'tX -> 'tX); + mkD : ('tX -> 'tX -> 'tX); + mkI : ('tX -> 'tX -> 'tX); + mkN : ('tX -> 'tX) } + +(** val aformula : + ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 **) + +let rec aformula to_constr = function +| TT -> to_constr.mkTT +| FF -> to_constr.mkFF +| X p -> p +| A (x, t0) -> to_constr.mkA x t0 +| Cj (f1, f2) -> + to_constr.mkCj (aformula to_constr f1) (aformula to_constr f2) +| D (f1, f2) -> to_constr.mkD (aformula to_constr f1) (aformula to_constr f2) +| N f0 -> to_constr.mkN (aformula to_constr f0) +| I (f1, _, f2) -> + to_constr.mkI (aformula to_constr f1) (aformula to_constr f2) + +(** val is_X : ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option **) + +let is_X = function +| X p -> Some p +| _ -> None + +(** val abs_and : + ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, + 'a3, 'a4) tFormula -> (('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, + 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) + gFormula **) + +let abs_and to_constr f1 f2 c = + match is_X f1 with + | Some _ -> X (aformula to_constr (c f1 f2)) + | None -> + (match is_X f2 with + | Some _ -> X (aformula to_constr (c f1 f2)) + | None -> c f1 f2) + +(** val abs_or : + ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, + 'a3, 'a4) tFormula -> (('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, + 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) + gFormula **) + +let abs_or to_constr f1 f2 c = + match is_X f1 with + | Some _ -> + (match is_X f2 with + | Some _ -> X (aformula to_constr (c f1 f2)) + | None -> c f1 f2) + | None -> c f1 f2 + +(** val mk_arrow : + 'a4 option -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) + tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **) + +let mk_arrow o f1 f2 = + match o with + | Some _ -> (match is_X f1 with + | Some _ -> f2 + | None -> I (f1, o, f2)) + | None -> I (f1, None, f2) + +(** val abst_form : + ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> ('a1, 'a2, 'a3, + 'a4) tFormula -> ('a1, 'a3, 'a2, 'a4) gFormula **) + +let rec abst_form to_constr needA pol0 = function +| TT -> if pol0 then TT else X to_constr.mkTT +| FF -> if pol0 then X to_constr.mkFF else FF +| X p -> X p +| A (x, t0) -> if needA t0 then A (x, t0) else X (to_constr.mkA x t0) +| Cj (f1, f2) -> + let f3 = abst_form to_constr needA pol0 f1 in + let f4 = abst_form to_constr needA pol0 f2 in + if pol0 + then abs_and to_constr f3 f4 (fun x x0 -> Cj (x, x0)) + else abs_or to_constr f3 f4 (fun x x0 -> Cj (x, x0)) +| D (f1, f2) -> + let f3 = abst_form to_constr needA pol0 f1 in + let f4 = abst_form to_constr needA pol0 f2 in + if pol0 + then abs_or to_constr f3 f4 (fun x x0 -> D (x, x0)) + else abs_and to_constr f3 f4 (fun x x0 -> D (x, x0)) +| N f0 -> + let f1 = abst_form to_constr needA (negb pol0) f0 in + (match is_X f1 with + | Some a -> X (to_constr.mkN a) + | None -> N f1) +| I (f1, o, f2) -> + let f3 = abst_form to_constr needA (negb pol0) f1 in + let f4 = abst_form to_constr needA pol0 f2 in + if pol0 + then abs_or to_constr f3 f4 (mk_arrow o) + else abs_and to_constr f3 f4 (mk_arrow o) (** val cnf_checker : (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool **) @@ -1222,8 +1409,8 @@ let rec cnf_checker checker f l = cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> bool) -> ('a1, __, 'a3, unit0) gFormula -> 'a4 list -> bool **) -let tauto_checker unsat deduce normalise0 negate0 checker f w = - cnf_checker checker (xcnf unsat deduce normalise0 negate0 true f) w +let tauto_checker unsat deduce normalise1 negate0 checker f w = + cnf_checker checker (xcnf unsat deduce normalise1 negate0 true f) w (** val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool **) @@ -1413,62 +1600,76 @@ let psub0 = let padd0 = padd -(** val xnormalise : +(** val popp0 : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol **) + +let popp0 = + popp + +(** val normalise : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 - nFormula list **) + nFormula **) -let xnormalise cO cI cplus ctimes cminus copp ceqb t0 = - let { flhs = lhs; fop = o; frhs = rhs } = t0 in +let normalise cO cI cplus ctimes cminus copp ceqb f = + let { flhs = lhs; fop = op; frhs = rhs } = f in let lhs0 = norm cO cI cplus ctimes cminus copp ceqb lhs in let rhs0 = norm cO cI cplus ctimes cminus copp ceqb rhs in + (match op with + | OpEq -> (psub0 cO cplus cminus copp ceqb lhs0 rhs0),Equal + | OpNEq -> (psub0 cO cplus cminus copp ceqb lhs0 rhs0),NonEqual + | OpLe -> (psub0 cO cplus cminus copp ceqb rhs0 lhs0),NonStrict + | OpGe -> (psub0 cO cplus cminus copp ceqb lhs0 rhs0),NonStrict + | OpLt -> (psub0 cO cplus cminus copp ceqb rhs0 lhs0),Strict + | OpGt -> (psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict) + +(** val xnormalise : ('a1 -> 'a1) -> 'a1 nFormula -> 'a1 nFormula list **) + +let xnormalise copp = function +| e,o -> (match o with - | OpEq -> - ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::(((psub0 cO cplus - cminus copp - ceqb rhs0 lhs0),Strict)::[]) - | OpNEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Equal)::[] - | OpLe -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::[] - | OpGe -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),Strict)::[] - | OpLt -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),NonStrict)::[] - | OpGt -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),NonStrict)::[]) + | Equal -> (e,Strict)::(((popp0 copp e),Strict)::[]) + | NonEqual -> (e,Equal)::[] + | Strict -> ((popp0 copp e),NonStrict)::[] + | NonStrict -> ((popp0 copp e),Strict)::[]) -(** val cnf_normalise : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> - ('a1 nFormula, 'a2) cnf **) +(** val xnegate : ('a1 -> 'a1) -> 'a1 nFormula -> 'a1 nFormula list **) -let cnf_normalise cO cI cplus ctimes cminus copp ceqb t0 tg = - map (fun x -> (x,tg)::[]) - (xnormalise cO cI cplus ctimes cminus copp ceqb t0) +let xnegate copp = function +| e,o -> + (match o with + | NonEqual -> (e,Strict)::(((popp0 copp e),Strict)::[]) + | x -> (e,x)::[]) + +(** val cnf_of_list : + 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list + -> 'a2 -> ('a1 nFormula, 'a2) cnf **) + +let cnf_of_list cO ceqb cleb l tg = + fold_right (fun x acc -> + if check_inconsistent cO ceqb cleb x then acc else ((x,tg)::[])::acc) + cnf_tt l -(** val xnegate : +(** val cnf_normalise : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 - nFormula list **) + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) + -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf **) -let xnegate cO cI cplus ctimes cminus copp ceqb t0 = - let { flhs = lhs; fop = o; frhs = rhs } = t0 in - let lhs0 = norm cO cI cplus ctimes cminus copp ceqb lhs in - let rhs0 = norm cO cI cplus ctimes cminus copp ceqb rhs in - (match o with - | OpEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Equal)::[] - | OpNEq -> - ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::(((psub0 cO cplus - cminus copp - ceqb rhs0 lhs0),Strict)::[]) - | OpLe -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),NonStrict)::[] - | OpGe -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),NonStrict)::[] - | OpLt -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),Strict)::[] - | OpGt -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::[]) +let cnf_normalise cO cI cplus ctimes cminus copp ceqb cleb t0 tg = + let f = normalise cO cI cplus ctimes cminus copp ceqb t0 in + if check_inconsistent cO ceqb cleb f + then cnf_ff + else cnf_of_list cO ceqb cleb (xnormalise copp f) tg (** val cnf_negate : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> - ('a1 nFormula, 'a2) cnf **) + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) + -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf **) -let cnf_negate cO cI cplus ctimes cminus copp ceqb t0 tg = - map (fun x -> (x,tg)::[]) (xnegate cO cI cplus ctimes cminus copp ceqb t0) +let cnf_negate cO cI cplus ctimes cminus copp ceqb cleb t0 tg = + let f = normalise cO cI cplus ctimes cminus copp ceqb t0 in + if check_inconsistent cO ceqb cleb f + then cnf_tt + else cnf_of_list cO ceqb cleb (xnegate copp f) tg (** val xdenorm : positive -> 'a1 pol -> 'a1 pExpr **) @@ -1696,67 +1897,75 @@ let padd1 = let normZ = norm Z0 (Zpos XH) Z.add Z.mul Z.sub Z.opp zeq_bool -(** val xnormalise0 : z formula -> z nFormula list **) +(** val zunsat : z nFormula -> bool **) -let xnormalise0 t0 = - let { flhs = lhs; fop = o; frhs = rhs } = t0 in - let lhs0 = normZ lhs in - let rhs0 = normZ rhs in - (match o with - | OpEq -> - ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::(((psub1 rhs0 - (padd1 lhs0 - (Pc (Zpos - XH)))),NonStrict)::[]) - | OpNEq -> ((psub1 lhs0 rhs0),Equal)::[] - | OpLe -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::[] - | OpGe -> ((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))),NonStrict)::[] - | OpLt -> ((psub1 lhs0 rhs0),NonStrict)::[] - | OpGt -> ((psub1 rhs0 lhs0),NonStrict)::[]) +let zunsat = + check_inconsistent Z0 zeq_bool Z.leb -(** val normalise : z formula -> 'a1 -> (z nFormula, 'a1) cnf **) +(** val zdeduce : z nFormula -> z nFormula -> z nFormula option **) -let normalise t0 tg = - map (fun x -> (x,tg)::[]) (xnormalise0 t0) +let zdeduce = + nformula_plus_nformula Z0 Z.add zeq_bool -(** val xnegate0 : z formula -> z nFormula list **) +(** val xnnormalise : z formula -> z nFormula **) -let xnegate0 t0 = +let xnnormalise t0 = let { flhs = lhs; fop = o; frhs = rhs } = t0 in let lhs0 = normZ lhs in let rhs0 = normZ rhs in (match o with - | OpEq -> ((psub1 lhs0 rhs0),Equal)::[] - | OpNEq -> - ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::(((psub1 rhs0 - (padd1 lhs0 - (Pc (Zpos - XH)))),NonStrict)::[]) - | OpLe -> ((psub1 rhs0 lhs0),NonStrict)::[] - | OpGe -> ((psub1 lhs0 rhs0),NonStrict)::[] - | OpLt -> ((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))),NonStrict)::[] - | OpGt -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::[]) + | OpEq -> (psub1 rhs0 lhs0),Equal + | OpNEq -> (psub1 rhs0 lhs0),NonEqual + | OpLe -> (psub1 rhs0 lhs0),NonStrict + | OpGe -> (psub1 lhs0 rhs0),NonStrict + | OpLt -> (psub1 rhs0 lhs0),Strict + | OpGt -> (psub1 lhs0 rhs0),Strict) -(** val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf **) +(** val xnormalise0 : z nFormula -> z nFormula list **) -let negate t0 tg = - map (fun x -> (x,tg)::[]) (xnegate0 t0) +let xnormalise0 = function +| e,o -> + (match o with + | Equal -> + ((psub1 e (Pc (Zpos XH))),NonStrict)::(((psub1 (Pc (Zneg XH)) e),NonStrict)::[]) + | NonEqual -> (e,Equal)::[] + | Strict -> ((psub1 (Pc Z0) e),NonStrict)::[] + | NonStrict -> ((psub1 (Pc (Zneg XH)) e),NonStrict)::[]) -(** val zunsat : z nFormula -> bool **) +(** val cnf_of_list0 : + 'a1 -> z nFormula list -> (z nFormula * 'a1) list list **) -let zunsat = - check_inconsistent Z0 zeq_bool Z.leb +let cnf_of_list0 tg l = + fold_right (fun x acc -> if zunsat x then acc else ((x,tg)::[])::acc) + cnf_tt l -(** val zdeduce : z nFormula -> z nFormula -> z nFormula option **) +(** val normalise0 : z formula -> 'a1 -> (z nFormula, 'a1) cnf **) -let zdeduce = - nformula_plus_nformula Z0 Z.add zeq_bool +let normalise0 t0 tg = + let f = xnnormalise t0 in + if zunsat f then cnf_ff else cnf_of_list0 tg (xnormalise0 f) + +(** val xnegate0 : z nFormula -> z nFormula list **) + +let xnegate0 = function +| e,o -> + (match o with + | NonEqual -> + ((psub1 e (Pc (Zpos XH))),NonStrict)::(((psub1 (Pc (Zneg XH)) e),NonStrict)::[]) + | Strict -> ((psub1 e (Pc (Zpos XH))),NonStrict)::[] + | x -> (e,x)::[]) + +(** val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf **) + +let negate t0 tg = + let f = xnnormalise t0 in + if zunsat f then cnf_tt else cnf_of_list0 tg (xnegate0 f) (** val cnfZ : (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 list **) let cnfZ f = - rxcnf zunsat zdeduce normalise negate true f + rxcnf zunsat zdeduce normalise0 negate true f (** val ceiling : z -> z -> z **) @@ -2027,7 +2236,7 @@ let rec zChecker l = function (** val zTautoChecker : z formula bFormula -> zArithProof list -> bool **) let zTautoChecker f w = - tauto_checker zunsat zdeduce normalise negate (fun cl -> + tauto_checker zunsat zdeduce normalise0 negate (fun cl -> zChecker (map fst cl)) f w type qWitness = q psatz @@ -2042,13 +2251,13 @@ let qWeakChecker = let qnormalise t0 tg = cnf_normalise { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } - qplus qmult qminus qopp qeq_bool t0 tg + qplus qmult qminus qopp qeq_bool qle_bool t0 tg (** val qnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf **) let qnegate t0 tg = cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus - qmult qminus qopp qeq_bool t0 tg + qmult qminus qopp qeq_bool qle_bool t0 tg (** val qunsat : q nFormula -> bool **) @@ -2122,13 +2331,13 @@ let rWeakChecker = let rnormalise t0 tg = cnf_normalise { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } - qplus qmult qminus qopp qeq_bool t0 tg + qplus qmult qminus qopp qeq_bool qle_bool t0 tg (** val rnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf **) let rnegate t0 tg = cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus - qmult qminus qopp qeq_bool t0 tg + qmult qminus qopp qeq_bool qle_bool t0 tg (** val runsat : q nFormula -> bool **) diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli index 6da0c754f4..822fde9ab0 100644 --- a/plugins/micromega/micromega.mli +++ b/plugins/micromega/micromega.mli @@ -31,8 +31,12 @@ val add : nat -> nat -> nat val nth : nat -> 'a1 list -> 'a1 -> 'a1 +val rev_append : 'a1 list -> 'a1 list -> 'a1 list + val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list +val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1 + val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 type positive = @@ -187,45 +191,43 @@ val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol val paddI : - ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol - -> 'a1 pol + ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> + 'a1 pol val psubI : - ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> - positive -> 'a1 pol -> 'a1 pol + ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive + -> 'a1 pol -> 'a1 pol val paddX : - 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> - 'a1 pol -> 'a1 pol + 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 + pol -> 'a1 pol val psubX : - 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 - pol -> positive -> 'a1 pol -> 'a1 pol + 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> + positive -> 'a1 pol -> 'a1 pol -val padd : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol +val padd : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol val psub : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> - bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> + 'a1 pol -> 'a1 pol -> 'a1 pol -val pmulC_aux : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol +val pmulC_aux : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol val pmulC : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol val pmulI : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 - pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) + -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol val pmul : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 - pol -> 'a1 pol -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol + -> 'a1 pol -> 'a1 pol val psquare : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 - pol -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol + -> 'a1 pol type 'c pExpr = | PEc of 'c @@ -239,16 +241,16 @@ type 'c pExpr = val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol val ppow_pos : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 - pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol + -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol val ppow_N : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 - pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol + -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol val norm_aux : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 - -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol type ('tA, 'tX, 'aA, 'aF) gFormula = | TT @@ -284,56 +286,106 @@ val cnf_tt : ('a1, 'a2) cnf val cnf_ff : ('a1, 'a2) cnf val add_term : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> ('a1, - 'a2) clause option + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> ('a1, 'a2) + clause option val or_clause : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) clause -> ('a1, 'a2) clause option +val xor_clause_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf -> ('a1, + 'a2) cnf + val or_clause_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf -> - ('a1, 'a2) cnf + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf -> ('a1, + 'a2) cnf val or_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, - 'a2) cnf + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) + cnf val and_cnf : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf type ('term, 'annot, 'tX, 'aF) tFormula = ('term, 'tX, 'annot, 'aF) gFormula +val is_cnf_tt : ('a1, 'a2) cnf -> bool + +val is_cnf_ff : ('a1, 'a2) cnf -> bool + +val and_cnf_opt : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf + +val or_cnf_opt : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) + cnf + val xcnf : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> - 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 + -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf val radd_term : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> - (('a1, 'a2) clause, 'a2 list) sum + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> (('a1, + 'a2) clause, 'a2 list) sum val ror_clause : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause -> (('a1, 'a2) clause, 'a2 list) sum +val xror_clause_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause list -> + ('a1, 'a2) clause list * 'a2 list + val ror_clause_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause - list -> ('a1, 'a2) clause list * 'a2 list + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause list -> + ('a1, 'a2) clause list * 'a2 list val ror_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list list -> ('a1, 'a2) - clause list -> ('a1, 'a2) cnf * 'a2 list + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause list -> ('a1, 'a2) clause + list -> ('a1, 'a2) cnf * 'a2 list + +val ror_cnf_opt : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) + cnf * 'a2 list + +val ratom : ('a1, 'a2) cnf -> 'a2 -> ('a1, 'a2) cnf * 'a2 list val rxcnf : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> - 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 - list + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 + -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list + +type ('term, 'annot, 'tX) to_constrT = { mkTT : 'tX; mkFF : 'tX; + mkA : ('term -> 'annot -> 'tX); + mkCj : ('tX -> 'tX -> 'tX); mkD : ('tX -> 'tX -> 'tX); + mkI : ('tX -> 'tX -> 'tX); mkN : ('tX -> 'tX) } + +val aformula : ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 + +val is_X : ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option + +val abs_and : + ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula + -> (('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) + tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula + +val abs_or : + ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula + -> (('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) + tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula + +val mk_arrow : + 'a4 option -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, + 'a3, 'a4) tFormula + +val abst_form : + ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, + 'a3, 'a2, 'a4) gFormula val cnf_checker : (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool val tauto_checker : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> - 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> bool) -> ('a1, __, 'a3, unit0) - gFormula -> 'a4 list -> bool + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 + -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> bool) -> ('a1, __, 'a3, unit0) gFormula -> + 'a4 list -> bool val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool @@ -367,27 +419,27 @@ val map_option : ('a1 -> 'a2 option) -> 'a1 option -> 'a2 option val map_option2 : ('a1 -> 'a2 -> 'a3 option) -> 'a1 option -> 'a2 option -> 'a3 option val pexpr_times_nformula : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 - polC -> 'a1 nFormula -> 'a1 nFormula option + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 polC + -> 'a1 nFormula -> 'a1 nFormula option val nformula_times_nformula : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option val nformula_plus_nformula : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> - 'a1 nFormula option + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 + nFormula option val eval_Psatz : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 - -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1 nFormula option + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> + 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1 nFormula option val check_inconsistent : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> bool val check_normalised_formulas : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 - -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> + 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool type op2 = | OpEq @@ -400,31 +452,38 @@ type op2 = type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr } val norm : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 - -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol val psub0 : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> - bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> + 'a1 pol -> 'a1 pol -> 'a1 pol -val padd0 : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol +val padd0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol -val xnormalise : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 - -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list +val popp0 : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol -val cnf_normalise : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 - -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf +val normalise : + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula + +val xnormalise : ('a1 -> 'a1) -> 'a1 nFormula -> 'a1 nFormula list + +val xnegate : ('a1 -> 'a1) -> 'a1 nFormula -> 'a1 nFormula list + +val cnf_of_list : + 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a2 -> ('a1 + nFormula, 'a2) cnf -val xnegate : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 - -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list +val cnf_normalise : + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, + 'a2) cnf val cnf_negate : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 - -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> + 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, + 'a2) cnf val xdenorm : positive -> 'a1 pol -> 'a1 pExpr @@ -487,17 +546,21 @@ val padd1 : z pol -> z pol -> z pol val normZ : z pExpr -> z pol -val xnormalise0 : z formula -> z nFormula list +val zunsat : z nFormula -> bool -val normalise : z formula -> 'a1 -> (z nFormula, 'a1) cnf +val zdeduce : z nFormula -> z nFormula -> z nFormula option -val xnegate0 : z formula -> z nFormula list +val xnnormalise : z formula -> z nFormula -val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf +val xnormalise0 : z nFormula -> z nFormula list -val zunsat : z nFormula -> bool +val cnf_of_list0 : 'a1 -> z nFormula list -> (z nFormula * 'a1) list list -val zdeduce : z nFormula -> z nFormula -> z nFormula option +val normalise0 : z formula -> 'a1 -> (z nFormula, 'a1) cnf + +val xnegate0 : z nFormula -> z nFormula list + +val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf val cnfZ : (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 list @@ -565,8 +628,8 @@ val bound_var : positive -> z formula val mk_eq_pos : positive -> positive -> positive -> z formula val bound_vars : - (positive -> positive -> bool option -> 'a2) -> positive -> Vars.t -> (z formula, 'a1, - 'a2, 'a3) gFormula + (positive -> positive -> bool option -> 'a2) -> positive -> Vars.t -> (z formula, 'a1, 'a2, + 'a3) gFormula val bound_problem_fr : (positive -> positive -> bool option -> 'a2) -> positive -> (z formula, 'a1, 'a2, 'a3) diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 5829292a0c..14a1bc9712 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -16,25 +16,19 @@ module type PHashtable = sig + (* see documentation in [persistent_cache.mli] *) type 'a t type key val open_in : string -> 'a t - (** [open_in f] rebuilds a table from the records stored in file [f]. - As marshaling is not type-safe, it might segfault. - *) val find : 'a t -> key -> 'a - (** find has the specification of Hashtable.find *) val add : 'a t -> key -> 'a -> unit - (** [add tbl key elem] adds the binding [key] [elem] to the table [tbl]. - (and writes the binding to the file associated with [tbl].) - If [key] is already bound, raises KeyAlreadyBound *) val memo : string -> (key -> 'a) -> (key -> 'a) - (** [memo cache f] returns a memo function for [f] using file [cache] as persistent table. - Note that the cache will only be loaded when the function is used for the first time *) + + val memo_cond : string -> (key -> bool) -> (key -> 'a) -> (key -> 'a) end @@ -200,6 +194,24 @@ let memo cache f = add tbl x res ; res +let memo_cond cache cond f = + let tbl = lazy (try Some (open_in cache) with _ -> None) in + fun x -> + match Lazy.force tbl with + | None -> f x + | Some tbl -> + if cond x + then + begin + try find tbl x + with Not_found -> + let res = f x in + add tbl x res ; + res + end + else f x + + end diff --git a/plugins/micromega/persistent_cache.mli b/plugins/micromega/persistent_cache.mli index 4248407221..cb14d73972 100644 --- a/plugins/micromega/persistent_cache.mli +++ b/plugins/micromega/persistent_cache.mli @@ -32,6 +32,10 @@ module type PHashtable = (** [memo cache f] returns a memo function for [f] using file [cache] as persistent table. Note that the cache will only be loaded when the function is used for the first time *) + val memo_cond : string -> (key -> bool) -> (key -> 'a) -> (key -> 'a) + (** [memo cache cond f] only use the cache if [cond k] holds for the key [k]. *) + + end module PHashtable(Key:HashedType) : PHashtable with type key = Key.t diff --git a/plugins/micromega/plugin_base.dune b/plugins/micromega/plugin_base.dune index c2d396f0f9..4153d06161 100644 --- a/plugins/micromega/plugin_base.dune +++ b/plugins/micromega/plugin_base.dune @@ -2,7 +2,7 @@ (name micromega_plugin) (public_name coq.plugins.micromega) ; be careful not to link the executable to the plugin! - (modules (:standard \ csdpcert)) + (modules (:standard \ csdpcert g_zify zify)) (synopsis "Coq's micromega plugin") (libraries num coq.plugins.ltac)) @@ -13,3 +13,10 @@ (modules csdpcert) (flags :standard -open Micromega_plugin) (libraries coq.plugins.micromega)) + +(library + (name zify_plugin) + (public_name coq.plugins.zify) + (modules g_zify zify) + (synopsis "Coq's zify plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml new file mode 100644 index 0000000000..be6037ccdb --- /dev/null +++ b/plugins/micromega/zify.ml @@ -0,0 +1,1117 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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) *) +(************************************************************************) + +open Constr +open Names +open Pp +open Lazy + +(** [get_type_of] performs beta reduction ; + Is it ok for Retyping.get_type_of (Zpower_nat n q) to return (fun _ : nat => Z) q ? *) +let get_type_of env evd e = + Tacred.cbv_beta env evd (Retyping.get_type_of env evd e) + +(** [unsafe_to_constr c] returns a [Constr.t] without considering an evar_map. + This is useful for calling Constr.hash *) +let unsafe_to_constr = EConstr.Unsafe.to_constr + +let pr_constr env evd e = Printer.pr_econstr_env env evd e + +(** [get_arrow_typ evd t] returns [t1;.tn] such that t = t1 -> .. -> tn.ci_npar + (only syntactic matching) + *) +let rec get_arrow_typ evd t = + match EConstr.kind evd t with + | Prod (a, p1, p2) (*when a.Context.binder_name = Names.Anonymous*) -> + p1 :: get_arrow_typ evd p2 + | _ -> [t] + +(** [get_binary_arrow t] return t' such that t = t' -> t' -> t' *) +let get_binary_arrow evd t = + let l = get_arrow_typ evd t in + match l with + | [] -> assert false + | [t1; t2; t3] -> Some (t1, t2, t3) + | _ -> None + +(** [get_unary_arrow t] return t' such that t = t' -> t' *) +let get_unary_arrow evd t = + let l = get_arrow_typ evd t in + match l with [] -> assert false | [t1; t2] -> Some (t1, t2) | _ -> None + +(** [HConstr] is a map indexed by EConstr.t. + It should only be used using closed terms. + *) +module HConstr = struct + module M = Map.Make (struct + type t = EConstr.t + + let compare c c' = + Constr.compare (unsafe_to_constr c) (unsafe_to_constr c') + end) + + let lfind h m = try M.find h m with Not_found -> [] + + let add h e m = + let l = lfind h m in + M.add h (e :: l) m + + let empty = M.empty + + let find h m = match lfind h m with e :: _ -> e | [] -> raise Not_found + + let find_all = lfind + + let fold f m acc = + M.fold (fun k l acc -> List.fold_left (fun acc e -> f k e acc) acc l) m acc + + let iter = M.iter + +end + +(** [get_projections_from_constant (evd,c) ] + returns an array of constr [| a1,.. an|] such that [c] is defined as + Definition c := mk a1 .. an with mk a constructor. + ai is therefore either a type parameter or a projection. + *) +let get_projections_from_constant (evd, i) = + match Constr.kind (unsafe_to_constr i) with + | Constr.Const (c, u) -> + (match Environ.constant_opt_value_in (Global.env ()) (c,u) with + | None -> failwith "Add Injection requires a constant (with a body)" + | Some c -> ( + match EConstr.kind evd (EConstr.of_constr c) with + | App (c, a) -> Some a + | _ -> None )) + | _ -> None + + +(** An instance of type, say T, is registered into a hashtable, say TableT. *) + +type 'a decl = + { decl: EConstr.t + ; (* Registered type instance *) + deriv: 'a + (* Projections of insterest *) } + +(* Different type of declarations *) +type decl_kind = + | PropOp + | InjTyp + | BinRel + | BinOp + | UnOp + | CstOp + | Saturate + +let string_of_decl = function + | PropOp -> "PropOp" + | InjTyp -> "InjTyp" + | BinRel -> "BinRel" + | BinOp -> "BinOp" + | UnOp -> "UnOp" + | CstOp -> "CstOp" + | Saturate -> "Saturate" + + + + + +module type Elt = sig + type elt + + val name : decl_kind + (** [name] of the table *) + + val get_key : int + (** [get_key] is the type-index used as key for the instance *) + + val mk_elt : Evd.evar_map -> EConstr.t -> EConstr.t array -> elt + (** [mk_elt evd i [a0,..,an] returns the element of the table + built from the type-instance i and the arguments (type indexes and projections) + of the type-class constructor. *) + + val reduce_term : Evd.evar_map -> EConstr.t -> EConstr.t + (** [reduce_term evd t] normalises [t] in a table dependent way. *) + +end + +module type S = sig + val register : Constrexpr.constr_expr -> unit + + val print : unit -> unit +end + +let not_registered = Summary.ref ~name:"zify_to_register" [] + +module MakeTable (E : Elt) = struct + (** Given a term [c] and its arguments ai, + we construct a HConstr.t table that is + indexed by ai for i = E.get_key. + The elements of the table are built using E.mk_elt c [|a0,..,an|] + *) + + let make_elt (evd, i) = + match get_projections_from_constant (evd, i) with + | None -> + let env = Global.env () in + let t = string_of_ppcmds (pr_constr env evd i) in + failwith ("Cannot register term " ^ t) + | Some a -> E.mk_elt evd i a + + let table = Summary.ref ~name:("zify_" ^ string_of_decl E.name) HConstr.empty + + let register_constr env evd c = + let c = EConstr.of_constr c in + let t = get_type_of env evd c in + match EConstr.kind evd t with + | App (intyp, args) -> + let styp = E.reduce_term evd args.(E.get_key) in + let elt = {decl= c; deriv= make_elt (evd, c)} in + table := HConstr.add styp elt !table + | _ -> failwith "Can only register terms of type [F X1 .. Xn]" + + let get evd c = + let c' = E.reduce_term evd c in + HConstr.find c' !table + + let get_all evd c = + let c' = E.reduce_term evd c in + HConstr.find_all c' !table + + let fold_declared_const f evd acc = + HConstr.fold + (fun _ e acc -> f (fst (EConstr.destConst evd e.decl)) acc) + !table acc + + exception FoundNorm of EConstr.t + + let can_unify evd k t = + try + let _ = Unification.w_unify (Global.env ()) evd Reduction.CONV k t in + true ; + with _ -> false + + let unify_with_key evd t = + try + HConstr.iter + (fun k _ -> + if can_unify evd k t + then raise (FoundNorm k) + else ()) !table ; t + with FoundNorm k -> k + + + let pp_keys () = + let env = Global.env () in + let evd = Evd.from_env env in + HConstr.fold + (fun k _ acc -> Pp.(pr_constr env evd k ++ str " " ++ acc)) + !table (Pp.str "") + + let register_obj : Constr.constr -> Libobject.obj = + let cache_constr (_, c) = + not_registered := (E.name,c)::!not_registered + in + let subst_constr (subst, c) = Mod_subst.subst_mps subst c in + Libobject.declare_object + @@ Libobject.superglobal_object_nodischarge + ("register-zify-" ^ string_of_decl E.name) + ~cache:cache_constr ~subst:(Some subst_constr) + + (** [register c] is called from the VERNACULAR ADD [name] constr(t). + The term [c] is interpreted and + registered as a [superglobal_object_nodischarge]. + TODO: pre-compute [get_type_of] - [cache_constr] is using another environment. + *) + let register c = + let env = Global.env () in + let evd = Evd.from_env env in + let evd, c = Constrintern.interp_open_constr env evd c in + let _ = Lib.add_anonymous_leaf (register_obj (EConstr.to_constr evd c)) in + () + + let print () = Feedback.msg_notice (pp_keys ()) +end + +(** Each type-class gives rise to a different table. + They only differ on how projections are extracted. *) +module InjElt = struct + type elt = + { isid: bool + ; (* S = T -> inj = fun x -> x*) + source: EConstr.t + ; (* S *) + target: EConstr.t + ; (* T *) + (* projections *) + inj: EConstr.t + ; (* S -> T *) + pred: EConstr.t + ; (* T -> Prop *) + cstr: EConstr.t option + (* forall x, pred (inj x) *) } + + let name = InjTyp + + let mk_elt evd i (a : EConstr.t array) = + let isid = EConstr.eq_constr evd a.(0) a.(1) in + { isid + ; source= a.(0) + ; target= a.(1) + ; inj= a.(2) + ; pred= a.(3) + ; cstr= (if isid then None else Some a.(4)) } + + let get_key = 0 + + let reduce_term evd t = t + +end + +module InjTable = MakeTable (InjElt) + + +let coq_eq = lazy ( EConstr.of_constr + (UnivGen.constr_of_monomorphic_global + (Coqlib.lib_ref ("core.eq.type")))) + +let reduce_type evd ty = + try ignore (InjTable.get evd ty) ; ty + with Not_found -> + (* Maybe it unifies *) + InjTable.unify_with_key evd ty + +module EBinOp = struct + type elt = + { (* Op : source1 -> source2 -> source3 *) + source1: EConstr.t + ; source2: EConstr.t + ; source3: EConstr.t + ; target: EConstr.t + ; inj1: EConstr.t + ; (* InjTyp source1 target *) + inj2: EConstr.t + ; (* InjTyp source2 target *) + inj3: EConstr.t + ; (* InjTyp source3 target *) + tbop: EConstr.t + (* TBOpInj *) } + + let name = BinOp + + let mk_elt evd i a = + { source1= a.(0) + ; source2= a.(1) + ; source3= a.(2) + ; target= a.(3) + ; inj1= a.(5) + ; inj2= a.(6) + ; inj3= a.(7) + ; tbop= a.(9) } + + let get_key = 4 + + let reduce_term evd t = t + +end + +module ECstOp = struct + type elt = {source: EConstr.t; target: EConstr.t; inj: EConstr.t} + + let name = CstOp + + let mk_elt evd i a = {source= a.(0); target= a.(1); inj= a.(3)} + + let get_key = 2 + + let reduce_term evd t = t + +end + + +module EUnOp = struct + type elt = + { source1: EConstr.t + ; source2: EConstr.t + ; target: EConstr.t + ; inj1_t: EConstr.t + ; inj2_t: EConstr.t + ; unop: EConstr.t } + + let name = UnOp + + let mk_elt evd i a = + { source1= a.(0) + ; source2= a.(1) + ; target= a.(2) + ; inj1_t= a.(4) + ; inj2_t= a.(5) + ; unop= a.(6) } + + let get_key = 3 + + let reduce_term evd t = t + +end + +open EUnOp + +module EBinRel = struct + type elt = + {source: EConstr.t; target: EConstr.t; inj: EConstr.t; brel: EConstr.t} + + let name = BinRel + + let mk_elt evd i a = {source= a.(0); target= a.(1); inj= a.(3); brel= a.(4)} + + let get_key = 2 + + + (** [reduce_term evd t] if t = @eq ty normalises ty to a declared type e.g Z if it exists. *) + let reduce_term evd t = + match EConstr.kind evd t with + | App(c,a) -> if EConstr.eq_constr evd (Lazy.force coq_eq) c + then + match a with + | [| ty |] -> EConstr.mkApp(c,[| reduce_type evd ty|]) + | _ -> t + else t + | _ -> t + +end + +module EPropOp = struct + type elt = EConstr.t + + let name = PropOp + + let mk_elt evd i a = i + + let get_key = 0 + + let reduce_term evd t = t + +end + +module ESat = struct + type elt = {parg1: EConstr.t; parg2: EConstr.t; satOK: EConstr.t} + + let name = Saturate + + let mk_elt evd i a = {parg1= a.(2); parg2= a.(3); satOK= a.(5)} + + let get_key = 1 + + let reduce_term evd t = t + +end + + + +module BinOp = MakeTable (EBinOp) +module UnOp = MakeTable (EUnOp) +module CstOp = MakeTable (ECstOp) +module BinRel = MakeTable (EBinRel) +module PropOp = MakeTable (EPropOp) +module Saturate = MakeTable (ESat) + + + + +(** The module [Spec] is used to register + the instances of [BinOpSpec], [UnOpSpec]. + They are not indexed and stored in a list. *) + +module Spec = struct + let table = Summary.ref ~name:"zify_Spec" [] + + let register_obj : Constr.constr -> Libobject.obj = + let cache_constr (_, c) = table := EConstr.of_constr c :: !table in + let subst_constr (subst, c) = Mod_subst.subst_mps subst c in + Libobject.declare_object + @@ Libobject.superglobal_object_nodischarge "register-zify-Spec" + ~cache:cache_constr ~subst:(Some subst_constr) + + let register c = + let env = Global.env () in + let evd = Evd.from_env env in + let _, c = Constrintern.interp_open_constr env evd c in + let _ = Lib.add_anonymous_leaf (register_obj (EConstr.to_constr evd c)) in + () + + let get () = !table + + let print () = + let env = Global.env () in + let evd = Evd.from_env env in + let constr_of_spec c = + let t = get_type_of env evd c in + match EConstr.kind evd t with + | App (intyp, args) -> pr_constr env evd args.(2) + | _ -> Pp.str "" + in + let l = + List.fold_left + (fun acc c -> Pp.(constr_of_spec c ++ str " " ++ acc)) + (Pp.str "") !table + in + Feedback.msg_notice l +end + + +let register_decl = function + | PropOp -> PropOp.register_constr + | InjTyp -> InjTable.register_constr + | BinRel -> BinRel.register_constr + | BinOp -> BinOp.register_constr + | UnOp -> UnOp.register_constr + | CstOp -> CstOp.register_constr + | Saturate -> Saturate.register_constr + + +let process_decl (d,c) = + let env = Global.env () in + let evd = Evd.from_env env in + register_decl d env evd c + +let process_all_decl () = + List.iter process_decl !not_registered ; + not_registered := [] + + +let unfold_decl evd = + let f cst acc = cst :: acc in + let acc = InjTable.fold_declared_const f evd [] in + let acc = BinOp.fold_declared_const f evd acc in + let acc = UnOp.fold_declared_const f evd acc in + let acc = CstOp.fold_declared_const f evd acc in + let acc = BinRel.fold_declared_const f evd acc in + let acc = PropOp.fold_declared_const f evd acc in + acc + +open InjElt + +(** Get constr of lemma and projections in ZifyClasses. *) + +let zify str = + EConstr.of_constr + (UnivGen.constr_of_monomorphic_global + (Coqlib.lib_ref ("ZifyClasses." ^ str))) + +let locate_const str = + let rf = "ZifyClasses." ^ str in + match Coqlib.lib_ref rf with + | GlobRef.ConstRef c -> c + | _ -> CErrors.anomaly Pp.(str rf ++ str " should be a constant") + +(* The following [constr] are necessary for constructing the proof terms *) +let mkapp2 = lazy (zify "mkapp2") + +let mkapp = lazy (zify "mkapp") + +let mkapp0 = lazy (zify "mkapp0") + +let mkdp = lazy (zify "mkinjterm") + +let eq_refl = lazy (zify "eq_refl") + +let mkrel = lazy (zify "mkrel") + +let mkprop_op = lazy (zify "mkprop_op") + +let mkuprop_op = lazy (zify "mkuprop_op") + +let mkdpP = lazy (zify "mkinjprop") + +let iff_refl = lazy (zify "iff_refl") + +let q = lazy (zify "target_prop") + +let ieq = lazy (zify "injprop_ok") + +let iff = lazy (zify "iff") + + + +(* A super-set of the previous are needed to unfold the generated proof terms. *) + +let to_unfold = + lazy + (List.map locate_const + [ "source_prop" + ; "target_prop" + ; "uop_iff" + ; "op_iff" + ; "mkuprop_op" + ; "TUOp" + ; "inj_ok" + ; "TRInj" + ; "inj" + ; "source" + ; "injprop_ok" + ; "TR" + ; "TBOp" + ; "TCst" + ; "target" + ; "mkrel" + ; "mkapp2" + ; "mkapp" + ; "mkapp0" + ; "mkprop_op" ]) + +(** Module [CstrTable] records terms [x] injected into [inj x] + together with the corresponding type constraint. + The terms are stored by side-effect during the traversal + of the goal. It must therefore be cleared before calling + the main tactic. + *) + +module CstrTable = struct + module HConstr = Hashtbl.Make (struct + type t = EConstr.t + + let hash c = Constr.hash (unsafe_to_constr c) + + let equal c c' = Constr.equal (unsafe_to_constr c) (unsafe_to_constr c') + end) + + let table : EConstr.t HConstr.t = HConstr.create 10 + + let register evd t (i : EConstr.t) = HConstr.replace table t i + + let get () = + let l = HConstr.fold (fun k i acc -> (k, i) :: acc) table [] in + HConstr.clear table ; l + + (** [gen_cstr table] asserts (cstr k) for each element of the table (k,cstr). + NB: the constraint is only asserted if it does not already exist in the context. + *) + let gen_cstr table = + Proofview.Goal.enter (fun gl -> + let evd = Tacmach.New.project gl in + (* Build the table of existing hypotheses *) + let has_hyp = + let hyps_table = HConstr.create 20 in + List.iter + (fun (_, (t : EConstr.types)) -> HConstr.replace hyps_table t ()) + (Tacmach.New.pf_hyps_types gl) ; + fun c -> HConstr.mem hyps_table c + in + (* Add the constraint (cstr k) if it is not already present *) + let gen k cstr = + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let term = EConstr.mkApp (cstr, [|k|]) in + let types = get_type_of env evd term in + if has_hyp types then Tacticals.New.tclIDTAC + else + let n = + Tactics.fresh_id_in_env Id.Set.empty + (Names.Id.of_string "cstr") + env + in + Tactics.pose_proof (Names.Name n) term ) + in + List.fold_left + (fun acc (k, i) -> Tacticals.New.tclTHEN (gen k i) acc) + Tacticals.New.tclIDTAC table ) +end + +let mkvar red evd inj v = + ( if not red then + match inj.cstr with None -> () | Some ctr -> CstrTable.register evd v ctr + ) ; + let iv = EConstr.mkApp (inj.inj, [|v|]) in + let iv = if red then Tacred.compute (Global.env ()) evd iv else iv in + EConstr.mkApp + ( force mkdp + , [| inj.source + ; inj.target + ; inj.inj + ; v + ; iv + ; EConstr.mkApp (force eq_refl, [|inj.target; iv|]) |] ) + +type texpr = + | Var of InjElt.elt * EConstr.t + (** Var is a term that cannot be injected further *) + | Constant of InjElt.elt * EConstr.t + (** Constant is a term that is solely built from constructors *) + | Injterm of EConstr.t + (** Injected is an injected term represented by a term of type [injterm] *) + +let is_constant = function Constant _ -> true | _ -> false + +let constr_of_texpr = function + | Constant (i, e) | Var (i, e) -> if i.isid then Some e else None + | _ -> None + +let inj_term_of_texpr evd = function + | Injterm e -> e + | Var (inj, e) -> mkvar false evd inj e + | Constant (inj, e) -> mkvar true evd inj e + +let mkapp2_id evd i (* InjTyp S3 T *) + inj (* deriv i *) + t (* S1 -> S2 -> S3 *) + b (* Binop S1 S2 S3 t ... *) + dbop (* deriv b *) e1 e2 = + let default () = + let e1' = inj_term_of_texpr evd e1 in + let e2' = inj_term_of_texpr evd e2 in + EBinOp.( + Injterm + (EConstr.mkApp + ( force mkapp2 + , [| dbop.source1 + ; dbop.source2 + ; dbop.source3 + ; dbop.target + ; t + ; dbop.inj1 + ; dbop.inj2 + ; dbop.inj3 + ; b + ; e1' + ; e2' |] ))) + in + if not inj.isid then default () + else + match (e1, e2) with + | Constant (_, e1), Constant (_, e2) + |Var (_, e1), Var (_, e2) + |Constant (_, e1), Var (_, e2) + |Var (_, e1), Constant (_, e2) -> + Var (inj, EConstr.mkApp (t, [|e1; e2|])) + | _, _ -> default () + +let mkapp_id evd i inj (unop, u) f e1 = + if EConstr.eq_constr evd u.unop f then + (* Injection does nothing *) + match e1 with + | Constant (_, e) | Var (_, e) -> Var (inj, EConstr.mkApp (f, [|e|])) + | Injterm e1 -> + Injterm + (EConstr.mkApp + ( force mkapp + , [| u.source1 + ; u.source2 + ; u.target + ; f + ; u.inj1_t + ; u.inj2_t + ; unop + ; e1 |] )) + else + let e1 = inj_term_of_texpr evd e1 in + Injterm + (EConstr.mkApp + ( force mkapp + , [|u.source1; u.source2; u.target; f; u.inj1_t; u.inj2_t; unop; e1|] + )) + +type typed_constr = {constr: EConstr.t; typ: EConstr.t} + +type op = + | Unop of + { unop: EConstr.t + ; (* unop : typ unop_arg -> unop_typ *) + unop_typ: EConstr.t + ; unop_arg: typed_constr } + | Binop of + { binop: EConstr.t + ; (* binop : typ binop_arg1 -> typ binop_arg2 -> binop_typ *) + binop_typ: EConstr.t + ; binop_arg1: typed_constr + ; binop_arg2: typed_constr } + + +let rec trans_expr env evd e = + (* Get the injection *) + let {decl= i; deriv= inj} = InjTable.get evd e.typ in + let e = e.constr in + if EConstr.isConstruct evd e then Constant (inj, e) (* Evaluate later *) + else + try + (* The term [e] might be a registered constant *) + let {decl= c} = CstOp.get evd e in + Injterm + (EConstr.mkApp (force mkapp0, [|inj.source; inj.target; e; i; c|])) + with Not_found -> ( + (* Let decompose the term *) + match EConstr.kind evd e with + | App (t, a) -> ( + try + match Array.length a with + | 1 -> + let {decl= unop; deriv= u} = UnOp.get evd t in + let a' = trans_expr env evd {constr= a.(0); typ= u.source1} in + if is_constant a' && EConstr.isConstruct evd t then + Constant (inj, e) + else mkapp_id evd i inj (unop, u) t a' + | 2 -> + let {decl= bop; deriv= b} = BinOp.get evd t in + let a0 = + trans_expr env evd {constr= a.(0); typ= b.EBinOp.source1} + in + let a1 = + trans_expr env evd {constr= a.(1); typ= b.EBinOp.source2} + in + if is_constant a0 && is_constant a1 && EConstr.isConstruct evd t + then Constant (inj, e) + else mkapp2_id evd i inj t bop b a0 a1 + | _ -> Var (inj, e) + with Not_found -> Var (inj, e) ) + | _ -> Var (inj, e) ) + +let trans_expr env evd e = + try trans_expr env evd e with Not_found -> + raise + (CErrors.user_err + ( Pp.str "Missing injection for type " + ++ Printer.pr_leconstr_env env evd e.typ )) + +let is_prop env sigma term = + let sort = Retyping.get_sort_of env sigma term in + Sorts.is_prop sort + +let get_rel env evd e = + let is_arrow a p1 p2 = + is_prop env evd p1 && is_prop (EConstr.push_rel (Context.Rel.Declaration.LocalAssum(a,p1)) env) evd p2 + && (a.Context.binder_name = Names.Anonymous || EConstr.Vars.noccurn evd 1 p2) + in + match EConstr.kind evd e with + | Prod (a, p1, p2) when is_arrow a p1 p2 -> + (* X -> Y becomes (fun x y => x -> y) x y *) + let name x = + Context.make_annot (Name.mk_name (Names.Id.of_string x)) Sorts.Relevant + in + let arrow = + EConstr.mkLambda + ( name "x" + , EConstr.mkProp + , EConstr.mkLambda + ( name "y" + , EConstr.mkProp + , EConstr.mkProd + ( Context.make_annot Names.Anonymous Sorts.Relevant + , EConstr.mkRel 2 + , EConstr.mkRel 2 ) ) ) + in + Binop + { binop= arrow + ; binop_typ= EConstr.mkProp + ; binop_arg1= {constr= p1; typ= EConstr.mkProp} + ; binop_arg2= {constr= p2; typ= EConstr.mkProp} } + | App (c, a) -> + let len = Array.length a in + if len >= 2 then + let c, a1, a2 = + if len = 2 then (c, a.(0), a.(1)) + else if len > 2 then + ( EConstr.mkApp (c, Array.sub a 0 (len - 2)) + , a.(len - 2) + , a.(len - 1) ) + else raise Not_found + in + let typ = get_type_of env evd c in + match get_binary_arrow evd typ with + | None -> raise Not_found + | Some (t1, t2, t3) -> + Binop + { binop= c + ; binop_typ= t3 + ; binop_arg1= {constr= a1; typ= t1} + ; binop_arg2= {constr= a2; typ= t2} } + else if len = 1 then + let typ = get_type_of env evd c in + match get_unary_arrow evd typ with + | None -> raise Not_found + | Some (t1, t2) -> + Unop {unop= c; unop_typ= t2; unop_arg= {constr= a.(0); typ= t1}} + else raise Not_found + | _ -> raise Not_found + +let get_rel env evd e = try Some (get_rel env evd e) with Not_found -> None + +type tprop = + | TProp of EConstr.t (** Transformed proposition *) + | IProp of EConstr.t (** Identical proposition *) + +let mk_iprop e = + EConstr.mkApp (force mkdpP, [|e; e; EConstr.mkApp (force iff_refl, [|e|])|]) + +let inj_prop_of_tprop = function TProp p -> p | IProp e -> mk_iprop e + +let rec trans_prop env evd e = + match get_rel env evd e with + | None -> IProp e + | Some (Binop {binop= r; binop_typ= t1; binop_arg1= a1; binop_arg2= a2}) -> + assert (EConstr.eq_constr evd EConstr.mkProp t1) ; + if EConstr.eq_constr evd a1.typ a2.typ then + (* Arguments have the same type *) + if + EConstr.eq_constr evd EConstr.mkProp t1 + && EConstr.eq_constr evd EConstr.mkProp a1.typ + then + (* Prop -> Prop -> Prop *) + try + let {decl= rop} = PropOp.get evd r in + let t1 = trans_prop env evd a1.constr in + let t2 = trans_prop env evd a2.constr in + match (t1, t2) with + | IProp _, IProp _ -> IProp e + | _, _ -> + let t1 = inj_prop_of_tprop t1 in + let t2 = inj_prop_of_tprop t2 in + TProp (EConstr.mkApp (force mkprop_op, [|r; rop; t1; t2|])) + with Not_found -> IProp e + else + (* A -> A -> Prop *) + try + let {decl= br; deriv= rop} = BinRel.get evd r in + let a1 = trans_expr env evd {a1 with typ = rop.EBinRel.source} in + let a2 = trans_expr env evd {a2 with typ = rop.EBinRel.source} in + if EConstr.eq_constr evd r rop.EBinRel.brel then + match (constr_of_texpr a1, constr_of_texpr a2) with + | Some e1, Some e2 -> IProp (EConstr.mkApp (r, [|e1; e2|])) + | _, _ -> + let a1 = inj_term_of_texpr evd a1 in + let a2 = inj_term_of_texpr evd a2 in + TProp + (EConstr.mkApp + ( force mkrel + , [| rop.EBinRel.source + ; rop.EBinRel.target + ; r + ; rop.EBinRel.inj + ; br + ; a1 + ; a2 |] )) + else + let a1 = inj_term_of_texpr evd a1 in + let a2 = inj_term_of_texpr evd a2 in + TProp + (EConstr.mkApp + ( force mkrel + , [| rop.EBinRel.source + ; rop.EBinRel.target + ; r + ; rop.EBinRel.inj + ; br + ; a1 + ; a2 |] )) + with Not_found -> IProp e + else IProp e + | Some (Unop {unop; unop_typ; unop_arg}) -> + if + EConstr.eq_constr evd EConstr.mkProp unop_typ + && EConstr.eq_constr evd EConstr.mkProp unop_arg.typ + then + try + let {decl= rop} = PropOp.get evd unop in + let t1 = trans_prop env evd unop_arg.constr in + match t1 with + | IProp _ -> IProp e + | _ -> + let t1 = inj_prop_of_tprop t1 in + TProp (EConstr.mkApp (force mkuprop_op, [|unop; rop; t1|])) + with Not_found -> IProp e + else IProp e + +let unfold n env evd c = + let cbv l = + CClosure.RedFlags.( + Tacred.cbv_norm_flags + (mkflags + (fBETA :: fMATCH :: fFIX :: fCOFIX :: fZETA :: List.map fCONST l))) + in + let unfold_decl = unfold_decl evd in + (* Unfold the let binding *) + let c = + match n with + | None -> c + | Some n -> + Tacred.unfoldn [(Locus.AllOccurrences, Names.EvalVarRef n)] env evd c + in + (* Reduce the term *) + let c = cbv (force to_unfold @ unfold_decl) env evd c in + c + +let trans_check_prop env evd t = + if is_prop env evd t then + (*let t = Tacred.unfoldn [Locus.AllOccurrences, Names.EvalConstRef coq_not] env evd t in*) + match trans_prop env evd t with IProp e -> None | TProp e -> Some e + else None + +let trans_hyps env evd l = + List.fold_left + (fun acc (h, p) -> + match trans_check_prop env evd p with + | None -> acc + | Some p' -> (h, p, p') :: acc ) + [] (List.rev l) + +(* Only used if a direct rewrite fails *) +let trans_hyp h t = + Tactics.( + Tacticals.New.( + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let n = + fresh_id_in_env Id.Set.empty (Names.Id.of_string "__zify") env + in + let h' = fresh_id_in_env Id.Set.empty h env in + tclTHENLIST + [ letin_tac None (Names.Name n) t None + Locus.{onhyps= None; concl_occs= NoOccurrences} + ; assert_by (Name.Name h') + (EConstr.mkApp (force q, [|EConstr.mkVar n|])) + (tclTHEN + (Equality.rewriteRL + (EConstr.mkApp (force ieq, [|EConstr.mkVar n|]))) + (exact_check (EConstr.mkVar h))) + ; reduct_in_hyp ~check:true ~reorder:false (unfold (Some n)) + (h', Locus.InHyp) + ; clear [n] + ; (* [clear H] may fail if [h] has dependencies *) + tclTRY (clear [h]) ] ))) + +let is_progress_rewrite evd t rew = + match EConstr.kind evd rew with + | App (c, [|lhs; rhs|]) -> + if EConstr.eq_constr evd (force iff) c then + (* This is a successful rewriting *) + not (EConstr.eq_constr evd lhs rhs) + else + CErrors.anomaly + Pp.( + str "is_progress_rewrite: not a rewrite" + ++ pr_constr (Global.env ()) evd rew) + | _ -> failwith "is_progress_rewrite: not even an application" + +let trans_hyp h t0 t = + Tacticals.New.( + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + let t' = unfold None env evd (EConstr.mkApp (force ieq, [|t|])) in + if is_progress_rewrite evd t0 (get_type_of env evd t') then + tclFIRST + [ Equality.general_rewrite_in true Locus.AllOccurrences true false + h t' false + ; trans_hyp h t ] + else tclIDTAC )) + +let trans_concl t = + Tacticals.New.( + Proofview.Goal.enter (fun gl -> + let concl = Tacmach.New.pf_concl gl in + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + let t' = unfold None env evd (EConstr.mkApp (force ieq, [|t|])) in + if is_progress_rewrite evd concl (get_type_of env evd t') then + Equality.general_rewrite true Locus.AllOccurrences true false t' + else tclIDTAC )) + +let tclTHENOpt e tac tac' = + match e with None -> tac' | Some e' -> Tacticals.New.tclTHEN (tac e') tac' + +let zify_tac = + Proofview.Goal.enter (fun gl -> + Coqlib.check_required_library ["Coq"; "micromega"; "ZifyClasses"] ; + Coqlib.check_required_library ["Coq"; "micromega"; "ZifyInst"] ; + process_all_decl (); + let evd = Tacmach.New.project gl in + let env = Tacmach.New.pf_env gl in + let concl = trans_check_prop env evd (Tacmach.New.pf_concl gl) in + let hyps = trans_hyps env evd (Tacmach.New.pf_hyps_types gl) in + let l = CstrTable.get () in + tclTHENOpt concl trans_concl + (Tacticals.New.tclTHEN + (Tacticals.New.tclTHENLIST + (List.map (fun (h, p, t) -> trans_hyp h p t) hyps)) + (CstrTable.gen_cstr l)) ) + +let iter_specs tac = + Tacticals.New.tclTHENLIST + (List.fold_right (fun d acc -> tac d :: acc) (Spec.get ()) []) + + +let iter_specs (tac: Ltac_plugin.Tacinterp.Value.t) = + iter_specs (fun c -> Ltac_plugin.Tacinterp.Value.apply tac [Ltac_plugin.Tacinterp.Value.of_constr c]) + +let find_hyp evd t l = + try Some (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l)) + with Not_found -> None + +let sat_constr c d = + Proofview.Goal.enter (fun gl -> + let evd = Tacmach.New.project gl in + let env = Tacmach.New.pf_env gl in + let hyps = Tacmach.New.pf_hyps_types gl in + match EConstr.kind evd c with + | App (c, args) -> + if Array.length args = 2 then ( + let h1 = + Tacred.cbv_beta env evd + (EConstr.mkApp (d.ESat.parg1, [|args.(0)|])) + in + let h2 = + Tacred.cbv_beta env evd + (EConstr.mkApp (d.ESat.parg2, [|args.(1)|])) + in + match (find_hyp evd h1 hyps, find_hyp evd h2 hyps) with + | Some h1, Some h2 -> + let n = + Tactics.fresh_id_in_env Id.Set.empty + (Names.Id.of_string "__sat") + env + in + let trm = + EConstr.mkApp + ( d.ESat.satOK + , [|args.(0); args.(1); EConstr.mkVar h1; EConstr.mkVar h2|] + ) + in + Tactics.pose_proof (Names.Name n) trm + | _, _ -> Tacticals.New.tclIDTAC ) + else Tacticals.New.tclIDTAC + | _ -> Tacticals.New.tclIDTAC ) + +let saturate = + Proofview.Goal.enter (fun gl -> + let table = CstrTable.HConstr.create 20 in + let concl = Tacmach.New.pf_concl gl in + let hyps = Tacmach.New.pf_hyps_types gl in + let evd = Tacmach.New.project gl in + process_all_decl (); + let rec sat t = + match EConstr.kind evd t with + | App (c, args) -> + sat c ; + Array.iter sat args ; + if Array.length args = 2 then + let ds = Saturate.get_all evd c in + if ds = [] then () + else ( + List.iter (fun x -> CstrTable.HConstr.add table t x.deriv) ds ) + else () + | Prod (a, t1, t2) when a.Context.binder_name = Names.Anonymous -> + sat t1 ; sat t2 + | _ -> () + in + (* Collect all the potential saturation lemma *) + sat concl ; + List.iter (fun (_, t) -> sat t) hyps ; + Tacticals.New.tclTHENLIST + (CstrTable.HConstr.fold (fun c d acc -> sat_constr c d :: acc) table []) + ) diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli new file mode 100644 index 0000000000..f7844f53bc --- /dev/null +++ b/plugins/micromega/zify.mli @@ -0,0 +1,25 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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) *) +(************************************************************************) +open Constrexpr + +module type S = sig val register : constr_expr -> unit val print : unit -> unit end + +module InjTable : S +module UnOp : S +module BinOp : S +module CstOp : S +module BinRel : S +module PropOp : S +module Spec : S +module Saturate : S + +val zify_tac : unit Proofview.tactic +val saturate : unit Proofview.tactic +val iter_specs : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic diff --git a/plugins/micromega/zify_plugin.mlpack b/plugins/micromega/zify_plugin.mlpack new file mode 100644 index 0000000000..8d301b53c4 --- /dev/null +++ b/plugins/micromega/zify_plugin.mlpack @@ -0,0 +1,2 @@ +Zify +G_zify diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index acc8214e3e..f5d53cbbf3 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -127,6 +127,8 @@ Module Z. Ltac to_euclidean_division_equations := div_mod_to_equations'; quot_rem_to_equations'; euclidean_division_equations_cleanup. End Z. +Set Warnings "-deprecated-tactic". + (** * zify: the Z-ification tactic *) (* This tactic searches for nat and N and positive elements in the goal and @@ -150,12 +152,14 @@ End Z. (** I) translation of Z.max, Z.min, Z.abs, Z.sgn into recognized equations *) +#[deprecated( note = "Use 'zify' instead")] 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. +#[deprecated( note = "Use 'zify' instead")] Ltac zify_unop_var_or_term t thm a := (* If a is a variable, no need for aliasing *) let za := fresh "z" in @@ -163,6 +167,7 @@ Ltac zify_unop_var_or_term t thm a := (* Otherwise, a is a complex term: we alias it. *) (remember a as za; zify_unop_core t thm za). +#[deprecated( note = "Use 'zify' instead")] 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) *) @@ -174,6 +179,7 @@ Ltac zify_unop t thm a := | _ => zify_unop_var_or_term t thm a end. +#[deprecated( note = "Use 'zify' instead")] 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 @@ -182,6 +188,7 @@ Ltac zify_unop_nored t thm a := | _ => zify_unop_var_or_term t thm a end. +#[deprecated( note = "Use 'zify' instead")] 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 *) @@ -197,6 +204,7 @@ Ltac zify_binop t thm a b:= end) end. +#[deprecated( note = "Use 'zify' instead")] 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 @@ -213,9 +221,6 @@ Ltac zify_op_1 := Ltac zify_op := repeat zify_op_1. - - - (** II) Conversion from nat to Z *) @@ -226,6 +231,7 @@ Ltac hide_Z_of_nat t := change Z.of_nat with Z_of_nat' in z; unfold z in *; clear z. +#[deprecated( note = "Use 'zify' instead")] Ltac zify_nat_rel := match goal with (* I: equalities *) @@ -321,11 +327,9 @@ Ltac zify_nat_op := pose proof (Nat2Z.is_nonneg a); hide_Z_of_nat a end. +#[deprecated( note = "Use 'zify' instead")] 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. @@ -336,6 +340,7 @@ Ltac hide_Zpos t := change Zpos with Zpos' in z; unfold z in *; clear z. +#[deprecated( note = "Use 'zify' instead")] Ltac zify_positive_rel := match goal with (* I: equalities *) @@ -357,6 +362,7 @@ Ltac zify_positive_rel := | |- context [ (?a >= ?b)%positive ] => change (a>=b)%positive with (Zpos a>=Zpos b) end. +#[deprecated( note = "Use 'zify' instead")] Ltac zify_positive_op := match goal with (* Z.pow_pos -> Z.pow *) @@ -453,6 +459,7 @@ Ltac zify_positive_op := | |- context [ Zpos ?a ] => pose proof (Pos2Z.is_pos a); hide_Zpos a end. +#[deprecated( note = "Use 'zify' instead")] Ltac zify_positive := repeat zify_positive_rel; repeat zify_positive_op; unfold Zpos',Zneg' in *. @@ -469,6 +476,7 @@ Ltac hide_Z_of_N t := change Z.of_N with Z_of_N' in z; unfold z in *; clear z. +#[deprecated( note = "Use 'zify' instead")] Ltac zify_N_rel := match goal with (* I: equalities *) @@ -490,6 +498,7 @@ Ltac zify_N_rel := | |- context [ (?a >= ?b)%N ] => rewrite (N2Z.inj_ge a b) end. +#[deprecated( note = "Use 'zify' instead")] Ltac zify_N_op := match goal with (* misc type conversions: nat to positive *) @@ -556,10 +565,35 @@ Ltac zify_N_op := | |- context [ Z.of_N ?a ] => pose proof (N2Z.is_nonneg a); hide_Z_of_N a end. +#[deprecated( note = "Use 'zify' instead")] Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. +(** The complete Z-ification tactic *) +Require Import ZifyClasses ZifyInst. +Require Zify. + + +(** [is_inj T] returns true iff the type T has an injection *) +Ltac is_inj T := + match T with + | _ => let x := constr:(_ : InjTyp T _ ) in true + | _ => false + end. + +(* [elim_let] replaces a let binding (x := e : t) + by an equation (x = e) if t is an injected type *) +Ltac elim_let := + repeat + match goal with + | x := ?t : ?ty |- _ => + let b := is_inj ty in + match b with + | true => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x + end + end. -(** The complete Z-ification tactic *) -Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op. +Ltac zify := + intros ; elim_let ; + Zify.zify ; ZifyInst.saturate. diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg index bb9bee080a..84964a7bd2 100644 --- a/plugins/omega/g_omega.mlg +++ b/plugins/omega/g_omega.mlg @@ -54,6 +54,7 @@ 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"] } +| [ "omega" "with" "*" ] -> + { Tacticals.New.tclTHEN (eval_tactic "zify") (omega_tactic []) } END diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex e0324b0232..b3bcb5b056 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache diff --git a/test-suite/micromega/non_lin_ci.v b/test-suite/micromega/non_lin_ci.v index ec39209230..2a66cc9a5a 100644 --- a/test-suite/micromega/non_lin_ci.v +++ b/test-suite/micromega/non_lin_ci.v @@ -43,18 +43,18 @@ Proof. Qed. Goal - forall (__x1 __x2 __x3 __x4 __x5 __x6 __x7 __x8 __x9 __x10 __x11 __x12 __x13 - __x14 __x15 __x16 : Z) - (H6 : __x8 < __x10 ^ 2 * __x15 ^ 2 + 2 * __x10 * __x15 * __x14 + __x14 ^ 2) - (H7 : 0 <= __x8) - (H12 : 0 <= __x14) - (H0 : __x8 = __x15 * __x11 + __x9) - (H14 : __x10 ^ 2 * __x15 + __x10 * __x14 < __x16) - (H17 : __x16 <= 0) - (H15 : 0 <= __x9) - (H18 : __x9 < __x15) - (H16 : 0 <= __x12) - (H19 : __x12 < (__x10 * __x15 + __x14) * __x10) + forall (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 + x14 x15 x16 : Z) + (H6 : x8 < x10 ^ 2 * x15 ^ 2 + 2 * x10 * x15 * x14 + x14 ^ 2) + (H7 : 0 <= x8) + (H12 : 0 <= x14) + (H0 : x8 = x15 * x11 + x9) + (H14 : x10 ^ 2 * x15 + x10 * x14 < x16) + (H17 : x16 <= 0) + (H15 : 0 <= x9) + (H18 : x9 < x15) + (H16 : 0 <= x12) + (H19 : x12 < (x10 * x15 + x14) * x10) , False. Proof. intros. diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v index 52dc9ed2e0..354c608e23 100644 --- a/test-suite/micromega/rexample.v +++ b/test-suite/micromega/rexample.v @@ -24,6 +24,16 @@ Proof. lra. Qed. +Goal + forall (a c : R) + (Had : a <> a), + a > c. +Proof. + intros. + lra. +Qed. + + (* Other (simple) examples *) Lemma binomial : forall x y, ((x+y)^2 = x^2 + 2 *x*y + y^2). @@ -32,7 +42,6 @@ Proof. lra. Qed. - Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m. Proof. intros ; lra. diff --git a/test-suite/micromega/rsyntax.v b/test-suite/micromega/rsyntax.v index f02d93f911..a0afe99181 100644 --- a/test-suite/micromega/rsyntax.v +++ b/test-suite/micromega/rsyntax.v @@ -60,7 +60,6 @@ Proof. lia. (* exponent is a constant expr *) Qed. - Goal (1 / IZR (Z.pow_pos 10 25) = 1 / 10 ^ 25)%R. Proof. lra. diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v index 55691f553c..3d99af95ec 100644 --- a/test-suite/micromega/zomicron.v +++ b/test-suite/micromega/zomicron.v @@ -1,5 +1,63 @@ Require Import ZArith. Require Import Lia. + +Section S. + Variables H1 H2 H3 H4 : True. + + Lemma bug_9848 : True. + Proof using. + lia. + Qed. +End S. + +Lemma concl_in_Type : forall (k : nat) + (H : (k < 0)%nat) (F : k < 0 -> Type), + F H. +Proof. + intros. + lia. +Qed. + +Lemma bug_10707 : forall + (T : Type) + (t : nat -> Type) + (k : nat) + (default : T) + (arr : t 0 -> T) + (H : (k < 0)%nat) of_nat_lt, + match k with + | 0 | _ => default + end = arr (of_nat_lt H). +Proof. + intros. + lia. +Qed. + +Axiom decompose_nat : nat -> nat -> nat. +Axiom inleft : forall {P}, {m : nat & P m} -> nat. +Axiom foo : nat. + +Lemma bug_7886 : forall (x x0 : nat) + (e : 0 = x0 + S x) + (H : decompose_nat x 0 = inleft (existT (fun m : nat => 0 = m + S x) x0 e)) + (x1 : nat) + (e0 : 0 = x1 + S (S x)) + (H1 : decompose_nat (S x) 0 = inleft (existT (fun m : nat => 0 = m + S (S x)) x1 e0)), + False. +Proof. + intros. + lia. +Qed. + + +Lemma bug_8898 : forall (p : 0 < 0) (H: p = p), False. +Proof. + intros p H. + lia. +Qed. + + + Open Scope Z_scope. Lemma two_x_eq_1 : forall x, 2 * x = 1 -> False. @@ -34,12 +92,12 @@ Proof. Qed. Lemma compact_proof : forall z, - (z < 0) -> - (z >= 0) -> - (0 >= z \/ 0 < z) -> False. + (z < 0) -> + (z >= 0) -> + (0 >= z \/ 0 < z) -> False. Proof. - intros. - lia. + intros. + lia. Qed. Lemma dummy_ex : exists (x:Z), x = x. @@ -74,9 +132,17 @@ Proof. lia. Qed. + +Lemma fresh1 : forall (__p1 __p2 __p3 __p5:Prop) (x y z:Z), (x = 0 /\ y = 0) /\ z = 0 -> x = 0. +Proof. + intros. + lia. +Qed. + + Class Foo {x : Z} := { T : Type ; dec : T -> Z }. Goal forall bound {F : @Foo bound} (x y : T), 0 <= dec x < bound -> 0 <= dec y -< bound -> dec x + dec y >= bound -> dec x + dec y < 2 * bound. + < bound -> dec x + dec y >= bound -> dec x + dec y < 2 * bound. Proof. intros. lia. @@ -98,7 +164,19 @@ Section S. lia. Qed. - End S. +End S. + +Section S. + Variable x y: Z. + Variable H1 : 1 > 0 -> x = 1. + Variable H2 : x = y. + + Goal x = y. + Proof using H2. + lia. + Qed. + +End S. (* Bug 5073 *) Lemma opp_eq_0_iff a : -a = 0 <-> a = 0. @@ -122,8 +200,50 @@ Goal forall (H5 : - b < r) (H6 : r <= 0) (H2 : 0 <= b), - b = 0 -> False. + b = 0 -> False. Proof. intros b q r. lia. Qed. + + +Section S. + (* From bedrock2, used to be slow *) + Variables (x3 q r q2 r3 : Z) + (H : 2 ^ 2 <> 0 -> r3 + 3 = 2 ^ 2 * q + r) + (H0 : 0 < 2 ^ 2 -> 0 <= r < 2 ^ 2) + (H1 : 2 ^ 2 < 0 -> 2 ^ 2 < r <= 0) + (H2 : 2 ^ 2 = 0 -> q = 0) + (H3 : 2 ^ 2 = 0 -> r = 0) + (q0 r0 : Z) + (H4 : 4 <> 0 -> 0 = 4 * q0 + r0) + (H5 : 0 < 4 -> 0 <= r0 < 4) + (H6 : 4 < 0 -> 4 < r0 <= 0) + (H7 : 4 = 0 -> q0 = 0) + (H8 : 4 = 0 -> r0 = 0) + (q1 r1 : Z) + (H9 : 4 <> 0 -> q + q + (q + q) = 4 * q1 + r1) + (H10 : 0 < 4 -> 0 <= r1 < 4) + (H11 : 4 < 0 -> 4 < r1 <= 0) + (H12 : 4 = 0 -> q1 = 0) + (H13 : 4 = 0 -> r1 = 0) + (r2 : Z) + (H14 : 2 ^ 16 <> 0 -> x3 = 2 ^ 16 * q2 + r2) + (H15 : 0 < 2 ^ 16 -> 0 <= r2 < 2 ^ 16) + (H16 : 2 ^ 16 < 0 -> 2 ^ 16 < r2 <= 0) + (H17 : 2 ^ 16 = 0 -> q2 = 0) + (H18 : 2 ^ 16 = 0 -> r2 = 0) + (q3 : Z) + (H19 : 16383 + 1 <> 0 -> q2 = (16383 + 1) * q3 + r3) + (H20 : 0 < 16383 + 1 -> 0 <= r3 < 16383 + 1) + (H21 : 16383 + 1 < 0 -> 16383 + 1 < r3 <= 0) + (H22 : 16383 + 1 = 0 -> q3 = 0) + (H23 : 16383 + 1 = 0 -> r3 = 0). + + Goal r0 = r1. + Proof using H10 H9 H5 H4. + intros. + lia. + Qed. + +End S. diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v index c0ef9b392d..668be1fdbc 100644 --- a/test-suite/output/MExtraction.v +++ b/test-suite/output/MExtraction.v @@ -1,14 +1,65 @@ -Require Import micromega.MExtraction. -Require Import RingMicromega. -Require Import QArith. -Require Import VarMap. +(************************************************************************) +(* * 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) *) +(************************************************************************) +(* *) +(* Micromega: A reflexive tactic using the Positivstellensatz *) +(* *) +(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* *) +(************************************************************************) + +(* Used to generate micromega.ml *) + +Require Extraction. Require Import ZMicromega. Require Import QMicromega. Require Import RMicromega. +Require Import VarMap. +Require Import RingMicromega. +Require Import NArith. +Require Import QArith. + +Extract Inductive prod => "( * )" [ "(,)" ]. +Extract Inductive list => list [ "[]" "(::)" ]. +Extract Inductive bool => bool [ true false ]. +Extract Inductive sumbool => bool [ true false ]. +Extract Inductive option => option [ Some None ]. +Extract Inductive sumor => option [ Some None ]. +(** Then, in a ternary alternative { }+{ }+{ }, + - leftmost choice (Inleft Left) is (Some true), + - middle choice (Inleft Right) is (Some false), + - rightmost choice (Inright) is (None) *) + + +(** To preserve its laziness, andb is normally expanded. + Let's rather use the ocaml && *) +Extract Inlined Constant andb => "(&&)". + +Import Reals.Rdefinitions. + +Extract Constant R => "int". +Extract Constant R0 => "0". +Extract Constant R1 => "1". +Extract Constant Rplus => "( + )". +Extract Constant Rmult => "( * )". +Extract Constant Ropp => "fun x -> - x". +Extract Constant Rinv => "fun x -> 1 / x". +(** In order to avoid annoying build dependencies the actual + extraction is only performed as a test in the test suite. *) Recursive Extraction -Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula - ZMicromega.cnfZ ZMicromega.Zeval_const ZMicromega.bound_problem_fr QMicromega.cnfQ + Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula + Tauto.abst_form + ZMicromega.cnfZ ZMicromega.bound_problem_fr ZMicromega.Zeval_const QMicromega.cnfQ List.map simpl_cone (*map_cone indexes*) denorm Qpower vm_add normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. +(* Local Variables: *) +(* coding: utf-8 *) +(* End: *) diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v index 62ecece792..2eac9660b4 100644 --- a/test-suite/success/Nia.v +++ b/test-suite/success/Nia.v @@ -4,7 +4,8 @@ Open Scope Z_scope. (** Add [Z.to_euclidean_division_equations] to the end of [zify], just for this file. *) -Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.to_euclidean_division_equations. +Require Zify. +Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations. Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed. Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed. |