diff options
author | 2016-08-30 17:12:27 +0200 | |
---|---|---|
committer | 2016-08-30 17:59:59 +0200 | |
commit | 721637c98514a77d05d080f53f226cab3a8da1e7 (patch) | |
tree | 9a04e0482488764d39c0e24847e93f4b23f62cde /plugins | |
parent | 44ada644ef50563aa52cfcd7717d44bde29e5a20 (diff) |
plugin micromega : nra also handles non-linear rational arithmetic over Q (Fixed #4985)
Lqa.v defines the tactics lra and nra working over Q.
Lra.v defines the tactics lra and nra working over R.
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/micromega/Lqa.v | 55 | ||||
-rw-r--r-- | plugins/micromega/Lra.v | 56 | ||||
-rw-r--r-- | plugins/micromega/Psatz.v | 40 | ||||
-rw-r--r-- | plugins/micromega/coq_micromega.ml | 20 | ||||
-rw-r--r-- | plugins/micromega/g_micromega.ml4 | 10 | ||||
-rw-r--r-- | plugins/micromega/vo.itarget | 4 |
6 files changed, 152 insertions, 33 deletions
diff --git a/plugins/micromega/Lqa.v b/plugins/micromega/Lqa.v new file mode 100644 index 000000000..0055600a0 --- /dev/null +++ b/plugins/micromega/Lqa.v @@ -0,0 +1,55 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* *) +(* Micromega: A reflexive tactic using the Positivstellensatz *) +(* *) +(* Frédéric Besson (Irisa/Inria) 2016 *) +(* *) +(************************************************************************) + +Require Import QMicromega. +Require Import QArith. +Require Import RingMicromega. +Require Import VarMap. +Require Coq.micromega.Tauto. +Declare ML Module "micromega_plugin". + +(** Here, lra stands for linear rational arithmetic *) +Ltac lra := lra_Q ; + (abstract(intros __wit __varmap __ff ; + change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; + apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))). + +(** Here, nra stands for non-linear rational arithmetic *) +Ltac nra := + xnqa ; + (abstract(intros __wit __varmap __ff ; + change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; + apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))). + +Ltac xpsatz dom d := + let tac := lazymatch dom with + | Q => + (sos_Q || psatz_Q d) ; + (* If csdp is not installed, the previous step might not produce any + progress: the rest of the tactical will then fail. Hence the 'try'. *) + try (abstract(intros __wit __varmap __ff ; + change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; + apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) + | _ => fail "Unsupported domain" + end in tac. + +Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n. +Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1). + + + + +(* Local Variables: *) +(* coding: utf-8 *) +(* End: *) diff --git a/plugins/micromega/Lra.v b/plugins/micromega/Lra.v new file mode 100644 index 000000000..7ffe1e4ed --- /dev/null +++ b/plugins/micromega/Lra.v @@ -0,0 +1,56 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* *) +(* Micromega: A reflexive tactic using the Positivstellensatz *) +(* *) +(* Frédéric Besson (Irisa/Inria) 2016 *) +(* *) +(************************************************************************) + +Require Import RMicromega. +Require Import QMicromega. +Require Import Rdefinitions. +Require Import RingMicromega. +Require Import VarMap. +Require Coq.micromega.Tauto. +Declare ML Module "micromega_plugin". + +(** Here, lra stands for linear real arithmetic *) +Ltac lra := + unfold Rdiv in * ; + lra_R ; + (abstract((intros __wit __varmap __ff ; + change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; + apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))). + +(** Here, nra stands for non-linear real arithmetic *) +Ltac nra := + xnra ; + (abstract((intros __wit __varmap __ff ; + change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; + apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))). + +Ltac xpsatz dom d := + let tac := lazymatch dom with + | R => + (sos_R || psatz_R d) ; + (* If csdp is not installed, the previous step might not produce any + progress: the rest of the tactical will then fail. Hence the 'try'. *) + try (abstract(intros __wit __varmap __ff ; + change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; + apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) + | _ => fail "Unsupported domain" + end in tac. + +Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n. +Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1). + + +(* Local Variables: *) +(* coding: utf-8 *) +(* End: *) diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index fafd8a5f2..b1f242f58 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -8,7 +8,7 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* Frédéric Besson (Irisa/Inria) 2006-2016 *) (* *) (************************************************************************) @@ -75,35 +75,39 @@ Ltac psatzl dom := let tac := lazymatch dom with | Z => lia | Q => - psatzl_Q ; - (* If csdp is not installed, the previous step might not produce any - progress: the rest of the tactical will then fail. Hence the 'try'. *) - try (abstract(intros __wit __varmap __ff ; - change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; - apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) + lra_Q ; + (abstract(intros __wit __varmap __ff ; + change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; + apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) | R => unfold Rdiv in * ; - psatzl_R ; - (* If csdp is not installed, the previous step might not produce any - progress: the rest of the tactical will then fail. Hence the 'try'. *) - try abstract((intros __wit __varmap __ff ; - change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; - apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) - | _ => fail "Unsupported domain" + lra_R ; + (abstract((intros __wit __varmap __ff ; + change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; + apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))) +| _ => fail "Unsupported domain" end in tac. Ltac lra := first [ psatzl R | psatzl Q ]. -Ltac nra := +Ltac nra_R := unfold Rdiv in * ; xnra ; abstract (intros __wit __varmap __ff ; - change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; - apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity). - + change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; + apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity). + +Ltac nra_Q := + xnqa ; + (abstract(intros __wit __varmap __ff ; + change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; + apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))). + +Ltac nra := + first [ nra_R | nra_Q ]. (* Local Variables: *) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index b8e5e66ca..edcb00b90 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -2100,11 +2100,7 @@ let tauto_lia ff = * solvers *) -let psatzl_Z = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec - [ linear_Z ] - -let psatzl_Q = +let lra_Q = micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec [ linear_prover_Q ] @@ -2112,7 +2108,7 @@ let psatz_Q i = micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] -let psatzl_R = +let lra_R = micromega_genr [ linear_prover_R ] let psatz_R i = @@ -2136,21 +2132,21 @@ let sos_R = micromega_genr [ non_linear_prover_R "pure_sos" None ] -let xlia = - try - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec +let xlia = micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ linear_Z ] - with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise let xnlia = - try micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ nlinear_Z ] - with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise let nra = micromega_genr [ nlinear_prover_R ] +let nqa = + micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec + [ nlinear_prover_R ] + + (* Local Variables: *) (* coding: utf-8 *) diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index e6b5cc60d..974dcee87 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -37,6 +37,12 @@ TACTIC EXTEND NRA [ "xnra" ] -> [ (Coq_micromega.nra)] END +TACTIC EXTEND NQA +[ "xnqa" ] -> [ (Coq_micromega.nqa)] +END + + + TACTIC EXTEND Sos_Z | [ "sos_Z" ] -> [ (Coq_micromega.sos_Z) ] END @@ -50,11 +56,11 @@ TACTIC EXTEND Sos_R END TACTIC EXTEND LRA_Q -[ "psatzl_Q" ] -> [ (Coq_micromega.psatzl_Q) ] +[ "lra_Q" ] -> [ (Coq_micromega.lra_Q) ] END TACTIC EXTEND LRA_R -[ "psatzl_R" ] -> [ (Coq_micromega.psatzl_R) ] +[ "lra_R" ] -> [ (Coq_micromega.lra_R) ] END TACTIC EXTEND PsatzR diff --git a/plugins/micromega/vo.itarget b/plugins/micromega/vo.itarget index bf6a1a7db..cb4b2b8a5 100644 --- a/plugins/micromega/vo.itarget +++ b/plugins/micromega/vo.itarget @@ -10,4 +10,6 @@ Tauto.vo VarMap.vo ZCoeff.vo ZMicromega.vo -Lia.vo
\ No newline at end of file +Lia.vo +Lqa.vo +Lra.vo
\ No newline at end of file |