summaryrefslogtreecommitdiff
path: root/contrib/micromega/coq_micromega.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/micromega/coq_micromega.ml')
-rw-r--r--contrib/micromega/coq_micromega.ml334
1 files changed, 165 insertions, 169 deletions
diff --git a/contrib/micromega/coq_micromega.ml b/contrib/micromega/coq_micromega.ml
index 29e2a183..02ff61a1 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 *)
@@ -1235,8 +1183,8 @@ let lift_ratproof prover l =
| Some c -> Some (Mc.RatProof c)
-type csdpcert = Certificate.Mc.z Certificate.Mc.coneMember option
-type micromega_polys = (Micromega.z Mc.pExpr, Mc.op1) Micromega.prod list
+type csdpcert = Sos.positivstellensatz option
+type micromega_polys = (Micromega.q Mc.pExpr, Mc.op1) Micromega.prod list
type provername = string * int option
let call_csdpcert provername poly =
@@ -1255,36 +1203,84 @@ let call_csdpcert provername poly =
close_in ch_from; Sys.remove tmp_from;
cert
-let omicron gl =
+let rec z_to_q_expr e =
+ match e with
+ | Mc.PEc z -> Mc.PEc {Mc.qnum = z ; Mc.qden = Mc.XH}
+ | Mc.PEX x -> Mc.PEX x
+ | Mc.PEadd(e1,e2) -> Mc.PEadd(z_to_q_expr e1, z_to_q_expr e2)
+ | Mc.PEsub(e1,e2) -> Mc.PEsub(z_to_q_expr e1, z_to_q_expr e2)
+ | Mc.PEmul(e1,e2) -> Mc.PEmul(z_to_q_expr e1, z_to_q_expr e2)
+ | Mc.PEopp(e) -> Mc.PEopp(z_to_q_expr e)
+ | Mc.PEpow(e,n) -> Mc.PEpow(z_to_q_expr e,n)
+
+
+let call_csdpcert_q provername poly =
+ match call_csdpcert provername poly with
+ | None -> None
+ | Some cert ->
+ let cert = Certificate.q_cert_of_pos cert in
+ match Mc.qWeakChecker (CamlToCoq.list (fun x -> x) poly) cert with
+ | Mc.True -> Some cert
+ | Mc.False -> (print_string "buggy certificate" ; flush stdout) ;None
+
+
+let call_csdpcert_z provername poly =
+ let l = List.map (fun (Mc.Pair(e,o)) -> (Mc.Pair(z_to_q_expr e,o))) poly in
+ match call_csdpcert provername l with
+ | None -> None
+ | Some cert ->
+ let cert = Certificate.z_cert_of_pos cert in
+ match Mc.zWeakChecker (CamlToCoq.list (fun x -> x) poly) cert with
+ | Mc.True -> Some cert
+ | Mc.False -> (print_string "buggy certificate" ; flush stdout) ;None
+
+
+
+
+let psatzl_Z gl =
micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec
[lift_ratproof
(Certificate.linear_prover Certificate.z_spec), "fourier refutation" ] gl
-let qomicron gl =
+let psatzl_Q gl =
micromega_gen parse_qarith Mc.cnf_negate Mc.cnf_normalise qq_domain_spec
[ Certificate.linear_prover Certificate.q_spec, "fourier refutation" ] gl
-let romicron gl =
+let psatz_Q i gl =
+ micromega_gen parse_qarith Mc.cnf_negate Mc.cnf_normalise qq_domain_spec
+ [ call_csdpcert_q ("real_nonlinear_prover", Some i), "fourier refutation" ] gl
+
+let psatzl_R gl =
micromega_gen parse_rarith Mc.cnf_negate Mc.cnf_normalise rz_domain_spec
[ Certificate.linear_prover Certificate.z_spec, "fourier refutation" ] gl
-let rmicromega i gl =
- micromega_gen parse_rarith Mc.negate Mc.normalise rz_domain_spec
- [ call_csdpcert ("real_nonlinear_prover", Some i), "fourier refutation" ] gl
+let psatz_R i gl =
+ micromega_gen parse_rarith Mc.cnf_negate Mc.cnf_normalise rz_domain_spec
+ [ call_csdpcert_z ("real_nonlinear_prover", Some i), "fourier refutation" ] gl
-let micromega i gl =
+let psatz_Z i gl =
micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec
- [lift_ratproof (call_csdpcert ("real_nonlinear_prover",Some i)),
+ [lift_ratproof (call_csdpcert_z ("real_nonlinear_prover",Some i)),
"fourier refutation" ] gl
-let sos gl =
+let sos_Z gl =
micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec
- [lift_ratproof (call_csdpcert ("pure_sos", None)), "pure sos refutation"] gl
+ [lift_ratproof (call_csdpcert_z ("pure_sos", None)), "pure sos refutation"] gl
+
+let sos_Q gl =
+ micromega_gen parse_qarith Mc.cnf_negate Mc.cnf_normalise qq_domain_spec
+ [call_csdpcert_q ("pure_sos", None), "pure sos refutation"] gl
+
+let sos_R gl =
+ micromega_gen parse_rarith Mc.cnf_negate Mc.cnf_normalise rz_domain_spec
+ [call_csdpcert_z ("pure_sos", None), "pure sos refutation"] gl
+
+
-let zomicron gl =
+let xlia gl =
micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec
[Certificate.zlinear_prover, "zprover"] gl
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-05 23:39:13 +0000