diff options
| author | Frédéric Besson | 2019-03-08 09:56:49 +0100 |
|---|---|---|
| committer | Frédéric Besson | 2019-04-01 12:08:45 +0200 |
| commit | 6f1634d2f822037a482436a64d3ef3bfb2fac2a0 (patch) | |
| tree | 2f09d223261f45a527b36231a4f74c803ccf8fa6 | |
| parent | 4c3f4d105a32cc7661ae714fe4e25619e32bc84c (diff) | |
Several improvements and fixes of Lia
- Improved reification for Micromega (support for #8764)
- Fixes #9268: Do not take universes into account in lia reification
Improve #9291 by threading the evar_map during reification.
Universes are unified.
- Remove (potentially cyclic) dependency over lra for Rle_abs
- Towards a complete simplex-based lia
fixes #9615
Lia is now exclusively using cutting plane proofs.
For this to always work, all the variables need to be positive.
Therefore, lia is pre-processing the goal for each variable x
it introduces the constraints x = y - z , y>=0 , z >= 0
for some fresh variable y and z.
For scalability, nia is currently NOT performing this pre-processing.
- Lia is using the FSet library
manual merge of commit #230899e87c51c12b2f21b6fedc414d099a1425e4
to work around a "leaked" hint breaking compatibility of eauto
37 files changed, 3346 insertions, 1285 deletions
diff --git a/CHANGES.md b/CHANGES.md index 44ce712a87..d4bb260e2c 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -114,6 +114,8 @@ Tactics - The syntax of the `autoapply` tactic was fixed to conform with preexisting documentation: it now takes a `with` clause instead of a `using` clause. + + Vernacular commands - `Combined Scheme` can now work when inductive schemes are generated in sort @@ -219,6 +221,9 @@ Standard Library - Added lemmas about `Z.testbit`, `Z.ones`, and `Z.modulo`. +- Moved the `auto` hints of the `FSet` library into a new + `fset` database. + Universes - Added `Print Universes Subgraph` variant of `Print Universes`. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 7b395900e9..afb0239be4 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3912,6 +3912,8 @@ At Coq startup, only the core database is nonempty and can be used. environment, including those used for ``setoid_rewrite``, from the Classes directory. +:fset: internal database for the implementation of the ``FSets`` library. + You are advised not to put your own hints in the core database, but use one or several databases specific to your development. diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index b58148ffff..b25104ddb9 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -22,6 +22,7 @@ plugins/extraction/Extraction.v plugins/funind/FunInd.v plugins/funind/Recdef.v plugins/ltac/Ltac.v +plugins/micromega/DeclConstant.v plugins/micromega/Env.v plugins/micromega/EnvRing.v plugins/micromega/Fourier.v diff --git a/plugins/micromega/DeclConstant.v b/plugins/micromega/DeclConstant.v new file mode 100644 index 0000000000..47fcac6481 --- /dev/null +++ b/plugins/micromega/DeclConstant.v @@ -0,0 +1,68 @@ +(************************************************************************) +(* * 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) 2019 *) +(* *) +(************************************************************************) + +(** Declaring 'allowed' terms using type classes. + + Motivation: reification needs to know which terms are allowed. + For 'lia', the constant are only the integers built from Z0, Zpos, Zneg, xH, xO, xI. + However, if the term is ground it may be convertible to an integer. + Thus we could allow i.e. sqrt z for some integer z. + + Proposal: for each type, the user declares using type-classes the set of allowed ground terms. + *) + +Require Import List. + +(** Declarative definition of constants. + These are ground terms (without variables) of interest. + e.g. nat is built from O and S + NB: this does not need to be restricted to constructors. + *) + +(** Ground terms (see [GT] below) are built inductively from declared constants. *) + +Class DeclaredConstant {T : Type} (F : T). + +Class GT {T : Type} (F : T). + +Instance GT_O {T : Type} (F : T) {DC : DeclaredConstant F} : GT F. +Defined. + +Instance GT_APP1 {T1 T2 : Type} (F : T1 -> T2) (A : T1) : + DeclaredConstant F -> + GT A -> GT (F A). +Defined. + +Instance GT_APP2 {T1 T2 T3: Type} (F : T1 -> T2 -> T3) + {A1 : T1} {A2 : T2} {DC:DeclaredConstant F} : + GT A1 -> GT A2 -> GT (F A1 A2). +Defined. + +Require Import ZArith. + +Instance DO : DeclaredConstant O := {}. +Instance DS : DeclaredConstant S := {}. +Instance DxH: DeclaredConstant xH := {}. +Instance DxI: DeclaredConstant xI := {}. +Instance DxO: DeclaredConstant xO := {}. +Instance DZO: DeclaredConstant Z0 := {}. +Instance DZpos: DeclaredConstant Zpos := {}. +Instance DZneg: DeclaredConstant Zneg := {}. +Instance DZpow_pos : DeclaredConstant Z.pow_pos := {}. + +Require Import QArith. + +Instance DQ : DeclaredConstant Qmake := {}. diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v index dd6319d5c4..1582ec554e 100644 --- a/plugins/micromega/Lia.v +++ b/plugins/micromega/Lia.v @@ -18,6 +18,7 @@ Require Import ZMicromega. Require Import ZArith. Require Import RingMicromega. Require Import VarMap. +Require Import DeclConstant. Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". @@ -25,18 +26,22 @@ Declare ML Module "micromega_plugin". Ltac preprocess := zify ; unfold Z.succ in * ; unfold Z.pred in *. -Ltac zchange := +Ltac zchange checker := intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit). + change (@Tauto.eval_bf _ (Zeval_formula (@find Z Z0 __varmap)) __ff) ; + apply (checker __ff __wit). -Ltac zchecker_no_abstract := zchange ; vm_compute ; reflexivity. +Ltac zchecker_no_abstract checker := + zchange checker ; vm_compute ; reflexivity. -Ltac zchecker_abstract := abstract (zchange ; vm_cast_no_check (eq_refl true)). +Ltac zchecker_abstract checker := + abstract (zchange checker ; vm_cast_no_check (eq_refl true)). -Ltac zchecker := zchecker_no_abstract. +Ltac zchecker := zchecker_no_abstract ZTautoChecker_sound. -Ltac lia := preprocess; xlia zchecker. +Ltac zchecker_ext := zchecker_no_abstract ZTautoCheckerExt_sound. + +Ltac lia := preprocess; xlia zchecker_ext. Ltac nia := preprocess; xnlia zchecker. diff --git a/plugins/micromega/Lqa.v b/plugins/micromega/Lqa.v index caaec541eb..f3cd24be8a 100644 --- a/plugins/micromega/Lqa.v +++ b/plugins/micromega/Lqa.v @@ -18,12 +18,13 @@ Require Import QMicromega. Require Import QArith. Require Import RingMicromega. Require Import VarMap. +Require Import DeclConstant. Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". Ltac rchange := intros __wit __varmap __ff ; - change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; + change (Tauto.eval_bf (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; apply (QTautoChecker_sound __ff __wit). Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity. diff --git a/plugins/micromega/Lra.v b/plugins/micromega/Lra.v index 4ff483fbab..72e29319ff 100644 --- a/plugins/micromega/Lra.v +++ b/plugins/micromega/Lra.v @@ -24,7 +24,7 @@ Declare ML Module "micromega_plugin". Ltac rchange := intros __wit __varmap __ff ; - change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; + change (Tauto.eval_bf (Reval_formula (@find R 0%R __varmap)) __ff) ; apply (RTautoChecker_sound __ff __wit). Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity. diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 5f01f981ef..6112eda200 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -54,8 +54,10 @@ 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. *) (*Extraction "micromega.ml" -(*Recursive Extraction*) List.map simpl_cone (*map_cone indexes*) - denorm Qpower vm_add + Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula + ZMicromega.cnfZ ZMicromega.bound_problem_fr 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: *) diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v index 2880a05d8d..0d593a321c 100644 --- a/plugins/micromega/QMicromega.v +++ b/plugins/micromega/QMicromega.v @@ -173,6 +173,7 @@ Qed. Require Import Coq.micromega.Tauto. Definition Qnormalise := @cnf_normalise Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool. + Definition Qnegate := @cnf_negate Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool. Definition qunsat := check_inconsistent 0 Qeq_bool Qle_bool. @@ -182,30 +183,36 @@ Definition qdeduce := nformula_plus_nformula 0 Qplus Qeq_bool. Definition normQ := norm 0 1 Qplus Qmult Qminus Qopp Qeq_bool. Declare Equivalent Keys normQ RingMicromega.norm. +Definition cnfQ (Annot TX AF: Type) (f: TFormula (Formula Q) Annot TX AF) := + rxcnf qunsat qdeduce (Qnormalise Annot) (Qnegate Annot) true f. Definition QTautoChecker (f : BFormula (Formula Q)) (w: list QWitness) : bool := - @tauto_checker (Formula Q) (NFormula Q) + @tauto_checker (Formula Q) (NFormula Q) unit qunsat qdeduce - Qnormalise - Qnegate QWitness QWeakChecker f w. + (Qnormalise unit) + (Qnegate unit) QWitness (fun cl => QWeakChecker (List.map fst cl)) f w. -Lemma QTautoChecker_sound : forall f w, QTautoChecker f w = true -> forall env, eval_f (Qeval_formula env) f. +Lemma QTautoChecker_sound : forall f w, QTautoChecker f w = true -> forall env, eval_bf (Qeval_formula env) f. Proof. intros f w. unfold QTautoChecker. - apply (tauto_checker_sound Qeval_formula Qeval_nformula). - apply Qeval_nformula_dec. - intros until env. - 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). - intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now apply (cnf_normalise_correct Qsor QSORaddon). - intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now apply (cnf_negate_correct Qsor QSORaddon). - intros t w0. - apply QWeakChecker_sound. + apply tauto_checker_sound with (eval:= Qeval_formula) (eval':= Qeval_nformula). + - apply Qeval_nformula_dec. + - intros until env. + 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). + - 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. + unfold eval_tt. + intros. + rewrite make_impl_map with (eval := Qeval_nformula env). + eapply QWeakChecker_sound; eauto. + tauto. Qed. (* Local Variables: *) diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index c2b40c730f..7704e42d40 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -17,10 +17,11 @@ Require Import OrderedRing. Require Import RingMicromega. Require Import Refl. -Require Import Raxioms RIneq Rpow_def DiscrR. +Require Import Raxioms Rfunctions RIneq Rpow_def DiscrR. Require Import QArith. Require Import Qfield. Require Import Qreals. +Require Import DeclConstant. Require Setoid. (*Declare ML Module "micromega_plugin".*) @@ -57,8 +58,6 @@ Proof. now apply Rmult_lt_0_compat. Qed. -Notation IQR := Q2R (only parsing). - Lemma Rinv_1 : forall x, x * / 1 = x. Proof. intro. @@ -66,13 +65,13 @@ Proof. apply Rmult_1_r. Qed. -Lemma Qeq_true : forall x y, Qeq_bool x y = true -> IQR x = IQR y. +Lemma Qeq_true : forall x y, Qeq_bool x y = true -> Q2R x = Q2R y. Proof. intros. now apply Qeq_eqR, Qeq_bool_eq. Qed. -Lemma Qeq_false : forall x y, Qeq_bool x y = false -> IQR x <> IQR y. +Lemma Qeq_false : forall x y, Qeq_bool x y = false -> Q2R x <> Q2R y. Proof. intros. apply Qeq_bool_neq in H. @@ -80,24 +79,24 @@ Proof. now apply eqR_Qeq. Qed. -Lemma Qle_true : forall x y : Q, Qle_bool x y = true -> IQR x <= IQR y. +Lemma Qle_true : forall x y : Q, Qle_bool x y = true -> Q2R x <= Q2R y. Proof. intros. now apply Qle_Rle, Qle_bool_imp_le. Qed. -Lemma IQR_0 : IQR 0 = 0. +Lemma Q2R_0 : Q2R 0 = 0. Proof. apply Rmult_0_l. Qed. -Lemma IQR_1 : IQR 1 = 1. +Lemma Q2R_1 : Q2R 1 = 1. Proof. compute. apply Rinv_1. Qed. -Lemma IQR_inv_ext : forall x, - IQR (/ x) = (if Qeq_bool x 0 then 0 else / IQR x). +Lemma Q2R_inv_ext : forall x, + Q2R (/ x) = (if Qeq_bool x 0 then 0 else / Q2R x). Proof. intros. case_eq (Qeq_bool x 0). @@ -120,12 +119,12 @@ Lemma QSORaddon : R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle (* ring elements *) Q 0%Q 1%Q Qplus Qmult Qminus Qopp (* coefficients *) Qeq_bool Qle_bool - IQR nat to_nat pow. + Q2R nat to_nat pow. Proof. constructor. constructor ; intros ; try reflexivity. - apply IQR_0. - apply IQR_1. + apply Q2R_0. + apply Q2R_1. apply Q2R_plus. apply Q2R_minus. apply Q2R_mult. @@ -136,20 +135,27 @@ Proof. apply Qle_true. Qed. +(* Syntactic ring coefficients. *) -(* Syntactic ring coefficients. - For computing, we use Q. *) Inductive Rcst := -| C0 -| C1 -| CQ (r : Q) -| CZ (r : Z) -| CPlus (r1 r2 : Rcst) -| CMinus (r1 r2 : Rcst) -| CMult (r1 r2 : Rcst) -| CInv (r : Rcst) -| COpp (r : Rcst). - + | C0 + | C1 + | CQ (r : Q) + | CZ (r : Z) + | CPlus (r1 r2 : Rcst) + | CMinus (r1 r2 : Rcst) + | CMult (r1 r2 : Rcst) + | CPow (r1 : Rcst) (z:Z+nat) + | CInv (r : Rcst) + | COpp (r : Rcst). + + + +Definition z_of_exp (z : Z + nat) := + match z with + | inl z => z + | inr n => Z.of_nat n + end. Fixpoint Q_of_Rcst (r : Rcst) : Q := match r with @@ -160,42 +166,198 @@ Fixpoint Q_of_Rcst (r : Rcst) : Q := | CPlus r1 r2 => Qplus (Q_of_Rcst r1) (Q_of_Rcst r2) | CMinus r1 r2 => Qminus (Q_of_Rcst r1) (Q_of_Rcst r2) | CMult r1 r2 => Qmult (Q_of_Rcst r1) (Q_of_Rcst r2) - | CInv r => Qinv (Q_of_Rcst r) + | CPow r1 z => Qpower (Q_of_Rcst r1) (z_of_exp z) + | CInv r => Qinv (Q_of_Rcst r) | COpp r => Qopp (Q_of_Rcst r) end. +Definition is_neg (z: Z+nat) := + match z with + | inl (Zneg _) => true + | _ => false + end. + +Lemma is_neg_true : forall z, is_neg z = true -> (z_of_exp z < 0)%Z. +Proof. + destruct z ; simpl ; try congruence. + destruct z ; try congruence. + intros. + reflexivity. +Qed. + +Lemma is_neg_false : forall z, is_neg z = false -> (z_of_exp z >= 0)%Z. +Proof. + destruct z ; simpl ; try congruence. + destruct z ; try congruence. + compute. congruence. + compute. congruence. + generalize (Zle_0_nat n). auto with zarith. +Qed. + +Definition CInvR0 (r : Rcst) := Qeq_bool (Q_of_Rcst r) (0 # 1). + +Definition CPowR0 (z : Z) (r : Rcst) := + Z.ltb z Z0 && Qeq_bool (Q_of_Rcst r) (0 # 1). + Fixpoint R_of_Rcst (r : Rcst) : R := match r with | C0 => R0 | C1 => R1 | CZ z => IZR z - | CQ q => IQR q + | CQ q => Q2R q | CPlus r1 r2 => (R_of_Rcst r1) + (R_of_Rcst r2) | CMinus r1 r2 => (R_of_Rcst r1) - (R_of_Rcst r2) | CMult r1 r2 => (R_of_Rcst r1) * (R_of_Rcst r2) + | CPow r1 z => + match z with + | inl z => + if CPowR0 z r1 + then R0 + else powerRZ (R_of_Rcst r1) z + | inr n => pow (R_of_Rcst r1) n + end | CInv r => - if Qeq_bool (Q_of_Rcst r) (0 # 1) - then R0 - else Rinv (R_of_Rcst r) - | COpp r => - (R_of_Rcst r) + if CInvR0 r then R0 + else Rinv (R_of_Rcst r) + | COpp r => - (R_of_Rcst r) end. -Lemma Q_of_RcstR : forall c, IQR (Q_of_Rcst c) = R_of_Rcst c. +Add Morphism Q2R with signature Qeq ==> @eq R as Q2R_m. + exact Qeq_eqR. +Qed. + +Lemma Q2R_pow_pos : forall q p, + Q2R (pow_pos Qmult q p) = pow_pos Rmult (Q2R q) p. +Proof. + induction p ; simpl;auto; + rewrite <- IHp; + repeat rewrite Q2R_mult; + reflexivity. +Qed. + +Lemma Q2R_pow_N : forall q n, + Q2R (pow_N 1%Q Qmult q n) = pow_N 1 Rmult (Q2R q) n. +Proof. + destruct n ; simpl. + - apply Q2R_1. + - apply Q2R_pow_pos. +Qed. + +Lemma Qmult_integral : forall q r, q * r == 0 -> q == 0 \/ r == 0. +Proof. + intros. + destruct (Qeq_dec q 0)%Q. + - left ; apply q0. + - apply Qmult_integral_l in H ; tauto. +Qed. + +Lemma Qpower_positive_eq_zero : forall q p, + Qpower_positive q p == 0 -> q == 0. +Proof. + unfold Qpower_positive. + induction p ; simpl; intros; + repeat match goal with + | H : _ * _ == 0 |- _ => + apply Qmult_integral in H; destruct H + end; tauto. +Qed. + +Lemma Qpower_positive_zero : forall p, + Qpower_positive 0 p == 0%Q. +Proof. + induction p ; simpl; + try rewrite IHp ; reflexivity. +Qed. + + +Lemma Q2RpowerRZ : + forall q z + (DEF : not (q == 0)%Q \/ (z >= Z0)%Z), + Q2R (q ^ z) = powerRZ (Q2R q) z. +Proof. + intros. + destruct Qpower_theory. + destruct R_power_theory. + unfold Qpower, powerRZ. + destruct z. + - apply Q2R_1. + - + change (Qpower_positive q p) + with (Qpower q (Zpos p)). + rewrite <- N2Z.inj_pos. + rewrite <- positive_N_nat. + rewrite rpow_pow_N. + rewrite rpow_pow_N0. + apply Q2R_pow_N. + - + rewrite Q2R_inv. + unfold Qpower_positive. + rewrite <- positive_N_nat. + rewrite rpow_pow_N0. + unfold pow_N. + rewrite Q2R_pow_pos. + auto. + intro. + apply Qpower_positive_eq_zero in H. + destruct DEF ; auto with arith. +Qed. + +Lemma Qpower0 : forall z, (z <> 0)%Z -> (0 ^ z == 0)%Q. Proof. - induction c ; simpl ; try (rewrite <- IHc1 ; rewrite <- IHc2). - apply IQR_0. - apply IQR_1. + unfold Qpower. + destruct z;intros. + - congruence. + - apply Qpower_positive_zero. + - rewrite Qpower_positive_zero. reflexivity. - unfold IQR. simpl. rewrite Rinv_1. reflexivity. - apply Q2R_plus. - apply Q2R_minus. - apply Q2R_mult. - rewrite <- IHc. - apply IQR_inv_ext. - rewrite <- IHc. +Qed. + + +Lemma Q_of_RcstR : forall c, Q2R (Q_of_Rcst c) = R_of_Rcst c. +Proof. + induction c ; simpl ; try (rewrite <- IHc1 ; rewrite <- IHc2). + - apply Q2R_0. + - apply Q2R_1. + - reflexivity. + - unfold Q2R. simpl. rewrite Rinv_1. reflexivity. + - apply Q2R_plus. + - apply Q2R_minus. + - apply Q2R_mult. + - destruct z. + destruct (CPowR0 z c) eqn:C; unfold CPowR0 in C. + + + rewrite andb_true_iff in C. + destruct C as (C1 & C2). + rewrite Z.ltb_lt in C1. + apply Qeq_bool_eq in C2. + rewrite C2. + simpl. + rewrite Qpower0 by auto with zarith. + apply Q2R_0. + + rewrite Q2RpowerRZ. + rewrite IHc. + reflexivity. + rewrite andb_false_iff in C. + destruct C. + simpl. apply Z.ltb_ge in H. + auto with zarith. + left ; apply Qeq_bool_neq; auto. + + simpl. + rewrite <- IHc. + destruct Qpower_theory. + rewrite <- nat_N_Z. + rewrite rpow_pow_N. + destruct R_power_theory. + rewrite <- (Nnat.Nat2N.id n) at 2. + rewrite rpow_pow_N0. + apply Q2R_pow_N. + - rewrite <- IHc. + unfold CInvR0. + apply Q2R_inv_ext. + - rewrite <- IHc. apply Q2R_opp. - Qed. +Qed. Require Import EnvRing. @@ -227,7 +389,7 @@ Definition Reval_formula' := eval_sformula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt N.to_nat pow R_of_Rcst. Definition QReval_formula := - eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IQR N.to_nat pow . + eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt Q2R N.to_nat pow . Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f. Proof. @@ -242,12 +404,12 @@ Proof. Qed. Definition Qeval_nformula := - eval_nformula 0 Rplus Rmult (@eq R) Rle Rlt IQR. + eval_nformula 0 Rplus Rmult (@eq R) Rle Rlt Q2R. Lemma Reval_nformula_dec : forall env d, (Qeval_nformula env d) \/ ~ (Qeval_nformula env d). Proof. - exact (fun env d =>eval_nformula_dec Rsor IQR env d). + exact (fun env d =>eval_nformula_dec Rsor Q2R env d). Qed. Definition RWitness := Psatz Q. @@ -279,32 +441,41 @@ Definition rdeduce := nformula_plus_nformula 0%Q Qplus Qeq_bool. Definition RTautoChecker (f : BFormula (Formula Rcst)) (w: list RWitness) : bool := @tauto_checker (Formula Q) (NFormula Q) - runsat rdeduce - Rnormalise Rnegate - RWitness RWeakChecker (map_bformula (map_Formula Q_of_Rcst) f) w. + unit runsat rdeduce + (Rnormalise unit) (Rnegate unit) + RWitness (fun cl => RWeakChecker (List.map fst cl)) (map_bformula (map_Formula Q_of_Rcst) f) w. -Lemma RTautoChecker_sound : forall f w, RTautoChecker f w = true -> forall env, eval_f (Reval_formula env) f. +Lemma RTautoChecker_sound : forall f w, RTautoChecker f w = true -> forall env, eval_bf (Reval_formula env) f. Proof. intros f w. unfold RTautoChecker. intros TC env. - apply (tauto_checker_sound QReval_formula Qeval_nformula) with (env := env) in TC. - rewrite eval_f_map in TC. - rewrite eval_f_morph with (ev':= Reval_formula env) in TC ; auto. + apply tauto_checker_sound with (eval:=QReval_formula) (eval':= Qeval_nformula) (env := env) in TC. + - change (eval_f (fun x : Prop => x) (QReval_formula env)) + with + (eval_bf (QReval_formula env)) in TC. + rewrite eval_bf_map in TC. + unfold eval_bf in TC. + rewrite eval_f_morph with (ev':= Reval_formula env) in TC ; auto. intro. unfold QReval_formula. rewrite <- eval_formulaSC with (phiS := R_of_Rcst). rewrite Reval_formula_compat. tauto. intro. rewrite Q_of_RcstR. reflexivity. + - apply Reval_nformula_dec. - destruct t. + - destruct t. apply (check_inconsistent_sound Rsor QSORaddon) ; auto. - unfold rdeduce. apply (nformula_plus_nformula_correct Rsor QSORaddon). - now apply (cnf_normalise_correct Rsor QSORaddon). - intros. now apply (cnf_negate_correct Rsor QSORaddon). - intros t w0. - apply RWeakChecker_sound. + - unfold rdeduce. apply (nformula_plus_nformula_correct Rsor QSORaddon). + - now apply (cnf_normalise_correct Rsor QSORaddon). + - intros. now eapply (cnf_negate_correct Rsor QSORaddon); eauto. + - intros t w0. + unfold eval_tt. + intros. + rewrite make_impl_map with (eval := Qeval_nformula env0). + eapply RWeakChecker_sound; eauto. + tauto. Qed. diff --git a/plugins/micromega/Refl.v b/plugins/micromega/Refl.v index 952a1b91e7..898a3a1a28 100644 --- a/plugins/micromega/Refl.v +++ b/plugins/micromega/Refl.v @@ -36,6 +36,21 @@ trivial. intro; apply IH. Qed. + +Theorem make_impl_map : + forall (A B: Type) (eval : A -> Prop) (eval' : A*B -> Prop) (l : list (A*B)) r + (EVAL : forall x, eval' x <-> eval (fst x)), + make_impl eval' l r <-> make_impl eval (List.map fst l) r. +Proof. +induction l as [| a l IH]; simpl. +- tauto. +- intros. + rewrite EVAL. + rewrite IH. + tauto. + auto. +Qed. + Fixpoint make_conj (A : Type) (eval : A -> Prop) (l : list A) {struct l} : Prop := match l with | nil => True diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 9504f4edf6..60931df517 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -706,6 +706,8 @@ Definition psub := Psub cO cplus cminus copp ceqb. Definition padd := Padd cO cplus ceqb. +Definition pmul := Pmul cO cI cplus ctimes ceqb. + Definition normalise (f : Formula C) : NFormula := let (lhs, op, rhs) := f in let lhs := norm lhs in @@ -747,6 +749,15 @@ Proof. (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon)). Qed. +Lemma eval_pol_mul : forall env lhs rhs, eval_pol env (pmul lhs rhs) == eval_pol env lhs * eval_pol env rhs. +Proof. + intros. + apply (Pmul_ok sor.(SORsetoid) Rops_wd + (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)). +Qed. + + + Lemma eval_pol_norm : forall env lhs, eval_pexpr env lhs == eval_pol env (norm lhs). Proof. intros. @@ -801,29 +812,29 @@ Definition xnormalise (t:Formula C) : list (NFormula) := Import Coq.micromega.Tauto. -Definition cnf_normalise (t:Formula C) : cnf (NFormula) := - List.map (fun x => x::nil) (xnormalise t). +Definition cnf_normalise {T : Type} (t:Formula C) (tg : T) : cnf NFormula T := + List.map (fun x => (x,tg)::nil) (xnormalise t). Add Ring SORRing : (SORrt sor). -Lemma cnf_normalise_correct : forall env t, eval_cnf eval_nformula env (cnf_normalise t) -> eval_formula env t. +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. - unfold cnf_normalise, xnormalise ; simpl ; intros env t. + unfold cnf_normalise, xnormalise ; simpl ; intros T env t tg. unfold eval_cnf, eval_clause. - destruct t as [lhs o rhs]; case_eq o ; simpl; + 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. + - 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. Qed. Definition xnegate (t:Formula C) : list (NFormula) := @@ -839,30 +850,27 @@ Definition xnegate (t:Formula C) : list (NFormula) := | OpLe => (psub rhs lhs,NonStrict) :: nil end. -Definition cnf_negate (t:Formula C) : cnf (NFormula) := - List.map (fun x => x::nil) (xnegate t). +Definition cnf_negate {T : Type} (t:Formula C) (tg:T) : cnf NFormula T := + List.map (fun x => (x,tg)::nil) (xnegate t). -Lemma cnf_negate_correct : forall env t, eval_cnf eval_nformula env (cnf_negate t) -> ~ 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 env t. + unfold cnf_negate, xnegate ; simpl ; intros T env t tg. unfold eval_cnf, eval_clause. - destruct t as [lhs o rhs]; case_eq o ; simpl; + 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. - (**) + - 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. + - 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. 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 587f2f1fa4..7b9b88c0fe 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -10,7 +10,7 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2006-20011 *) +(* Frédéric Besson (Irisa/Inria) 2006-20019 *) (* *) (************************************************************************) @@ -21,176 +21,363 @@ Require Import Bool. Set Implicit Arguments. +Section S. + Context {TA : Type}. (* type of interpreted atoms *) + Context {TX : Type}. (* type of uninterpreted terms (Prop) *) + Context {AA : Type}. (* type of annotations for atoms *) + Context {AF : Type}. (* type of formulae identifiers *) + #[universes(template)] - Inductive BFormula (A:Type) : Type := - | TT : BFormula A - | FF : BFormula A - | X : Prop -> BFormula A - | A : A -> BFormula A - | Cj : BFormula A -> BFormula A -> BFormula A - | D : BFormula A-> BFormula A -> BFormula A - | N : BFormula A -> BFormula A - | I : BFormula A-> BFormula A-> BFormula A. - - Fixpoint eval_f (A:Type) (ev:A -> Prop ) (f:BFormula A) {struct f}: Prop := - match f with - | TT _ => True - | FF _ => False - | A a => ev a - | X _ p => p - | Cj e1 e2 => (eval_f ev e1) /\ (eval_f ev e2) - | D e1 e2 => (eval_f ev e1) \/ (eval_f ev e2) - | N e => ~ (eval_f ev e) - | I f1 f2 => (eval_f ev f1) -> (eval_f ev f2) - end. + Inductive GFormula : Type := + | TT : GFormula + | FF : GFormula + | X : TX -> GFormula + | A : TA -> AA -> GFormula + | Cj : GFormula -> GFormula -> GFormula + | D : GFormula -> GFormula -> GFormula + | N : GFormula -> GFormula + | I : GFormula -> option AF -> GFormula -> GFormula. + + Section MAPX. + Variable F : TX -> TX. + + Fixpoint mapX (f : GFormula) : GFormula := + match f with + | TT => TT + | FF => FF + | X x => X (F x) + | A a an => A a an + | Cj f1 f2 => Cj (mapX f1) (mapX f2) + | D f1 f2 => D (mapX f1) (mapX f2) + | N f => N (mapX f) + | I f1 o f2 => I (mapX f1) o (mapX f2) + end. - Lemma eval_f_morph : forall A (ev ev' : A -> Prop) (f : BFormula A), - (forall a, ev a <-> ev' a) -> (eval_f ev f <-> eval_f ev' f). - Proof. - induction f ; simpl ; try tauto. - intros. - assert (H' := H a). - auto. - Qed. + End MAPX. + + Section FOLDANNOT. + Variable ACC : Type. + Variable F : ACC -> AA -> ACC. + + Fixpoint foldA (f : GFormula) (acc : ACC) : ACC := + match f with + | TT => acc + | FF => acc + | X x => acc + | A a an => F acc an + | Cj f1 f2 + | D f1 f2 + | I f1 _ f2 => foldA f1 (foldA f2 acc) + | N f => foldA f acc + end. + End FOLDANNOT. - Fixpoint map_bformula (T U : Type) (fct : T -> U) (f : BFormula T) : BFormula U := + Definition cons_id (id : option AF) (l : list AF) := + match id with + | None => l + | Some id => id :: l + end. + + Fixpoint ids_of_formula f := match f with - | TT _ => TT _ - | FF _ => FF _ - | X _ p => X _ p - | A a => A (fct a) - | Cj f1 f2 => Cj (map_bformula fct f1) (map_bformula fct f2) - | D f1 f2 => D (map_bformula fct f1) (map_bformula fct f2) - | N f => N (map_bformula fct f) - | I f1 f2 => I (map_bformula fct f1) (map_bformula fct f2) + | I f id f' => cons_id id (ids_of_formula f') + | _ => nil end. - Lemma eval_f_map : forall T U (fct: T-> U) env f , - eval_f env (map_bformula fct f) = eval_f (fun x => env (fct x)) f. - Proof. - induction f ; simpl ; try (rewrite IHf1 ; rewrite IHf2) ; auto. - rewrite <- IHf. auto. - Qed. + Fixpoint collect_annot (f : GFormula) : list AA := + match f with + | TT | FF | X _ => nil + | A _ a => a ::nil + | Cj f1 f2 + | D f1 f2 + | I f1 _ f2 => collect_annot f1 ++ collect_annot f2 + | N f => collect_annot f + end. + Variable ex : TX -> Prop. (* [ex] will be the identity *) + Section EVAL. - Lemma map_simpl : forall A B f l, @map A B f l = match l with - | nil => nil - | a :: l=> (f a) :: (@map A B f l) - end. + Variable ea : TA -> Prop. + + Fixpoint eval_f (f:GFormula) {struct f}: Prop := + match f with + | TT => True + | FF => False + | A a _ => ea a + | X p => ex p + | Cj e1 e2 => (eval_f e1) /\ (eval_f e2) + | D e1 e2 => (eval_f e1) \/ (eval_f e2) + | N e => ~ (eval_f e) + | I f1 _ f2 => (eval_f f1) -> (eval_f f2) + end. + + + End EVAL. + + + + + + Lemma eval_f_morph : + forall (ev ev' : TA -> Prop) (f : GFormula), + (forall a, ev a <-> ev' a) -> (eval_f ev f <-> eval_f ev' f). Proof. - destruct l ; reflexivity. + induction f ; simpl ; try tauto. + intros. + apply H. Qed. +End S. - Section S. - Variable Env : Type. - Variable Term : Type. - Variable eval : Env -> Term -> Prop. - Variable Term' : Type. - Variable eval' : Env -> Term' -> Prop. +(** Typical boolean formulae *) +Definition BFormula (A : Type) := @GFormula A Prop unit unit. +Section MAPATOMS. + Context {TA TA':Type}. + Context {TX : Type}. + Context {AA : Type}. + Context {AF : Type}. - Variable no_middle_eval' : forall env d, (eval' env d) \/ ~ (eval' env d). +Fixpoint map_bformula (fct : TA -> TA') (f : @GFormula TA TX AA AF ) : @GFormula TA' TX AA AF := + match f with + | TT => TT + | FF => FF + | X p => X p + | A a t => A (fct a) t + | Cj f1 f2 => Cj (map_bformula fct f1) (map_bformula fct f2) + | D f1 f2 => D (map_bformula fct f1) (map_bformula fct f2) + | N f => N (map_bformula fct f) + | I f1 a f2 => I (map_bformula fct f1) a (map_bformula fct f2) + end. - Variable unsat : Term' -> bool. +End MAPATOMS. - Variable unsat_prop : forall t, unsat t = true -> - forall env, eval' env t -> False. +Lemma map_simpl : forall A B f l, @map A B f l = match l with + | nil => nil + | a :: l=> (f a) :: (@map A B f l) + end. +Proof. + destruct l ; reflexivity. +Qed. - Variable deduce : Term' -> Term' -> option Term'. - Variable deduce_prop : forall env t t' u, - eval' env t -> eval' env t' -> deduce t t' = Some u -> eval' env u. +Section S. + (** A cnf tracking annotations of atoms. *) + + (** Type parameters *) + Variable Env : Type. + Variable Term : Type. + Variable Term' : Type. + Variable Annot : Type. + + Variable unsat : Term' -> bool. (* see [unsat_prop] *) + Variable deduce : Term' -> Term' -> option Term'. (* see [deduce_prop] *) - Definition clause := list Term'. - Definition cnf := list clause. + Definition clause := list (Term' * Annot). + Definition cnf := list clause. - Variable normalise : Term -> cnf. - Variable negate : Term -> cnf. + Variable normalise : Term -> Annot -> cnf. + Variable negate : Term -> Annot -> cnf. - Definition tt : cnf := @nil clause. - Definition ff : cnf := cons (@nil Term') nil. + Definition cnf_tt : cnf := @nil clause. + Definition cnf_ff : cnf := cons (@nil (Term' * Annot)) nil. + (** Our cnf is optimised and detects contradictions on the fly. *) - Fixpoint add_term (t: Term') (cl : clause) : option clause := + Fixpoint add_term (t: Term' * Annot) (cl : clause) : option clause := match cl with - | nil => - match deduce t t with - | None => Some (t ::nil) - | Some u => if unsat u then None else Some (t::nil) - end - | t'::cl => - match deduce t t' with - | None => - match add_term t cl with - | None => None - | Some cl' => Some (t' :: cl') - end - | Some u => - if unsat u then None else - match add_term t cl with - | None => None - | Some cl' => Some (t' :: cl') - end + | nil => + match deduce (fst t) (fst t) with + | None => Some (t ::nil) + | Some u => if unsat u then None else Some (t::nil) + end + | t'::cl => + match deduce (fst t) (fst t') with + | None => + match add_term t cl with + | None => None + | Some cl' => Some (t' :: cl') end + | Some u => + if unsat u then None else + match add_term t cl with + | None => None + | Some cl' => Some (t' :: cl') + end + end end. Fixpoint or_clause (cl1 cl2 : clause) : option clause := match cl1 with - | nil => Some cl2 - | t::cl => match add_term t cl2 with - | None => None - | Some cl' => or_clause cl cl' - end + | nil => Some cl2 + | t::cl => match add_term t cl2 with + | None => None + | Some cl' => or_clause cl cl' + 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.map (fun x => (t++x)) f. *) Definition or_clause_cnf (t:clause) (f:cnf) : cnf := - List.fold_right (fun e acc => - match or_clause t e with - | None => acc - | Some cl => cl :: acc - end) nil f. + List.fold_right (fun e acc => + match or_clause t e with + | None => acc + | Some cl => cl :: acc + end) nil f. Fixpoint or_cnf (f : cnf) (f' : cnf) {struct f}: cnf := match f with - | nil => tt - | e :: rst => (or_cnf rst f') ++ (or_clause_cnf e f') + | nil => cnf_tt + | e :: rst => (or_cnf rst f') ++ (or_clause_cnf e f') end. Definition and_cnf (f1 : cnf) (f2 : cnf) : cnf := f1 ++ f2. - Fixpoint xcnf (pol : bool) (f : BFormula Term) {struct f}: cnf := + (** 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. + + Fixpoint xcnf {TX AF: Type} (pol : bool) (f : TFormula TX AF) {struct f}: cnf := match f with - | TT _ => if pol then tt else ff - | FF _ => if pol then ff else tt - | X _ p => if pol then ff else ff (* This is not complete - cannot negate any proposition *) - | A x => if pol then normalise x else negate x - | 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) + | TT => if pol then cnf_tt else cnf_ff + | FF => if pol then cnf_ff else cnf_tt + | X p => if pol then cnf_ff else cnf_ff (* This is not complete - cannot negate any proposition *) + | 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) end. - Definition eval_clause (env : Env) (cl : clause) := ~ make_conj (eval' env) cl. + Section CNFAnnot. + + (** Records annotations used to optimise the cnf. + Those need to be kept when pruning the formula. + 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. *) + match deduce (fst t) (fst t) with + | Some u => if unsat u then inr ((snd t)::nil) else inl (t::nil) + | None => inl (t::nil) + end + | t'::cl => (* if t /\ t' is unsat, the clause is empty BUT t & t' are needed *) + match deduce (fst t) (fst t') with + | Some u => if unsat u then inr ((snd t)::(snd t')::nil) + else match radd_term t cl with + | inl cl' => inl (t'::cl') + | inr l => inr l + end + | None => match radd_term t cl with + | inl cl' => inl (t'::cl') + | inr l => inr l + end + end + end. + + Fixpoint ror_clause cl1 cl2 := + match cl1 with + | nil => inl cl2 + | t::cl => match radd_term t cl2 with + | inl cl' => ror_clause cl cl' + | inr l => inr l + end + end. + + Definition ror_clause_cnf t f := + List.fold_right (fun e '(acc,tg) => + match ror_clause t e with + | inl cl => (cl :: acc,tg) + | inr l => (acc,tg++l) + end) (nil,nil) f . + + + Fixpoint ror_cnf f f' := + 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') + end. + + Fixpoint rxcnf {TX AF: Type}(polarity : bool) (f : TFormula TX AF) := + 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) + | N e => rxcnf (negb polarity) e + | Cj e1 e2 => + 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') + | D e1 e2 => + 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 + if polarity + then let (f',t') := ror_cnf e1 e2 in + (f', t1 ++ t2 ++ t') + else (and_cnf e1 e2, t1 ++ t2) + end. + + End CNFAnnot. + + + + Variable eval : Env -> Term -> Prop. + + Variable eval' : Env -> Term' -> Prop. + + Variable no_middle_eval' : forall env d, (eval' env d) \/ ~ (eval' env d). + + + Variable unsat_prop : forall t, unsat t = true -> + forall env, eval' env t -> False. + + + + Variable deduce_prop : forall env t t' u, + eval' env t -> eval' env t' -> deduce t t' = Some u -> eval' env u. + + + + Definition eval_tt (env : Env) (tt : Term' * Annot) := eval' env (fst tt). + + + Definition eval_clause (env : Env) (cl : clause) := ~ make_conj (eval_tt env) cl. 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. Proof. unfold eval_cnf. @@ -201,97 +388,107 @@ Set Implicit Arguments. Definition eval_opt_clause (env : Env) (cl: option clause) := match cl with - | None => True - | Some cl => eval_clause env cl + | None => True + | Some cl => eval_clause env cl end. - 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 t 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. - (* IC *) - simpl. - case_eq (deduce t 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 *. - 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. - Qed. - - - 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 add_term_correct : forall env t cl , eval_opt_clause env (add_term t cl) -> eval_clause env (t::cl). Proof. induction cl. - simpl. tauto. + - (* 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. + - (* IC *) simpl. - assert (HH := add_term_correct env a cl'). - case_eq (add_term a cl'). - simpl in *. + 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. - apply IHcl in H0. - rewrite H in HH. - simpl in HH. + repeat rewrite make_conj_cons in *. + tauto. + rewrite H0 in IHcl ; simpl in *. unfold eval_clause in *. - destruct H0. + intros. repeat rewrite make_conj_cons in *. tauto. - apply HH in H0. - apply not_make_conj_cons in H0 ; auto. + 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. - intros. - rewrite H in HH. - simpl in HH. + simpl in *. + rewrite H in IHcl. + simpl in IHcl. unfold eval_clause in *. - assert (HH' := HH Coq.Init.Logic.I). - apply not_make_conj_cons in HH'; auto. repeat rewrite make_conj_cons in *. tauto. Qed. - + + + Lemma no_middle_eval_tt : forall env a, + eval_tt env a \/ ~ eval_tt env a. + Proof. + unfold eval_tt. + auto. + Qed. + + 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'. + Proof. + induction cl. + - simpl. tauto. + - intros *. + simpl. + assert (HH := add_term_correct env a cl'). + case_eq (add_term a cl'). + + + intros. + apply IHcl in H0. + rewrite H in HH. + simpl in HH. + unfold eval_clause in *. + destruct H0. + * + repeat rewrite make_conj_cons in *. + tauto. + * apply HH in H0. + apply not_make_conj_cons in H0 ; auto with tauto. + 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). Proof. @@ -299,39 +496,38 @@ Set Implicit Arguments. unfold or_clause_cnf. intros until t. set (F := (fun (e : clause) (acc : list clause) => - match or_clause t e with - | Some cl => cl :: acc - | None => acc - end)). - induction f. - auto. - (**) + 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. + - 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. Qed. - Lemma eval_cnf_cons : forall env a f, (~ make_conj (eval' env) a) -> eval_cnf env f -> eval_cnf env (a::f). - Proof. - intros. - unfold eval_cnf in *. - rewrite make_conj_cons ; eauto. - Qed. + 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. + Qed. Lemma or_cnf_correct : forall env f f', eval_cnf env (or_cnf f f') -> (eval_cnf env f) \/ (eval_cnf env f'). Proof. @@ -352,12 +548,11 @@ Set Implicit Arguments. right ; auto. Qed. - Variable normalise_correct : forall env t, eval_cnf env (normalise t) -> eval env t. - - Variable negate_correct : forall env t, eval_cnf env (negate t) -> ~ eval env t. + 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. - Lemma xcnf_correct : forall f pol env, eval_cnf env (xcnf pol f) -> eval_f (eval env) (if pol then f else N f). + 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 *) @@ -385,10 +580,10 @@ Set Implicit Arguments. simpl. destruct pol ; simpl. intros. - apply normalise_correct ; auto. + eapply normalise_correct ; eauto. (* A 2 *) intros. - apply negate_correct ; auto. + eapply negate_correct ; eauto. auto. (* Cj *) destruct pol ; simpl. @@ -462,21 +657,21 @@ Set Implicit Arguments. Variable Witness : Type. - Variable checker : list Term' -> Witness -> bool. + Variable checker : list (Term'*Annot) -> Witness -> bool. - Variable checker_sound : forall t w, checker t w = true -> forall env, make_impl (eval' env) t False. + Variable checker_sound : forall t w, checker t w = true -> forall env, make_impl (eval_tt env) t False. Fixpoint cnf_checker (f : cnf) (l : list Witness) {struct f}: bool := match f with - | nil => true - | e::f => match l with - | nil => false - | c::l => match checker e c with - | true => cnf_checker f l - | _ => false - end - end - end. + | nil => true + | e::f => match l with + | nil => false + | c::l => match checker e c with + | true => cnf_checker f l + | _ => false + end + end + end. Lemma cnf_checker_sound : forall t w, cnf_checker t w = true -> forall env, eval_cnf env t. Proof. @@ -501,22 +696,32 @@ Set Implicit Arguments. Qed. - Definition tauto_checker (f:BFormula Term) (w:list Witness) : bool := + Definition tauto_checker (f:@GFormula Term Prop Annot unit) (w:list Witness) : bool := cnf_checker (xcnf true f) w. - Lemma tauto_checker_sound : forall t w, tauto_checker t w = true -> forall env, eval_f (eval env) t. + Lemma tauto_checker_sound : forall t w, tauto_checker t w = true -> forall env, eval_f (fun x => x) (eval env) t. Proof. unfold tauto_checker. intros. - change (eval_f (eval env) t) with (eval_f (eval env) (if true then t else TT Term)). + change (eval_f (fun x => x) (eval env) t) with (eval_f (fun x => x) (eval env) (if true then t else TT)). apply (xcnf_correct t true). eapply cnf_checker_sound ; eauto. Qed. + Definition eval_bf {A : Type} (ea : A -> Prop) (f: BFormula A) := eval_f (fun x => x) ea f. + + + Lemma eval_bf_map : forall T U (fct: T-> U) env f , + eval_bf env (map_bformula fct f) = eval_bf (fun x => env (fct x)) f. +Proof. + induction f ; simpl ; try (rewrite IHf1 ; rewrite IHf2) ; auto. + rewrite <- IHf. auto. +Qed. End S. + (* Local Variables: *) (* coding: utf-8 *) (* End: *) diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v index c888f9af45..8148c7033c 100644 --- a/plugins/micromega/VarMap.v +++ b/plugins/micromega/VarMap.v @@ -33,14 +33,14 @@ Section MakeVarMap. #[universes(template)] Inductive t : Type := | Empty : t - | Leaf : A -> t - | Node : t -> A -> t -> t . + | Elt : A -> t + | Branch : t -> A -> t -> t . Fixpoint find (vm : t) (p:positive) {struct vm} : A := match vm with | Empty => default - | Leaf i => i - | Node l e r => match p with + | Elt i => i + | Branch l e r => match p with | xH => e | xO p => find l p | xI p => find r p @@ -50,25 +50,25 @@ Section MakeVarMap. Fixpoint singleton (x:positive) (v : A) : t := match x with - | xH => Leaf v - | xO p => Node (singleton p v) default Empty - | xI p => Node Empty default (singleton p v) + | xH => Elt v + | xO p => Branch (singleton p v) default Empty + | xI p => Branch Empty default (singleton p v) end. Fixpoint vm_add (x: positive) (v : A) (m : t) {struct m} : t := match m with | Empty => singleton x v - | Leaf vl => + | Elt vl => match x with - | xH => Leaf v - | xO p => Node (singleton p v) vl Empty - | xI p => Node Empty vl (singleton p v) + | xH => Elt v + | xO p => Branch (singleton p v) vl Empty + | xI p => Branch Empty vl (singleton p v) end - | Node l o r => + | Branch l o r => match x with - | xH => Node l v r - | xI p => Node l o (vm_add p v r) - | xO p => Node (vm_add p v l) o r + | xH => Branch l v r + | xI p => Branch l o (vm_add p v r) + | xO p => Branch (vm_add p v l) o r end end. diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index f341a04e03..ab218a1778 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -14,13 +14,14 @@ (* *) (************************************************************************) +Require Import List. +Require Import Bool. Require Import OrderedRing. Require Import RingMicromega. +Require FSetPositive FSetEqProperties. Require Import ZCoeff. Require Import Refl. Require Import ZArith. -Require Import List. -Require Import Bool. (*Declare ML Module "micromega_plugin".*) Ltac flatten_bool := @@ -162,6 +163,8 @@ Declare Equivalent Keys psub RingMicromega.psub. Definition padd := padd Z0 Z.add Zeq_bool. Declare Equivalent Keys padd RingMicromega.padd. +Definition pmul := pmul 0 1 Z.add Z.mul Zeq_bool. + Definition normZ := norm 0 1 Z.add Z.mul Z.sub Z.opp Zeq_bool. Declare Equivalent Keys normZ RingMicromega.norm. @@ -180,6 +183,13 @@ Proof. apply (eval_pol_add Zsor ZSORaddon). Qed. +Lemma eval_pol_mul : forall env lhs rhs, eval_pol env (pmul lhs rhs) = eval_pol env lhs * eval_pol env rhs. +Proof. + intros. + apply (eval_pol_mul Zsor ZSORaddon). +Qed. + + Lemma eval_pol_norm : forall env e, eval_expr env e = eval_pol env (normZ e) . Proof. intros. @@ -202,13 +212,13 @@ Definition xnormalise (t:Formula Z) : list (NFormula Z) := Require Import Coq.micromega.Tauto BinNums. -Definition normalise (t:Formula Z) : cnf (NFormula Z) := - List.map (fun x => x::nil) (xnormalise t). +Definition normalise {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T := + List.map (fun x => (x,tg)::nil) (xnormalise t). -Lemma normalise_correct : forall env t, eval_cnf eval_nformula env (normalise t) <-> Zeval_formula env t. +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 env t. + 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]; @@ -236,18 +246,18 @@ Definition xnegate (t:RingMicromega.Formula Z) : list (NFormula Z) := | OpLe => (psub rhs lhs,NonStrict) :: nil end. -Definition negate (t:RingMicromega.Formula Z) : cnf (NFormula Z) := - List.map (fun x => x::nil) (xnegate t). +Definition negate {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T := + List.map (fun x => (x,tg)::nil) (xnegate t). -Lemma negate_correct : forall env t, eval_cnf eval_nformula env (negate t) <-> ~ Zeval_formula env t. +Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env t. Proof. Proof. Opaque padd. - intros env t. + 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; simpl; + 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 *; @@ -264,9 +274,11 @@ Definition Zunsat := check_inconsistent 0 Zeq_bool Z.leb. Definition Zdeduce := nformula_plus_nformula 0 Z.add Zeq_bool. +Definition cnfZ (Annot TX AF : Type) (f : TFormula (Formula Z) Annot TX AF) := + rxcnf Zunsat Zdeduce normalise negate true f. Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z)) : bool := - @tauto_checker (Formula Z) (NFormula Z) Zunsat Zdeduce normalise negate ZWitness ZWeakChecker f w. + @tauto_checker (Formula Z) (NFormula Z) unit Zunsat Zdeduce normalise negate ZWitness (fun cl => ZWeakChecker (List.map fst cl)) f w. (* To get a complete checker, the proof format has to be enriched *) @@ -326,7 +338,9 @@ Inductive ZArithProof := | RatProof : ZWitness -> ZArithProof -> ZArithProof | CutProof : ZWitness -> ZArithProof -> ZArithProof | EnumProof : ZWitness -> ZWitness -> list ZArithProof -> ZArithProof -(*| SplitProof : PolC Z -> ZArithProof -> ZArithProof -> ZArithProof*). +(*| ExProof : positive -> positive -> positive -> ZArithProof ExProof z t x : exists z t, x = z - t /\ z >= 0 /\ t >= 0 *) +. +(*| SplitProof : PolC Z -> ZArithProof -> ZArithProof -> ZArithProof.*) @@ -600,6 +614,186 @@ Definition valid_cut_sign (op:Op1) := | _ => false end. +Module Vars. + Import FSetPositive. + Include PositiveSet. + + Module Facts := FSetEqProperties.EqProperties(PositiveSet). + + Lemma mem_union_l : forall x s s', + mem x s = true -> + mem x (union s s') = true. + Proof. + intros. + rewrite Facts.union_mem. + rewrite H. reflexivity. + Qed. + + Lemma mem_union_r : forall x s s', + mem x s' = true -> + mem x (union s s') = true. + Proof. + intros. + rewrite Facts.union_mem. + rewrite H. rewrite orb_comm. reflexivity. + Qed. + + Lemma mem_singleton : forall p, + mem p (singleton p) = true. + Proof. + apply Facts.singleton_mem_1. + Qed. + + Lemma mem_elements : forall x v, + mem x v = true <-> List.In x (PositiveSet.elements v). + Proof. + intros. + rewrite Facts.MP.FM.elements_b. + rewrite existsb_exists. + unfold Facts.MP.FM.eqb. + split ; intros. + - destruct H as (x' & IN & EQ). + destruct (PositiveSet.E.eq_dec x x') ; try congruence. + subst ; auto. + - exists x. + split ; auto. + destruct (PositiveSet.E.eq_dec x x) ; congruence. + Qed. + + Definition max_element (vars : t) := + fold Pos.max vars xH. + + Lemma max_element_max : + forall x vars, mem x vars = true -> Pos.le x (max_element vars). + Proof. + unfold max_element. + intros. + rewrite mem_elements in H. + rewrite PositiveSet.fold_1. + set (F := (fun (a : positive) (e : PositiveSet.elt) => Pos.max e a)). + revert H. + assert (((x <= 1 -> x <= fold_left F (PositiveSet.elements vars) 1) + /\ + (List.In x (PositiveSet.elements vars) -> + x <= fold_left F (PositiveSet.elements vars) 1))%positive). + { + revert x. + generalize xH as acc. + induction (PositiveSet.elements vars). + - simpl. tauto. + - simpl. + intros. + destruct (IHl (F acc a) x). + split ; intros. + apply H. + unfold F. + rewrite Pos.max_le_iff. + tauto. + destruct H1 ; subst. + apply H. + unfold F. + rewrite Pos.max_le_iff. + simpl. + left. + apply Pos.le_refl. + tauto. + } + tauto. + Qed. + + Definition is_subset (v1 v2 : t) := + forall x, mem x v1 = true -> mem x v2 = true. + + Lemma is_subset_union_l : forall v1 v2, + is_subset v1 (union v1 v2). + Proof. + unfold is_subset. + intros. + apply mem_union_l; auto. + Qed. + + Lemma is_subset_union_r : forall v1 v2, + is_subset v1 (union v2 v1). + Proof. + unfold is_subset. + intros. + apply mem_union_r; auto. + Qed. + + + End Vars. + + +Fixpoint vars_of_pexpr (e : PExpr Z) : Vars.t := + match e with + | PEc _ => Vars.empty + | PEX _ x => Vars.singleton x + | PEadd e1 e2 | PEsub e1 e2 | PEmul e1 e2 => + let v1 := vars_of_pexpr e1 in + let v2 := vars_of_pexpr e2 in + Vars.union v1 v2 + | PEopp c => vars_of_pexpr c + | PEpow e n => vars_of_pexpr e + end. + +Definition vars_of_formula (f : Formula Z) := + match f with + | Build_Formula l o r => + let v1 := vars_of_pexpr l in + let v2 := vars_of_pexpr r in + Vars.union v1 v2 + end. + +Fixpoint vars_of_bformula {TX : Type} {TG : Type} {ID : Type} + (F : @GFormula (Formula Z) TX TG ID) : Vars.t := + match F with + | TT => Vars.empty + | FF => Vars.empty + | X p => Vars.empty + | A a t => vars_of_formula a + | Cj f1 f2 | D f1 f2 | I f1 _ f2 => + let v1 := vars_of_bformula f1 in + let v2 := vars_of_bformula f2 in + Vars.union v1 v2 + | Tauto.N f => vars_of_bformula f + end. + +Definition bound_var (v : positive) : Formula Z := + Build_Formula (PEX _ v) OpGe (PEc 0). + +Definition mk_eq_pos (x : positive) (y:positive) (t : positive) : Formula Z := + Build_Formula (PEX _ x) OpEq (PEsub (PEX _ y) (PEX _ t)). + +Section BOUND. + Context {TX TG ID : Type}. + + Variable tag_of_var : positive -> positive -> option bool -> TG. + + Definition bound_vars (fr : positive) + (v : Vars.t) : @GFormula (Formula Z) TX TG ID := + Vars.fold (fun k acc => + let y := (xO (fr + k)) in + let z := (xI (fr + k)) in + Cj + (Cj (A (mk_eq_pos k y z) (tag_of_var fr k None)) + (Cj (A (bound_var y) (tag_of_var fr k (Some false))) + (A (bound_var z) (tag_of_var fr k (Some true))))) + acc) v TT. + + Definition bound_problem (F : @GFormula (Formula Z) TX TG ID) : GFormula := + let v := vars_of_bformula F in + I (bound_vars (Pos.succ (Vars.max_element v)) v) None F. + + + Definition bound_problem_fr (fr : positive) (F : @GFormula (Formula Z) TX TG ID) : GFormula := + let v := vars_of_bformula F in + I (bound_vars fr v) None F. + + +End BOUND. + + + Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof) {struct pf} : bool := match pf with | DoneProof => false @@ -619,6 +813,10 @@ Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof) {struct pf} : bool : | Some cp => ZChecker (nformula_of_cutting_plane cp::l) pf end end +(* | SplitProof e pf1 pf2 => + match ZChecker ((e,NonStrict)::l) pf1 , ZChecker (( +*) + | EnumProof w1 w2 pf => match eval_Psatz l w1 , eval_Psatz l w2 with | Some f1 , Some f2 => @@ -993,26 +1191,299 @@ Proof. apply genCuttingPlaneNone with (2:= H2) ; auto. Qed. + + Definition ZTautoChecker (f : BFormula (Formula Z)) (w: list ZArithProof): bool := - @tauto_checker (Formula Z) (NFormula Z) Zunsat Zdeduce normalise negate ZArithProof ZChecker f w. + @tauto_checker (Formula Z) (NFormula Z) unit Zunsat Zdeduce normalise negate ZArithProof (fun cl => ZChecker (List.map fst cl)) f w. -Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_f (Zeval_formula env) f. +Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_f (fun x => x) (Zeval_formula env) f. Proof. intros f w. unfold ZTautoChecker. - apply (tauto_checker_sound Zeval_formula eval_nformula). - apply Zeval_nformula_dec. - intros until env. + apply tauto_checker_sound with (eval' := eval_nformula). + - apply Zeval_nformula_dec. + - intros until env. 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). - intros env t. - rewrite normalise_correct ; auto. - intros env t. - rewrite negate_correct ; auto. - intros t w0. - apply ZChecker_sound. + - unfold Zdeduce. apply (nformula_plus_nformula_correct Zsor ZSORaddon). + - + intros env t tg. + rewrite normalise_correct ; auto. + - + intros env t tg. + rewrite negate_correct ; auto. + - intros t w0. + unfold eval_tt. + intros. + rewrite make_impl_map with (eval := eval_nformula env). + eapply ZChecker_sound; eauto. + tauto. +Qed. + +Record is_diff_env_elt (fr : positive) (env env' : positive -> Z) (x:positive):= + { + eq_env : env x = env' x; + eq_diff : env x = env' (xO (fr+ x)) - env' (xI (fr + x)); + pos_xO : env' (xO (fr+x)) >= 0; + pos_xI : env' (xI (fr+x)) >= 0; + }. + + +Definition is_diff_env (s : Vars.t) (env env' : positive -> Z) := + let fr := Pos.succ (Vars.max_element s) in + forall x, Vars.mem x s = true -> + is_diff_env_elt fr env env' x. + +Definition mk_diff_env (s : Vars.t) (env : positive -> Z) := + let fr := Vars.max_element s in + fun x => + if Pos.leb x fr + then env x + else + let fr' := Pos.succ fr in + match x with + | xO x => if Z.leb (env (x - fr')%positive) 0 + then 0 else env (x -fr')%positive + | xI x => if Z.leb (env (x - fr')%positive) 0 + then - (env (x - fr')%positive) else 0 + | xH => 0 + end. + +Lemma le_xO : forall x, (x <= xO x)%positive. +Proof. + intros. + change x with (1 * x)%positive at 1. + change (xO x) with (2 * x)%positive. + apply Pos.mul_le_mono. + compute. congruence. + apply Pos.le_refl. +Qed. + +Lemma leb_xO_false : + (forall x y, x <=? y = false -> + xO x <=? y = false)%positive. +Proof. + intros. + rewrite Pos.leb_nle in *. + intro. apply H. + eapply Pos.le_trans ; eauto. + apply le_xO. +Qed. + +Lemma leb_xI_false : + (forall x y, x <=? y = false -> + xI x <=? y = false)%positive. +Proof. + intros. + rewrite Pos.leb_nle in *. + intro. apply H. + eapply Pos.le_trans ; eauto. + generalize (le_xO x). + intros. + eapply Pos.le_trans ; eauto. + change (xI x) with (Pos.succ (xO x))%positive. + apply Pos.lt_le_incl. + apply Pos.lt_succ_diag_r. +Qed. + +Lemma is_diff_env_ex : forall s env, + is_diff_env s env (mk_diff_env s env). +Proof. + intros. + unfold is_diff_env, mk_diff_env. + intros. + assert + ((Pos.succ (Vars.max_element s) + x <=? Vars.max_element s = false)%positive). + { + rewrite Pos.leb_nle. + intro. + eapply (Pos.lt_irrefl (Pos.succ (Vars.max_element s) + x)). + eapply Pos.le_lt_trans ; eauto. + generalize (Pos.lt_succ_diag_r (Vars.max_element s)). + intro. + eapply Pos.lt_trans ; eauto. + apply Pos.lt_add_r. + } + constructor. + - apply Vars.max_element_max in H. + rewrite <- Pos.leb_le in H. + rewrite H. auto. + - + rewrite leb_xO_false by auto. + rewrite leb_xI_false by auto. + rewrite Pos.add_comm. + rewrite Pos.add_sub. + destruct (env x <=? 0); ring. + - rewrite leb_xO_false by auto. + rewrite Pos.add_comm. + rewrite Pos.add_sub. + destruct (env x <=? 0) eqn:EQ. + apply Z.le_ge. + apply Z.le_refl. + rewrite Z.leb_gt in EQ. + apply Z.le_ge. + apply Z.lt_le_incl. + auto. + - rewrite leb_xI_false by auto. + rewrite Pos.add_comm. + rewrite Pos.add_sub. + destruct (env x <=? 0) eqn:EQ. + rewrite Z.leb_le in EQ. + apply Z.le_ge. + apply Z.opp_nonneg_nonpos; auto. + apply Z.le_ge. + apply Z.le_refl. +Qed. + +Lemma env_bounds : forall tg env s, + let fr := Pos.succ (Vars.max_element s) in + exists env', is_diff_env s env env' + /\ + eval_bf (Zeval_formula env') (bound_vars tg fr s). +Proof. + intros. + assert (DIFF:=is_diff_env_ex s env). + exists (mk_diff_env s env). split ; auto. + unfold bound_vars. + rewrite FSetPositive.PositiveSet.fold_1. + revert DIFF. + set (env' := mk_diff_env s env). + intro. + assert (ACC : eval_bf (Zeval_formula env') TT ). + { + simpl. auto. + } + revert ACC. + match goal with + | |- context[@TT ?A ?B ?C ?D] => generalize (@TT A B C D) as acc + end. + unfold is_diff_env in DIFF. + assert (DIFFL : forall x, In x (FSetPositive.PositiveSet.elements s) -> + (x < fr)%positive /\ + is_diff_env_elt fr env env' x). + { + intros. + rewrite <- Vars.mem_elements in H. + split. + apply Vars.max_element_max in H. + unfold fr in *. + eapply Pos.le_lt_trans ; eauto. + apply Pos.lt_succ_diag_r. + apply DIFF; auto. + } + clear DIFF. + match goal with + | |- context[fold_left ?F _ _] => + set (FUN := F) + end. + induction (FSetPositive.PositiveSet.elements s). + - simpl; auto. + - simpl. + intros. + eapply IHl ; eauto. + + intros. apply DIFFL. + simpl ; auto. + + unfold FUN. + simpl. + split ; auto. + assert (HYP : (a < fr /\ is_diff_env_elt fr env env' a)%positive). + { + apply DIFFL. + simpl. tauto. + } + destruct HYP as (LT & DIFF). + destruct DIFF. + rewrite <- eq_env0. + tauto. +Qed. + +Definition agree_env (v : Vars.t) (env env' : positive -> Z) : Prop := + forall x, Vars.mem x v = true -> env x = env' x. + +Lemma agree_env_subset : forall s1 s2 env env', + agree_env s1 env env' -> + Vars.is_subset s2 s1 -> + agree_env s2 env env'. +Proof. + unfold agree_env. + intros. + apply H. apply H0; auto. +Qed. + +Lemma agree_env_union : forall s1 s2 env env', + agree_env (Vars.union s1 s2) env env' -> + agree_env s1 env env' /\ agree_env s2 env env'. +Proof. + split; + eapply agree_env_subset; eauto. + apply Vars.is_subset_union_l. + apply Vars.is_subset_union_r. +Qed. + + + +Lemma agree_env_eval_expr : + forall env env' e + (AGREE : agree_env (vars_of_pexpr e) env env'), + Zeval_expr env e = Zeval_expr env' e. +Proof. + induction e; simpl;intros; + try (apply agree_env_union in AGREE; destruct AGREE); try f_equal ; auto. + - intros ; apply AGREE. + apply Vars.mem_singleton. +Qed. + +Lemma agree_env_eval_bf : + forall env env' f + (AGREE: agree_env (vars_of_bformula f) env env'), + eval_bf (Zeval_formula env') f <-> + eval_bf (Zeval_formula env) f. +Proof. + induction f; simpl; intros ; + try (apply agree_env_union in AGREE; destruct AGREE) ; try intuition fail. + - + unfold Zeval_formula. + destruct t. + simpl in * ; intros. + apply agree_env_union in AGREE ; destruct AGREE. + rewrite <- agree_env_eval_expr with (env:=env) by auto. + rewrite <- agree_env_eval_expr with (e:= Frhs) (env:=env) by auto. + tauto. +Qed. + +Lemma bound_problem_sound : forall tg f, + (forall env' : PolEnv Z, + eval_bf (Zeval_formula env') + (bound_problem tg f)) -> + forall env, + eval_bf (Zeval_formula env) f. +Proof. + intros. + unfold bound_problem in H. + destruct (env_bounds tg env (vars_of_bformula f)) + as (env' & DIFF & EVAL). + simpl in H. + apply H in EVAL. + eapply agree_env_eval_bf ; eauto. + unfold is_diff_env, agree_env in *. + intros. + apply DIFF in H0. + destruct H0. + intuition. +Qed. + + + +Definition ZTautoCheckerExt (f : BFormula (Formula Z)) (w : list ZArithProof) : bool := + ZTautoChecker (bound_problem (fun _ _ _ => tt) f) w. + +Lemma ZTautoCheckerExt_sound : forall f w, ZTautoCheckerExt f w = true -> forall env, eval_bf (Zeval_formula env) f. +Proof. + intros. + unfold ZTautoCheckerExt in H. + specialize (ZTautoChecker_sound _ _ H). + intros ; apply bound_problem_sound with (tg:= fun _ _ _ => tt); auto. Qed. Fixpoint xhyps_of_pt (base:nat) (acc : list nat) (pt:ZArithProof) : list nat := @@ -1028,18 +1499,10 @@ 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. -(*Lemma hyps_of_pt_correct : forall pt l, *) - - - - - - Open Scope Z_scope. (** To ease bindings from ml code **) -(*Definition varmap := Quote.varmap.*) Definition make_impl := Refl.make_impl. Definition make_conj := Refl.make_conj. @@ -1047,9 +1510,9 @@ Require VarMap. (*Definition varmap_type := VarMap.t Z. *) Definition env := PolEnv Z. -Definition node := @VarMap.Node Z. +Definition node := @VarMap.Branch Z. Definition empty := @VarMap.Empty Z. -Definition leaf := @VarMap.Leaf Z. +Definition leaf := @VarMap.Elt Z. Definition coneMember := ZWitness. diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index af292c088f..3f9f4726e7 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -19,7 +19,6 @@ let debug = false -open Util open Big_int open Num open Polynomial @@ -31,6 +30,16 @@ module C2Ml = Mutils.CoqToCaml let use_simplex = ref true +type ('prf,'model) res = + | Prf of 'prf + | Model of 'model + | Unknown + +type zres = (Mc.zArithProof , (int * Mc.z list)) res + +type qres = (Mc.q Mc.psatz , (int * Mc.q list)) res + + open Mutils type 'a number_spec = { bigint_to_number : big_int -> 'a; @@ -181,7 +190,7 @@ let build_dual_linear_system l = {coeffs = Vect.from_list ([Big_int zero_big_int ;Big_int unit_big_int]) ; op = Ge ; cst = Big_int zero_big_int}::(strict::(positivity l)@c::s0) - +open Util (** [direct_linear_prover l] does not handle strict inegalities *) let fourier_linear_prover l = @@ -201,11 +210,11 @@ let direct_linear_prover l = else fourier_linear_prover l let find_point l = - if !use_simplex - then Simplex.find_point l - else match Mfourier.Fourier.find_point l with - | Inr _ -> None - | Inl cert -> Some cert + if !use_simplex + then Simplex.find_point l + else match Mfourier.Fourier.find_point l with + | Inr _ -> None + | Inl cert -> Some cert let optimise v l = if !use_simplex @@ -253,9 +262,6 @@ let simple_linear_prover l = (* Fourier elimination should handle > *) dual_raw_certificate l -open ProofFormat - - let env_of_list l = snd (List.fold_left (fun (i,m) p -> (i+1,IMap.add i p m)) (0,IMap.empty) l) @@ -268,7 +274,7 @@ let linear_prover_cstr sys = match simple_linear_prover sysi with | None -> None - | Some cert -> Some (proof_of_farkas (env_of_list prfi) cert) + | Some cert -> Some (ProofFormat.proof_of_farkas (env_of_list prfi) cert) let linear_prover_cstr = if debug @@ -301,15 +307,14 @@ let develop_constraint z_spec (e,k) = - 0 = c for c a non-zero constant - e = c when the coeffs of e are all integers and c is rational *) -open ProofFormat type checksat = | Tauto (* Tautology *) - | Unsat of prf_rule (* Unsatisfiable *) - | Cut of cstr * prf_rule (* Cutting plane *) - | Normalise of cstr * prf_rule (* Coefficients may be normalised i.e relatively prime *) + | Unsat of ProofFormat.prf_rule (* Unsatisfiable *) + | Cut of cstr * ProofFormat.prf_rule (* Cutting plane *) + | Normalise of cstr * ProofFormat.prf_rule (* Coefficients may be normalised i.e relatively prime *) -exception FoundProof of prf_rule +exception FoundProof of ProofFormat.prf_rule (** [check_sat] @@ -336,17 +341,17 @@ let check_int_sat (cstr,prf) = coeffs = Vect.div gcd coeffs; op = op ; cst = cst // gcd } in - Normalise(cstr,Gcd(gcdi,prf)) + Normalise(cstr,ProofFormat.Gcd(gcdi,prf)) (* Normalise(cstr,CutPrf prf)*) end else match op with - | Eq -> Unsat (CutPrf prf) + | Eq -> Unsat (ProofFormat.CutPrf prf) | Ge -> let cstr = { coeffs = Vect.div gcd coeffs; op = op ; cst = ceiling_num (cst // gcd) - } in Cut(cstr,CutPrf prf) + } in Cut(cstr,ProofFormat.CutPrf prf) | Gt -> failwith "check_sat : Unexpected operator" @@ -363,29 +368,6 @@ let apply_and_normalise check f psys = ) [] psys -let simplify f sys = - let (sys',b) = - List.fold_left (fun (sys',b) c -> - match f c with - | None -> (c::sys',b) - | Some c' -> - (c'::sys',true) - ) ([],false) sys in - if b then Some sys' else None - -let saturate f sys = - List.fold_left (fun sys' c -> match f c with - | None -> sys' - | Some c' -> c'::sys' - ) [] sys - -let is_substitution strict ((p,o),prf) = - let pred v = if strict then v =/ Int 1 || v =/ Int (-1) else true in - - match o with - | Eq -> LinPoly.search_linear pred p - | _ -> None - let is_linear_for v pc = LinPoly.is_linear (fst (fst pc)) || LinPoly.is_linear_for v (fst (fst pc)) @@ -393,11 +375,11 @@ let is_linear_for v pc = -let non_linear_pivot sys pc v pc' = +(*let non_linear_pivot sys pc v pc' = if LinPoly.is_linear (fst (fst pc')) then None (* There are other ways to deal with those *) else WithProof.linear_pivot sys pc v pc' - + *) let is_linear_substitution sys ((p,o),prf) = let pred v = v =/ Int 1 || v =/ Int (-1) in @@ -423,7 +405,33 @@ let elim_simple_linear_equality sys0 = iterate_until_stable elim sys0 -let saturate_linear_equality_non_linear sys0 = + +let output_sys o sys = + List.iter (fun s -> Printf.fprintf o "%a\n" WithProof.output s) sys + +let subst sys = + let sys' = WithProof.subst sys in + if debug then Printf.fprintf stdout "[subst:\n%a\n==>\n%a\n]" output_sys sys output_sys sys' ; + sys' + + + +(** [saturate_linear_equality sys] generate new constraints + obtained by eliminating linear equalities by pivoting. + For integers, the obtained constraints are sound but not complete. + *) + let saturate_by_linear_equalities sys0 = + WithProof.saturate_subst false sys0 + + +let saturate_by_linear_equalities sys = + let sys' = saturate_by_linear_equalities sys in + if debug then Printf.fprintf stdout "[saturate_by_linear_equalities:\n%a\n==>\n%a\n]" output_sys sys output_sys sys' ; + sys' + + + +(* let saturate_linear_equality_non_linear sys0 = let (l,_) = extract_all (is_substitution false) sys0 in let rec elim l acc = match l with @@ -432,18 +440,51 @@ let saturate_linear_equality_non_linear sys0 = let nc = saturate (non_linear_pivot sys0 pc v) (sys0@acc) in elim l' (nc@acc) in elim l [] + *) +let bounded_vars (sys: WithProof.t list) = + let l = (fst (extract_all (fun ((p,o),prf) -> + LinPoly.is_variable p + ) sys)) in + List.fold_left (fun acc (i,wp) -> IMap.add i wp acc) IMap.empty l + +let rec power n p = + if n = 1 then p + else WithProof.product p (power (n-1) p) + +let bound_monomial mp m = + if Monomial.is_var m || Monomial.is_const m + then None + else + try + Some (Monomial.fold + (fun v i acc -> + let wp = IMap.find v mp in + WithProof.product (power i wp) acc) m (WithProof.const (Int 1)) + ) + with Not_found -> None + + +let bound_monomials (sys:WithProof.t list) = + let mp = bounded_vars sys in + let m = + List.fold_left (fun acc ((p,_),_) -> + Vect.fold (fun acc v _ -> let m = LinPoly.MonT.retrieve v in + match bound_monomial mp m with + | None -> acc + | Some r -> IMap.add v r acc) acc p) IMap.empty sys in + IMap.fold (fun _ e acc -> e::acc) m [] let develop_constraints prfdepth n_spec sys = LinPoly.MonT.clear (); max_nb_cstr := compute_max_nb_cstr sys prfdepth ; let sys = List.map (develop_constraint n_spec) sys in - List.mapi (fun i (p,o) -> ((LinPoly.linpol_of_pol p,o),Hyp i)) sys + List.mapi (fun i (p,o) -> ((LinPoly.linpol_of_pol p,o),ProofFormat.Hyp i)) sys let square_of_var i = let x = LinPoly.var i in - ((LinPoly.product x x,Ge),(Square x)) + ((LinPoly.product x x,Ge),(ProofFormat.Square x)) (** [nlinear_preprocess sys] augments the system [sys] by performing some limited non-linear reasoning. @@ -462,7 +503,7 @@ let nlinear_preprocess (sys:WithProof.t list) = let sys = MonMap.fold (fun s m acc -> let s = LinPoly.of_monomial s in let m = LinPoly.of_monomial m in - ((m, Ge), (Square s))::acc) collect_square sys in + ((m, Ge), (ProofFormat.Square s))::acc) collect_square sys in let collect_vars = List.fold_left (fun acc p -> ISet.union acc (LinPoly.variables (fst (fst p)))) ISet.empty sys in @@ -482,16 +523,16 @@ let nlinear_preprocess (sys:WithProof.t list) = let nlinear_prover prfdepth sys = let sys = develop_constraints prfdepth q_spec sys in let sys1 = elim_simple_linear_equality sys in - let sys2 = saturate_linear_equality_non_linear sys1 in + let sys2 = saturate_by_linear_equalities sys1 in let sys = nlinear_preprocess sys1@sys2 in let sys = List.map (fun ((p,o),prf) -> (cstr_of_poly (p,o), prf)) sys in let id = (List.fold_left (fun acc (_,r) -> max acc (ProofFormat.pr_rule_max_id r)) 0 sys) in let env = CList.interval 0 id in match linear_prover_cstr sys with - | None -> None + | None -> Unknown | Some cert -> - Some (cmpl_prf_rule Mc.normQ CamlToCoq.q env cert) + Prf (ProofFormat.cmpl_prf_rule Mc.normQ CamlToCoq.q env cert) let linear_prover_with_cert prfdepth sys = @@ -500,9 +541,9 @@ let linear_prover_with_cert prfdepth sys = let sys = List.map (fun (c,p) -> cstr_of_poly c,p) sys in match linear_prover_cstr sys with - | None -> None + | None -> Unknown | Some cert -> - Some (cmpl_prf_rule Mc.normQ CamlToCoq.q (List.mapi (fun i e -> i) sys) cert) + Prf (ProofFormat.cmpl_prf_rule Mc.normQ CamlToCoq.q (List.mapi (fun i e -> i) sys) cert) (* The prover is (probably) incomplete -- only searching for naive cutting planes *) @@ -643,7 +684,7 @@ open Polynomial -type prf_sys = (cstr * prf_rule) list +type prf_sys = (cstr * ProofFormat.prf_rule) list @@ -661,7 +702,7 @@ let pivot v (c1,p1) (c2,p2) = op = opAdd op1 op2 ; cst = n1 */ cv1 +/ n2 */ cv2 }, - AddPrf(mul_cst_proof cv1 p1,mul_cst_proof cv2 p2)) in + ProofFormat.add_proof (ProofFormat.mul_cst_proof cv1 p1) (ProofFormat.mul_cst_proof cv2 p2)) in match Vect.get v v1 , Vect.get v v2 with | Int 0 , _ | _ , Int 0 -> None @@ -747,7 +788,7 @@ let reduce_coprime psys = op = Eq ; cst = (l1' */ c1.cst) +/ (l2' */ c2.cst) } in - let prf = add_proof (mul_cst_proof l1' p1) (mul_cst_proof l2' p2) in + let prf = ProofFormat.add_proof (ProofFormat.mul_cst_proof l1' p1) (ProofFormat.mul_cst_proof l2' p2) in Some (pivot_sys v (cstr,prf) ((c1,p1)::sys)) @@ -798,7 +839,7 @@ let reduce_var_change psys = let m = minus_num (vx */ l1 +/ vx' */ l2) in Some ({coeffs = Vect.add (Vect.mul m c.coeffs) coeffs ; op = op ; cst = m */ c.cst +/ cst} , - AddPrf(MulC((LinPoly.constant m),p),p')) in + ProofFormat.add_proof (ProofFormat.mul_cst_proof m p) p') in Some (apply_and_normalise check_int_sat pivot_eq sys) @@ -871,40 +912,42 @@ let get_bound sys = let check_sys sys = List.for_all (fun (c,p) -> Vect.for_all (fun _ n -> sign_num n <> 0) c.coeffs) sys +open ProofFormat let xlia (can_enum:bool) reduction_equations sys = - let rec enum_proof (id:int) (sys:prf_sys) : ProofFormat.proof option = + let rec enum_proof (id:int) (sys:prf_sys) = if debug then (Printf.printf "enum_proof\n" ; flush stdout) ; assert (check_sys sys) ; let nsys,prf = List.split sys in match get_bound nsys with - | None -> None (* Is the systeme really unbounded ? *) + | None -> Unknown (* Is the systeme really unbounded ? *) | Some(prf1,(lb,e,ub),prf2) -> if debug then Printf.printf "Found interval: %a in [%s;%s] -> " Vect.pp e (string_of_num lb) (string_of_num ub) ; (match start_enum id e (ceiling_num lb) (floor_num ub) sys with - | Some prfl -> - Some(Enum(id,proof_of_farkas (env_of_list prf) (Vect.from_list prf1),e, - proof_of_farkas (env_of_list prf) (Vect.from_list prf2),prfl)) - | None -> None + | Prf prfl -> + Prf(ProofFormat.Enum(id,ProofFormat.proof_of_farkas (env_of_list prf) (Vect.from_list prf1),e, + ProofFormat.proof_of_farkas (env_of_list prf) (Vect.from_list prf2),prfl)) + | _ -> Unknown ) - and start_enum id e clb cub sys = + and start_enum id e clb cub sys = if clb >/ cub - then Some [] + then Prf [] else let eq = {coeffs = e ; op = Eq ; cst = clb} in - match aux_lia (id+1) ((eq, Def id) :: sys) with - | None -> None - | Some prf -> + match aux_lia (id+1) ((eq, ProofFormat.Def id) :: sys) with + | Unknown | Model _ -> Unknown + | Prf prf -> match start_enum id e (clb +/ (Int 1)) cub sys with - | None -> None - | Some l -> Some (prf::l) + | Prf l -> Prf (prf::l) + | _ -> Unknown - and aux_lia (id:int) (sys:prf_sys) : ProofFormat.proof option = + + and aux_lia (id:int) (sys:prf_sys) = assert (check_sys sys) ; if debug then Printf.printf "xlia: %a \n" (pp_list ";" (fun o (c,_) -> output_cstr o c)) sys ; try @@ -912,11 +955,11 @@ let xlia (can_enum:bool) reduction_equations sys = if debug then Printf.printf "after reduction: %a \n" (pp_list ";" (fun o (c,_) -> output_cstr o c)) sys ; match linear_prover_cstr sys with - | Some prf -> Some (Step(id,prf,Done)) - | None -> if can_enum then enum_proof id sys else None + | Some prf -> Prf (Step(id,prf,Done)) + | None -> if can_enum then enum_proof id sys else Unknown with FoundProof prf -> (* [reduction_equations] can find a proof *) - Some(Step(id,prf,Done)) in + Prf(Step(id,prf,Done)) in (* let sys' = List.map (fun (p,o) -> Mc.norm0 p , o) sys in*) let id = 1 + (List.fold_left @@ -925,10 +968,10 @@ let xlia (can_enum:bool) reduction_equations sys = try let sys = simpl_sys sys in aux_lia id sys - with FoundProof pr -> Some(Step(id,pr,Done)) in + with FoundProof pr -> Prf(Step(id,pr,Done)) in match orpf with - | None -> None - | Some prf -> + | Unknown | Model _ -> Unknown + | Prf prf -> let env = CList.interval 0 (id - 1) in if debug then begin Printf.fprintf stdout "direct proof %a\n" output_proof prf; @@ -939,21 +982,25 @@ let xlia (can_enum:bool) reduction_equations sys = if Mc.zChecker sys' prf then Some prf else raise Certificate.BadCertificate with Failure s -> (Printf.printf "%s" s ; Some prf) - *) Some prf + *) Prf prf -let xlia_simplex env sys = - match Simplex.integer_solver sys with - | None -> None - | Some prf -> - (*let _ = ProofFormat.eval_proof (env_of_list env) prf in *) +let xlia_simplex env red sys = + let compile_prf sys prf = + let id = 1 + (List.fold_left + (fun acc (_,r) -> max acc (ProofFormat.pr_rule_max_id r)) 0 sys) in + let env = CList.interval 0 (id - 1) in + Prf (compile_proof env prf) in - let id = 1 + (List.fold_left - (fun acc (_,r) -> max acc (ProofFormat.pr_rule_max_id r)) 0 sys) in - let env = CList.interval 0 (id - 1) in - Some (compile_proof env prf) + try + let sys = red sys in + + match Simplex.integer_solver sys with + | None -> Unknown + | Some prf -> compile_prf sys prf + with FoundProof prf -> compile_prf sys (Step(0,prf,Done)) let xlia env0 en red sys = - if !use_simplex then xlia_simplex env0 sys + if !use_simplex then xlia_simplex env0 red sys else xlia en red sys @@ -971,9 +1018,9 @@ let gen_bench (tac, prover) can_enum prfdepth sys = Printf.fprintf o "Goal %a.\n" (LinPoly.pp_goal "Z") (List.map fst sys) ; begin match res with - | None -> + | Unknown | Model _ -> Printf.fprintf o "Proof.\n intros. Fail %s.\nAbort.\n" tac - | Some res -> + | Prf res -> Printf.fprintf o "Proof.\n intros. %s.\nQed.\n" tac end ; @@ -987,7 +1034,14 @@ let lia (can_enum:bool) (prfdepth:int) sys = if debug then begin Printf.fprintf stdout "Input problem\n"; List.iter (fun s -> Printf.fprintf stdout "%a\n" WithProof.output s) sys; + Printf.fprintf stdout "Input problem\n"; + let string_of_op = function Eq -> "=" | Ge -> ">=" | Gt -> ">" in + List.iter (fun ((p,op),_) -> Printf.fprintf stdout "(assert (%s %a))\n" (string_of_op op) Vect.pp_smt p) sys; end; + let sys = subst sys in + let bnd = bound_monomials sys in (* To deal with non-linear monomials *) + let sys = bnd@(saturate_by_linear_equalities sys)@sys in + let sys' = List.map (fun ((p,o),prf) -> (cstr_of_poly (p,o), prf)) sys in xlia (List.map fst sys) can_enum reduction_equations sys' @@ -1013,7 +1067,7 @@ let nlia enum prfdepth sys = It would only be safe if the variable is linear... *) let sys1 = elim_simple_linear_equality sys in - let sys2 = saturate_linear_equality_non_linear sys1 in + let sys2 = saturate_by_linear_equalities sys1 in let sys3 = nlinear_preprocess (sys1@sys2) in let sys4 = make_cstr_system ((*sys2@*)sys3) in diff --git a/plugins/micromega/certificate.mli b/plugins/micromega/certificate.mli index e925f1bc5e..3428428441 100644 --- a/plugins/micromega/certificate.mli +++ b/plugins/micromega/certificate.mli @@ -15,6 +15,15 @@ module Mc = Micromega If set, use the Simplex method, otherwise use Fourier *) val use_simplex : bool ref +type ('prf,'model) res = + | Prf of 'prf + | Model of 'model + | Unknown + +type zres = (Mc.zArithProof , (int * Mc.z list)) res + +type qres = (Mc.q Mc.psatz , (int * Mc.q list)) res + (** [dump_file] is bound to the Coq option Dump Arith. If set to some [file], arithmetic goals are dumped in filexxx.v *) val dump_file : string option ref @@ -27,16 +36,16 @@ val z_cert_of_pos : Sos_types.positivstellensatz -> Mc.z Mc.psatz (** [lia enum depth sys] generates an unsat proof for the linear constraints in [sys]. If the Simplex option is set, any failure to find a proof should be considered as a bug. *) -val lia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> Mc.zArithProof option +val lia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres (** [nlia enum depth sys] generates an unsat proof for the non-linear constraints in [sys]. The solver is incomplete -- the problem is undecidable *) -val nlia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> Mc.zArithProof option +val nlia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres (** [linear_prover_with_cert depth sys] generates an unsat proof for the linear constraints in [sys]. Over the rationals, the solver is complete. *) -val linear_prover_with_cert : int -> (Mc.q Mc.pExpr * Mc.op1) list -> Mc.q Micromega.psatz option +val linear_prover_with_cert : int -> (Mc.q Mc.pExpr * Mc.op1) list -> qres (** [nlinear depth sys] generates an unsat proof for the non-linear constraints in [sys]. The solver is incompete -- the problem is decidable. *) -val nlinear_prover : int -> (Mc.q Mc.pExpr * Mc.op1) list -> Mc.q Mc.psatz option +val nlinear_prover : int -> (Mc.q Mc.pExpr * Mc.op1) list -> qres diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 6c04fe9a8a..ef6af16036 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -14,7 +14,7 @@ (* *) (* - Modules M, Mc, Env, Cache, CacheZ *) (* *) -(* Frédéric Besson (Irisa/Inria) 2006-20011 *) +(* Frédéric Besson (Irisa/Inria) 2006-2019 *) (* *) (************************************************************************) @@ -103,6 +103,7 @@ let () = *) type tag = Tag.t +module Mc = Micromega (** * An atom is of the form: @@ -111,205 +112,30 @@ type tag = Tag.t * parametrized by 'cst, which is used as the type of constants. *) -type 'cst atom = 'cst Micromega.formula +type 'cst atom = 'cst Mc.formula -(** - * Micromega's encoding of formulas. - * By order of appearance: boolean constants, variables, atoms, conjunctions, - * disjunctions, negation, implication. -*) - -type 'cst formula = - | TT - | FF - | X of EConstr.constr - | A of 'cst atom * tag * EConstr.constr - | C of 'cst formula * 'cst formula - | D of 'cst formula * 'cst formula - | N of 'cst formula - | I of 'cst formula * Names.Id.t option * 'cst formula +type 'cst formula = ('cst atom, EConstr.constr,tag * EConstr.constr,Names.Id.t) Mc.gFormula -(** - * Formula pretty-printer. - *) +type 'cst clause = ('cst Mc.nFormula, tag * EConstr.constr) Mc.clause +type 'cst cnf = ('cst Mc.nFormula, tag * EConstr.constr) Mc.cnf -let rec pp_formula o f = + +let rec pp_formula o (f:'cst formula) = + Mc.( match f with | TT -> output_string o "tt" | FF -> output_string o "ff" | X c -> output_string o "X " - | A(_,t,_) -> Printf.fprintf o "A(%a)" Tag.pp t - | C(f1,f2) -> Printf.fprintf o "C(%a,%a)" pp_formula f1 pp_formula f2 + | A(_,(t,_)) -> Printf.fprintf o "A(%a)" Tag.pp t + | Cj(f1,f2) -> Printf.fprintf o "C(%a,%a)" pp_formula f1 pp_formula f2 | D(f1,f2) -> Printf.fprintf o "D(%a,%a)" pp_formula f1 pp_formula f2 - | I(f1,n,f2) -> Printf.fprintf o "I(%a%s,%a)" - pp_formula f1 - (match n with - | Some id -> Names.Id.to_string id - | None -> "") pp_formula f2 + | I(f1,n,f2) -> Printf.fprintf o "I(%a,%s,%a)" + pp_formula f1 + (match n with + | Some id -> Names.Id.to_string id + | None -> "") pp_formula f2 | N(f) -> Printf.fprintf o "N(%a)" pp_formula f - - -let rec map_atoms fct f = - match f with - | TT -> TT - | FF -> FF - | X x -> X x - | A (at,tg,cstr) -> A(fct at,tg,cstr) - | C (f1,f2) -> C(map_atoms fct f1, map_atoms fct f2) - | D (f1,f2) -> D(map_atoms fct f1, map_atoms fct f2) - | N f -> N(map_atoms fct f) - | I(f1,o,f2) -> I(map_atoms fct f1, o , map_atoms fct f2) - -let rec map_prop fct f = - match f with - | TT -> TT - | FF -> FF - | X x -> X (fct x) - | A (at,tg,cstr) -> A(at,tg,cstr) - | C (f1,f2) -> C(map_prop fct f1, map_prop fct f2) - | D (f1,f2) -> D(map_prop fct f1, map_prop fct f2) - | N f -> N(map_prop fct f) - | I(f1,o,f2) -> I(map_prop fct f1, o , map_prop fct f2) - -(** - * Collect the identifiers of a (string of) implications. Implication labels - * are inherited from Coq/CoC's higher order dependent type constructor (Pi). - *) - -let rec ids_of_formula f = - match f with - | I(f1,Some id,f2) -> id::(ids_of_formula f2) - | _ -> [] - -(** - * A clause is a list of (tagged) nFormulas. - * nFormulas are normalized formulas, i.e., of the form: - * cPol \{=,<>,>,>=\} 0 - * with cPol compact polynomials (see the Pol inductive type in EnvRing.v). - *) - -type 'cst clause = ('cst Micromega.nFormula * tag) list - -(** - * A CNF is a list of clauses. - *) - -type 'cst cnf = ('cst clause) list - -(** - * True and False are empty cnfs and clauses. - *) - -let tt : 'cst cnf = [] - -let ff : 'cst cnf = [ [] ] - -(** - * A refinement of cnf with tags left out. This is an intermediary form - * between the cnf tagged list representation ('cst cnf) used to solve psatz, - * and the freeform formulas ('cst formula) that is retrieved from Coq. - *) - -module Mc = Micromega - -type 'cst mc_cnf = ('cst Mc.nFormula) list list - -(** - * From a freeform formula, build a cnf. - * The parametric functions negate and normalize are theory-dependent, and - * originate in micromega.ml (extracted, e.g. for rnegate, from RMicromega.v - * and RingMicromega.v). - *) - -type 'a tagged_option = T of tag list | S of 'a - -let cnf - (negate: 'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf) - (unsat : 'cst Mc.nFormula -> bool) (deduce : 'cst Mc.nFormula -> 'cst Mc.nFormula -> 'cst Mc.nFormula option) (f:'cst formula) = - - let negate a t = - List.map (fun cl -> List.map (fun x -> (x,t)) cl) (negate a) in - - let normalise a t = - List.map (fun cl -> List.map (fun x -> (x,t)) cl) (normalise a) in - - let and_cnf x y = x @ y in - -let rec add_term t0 = function - | [] -> - (match deduce (fst t0) (fst t0) with - | Some u -> if unsat u then T [snd t0] else S (t0::[]) - | None -> S (t0::[])) - | t'::cl0 -> - (match deduce (fst t0) (fst t') with - | Some u -> - if unsat u - then T [snd t0 ; snd t'] - else (match add_term t0 cl0 with - | S cl' -> S (t'::cl') - | T l -> T l) - | None -> - (match add_term t0 cl0 with - | S cl' -> S (t'::cl') - | T l -> T l)) in - - - let rec or_clause cl1 cl2 = - match cl1 with - | [] -> S cl2 - | t0::cl -> - (match add_term t0 cl2 with - | S cl' -> or_clause cl cl' - | T l -> T l) in - - - - let or_clause_cnf t f = - List.fold_right (fun e (acc,tg) -> - match or_clause t e with - | S cl -> (cl :: acc,tg) - | T l -> (acc,tg@l)) f ([],[]) in - - - let rec or_cnf f f' = - match f with - | [] -> tt,[] - | e :: rst -> - let (rst_f',t) = or_cnf rst f' in - let (e_f', t') = or_clause_cnf e f' in - (rst_f' @ e_f', t @ t') in - - - let rec xcnf (polarity : bool) f = - match f with - | TT -> if polarity then (tt,[]) else (ff,[]) - | FF -> if polarity then (ff,[]) else (tt,[]) - | X p -> if polarity then (ff,[]) else (ff,[]) - | A(x,t,_) -> ((if polarity then normalise x t else negate x t),[]) - | N(e) -> xcnf (not polarity) e - | C(e1,e2) -> - let e1,t1 = xcnf polarity e1 in - let e2,t2 = xcnf polarity e2 in - if polarity - then and_cnf e1 e2, t1 @ t2 - else let f',t' = or_cnf e1 e2 in - (f', t1 @ t2 @ t') - | D(e1,e2) -> - let e1,t1 = xcnf polarity e1 in - let e2,t2 = xcnf polarity e2 in - if polarity - then let f',t' = or_cnf e1 e2 in - (f', t1 @ t2 @ t') - else and_cnf e1 e2, t1 @ t2 - | I(e1,_,e2) -> - let e1 , t1 = (xcnf (not polarity) e1) in - let e2 , t2 = (xcnf polarity e2) in - if polarity - then let f',t' = or_cnf e1 e2 in - (f', t1 @ t2 @ t') - else and_cnf e1 e2, t1 @ t2 in - - xcnf true f + ) (** @@ -344,10 +170,11 @@ struct let mic_modules = [ ["Coq";"Lists";"List"]; - ["ZMicromega"]; - ["Tauto"]; - ["RingMicromega"]; - ["EnvRing"]; + ["Coq"; "micromega";"ZMicromega"]; + ["Coq"; "micromega";"Tauto"]; + ["Coq"; "micromega"; "DeclConstant"]; + ["Coq"; "micromega";"RingMicromega"]; + ["Coq"; "micromega";"EnvRing"]; ["Coq"; "micromega"; "ZMicromega"]; ["Coq"; "micromega"; "RMicromega"]; ["Coq" ; "micromega" ; "Tauto"]; @@ -405,6 +232,15 @@ struct let coq_O = lazy (init_constant "O") let coq_S = lazy (init_constant "S") + let coq_nat = lazy (init_constant "nat") + let coq_unit = lazy (init_constant "unit") + (* let coq_option = lazy (init_constant "option")*) + let coq_None = lazy (init_constant "None") + let coq_tt = lazy (init_constant "tt") + let coq_Inl = lazy (init_constant "inl") + let coq_Inr = lazy (init_constant "inr") + + let coq_N0 = lazy (bin_constant "N0") let coq_Npos = lazy (bin_constant "Npos") @@ -431,6 +267,7 @@ struct let coq_CPlus = lazy (m_constant "CPlus") let coq_CMinus = lazy (m_constant "CMinus") let coq_CMult = lazy (m_constant "CMult") + let coq_CPow = lazy (m_constant "CPow") let coq_CInv = lazy (m_constant "CInv") let coq_COpp = lazy (m_constant "COpp") @@ -477,6 +314,7 @@ struct let coq_Rmult = lazy (r_constant "Rmult") let coq_Rinv = lazy (r_constant "Rinv") let coq_Rpower = lazy (r_constant "pow") + let coq_powerZR = lazy (r_constant "powerRZ") let coq_IZR = lazy (r_constant "IZR") let coq_IQR = lazy (r_constant "Q2R") @@ -508,6 +346,8 @@ struct let coq_PsatzC = lazy (constant "PsatzC") let coq_PsatzZ = lazy (constant "PsatzZ") + let coq_GT = lazy (m_constant "GT") + let coq_TT = lazy (gen_constant_in_modules "ZMicromega" [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "TT") @@ -615,6 +455,22 @@ struct | 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 + what to consider as a constant (see [parse_constant]) + *) + + let is_ground_term env sigma term = + let typ = Retyping.get_type_of env sigma term in + try + ignore (Typeclasses.resolve_one_typeclass env sigma (EConstr.mkApp(Lazy.force coq_GT,[| typ;term|]))) ; + true + with + | Not_found -> false + + let parse_z sigma term = let (i,c) = get_left_construct sigma term in match i with @@ -652,6 +508,7 @@ struct | Mc.CPlus(x,y) -> Printf.fprintf o "(%a + %a)" pp_Rcst x pp_Rcst y | Mc.CMinus(x,y) -> Printf.fprintf o "(%a - %a)" pp_Rcst x pp_Rcst y | Mc.CMult(x,y) -> Printf.fprintf o "(%a * %a)" pp_Rcst x pp_Rcst y + | Mc.CPow(x,y) -> Printf.fprintf o "(%a ^ _)" pp_Rcst x | Mc.CInv t -> Printf.fprintf o "(/ %a)" pp_Rcst t | Mc.COpp t -> Printf.fprintf o "(- %a)" pp_Rcst t @@ -665,6 +522,11 @@ struct | Mc.CPlus(x,y) -> EConstr.mkApp(Lazy.force coq_CPlus, [| dump_Rcst x ; dump_Rcst y |]) | Mc.CMinus(x,y) -> EConstr.mkApp(Lazy.force coq_CMinus, [| dump_Rcst x ; dump_Rcst y |]) | Mc.CMult(x,y) -> EConstr.mkApp(Lazy.force coq_CMult, [| dump_Rcst x ; dump_Rcst y |]) + | Mc.CPow(x,y) -> EConstr.mkApp(Lazy.force coq_CPow, [| dump_Rcst x ; + match y with + | Mc.Inl z -> EConstr.mkApp(Lazy.force coq_Inl,[| Lazy.force coq_Z ; Lazy.force coq_nat; dump_z z|]) + | Mc.Inr n -> EConstr.mkApp(Lazy.force coq_Inr,[| Lazy.force coq_Z ; Lazy.force coq_nat; dump_nat n|]) + |]) | Mc.CInv t -> EConstr.mkApp(Lazy.force coq_CInv, [| dump_Rcst t |]) | Mc.COpp t -> EConstr.mkApp(Lazy.force coq_COpp, [| dump_Rcst t |]) @@ -718,9 +580,18 @@ struct | Mc.PX(pol1,p,pol2) -> Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 in pp_pol o e - let pp_cnf pp_c o f = - let pp_clause o l = List.iter (fun ((p,_),t) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c) p Tag.pp t) l in - List.iter (fun l -> Printf.fprintf o "[%a]" pp_clause l) f +(* let pp_clause pp_c o (f: 'cst clause) = + List.iter (fun ((p,_),(t,_)) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c) p Tag.pp t) f *) + + let pp_clause_tag o (f: 'cst clause) = + List.iter (fun ((p,_),(t,_)) -> Printf.fprintf o "(_ @%a)" Tag.pp t) f + +(* let pp_cnf pp_c o (f:'cst cnf) = + List.iter (fun l -> Printf.fprintf o "[%a]" (pp_clause pp_c) l) f *) + + let pp_cnf_tag o (f:'cst cnf) = + List.iter (fun l -> Printf.fprintf o "[%a]" pp_clause_tag l) f + let dump_psatz typ dump_z e = let z = Lazy.force typ in @@ -842,34 +713,74 @@ struct module Env = struct - let compute_rank_add env sigma v = - let rec _add env n v = - match env with - | [] -> ([v],n) - | e::l -> - if EConstr.eq_constr_nounivs sigma e v - then (env,n) - else - let (env,n) = _add l ( n+1) v in - (e::env,n) in - let (env, n) = _add env 1 v in - (env, CamlToCoq.positive n) - let get_rank env sigma v = + type t = { + vars : EConstr.t list ; + (* The list represents a mapping from EConstr.t to indexes. *) + gl : gl; + (* The evar_map may be updated due to unification of universes *) + } + + let empty gl = + { + vars = []; + gl = gl + } + + + (** [eq_constr gl x y] returns an updated [gl] if x and y can be unified *) + let eq_constr gl x y = + let evd = gl.sigma in + match EConstr.eq_constr_universes gl.env evd x y with + | Some csts -> + let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in + begin + match Evd.add_constraints evd csts with + | evd -> Some {gl with sigma = evd} + | exception Univ.UniverseInconsistency _ -> None + end + | None -> None + + let compute_rank_add env v = + let rec _add gl vars n v = + match vars with + | [] -> (gl, [v] ,n) + | e::l -> + match eq_constr gl e v with + | Some gl' -> (gl', vars , n) + | None -> + let (gl,l',n) = _add gl l ( n+1) v in + (gl,e::l',n) in + let (gl',vars', n) = _add env.gl env.vars 1 v in + ({vars=vars';gl=gl'}, CamlToCoq.positive n) + + let get_rank env v = + let evd = env.gl.sigma in let rec _get_rank env n = match env with | [] -> raise (Invalid_argument "get_rank") | e::l -> - if EConstr.eq_constr sigma e v + if EConstr.eq_constr evd e v then n else _get_rank l (n+1) in - _get_rank env 1 + _get_rank env.vars 1 - - let empty = [] + let elements env = env.vars - let elements env = env +(* let string_of_env gl env = + let rec string_of_env i env acc = + match env with + | [] -> acc + | e::env -> string_of_env (i+1) env + (IMap.add i + (Pp.string_of_ppcmds + (Printer.pr_econstr_env gl.env gl.sigma e)) acc) in + string_of_env 1 env IMap.empty + *) + let pp gl env = + let ppl = List.mapi (fun i e -> Pp.str "x" ++ Pp.int (i+1) ++ Pp.str ":" ++ Printer.pr_econstr_env gl.env gl.sigma e)env in + List.fold_right (fun e p -> e ++ Pp.str " ; " ++ p ) ppl (Pp.str "\n") end (* MODULE END: Env *) @@ -877,20 +788,13 @@ struct * This is the big generic function for expression parsers. *) - let parse_expr env sigma parse_constant parse_exp ops_spec term_env term = + let parse_expr gl parse_constant parse_exp ops_spec env term = if debug - then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term); + then ( + Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env gl.env gl.sigma term)); -(* - let constant_or_variable env term = - try - ( Mc.PEc (parse_constant term) , env) - with ParseError -> - let (env,n) = Env.compute_rank_add env term in - (Mc.PEX n , env) in -*) let parse_variable env term = - let (env,n) = Env.compute_rank_add env sigma term in + let (env,n) = Env.compute_rank_add env term in (Mc.PEX n , env) in let rec parse_expr env term = @@ -899,36 +803,36 @@ struct let (expr2,env) = parse_expr env t2 in (op expr1 expr2,env) in - try (Mc.PEc (parse_constant term) , env) + try (Mc.PEc (parse_constant gl term) , env) with ParseError -> - match EConstr.kind sigma term with + match EConstr.kind gl.sigma term with | App(t,args) -> ( - match EConstr.kind sigma t with + match EConstr.kind gl.sigma t with | Const c -> - ( match assoc_ops sigma t ops_spec with + ( match assoc_ops gl.sigma t ops_spec with | 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 + | Opp -> let (expr,env) = parse_expr env args.(0) in + (Mc.PEopp expr, env) + | Power -> + begin try let (expr,env) = parse_expr env args.(0) in let power = (parse_exp expr args.(1)) in - (power , env) + (power , env) with e when CErrors.noncritical e -> (* if the exponent is a variable *) - let (env,n) = Env.compute_rank_add env sigma term in (Mc.PEX n, env) - end - | Ukn s -> - if debug - then (Printf.printf "unknown op: %s\n" s; flush stdout;); - let (env,n) = Env.compute_rank_add env sigma term in (Mc.PEX n, env) - ) + let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env) + end + | Ukn s -> + if debug + 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 in - parse_expr term_env term + parse_expr env term let zop_spec = [ @@ -954,9 +858,23 @@ struct coq_Ropp , Opp ; coq_Rpower , Power] - let zconstant = parse_z - let qconstant = parse_q + (** [parse_constant parse gl t] returns the reification of term [t]. + If [t] is a ground term, then it is first reduced to normal form + before using a 'syntactic' parser *) + let parse_constant parse gl t = + if is_ground_term gl.env gl.sigma t + then + parse gl.sigma (Redexpr.cbv_vm gl.env gl.sigma t) + else raise ParseError + + let zconstant = parse_constant parse_z + let qconstant = parse_constant parse_q + let nconstant = parse_constant parse_nat + (* NB: R is a different story. + Because it is axiomatised, reducing would not be effective. + Therefore, there is a specific parser for constant over R + *) let rconst_assoc = [ @@ -966,60 +884,69 @@ struct (* coq_Rdiv , (fun x y -> Mc.CMult(x,Mc.CInv y)) ;*) ] - let rec rconstant sigma term = - match EConstr.kind sigma term with - | Const x -> - if EConstr.eq_constr sigma term (Lazy.force coq_R0) - then Mc.C0 + let rconstant gl term = + + let sigma = gl.sigma in + + let rec rconstant term = + match EConstr.kind sigma term with + | Const x -> + if EConstr.eq_constr sigma term (Lazy.force coq_R0) + then Mc.C0 else if EConstr.eq_constr sigma term (Lazy.force coq_R1) - then Mc.C1 - else raise ParseError - | App(op,args) -> - begin - try - (* the evaluation order is important in the following *) - let f = assoc_const sigma op rconst_assoc in - let a = rconstant sigma args.(0) in - let b = rconstant sigma args.(1) in - f a b - with + then Mc.C1 + else raise ParseError + | App(op,args) -> + begin + try + (* the evaluation order is important in the following *) + let f = assoc_const sigma op rconst_assoc in + let a = rconstant args.(0) in + let b = rconstant args.(1) in + f a b + with ParseError -> match op with | op when EConstr.eq_constr sigma op (Lazy.force coq_Rinv) -> - let arg = rconstant sigma args.(0) in + 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) - | op when EConstr.eq_constr sigma op (Lazy.force coq_IQR) -> Mc.CQ (parse_q sigma args.(0)) - | op when EConstr.eq_constr sigma op (Lazy.force coq_IZR) -> Mc.CZ (parse_z sigma args.(0)) + | op when EConstr.eq_constr sigma op (Lazy.force coq_Rpower) -> + Mc.CPow(rconstant args.(0) , Mc.Inr (nconstant gl args.(1))) + | op when EConstr.eq_constr sigma op (Lazy.force coq_IQR) -> + Mc.CQ (qconstant gl args.(0)) + | op when EConstr.eq_constr sigma op (Lazy.force coq_IZR) -> + Mc.CZ (zconstant gl args.(0)) | _ -> raise ParseError end + | _ -> raise ParseError in - | _ -> raise ParseError + rconstant term - let rconstant env sigma term = + let rconstant gl term = if debug - then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ()); - let res = rconstant sigma term in + 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) ; res - let parse_zexpr env sigma = parse_expr env sigma - (zconstant sigma) + let parse_zexpr gl = parse_expr gl + zconstant (fun expr x -> - let exp = (parse_z sigma x) in + let exp = (zconstant gl x) in match exp with | Mc.Zneg _ -> Mc.PEc Mc.Z0 | _ -> Mc.PEpow(expr, Mc.Z.to_N exp)) zop_spec - let parse_qexpr env sigma = parse_expr env sigma - (qconstant sigma) + let parse_qexpr gl = parse_expr gl + qconstant (fun expr x -> - let exp = parse_z sigma x in + let exp = zconstant gl x in match exp with | Mc.Zneg _ -> begin @@ -1031,24 +958,23 @@ struct Mc.PEpow(expr,exp)) qop_spec - let parse_rexpr env sigma = parse_expr env sigma - (rconstant env sigma) + let parse_rexpr gl = parse_expr gl + rconstant (fun expr x -> - let exp = Mc.N.of_nat (parse_nat sigma x) in + let exp = Mc.N.of_nat (parse_nat gl.sigma x) in Mc.PEpow(expr,exp)) rop_spec - let parse_arith parse_op parse_expr term_env cstr gl = + let parse_arith parse_op parse_expr env cstr gl = let sigma = gl.sigma in - let env = gl.env in if debug - then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env env sigma cstr ++ fnl ()); + then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ()); match EConstr.kind sigma cstr with | App(op,args) -> let (op,lhs,rhs) = parse_op gl (op,args) in - let (e1,term_env) = parse_expr env sigma term_env lhs in - let (e2,term_env) = parse_expr env sigma term_env rhs in - ({Mc.flhs = e1; Mc.fop = op;Mc.frhs = e2},term_env) + let (e1,env) = parse_expr gl env lhs in + let (e2,env) = parse_expr gl env rhs in + ({Mc.flhs = e1; Mc.fop = op;Mc.frhs = e2},env) | _ -> failwith "error : parse_arith(2)" let parse_zarith = parse_arith parse_zop parse_zexpr @@ -1059,14 +985,14 @@ struct (* generic parsing of arithmetic expressions *) - let mkC f1 f2 = C(f1,f2) - let mkD f1 f2 = D(f1,f2) - let mkIff f1 f2 = C(I(f1,None,f2),I(f2,None,f1)) - let mkI f1 f2 = I(f1,None,f2) + let mkC f1 f2 = Mc.Cj(f1,f2) + let mkD f1 f2 = Mc.D(f1,f2) + let mkIff f1 f2 = Mc.Cj(Mc.I(f1,None,f2),Mc.I(f2,None,f1)) + let mkI f1 f2 = Mc.I(f1,None,f2) let mkformula_binary g term f1 f2 = match f1 , f2 with - | X _ , X _ -> X(term) + | Mc.X _ , Mc.X _ -> Mc.X(term) | _ -> g f1 f2 (** @@ -1079,8 +1005,8 @@ struct let parse_atom env tg t = try let (at,env) = parse_atom env t gl in - (A(at,tg,t), env,Tag.next tg) - with e when CErrors.noncritical e -> (X(t),env,tg) in + (Mc.A(at,(tg,t)), env,Tag.next tg) + with e when CErrors.noncritical e -> (Mc.X(t),env,tg) in let is_prop term = let sort = Retyping.get_sort_of gl.env gl.sigma term in @@ -1099,7 +1025,7 @@ struct let g,env,tg = xparse_formula env tg b in mkformula_binary mkD term f g,env,tg | [|a|] when EConstr.eq_constr sigma l (Lazy.force coq_not) -> - let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg) + let (f,env,tg) = xparse_formula env tg a in (Mc.N(f), env,tg) | [|a;b|] when EConstr.eq_constr sigma l (Lazy.force coq_iff) -> let f,env,tg = xparse_formula env tg a in let g,env,tg = xparse_formula env tg b in @@ -1109,36 +1035,41 @@ struct let f,env,tg = xparse_formula env tg a in let g,env,tg = xparse_formula env tg b in mkformula_binary mkI term f g,env,tg - | _ when EConstr.eq_constr sigma term (Lazy.force coq_True) -> (TT,env,tg) - | _ when EConstr.eq_constr sigma term (Lazy.force coq_False) -> (FF,env,tg) - | _ when is_prop term -> X(term),env,tg + | _ when EConstr.eq_constr sigma term (Lazy.force coq_True) -> (Mc.TT,env,tg) + | _ when EConstr.eq_constr sigma term (Lazy.force coq_False) -> Mc.(FF,env,tg) + | _ when is_prop term -> Mc.X(term),env,tg | _ -> raise ParseError in xparse_formula env tg ((*Reductionops.whd_zeta*) term) let dump_formula typ dump_atom f = - let rec xdump f = + let app_ctor c args = + EConstr.mkApp(Lazy.force c, Array.of_list (typ::EConstr.mkProp::Lazy.force coq_unit :: Lazy.force coq_unit :: args)) in + + let rec xdump f = match f with - | TT -> EConstr.mkApp(Lazy.force coq_TT,[|typ|]) - | FF -> EConstr.mkApp(Lazy.force coq_FF,[|typ|]) - | C(x,y) -> EConstr.mkApp(Lazy.force coq_And,[|typ ; xdump x ; xdump y|]) - | D(x,y) -> EConstr.mkApp(Lazy.force coq_Or,[|typ ; xdump x ; xdump y|]) - | I(x,_,y) -> EConstr.mkApp(Lazy.force coq_Impl,[|typ ; xdump x ; xdump y|]) - | N(x) -> EConstr.mkApp(Lazy.force coq_Neg,[|typ ; xdump x|]) - | A(x,_,_) -> EConstr.mkApp(Lazy.force coq_Atom,[|typ ; dump_atom x|]) - | X(t) -> EConstr.mkApp(Lazy.force coq_X,[|typ ; t|]) in + | Mc.TT -> app_ctor coq_TT [] + | Mc.FF -> app_ctor coq_FF [] + | Mc.Cj(x,y) -> app_ctor coq_And [xdump x ; xdump y] + | Mc.D(x,y) -> app_ctor coq_Or [xdump x ; xdump y] + | Mc.I(x,_,y) -> app_ctor coq_Impl [xdump x ; EConstr.mkApp(Lazy.force coq_None,[|Lazy.force coq_unit|]); xdump y] + | Mc.N(x) -> app_ctor coq_Neg [xdump x] + | Mc.A(x,_) -> app_ctor coq_Atom [dump_atom x;Lazy.force coq_tt] + | Mc.X(t) -> app_ctor coq_X [t] in xdump f - let prop_env_of_formula sigma form = + let prop_env_of_formula gl form = + Mc.( let rec doit env = function - | TT | FF | A(_,_,_) -> env - | X t -> fst (Env.compute_rank_add env sigma t) - | C(f1,f2) | D(f1,f2) | I(f1,_,f2) -> + | TT | FF | A(_,_) -> env + | X t -> fst (Env.compute_rank_add env t) + | Cj(f1,f2) | D(f1,f2) | I(f1,_,f2) -> doit (doit env f1) f2 - | N f -> doit env f in + | N f -> doit env f + in - doit [] form + doit (Env.empty gl) form) let var_env_of_formula form = @@ -1152,14 +1083,14 @@ struct let vars_of_atom {Mc.flhs ; Mc.fop; Mc.frhs} = ISet.union (vars_of_expr flhs) (vars_of_expr frhs) in - + Mc.( let rec doit = function - | TT | FF | X _ -> ISet.empty - | A (a,t,c) -> vars_of_atom a - | C(f1,f2) | D(f1,f2) |I (f1,_,f2) -> ISet.union (doit f1) (doit f2) + | TT | FF | X _ -> ISet.empty + | A (a,(t,c)) -> vars_of_atom a + | Cj(f1,f2) | D(f1,f2) |I (f1,_,f2) -> ISet.union (doit f1) (doit f2) | N f -> doit f in - doit form + doit form) @@ -1212,6 +1143,12 @@ let rec dump_Rcst_as_R cst = | Mc.CPlus(x,y) -> EConstr.mkApp(Lazy.force coq_Rplus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) | Mc.CMinus(x,y) -> EConstr.mkApp(Lazy.force coq_Rminus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) | Mc.CMult(x,y) -> EConstr.mkApp(Lazy.force coq_Rmult, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) + | Mc.CPow(x,y) -> + begin + match y with + | Mc.Inl z -> EConstr.mkApp(Lazy.force coq_powerZR,[| dump_Rcst_as_R x ; dump_z z|]) + | Mc.Inr n -> EConstr.mkApp(Lazy.force coq_Rpower,[| dump_Rcst_as_R x ; dump_nat n|]) + end | Mc.CInv t -> EConstr.mkApp(Lazy.force coq_Rinv, [| dump_Rcst_as_R t |]) | Mc.COpp t -> EConstr.mkApp(Lazy.force coq_Ropp, [| dump_Rcst_as_R t |]) @@ -1247,17 +1184,17 @@ let prodn n env b = in prodrec (n,env,b) -let make_goal_of_formula sigma dexpr form = +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 sigma form in + 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) props 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 var_name_pos = List.map2 (fun (idx,_) (id,_) -> id,idx) vars_idx vars_n in @@ -1288,14 +1225,14 @@ let make_goal_of_formula sigma dexpr form = let rec xdump pi xi f = match f with - | TT -> Lazy.force coq_True - | FF -> Lazy.force coq_False - | C(x,y) -> EConstr.mkApp(Lazy.force coq_and,[|xdump pi xi x ; xdump pi xi y|]) - | D(x,y) -> EConstr.mkApp(Lazy.force coq_or,[| xdump pi xi x ; xdump pi xi y|]) - | I(x,_,y) -> EConstr.mkArrow (xdump pi xi x) Sorts.Relevant (xdump (pi+1) (xi+1) y) - | N(x) -> EConstr.mkArrow (xdump pi xi x) Sorts.Relevant (Lazy.force coq_False) - | A(x,_,_) -> dump_cstr xi x - | X(t) -> let idx = Env.get_rank props sigma t in + | Mc.TT -> Lazy.force coq_True + | Mc.FF -> Lazy.force coq_False + | Mc.Cj(x,y) -> EConstr.mkApp(Lazy.force coq_and,[|xdump pi xi x ; xdump pi xi y|]) + | Mc.D(x,y) -> EConstr.mkApp(Lazy.force coq_or,[| xdump pi xi x ; xdump pi xi y|]) + | Mc.I(x,_,y) -> EConstr.mkArrow (xdump pi xi x) Sorts.Relevant (xdump (pi+1) (xi+1) y) + | 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 let nb_vars = List.length vars_n in @@ -1304,10 +1241,10 @@ let make_goal_of_formula sigma dexpr form = (* Printf.fprintf stdout "NBProps : %i\n" nb_props ;*) let subst_prop p = - let idx = Env.get_rank props sigma p in + let idx = Env.get_rank props p in EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx)) in - let form' = map_prop subst_prop form in + let form' = Mc.mapX subst_prop form in (prodn nb_props (List.map (fun (x,y) -> Name.Name x,y) props_n) (prodn nb_vars (List.map (fun (x,y) -> Name.Name x,y) vars_n) @@ -1336,12 +1273,12 @@ end (** open M -let coq_Node = +let coq_Branch = lazy (gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node") -let coq_Leaf = + [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Branch") +let coq_Elt = lazy (gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf") + [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Elt") let coq_Empty = lazy (gen_constant_in_modules "VarMap" [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty") @@ -1354,9 +1291,9 @@ let coq_VarMap = let rec dump_varmap typ m = match m with | Mc.Empty -> EConstr.mkApp(Lazy.force coq_Empty,[| typ |]) - | Mc.Leaf v -> EConstr.mkApp(Lazy.force coq_Leaf,[| typ; v|]) - | Mc.Node(l,o,r) -> - EConstr.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |]) + | Mc.Elt v -> EConstr.mkApp(Lazy.force coq_Elt,[| typ; v|]) + | Mc.Branch(l,o,r) -> + EConstr.mkApp (Lazy.force coq_Branch, [| typ; dump_varmap typ l; o ; dump_varmap typ r |]) let vm_of_list env = @@ -1426,7 +1363,9 @@ let rec parse_hyps gl parse_arith env tg hyps = (*exception ParseError*) -let parse_goal gl parse_arith env hyps term = + + +let parse_goal gl parse_arith (env:Env.t) hyps term = (* try*) let (f,env,tg) = parse_formula gl parse_arith env (Tag.from 0) term in let (lhyps,env,tg) = parse_hyps gl parse_arith env tg hyps in @@ -1460,6 +1399,40 @@ let qq_domain_spec = lazy { dump_proof = dump_psatz coq_Q dump_q } +let max_tag f = 1 + (Tag.to_int (Mc.foldA (fun t1 (t2,_) -> Tag.max t1 t2) f (Tag.from 0))) + + +(** For completeness of the cutting-plane procedure, + each variable 'x' is replaced by 'y' - 'z' where + 'y' and 'z' are positive *) +let pre_processZ mt f = + + let x0 i = 2 * i in + let x1 i = 2 * i + 1 in + + let tag_of_var fr p b = + + let ip = CoqToCaml.positive fr + (CoqToCaml.positive p) in + + match b with + | None -> + let y = Mc.XO (Mc.Coq_Pos.add fr p) in + let z = Mc.XI (Mc.Coq_Pos.add fr p) in + let tag = Tag.from (- x0 (x0 ip)) in + let constr = Mc.mk_eq_pos p y z in + (tag, dump_cstr (Lazy.force coq_Z) dump_z constr) + | Some false -> + let y = Mc.XO (Mc.Coq_Pos.add fr p) in + let tag = Tag.from (- x0 (x1 ip)) in + let constr = Mc.bound_var (Mc.XO y) in + (tag, dump_cstr (Lazy.force coq_Z) dump_z constr) + | Some true -> + let z = Mc.XI (Mc.Coq_Pos.add fr p) in + let tag = Tag.from (- x1 (x1 ip)) in + let constr = Mc.bound_var (Mc.XI z) in + (tag, dump_cstr (Lazy.force coq_Z) dump_z constr) in + + 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 @@ -1495,10 +1468,12 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* * The datastructures that aggregate prover attributes. *) -type ('option,'a,'prf) prover = { +open Certificate + +type ('option,'a,'prf,'model) prover = { name : string ; (* name of the prover *) - get_option : unit ->'option ; (* find the options of the prover *) - prover : 'option * 'a list -> 'prf option ; (* the prover itself *) + get_option : unit ->'option ; (* find the options of the prover *) + prover : ('option * 'a list) -> ('prf, 'model) Certificate.res ; (* the prover itself *) hyps : 'prf -> ISet.t ; (* extract the indexes of the hypotheses really used in the proof *) compact : 'prf -> (int -> int) -> 'prf ; (* remap the hyp indexes according to function *) pp_prf : out_channel -> 'prf -> unit ;(* pretting printing of proof *) @@ -1508,37 +1483,37 @@ type ('option,'a,'prf) prover = { (** - * Given a list of provers and a disjunction of atoms, find a proof of any of + * 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 * datastructure. *) -let find_witness provers polys1 = - let provers = List.map (fun p -> - (fun l -> - match p.prover (p.get_option (),l) with - | None -> None - | Some prf -> Some(prf,p)) , p.name) provers in - try_any provers (List.map fst polys1) +let find_witness p polys1 = + let polys1 = List.map fst polys1 in + match p.prover (p.get_option (), polys1) with + | Model m -> Model m + | Unknown -> Unknown + | Prf prf -> Prf(prf,p) (** - * Given a list of provers and a CNF, find a proof for each of the clauses. + * Given a prover and a CNF, find a proof for each of the clauses. * Return the proofs as a list. *) -let witness_list prover l = +let witness_list prover l = let rec xwitness_list l = match l with - | [] -> Some [] + | [] -> Prf [] | e :: l -> - match find_witness prover e with - | None -> None - | Some w -> - (match xwitness_list l with - | None -> None - | Some l -> Some (w :: l) - ) in - xwitness_list l + match xwitness_list l with + | Model (m,e) -> Model (m,e) + | Unknown -> Unknown + | Prf l -> + match find_witness prover e with + | Model m -> Model (m,e) + | Unknown -> Unknown + | Prf w -> Prf (w::l) in + xwitness_list l let witness_list_tags = witness_list @@ -1546,6 +1521,7 @@ let witness_list_tags = witness_list * Prune the proof object, according to the 'diff' between two cnf formulas. *) + let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = let compact_proof (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) = @@ -1564,9 +1540,9 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = let res = try prover.compact prf remap with x when CErrors.noncritical x -> if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ; (* This should not happen -- this is the recovery plan... *) - match prover.prover (prover.get_option () ,List.map fst new_cl) with - | None -> failwith "proof compaction error" - | Some p -> p + match prover.prover (prover.get_option (), List.map fst new_cl) with + | Unknown | Model _ -> failwith "proof compaction error" + | Prf p -> p in if debug then begin @@ -1581,11 +1557,31 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = let hyps = selecti hyps_idx old_cl in is_sublist Pervasives.(=) hyps new_cl in + + let cnf_res = List.combine cnf_ff res in (* we get pairs clause * proof *) + if debug then + begin + Printf.printf "CNFRES\n"; flush stdout; + List.iter (fun (cl,(prf,prover)) -> + let hyps_idx = prover.hyps prf in + let hyps = selecti hyps_idx cl in + Printf.printf "\nProver %a -> %a\n" + pp_clause_tag cl pp_clause_tag hyps;flush stdout) cnf_res; + Printf.printf "CNFNEW %a\n" pp_cnf_tag cnf_ff'; + + end; List.map (fun x -> - let (o,p) = List.find (fun (l,p) -> is_proof_compatible l p x) cnf_res - in compact_proof o p x) cnf_ff' + let (o,p) = + try + List.find (fun (l,p) -> is_proof_compatible l p x) cnf_res + with Not_found -> + begin + Printf.printf "ERROR: no compatible proof" ; flush stdout; + failwith "Cannot find compatible proof" end + in + compact_proof o p x) cnf_ff' (** @@ -1594,14 +1590,15 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = *) 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) - | C(f1,f2) -> + | 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 -> C(f1,f2) ) + | 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|])) @@ -1618,21 +1615,22 @@ let abstract_formula hyps f = ) | FF -> FF | TT -> TT - in xabs f + in xabs f) (* [abstract_wrt_formula] is used in contexts whre f1 is already an abstraction of f2 *) let rec abstract_wrt_formula f1 f2 = + Mc.( match f1 , f2 with | X c , _ -> X c | A _ , A _ -> f2 - | C(a,b) , C(a',b') -> C(abstract_wrt_formula a a', abstract_wrt_formula b b') + | Cj(a,b) , Cj(a',b') -> Cj(abstract_wrt_formula a a', abstract_wrt_formula b b') | D(a,b) , D(a',b') -> D(abstract_wrt_formula a a', abstract_wrt_formula b b') | I(a,_,b) , I(a',x,b') -> I(abstract_wrt_formula a a',x, abstract_wrt_formula b b') | FF , FF -> FF | TT , TT -> TT | N x , N y -> N(abstract_wrt_formula x y) - | _ -> failwith "abstract_wrt_formula" + | _ -> failwith "abstract_wrt_formula") (** * This exception is raised by really_call_csdpcert if Coq's configure didn't @@ -1651,52 +1649,46 @@ let formula_hyps_concl hyps concl = List.fold_right (fun (id,f) (cc,ids) -> match f with - X _ -> (cc,ids) - | _ -> (I(f,Some id,cc), id::ids)) + Mc.X _ -> (cc,ids) + | _ -> (Mc.I(f,Some id,cc), id::ids)) hyps (concl,[]) -let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 gl = +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 *) let (ff,ids) = formula_hyps_concl polys1 polys2 in + let mt = CamlToCoq.positive (max_tag ff) in - (* Convert the aplpication into a (mc_)cnf (a list of lists of formulas) *) - let cnf_ff,cnf_ff_tags = cnf negate normalise unsat deduce ff in - - if debug then - begin - Feedback.msg_notice (Pp.str "Formula....\n") ; - let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in - let ff = dump_formula formula_typ - (dump_cstr spec.typ spec.dump_coeff) ff in - Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff); - Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff - end; + (* Construction of cnf *) + let pre_ff = (pre_process mt ff) in + let (cnf_ff,cnf_ff_tags) = cnf pre_ff in match witness_list_tags prover cnf_ff with - | None -> None - | Some res -> (*Printf.printf "\nList %i" (List.length `res); *) - let hyps = List.fold_left (fun s (cl,(prf,p)) -> - let tags = ISet.fold (fun i s -> let t = 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 cnf_ff_tags) (List.combine cnf_ff res) in - - if debug then (Printf.printf "TForm : %a\n" pp_formula ff ; flush stdout; - Printf.printf "Hyps : %a\n" (fun o s -> TagSet.fold (fun i _ -> Printf.fprintf o "%a " Tag.pp i) s ()) hyps) ; + | Model m -> Model m + | Unknown -> Unknown + | Prf res -> (*Printf.printf "\nList %i" (List.length `res); *) + let hyps = 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 let ff' = abstract_formula hyps ff in - let cnf_ff',_ = cnf negate normalise unsat deduce ff' in + + let pre_ff' = pre_process mt ff' in + let cnf_ff',_ = cnf pre_ff' in + if debug then begin - Feedback.msg_notice (Pp.str "\nAFormula\n") ; - let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in - let ff' = dump_formula formula_typ - (dump_cstr spec.typ spec.dump_coeff) ff' in - Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff'); - Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff' + output_string stdout "\n"; + Printf.printf "TForm : %a\n" pp_formula 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; end; (* Even if it does not work, this does not mean it is not provable @@ -1710,10 +1702,18 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 end ; *) let res' = compact_proofs cnf_ff res cnf_ff' in - let (ff',res',ids) = (ff',res', ids_of_formula ff') in + let (ff',res',ids) = (ff',res', Mc.ids_of_formula ff') in let res' = dump_list (spec.proof_typ) spec.dump_proof res' in - Some (ids,ff',res') + Prf (ids,ff',res') + +let micromega_tauto pre_process cnf spec prover env (polys1: (Names.Id.t * 'cst formula) list) (polys2: 'cst formula) gl = + try micromega_tauto pre_process cnf spec prover env polys1 polys2 gl + with Not_found -> + begin + Printexc.print_backtrace stdout; flush stdout; + Unknown + end (** @@ -1725,9 +1725,8 @@ let fresh_id avoid id gl = let micromega_gen parse_arith - (negate:'cst atom -> 'cst mc_cnf) - (normalise:'cst atom -> 'cst mc_cnf) - unsat deduce + pre_process + cnf spec dumpexpr prover tac = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in @@ -1735,15 +1734,19 @@ let micromega_gen let hyps = Tacmach.New.pf_hyps_types gl in try let gl0 = { env = Tacmach.New.pf_env gl; sigma } in - let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in + 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 dumpexpr = Lazy.force dumpexpr in + + + if debug then Feedback.msg_debug (Pp.str "Env " ++ (Env.pp gl0 env)) ; - match micromega_tauto negate normalise unsat deduce spec prover env hyps concl gl0 with - | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") - | Some (ids,ff',res') -> - let (arith_goal,props,vars,ff_arith) = make_goal_of_formula sigma dumpexpr ff' in + 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_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in @@ -1756,7 +1759,7 @@ let micromega_gen micromega_order_change spec res' (EConstr.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env' ff_arith ] in - let goal_props = List.rev (prop_env_of_formula sigma ff') 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 @@ -1786,16 +1789,10 @@ let micromega_gen ^ "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_gen parse_arith - (negate:'cst atom -> 'cst mc_cnf) - (normalise:'cst atom -> 'cst mc_cnf) - unsat deduce - spec prover = - (micromega_gen parse_arith negate normalise unsat deduce spec prover) - - + | x -> begin if debug then Tacticals.New.tclFAIL 0 (Pp.str (Printexc.get_backtrace ())) + else raise x + end + end 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 *) @@ -1826,10 +1823,6 @@ let micromega_order_changer cert env ff = let micromega_genr prover tac = let parse_arith = parse_rarith in - let negate = Mc.rnegate in - let normalise = Mc.rnormalise in - let unsat = Mc.runsat in - let deduce = Mc.rdeduce in let spec = lazy { typ = Lazy.force coq_R; coeff = Lazy.force coq_Rcst; @@ -1844,21 +1837,21 @@ let micromega_genr prover tac = try let gl0 = { env = Tacmach.New.pf_env gl; sigma } in - let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in + 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, map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in - let concl' = map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) concl 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 negate normalise unsat deduce spec prover env hyps' concl' gl0 with - | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") - | Some (ids,ff',res') -> + 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' = abstract_wrt_formula ff' ff in - let (arith_goal,props,vars,ff_arith) = make_goal_of_formula sigma (Lazy.force dump_rexpr) 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_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in @@ -1870,7 +1863,7 @@ let micromega_genr prover tac = let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; micromega_order_changer res' env' ff_arith ] in - let goal_props = List.rev (prop_env_of_formula sigma ff') 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 @@ -1911,8 +1904,8 @@ let micromega_genr prover = (micromega_genr prover) let lift_ratproof prover l = match prover l with - | None -> None - | Some c -> Some (Mc.RatProof( c,Mc.DoneProof)) + | Unknown | Model _ -> Unknown + | Prf c -> Prf (Mc.RatProof( c,Mc.DoneProof)) type micromega_polys = (Micromega.q Mc.pol * Mc.op1) list @@ -1983,22 +1976,22 @@ let rec z_to_q_pol e = let call_csdpcert_q provername poly = match call_csdpcert provername poly with - | None -> None + | None -> Unknown | Some cert -> let cert = Certificate.q_cert_of_pos cert in if Mc.qWeakChecker poly cert - then Some cert - else ((print_string "buggy certificate") ;None) + then Prf cert + else ((print_string "buggy certificate") ;Unknown) let call_csdpcert_z provername poly = let l = List.map (fun (e,o) -> (z_to_q_pol e,o)) poly in match call_csdpcert provername l with - | None -> None + | None -> Unknown | Some cert -> let cert = Certificate.z_cert_of_pos cert in if Mc.zWeakChecker poly cert - then Some cert - else ((print_string "buggy certificate" ; flush stdout) ;None) + then Prf cert + else ((print_string "buggy certificate" ; flush stdout) ;Unknown) let xhyps_of_cone base acc prf = let rec xtract e acc = @@ -2041,12 +2034,6 @@ let hyps_of_pt pt = xhyps 0 pt ISet.empty -let hyps_of_pt pt = - let res = hyps_of_pt pt in - if debug - then (Printf.fprintf stdout "\nhyps_of_pt : %a -> " pp_proof_term pt ; ISet.iter (fun i -> Printf.printf "%i " i) res); - res - let compact_pt pt f = let translate ofset x = if x < ofset then x @@ -2141,8 +2128,8 @@ let non_linear_prover_R str o = { let non_linear_prover_Z str o = { name = "real nonlinear prover"; - get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l); + get_option = (fun () -> (str,o)); + prover = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l); hyps = hyps_of_pt; compact = compact_pt; pp_prf = pp_proof_term; @@ -2175,52 +2162,65 @@ let nlinear_Z = { *) let lra_Q = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr - [ linear_prover_Q ] + micromega_gen parse_qarith (fun _ x -> x) Mc.cnfQ qq_domain_spec dump_qexpr + linear_prover_Q let psatz_Q i = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr - [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] + micromega_gen parse_qarith (fun _ x -> x) Mc.cnfQ qq_domain_spec dump_qexpr + (non_linear_prover_Q "real_nonlinear_prover" (Some i) ) let lra_R = - micromega_genr [ linear_prover_R ] + micromega_genr linear_prover_R let psatz_R i = - micromega_genr [ non_linear_prover_R "real_nonlinear_prover" (Some i) ] + micromega_genr (non_linear_prover_R "real_nonlinear_prover" (Some i)) let psatz_Z i = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr - [ non_linear_prover_Z "real_nonlinear_prover" (Some i) ] + micromega_gen parse_zarith (fun _ x -> x) Mc.cnfZ zz_domain_spec dump_zexpr + (non_linear_prover_Z "real_nonlinear_prover" (Some i) ) let sos_Z = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr - [ non_linear_prover_Z "pure_sos" None ] + micromega_gen parse_zarith (fun _ x -> x) Mc.cnfZ zz_domain_spec dump_zexpr + (non_linear_prover_Z "pure_sos" None) let sos_Q = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr - [ non_linear_prover_Q "pure_sos" None ] + micromega_gen parse_qarith (fun _ x -> x) Mc.cnfQ qq_domain_spec dump_qexpr + (non_linear_prover_Q "pure_sos" None) let sos_R = - micromega_genr [ non_linear_prover_R "pure_sos" None ] + micromega_genr (non_linear_prover_R "pure_sos" None) -let xlia = micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr - [ linear_Z ] +let xlia = + micromega_gen parse_zarith pre_processZ Mc.cnfZ zz_domain_spec dump_zexpr + linear_Z + let xnlia = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr - [ nlinear_Z ] + micromega_gen parse_zarith (fun _ x -> x) Mc.cnfZ zz_domain_spec dump_zexpr + nlinear_Z let nra = - micromega_genr [ nlinear_prover_R ] + micromega_genr nlinear_prover_R let nqa = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr - [ nlinear_prover_R ] + 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 *) diff --git a/plugins/micromega/coq_micromega.mli b/plugins/micromega/coq_micromega.mli index d1776b8ca4..075594cffc 100644 --- a/plugins/micromega/coq_micromega.mli +++ b/plugins/micromega/coq_micromega.mli @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +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 21f0414e9c..6bf5f76a04 100644 --- a/plugins/micromega/g_micromega.mlg +++ b/plugins/micromega/g_micromega.mlg @@ -30,6 +30,9 @@ 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 diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index f67f1da146..b34c3b2b7d 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -1,4 +1,9 @@ +type __ = Obj.t + +type unit0 = +| Tt + (** val negb : bool -> bool **) let negb = function @@ -9,6 +14,20 @@ type nat = | O | S of nat +type ('a, 'b) sum = +| Inl of 'a +| Inr of 'b + +(** val fst : ('a1 * 'a2) -> 'a1 **) + +let fst = function +| x,_ -> x + +(** val snd : ('a1 * 'a2) -> 'a2 **) + +let snd = function +| _,y -> y + (** val app : 'a1 list -> 'a1 list -> 'a1 list **) let rec app l m = @@ -37,6 +56,29 @@ module Coq__1 = struct end include Coq__1 +(** val nth : nat -> 'a1 list -> 'a1 -> 'a1 **) + +let rec nth n0 l default = + match n0 with + | O -> (match l with + | [] -> default + | x::_ -> x) + | S m -> (match l with + | [] -> default + | _::t0 -> nth m t0 default) + +(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **) + +let rec map f = function +| [] -> [] +| a::t0 -> (f a)::(map f t0) + +(** val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 **) + +let rec fold_right f a0 = function +| [] -> a0 +| b::t0 -> f b (fold_right f a0 t0) + type positive = | XI of positive | XO of positive @@ -269,29 +311,6 @@ let rec pow_pos rmul x = function | XO i0 -> let p = pow_pos rmul x i0 in rmul p p | XH -> x -(** val nth : nat -> 'a1 list -> 'a1 -> 'a1 **) - -let rec nth n0 l default = - match n0 with - | O -> (match l with - | [] -> default - | x::_ -> x) - | S m -> (match l with - | [] -> default - | _::t0 -> nth m t0 default) - -(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **) - -let rec map f = function -| [] -> [] -| a::t0 -> (f a)::(map f t0) - -(** val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 **) - -let rec fold_right f a0 = function -| [] -> a0 -| b::t0 -> f b (fold_right f a0 t0) - module Z = struct (** val double : z -> z **) @@ -435,6 +454,12 @@ module Z = | Zpos p -> Npos p | _ -> N0 + (** val of_nat : nat -> z **) + + let of_nat = function + | O -> Z0 + | S n1 -> Zpos (Coq_Pos.of_succ_nat n1) + (** val pos_div_eucl : positive -> z -> z * z **) let rec pos_div_eucl a b = @@ -889,53 +914,105 @@ let rec norm_aux cO cI cadd cmul csub copp ceqb = function ppow_N cO cI cadd cmul ceqb (fun p -> p) (norm_aux cO cI cadd cmul csub copp ceqb pe1) n0 -type 'a bFormula = +type ('tA, 'tX, 'aA, 'aF) gFormula = | TT | FF -| X -| A of 'a -| Cj of 'a bFormula * 'a bFormula -| D of 'a bFormula * 'a bFormula -| N of 'a bFormula -| I of 'a bFormula * 'a bFormula - -(** val map_bformula : ('a1 -> 'a2) -> 'a1 bFormula -> 'a2 bFormula **) +| X of 'tX +| A of 'tA * 'aA +| Cj of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula +| D of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula +| N of ('tA, 'tX, 'aA, 'aF) gFormula +| I of ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option + * ('tA, 'tX, 'aA, 'aF) gFormula + +(** val mapX : + ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) + gFormula **) + +let rec mapX f = function +| X x -> X (f x) +| Cj (f1, f2) -> Cj ((mapX f f1), (mapX f f2)) +| D (f1, f2) -> D ((mapX f f1), (mapX f f2)) +| N f1 -> N (mapX f f1) +| I (f1, o, f2) -> I ((mapX f f1), o, (mapX f f2)) +| x -> x + +(** val foldA : + ('a5 -> 'a3 -> 'a5) -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 **) + +let rec foldA f f0 acc = + match f0 with + | A (_, an) -> f acc an + | Cj (f1, f2) -> foldA f f1 (foldA f f2 acc) + | D (f1, f2) -> foldA f f1 (foldA f f2 acc) + | N f1 -> foldA f f1 acc + | I (f1, _, f2) -> foldA f f1 (foldA f f2 acc) + | _ -> acc + +(** val cons_id : 'a1 option -> 'a1 list -> 'a1 list **) + +let cons_id id l = + match id with + | Some id0 -> id0::l + | None -> l + +(** val ids_of_formula : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list **) + +let rec ids_of_formula = function +| I (_, id, f') -> cons_id id (ids_of_formula f') +| _ -> [] + +(** val collect_annot : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list **) + +let rec collect_annot = function +| A (_, a) -> a::[] +| Cj (f1, f2) -> app (collect_annot f1) (collect_annot f2) +| D (f1, f2) -> app (collect_annot f1) (collect_annot f2) +| N f0 -> collect_annot f0 +| I (f1, _, f2) -> app (collect_annot f1) (collect_annot f2) +| _ -> [] + +type 'a bFormula = ('a, __, unit0, unit0) gFormula + +(** val map_bformula : + ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, 'a5) + gFormula **) let rec map_bformula fct = function | TT -> TT | FF -> FF -| X -> X -| A a -> A (fct a) +| X p -> X p +| A (a, t0) -> A ((fct a), t0) | Cj (f1, f2) -> Cj ((map_bformula fct f1), (map_bformula fct f2)) | D (f1, f2) -> D ((map_bformula fct f1), (map_bformula fct f2)) | N f0 -> N (map_bformula fct f0) -| I (f1, f2) -> I ((map_bformula fct f1), (map_bformula fct f2)) +| I (f1, a, f2) -> I ((map_bformula fct f1), a, (map_bformula fct f2)) -type 'x clause = 'x list +type ('x, 'annot) clause = ('x * 'annot) list -type 'x cnf = 'x clause list +type ('x, 'annot) cnf = ('x, 'annot) clause list -(** val tt : 'a1 cnf **) +(** val cnf_tt : ('a1, 'a2) cnf **) -let tt = +let cnf_tt = [] -(** val ff : 'a1 cnf **) +(** val cnf_ff : ('a1, 'a2) cnf **) -let ff = +let cnf_ff = []::[] (** val add_term : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause -> 'a1 - clause option **) + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) + clause -> ('a1, 'a2) clause option **) let rec add_term unsat deduce t0 = function | [] -> - (match deduce t0 t0 with + (match deduce (fst t0) (fst t0) with | Some u -> if unsat u then None else Some (t0::[]) | None -> Some (t0::[])) | t'::cl0 -> - (match deduce t0 t' with + (match deduce (fst t0) (fst t') with | Some u -> if unsat u then None @@ -948,8 +1025,8 @@ let rec add_term unsat deduce t0 = function | None -> None)) (** val or_clause : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 clause - -> 'a1 clause option **) + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, + 'a2) clause -> ('a1, 'a2) clause option **) let rec or_clause unsat deduce cl1 cl2 = match cl1 with @@ -960,8 +1037,8 @@ let rec or_clause unsat deduce cl1 cl2 = | None -> None) (** val or_clause_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 cnf -> - 'a1 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 -> @@ -970,29 +1047,32 @@ let or_clause_cnf unsat deduce t0 f = | None -> acc) [] f (** val or_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 cnf -> 'a1 cnf -> 'a1 - cnf **) + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, + 'a2) cnf -> ('a1, 'a2) cnf **) let rec or_cnf unsat deduce f f' = match f with - | [] -> tt + | [] -> cnf_tt | e::rst -> app (or_cnf unsat deduce rst f') (or_clause_cnf unsat deduce e f') -(** val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **) +(** val and_cnf : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf **) let and_cnf = app +type ('term, 'annot, 'tX, 'aF) tFormula = ('term, 'tX, 'annot, 'aF) gFormula + (** val xcnf : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 - -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 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 **) let rec xcnf unsat deduce normalise0 negate0 pol0 = function -| TT -> if pol0 then tt else ff -| FF -> if pol0 then ff else tt -| X -> ff -| A x -> if pol0 then normalise0 x else negate0 x +| 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 | Cj (e1, e2) -> if pol0 then and_cnf (xcnf unsat deduce normalise0 negate0 pol0 e1) @@ -1006,7 +1086,7 @@ let rec xcnf unsat deduce normalise0 negate0 pol0 = function 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 -| I (e1, e2) -> +| I (e1, _, e2) -> if pol0 then or_cnf unsat deduce (xcnf unsat deduce normalise0 negate0 (negb pol0) e1) @@ -1014,8 +1094,95 @@ let rec xcnf unsat deduce normalise0 negate0 pol0 = function else and_cnf (xcnf unsat deduce normalise0 negate0 (negb pol0) e1) (xcnf unsat deduce normalise0 negate0 pol0 e2) +(** val radd_term : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) + clause -> (('a1, 'a2) clause, 'a2 list) sum **) + +let rec radd_term unsat deduce t0 = function +| [] -> + (match deduce (fst t0) (fst t0) with + | Some u -> if unsat u then Inr ((snd t0)::[]) else Inl (t0::[]) + | None -> Inl (t0::[])) +| t'::cl0 -> + (match deduce (fst t0) (fst t') with + | Some u -> + if unsat u + then Inr ((snd t0)::((snd t')::[])) + else (match radd_term unsat deduce t0 cl0 with + | Inl cl' -> Inl (t'::cl') + | Inr l -> Inr l) + | None -> + (match radd_term unsat deduce t0 cl0 with + | Inl cl' -> Inl (t'::cl') + | Inr l -> Inr l)) + +(** val ror_clause : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, + 'a2) clause -> (('a1, 'a2) clause, 'a2 list) sum **) + +let rec ror_clause unsat deduce cl1 cl2 = + match cl1 with + | [] -> Inl cl2 + | t0::cl -> + (match radd_term unsat deduce t0 cl2 with + | Inl cl' -> ror_clause unsat deduce cl cl' + | Inr l -> Inr l) + +(** 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 = + fold_right (fun e pat -> + 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 + +(** val ror_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list list -> + ('a1, 'a2) clause list -> ('a1, 'a2) cnf * 'a2 list **) + +let rec ror_cnf unsat deduce f f' = + match f with + | [] -> cnf_tt,[] + | 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') + +(** 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 +| 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),[] +| 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 + 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')) +| 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 + 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 +| 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 + 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) + (** val cnf_checker : - ('a1 list -> 'a2 -> bool) -> 'a1 cnf -> 'a2 list -> bool **) + (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool **) let rec cnf_checker checker f l = match f with @@ -1026,9 +1193,9 @@ let rec cnf_checker checker f l = | c::l0 -> if checker e c then cnf_checker checker f0 l0 else false) (** val tauto_checker : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 - -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 bFormula -> 'a3 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 **) let tauto_checker unsat deduce normalise0 negate0 checker f w = cnf_checker checker (xcnf unsat deduce normalise0 negate0 true f) w @@ -1243,11 +1410,12 @@ let xnormalise cO cI cplus ctimes cminus copp ceqb t0 = (** val cnf_normalise : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 - nFormula cnf **) + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> + ('a1 nFormula, 'a2) cnf **) -let cnf_normalise cO cI cplus ctimes cminus copp ceqb t0 = - map (fun x -> x::[]) (xnormalise cO cI cplus ctimes cminus copp ceqb t0) +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) (** val xnegate : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 @@ -1271,11 +1439,11 @@ let xnegate cO cI cplus ctimes cminus copp ceqb t0 = (** val cnf_negate : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 - nFormula cnf **) + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> + ('a1 nFormula, 'a2) cnf **) -let cnf_negate cO cI cplus ctimes cminus copp ceqb t0 = - map (fun x -> x::[]) (xnegate cO cI cplus ctimes cminus copp ceqb t0) +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) (** val xdenorm : positive -> 'a1 pol -> 'a1 pExpr **) @@ -1366,6 +1534,13 @@ let simpl_cone cO cI ctimes ceqb e = match e with | _ -> PsatzAdd (t1, t2))) | _ -> e +module PositiveSet = + struct + type tree = + | Leaf + | Node of tree * bool * tree + end + type q = { qnum : z; qden : positive } (** val qnum : q -> z **) @@ -1429,16 +1604,16 @@ let qpower q0 = function type 'a t = | Empty -| Leaf of 'a -| Node of 'a t * 'a * 'a t +| Elt of 'a +| Branch of 'a t * 'a * 'a t (** val find : 'a1 -> 'a1 t -> positive -> 'a1 **) let rec find default vm p = match vm with | Empty -> default - | Leaf i -> i - | Node (l, e, r) -> + | Elt i -> i + | Branch (l, e, r) -> (match p with | XI p2 -> find default r p2 | XO p2 -> find default l p2 @@ -1448,24 +1623,24 @@ let rec find default vm p = let rec singleton default x v = match x with - | XI p -> Node (Empty, default, (singleton default p v)) - | XO p -> Node ((singleton default p v), default, Empty) - | XH -> Leaf v + | XI p -> Branch (Empty, default, (singleton default p v)) + | XO p -> Branch ((singleton default p v), default, Empty) + | XH -> Elt v (** val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t **) let rec vm_add default x v = function | Empty -> singleton default x v -| Leaf vl -> +| Elt vl -> (match x with - | XI p -> Node (Empty, vl, (singleton default p v)) - | XO p -> Node ((singleton default p v), vl, Empty) - | XH -> Leaf v) -| Node (l, o, r) -> + | XI p -> Branch (Empty, vl, (singleton default p v)) + | XO p -> Branch ((singleton default p v), vl, Empty) + | XH -> Elt v) +| Branch (l, o, r) -> (match x with - | XI p -> Node (l, o, (vm_add default p v r)) - | XO p -> Node ((vm_add default p v l), o, r) - | XH -> Node (l, v, r)) + | XI p -> Branch (l, o, (vm_add default p v r)) + | XO p -> Branch ((vm_add default p v l), o, r) + | XH -> Branch (l, v, r)) type zWitness = z psatz @@ -1507,10 +1682,10 @@ let xnormalise0 t0 = | OpLt -> ((psub1 lhs0 rhs0),NonStrict)::[] | OpGt -> ((psub1 rhs0 lhs0),NonStrict)::[]) -(** val normalise : z formula -> z nFormula cnf **) +(** val normalise : z formula -> 'a1 -> (z nFormula, 'a1) cnf **) -let normalise t0 = - map (fun x -> x::[]) (xnormalise0 t0) +let normalise t0 tg = + map (fun x -> (x,tg)::[]) (xnormalise0 t0) (** val xnegate0 : z formula -> z nFormula list **) @@ -1530,10 +1705,10 @@ let xnegate0 t0 = | OpLt -> ((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))),NonStrict)::[] | OpGt -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::[]) -(** val negate : z formula -> z nFormula cnf **) +(** val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf **) -let negate t0 = - map (fun x -> x::[]) (xnegate0 t0) +let negate t0 tg = + map (fun x -> (x,tg)::[]) (xnegate0 t0) (** val zunsat : z nFormula -> bool **) @@ -1545,6 +1720,12 @@ let zunsat = let zdeduce = nformula_plus_nformula Z0 Z.add zeq_bool +(** val cnfZ : + (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 list **) + +let cnfZ f = + rxcnf zunsat zdeduce normalise negate true f + (** val ceiling : z -> z -> z **) let ceiling a b = @@ -1629,6 +1810,145 @@ let valid_cut_sign = function | NonStrict -> true | _ -> false +module Vars = + struct + type elt = positive + + type tree = PositiveSet.tree = + | Leaf + | Node of tree * bool * tree + + type t = tree + + (** val empty : t **) + + let empty = + Leaf + + (** val add : elt -> t -> t **) + + let rec add i = function + | Leaf -> + (match i with + | XI i0 -> Node (Leaf, false, (add i0 Leaf)) + | XO i0 -> Node ((add i0 Leaf), false, Leaf) + | XH -> Node (Leaf, true, Leaf)) + | Node (l, o, r) -> + (match i with + | XI i0 -> Node (l, o, (add i0 r)) + | XO i0 -> Node ((add i0 l), o, r) + | XH -> Node (l, true, r)) + + (** val singleton : elt -> t **) + + let singleton i = + add i empty + + (** val union : t -> t -> t **) + + let rec union m m' = + match m with + | Leaf -> m' + | Node (l, o, r) -> + (match m' with + | Leaf -> m + | Node (l', o', r') -> + Node ((union l l'), (if o then true else o'), (union r r'))) + + (** val rev_append : elt -> elt -> elt **) + + let rec rev_append y x = + match y with + | XI y0 -> rev_append y0 (XI x) + | XO y0 -> rev_append y0 (XO x) + | XH -> x + + (** val rev : elt -> elt **) + + let rev x = + rev_append x XH + + (** val xfold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> elt -> 'a1 **) + + let rec xfold f m v i = + match m with + | Leaf -> v + | Node (l, b, r) -> + if b + then xfold f r (f (rev i) (xfold f l v (XO i))) (XI i) + else xfold f r (xfold f l v (XO i)) (XI i) + + (** val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 **) + + let fold f m i = + xfold f m i XH + end + +(** val vars_of_pexpr : z pExpr -> Vars.t **) + +let rec vars_of_pexpr = function +| PEc _ -> Vars.empty +| PEX x -> Vars.singleton x +| PEadd (e1, e2) -> + let v1 = vars_of_pexpr e1 in let v2 = vars_of_pexpr e2 in Vars.union v1 v2 +| PEsub (e1, e2) -> + let v1 = vars_of_pexpr e1 in let v2 = vars_of_pexpr e2 in Vars.union v1 v2 +| PEmul (e1, e2) -> + let v1 = vars_of_pexpr e1 in let v2 = vars_of_pexpr e2 in Vars.union v1 v2 +| PEopp c -> vars_of_pexpr c +| PEpow (e0, _) -> vars_of_pexpr e0 + +(** val vars_of_formula : z formula -> Vars.t **) + +let vars_of_formula f = + let { flhs = l; fop = _; frhs = r } = f in + let v1 = vars_of_pexpr l in let v2 = vars_of_pexpr r in Vars.union v1 v2 + +(** val vars_of_bformula : (z formula, 'a1, 'a2, 'a3) gFormula -> Vars.t **) + +let rec vars_of_bformula = function +| A (a, _) -> vars_of_formula a +| Cj (f1, f2) -> + let v1 = vars_of_bformula f1 in + let v2 = vars_of_bformula f2 in Vars.union v1 v2 +| D (f1, f2) -> + let v1 = vars_of_bformula f1 in + let v2 = vars_of_bformula f2 in Vars.union v1 v2 +| N f0 -> vars_of_bformula f0 +| I (f1, _, f2) -> + let v1 = vars_of_bformula f1 in + let v2 = vars_of_bformula f2 in Vars.union v1 v2 +| _ -> Vars.empty + +(** val bound_var : positive -> z formula **) + +let bound_var v = + { flhs = (PEX v); fop = OpGe; frhs = (PEc Z0) } + +(** val mk_eq_pos : positive -> positive -> positive -> z formula **) + +let mk_eq_pos x y t0 = + { flhs = (PEX x); fop = OpEq; frhs = (PEsub ((PEX y), (PEX t0))) } + +(** val bound_vars : + (positive -> positive -> bool option -> 'a2) -> positive -> Vars.t -> (z + formula, 'a1, 'a2, 'a3) gFormula **) + +let bound_vars tag_of_var fr v = + Vars.fold (fun k acc -> + let y = XO (Coq_Pos.add fr k) in + let z0 = XI (Coq_Pos.add fr k) in + Cj ((Cj ((A ((mk_eq_pos k y z0), (tag_of_var fr k None))), (Cj ((A + ((bound_var y), (tag_of_var fr k (Some false)))), (A ((bound_var z0), + (tag_of_var fr k (Some true)))))))), acc)) v TT + +(** val bound_problem_fr : + (positive -> positive -> bool option -> 'a2) -> positive -> (z formula, + 'a1, 'a2, 'a3) gFormula -> (z formula, 'a1, 'a2, 'a3) gFormula **) + +let bound_problem_fr tag_of_var fr f = + let v = vars_of_bformula f in I ((bound_vars tag_of_var fr v), None, f) + (** val zChecker : z nFormula list -> zArithProof -> bool **) let rec zChecker l = function @@ -1675,7 +1995,8 @@ let rec zChecker l = function (** val zTautoChecker : z formula bFormula -> zArithProof list -> bool **) let zTautoChecker f w = - tauto_checker zunsat zdeduce normalise negate zChecker f w + tauto_checker zunsat zdeduce normalise negate (fun cl -> + zChecker (map fst cl)) f w type qWitness = q psatz @@ -1685,17 +2006,17 @@ let qWeakChecker = check_normalised_formulas { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus qmult qeq_bool qle_bool -(** val qnormalise : q formula -> q nFormula cnf **) +(** val qnormalise : q formula -> 'a1 -> (q nFormula, 'a1) cnf **) -let qnormalise = +let qnormalise t0 tg = cnf_normalise { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } - qplus qmult qminus qopp qeq_bool + qplus qmult qminus qopp qeq_bool t0 tg -(** val qnegate : q formula -> q nFormula cnf **) +(** val qnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf **) -let qnegate = +let qnegate t0 tg = cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus - qmult qminus qopp qeq_bool + qmult qminus qopp qeq_bool t0 tg (** val qunsat : q nFormula -> bool **) @@ -1713,10 +2034,17 @@ let normQ = norm { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus qmult qminus qopp qeq_bool +(** val cnfQ : + (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) cnf * 'a1 list **) + +let cnfQ f = + rxcnf qunsat qdeduce qnormalise qnegate true f + (** val qTautoChecker : q formula bFormula -> qWitness list -> bool **) let qTautoChecker f w = - tauto_checker qunsat qdeduce qnormalise qnegate qWeakChecker f w + tauto_checker qunsat qdeduce qnormalise qnegate (fun cl -> + qWeakChecker (map fst cl)) f w type rcst = | C0 @@ -1726,9 +2054,16 @@ type rcst = | CPlus of rcst * rcst | CMinus of rcst * rcst | CMult of rcst * rcst +| CPow of rcst * (z, nat) sum | CInv of rcst | COpp of rcst +(** val z_of_exp : (z, nat) sum -> z **) + +let z_of_exp = function +| Inl z1 -> z1 +| Inr n0 -> Z.of_nat n0 + (** val q_of_Rcst : rcst -> q **) let rec q_of_Rcst = function @@ -1739,6 +2074,7 @@ let rec q_of_Rcst = function | CPlus (r1, r2) -> qplus (q_of_Rcst r1) (q_of_Rcst r2) | CMinus (r1, r2) -> qminus (q_of_Rcst r1) (q_of_Rcst r2) | CMult (r1, r2) -> qmult (q_of_Rcst r1) (q_of_Rcst r2) +| CPow (r1, z0) -> qpower (q_of_Rcst r1) (z_of_exp z0) | CInv r0 -> qinv (q_of_Rcst r0) | COpp r0 -> qopp (q_of_Rcst r0) @@ -1750,17 +2086,17 @@ let rWeakChecker = check_normalised_formulas { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus qmult qeq_bool qle_bool -(** val rnormalise : q formula -> q nFormula cnf **) +(** val rnormalise : q formula -> 'a1 -> (q nFormula, 'a1) cnf **) -let rnormalise = +let rnormalise t0 tg = cnf_normalise { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } - qplus qmult qminus qopp qeq_bool + qplus qmult qminus qopp qeq_bool t0 tg -(** val rnegate : q formula -> q nFormula cnf **) +(** val rnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf **) -let rnegate = +let rnegate t0 tg = cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus - qmult qminus qopp qeq_bool + qmult qminus qopp qeq_bool t0 tg (** val runsat : q nFormula -> bool **) @@ -1775,5 +2111,5 @@ let rdeduce = (** val rTautoChecker : rcst formula bFormula -> rWitness list -> bool **) let rTautoChecker f w = - tauto_checker runsat rdeduce rnormalise rnegate rWeakChecker - (map_bformula (map_Formula q_of_Rcst) f) w + tauto_checker runsat rdeduce rnormalise rnegate (fun cl -> + rWeakChecker (map fst cl)) (map_bformula (map_Formula q_of_Rcst) f) w diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli index 72c2bf7da3..5de6caac0b 100644 --- a/plugins/micromega/micromega.mli +++ b/plugins/micromega/micromega.mli @@ -1,10 +1,23 @@ +type __ = Obj.t + +type unit0 = +| Tt + val negb : bool -> bool type nat = | O | S of nat +type ('a, 'b) sum = +| Inl of 'a +| Inr of 'b + +val fst : ('a1 * 'a2) -> 'a1 + +val snd : ('a1 * 'a2) -> 'a2 + val app : 'a1 list -> 'a1 list -> 'a1 list type comparison = @@ -16,6 +29,12 @@ val compOpp : comparison -> comparison val add : nat -> nat -> nat +val nth : nat -> 'a1 list -> 'a1 -> 'a1 + +val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list + +val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 + type positive = | XI of positive | XO of positive @@ -87,12 +106,6 @@ module N : val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 -val nth : nat -> 'a1 list -> 'a1 -> 'a1 - -val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list - -val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 - module Z : sig val double : z -> z @@ -125,6 +138,8 @@ module Z : val to_N : z -> n + val of_nat : nat -> z + val pos_div_eucl : positive -> z -> z * z val div_eucl : z -> z -> z * z @@ -163,27 +178,47 @@ 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 +val paddI : + ('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 +val psubI : + ('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 +val paddX : + '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 +val psubX : + '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 +val psub : + '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 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 +val pmulI : + '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 +val pmul : + '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 +val psquare : + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> + 'a1 pol -> 'a1 pol type 'c pExpr = | PEc of 'c @@ -197,49 +232,104 @@ 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 +val ppow_N : + '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 'a bFormula = +type ('tA, 'tX, 'aA, 'aF) gFormula = | TT | FF -| X -| A of 'a -| Cj of 'a bFormula * 'a bFormula -| D of 'a bFormula * 'a bFormula -| N of 'a bFormula -| I of 'a bFormula * 'a bFormula +| X of 'tX +| A of 'tA * 'aA +| Cj of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula +| D of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula +| N of ('tA, 'tX, 'aA, 'aF) gFormula +| I of ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option * ('tA, 'tX, 'aA, 'aF) gFormula + +val mapX : + ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) gFormula + +val foldA : ('a5 -> 'a3 -> 'a5) -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 + +val cons_id : 'a1 option -> 'a1 list -> 'a1 list + +val ids_of_formula : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list + +val collect_annot : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list + +type 'a bFormula = ('a, __, unit0, unit0) gFormula + +val map_bformula : + ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, 'a5) gFormula + +type ('x, 'annot) clause = ('x * 'annot) list + +type ('x, 'annot) cnf = ('x, 'annot) clause list + +val cnf_tt : ('a1, 'a2) cnf -val map_bformula : ('a1 -> 'a2) -> 'a1 bFormula -> 'a2 bFormula +val cnf_ff : ('a1, 'a2) cnf -type 'x clause = 'x list +val add_term : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> + ('a1, 'a2) clause option -type 'x cnf = 'x clause list +val or_clause : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) + clause -> ('a1, 'a2) clause option -val tt : 'a1 cnf +val or_clause_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf + -> ('a1, 'a2) cnf -val ff : 'a1 cnf +val or_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> + ('a1, 'a2) cnf -val add_term : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause -> 'a1 clause option +val and_cnf : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -val or_clause : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 clause -> 'a1 clause option +type ('term, 'annot, 'tX, 'aF) tFormula = ('term, 'tX, 'annot, 'aF) gFormula -val or_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 cnf -> 'a1 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 -val or_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 cnf -> 'a1 cnf -> 'a1 cnf +val radd_term : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> + (('a1, 'a2) clause, 'a2 list) sum -val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf +val ror_clause : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause + -> (('a1, 'a2) clause, 'a2 list) sum -val xcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf +val ror_clause_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause + list -> ('a1, 'a2) clause list * 'a2 list -val cnf_checker : ('a1 list -> 'a2 -> bool) -> 'a1 cnf -> 'a2 list -> bool +val ror_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list list -> ('a1, 'a2) + clause list -> ('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 + +val cnf_checker : + (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool val tauto_checker : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 bFormula -> 'a3 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 @@ -273,21 +363,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 + '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 +val nformula_plus_nformula : + '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_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 @@ -300,27 +396,31 @@ 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 +val psub0 : + '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 + '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 formula -> 'a1 - nFormula cnf + '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 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 - nFormula list + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> + ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list val cnf_negate : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 - nFormula cnf + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> + ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf val xdenorm : positive -> 'a1 pol -> 'a1 pExpr @@ -330,7 +430,15 @@ val map_PExpr : ('a2 -> 'a1) -> 'a2 pExpr -> 'a1 pExpr val map_Formula : ('a2 -> 'a1) -> 'a2 formula -> 'a1 formula -val simpl_cone : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz -> 'a1 psatz +val simpl_cone : + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz -> 'a1 psatz + +module PositiveSet : + sig + type tree = + | Leaf + | Node of tree * bool * tree + end type q = { qnum : z; qden : positive } @@ -358,8 +466,8 @@ val qpower : q -> z -> q type 'a t = | Empty -| Leaf of 'a -| Node of 'a t * 'a * 'a t +| Elt of 'a +| Branch of 'a t * 'a * 'a t val find : 'a1 -> 'a1 t -> positive -> 'a1 @@ -379,16 +487,18 @@ val normZ : z pExpr -> z pol val xnormalise0 : z formula -> z nFormula list -val normalise : z formula -> z nFormula cnf +val normalise : z formula -> 'a1 -> (z nFormula, 'a1) cnf val xnegate0 : z formula -> z nFormula list -val negate : z formula -> z nFormula cnf +val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf val zunsat : z nFormula -> bool val zdeduce : z nFormula -> z nFormula -> z nFormula option +val cnfZ : (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 list + val ceiling : z -> z -> z type zArithProof = @@ -415,6 +525,51 @@ val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option val valid_cut_sign : op1 -> bool +module Vars : + sig + type elt = positive + + type tree = PositiveSet.tree = + | Leaf + | Node of tree * bool * tree + + type t = tree + + val empty : t + + val add : elt -> t -> t + + val singleton : elt -> t + + val union : t -> t -> t + + val rev_append : elt -> elt -> elt + + val rev : elt -> elt + + val xfold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> elt -> 'a1 + + val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 + end + +val vars_of_pexpr : z pExpr -> Vars.t + +val vars_of_formula : z formula -> Vars.t + +val vars_of_bformula : (z formula, 'a1, 'a2, 'a3) gFormula -> Vars.t + +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 + +val bound_problem_fr : + (positive -> positive -> bool option -> 'a2) -> positive -> (z formula, 'a1, 'a2, + 'a3) gFormula -> (z formula, 'a1, 'a2, 'a3) gFormula + val zChecker : z nFormula list -> zArithProof -> bool val zTautoChecker : z formula bFormula -> zArithProof list -> bool @@ -423,9 +578,9 @@ type qWitness = q psatz val qWeakChecker : q nFormula list -> q psatz -> bool -val qnormalise : q formula -> q nFormula cnf +val qnormalise : q formula -> 'a1 -> (q nFormula, 'a1) cnf -val qnegate : q formula -> q nFormula cnf +val qnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf val qunsat : q nFormula -> bool @@ -433,6 +588,8 @@ val qdeduce : q nFormula -> q nFormula -> q nFormula option val normQ : q pExpr -> q pol +val cnfQ : (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) cnf * 'a1 list + val qTautoChecker : q formula bFormula -> qWitness list -> bool type rcst = @@ -443,18 +600,21 @@ type rcst = | CPlus of rcst * rcst | CMinus of rcst * rcst | CMult of rcst * rcst +| CPow of rcst * (z, nat) sum | CInv of rcst | COpp of rcst +val z_of_exp : (z, nat) sum -> z + val q_of_Rcst : rcst -> q type rWitness = q psatz val rWeakChecker : q nFormula list -> q psatz -> bool -val rnormalise : q formula -> q nFormula cnf +val rnormalise : q formula -> 'a1 -> (q nFormula, 'a1) cnf -val rnegate : q formula -> q nFormula cnf +val rnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf val runsat : q nFormula -> bool diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 809731ecc4..084ea39c27 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -19,8 +19,18 @@ (* *) (************************************************************************) +module Int = struct + type t = int + let compare : int -> int -> int = Pervasives.compare + let equal : int -> int -> bool = (=) +end -module ISet = Set.Make(Int) +module ISet = + struct + include Set.Make(Int) + + let pp o s = iter (fun i -> Printf.fprintf o "%i " i) s + end module IMap = struct @@ -82,12 +92,69 @@ let extract pred l = | _ -> (fd, e::sys) ) (None,[]) l +let extract_best red lt l = + let rec extractb c e rst l = + match l with + [] -> Some (c,e) , rst + | e'::l' -> match red e' with + | None -> extractb c e (e'::rst) l' + | Some c' -> if lt c' c + then extractb c' e' (e::rst) l' + else extractb c e (e'::rst) l' in + match extract red l with + | None , _ -> None,l + | Some(c,e), rst -> extractb c e [] rst + + +let rec find_some pred l = + match l with + | [] -> None + | e::l -> match pred e with + | Some r -> Some r + | None -> find_some pred l + + let extract_all pred l = List.fold_left (fun (s1,s2) e -> match pred e with | None -> s1,e::s2 | Some v -> (v,e)::s1 , s2) ([],[]) l +let simplify f sys = + let (sys',b) = + List.fold_left (fun (sys',b) c -> + match f c with + | None -> (c::sys',b) + | Some c' -> + (c'::sys',true) + ) ([],false) sys in + if b then Some sys' else None + +let generate_acc f acc sys = + List.fold_left (fun sys' c -> match f c with + | None -> sys' + | Some c' -> c'::sys' + ) acc sys + + +let generate f sys = generate_acc f [] sys + + +let saturate p f sys = + let rec sat acc l = + match extract p l with + | None,_ -> acc + | Some r,l' -> + let n = generate (f r) (l'@acc) in + sat (n@acc) l' in + try sat [] sys with + x -> + begin + Printexc.print_backtrace stdout ; + raise x + end + + open Num open Big_int @@ -276,7 +343,8 @@ sig val next : t -> t val pp : out_channel -> t -> unit val compare : t -> t -> int - + val max : t -> t -> t + val to_int : t -> int end module Tag : Tag = @@ -286,8 +354,10 @@ struct let from i = i let next i = i + 1 + let max : int -> int -> int = Pervasives.max let pp o i = output_string o (string_of_int i) let compare : int -> int -> int = Int.compare + let to_int x = x end diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli index e92f086886..739d1a73da 100644 --- a/plugins/micromega/mutils.mli +++ b/plugins/micromega/mutils.mli @@ -8,8 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +module Int : sig type t = int val compare : int -> int -> int val equal : int -> int -> bool end -module ISet : Set.S with type elt = int + +module ISet : sig + include Set.S with type elt = int + val pp : out_channel -> t -> unit +end module IMap : sig @@ -36,7 +41,9 @@ module Tag : sig val pp : out_channel -> t -> unit val next : t -> t + val max : t -> t -> t val from : int -> t + val to_int : t -> int end @@ -78,8 +85,18 @@ val extract : ('a -> 'b option) -> 'a list -> ('b * 'a) option * 'a list val extract_all : ('a -> 'b option) -> 'a list -> ('b * 'a) list * 'a list +val extract_best : ('a -> 'b option) -> ('b -> 'b -> bool) -> 'a list -> ('b *'a) option * 'a list + +val find_some : ('a -> 'b option) -> 'a list -> 'b option + val iterate_until_stable : ('a -> 'a option) -> 'a -> 'a +val simplify : ('a -> 'a option) -> 'a list -> 'a list option + +val saturate : ('a -> 'b option) -> ('b * 'a -> 'a -> 'a option) -> 'a list -> 'a list + +val generate : ('a -> 'b option) -> 'a list -> 'b list + val app_funs : ('a -> 'b option) list -> 'a -> 'b option val command : string -> string array -> 'a -> 'b diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index 76e7769e82..d406560fb8 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -378,6 +378,7 @@ module LinPoly = struct let pp o p = Vect.pp_gen pp_var o p + let constant c = if sign_num c = 0 then Vect.null @@ -389,6 +390,12 @@ module LinPoly = struct let mn = (MonT.retrieve v) in Monomial.is_var mn || Monomial.is_const mn) p + let is_variable p = + let ((x,v),r) = Vect.decomp_fst p in + if Vect.is_null r && v >/ Int 0 + then Monomial.get_var (MonT.retrieve x) + else None + let factorise x p = let (px,cx) = Poly.factorise x (pol_of_linpol p) in @@ -399,20 +406,6 @@ module LinPoly = struct let (a,b) = factorise x p in Vect.is_constant a - let search_linear p l = - - Vect.find (fun x v -> - if p v - then - let x' = MonT.retrieve x in - match Monomial.get_var x' with - | None -> None - | Some x -> if is_linear_for x l - then Some x - else None - else None) l - - let search_all_linear p l = Vect.fold (fun acc x v -> if p v @@ -426,12 +419,24 @@ module LinPoly = struct else acc else acc) [] l + let min_list (l:int list) = + match l with + | [] -> None + | e::l -> Some (List.fold_left Pervasives.min e l) + + let search_linear p l = + min_list (search_all_linear p l) + let product p1 p2 = linpol_of_pol (Poly.product (pol_of_linpol p1) (pol_of_linpol p2)) let addition p1 p2 = Vect.add p1 p2 + + let of_vect v = + Vect.fold (fun acc v vl -> addition (product (var v) (constant vl)) acc) Vect.null v + let variables p = Vect.fold (fun acc v _ -> ISet.union (Monomial.variables (MonT.retrieve v)) acc) ISet.empty p @@ -489,8 +494,8 @@ module ProofFormat = struct | Cst c -> Printf.fprintf o "Cst %s" (string_of_num c) | Zero -> Printf.fprintf o "Zero" | Square s -> Printf.fprintf o "(%a)^2" Poly.pp (LinPoly.pol_of_linpol s) - | MulC(p,pr) -> Printf.fprintf o "(%a) * %a" Poly.pp (LinPoly.pol_of_linpol p) output_prf_rule pr - | MulPrf(p1,p2) -> Printf.fprintf o "%a * %a" output_prf_rule p1 output_prf_rule p2 + | MulC(p,pr) -> Printf.fprintf o "(%a) * (%a)" Poly.pp (LinPoly.pol_of_linpol p) output_prf_rule pr + | MulPrf(p1,p2) -> Printf.fprintf o "(%a) * (%a)" output_prf_rule p1 output_prf_rule p2 | AddPrf(p1,p2) -> Printf.fprintf o "%a + %a" output_prf_rule p1 output_prf_rule p2 | CutPrf(p) -> Printf.fprintf o "[%a]" output_prf_rule p | Gcd(c,p) -> Printf.fprintf o "(%a)/%s" output_prf_rule p (string_of_big_int c) @@ -502,6 +507,18 @@ module ProofFormat = struct output_prf_rule p1 Vect.pp v output_prf_rule p2 (pp_list ";" output_proof) pl + let rec pr_size = function + | Annot(_,p) -> pr_size p + | Zero| Square _ -> Int 0 + | Hyp _ -> Int 1 + | Def _ -> Int 1 + | Cst n -> n + | Gcd(i, p) -> pr_size p // (Big_int i) + | MulPrf(p1,p2) | AddPrf(p1,p2) -> pr_size p1 +/ pr_size p2 + | CutPrf p -> pr_size p + | MulC(v, p) -> pr_size p + + let rec pr_rule_max_id = function | Annot(_,p) -> pr_rule_max_id p | Hyp i | Def i -> i @@ -613,6 +630,48 @@ module ProofFormat = struct if debug then Printf.printf "normalise_proof %a -> %a" output_proof prf output_proof (snd res) ; res + module OrdPrfRule = + struct + type t = prf_rule + + let id_of_constr = function + | Annot _ -> 0 + | Hyp _ -> 1 + | Def _ -> 2 + | Cst _ -> 3 + | Zero -> 4 + | Square _ -> 5 + | MulC _ -> 6 + | Gcd _ -> 7 + | MulPrf _ -> 8 + | AddPrf _ -> 9 + | CutPrf _ -> 10 + + let cmp_pair c1 c2 (x1,x2) (y1,y2) = + match c1 x1 y1 with + | 0 -> c2 x2 y2 + | i -> i + + + let rec compare p1 p2 = + match p1, p2 with + | Annot(s1,p1) , Annot(s2,p2) -> if s1 = s2 then compare p1 p2 + else Pervasives.compare s1 s2 + | Hyp i , Hyp j -> Pervasives.compare i j + | Def i , Def j -> Pervasives.compare i j + | Cst n , Cst m -> Num.compare_num n m + | Zero , Zero -> 0 + | Square v1 , Square v2 -> Vect.compare v1 v2 + | MulC(v1,p1) , MulC(v2,p2) -> cmp_pair Vect.compare compare (v1,p1) (v2,p2) + | Gcd(b1,p1) , Gcd(b2,p2) -> cmp_pair Big_int.compare_big_int compare (b1,p1) (b2,p2) + | MulPrf(p1,q1) , MulPrf(p2,q2) -> cmp_pair compare compare (p1,q1) (p2,q2) + | AddPrf(p1,q1) , MulPrf(p2,q2) -> cmp_pair compare compare (p1,q1) (p2,q2) + | CutPrf p , CutPrf p' -> compare p p' + | _ , _ -> Pervasives.compare (id_of_constr p1) (id_of_constr p2) + + end + + let add_proof x y = @@ -621,23 +680,91 @@ module ProofFormat = struct | _ -> AddPrf(x,y) - let mul_cst_proof c p = - match sign_num c with - | 0 -> Zero (* This is likely to be a bug *) - | -1 -> MulC(LinPoly.constant c,p) (* [p] should represent an equality *) - | 1 -> - if eq_num (Int 1) c - then p - else MulPrf(Cst c,p) - | _ -> assert false + let rec mul_cst_proof c p = + match p with + | Annot(s,p) -> Annot(s,mul_cst_proof c p) + | MulC(v,p') -> MulC(Vect.mul c v,p') + | _ -> + match sign_num c with + | 0 -> Zero (* This is likely to be a bug *) + | -1 -> MulC(LinPoly.constant c, p) (* [p] should represent an equality *) + | 1 -> + if eq_num (Int 1) c + then p + else MulPrf(Cst c,p) + | _ -> assert false + + + let sMulC v p = + let (c,v') = Vect.decomp_cst v in + if Vect.is_null v' then mul_cst_proof c p + else MulC(v,p) let mul_proof p1 p2 = match p1 , p2 with | Zero , _ | _ , Zero -> Zero - | Cst (Int 1) , p | p , Cst (Int 1) -> p - | _ , _ -> MulPrf(p1,p2) + | Cst c , p | p , Cst c -> mul_cst_proof c p + | _ , _ -> + MulPrf(p1,p2) + + module PrfRuleMap = Map.Make(OrdPrfRule) + + let prf_rule_of_map m = + PrfRuleMap.fold (fun k v acc -> add_proof (sMulC v k) acc) m Zero + + + let rec dev_prf_rule p = + match p with + | Annot(s,p) -> dev_prf_rule p + | Hyp _ | Def _ | Cst _ | Zero | Square _ -> PrfRuleMap.singleton p (LinPoly.constant (Int 1)) + | MulC(v,p) -> PrfRuleMap.map (fun v1 -> LinPoly.product v v1) (dev_prf_rule p) + | AddPrf(p1,p2) -> PrfRuleMap.merge (fun k o1 o2 -> + match o1 , o2 with + | None , None -> None + | None , Some v | Some v, None -> Some v + | Some v1 , Some v2 -> Some (LinPoly.addition v1 v2)) (dev_prf_rule p1) (dev_prf_rule p2) + | MulPrf(p1, p2) -> + begin + let p1' = dev_prf_rule p1 in + let p2' = dev_prf_rule p2 in + + let p1'' = prf_rule_of_map p1' in + let p2'' = prf_rule_of_map p2' in + + match p1'' with + | Cst c -> PrfRuleMap.map (fun v1 -> Vect.mul c v1) p2' + | _ -> PrfRuleMap.singleton (MulPrf(p1'',p2'')) (LinPoly.constant (Int 1)) + end + | _ -> PrfRuleMap.singleton p (LinPoly.constant (Int 1)) + + let simplify_prf_rule p = + prf_rule_of_map (dev_prf_rule p) + + + (* + let mul_proof p1 p2 = + let res = mul_proof p1 p2 in + Printf.printf "mul_proof %a %a = %a\n" + output_prf_rule p1 output_prf_rule p2 output_prf_rule res; res + + let add_proof p1 p2 = + let res = add_proof p1 p2 in + Printf.printf "add_proof %a %a = %a\n" + output_prf_rule p1 output_prf_rule p2 output_prf_rule res; res + + + let sMulC v p = + let res = sMulC v p in + Printf.printf "sMulC %a %a = %a\n" Vect.pp v output_prf_rule p output_prf_rule res ; + res + + let mul_cst_proof c p = + let res = mul_cst_proof c p in + Printf.printf "mul_cst_proof %s %a = %a\n" (Num.string_of_num c) output_prf_rule p output_prf_rule res ; + res + *) let proof_of_farkas env vect = Vect.fold (fun prf x n -> @@ -645,6 +772,7 @@ module ProofFormat = struct + module Env = struct let rec string_of_int_list l = @@ -768,10 +896,14 @@ module WithProof = struct let output o ((lp,op),prf) = Printf.fprintf o "%a %s 0 by %a\n" LinPoly.pp lp (string_of_op op) ProofFormat.output_prf_rule prf + let output_sys o l = + List.iter (Printf.fprintf o "%a\n" output) l + exception InvalidProof let zero = ((Vect.null,Eq), ProofFormat.Zero) + let const n = ((LinPoly.constant n,Ge), ProofFormat.Cst n) let of_cstr (c,prf) = (Vect.set 0 (Num.minus_num (c.cst)) c.coeffs,c.op), prf @@ -784,7 +916,7 @@ module WithProof = struct let mult p ((p1,o1),prf1) = match o1 with - | Eq -> ((LinPoly.product p p1,o1), ProofFormat.MulC(p, prf1)) + | Eq -> ((LinPoly.product p p1,o1), ProofFormat.sMulC p prf1) | Gt| Ge -> let (n,r) = Vect.decomp_cst p in if Vect.is_null r && n >/ Int 0 then ((LinPoly.product p p1, o1), ProofFormat.mul_cst_proof n prf1) @@ -890,6 +1022,51 @@ module WithProof = struct end | (Ge|Gt) , Eq -> failwith "pivot: equality as second argument" + let linear_pivot sys ((lp1,op1), prf1) x ((lp2,op2), prf2) = + match linear_pivot sys ((lp1,op1), prf1) x ((lp2,op2), prf2) with + | None -> None + | Some (c,p) -> Some(c, ProofFormat.simplify_prf_rule p) + + +let is_substitution strict ((p,o),prf) = + let pred v = if strict then v =/ Int 1 || v =/ Int (-1) else true in + + match o with + | Eq -> LinPoly.search_linear pred p + | _ -> None + + +let subst1 sys0 = + let (oeq,sys') = extract (is_substitution true) sys0 in + match oeq with + | None -> sys0 + | Some(v,pc) -> + match simplify (linear_pivot sys0 pc v) sys' with + | None -> sys0 + | Some sys' -> sys' + + + +let subst sys0 = + let elim sys = + let (oeq,sys') = extract (is_substitution true) sys in + match oeq with + | None -> None + | Some(v,pc) -> simplify (linear_pivot sys0 pc v) sys' in + + iterate_until_stable elim sys0 + + +let saturate_subst b sys0 = + let select = is_substitution b in + let gen (v,pc) ((c,op),prf) = + if ISet.mem v (LinPoly.variables c) + then linear_pivot sys0 pc v ((c,op),prf) + else None + in + saturate select gen sys0 + + end diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli index 23f3470d77..b5c6fefbb5 100644 --- a/plugins/micromega/polynomial.mli +++ b/plugins/micromega/polynomial.mli @@ -28,6 +28,8 @@ module Monomial : sig @return the empty monomial i.e. without any variable *) val const : t + val is_const : t -> bool + (** [var x] @return the monomial x^1 *) val var : var -> t @@ -40,6 +42,11 @@ module Monomial : sig @return [true] iff m = x^1 for some variable x *) val is_var : t -> bool + (** [get_var m] + @return [x] iff m = x^1 for variable x *) + val get_var : t -> var option + + (** [div m1 m2] @return a pair [mr,n] such that mr * (m2)^n = m1 where n is maximum *) val div : t -> t -> t * int @@ -141,6 +148,10 @@ module LinPoly : sig @return the monomial corresponding to the variable [x] *) val retrieve : int -> Monomial.t + (** [register m] + @return the variable index for the monomial m *) + val register : Monomial.t -> int + end (** [linpol_of_pol p] linearise the polynomial p *) @@ -161,11 +172,21 @@ module LinPoly : sig @returns 1.x where x is the variable (index) for monomial m *) val of_monomial : Monomial.t -> t + (** [of_vect v] + @returns a1.x1 + ... + an.xn + This is not the identity because xi is the variable index of xi^1 + *) + val of_vect : Vect.t -> t + (** [variables p] @return the set of variables of the polynomial p interpreted as a multi-variate polynomial *) val variables : t -> ISet.t + (** [is_variable p] + @return Some x if p = a.x for a >= 0 *) + val is_variable : t -> var option + (** [is_linear p] @return whether the multi-variate polynomial is linear. *) val is_linear : t -> bool @@ -245,6 +266,8 @@ module ProofFormat : sig | Step of int * prf_rule * proof | Enum of int * prf_rule * Vect.t * prf_rule * proof list + val pr_size : prf_rule -> Num.num + val pr_rule_max_id : prf_rule -> int val proof_max_id : proof -> int @@ -294,9 +317,14 @@ sig (** [out_channel chan c] pretty-prints the constraint [c] over the channel [chan] *) val output : out_channel -> t -> unit + val output_sys : out_channel -> t list -> unit + (** [zero] represents the tautology (0=0) *) val zero : t + (** [const n] represents the tautology (n>=0) *) + val const : Num.num -> t + (** [product p q] @return the polynomial p*q with its sign and proof *) val product : t -> t -> t @@ -321,4 +349,24 @@ sig *) val linear_pivot : t list -> t -> Vect.var -> t -> t option + +(** [subst sys] performs the equivalent of the 'subst' tactic of Coq. + For every p=0 \in sys such that p is linear in x with coefficient +/- 1 + i.e. p = 0 <-> x = e and x \notin e. + Replace x by e in sys + + NB: performing this transformation may hinders the non-linear prover to find a proof. + [elim_simple_linear_equality] is much more careful. + *) + + val subst : t list -> t list + + (** [subst1 sys] performs a single substitution *) + val subst1 : t list -> t list + + val saturate_subst : bool -> t list -> t list + + + val is_substitution : bool -> t -> var option + end diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml index 4465aa1ee1..4ddeb6c2c0 100644 --- a/plugins/micromega/simplex.ml +++ b/plugins/micromega/simplex.ml @@ -11,9 +11,11 @@ (** A naive simplex *) open Polynomial open Num -open Util +(*open Util*) open Mutils +type ('a,'b) sum = Inl of 'a | Inr of 'b + let debug = false type iset = unit IMap.t @@ -130,12 +132,6 @@ let is_maximised rst v = violating a restriction. *) -(* let is_unbounded rst tbl vr = - IMap.for_all (fun x v -> if Vect.get vr v </ Int 0 - then not (IMap.mem vr rst) - else true - ) tbl - *) type result = | Max of num (** Maximum is reached *) @@ -335,6 +331,8 @@ let normalise_row (t : tableau) (v: Vect.t) = let add_row (nw :var) (t : tableau) (v : Vect.t) : tableau = IMap.add nw (normalise_row t v) t + + (** [push_real] performs reasoning over the rationals *) let push_real (opt : bool) (nw : var) (v : Vect.t) (rst: Restricted.t) (t : tableau) : certificate = if debug @@ -361,7 +359,7 @@ let push_real (opt : bool) (nw : var) (v : Vect.t) (rst: Restricted.t) (t : tabl Unsat (Vect.set nw (Int 1) (Vect.set 0 (Int 0) (Vect.mul (Int (-1)) v'))) -(** One complication is that equalities needs some pre-processing.contents +(** One complication is that equalities needs some pre-processing. *) open Mutils open Polynomial @@ -406,25 +404,21 @@ let find_solution rst tbl = let choose_conflict (sol:Vect.t) (l: (var * Vect.t) list) = let esol = Vect.set 0 (Int 1) sol in - let is_conflict (x,v) = - if Vect.dotproduct esol v >=/ Int 0 - then None else Some(x,v) in - let (c,r) = extract is_conflict l in - match c with - | Some (c,_) -> Some (c,r) - | None -> match l with - | [] -> None - | e::l -> Some(e,l) - -(*let remove_redundant rst t = - IMap.fold (fun k v m -> if Restricted.is_restricted k rst && Vect.for_all (fun x _ -> x == 0 || Restricted.is_restricted x rst) v - then begin - if debug then - Printf.printf "%a is redundant\n" LinPoly.pp_var k; - IMap.remove k m - end - else m) t t - *) + + let rec most_violating l e (x,v) rst = + match l with + | [] -> Some((x,v),rst) + | (x',v')::l -> + let e' = Vect.dotproduct esol v' in + if e' <=/ e + then most_violating l e' (x',v') ((x,v)::rst) + else most_violating l e (x,v) ((x',v')::rst) in + + match l with + | [] -> None + | (x,v)::l -> let e = Vect.dotproduct esol v in + most_violating l e (x,v) [] + let rec solve opt l (rst:Restricted.t) (t:tableau) = @@ -515,65 +509,117 @@ let make_farkas_proof (env: WithProof.t IMap.t) vm v = WithProof.mult (Vect.cst n) (IMap.find x env) end) WithProof.zero v -(* -let incr_cut rmin x = - match rmin with - | None -> true - | Some r -> Int.compare x r = 1 - *) -let cut env rmin sol vm (rst:Restricted.t) (x,v) = -(* if not (incr_cut rmin x) - then None - else *) - let (n,r) = Vect.decomp_cst v in +let frac_num n = n -/ Num.floor_num n - let nf = Num.floor_num n in - if nf =/ n + +(* [resolv_var v rst tbl] returns (if it exists) a restricted variable vr such that v = vr *) +exception FoundVar of int + +let resolve_var v rst tbl = + let v = Vect.set v (Int 1) Vect.null in + try + IMap.iter (fun k vect -> + if Restricted.is_restricted k rst + then if Vect.equal v vect then raise (FoundVar k) + else ()) tbl ; None + with FoundVar k -> Some k + +let prepare_cut env rst tbl x v = + (* extract the unrestricted part *) + let (unrst,rstv) = Vect.partition (fun x vl -> not (Restricted.is_restricted x rst) && frac_num vl <>/ Int 0) (Vect.set 0 (Int 0) v) in + if Vect.is_null unrst + then Some rstv + else Some (Vect.fold (fun acc k i -> + match resolve_var k rst tbl with + | None -> acc (* Should not happen *) + | Some v' -> Vect.set v' i acc) + rstv unrst) + +let cut env rmin sol vm (rst:Restricted.t) tbl (x,v) = + begin + (* Printf.printf "Trying to cut %i\n" x;*) + let (n,r) = Vect.decomp_cst v in + + + let f = frac_num n in + + if f =/ Int 0 then None (* The solution is integral *) else (* This is potentially a cut *) - let cut = Vect.normalise - (Vect.fold (fun acc x n -> - if Restricted.is_restricted x rst then - Vect.set x (n -/ (Num.floor_num n)) acc - else acc - ) Vect.null r) in - if debug then Printf.fprintf stdout "Cut vector for %a : %a\n" LinPoly.pp_var x LinPoly.pp cut ; - let cut = make_farkas_proof env vm cut in - - match WithProof.cutting_plane cut with - | None -> None - | Some (v,prf) -> - if debug then begin - Printf.printf "This is a cutting plane:\n" ; - Printf.printf "%a -> %a\n" WithProof.output cut WithProof.output (v,prf); - end; - if Pervasives.(=) (snd v) Eq - then (* Unsat *) Some (x,(v,prf)) - else if eval_op Ge (Vect.dotproduct (fst v) (Vect.set 0 (Int 1) sol)) (Int 0) - then begin - (* Can this happen? *) - if debug then Printf.printf "The cut is feasible - drop it\n"; - None - end - else Some(x,(v,prf)) - -let find_cut env u sol vm rst tbl = - (* find first *) - IMap.fold (fun x v acc -> - match acc with - | None -> cut env u sol vm rst (x,v) - | Some c -> acc) tbl None - -(* -let find_cut env u sol vm rst tbl = - IMap.fold (fun x v acc -> - match acc with - | Some c -> Some c - | None -> cut env u sol vm rst (x,v) - ) tbl None - *) + let t = + if f </ (Int 1) // (Int 2) + then + let t' = ((Int 1) // f) in + if Num.is_integer_num t' + then t' -/ Int 1 + else Num.floor_num t' + else Int 1 in + + let cut_coeff1 v = + let fv = frac_num v in + if fv <=/ (Int 1 -/ f) + then fv // (Int 1 -/ f) + else (Int 1 -/ fv) // f in + + let cut_coeff2 v = frac_num (t */ v) in + + let cut_vector ccoeff = + match prepare_cut env rst tbl x v with + | None -> Vect.null + | Some r -> + (*Printf.printf "Potential cut %a\n" LinPoly.pp r;*) + Vect.fold (fun acc x n -> Vect.set x (ccoeff n) acc) Vect.null r + in + + let lcut = List.map (fun cv -> Vect.normalise (cut_vector cv)) [cut_coeff1 ; cut_coeff2] in + + let lcut = List.map (make_farkas_proof env vm) lcut in + + let check_cutting_plane c = + match WithProof.cutting_plane c with + | None -> + if debug then Printf.printf "This is not cutting plane for %a\n%a:" LinPoly.pp_var x WithProof.output c; + None + | Some(v,prf) -> + if debug then begin + Printf.printf "This is a cutting plane for %a:" LinPoly.pp_var x; + Printf.printf " %a\n" WithProof.output (v,prf); + end; + if Pervasives.(=) (snd v) Eq + then (* Unsat *) Some (x,(v,prf)) + else + let vl = (Vect.dotproduct (fst v) (Vect.set 0 (Int 1) sol)) in + if eval_op Ge vl (Int 0) + then begin + (* Can this happen? *) + if debug then Printf.printf "The cut is feasible %s >= 0 ??\n" (Num.string_of_num vl); + None + end + else Some(x,(v,prf)) in + + find_some check_cutting_plane lcut + end + +let find_cut nb env u sol vm rst tbl = + if nb = 0 + then + IMap.fold (fun x v acc -> + match acc with + | None -> cut env u sol vm rst tbl (x,v) + | Some c -> Some c) tbl None + else + IMap.fold (fun x v acc -> + match cut env u sol vm rst tbl (x,v) , acc with + | None , Some r | Some r , None -> Some r + | None , None -> None + | Some (v,((lp,o),p1)) , Some (v',((lp',o'),p2)) -> + Some (if ProofFormat.pr_size p1 </ ProofFormat.pr_size p2 + then (v,((lp,o),p1)) else (v',((lp',o'),p2))) + ) tbl None + + let integer_solver lp = let (l,_) = List.split lp in @@ -587,7 +633,10 @@ let integer_solver lp = | Sat (t',x) -> Inl (Restricted.restrict vr rst,t',x) | Unsat c -> Inr c in + let nb = ref 0 in + let rec isolve env cr vr res = + incr nb; match res with | Inr c -> Some (Step (vr, make_farkas_certificate env vm (Vect.normalise c),Done)) | Inl (rst,tbl,x) -> @@ -595,10 +644,11 @@ let integer_solver lp = Printf.fprintf stdout "Looking for a cut\n"; Printf.fprintf stdout "Restricted %a ...\n" Restricted.pp rst; Printf.fprintf stdout "Current Tableau\n%a\n" output_tableau tbl; + (* Printf.fprintf stdout "Bounding box\n%a\n" output_box (bounding_box (vr+1) rst tbl l')*) end; let sol = find_solution rst tbl in - match find_cut env cr (*x*) sol vm rst tbl with + match find_cut (!nb mod 2) env cr (*x*) sol vm rst tbl with | None -> None | Some(cr,((v,op),cut)) -> if Pervasives.(=) op Eq @@ -615,6 +665,8 @@ let integer_solver lp = isolve env None vr res let integer_solver lp = + if debug then Printf.printf "Input integer solver\n%a\n" WithProof.output_sys (List.map WithProof.of_cstr lp); + match integer_solver lp with | None -> None | Some prf -> if debug diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml index b188ab4278..b80d5536eb 100644 --- a/plugins/micromega/vect.ml +++ b/plugins/micromega/vect.ml @@ -54,6 +54,17 @@ let pp_var_num pp_var o (v,n) = | Int 0 -> () | _ -> Printf.fprintf o "%s*%a" (string_of_num n) pp_var v +let pp_var_num_smt pp_var o (v,n) = + if Int.equal v 0 + then if eq_num (Int 0) n then () + else Printf.fprintf o "%s" (string_of_num n) + else + match n with + | Int 1 -> pp_var o v + | Int -1 -> Printf.fprintf o "(- %a)" pp_var v + | Int 0 -> () + | _ -> Printf.fprintf o "(* %s %a)" (string_of_num n) pp_var v + let rec pp_gen pp_var o v = match v with @@ -66,6 +77,9 @@ let pp_var o v = Printf.fprintf o "x%i" v let pp o v = pp_gen pp_var o v +let pp_smt o v = + let list o v = List.iter (fun e -> Printf.fprintf o "%a " (pp_var_num_smt pp_var) e) v in + Printf.fprintf o "(+ %a)" list v let from_list (l: num list) = let rec xfrom_list i l = @@ -222,6 +236,19 @@ let decomp_cst v = | (0,vl)::v -> vl,v | _ -> Int 0,v +let rec decomp_at i v = + match v with + | [] -> (Int 0 , null) + | (vr,vl)::r -> if i = vr then (vl,r) + else if i < vr then (Int 0,v) + else decomp_at i r + +let decomp_fst v = + match v with + | [] -> ((0,Int 0),[]) + | x::v -> (x,v) + + let fold f acc v = List.fold_left (fun acc (v,i) -> f acc v i) acc v @@ -293,3 +320,19 @@ let dotproduct v1 v2 = then dot acc v1' v2 else dot acc v1 v2' in dot (Int 0) v1 v2 + + +let map f v = List.map (fun (x,v) -> f x v) v + +let abs_min_elt v = + match v with + | [] -> None + | (v,vl)::r -> + Some (List.fold_left (fun (v1,vl1) (v2,vl2) -> + if abs_num vl1 </ abs_num vl2 + then (v1,vl1) else (v2,vl2) ) (v,vl) r) + + +let partition p = List.partition (fun (vr,vl) -> p vr vl) + +let mkvar x = set x (Int 1) null diff --git a/plugins/micromega/vect.mli b/plugins/micromega/vect.mli index da6b1e8e9b..4c9b140aad 100644 --- a/plugins/micromega/vect.mli +++ b/plugins/micromega/vect.mli @@ -40,6 +40,9 @@ val pp_gen : (out_channel -> var -> unit) -> out_channel -> t -> unit (** [pp o v] prints the representation of the vector [v] over the channel [o] *) val pp : out_channel -> t -> unit +(** [pp_smt o v] prints the representation of the vector [v] over the channel [o] using SMTLIB conventions *) +val pp_smt : out_channel -> t -> unit + (** [variables v] returns the set of variables with non-zero coefficients *) val variables : t -> ISet.t @@ -49,6 +52,11 @@ val get_cst : t -> num (** [decomp_cst v] returns the pair (c,a1.x1+...+an.xn) *) val decomp_cst : t -> num * t +(** [decomp_cst v] returns the pair (ai, ai+1.xi+...+an.xn) *) +val decomp_at : int -> t -> num * t + +val decomp_fst : t -> (var * num) * t + (** [cst c] returns the vector v=c+0.x1+...+0.xn *) val cst : num -> t @@ -70,10 +78,13 @@ val get : var -> t -> num i.e. the coefficient of the variable xi is set to ai' *) val set : var -> num -> t -> t +(** [mkvar xi] returns 1.xi *) +val mkvar : var -> t + (** [update xi f v] returns c+a1.x1+...+f(ai).xi+...+an.xn *) val update : var -> (num -> num) -> t -> t -(** [fresh v] return the fresh variable with inded 1+ max (variables v) *) +(** [fresh v] return the fresh variable with index 1+ max (variables v) *) val fresh : t -> int (** [choose v] decomposes a vector [v] depending on whether it is [null] or not. @@ -154,3 +165,9 @@ val exists2 : (num -> num -> bool) -> t -> t -> (var * num * num) option (** [dotproduct v1 v2] is the dot product of v1 and v2. *) val dotproduct : t -> t -> num + +val map : (var -> num -> 'a) -> t -> 'a list + +val abs_min_elt : t -> (var * num) option + +val partition : (var -> num -> bool) -> t -> t * t diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex b85258505b..e0324b0232 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache diff --git a/test-suite/micromega/example_nia.v b/test-suite/micromega/example_nia.v index 8de631aa6a..485c24f0c9 100644 --- a/test-suite/micromega/example_nia.v +++ b/test-suite/micromega/example_nia.v @@ -435,6 +435,12 @@ Goal forall (R : sz + d * sz - sz * x >= 1), False. Proof. + (* Manual proof. + assert (H : sz >= 2) by GE + R. + assert (GEd : x - d >= 1 by GE / H + assert (Rd : 1 + d - x >= 1 by R / H) + 1 >= 2 by GEd + Rd + *) intros. assert (x - d >= 1) by nia. nia. diff --git a/test-suite/micromega/rsyntax.v b/test-suite/micromega/rsyntax.v new file mode 100644 index 0000000000..02b98b562f --- /dev/null +++ b/test-suite/micromega/rsyntax.v @@ -0,0 +1,75 @@ +Require Import ZArith. +Require Import Lra. +Require Import Reals. + +Goal (1 / (1 - 1) = 0)%R. + Fail lra. (* division by zero *) +Abort. + +Goal (0 / (1 - 1) = 0)%R. + lra. (* 0 * x = 0 *) +Qed. + +Goal (10 ^ 2 = 100)%R. + lra. (* pow is reified as a constant *) +Qed. + +Goal (2 / (1/2) ^ 2 = 8)%R. + lra. (* pow is reified as a constant *) +Qed. + + +Goal ( IZR (Z.sqrt 4) = 2)%R. +Proof. + Fail lra. +Abort. + +Require Import DeclConstant. + +Instance Dsqrt : DeclaredConstant Z.sqrt := {}. + +Goal ( IZR (Z.sqrt 4) = 2)%R. +Proof. + lra. +Qed. + +Require Import QArith. +Require Import Qreals. + +Goal (Q2R (1 # 2) = 1/2)%R. +Proof. + lra. +Qed. + +Goal ( 1 ^ (2 + 2) = 1)%R. +Proof. + Fail lra. +Abort. + +Instance Dplus : DeclaredConstant Init.Nat.add := {}. + +Goal ( 1 ^ (2 + 2) = 1)%R. +Proof. + lra. +Qed. + +Require Import Lia. + +Goal ( 1 ^ (2 + 2) = 1)%Z. +Proof. + Fail lia. + reflexivity. +Qed. + +Instance DZplus : DeclaredConstant Z.add := {}. + +Goal ( 1 ^ (2 + 2) = 1)%Z. +Proof. + lia. +Qed. + + +Goal (1 / IZR (Z.pow_pos 10 25) = 1 / 10 ^ 25)%R. +Proof. + lra. +Qed. diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v index 239bc69360..55691f553c 100644 --- a/test-suite/micromega/zomicron.v +++ b/test-suite/micromega/zomicron.v @@ -82,11 +82,48 @@ Proof. lia. Qed. +Section S. + Variables x y: Z. + Variables XGe : x >= 0. + Variables YGt : y > 0. + Variables YLt : y < 0. + + Goal False. + Proof using - XGe. + lia. + Qed. + + Goal False. + Proof using YGt YLt x y. + lia. + Qed. + + End S. + (* Bug 5073 *) Lemma opp_eq_0_iff a : -a = 0 <-> a = 0. Proof. lia. Qed. +Lemma ex_pos : forall x, exists z t, x = z - t /\ z >= 0 /\ t >= 0. +Proof. + intros. + destruct (dec_Zge x 0). + exists x, 0. + lia. + exists 0, (-x). + lia. +Qed. - +Goal forall + (b q r : Z) + (H : b * q + r <= 0) + (H5 : - b < r) + (H6 : r <= 0) + (H2 : 0 <= b), + b = 0 -> False. +Proof. + intros b q r. + lia. +Qed. diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v index 36992e4dda..7429a521b3 100644 --- a/test-suite/output/MExtraction.v +++ b/test-suite/output/MExtraction.v @@ -7,6 +7,8 @@ Require Import QMicromega. Require Import RMicromega. Recursive Extraction - List.map simpl_cone (*map_cone indexes*) - denorm Qpower vm_add + Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula + ZMicromega.cnfZ ZMicromega.bound_problem_fr 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/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index 59b2f789ab..3f8840529e 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -170,7 +170,7 @@ Qed. Lemma equal_cardinal: equal s s'=true -> cardinal s=cardinal s'. Proof. -auto with set. +auto with set fset. Qed. (* Properties of [subset] *) @@ -268,7 +268,7 @@ Proof. intros; apply bool_1; split; intros. rewrite MP.cardinal_1; simpl; auto with set. assert (cardinal s = 0) by (apply zerob_true_elim; auto). -auto with set. +auto with set fset. Qed. (** Properties of [singleton] *) @@ -551,7 +551,7 @@ End Fold. Lemma add_cardinal_1: forall s x, mem x s=true -> cardinal (add x s)=cardinal s. Proof. -auto with set. +auto with set fset. Qed. Lemma add_cardinal_2: @@ -846,9 +846,9 @@ Lemma sum_plus : Proof. unfold sum. intros f g Hf Hg. -assert (fc : compat_opL (fun x:elt =>plus (f x))). red; auto. +assert (fc : compat_opL (fun x:elt =>plus (f x))). red; auto with fset. assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega. -assert (gc : compat_opL (fun x:elt => plus (g x))). red; auto. +assert (gc : compat_opL (fun x:elt => plus (g x))). red; auto with fset. assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega. assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). repeat red; auto. assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega. diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 17f0e25e7a..6b6546f82d 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -21,8 +21,8 @@ Require Import DecidableTypeEx FSetFacts FSetDecide. Set Implicit Arguments. Unset Strict Implicit. -Hint Unfold transpose compat_op Proper respectful : core. -Hint Extern 1 (Equivalence _) => constructor; congruence : core. +Hint Unfold transpose compat_op Proper respectful : fset. +Hint Extern 1 (Equivalence _) => constructor; congruence : fset. (** First, a functor for Weak Sets in functorial version. *) @@ -708,7 +708,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0. Proof. - intros; rewrite cardinal_fold; apply fold_1; auto. + intros; rewrite cardinal_fold; apply fold_1; auto with fset. Qed. Lemma cardinal_2 : @@ -716,7 +716,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). Proof. intros; do 2 rewrite cardinal_fold. change S with ((fun _ => S) x). - apply fold_2; auto. + apply fold_2; auto with fset. Qed. (** ** Cardinal and (non-)emptiness *) @@ -732,7 +732,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). Proof. intros; rewrite cardinal_Empty; auto. Qed. - Hint Resolve cardinal_inv_1 : core. + Hint Resolve cardinal_inv_1 : fset. Lemma cardinal_inv_2 : forall s n, cardinal s = S n -> { x : elt | In x s }. @@ -757,7 +757,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). symmetry. remember (cardinal s) as n; symmetry in Heqn; revert s s' Heqn H. induction n; intros. - apply cardinal_1; rewrite <- H; auto. + apply cardinal_1; rewrite <- H; auto with fset. destruct (cardinal_inv_2 Heqn) as (x,H2). revert Heqn. rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set. @@ -769,13 +769,13 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). exact Equal_cardinal. Qed. - Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : core. + Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : fset. (** ** Cardinal and set operators *) Lemma empty_cardinal : cardinal empty = 0. Proof. - rewrite cardinal_fold; apply fold_1; auto with set. + rewrite cardinal_fold; apply fold_1; auto with set fset. Qed. Hint Immediate empty_cardinal cardinal_1 : set. @@ -795,7 +795,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). Proof. intros; do 3 rewrite cardinal_fold. rewrite <- fold_plus. - apply fold_diff_inter with (eqA:=@Logic.eq nat); auto. + apply fold_diff_inter with (eqA:=@Logic.eq nat); auto with fset. Qed. Lemma union_cardinal: @@ -804,7 +804,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). Proof. intros; do 3 rewrite cardinal_fold. rewrite <- fold_plus. - apply fold_union; auto. + apply fold_union; auto with fset. Qed. Lemma subset_cardinal : @@ -838,7 +838,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). intros. do 4 rewrite cardinal_fold. do 2 rewrite <- fold_plus. - apply fold_union_inter with (eqA:=@Logic.eq nat); auto. + apply fold_union_inter with (eqA:=@Logic.eq nat); auto with fset. Qed. Lemma union_cardinal_inter : @@ -860,7 +860,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). Lemma add_cardinal_1 : forall s x, In x s -> cardinal (add x s) = cardinal s. Proof. - auto with set. + auto with set fset. Qed. Lemma add_cardinal_2 : @@ -869,7 +869,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). intros. do 2 rewrite cardinal_fold. change S with ((fun _ => S) x); - apply fold_add with (eqA:=@Logic.eq nat); auto. + apply fold_add with (eqA:=@Logic.eq nat); auto with fset. Qed. Lemma remove_cardinal_1 : @@ -878,16 +878,16 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). intros. do 2 rewrite cardinal_fold. change S with ((fun _ =>S) x). - apply remove_fold_1 with (eqA:=@Logic.eq nat); auto. + apply remove_fold_1 with (eqA:=@Logic.eq nat); auto with fset. Qed. Lemma remove_cardinal_2 : forall s x, ~In x s -> cardinal (remove x s) = cardinal s. Proof. - auto with set. + auto with set fset. Qed. - Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : core. + Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : fset. End WProperties_fun. @@ -952,7 +952,7 @@ Module OrdProperties (M:S). red; intros x a b H; unfold leb. f_equal; apply gtb_compat; auto. Qed. - Hint Resolve gtb_compat leb_compat : core. + Hint Resolve gtb_compat leb_compat : fset. Lemma elements_split : forall x s, elements s = elements_lt x s ++ elements_ge x s. @@ -1047,7 +1047,7 @@ Module OrdProperties (M:S). (forall s s', P s -> forall x, Above x s -> Add x s s' -> P s') -> forall s : t, P s. Proof. - intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto. + intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto with fset. case_eq (max_elt s); intros. apply X0 with (remove e s) e; auto with set. apply IHn. @@ -1068,7 +1068,7 @@ Module OrdProperties (M:S). (forall s s', P s -> forall x, Below x s -> Add x s s' -> P s') -> forall s : t, P s. Proof. - intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto. + intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto with fset. case_eq (min_elt s); intros. apply X0 with (remove e s) e; auto with set. apply IHn. diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 59e0148625..e17f02bb6e 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -15,7 +15,6 @@ Require Import Rbase. Require Import R_Ifp. -Require Import Lra. Local Open Scope R_scope. Implicit Type r : R. @@ -357,7 +356,9 @@ Qed. Lemma Rle_abs : forall x:R, x <= Rabs x. Proof. - intro; unfold Rabs; case (Rcase_abs x); intros; lra. + intro; unfold Rabs; case (Rcase_abs x); intros;auto with real. + apply Rminus_le; rewrite <- Rplus_0_r; + unfold Rminus; rewrite Ropp_involutive; auto with real. Qed. Definition RRle_abs := Rle_abs. |