diff options
Diffstat (limited to 'contrib/micromega/coq_micromega.ml')
| -rw-r--r-- | contrib/micromega/coq_micromega.ml | 1286 |
1 files changed, 0 insertions, 1286 deletions
diff --git a/contrib/micromega/coq_micromega.ml b/contrib/micromega/coq_micromega.ml deleted file mode 100644 index b4863ffc..00000000 --- a/contrib/micromega/coq_micromega.ml +++ /dev/null @@ -1,1286 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \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) 2006-2008 *) -(* *) -(************************************************************************) - -open Mutils -let debug = false - -let time str f x = - let t0 = (Unix.times()).Unix.tms_utime in - let res = f x in - let t1 = (Unix.times()).Unix.tms_utime in - (*if debug then*) (Printf.printf "time %s %f\n" str (t1 -. t0) ; - flush stdout); - res - -type ('a,'b) formula = - | TT - | FF - | X of 'b - | A of 'a * Names.name - | C of ('a,'b) formula * ('a,'b) formula * Names.name - | D of ('a,'b) formula * ('a,'b) formula * Names.name - | N of ('a,'b) formula * Names.name - | I of ('a,'b) formula * ('a,'b) formula * Names.name - -let none = Names.Anonymous - -let tag_formula t f = - match f with - | A(x,_) -> A(x,t) - | C(x,y,_) -> C(x,y,t) - | D(x,y,_) -> D(x,y,t) - | N(x,_) -> N(x,t) - | I(x,y,_) -> I(x,y,t) - | _ -> f - -let tt = [] -let ff = [ [] ] - - -type ('constant,'contr) sentence = - ('constant Micromega.formula, 'contr) formula - -let cnf negate normalise f = - let negate a = - CoqToCaml.list (fun cl -> CoqToCaml.list (fun x -> x) cl) (negate a) in - - let normalise a = - CoqToCaml.list (fun cl -> CoqToCaml.list (fun x -> x) cl) (normalise a) in - - let and_cnf x y = x @ y in - let or_clause_cnf t f = List.map (fun x -> t@x ) f in - - let rec or_cnf f f' = - match f with - | [] -> tt - | e :: rst -> (or_cnf rst f') @ (or_clause_cnf e f') in - - let rec xcnf (pol : bool) f = - 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 (* ?? *) - | A(x,t) -> if pol then normalise x else negate x - | N(e,t) -> xcnf (not pol) e - | C(e1,e2,t) -> - (if pol then and_cnf else or_cnf) (xcnf pol e1) (xcnf pol e2) - | D(e1,e2,t) -> - (if pol then or_cnf else and_cnf) (xcnf pol e1) (xcnf pol e2) - | I(e1,e2,t) -> - (if pol then or_cnf else and_cnf) (xcnf (not pol) e1) (xcnf pol e2) in - - xcnf true f - - - -module M = -struct - open Coqlib - open Term - (* let constant = gen_constant_in_modules "Omicron" coq_modules*) - - - let logic_dir = ["Coq";"Logic";"Decidable"] - let coq_modules = - init_modules @ - [logic_dir] @ arith_modules @ zarith_base_modules @ - [ ["Coq";"Lists";"List"]; - ["ZMicromega"]; - ["Tauto"]; - ["RingMicromega"]; - ["EnvRing"]; - ["Coq"; "micromega"; "ZMicromega"]; - ["Coq" ; "micromega" ; "Tauto"]; - ["Coq" ; "micromega" ; "RingMicromega"]; - ["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 - - let coq_and = lazy (constant "and") - let coq_or = lazy (constant "or") - let coq_not = lazy (constant "not") - let coq_iff = lazy (constant "iff") - let coq_True = lazy (constant "True") - let coq_False = lazy (constant "False") - - let coq_cons = lazy (constant "cons") - let coq_nil = lazy (constant "nil") - let coq_list = lazy (constant "list") - - let coq_O = lazy (constant "O") - let coq_S = lazy (constant "S") - let coq_nat = lazy (constant "nat") - - let coq_NO = lazy - (gen_constant_in_modules "N" [ ["Coq";"NArith";"BinNat" ]] "N0") - let coq_Npos = lazy - (gen_constant_in_modules "N" [ ["Coq";"NArith"; "BinNat"]] "Npos") - (* let coq_n = lazy (constant "N")*) - - let coq_pair = lazy (constant "pair") - let coq_None = lazy (constant "None") - let coq_option = lazy (constant "option") - let coq_positive = lazy (constant "positive") - let coq_xH = lazy (constant "xH") - let coq_xO = lazy (constant "xO") - let coq_xI = lazy (constant "xI") - - let coq_N0 = lazy (constant "N0") - let coq_N0 = lazy (constant "Npos") - - - let coq_Z = lazy (constant "Z") - let coq_Q = lazy (constant "Q") - let coq_R = lazy (constant "R") - - let coq_ZERO = lazy (constant "Z0") - let coq_POS = lazy (constant "Zpos") - let coq_NEG = lazy (constant "Zneg") - - let coq_QWitness = lazy - (gen_constant_in_modules "QMicromega" - [["Coq"; "micromega"; "QMicromega"]] "QWitness") - let coq_ZWitness = lazy - (gen_constant_in_modules "QMicromega" - [["Coq"; "micromega"; "ZMicromega"]] "ZWitness") - - - let coq_Build_Witness = lazy (constant "Build_Witness") - - - 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") - let coq_cutProof = lazy (constant "CutProof") - let coq_enumProof = lazy (constant "EnumProof") - - let coq_Zgt = lazy (constant "Zgt") - let coq_Zge = lazy (constant "Zge") - let coq_Zle = lazy (constant "Zle") - let coq_Zlt = lazy (constant "Zlt") - let coq_Eq = lazy (constant "eq") - - let coq_Zplus = lazy (constant "Zplus") - 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") - let coq_PEadd = lazy (constant "PEadd") - let coq_PEopp = lazy (constant "PEopp") - let coq_PEmul = lazy (constant "PEmul") - let coq_PEsub = lazy (constant "PEsub") - let coq_PEpow = lazy (constant "PEpow") - - - let coq_OpEq = lazy (constant "OpEq") - let coq_OpNEq = lazy (constant "OpNEq") - let coq_OpLe = lazy (constant "OpLe") - let coq_OpLt = lazy (constant "OpLt") - let coq_OpGe = lazy (constant "OpGe") - let coq_OpGt = lazy (constant "OpGt") - - - let coq_S_In = lazy (constant "S_In") - let coq_S_Square = lazy (constant "S_Square") - let coq_S_Monoid = lazy (constant "S_Monoid") - let coq_S_Ideal = lazy (constant "S_Ideal") - let coq_S_Mult = lazy (constant "S_Mult") - let coq_S_Add = lazy (constant "S_Add") - let coq_S_Pos = lazy (constant "S_Pos") - let coq_S_Z = lazy (constant "S_Z") - let coq_coneMember = lazy (constant "coneMember") - - - let coq_make_impl = lazy - (gen_constant_in_modules "Zmicromega" [["Refl"]] "make_impl") - let coq_make_conj = lazy - (gen_constant_in_modules "Zmicromega" [["Refl"]] "make_conj") - - let coq_Build = lazy - (gen_constant_in_modules "RingMicromega" - [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ] - "Build_Formula") - let coq_Cstr = lazy - (gen_constant_in_modules "RingMicromega" - [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ] "Formula") - - - type parse_error = - | Ukn - | BadStr of string - | BadNum of int - | BadTerm of Term.constr - | Msg of string - | Goal of (Term.constr list ) * Term.constr * parse_error - - let string_of_error = function - | Ukn -> "ukn" - | BadStr s -> s - | BadNum i -> string_of_int i - | BadTerm _ -> "BadTerm" - | Msg s -> s - | Goal _ -> "Goal" - - - exception ParseError - - - - - let get_left_construct term = - match Term.kind_of_term term with - | Term.Construct(_,i) -> (i,[| |]) - | Term.App(l,rst) -> - (match Term.kind_of_term l with - | Term.Construct(_,i) -> (i,rst) - | _ -> raise ParseError - ) - | _ -> raise ParseError - - module Mc = Micromega - - let rec parse_nat term = - let (i,c) = get_left_construct term in - match i with - | 1 -> Mc.O - | 2 -> Mc.S (parse_nat (c.(0))) - | i -> raise ParseError - - - let pp_nat o n = Printf.fprintf o "%i" (CoqToCaml.nat n) - - - let rec dump_nat x = - match x with - | Mc.O -> Lazy.force coq_O - | Mc.S p -> Term.mkApp(Lazy.force coq_S,[| dump_nat p |]) - - - let rec parse_positive term = - let (i,c) = get_left_construct term in - match i with - | 1 -> Mc.XI (parse_positive c.(0)) - | 2 -> Mc.XO (parse_positive c.(0)) - | 3 -> Mc.XH - | i -> raise ParseError - - - let rec dump_positive x = - match x with - | Mc.XH -> Lazy.force coq_xH - | Mc.XO p -> Term.mkApp(Lazy.force coq_xO,[| dump_positive p |]) - | Mc.XI p -> Term.mkApp(Lazy.force coq_xI,[| dump_positive p |]) - - let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x) - - - let rec dump_n x = - match x with - | Mc.N0 -> Lazy.force coq_N0 - | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p|]) - - let rec dump_index x = - match x with - | Mc.XH -> Lazy.force coq_xH - | Mc.XO p -> Term.mkApp(Lazy.force coq_xO,[| dump_index p |]) - | Mc.XI p -> Term.mkApp(Lazy.force coq_xI,[| dump_index p |]) - - - let pp_index o x = Printf.fprintf o "%i" (CoqToCaml.index x) - - let rec dump_n x = - match x with - | Mc.N0 -> Lazy.force coq_NO - | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p |]) - - let rec pp_n o x = output_string o (string_of_int (CoqToCaml.n x)) - - let dump_pair t1 t2 dump_t1 dump_t2 (Mc.Pair (x,y)) = - Term.mkApp(Lazy.force coq_pair,[| t1 ; t2 ; dump_t1 x ; dump_t2 y|]) - - - let rec parse_z term = - let (i,c) = get_left_construct term in - match i with - | 1 -> Mc.Z0 - | 2 -> Mc.Zpos (parse_positive c.(0)) - | 3 -> Mc.Zneg (parse_positive c.(0)) - | i -> raise ParseError - - let dump_z x = - match x with - | Mc.Z0 ->Lazy.force coq_ZERO - | Mc.Zpos p -> Term.mkApp(Lazy.force coq_POS,[| dump_positive p|]) - | Mc.Zneg p -> Term.mkApp(Lazy.force coq_NEG,[| dump_positive p|]) - - let pp_z o x = Printf.fprintf o "%i" (CoqToCaml.z x) - -let dump_num bd1 = - Term.mkApp(Lazy.force coq_Qmake, - [|dump_z (CamlToCoq.bigint (numerator bd1)) ; - dump_positive (CamlToCoq.positive_big_int (denominator bd1)) |]) - - -let dump_q q = - Term.mkApp(Lazy.force coq_Qmake, - [| dump_z q.Micromega.qnum ; dump_positive q.Micromega.qden|]) - -let parse_q term = - match Term.kind_of_term term with - | 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 - - - let rec parse_list parse_elt term = - let (i,c) = get_left_construct term in - match i with - | 1 -> Mc.Nil - | 2 -> Mc.Cons(parse_elt c.(1), parse_list parse_elt c.(2)) - | i -> raise ParseError - - - let rec dump_list typ dump_elt l = - match l with - | Mc.Nil -> Term.mkApp(Lazy.force coq_nil,[| typ |]) - | Mc.Cons(e,l) -> Term.mkApp(Lazy.force coq_cons, - [| typ; dump_elt e;dump_list typ dump_elt l|]) - - let rec dump_ml_list typ dump_elt l = - match l with - | [] -> Term.mkApp(Lazy.force coq_nil,[| typ |]) - | e::l -> Term.mkApp(Lazy.force coq_cons, - [| typ; dump_elt e;dump_ml_list typ dump_elt l|]) - - - - let pp_list op cl elt o l = - let rec _pp o l = - match l with - | Mc.Nil -> () - | Mc.Cons(e,Mc.Nil) -> Printf.fprintf o "%a" elt e - | Mc.Cons(e,l) -> Printf.fprintf o "%a ,%a" elt e _pp l in - Printf.fprintf o "%s%a%s" op _pp l cl - - - - let pp_var = pp_positive - let dump_var = dump_positive - - let rec pp_expr o e = - match e with - | Mc.PEX n -> Printf.fprintf o "V %a" pp_var n - | Mc.PEc z -> pp_z o z - | Mc.PEadd(e1,e2) -> Printf.fprintf o "(%a)+(%a)" pp_expr e1 pp_expr e2 - | Mc.PEmul(e1,e2) -> Printf.fprintf o "%a*(%a)" pp_expr e1 pp_expr e2 - | Mc.PEopp e -> Printf.fprintf o "-(%a)" pp_expr e - | Mc.PEsub(e1,e2) -> Printf.fprintf o "(%a)-(%a)" pp_expr e1 pp_expr e2 - | Mc.PEpow(e,n) -> Printf.fprintf o "(%a)^(%a)" pp_expr e pp_n n - - - let dump_expr typ dump_z e = - let rec dump_expr e = - match e with - | Mc.PEX n -> mkApp(Lazy.force coq_PEX,[| typ; dump_var n |]) - | Mc.PEc z -> mkApp(Lazy.force coq_PEc,[| typ ; dump_z z |]) - | Mc.PEadd(e1,e2) -> mkApp(Lazy.force coq_PEadd, - [| typ; dump_expr e1;dump_expr e2|]) - | Mc.PEsub(e1,e2) -> mkApp(Lazy.force coq_PEsub, - [| typ; dump_expr e1;dump_expr e2|]) - | Mc.PEopp e -> mkApp(Lazy.force coq_PEopp, - [| typ; dump_expr e|]) - | Mc.PEmul(e1,e2) -> mkApp(Lazy.force coq_PEmul, - [| typ; dump_expr e1;dump_expr e2|]) - | Mc.PEpow(e,n) -> mkApp(Lazy.force coq_PEpow, - [| typ; dump_expr e; dump_n n|]) - in - dump_expr e - - let rec dump_monoid l = dump_list (Lazy.force coq_nat) dump_nat l - - let rec dump_cone typ dump_z e = - let z = Lazy.force typ in - let rec dump_cone e = - match e with - | Mc.S_In n -> mkApp(Lazy.force coq_S_In,[| z; dump_nat n |]) - | Mc.S_Ideal(e,c) -> mkApp(Lazy.force coq_S_Ideal, - [| z; dump_expr z dump_z e ; dump_cone c |]) - | Mc.S_Square e -> mkApp(Lazy.force coq_S_Square, - [| z;dump_expr z dump_z e|]) - | Mc.S_Monoid l -> mkApp (Lazy.force coq_S_Monoid, - [|z; dump_monoid l|]) - | Mc.S_Add(e1,e2) -> mkApp(Lazy.force coq_S_Add, - [| z; dump_cone e1; dump_cone e2|]) - | Mc.S_Mult(e1,e2) -> mkApp(Lazy.force coq_S_Mult, - [| z; dump_cone e1; dump_cone e2|]) - | Mc.S_Pos p -> mkApp(Lazy.force coq_S_Pos,[| z; dump_z p|]) - | Mc.S_Z -> mkApp( Lazy.force coq_S_Z,[| z|]) in - dump_cone e - - - let pp_cone pp_z o e = - let rec pp_cone o e = - match e with - | Mc.S_In n -> - Printf.fprintf o "(S_In %a)%%nat" pp_nat n - | Mc.S_Ideal(e,c) -> - Printf.fprintf o "(S_Ideal %a %a)" pp_expr e pp_cone c - | Mc.S_Square e -> - Printf.fprintf o "(S_Square %a)" pp_expr e - | Mc.S_Monoid l -> - Printf.fprintf o "(S_Monoid %a)" (pp_list "[" "]" pp_nat) l - | Mc.S_Add(e1,e2) -> - Printf.fprintf o "(S_Add %a %a)" pp_cone e1 pp_cone e2 - | Mc.S_Mult(e1,e2) -> - Printf.fprintf o "(S_Mult %a %a)" pp_cone e1 pp_cone e2 - | Mc.S_Pos p -> - Printf.fprintf o "(S_Pos %a)%%positive" pp_z p - | Mc.S_Z -> - Printf.fprintf o "S_Z" in - pp_cone o e - - - let rec dump_op = function - | Mc.OpEq-> Lazy.force coq_OpEq - | Mc.OpNEq-> Lazy.force coq_OpNEq - | Mc.OpLe -> Lazy.force coq_OpLe - | Mc.OpGe -> Lazy.force coq_OpGe - | Mc.OpGt-> Lazy.force coq_OpGt - | Mc.OpLt-> Lazy.force coq_OpLt - - - - let pp_op o e= - match e with - | Mc.OpEq-> Printf.fprintf o "=" - | Mc.OpNEq-> Printf.fprintf o "<>" - | Mc.OpLe -> Printf.fprintf o "=<" - | Mc.OpGe -> Printf.fprintf o ">=" - | Mc.OpGt-> Printf.fprintf o ">" - | Mc.OpLt-> Printf.fprintf o "<" - - - - - let pp_cstr o {Mc.flhs = l ; Mc.fop = op ; Mc.frhs = r } = - Printf.fprintf o"(%a %a %a)" pp_expr l pp_op op pp_expr r - - let dump_cstr typ dump_constant {Mc.flhs = e1 ; Mc.fop = o ; Mc.frhs = e2} = - Term.mkApp(Lazy.force coq_Build, - [| typ; dump_expr typ dump_constant e1 ; - 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 -> (assoc_const op zop_table, args.(0) , args.(1)) - | Ind(n,0) -> - 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) = - match kind_of_term op with - | Const x -> (assoc_const op rop_table, args.(0) , args.(1)) - | Ind(n,0) -> - 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) = - (assoc_const op qop_table, args.(0) , args.(1)) - - - module Env = - struct - type t = constr list - - let compute_rank_add env v = - let rec _add env n v = - match env with - | [] -> ([v],n) - | e::l -> - if eq_constr 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.idx n) - - - let empty = [] - - let elements env = env - - end - - - let is_constant t = (* This is an approx *) - match kind_of_term t with - | Construct(i,_) -> true - | _ -> false - - - type 'a op = - | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr) - | Opp - | Power - | 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: "); - Pp.pp_flush ();Pp.pp (Printer.prterm term); Pp.pp_flush ()); - - 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 rec parse_expr env term = - let combine env op (t1,t2) = - let (expr1,env) = parse_expr env t1 in - let (expr2,env) = parse_expr env t2 in - (op expr1 expr2,env) in - match kind_of_term term with - | App(t,args) -> - ( - match kind_of_term t with - | Const c -> - ( 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) - | Power -> - let (expr,env) = parse_expr env args.(0) in - let exp = (parse_exp args.(1)) in - (Mc.PEpow(expr, exp) , env) - | 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) - ) - | _ -> constant_or_variable env term - ) - | _ -> constant_or_variable env term in - parse_expr env term - - - 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 = - [ - 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 = - [ - 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] - - - - - -let zconstant = parse_z -let qconstant = parse_q - - -let rconstant term = - if debug - then (Pp.pp_flush (); - Pp.pp (Pp.str "rconstant: "); - Pp.pp (Printer.prterm term); Pp.pp_flush ()); - match Term.kind_of_term term with - | 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 - - -let parse_zexpr = - parse_expr zconstant (fun x -> Mc.n_of_Z (parse_z x)) zop_spec -let parse_qexpr = - parse_expr qconstant (fun x -> Mc.n_of_Z (parse_z x)) qop_spec -let parse_rexpr = - parse_expr rconstant (fun x -> Mc.n_of_nat (parse_nat x)) rop_spec - - - let parse_arith parse_op parse_expr env cstr = - if debug - then (Pp.pp_flush (); - Pp.pp (Pp.str "parse_arith: "); - Pp.pp (Printer.prterm cstr); - Pp.pp_flush ()); - match kind_of_term cstr with - | App(op,args) -> - let (op,lhs,rhs) = parse_op (op,args) in - let (e1,env) = parse_expr env lhs in - let (e2,env) = parse_expr 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 - - let parse_qarith = parse_arith parse_qop parse_qexpr - - let parse_rarith = parse_arith parse_rop parse_rexpr - - - (* generic parsing of arithmetic expressions *) - - - - - let rec f2f = function - | TT -> Mc.TT - | FF -> Mc.FF - | X _ -> Mc.X - | A (x,_) -> Mc.A x - | C (a,b,_) -> Mc.Cj(f2f a,f2f b) - | D (a,b,_) -> Mc.D(f2f a,f2f b) - | N (a,_) -> Mc.N(f2f a) - | I(a,b,_) -> Mc.I(f2f a,f2f b) - - let is_prop t = - match t with - | Names.Anonymous -> true (* Not quite right *) - | Names.Name x -> false - - let mkC f1 f2 = C(f1,f2,none) - let mkD f1 f2 = D(f1,f2,none) - let mkIff f1 f2 = C(I(f1,f2,none),I(f2,f2,none),none) - let mkI f1 f2 = I(f1,f2,none) - - let mkformula_binary g term f1 f2 = - match f1 , f2 with - | X _ , X _ -> X(term) - | _ -> g f1 f2 - - let parse_formula parse_atom env term = - let parse_atom env t = try let (at,env) = parse_atom env t in (A(at,none), env) with _ -> (X(t),env) in - - let rec xparse_formula env term = - match kind_of_term term with - | App(l,rst) -> - (match rst with - | [|a;b|] when l = Lazy.force coq_and -> - let f,env = xparse_formula env a in - let g,env = xparse_formula env b in - mkformula_binary mkC term f g,env - | [|a;b|] when l = Lazy.force coq_or -> - let f,env = xparse_formula env a in - let g,env = xparse_formula env b in - mkformula_binary mkD term f g,env - | [|a|] when l = Lazy.force coq_not -> - let (f,env) = xparse_formula env a in (N(f,none), env) - | [|a;b|] when l = Lazy.force coq_iff -> - let f,env = xparse_formula env a in - let g,env = xparse_formula env b in - mkformula_binary mkIff term f g,env - | _ -> parse_atom env term) - | Prod(typ,a,b) when not (Termops.dependent (mkRel 1) b) -> - let f,env = xparse_formula env a in - let g,env = xparse_formula env b in - mkformula_binary mkI term f g,env - | _ when term = Lazy.force coq_True -> (TT,env) - | _ when term = Lazy.force coq_False -> (FF,env) - | _ -> X(term),env in - xparse_formula env term - - let coq_TT = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "TT") - let coq_FF = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "FF") - let coq_And = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "Cj") - let coq_Or = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "D") - let coq_Neg = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "N") - let coq_Atom = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "A") - let coq_X = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "X") - let coq_Impl = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "I") - let coq_Formula = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "BFormula") - - let dump_formula typ dump_atom f = - let rec xdump f = - match f with - | TT -> mkApp(Lazy.force coq_TT,[| typ|]) - | FF -> mkApp(Lazy.force coq_FF,[| typ|]) - | C(x,y,_) -> mkApp(Lazy.force coq_And,[| typ ; xdump x ; xdump y|]) - | D(x,y,_) -> mkApp(Lazy.force coq_Or,[| typ ; xdump x ; xdump y|]) - | I(x,y,_) -> mkApp(Lazy.force coq_Impl,[| typ ; xdump x ; xdump y|]) - | N(x,_) -> mkApp(Lazy.force coq_Neg,[| typ ; xdump x|]) - | A(x,_) -> mkApp(Lazy.force coq_Atom,[| typ ; dump_atom x|]) - | X(t) -> mkApp(Lazy.force coq_X,[| typ ; t|]) in - - xdump f - - - - - (* ! reverse the list of bindings *) - let set l concl = - let rec _set acc = function - | [] -> acc - | (e::l) -> - let (name,expr,typ) = e in - _set (Term.mkNamedLetIn - (Names.id_of_string name) - expr typ acc) l in - _set concl l - - -end - -open M - - -let rec sig_of_cone = function - | Mc.S_In n -> [CoqToCaml.nat n] - | Mc.S_Ideal(e,w) -> sig_of_cone w - | Mc.S_Mult(w1,w2) -> - (sig_of_cone w1)@(sig_of_cone w2) - | Mc.S_Add(w1,w2) -> (sig_of_cone w1)@(sig_of_cone w2) - | _ -> [] - -let same_proof sg cl1 cl2 = - let cl1 = CoqToCaml.list (fun x -> x) cl1 in - let cl2 = CoqToCaml.list (fun x -> x) cl2 in - let rec xsame_proof sg = - match sg with - | [] -> true - | n::sg -> (try List.nth cl1 n = List.nth cl2 n with _ -> false) - && (xsame_proof sg ) in - xsame_proof sg - - - - -let tags_of_clause tgs wit clause = - let rec xtags tgs = function - | Mc.S_In n -> Names.Idset.union tgs - (snd (List.nth clause (CoqToCaml.nat n) )) - | Mc.S_Ideal(e,w) -> xtags tgs w - | Mc.S_Mult (w1,w2) | Mc.S_Add(w1,w2) -> xtags (xtags tgs w1) w2 - | _ -> tgs in - xtags tgs wit - -let tags_of_cnf wits cnf = - List.fold_left2 (fun acc w cl -> tags_of_clause acc w cl) - Names.Idset.empty wits cnf - - -let find_witness prover polys1 = - let l = CoqToCaml.list (fun x -> x) polys1 in - try_any prover l - -let rec witness prover l1 l2 = - match l2 with - | Micromega.Nil -> Some (Micromega.Nil) - | Micromega.Cons(e,l2) -> - match find_witness prover (Micromega.Cons( e,l1)) with - | None -> None - | Some w -> - (match witness prover l1 l2 with - | None -> None - | Some l -> Some (Micromega.Cons (w,l)) - ) - - -let rec apply_ids t ids = - match ids with - | [] -> t - | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids - - -let coq_Node = lazy - (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node") -let coq_Leaf = lazy - (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf") -let coq_Empty = lazy - (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty") - - -let btree_of_array typ a = - let size_of_a = Array.length a in - let semi_size_of_a = size_of_a lsr 1 in - let node = Lazy.force coq_Node - and leaf = Lazy.force coq_Leaf - and empty = Term.mkApp (Lazy.force coq_Empty, [| typ |]) in - let rec aux n = - if n > size_of_a - then empty - else if n > semi_size_of_a - then Term.mkApp (leaf, [| typ; a.(n-1) |]) - else Term.mkApp (node, [| typ; aux (2*n); a.(n-1); aux (2*n+1) |]) - in - aux 1 - -let btree_of_array typ a = - try - btree_of_array typ a - with x -> - failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x)) - -let dump_varmap typ env = - btree_of_array typ (Array.of_list env) - - -let rec pp_varmap o vm = - match vm with - | Mc.Empty -> output_string o "[]" - | Mc.Leaf z -> Printf.fprintf o "[%a]" pp_z z - | Mc.Node(l,z,r) -> Printf.fprintf o "[%a, %a, %a]" pp_varmap l pp_z z pp_varmap r - - - -let rec dump_proof_term = function - | Micromega.RatProof cone -> - Term.mkApp(Lazy.force coq_ratProof, [|dump_cone coq_Z dump_z cone|]) - | Micromega.CutProof(e,q,cone,prf) -> - Term.mkApp(Lazy.force coq_cutProof, - [| dump_expr (Lazy.force coq_Z) dump_z e ; - dump_q q ; - dump_cone coq_Z dump_z cone ; - dump_proof_term prf|]) - | Micromega.EnumProof( q1,e1,q2,c1,c2,prfs) -> - Term.mkApp (Lazy.force coq_enumProof, - [| dump_q q1 ; dump_expr (Lazy.force coq_Z) dump_z e1 ; dump_q q2; - dump_cone coq_Z dump_z c1 ; dump_cone coq_Z dump_z c2 ; - dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |]) - -let pp_q o q = Printf.fprintf o "%a/%a" pp_z q.Micromega.qnum pp_positive q.Micromega.qden - - -let rec pp_proof_term o = function - | Micromega.RatProof cone -> Printf.fprintf o "R[%a]" (pp_cone pp_z) cone - | Micromega.CutProof(e,q,_,p) -> failwith "not implemented" - | Micromega.EnumProof(q1,e1,q2,c1,c2,rst) -> - Printf.fprintf o "EP[%a,%a,%a,%a,%a,%a]" - pp_q q1 pp_expr e1 pp_q q2 (pp_cone pp_z) c1 (pp_cone pp_z) c2 - (pp_list "[" "]" pp_proof_term) rst - -let rec parse_hyps parse_arith env hyps = - match hyps with - | [] -> ([],env) - | (i,t)::l -> - let (lhyps,env) = parse_hyps parse_arith env l in - try - let (c,env) = parse_formula parse_arith env t in - ((i,c)::lhyps, env) - with _ -> (lhyps,env) - (*(if debug then Printf.printf "parse_arith : %s\n" x);*) - - -exception ParseError - -let parse_goal parse_arith env hyps term = - (* try*) - let (f,env) = parse_formula parse_arith env term in - let (lhyps,env) = parse_hyps parse_arith env hyps in - (lhyps,f,env) - (* with Failure x -> raise ParseError*) - - -type ('a, 'b) domain_spec = { - typ : Term.constr; (* Z, Q , R *) - coeff : Term.constr ; (* Z, Q *) - dump_coeff : 'a -> Term.constr ; - proof_typ : Term.constr ; - dump_proof : 'b -> Term.constr -} - -let zz_domain_spec = lazy { - typ = Lazy.force coq_Z; - coeff = Lazy.force coq_Z; - dump_coeff = dump_z ; - proof_typ = Lazy.force coq_proofTerm ; - dump_proof = dump_proof_term -} - -let qq_domain_spec = lazy { - typ = Lazy.force coq_Q; - coeff = Lazy.force coq_Q; - dump_coeff = dump_q ; - proof_typ = Lazy.force coq_QWitness ; - dump_proof = dump_cone coq_Q dump_q -} - -let rz_domain_spec = lazy { - typ = Lazy.force coq_R; - coeff = Lazy.force coq_Z; - dump_coeff = dump_z; - proof_typ = Lazy.force coq_ZWitness ; - dump_proof = dump_cone coq_Z dump_z -} - - - - -let micromega_order_change spec cert cert_typ env ff gl = - let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in - - let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in - let vm = dump_varmap ( spec.typ) env in - Tactics.change_in_concl None - (set - [ - ("__ff", ff, Term.mkApp(Lazy.force coq_Formula ,[| formula_typ |])); - ("__varmap", vm , Term.mkApp - (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "t", [| spec.typ|])); - ("__wit", cert,cert_typ) - ] - (Tacmach.pf_concl gl ) - - ) - gl - - -let detect_duplicates cnf wit = - let cnf = CoqToCaml.list (fun x -> x) cnf in - let wit = CoqToCaml.list (fun x -> x) wit in - - let rec xdup cnf wit = - match wit with - | [] -> [] - | w :: wit -> - let sg = sig_of_cone w in - match cnf with - | [] -> [] - | e::cnf -> - let (dups,cnf) = (List.partition (fun x -> same_proof sg e x) cnf) in - dups@(xdup cnf wit) in - xdup cnf wit - -let find_witness prover polys1 = - try_any prover polys1 - - -let witness_list_with_tags prover l = - - let rec xwitness_list l = - match l with - | [] -> Some([]) - | e::l -> - match find_witness prover (List.map fst e) with - | None -> None - | Some w -> - (match xwitness_list l with - | None -> None - | Some l -> Some (w::l) - ) in - xwitness_list l - -let witness_list_without_tags prover l = - - let rec xwitness_list l = - match l with - | [] -> Some([]) - | 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 - -let witness_list prover l = - let rec xwitness_list l = - match l with - | Micromega.Nil -> Some(Micromega.Nil) - | Micromega.Cons(e,l) -> - match find_witness prover e with - | None -> None - | Some w -> - (match xwitness_list l with - | None -> None - | Some l -> Some (Micromega.Cons(w,l)) - ) in - xwitness_list l - - - - -let is_singleton = function [] -> true | [e] -> true | _ -> false - - -let micromega_tauto negate normalise spec prover env polys1 polys2 gl = - let spec = Lazy.force spec in - let (ff,ids) = - List.fold_right - (fun (id,f) (cc,ids) -> - match f with - X _ -> (cc,ids) - | _ -> (I(tag_formula (Names.Name id) f,cc,none), id::ids)) - polys1 (polys2,[]) in - - let cnf_ff = cnf negate normalise ff in - - if debug then - (Pp.pp (Pp.str "Formula....\n") ; - let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in - let ff = dump_formula formula_typ - (dump_cstr spec.typ spec.dump_coeff) ff in - Pp.pp (Printer.prterm ff) ; Pp.pp_flush ()) ; - - match witness_list_without_tags prover cnf_ff with - | None -> Tacticals.tclFAIL 0 (Pp.str "Cannot find witness") gl - | Some res -> (*Printf.printf "\nList %i" (List.length res); *) - let (ff,res,ids) = (ff,res,List.map Term.mkVar ids) in - let res' = dump_ml_list (spec.proof_typ) spec.dump_proof res in - (Tacticals.tclTHENSEQ - [ - Tactics.generalize ids; - micromega_order_change spec res' - (Term.mkApp(Lazy.force coq_list,[| spec.proof_typ|])) env ff ; - ]) gl - - -let micromega_gen parse_arith negate normalise spec prover gl = - let concl = Tacmach.pf_concl gl in - let hyps = Tacmach.pf_hyps_types gl in - try - let (hyps,concl,env) = parse_goal parse_arith Env.empty hyps concl in - let env = Env.elements env in - micromega_tauto negate normalise spec prover env hyps concl gl - with - | Failure x -> flush stdout ; Pp.pp_flush () ; - Tacticals.tclFAIL 0 (Pp.str x) gl - | ParseError -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl - - -let lift_ratproof prover l = - match prover l with - | None -> None - | Some c -> Some (Mc.RatProof c) - - -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 = - let tmp_to,ch_to = Filename.open_temp_file "csdpcert" ".in" in - let tmp_from = Filename.temp_file "csdpcert" ".out" in - output_value ch_to (provername,poly : provername * micromega_polys); - close_out ch_to; - let cmdname = - List.fold_left Filename.concat (Envars.coqlib ()) - ["contrib"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in - let c = Sys.command (cmdname ^" "^ tmp_to ^" "^ tmp_from) in - (try Sys.remove tmp_to with _ -> ()); - if c <> 0 then Util.error ("Failed to call csdp certificate generator"); - let ch_from = open_in tmp_from in - let cert = (input_value ch_from : csdpcert) in - close_in ch_from; Sys.remove tmp_from; - cert - -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 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 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 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 psatz_Z i gl = - micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec - [lift_ratproof (call_csdpcert_z ("real_nonlinear_prover",Some i)), - "fourier refutation" ] gl - - -let sos_Z gl = - micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec - [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 xlia gl = - micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec - [Certificate.zlinear_prover, "zprover"] gl |