diff options
author | fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-02 13:24:47 +0000 |
---|---|---|
committer | fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-02 13:24:47 +0000 |
commit | 3bf96f48739699da368bb872663945ebdb2d78a4 (patch) | |
tree | 7d29f2a7a70a3b345bdc3587fe2563d6a586576d | |
parent | 7f110df7d7ff6a4d43f3c8d19305b20e24f4800e (diff) |
Improved robustness of micromega parser. Proof search of Micromega test-suites is now bounded -- ensure termination
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11200 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/micromega/coq_micromega.ml | 260 | ||||
-rw-r--r-- | doc/refman/Micromega.tex | 4 | ||||
-rw-r--r-- | test-suite/micromega/bertot.v | 2 | ||||
-rw-r--r-- | test-suite/micromega/example.v | 72 | ||||
-rw-r--r-- | test-suite/micromega/qexample.v | 3 | ||||
-rw-r--r-- | test-suite/micromega/rexample.v | 10 | ||||
-rw-r--r-- | test-suite/micromega/square.v | 8 |
7 files changed, 152 insertions, 207 deletions
diff --git a/contrib/micromega/coq_micromega.ml b/contrib/micromega/coq_micromega.ml index 3d6d5bcfa..02ff61a19 100644 --- a/contrib/micromega/coq_micromega.ml +++ b/contrib/micromega/coq_micromega.ml @@ -106,6 +106,7 @@ struct ["Coq" ; "micromega" ; "EnvRing"]; ["Coq";"QArith"; "QArith_base"]; ["Coq";"Reals" ; "Rdefinitions"]; + ["Coq";"Reals" ; "Rpow_def"]; ["LRing_normalise"]] let constant = gen_constant_in_modules "ZMicromega" coq_modules @@ -163,6 +164,9 @@ struct let coq_Qmake = lazy (constant "Qmake") + let coq_R0 = lazy (constant "R0") + let coq_R1 = lazy (constant "R1") + let coq_proofTerm = lazy (constant "ProofTerm") let coq_ratProof = lazy (constant "RatProof") @@ -179,10 +183,36 @@ struct let coq_Zminus = lazy (constant "Zminus") let coq_Zopp = lazy (constant "Zopp") let coq_Zmult = lazy (constant "Zmult") + let coq_Zpower = lazy (constant "Zpower") let coq_N_of_Z = lazy (gen_constant_in_modules "ZArithRing" [["Coq";"setoid_ring";"ZArithRing"]] "N_of_Z") + let coq_Qgt = lazy (constant "Qgt") + let coq_Qge = lazy (constant "Qge") + let coq_Qle = lazy (constant "Qle") + let coq_Qlt = lazy (constant "Qlt") + let coq_Qeq = lazy (constant "Qeq") + + + let coq_Qplus = lazy (constant "Qplus") + let coq_Qminus = lazy (constant "Qminus") + let coq_Qopp = lazy (constant "Qopp") + let coq_Qmult = lazy (constant "Qmult") + let coq_Qpower = lazy (constant "Qpower") + + + let coq_Rgt = lazy (constant "Rgt") + let coq_Rge = lazy (constant "Rge") + let coq_Rle = lazy (constant "Rle") + let coq_Rlt = lazy (constant "Rlt") + + let coq_Rplus = lazy (constant "Rplus") + let coq_Rminus = lazy (constant "Rminus") + let coq_Ropp = lazy (constant "Ropp") + let coq_Rmult = lazy (constant "Rmult") + let coq_Rpower = lazy (constant "pow") + let coq_PEX = lazy (constant "PEX" ) let coq_PEc = lazy (constant"PEc") @@ -225,6 +255,7 @@ struct (gen_constant_in_modules "RingMicromega" [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ] "Formula") + type parse_error = | Ukn | BadStr of string @@ -347,16 +378,11 @@ let dump_q q = let parse_q term = match Term.kind_of_term term with - | Term.App(c, args) -> - ( - match Term.kind_of_term c with - Term.Construct((n,j),i) -> - if Names.string_of_kn n = "Coq.QArith.QArith_base#<>#Q" - then {Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) } + | Term.App(c, args) -> if c = Lazy.force coq_Qmake then + {Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) } else raise ParseError - | _ -> raise ParseError - ) - | _ -> raise ParseError + | _ -> raise ParseError + let rec parse_list parse_elt term = let (i,c) = get_left_construct term in @@ -466,19 +492,6 @@ let parse_q term = pp_cone o e - - - let rec parse_op term = - let (i,c) = get_left_construct term in - match i with - | 1 -> Mc.OpEq - | 2 -> Mc.OpLe - | 3 -> Mc.OpGe - | 4 -> Mc.OpGt - | 5 -> Mc.OpLt - | i -> raise ParseError - - let rec dump_op = function | Mc.OpEq-> Lazy.force coq_OpEq | Mc.OpNEq-> Lazy.force coq_OpNEq @@ -510,68 +523,52 @@ let parse_q term = dump_op o ; dump_expr typ dump_constant e2|]) + let assoc_const x l = + try + snd (List.find (fun (x',y) -> x = Lazy.force x') l) + with + Not_found -> raise ParseError + + let zop_table = [ + coq_Zgt, Mc.OpGt ; + coq_Zge, Mc.OpGe ; + coq_Zlt, Mc.OpLt ; + coq_Zle, Mc.OpLe ] + + let rop_table = [ + coq_Rgt, Mc.OpGt ; + coq_Rge, Mc.OpGe ; + coq_Rlt, Mc.OpLt ; + coq_Rle, Mc.OpLe ] + + let qop_table = [ + coq_Qlt, Mc.OpLt ; + coq_Qle, Mc.OpLe ; + coq_Qeq, Mc.OpEq + ] let parse_zop (op,args) = match kind_of_term op with - | Const x -> - (match Names.string_of_con x with - | "Coq.ZArith.BinInt#<>#Zgt" -> (Mc.OpGt, args.(0), args.(1)) - | "Coq.ZArith.BinInt#<>#Zge" -> (Mc.OpGe, args.(0), args.(1)) - | "Coq.ZArith.BinInt#<>#Zlt" -> (Mc.OpLt, args.(0), args.(1)) - | "Coq.ZArith.BinInt#<>#Zle" -> (Mc.OpLe, args.(0), args.(1)) - (*| "Coq.Init.Logic#<>#not" -> Mc.OpNEq (* for backward compat *)*) - | s -> raise ParseError - ) + | Const x -> (assoc_const op zop_table, args.(0) , args.(1)) | Ind(n,0) -> - (match Names.string_of_kn n with - | "Coq.Init.Logic#<>#eq" -> - if args.(0) <> Lazy.force coq_Z - then raise ParseError - else (Mc.OpEq, args.(1), args.(2)) - | _ -> raise ParseError) + if op = Lazy.force coq_Eq && args.(0) = Lazy.force coq_Z + then (Mc.OpEq, args.(1), args.(2)) + else raise ParseError | _ -> failwith "parse_zop" let parse_rop (op,args) = - try match kind_of_term op with - | Const x -> - (match Names.string_of_con x with - | "Coq.Reals.Rdefinitions#<>#Rgt" -> (Mc.OpGt, args.(0), args.(1)) - | "Coq.Reals.Rdefinitions#<>#Rge" -> (Mc.OpGe, args.(0), args.(1)) - | "Coq.Reals.Rdefinitions#<>#Rlt" -> (Mc.OpLt, args.(0), args.(1)) - | "Coq.Reals.Rdefinitions#<>#Rle" -> (Mc.OpLe, args.(0), args.(1)) - (*| "Coq.Init.Logic#<>#not"-> Mc.OpNEq (* for backward compat *)*) - | s -> raise ParseError - ) + | Const x -> (assoc_const op rop_table, args.(0) , args.(1)) | Ind(n,0) -> - (match Names.string_of_kn n with - | "Coq.Init.Logic#<>#eq" -> - (* if args.(0) <> Lazy.force coq_R - then raise ParseError - else*) (Mc.OpEq, args.(1), args.(2)) - | _ -> raise ParseError) - | _ -> failwith "parse_rop" - with x -> - (Pp.pp (Pp.str "parse_rop failure ") ; - Pp.pp (Printer.prterm op) ; Pp.pp_flush ()) - ; raise x - + if op = Lazy.force coq_Eq && args.(0) = Lazy.force coq_R + then (Mc.OpEq, args.(1), args.(2)) + else raise ParseError + | _ -> failwith "parse_zop" let parse_qop (op,args) = - ( - (match kind_of_term op with - | Const x -> - (match Names.string_of_con x with - | "Coq.QArith.QArith_base#<>#Qgt" -> Mc.OpGt - | "Coq.QArith.QArith_base#<>#Qge" -> Mc.OpGe - | "Coq.QArith.QArith_base#<>#Qlt" -> Mc.OpLt - | "Coq.QArith.QArith_base#<>#Qle" -> Mc.OpLe - | "Coq.QArith.QArith_base#<>#Qeq" -> Mc.OpEq - | s -> raise ParseError - ) - | _ -> failwith "parse_zop") , args.(0) , args.(1)) + (assoc_const op qop_table, args.(0) , args.(1)) module Env = @@ -612,6 +609,14 @@ let parse_q term = | Ukn of string + let assoc_ops x l = + try + snd (List.find (fun (x',y) -> x = Lazy.force x') l) + with + Not_found -> Ukn "Oups" + + + let parse_expr parse_constant parse_exp ops_spec env term = if debug then (Pp.pp (Pp.str "parse_expr: "); @@ -634,7 +639,7 @@ let parse_q term = ( match kind_of_term t with | Const c -> - ( match ops_spec (Names.string_of_con c) with + ( match assoc_ops 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) @@ -653,29 +658,29 @@ let parse_q term = parse_expr env term -let zop_spec = function - | "Coq.ZArith.BinInt#<>#Zplus" -> Binop (fun x y -> Mc.PEadd(x,y)) - | "Coq.ZArith.BinInt#<>#Zminus" -> Binop (fun x y -> Mc.PEsub(x,y)) - | "Coq.ZArith.BinInt#<>#Zmult" -> Binop (fun x y -> Mc.PEmul (x,y)) - | "Coq.ZArith.BinInt#<>#Zopp" -> Opp - | "Coq.ZArith.Zpow_def#<>#Zpower" -> Power - | s -> Ukn s + let zop_spec = + [ + coq_Zplus , Binop (fun x y -> Mc.PEadd(x,y)) ; + coq_Zminus , Binop (fun x y -> Mc.PEsub(x,y)) ; + coq_Zmult , Binop (fun x y -> Mc.PEmul (x,y)) ; + coq_Zopp , Opp ; + coq_Zpower , Power] -let qop_spec = function - | "Coq.QArith.QArith_base#<>#Qplus" -> Binop (fun x y -> Mc.PEadd(x,y)) - | "Coq.QArith.QArith_base#<>#Qminus" -> Binop (fun x y -> Mc.PEsub(x,y)) - | "Coq.QArith.QArith_base#<>#Qmult" -> Binop (fun x y -> Mc.PEmul (x,y)) - | "Coq.QArith.QArith_base#<>#Qopp" -> Opp - | "Coq.QArith.QArith_base#<>#Qpower" -> Power - | s -> Ukn s +let qop_spec = + [ + coq_Qplus , Binop (fun x y -> Mc.PEadd(x,y)) ; + coq_Qminus , Binop (fun x y -> Mc.PEsub(x,y)) ; + coq_Qmult , Binop (fun x y -> Mc.PEmul (x,y)) ; + coq_Qopp , Opp ; + coq_Qpower , Power] -let rop_spec = function - | "Coq.Reals.Rdefinitions#<>#Rplus" -> Binop (fun x y -> Mc.PEadd(x,y)) - | "Coq.Reals.Rdefinitions#<>#Rminus" -> Binop (fun x y -> Mc.PEsub(x,y)) - | "Coq.Reals.Rdefinitions#<>#Rmult" -> Binop (fun x y -> Mc.PEmul (x,y)) - | "Coq.Reals.Rdefinitions#<>#Ropp" -> Opp - | "Coq.Reals.Rpow_def#<>#pow" -> Power - | s -> Ukn s +let rop_spec = + [ + coq_Rplus , Binop (fun x y -> Mc.PEadd(x,y)) ; + coq_Rminus , Binop (fun x y -> Mc.PEsub(x,y)) ; + coq_Rmult , Binop (fun x y -> Mc.PEmul (x,y)) ; + coq_Ropp , Opp ; + coq_Rpower , Power] @@ -691,12 +696,12 @@ let rconstant term = Pp.pp (Pp.str "rconstant: "); Pp.pp (Printer.prterm term); Pp.pp_flush ()); match Term.kind_of_term term with - | Const x -> - (match Names.string_of_con x with - | "Coq.Reals.Rdefinitions#<>#R0" -> Mc.Z0 - | "Coq.Reals.Rdefinitions#<>#R1" -> Mc.Zpos Mc.XH - | _ -> raise ParseError - ) + | Const x -> + if term = Lazy.force coq_R0 + then Mc.Z0 + else if term = Lazy.force coq_R1 + then Mc.Zpos Mc.XH + else raise ParseError | _ -> raise ParseError @@ -731,23 +736,6 @@ let parse_rexpr = (* generic parsing of arithmetic expressions *) - let rec parse_conj parse_arith env term = - match kind_of_term term with - | App(l,rst) -> - (match kind_of_term l with - | Ind (n,_) -> - ( match Names.string_of_kn n with - | "Coq.Init.Logic#<>#and" -> - let (e1,env) = parse_arith env rst.(0) in - let (e2,env) = parse_conj parse_arith env rst.(1) in - (Mc.Cons(e1,e2),env) - | _ -> (* This might be an equality *) - let (e,env) = parse_arith env term in - (Mc.Cons(e,Mc.Nil),env)) - | _ -> (* This is an arithmetic expression *) - let (e,env) = parse_arith env term in - (Mc.Cons(e,Mc.Nil),env)) - | _ -> failwith "parse_conj(2)" @@ -850,46 +838,6 @@ let parse_rexpr = xdump f - (* Backward compat *) - - let rec parse_concl parse_arith env term = - match kind_of_term term with - | Prod(_,expr,rst) -> (* a -> b *) - let (lhs,rhs,env) = parse_concl parse_arith env rst in - let (e,env) = parse_arith env expr in - (Mc.Cons(e,lhs),rhs,env) - | App(_,_) -> - let (conj, env) = parse_conj parse_arith env term in - (Mc.Nil,conj,env) - | Ind(n,_) -> - (match (Names.string_of_kn n) with - | "Coq.Init.Logic#<>#False" -> (Mc.Nil,Mc.Nil,env) - | s -> - print_string s ; flush stdout; - failwith "parse_concl") - | _ -> failwith "parse_concl" - - - let rec parse_hyps parse_arith env goal_hyps hyps = - match hyps with - | [] -> ([],goal_hyps,env) - | (i,t)::l -> - let (li,lt,env) = parse_hyps parse_arith env goal_hyps l in - try - let (c,env) = parse_arith env t in - (i::li, Mc.Cons(c,lt), env) - with x -> - (*(if debug then Printf.printf "parse_arith : %s\n" x);*) - (li,lt,env) - - - let parse_goal parse_arith env hyps term = - try - let (lhs,rhs,env) = parse_concl parse_arith env term in - let (li,lt,env) = parse_hyps parse_arith env lhs hyps in - (li,lt,rhs,env) - with Failure x -> raise ParseError - (* backward compat *) (* ! reverse the list of bindings *) diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index 11e3e8cce..234d51134 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -17,11 +17,11 @@ Load the {\tt Psatz} module ({\tt Require Psatz}.). This module defines the tac \begin{itemize} \item The {\tt psatzl} tactic solves linear goals using an embedded (naive) linear programming prover \emph{i.e.}, fourier elimination. - \item The {\tt psatz} tactic solves polynomial goals using an external prover {\tt cspd}\footnote{Source and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. Note that the {\tt csdp} driver is generating + \item The {\tt psatz} tactic solves polynomial goals using John Harrison's Hol light driver to the external prover {\tt cspd}\footnote{Source and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. Note that the {\tt csdp} driver is generating a \emph{proof cache} thus allowing to rerun scripts even without {\tt csdp}. \item The {\tt lia} (linear integer arithmetic) tactic is specialised to solve linear goals over $\mathbb{Z}$. It extends {\tt psatzl Z} and exploits the discreetness of $\mathbb{Z}$. - \item The {\tt sos} tactic is another driver to the {\tt csdp} prover. In theory, it is less general than + \item The {\tt sos} tactic is another Hol light driver to the {\tt csdp} prover. In theory, it is less general than {\tt psatz}. In practice, even when {\tt psatz} fails, it can be worth a try -- see Section~\ref{sec:psatz-back} for details. \end{itemize} diff --git a/test-suite/micromega/bertot.v b/test-suite/micromega/bertot.v index 8e9c0c6de..bcf222f92 100644 --- a/test-suite/micromega/bertot.v +++ b/test-suite/micromega/bertot.v @@ -17,6 +17,6 @@ Goal (forall x y n, (x < n /\ x <= n /\ 2 * y = x * (x+1) -> x + 1 <= n /\ 2 *(x+1+y) = (x+1)*(x+2))). Proof. intros. - psatz Z. + psatz Z 3. Qed. diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v index 23bea439a..905b9a938 100644 --- a/test-suite/micromega/example.v +++ b/test-suite/micromega/example.v @@ -28,14 +28,14 @@ Qed. Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0. Proof. intros. - psatz Z. + psatz Z 2. Qed. Lemma Zdiscr: forall a b c x, a * x ^ 2 + b * x + c = 0 -> b ^ 2 - 4 * a * c >= 0. Proof. - intros ; psatz Z. + intros ; psatz Z 4. Qed. @@ -51,13 +51,13 @@ Qed. Lemma mplus_minus : forall x y, x + y >= 0 -> x -y >= 0 -> x^2 - y^2 >= 0. Proof. - intros; psatz Z. + intros; psatz Z 2. Qed. Lemma pol3: forall x y, 0 <= x + y -> x^3 + 3*x^2*y + 3*x* y^2 + y^3 >= 0. Proof. - intros; psatz Z. + intros; psatz Z 4. Qed. @@ -96,7 +96,7 @@ Proof. generalize (H8 _ _ _ (conj H5 H4)). generalize (H10 _ _ _ (conj H5 H4)). generalize rho_ge. - psatz Z. + psatz Z 2. Qed. (* Rule of signs *) @@ -104,55 +104,55 @@ Qed. Lemma sign_pos_pos: forall x y, x > 0 -> y > 0 -> x*y > 0. Proof. - intros; psatz Z. + intros; psatz Z 2. Qed. Lemma sign_pos_zero: forall x y, x > 0 -> y = 0 -> x*y = 0. Proof. - intros; psatz Z. + intros; psatz Z 2. Qed. Lemma sign_pos_neg: forall x y, x > 0 -> y < 0 -> x*y < 0. Proof. - intros; psatz Z. + intros; psatz Z 2. Qed. Lemma sign_zer_pos: forall x y, x = 0 -> y > 0 -> x*y = 0. Proof. - intros; psatz Z. + intros; psatz Z 2. Qed. Lemma sign_zero_zero: forall x y, x = 0 -> y = 0 -> x*y = 0. Proof. - intros; psatz Z. + intros; psatz Z 2. Qed. Lemma sign_zero_neg: forall x y, x = 0 -> y < 0 -> x*y = 0. Proof. - intros; psatz Z. + intros; psatz Z 2. Qed. Lemma sign_neg_pos: forall x y, x < 0 -> y > 0 -> x*y < 0. Proof. - intros; psatz Z. + intros; psatz Z 2. Qed. Lemma sign_neg_zero: forall x y, x < 0 -> y = 0 -> x*y = 0. Proof. - intros; psatz Z. + intros; psatz Z 2. Qed. Lemma sign_neg_neg: forall x y, x < 0 -> y < 0 -> x*y > 0. Proof. - intros; psatz Z. + intros; psatz Z 2. Qed. @@ -167,20 +167,20 @@ Qed. Lemma product : forall x y, x >= 0 -> y >= 0 -> x * y >= 0. Proof. intros. - psatz Z. + psatz Z 2. Qed. Lemma product_strict : forall x y, x > 0 -> y > 0 -> x * y > 0. Proof. intros. - psatz Z. + psatz Z 2. Qed. Lemma pow_2_pos : forall x, x ^ 2 + 1 = 0 -> False. Proof. - intros ; psatz Z. + intros ; psatz Z 2. Qed. (* Found in Parrilo's talk *) @@ -188,7 +188,7 @@ Qed. Lemma parrilo_ex : forall x y, x - y^2 + 3 >= 0 -> y + x^2 + 2 = 0 -> False. Proof. intros. - psatz Z. + psatz Z 2. Qed. (* from hol_light/Examples/sos.ml *) @@ -198,26 +198,26 @@ Lemma hol_light1 : forall a1 a2 b1 b2, (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) -> (a1 * b1 + a2 * b2 = 0) -> a1 * a2 - b1 * b2 >= 0. Proof. - intros ; psatz Z. + intros ; psatz Z 4. Qed. Lemma hol_light2 : forall x a, 3 * x + 7 * a < 4 -> 3 < 2 * x -> a < 0. Proof. - intros ; psatz Z. + intros ; psatz Z 2. Qed. Lemma hol_light3 : forall b a c x, b ^ 2 < 4 * a * c -> (a * x ^2 + b * x + c = 0) -> False. Proof. -intros ; psatz Z. +intros ; psatz Z 4. Qed. Lemma hol_light4 : forall a c b x, a * x ^ 2 + b * x + c = 0 -> b ^ 2 >= 4 * a * c. Proof. -intros ; psatz Z. +intros ; psatz Z 4. Qed. Lemma hol_light5 : forall x y, @@ -227,7 +227,7 @@ Lemma hol_light5 : forall x y, x ^ 2 + (y - 1) ^ 2 < 1 \/ (x - 1) ^ 2 + (y - 1) ^ 2 < 1. Proof. -intros; psatz Z. +intros; psatz Z 3. Qed. @@ -236,32 +236,32 @@ Lemma hol_light7 : forall x y z, 0<= x /\ 0 <= y /\ 0 <= z /\ x + y + z <= 3 -> x * y + x * z + y * z >= 3 * x * y * z. Proof. -intros ; psatz Z. +intros ; psatz Z 3. Qed. Lemma hol_light8 : forall x y z, x ^ 2 + y ^ 2 + z ^ 2 = 1 -> (x + y + z) ^ 2 <= 3. Proof. - intros ; psatz Z. + intros ; psatz Z 2. Qed. Lemma hol_light9 : forall w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1 -> (w + x + y + z) ^ 2 <= 4. Proof. - intros; psatz Z. + intros; psatz Z 2. Qed. Lemma hol_light10 : forall x y, x >= 1 /\ y >= 1 -> x * y >= x + y - 1. Proof. - intros ; psatz Z. + intros ; psatz Z 2. Qed. Lemma hol_light11 : forall x y, x > 1 /\ y > 1 -> x * y > x + y - 1. Proof. - intros ; psatz Z. + intros ; psatz Z 2. Qed. @@ -273,14 +273,14 @@ Lemma hol_light12: forall x y z, Proof. intros x y z ; set (e:= (125841 / 50000)). compute in e. - unfold e ; intros ; psatz Z. + unfold e ; intros ; psatz Z 2. Qed. Lemma hol_light14 : forall x y z, 2 <= x /\ x <= 4 /\ 2 <= y /\ y <= 4 /\ 2 <= z /\ z <= 4 -> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z). Proof. - intros ;psatz Z. + intros ;psatz Z 2. Qed. (* ------------------------------------------------------------------------- *) @@ -291,20 +291,20 @@ Lemma hol_light16 : forall x y, 0 <= x /\ 0 <= y /\ (x * y = 1) -> x + y <= x ^ 2 + y ^ 2. Proof. - intros ; psatz Z. + intros ; psatz Z 2. Qed. Lemma hol_light17 : forall x y, 0 <= x /\ 0 <= y /\ (x * y = 1) -> x * y * (x + y) <= x ^ 2 + y ^ 2. Proof. - intros ; psatz Z. + intros ; psatz Z 3. Qed. Lemma hol_light18 : forall x y, 0 <= x /\ 0 <= y -> x * y * (x + y) ^ 2 <= (x ^ 2 + y ^ 2) ^ 2. Proof. - intros ; psatz Z. + intros ; psatz Z 4. Qed. (* ------------------------------------------------------------------------- *) @@ -319,7 +319,7 @@ Qed. Lemma hol_light22 : forall n, n >= 0 -> n <= n * n. Proof. intros. - psatz Z. + psatz Z 2. Qed. @@ -328,7 +328,7 @@ Lemma hol_light24 : forall x1 y1 x2 y2, x1 >= 0 -> x2 >= 0 -> y1 >= 0 -> y2 >= 0 -> (x1 + y1 = x2 + y2). Proof. intros. - psatz Z. + psatz Z 2. Qed. Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2) >= 0. @@ -342,5 +342,5 @@ Lemma motzkin : forall x y, (x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2) >= 0. Proof. intros. generalize (motzkin' x y). - psatz Z. + psatz Z 8. Qed. diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v index cdecebfcd..8a349a1d9 100644 --- a/test-suite/micromega/qexample.v +++ b/test-suite/micromega/qexample.v @@ -17,6 +17,9 @@ Proof. psatzl Q. Qed. + + + (* Other (simple) examples *) Open Scope Q_scope. diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v index 5738ebbff..1de1955db 100644 --- a/test-suite/micromega/rexample.v +++ b/test-suite/micromega/rexample.v @@ -12,7 +12,7 @@ Require Import Ring_normalize. Open Scope R_scope. -Lemma plus_minus : forall x y, +Lemma yplus_minus : forall x y, 0 = x + y -> 0 = x -y -> 0 = x /\ 0 = y. Proof. intros. @@ -74,10 +74,4 @@ Qed. Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). intros; split_Rabs; psatzl R. -Qed. - -Lemma l2 : - forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1. -intros. -split_Rabs; psatzl R. -Qed. +Qed.
\ No newline at end of file diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index 5594afbb9..b78bba25c 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -11,7 +11,7 @@ Open Scope Z_scope. Lemma Zabs_square : forall x, (Zabs x)^2 = x^2. Proof. - intros ; case (Zabs_dec x) ; intros ; psatz Z. + intros ; case (Zabs_dec x) ; intros ; psatz Z 2. Qed. Hint Resolve Zabs_pos Zabs_square. @@ -21,11 +21,11 @@ intros [n [p [Heq Hnz]]]; pose (n' := Zabs n); pose (p':=Zabs p). assert (facts : 0 <= Zabs n /\ 0 <= Zabs p /\ Zabs n^2=n^2 /\ Zabs p^2 = p^2) by auto. assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by - (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z). + (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z 2). generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear. intros n IHn p [Hn [Hp Heq]]. -assert (Hzwf : Zwf 0 (2*p-n) n) by (unfold Zwf; psatz Z). -assert (Hdecr : 0 < 2*p-n /\ 0 <= n-p /\ (2*p-n)^2=2*(n-p)^2) by psatz Z. +assert (Hzwf : Zwf 0 (2*p-n) n) by (unfold Zwf; psatz Z 2). +assert (Hdecr : 0 < 2*p-n /\ 0 <= n-p /\ (2*p-n)^2=2*(n-p)^2) by psatz Z 2. apply (IHn (2*p-n) Hzwf (n-p) Hdecr). Qed. |