From 91618b50da9508a75c2c43c42a4794a06b83a3ee Mon Sep 17 00:00:00 2001 From: fbesson Date: Thu, 30 Jul 2009 21:30:12 +0000 Subject: micromega : Better parsing of formulae - smaller proof terms for Z - redesign of proof cache git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12254 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/micromega/QMicromega.v | 38 ++++++++++++++++++++------------------ 1 file changed, 20 insertions(+), 18 deletions(-) (limited to 'plugins/micromega/QMicromega.v') diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v index f02209459..b266a1ab8 100644 --- a/plugins/micromega/QMicromega.v +++ b/plugins/micromega/QMicromega.v @@ -17,7 +17,7 @@ Require Import RingMicromega. Require Import Refl. Require Import QArith. Require Import Qfield. -Declare ML Module "micromega_plugin". +(*Declare ML Module "micromega_plugin".*) Lemma Qsor : SOR 0 1 Qplus Qmult Qminus Qopp Qeq Qle Qlt. Proof. @@ -105,6 +105,7 @@ Qed. Lemma Qeval_expr_compat : forall env e, Qeval_expr env e = Qeval_expr' env e. Proof. induction e ; simpl ; subst ; try congruence. + reflexivity. rewrite IHe. apply QNpower. Qed. @@ -137,9 +138,8 @@ Proof. Qed. - Definition Qeval_nformula := - eval_nformula 0 Qplus Qmult Qminus Qopp Qeq Qle Qlt (fun x => x) (fun x => x) (pow_N 1 Qmult). + eval_nformula 0 Qplus Qmult Qeq Qle Qlt (fun x => x) . Definition Qeval_op1 (o : Op1) : Q -> Prop := match o with @@ -149,22 +149,15 @@ match o with | NonStrict => fun x : Q => 0 <= x end. -Lemma Qeval_nformula_simpl : forall env f, Qeval_nformula env f = (let (p, op) := f in Qeval_op1 op (Qeval_expr env p)). -Proof. - intros. - destruct f. - rewrite Qeval_expr_compat. - reflexivity. -Qed. - + Lemma Qeval_nformula_dec : forall env d, (Qeval_nformula env d) \/ ~ (Qeval_nformula env d). Proof. - exact (fun env d =>eval_nformula_dec Qsor (fun x => x) (fun x => x) (pow_N 1 Qmult) env d). + exact (fun env d =>eval_nformula_dec Qsor (fun x => x) env d). Qed. -Definition QWitness := ConeMember Q. +Definition QWitness := Psatz Q. -Definition QWeakChecker := check_normalised_formulas 0 1 Qplus Qmult Qminus Qopp Qeq_bool Qle_bool. +Definition QWeakChecker := check_normalised_formulas 0 1 Qplus Qmult Qeq_bool Qle_bool. Require Import List. @@ -182,8 +175,15 @@ Qed. Require Import 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 QTautoChecker (f : BFormula (Formula Q)) (w: list QWitness) : bool := - @tauto_checker (Formula Q) (NFormula Q) (@cnf_normalise Q) (@cnf_negate Q) QWitness QWeakChecker f w. + @tauto_checker (Formula Q) (NFormula Q) + Qnormalise + Qnegate QWitness QWeakChecker f w. + + Lemma QTautoChecker_sound : forall f w, QTautoChecker f w = true -> forall env, eval_f (Qeval_formula env) f. Proof. @@ -191,10 +191,12 @@ Proof. unfold QTautoChecker. apply (tauto_checker_sound Qeval_formula Qeval_nformula). apply Qeval_nformula_dec. - intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now apply (cnf_normalise_correct Qsor). - intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now apply (cnf_negate_correct Qsor). + 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. Qed. - +(* Local Variables: *) +(* coding: utf-8 *) +(* End: *) -- cgit v1.2.3