diff options
| author | Maxime Dénès | 2020-06-15 11:46:25 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-06-15 11:46:25 +0200 |
| commit | 90345eb092f9e3fc7ef1bdfe7f61cb913cb53d18 (patch) | |
| tree | 98e649d22b8342a4c675a8077c372c8fc4dec34f | |
| parent | 61b63e09e4b5ce428bc8e8c038efe93560f328ff (diff) | |
| parent | 12e9f7ea1a2ae3111805fc42f8d75a1a24c36e3f (diff) | |
Merge PR #11906: [micromega] native support for boolean operators
Reviewed-by: maximedenes
Reviewed-by: pi8027
Reviewed-by: vbgl
| -rw-r--r-- | doc/changelog/04-tactics/11906-micromega-booleans.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 64 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 529 | ||||
| -rw-r--r-- | plugins/micromega/g_zify.mlg | 50 | ||||
| -rw-r--r-- | plugins/micromega/micromega.ml | 623 | ||||
| -rw-r--r-- | plugins/micromega/micromega.mli | 293 | ||||
| -rw-r--r-- | plugins/micromega/zify.ml | 128 | ||||
| -rw-r--r-- | plugins/micromega/zify.mli | 3 | ||||
| -rw-r--r-- | test-suite/micromega/zify.v | 229 | ||||
| -rw-r--r-- | theories/Bool/Bool.v | 2 | ||||
| -rw-r--r-- | theories/Init/Datatypes.v | 1 | ||||
| -rw-r--r-- | theories/ZArith/BinInt.v | 7 | ||||
| -rw-r--r-- | theories/micromega/Lia.v | 2 | ||||
| -rw-r--r-- | theories/micromega/QMicromega.v | 73 | ||||
| -rw-r--r-- | theories/micromega/RMicromega.v | 124 | ||||
| -rw-r--r-- | theories/micromega/Tauto.v | 2247 | ||||
| -rw-r--r-- | theories/micromega/ZMicromega.v | 78 | ||||
| -rw-r--r-- | theories/micromega/ZifyBool.v | 261 | ||||
| -rw-r--r-- | theories/micromega/ZifyClasses.v | 45 | ||||
| -rw-r--r-- | theories/micromega/ZifyComparison.v | 14 | ||||
| -rw-r--r-- | theories/micromega/ZifyInst.v | 231 |
21 files changed, 3336 insertions, 1672 deletions
diff --git a/doc/changelog/04-tactics/11906-micromega-booleans.rst b/doc/changelog/04-tactics/11906-micromega-booleans.rst new file mode 100644 index 0000000000..39d1525ac3 --- /dev/null +++ b/doc/changelog/04-tactics/11906-micromega-booleans.rst @@ -0,0 +1,4 @@ +- **Added:** + :tacn:`lia` is extended to deal with boolean operators e.g. `andb` or `Z.leb`. + (As `lia` gets more powerful, this may break proof scripts relying on `lia` failure.) + (`#11906 <https://github.com/coq/coq/pull/11906>`_, by Frédéric Besson). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 77bf58aac6..c4947e6b3a 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -64,16 +64,23 @@ arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\math The syntax of the formulas is the following: .. productionlist:: F - F : A ∣ P ∣ True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F + F : A ∣ P | True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F | F = F A : p = p ∣ p > p ∣ p < p ∣ p ≥ p ∣ p ≤ p p : c ∣ x ∣ −p ∣ p − p ∣ p + p ∣ p × p ∣ p ^ n -where :math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the +where :math:`F` is interpreted over either `Prop` or `bool`, +:math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the operators :math:`−, +, ×` are respectively subtraction, addition, and product; :math:`p ^ n` is exponentiation by a constant :math:`n`, :math:`P` is an arbitrary proposition. For :math:`\mathbb{Q}`, equality is not Leibniz equality ``=`` but the equality of rationals ``==``. +When :math:`F` is interpreted over `bool`, the boolean operators are +`&&`, `||`, `Bool.eqb`, `Bool.implb`, `Bool.negb` and the comparisons +in :math:`A` are also interpreted over the booleans (e.g., for +:math:`\mathbb{Z}`, we have `Z.eqb`, `Z.gtb`, `Z.ltb`, `Z.geb`, +`Z.leb`). + For :math:`\mathbb{Z}` (resp. :math:`\mathbb{Q}`), :math:`c` ranges over integer constants (resp. rational constants). For :math:`\mathbb{R}`, the tactic recognizes as real constants the following expressions: @@ -277,37 +284,54 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``. + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations``. + The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands. + The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``. -.. cmd:: Show Zify InjTyp - :name: Show Zify InjTyp +.. cmd:: Add Zify {| InjTyp | BinOp | UnOp |CstOp | BinRel | UnOpSpec | BinOpSpec } @qualid - This command shows the list of types that can be injected into :g:`Z`. + This command registers an instance of one of the typeclasses among ``InjTyp``, ``BinOp``, ``UnOp``, ``CstOp``, ``BinRel``, + ``UnOpSpec``, ``BinOpSpec``. -.. cmd:: Show Zify BinOp - :name: Show Zify BinOp +.. cmd:: Show Zify {| InjTyp | BinOp | UnOp |CstOp | BinRel | UnOpSpec | BinOpSpec } - This command shows the list of binary operators processed by :tacn:`zify`. + The command prints the typeclass instances of one the typeclasses + among ``InjTyp``, ``BinOp``, ``UnOp``, ``CstOp``, ``BinRel``, + ``UnOpSpec``, ``BinOpSpec``. For instance, :cmd:`Show Zify` ``InjTyp`` + prints the list of types that supported by :tacn:`zify` i.e., + :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`. -.. cmd:: Show Zify BinRel - :name: Show Zify BinRel +.. cmd:: Show Zify Spec - This command shows the list of binary relations processed by :tacn:`zify`. + .. deprecated:: 8.13 + Use instead either :cmd:`Show Zify` ``UnOpSpec`` or :cmd:`Show Zify` ``BinOpSpec``. +.. cmd:: Add InjTyp -.. cmd:: Show Zify UnOp - :name: Show Zify UnOp + .. deprecated:: 8.13 + Use instead either :cmd:`Add Zify` ``InjTyp``. - This command shows the list of unary operators processed by :tacn:`zify`. +.. cmd:: Add BinOp -.. cmd:: Show Zify CstOp - :name: Show Zify CstOp + .. deprecated:: 8.13 + Use instead either :cmd:`Add Zify` ``BinOp``. + +.. cmd:: Add UnOp + + .. deprecated:: 8.13 + Use instead either :cmd:`Add Zify` ``UnOp``. + +.. cmd:: Add CstOp + + .. deprecated:: 8.13 + Use instead either :cmd:`Add Zify` ``CstOp``. + +.. cmd:: Add BinRel + + .. deprecated:: 8.13 + Use instead either :cmd:`Add Zify` ``BinRel``. - This command shows the list of constants processed by :tacn:`zify`. -.. cmd:: Show Zify Spec - :name: Show Zify Spec - This command shows the list of operators over :g:`Z` that are compiled using their specification e.g., :g:`Z.min`. .. [#csdp] Sources and binaries can be found at https://projects.coin-or.org/Csdp .. [#fnpsatz] Variants deal with equalities and strict inequalities. diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 0f8d941b41..44bc20e55f 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -86,20 +86,30 @@ type 'cst formula = type 'cst clause = ('cst Mc.nFormula, tag * EConstr.constr) Mc.clause type 'cst cnf = ('cst Mc.nFormula, tag * EConstr.constr) Mc.cnf +let pp_kind o = function + | Mc.IsProp -> output_string o "Prop" + | Mc.IsBool -> output_string o "bool" + +let kind_is_prop = function Mc.IsProp -> true | Mc.IsBool -> false + let rec pp_formula o (f : 'cst formula) = Mc.( match f with - | TT -> output_string o "tt" - | FF -> output_string o "ff" - | X c -> output_string o "X " - | A (_, (t, _)) -> Printf.fprintf o "A(%a)" Tag.pp t - | Cj (f1, f2) -> Printf.fprintf o "C(%a,%a)" pp_formula f1 pp_formula f2 - | D (f1, f2) -> Printf.fprintf o "D(%a,%a)" pp_formula f1 pp_formula f2 - | I (f1, n, f2) -> - Printf.fprintf o "I(%a,%s,%a)" pp_formula f1 + | TT k -> output_string o (if kind_is_prop k then "True" else "true") + | FF k -> output_string o (if kind_is_prop k then "False" else "false") + | X (k, c) -> Printf.fprintf o "X %a" pp_kind k + | A (_, _, (t, _)) -> Printf.fprintf o "A(%a)" Tag.pp t + | AND (_, f1, f2) -> + Printf.fprintf o "AND(%a,%a)" pp_formula f1 pp_formula f2 + | OR (_, f1, f2) -> Printf.fprintf o "OR(%a,%a)" pp_formula f1 pp_formula f2 + | IMPL (_, f1, n, f2) -> + Printf.fprintf o "IMPL(%a,%s,%a)" pp_formula f1 (match n with Some id -> Names.Id.to_string id | None -> "") pp_formula f2 - | N f -> Printf.fprintf o "N(%a)" pp_formula f) + | NOT (_, f) -> Printf.fprintf o "NOT(%a)" pp_formula f + | IFF (_, f1, f2) -> + Printf.fprintf o "IFF(%a,%a)" pp_formula f1 pp_formula f2 + | EQ (f1, f2) -> Printf.fprintf o "EQ(%a,%a)" pp_formula f1 pp_formula f2) (** * Given a set of integers s=\{i0,...,iN\} and a list m, return the list of @@ -142,6 +152,14 @@ module M = struct let coq_iff = lazy (constr_of_ref "core.iff.type") let coq_True = lazy (constr_of_ref "core.True.type") let coq_False = lazy (constr_of_ref "core.False.type") + let coq_bool = lazy (constr_of_ref "core.bool.type") + let coq_true = lazy (constr_of_ref "core.bool.true") + let coq_false = lazy (constr_of_ref "core.bool.false") + let coq_andb = lazy (constr_of_ref "core.bool.andb") + let coq_orb = lazy (constr_of_ref "core.bool.orb") + let coq_implb = lazy (constr_of_ref "core.bool.implb") + let coq_eqb = lazy (constr_of_ref "core.bool.eqb") + let coq_negb = lazy (constr_of_ref "core.bool.negb") let coq_cons = lazy (constr_of_ref "core.list.cons") let coq_nil = lazy (constr_of_ref "core.list.nil") let coq_list = lazy (constr_of_ref "core.list.type") @@ -186,11 +204,18 @@ module M = struct let coq_cutProof = lazy (constr_of_ref "micromega.ZArithProof.CutProof") let coq_enumProof = lazy (constr_of_ref "micromega.ZArithProof.EnumProof") let coq_ExProof = lazy (constr_of_ref "micromega.ZArithProof.ExProof") + let coq_IsProp = lazy (constr_of_ref "micromega.kind.isProp") + let coq_IsBool = lazy (constr_of_ref "micromega.kind.isBool") let coq_Zgt = lazy (constr_of_ref "num.Z.gt") let coq_Zge = lazy (constr_of_ref "num.Z.ge") let coq_Zle = lazy (constr_of_ref "num.Z.le") let coq_Zlt = lazy (constr_of_ref "num.Z.lt") - let coq_Eq = lazy (constr_of_ref "core.eq.type") + let coq_Zgtb = lazy (constr_of_ref "num.Z.gtb") + let coq_Zgeb = lazy (constr_of_ref "num.Z.geb") + let coq_Zleb = lazy (constr_of_ref "num.Z.leb") + let coq_Zltb = lazy (constr_of_ref "num.Z.ltb") + let coq_Zeqb = lazy (constr_of_ref "num.Z.eqb") + let coq_eq = lazy (constr_of_ref "core.eq.type") let coq_Zplus = lazy (constr_of_ref "num.Z.add") let coq_Zminus = lazy (constr_of_ref "num.Z.sub") let coq_Zopp = lazy (constr_of_ref "num.Z.opp") @@ -248,13 +273,16 @@ module M = struct let coq_TT = lazy (constr_of_ref "micromega.GFormula.TT") let coq_FF = lazy (constr_of_ref "micromega.GFormula.FF") - let coq_And = lazy (constr_of_ref "micromega.GFormula.Cj") - let coq_Or = lazy (constr_of_ref "micromega.GFormula.D") - let coq_Neg = lazy (constr_of_ref "micromega.GFormula.N") + let coq_AND = lazy (constr_of_ref "micromega.GFormula.AND") + let coq_OR = lazy (constr_of_ref "micromega.GFormula.OR") + let coq_NOT = lazy (constr_of_ref "micromega.GFormula.NOT") let coq_Atom = lazy (constr_of_ref "micromega.GFormula.A") let coq_X = lazy (constr_of_ref "micromega.GFormula.X") - let coq_Impl = lazy (constr_of_ref "micromega.GFormula.I") + let coq_IMPL = lazy (constr_of_ref "micromega.GFormula.IMPL") + let coq_IFF = lazy (constr_of_ref "micromega.GFormula.IFF") + let coq_EQ = lazy (constr_of_ref "micromega.GFormula.EQ") let coq_Formula = lazy (constr_of_ref "micromega.BFormula.type") + let coq_eKind = lazy (constr_of_ref "micromega.eKind") (** * Initialization : a few Caml symbols are derived from other libraries; @@ -557,52 +585,56 @@ module M = struct (List.find (fun (x', y) -> EConstr.eq_constr sigma x (Lazy.force x')) l) with Not_found -> raise ParseError - let zop_table = + let zop_table_prop = [ (coq_Zgt, Mc.OpGt) ; (coq_Zge, Mc.OpGe) ; (coq_Zlt, Mc.OpLt) ; (coq_Zle, Mc.OpLe) ] - let rop_table = + let zop_table_bool = + [ (coq_Zgtb, Mc.OpGt) + ; (coq_Zgeb, Mc.OpGe) + ; (coq_Zltb, Mc.OpLt) + ; (coq_Zleb, Mc.OpLe) + ; (coq_Zeqb, Mc.OpEq) ] + + let rop_table_prop = [ (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 rop_table_bool = [] + + let qop_table_prop = + [(coq_Qlt, Mc.OpLt); (coq_Qle, Mc.OpLe); (coq_Qeq, Mc.OpEq)] + + let qop_table_bool = [] type gl = {env : Environ.env; sigma : Evd.evar_map} let is_convertible gl t1 t2 = Reductionops.is_conv gl.env gl.sigma t1 t2 - let parse_zop gl (op, args) = + let parse_operator table_prop table_bool has_equality typ gl k (op, args) = let sigma = gl.sigma in match args with - | [|a1; a2|] -> (assoc_const sigma op zop_table, a1, a2) + | [|a1; a2|] -> + ( assoc_const sigma op + (match k with Mc.IsProp -> table_prop | Mc.IsBool -> table_bool) + , a1 + , a2 ) | [|ty; a1; a2|] -> if - EConstr.eq_constr sigma op (Lazy.force coq_Eq) - && is_convertible gl ty (Lazy.force coq_Z) + has_equality + && EConstr.eq_constr sigma op (Lazy.force coq_eq) + && is_convertible gl ty (Lazy.force typ) then (Mc.OpEq, args.(1), args.(2)) else raise ParseError | _ -> raise ParseError - let parse_rop gl (op, args) = - let sigma = gl.sigma in - match args with - | [|a1; a2|] -> (assoc_const sigma op rop_table, a1, a2) - | [|ty; a1; a2|] -> - if - EConstr.eq_constr sigma op (Lazy.force coq_Eq) - && is_convertible gl ty (Lazy.force coq_R) - then (Mc.OpEq, a1, a2) - else raise ParseError - | _ -> raise ParseError - - let parse_qop gl (op, args) = - if Array.length args = 2 then - (assoc_const gl.sigma op qop_table, args.(0), args.(1)) - else raise ParseError + let parse_zop = parse_operator zop_table_prop zop_table_bool true coq_Z + let parse_rop = parse_operator rop_table_prop [] true coq_R + let parse_qop = parse_operator qop_table_prop [] false coq_R type 'a op = | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr) @@ -622,7 +654,7 @@ module M = struct module Env = struct type t = - { vars : EConstr.t list + { vars : (EConstr.t * Mc.kind) list ; (* The list represents a mapping from EConstr.t to indexes. *) gl : gl (* The evar_map may be updated due to unification of universes *) } @@ -642,16 +674,16 @@ module M = struct | exception Univ.UniverseInconsistency _ -> None ) | None -> None - let compute_rank_add env v = + let compute_rank_add env v is_prop = let rec _add gl vars n v = match vars with - | [] -> (gl, [v], n) - | e :: l -> ( + | [] -> (gl, [(v, is_prop)], n) + | (e, b) :: l -> ( match eq_constr gl e v with | Some gl' -> (gl', vars, n) | None -> let gl, l', n = _add gl l (n + 1) v in - (gl, e :: l', n) ) + (gl, (e, b) :: l', n) ) in let gl', vars', n = _add env.gl env.vars 1 v in ({vars = vars'; gl = gl'}, CamlToCoq.positive n) @@ -661,7 +693,7 @@ module M = struct let rec _get_rank env n = match env with | [] -> raise (Invalid_argument "get_rank") - | e :: l -> ( + | (e, _) :: l -> ( match eq_constr gl e v with Some _ -> n | None -> _get_rank l (n + 1) ) in @@ -682,7 +714,7 @@ module M = struct let pp gl env = let ppl = List.mapi - (fun i e -> + (fun i (e, _) -> Pp.str "x" ++ Pp.int (i + 1) ++ Pp.str ":" @@ -703,7 +735,7 @@ module M = struct Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env gl.env gl.sigma term); let parse_variable env term = - let env, n = Env.compute_rank_add env term in + let env, n = Env.compute_rank_add env term Mc.IsBool in (Mc.PEX n, env) in let rec parse_expr env term = @@ -730,13 +762,13 @@ module M = struct (power, env) with ParseError -> (* if the exponent is a variable *) - let env, n = Env.compute_rank_add env term in + let env, n = Env.compute_rank_add env term Mc.IsBool in (Mc.PEX n, 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 + let env, n = Env.compute_rank_add env term Mc.IsBool in (Mc.PEX n, env) ) | _ -> parse_variable env term ) | _ -> parse_variable env term ) @@ -878,7 +910,7 @@ module M = struct Mc.PEpow (expr, exp)) rop_spec - let parse_arith parse_op parse_expr env cstr gl = + let parse_arith parse_op parse_expr (k : Mc.kind) env cstr gl = let sigma = gl.sigma in if debug then Feedback.msg_debug @@ -887,7 +919,7 @@ module M = struct ++ fnl () ); match EConstr.kind sigma cstr with | App (op, args) -> - let op, lhs, rhs = parse_op gl (op, args) in + let op, lhs, rhs = parse_op gl k (op, args) in let e1, env = parse_expr gl env lhs in let e2, env = parse_expr gl env rhs in ({Mc.flhs = e1; Mc.fop = op; Mc.frhs = e2}, env) @@ -899,13 +931,16 @@ module M = struct (* generic parsing of arithmetic expressions *) - let mkC f1 f2 = Mc.Cj (f1, f2) - let mkD f1 f2 = Mc.D (f1, f2) - let mkIff f1 f2 = Mc.Cj (Mc.I (f1, None, f2), Mc.I (f2, None, f1)) - let mkI f1 f2 = Mc.I (f1, None, f2) + let mkAND b f1 f2 = Mc.AND (b, f1, f2) + let mkOR b f1 f2 = Mc.OR (b, f1, f2) + let mkIff b f1 f2 = Mc.IFF (b, f1, f2) + let mkIMPL b f1 f2 = Mc.IMPL (b, f1, None, f2) + let mkEQ f1 f2 = Mc.EQ (f1, f2) - let mkformula_binary g term f1 f2 = - match (f1, f2) with Mc.X _, Mc.X _ -> Mc.X term | _ -> g f1 f2 + let mkformula_binary b g term f1 f2 = + match (f1, f2) with + | Mc.X (b1, _), Mc.X (b2, _) -> Mc.X (b, term) + | _ -> g f1 f2 (** * This is the big generic function for formula parsers. @@ -915,83 +950,129 @@ module M = struct let sort = Retyping.get_sort_of env sigma term in Sorts.is_prop sort + type formula_op = + { op_and : EConstr.t + ; op_or : EConstr.t + ; op_iff : EConstr.t + ; op_not : EConstr.t + ; op_tt : EConstr.t + ; op_ff : EConstr.t } + + let prop_op = + lazy + { op_and = Lazy.force coq_and + ; op_or = Lazy.force coq_or + ; op_iff = Lazy.force coq_iff + ; op_not = Lazy.force coq_not + ; op_tt = Lazy.force coq_True + ; op_ff = Lazy.force coq_False } + + let bool_op = + lazy + { op_and = Lazy.force coq_andb + ; op_or = Lazy.force coq_orb + ; op_iff = Lazy.force coq_eqb + ; op_not = Lazy.force coq_negb + ; op_tt = Lazy.force coq_true + ; op_ff = Lazy.force coq_false } + let parse_formula gl parse_atom env tg term = let sigma = gl.sigma in - let is_prop term = is_prop gl.env gl.sigma term in - let parse_atom env tg t = + let parse_atom b env tg t = try - let at, env = parse_atom env t gl in - (Mc.A (at, (tg, t)), env, Tag.next tg) - with ParseError -> - if is_prop t then (Mc.X t, env, tg) else raise ParseError + let at, env = parse_atom b env t gl in + (Mc.A (b, at, (tg, t)), env, Tag.next tg) + with ParseError -> (Mc.X (b, t), env, tg) in - let rec xparse_formula env tg term = + let prop_op = Lazy.force prop_op in + let bool_op = Lazy.force bool_op in + let eq = Lazy.force coq_eq in + let bool = Lazy.force coq_bool in + let rec xparse_formula op k env tg term = match EConstr.kind sigma term with | App (l, rst) -> ( match rst with - | [|a; b|] when EConstr.eq_constr sigma l (Lazy.force coq_and) -> - let f, env, tg = xparse_formula env tg a in - let g, env, tg = xparse_formula env tg b in - (mkformula_binary mkC term f g, env, tg) - | [|a; b|] when EConstr.eq_constr sigma l (Lazy.force coq_or) -> - let f, env, tg = xparse_formula env tg a in - let g, env, tg = xparse_formula env tg b in - (mkformula_binary mkD term f g, env, tg) - | [|a|] when EConstr.eq_constr sigma l (Lazy.force coq_not) -> - let f, env, tg = xparse_formula env tg a in - (Mc.N f, env, tg) - | [|a; b|] when EConstr.eq_constr sigma l (Lazy.force coq_iff) -> - let f, env, tg = xparse_formula env tg a in - let g, env, tg = xparse_formula env tg b in - (mkformula_binary mkIff term f g, env, tg) - | _ -> parse_atom env tg term ) + | [|a; b|] when EConstr.eq_constr sigma l op.op_and -> + let f, env, tg = xparse_formula op k env tg a in + let g, env, tg = xparse_formula op k env tg b in + (mkformula_binary k (mkAND k) term f g, env, tg) + | [|a; b|] when EConstr.eq_constr sigma l op.op_or -> + let f, env, tg = xparse_formula op k env tg a in + let g, env, tg = xparse_formula op k env tg b in + (mkformula_binary k (mkOR k) term f g, env, tg) + | [|a; b|] when EConstr.eq_constr sigma l op.op_iff -> + let f, env, tg = xparse_formula op k env tg a in + let g, env, tg = xparse_formula op k env tg b in + (mkformula_binary k (mkIff k) term f g, env, tg) + | [|ty; a; b|] + when EConstr.eq_constr sigma l eq && is_convertible gl ty bool -> + let f, env, tg = xparse_formula bool_op Mc.IsBool env tg a in + let g, env, tg = xparse_formula bool_op Mc.IsBool env tg b in + (mkformula_binary Mc.IsProp mkEQ term f g, env, tg) + | [|a|] when EConstr.eq_constr sigma l op.op_not -> + let f, env, tg = xparse_formula op k env tg a in + (Mc.NOT (k, f), env, tg) + | _ -> parse_atom k env tg term ) | Prod (typ, a, b) - when typ.binder_name = Anonymous || EConstr.Vars.noccurn sigma 1 b -> - let f, env, tg = xparse_formula env tg a in - let g, env, tg = xparse_formula env tg b in - (mkformula_binary mkI term f g, env, tg) + when kind_is_prop k + && (typ.binder_name = Anonymous || EConstr.Vars.noccurn sigma 1 b) + -> + let f, env, tg = xparse_formula op k env tg a in + let g, env, tg = xparse_formula op k env tg b in + (mkformula_binary Mc.IsProp (mkIMPL Mc.IsProp) term f g, env, tg) | _ -> - if EConstr.eq_constr sigma term (Lazy.force coq_True) then - (Mc.TT, env, tg) - else if EConstr.eq_constr sigma term (Lazy.force coq_False) then - Mc.(FF, env, tg) - else if is_prop term then (Mc.X term, env, tg) - else raise ParseError + if EConstr.eq_constr sigma term op.op_tt then (Mc.TT k, env, tg) + else if EConstr.eq_constr sigma term op.op_ff then Mc.(FF k, env, tg) + else (Mc.X (k, term), env, tg) in - xparse_formula env tg (*Reductionops.whd_zeta*) term + xparse_formula prop_op Mc.IsProp env tg (*Reductionops.whd_zeta*) term + + (* let dump_bool b = Lazy.force (if b then coq_true else coq_false)*) + + let dump_kind k = + Lazy.force (match k with Mc.IsProp -> coq_IsProp | Mc.IsBool -> coq_IsBool) let dump_formula typ dump_atom f = let app_ctor c args = EConstr.mkApp ( Lazy.force c , Array.of_list - ( typ :: EConstr.mkProp :: Lazy.force coq_unit + ( typ :: Lazy.force coq_eKind :: Lazy.force coq_unit :: Lazy.force coq_unit :: args ) ) in let rec xdump f = match f with - | Mc.TT -> app_ctor coq_TT [] - | Mc.FF -> app_ctor coq_FF [] - | Mc.Cj (x, y) -> app_ctor coq_And [xdump x; xdump y] - | Mc.D (x, y) -> app_ctor coq_Or [xdump x; xdump y] - | Mc.I (x, _, y) -> - app_ctor coq_Impl - [ xdump x + | Mc.TT k -> app_ctor coq_TT [dump_kind k] + | Mc.FF k -> app_ctor coq_FF [dump_kind k] + | Mc.AND (k, x, y) -> app_ctor coq_AND [dump_kind k; xdump x; xdump y] + | Mc.OR (k, x, y) -> app_ctor coq_OR [dump_kind k; xdump x; xdump y] + | Mc.IMPL (k, x, _, y) -> + app_ctor coq_IMPL + [ dump_kind k + ; xdump x ; EConstr.mkApp (Lazy.force coq_None, [|Lazy.force coq_unit|]) ; xdump y ] - | Mc.N x -> app_ctor coq_Neg [xdump x] - | Mc.A (x, _) -> app_ctor coq_Atom [dump_atom x; Lazy.force coq_tt] - | Mc.X t -> app_ctor coq_X [t] + | Mc.NOT (k, x) -> app_ctor coq_NOT [dump_kind k; xdump x] + | Mc.IFF (k, x, y) -> app_ctor coq_IFF [dump_kind k; xdump x; xdump y] + | Mc.EQ (x, y) -> app_ctor coq_EQ [xdump x; xdump y] + | Mc.A (k, x, _) -> + app_ctor coq_Atom [dump_kind k; dump_atom x; Lazy.force coq_tt] + | Mc.X (k, t) -> app_ctor coq_X [dump_kind k; t] in xdump f let prop_env_of_formula gl form = Mc.( let rec doit env = function - | TT | FF | A (_, _) -> env - | X t -> fst (Env.compute_rank_add env t) - | Cj (f1, f2) | D (f1, f2) | I (f1, _, f2) -> doit (doit env f1) f2 - | N f -> doit env f + | TT _ | FF _ | A (_, _, _) -> env + | X (b, t) -> fst (Env.compute_rank_add env t b) + | AND (b, f1, f2) + |OR (b, f1, f2) + |IMPL (b, f1, _, f2) + |IFF (b, f1, f2) -> + doit (doit env f1) f2 + | NOT (b, f) -> doit env f + | EQ (f1, f2) -> doit (doit env f1) f2 in doit (Env.empty gl) form) @@ -1008,11 +1089,15 @@ module M = struct in Mc.( let rec doit = function - | TT | FF | X _ -> ISet.empty - | A (a, (t, c)) -> vars_of_atom a - | Cj (f1, f2) | D (f1, f2) | I (f1, _, f2) -> + | TT _ | FF _ | X _ -> ISet.empty + | A (_, a, (t, c)) -> vars_of_atom a + | AND (_, f1, f2) + |OR (_, f1, f2) + |IMPL (_, f1, _, f2) + |IFF (_, f1, f2) + |EQ (f1, f2) -> ISet.union (doit f1) (doit f2) - | N f -> doit f + | NOT (_, f) -> doit f in doit form) @@ -1026,7 +1111,8 @@ module M = struct ; dump_mul : EConstr.constr ; dump_pow : EConstr.constr ; dump_pow_arg : Mc.n -> EConstr.constr - ; dump_op : (Mc.op2 * EConstr.constr) list } + ; dump_op_prop : (Mc.op2 * EConstr.constr) list + ; dump_op_bool : (Mc.op2 * EConstr.constr) list } let dump_zexpr = lazy @@ -1038,7 +1124,9 @@ module M = struct ; dump_mul = Lazy.force coq_Zmult ; dump_pow = Lazy.force coq_Zpower ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))) - ; dump_op = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table } + ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_prop + ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_bool + } let dump_qexpr = lazy @@ -1050,7 +1138,9 @@ module M = struct ; dump_mul = Lazy.force coq_Qmult ; dump_pow = Lazy.force coq_Qpower ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))) - ; dump_op = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table } + ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_prop + ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_bool + } let rec dump_Rcst_as_R cst = match cst with @@ -1087,7 +1177,9 @@ module M = struct ; dump_mul = Lazy.force coq_Rmult ; dump_pow = Lazy.force coq_Rpower ; dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n))) - ; dump_op = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table } + ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_prop + ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_bool + } let prodn n env b = let rec prodrec = function @@ -1105,6 +1197,10 @@ module M = struct *) + let eKind = function + | Mc.IsProp -> EConstr.mkProp + | Mc.IsBool -> Lazy.force coq_bool + let make_goal_of_formula gl dexpr form = let vars_idx = List.mapi @@ -1120,7 +1216,7 @@ module M = struct in let props_n = List.mapi - (fun i _ -> (fresh_prop "__p" (i + 1), EConstr.mkProp)) + (fun i (_, k) -> (fresh_prop "__p" (i + 1), eKind k)) (Env.elements props) in let var_name_pos = @@ -1129,8 +1225,7 @@ module M = struct let dump_expr i e = let rec dump_expr = function | Mc.PEX n -> - EConstr.mkRel - (i + CList.assoc_f Int.equal (CoqToCaml.positive n) vars_idx) + EConstr.mkRel (i + List.assoc (CoqToCaml.positive n) vars_idx) | Mc.PEc z -> dexpr.dump_cst z | Mc.PEadd (e1, e2) -> EConstr.mkApp (dexpr.dump_add, [|dump_expr e1; dump_expr e2|]) @@ -1144,31 +1239,70 @@ module M = struct in dump_expr e in - let mkop op e1 e2 = - try - EConstr.mkApp - (CList.assoc_f Mutils.Hash.eq_op2 op dexpr.dump_op, [|e1; e2|]) + let mkop_prop op e1 e2 = + try EConstr.mkApp (List.assoc op dexpr.dump_op_prop, [|e1; e2|]) + with Not_found -> + EConstr.mkApp (Lazy.force coq_eq, [|dexpr.interp_typ; e1; e2|]) + in + let dump_cstr_prop i {Mc.flhs; Mc.fop; Mc.frhs} = + mkop_prop fop (dump_expr i flhs) (dump_expr i frhs) + in + let mkop_bool op e1 e2 = + try EConstr.mkApp (List.assoc op dexpr.dump_op_bool, [|e1; e2|]) with Not_found -> - EConstr.mkApp (Lazy.force coq_Eq, [|dexpr.interp_typ; e1; e2|]) + EConstr.mkApp (Lazy.force coq_eq, [|dexpr.interp_typ; e1; e2|]) in - let dump_cstr i {Mc.flhs; Mc.fop; Mc.frhs} = - mkop fop (dump_expr i flhs) (dump_expr i frhs) + let dump_cstr_bool i {Mc.flhs; Mc.fop; Mc.frhs} = + mkop_bool fop (dump_expr i flhs) (dump_expr i frhs) in - let rec xdump pi xi f = + let rec xdump_prop pi xi f = match f with - | Mc.TT -> Lazy.force coq_True - | Mc.FF -> Lazy.force coq_False - | Mc.Cj (x, y) -> - EConstr.mkApp (Lazy.force coq_and, [|xdump pi xi x; xdump pi xi y|]) - | Mc.D (x, y) -> - EConstr.mkApp (Lazy.force coq_or, [|xdump pi xi x; xdump pi xi y|]) - | Mc.I (x, _, y) -> - EConstr.mkArrow (xdump pi xi x) Sorts.Relevant - (xdump (pi + 1) (xi + 1) y) - | Mc.N x -> - EConstr.mkArrow (xdump pi xi x) Sorts.Relevant (Lazy.force coq_False) - | Mc.A (x, _) -> dump_cstr xi x - | Mc.X t -> + | Mc.TT _ -> Lazy.force coq_True + | Mc.FF _ -> Lazy.force coq_False + | Mc.AND (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_and, [|xdump_prop pi xi x; xdump_prop pi xi y|]) + | Mc.OR (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_or, [|xdump_prop pi xi x; xdump_prop pi xi y|]) + | Mc.IFF (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_iff, [|xdump_prop pi xi x; xdump_prop pi xi y|]) + | Mc.IMPL (_, x, _, y) -> + EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant + (xdump_prop (pi + 1) (xi + 1) y) + | Mc.NOT (_, x) -> + EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant + (Lazy.force coq_False) + | Mc.EQ (x, y) -> + EConstr.mkApp + ( Lazy.force coq_eq + , [|Lazy.force coq_bool; xdump_bool pi xi x; xdump_bool pi xi y|] ) + | Mc.A (_, x, _) -> dump_cstr_prop xi x + | Mc.X (_, t) -> + let idx = Env.get_rank props t in + EConstr.mkRel (pi + idx) + and xdump_bool pi xi f = + match f with + | Mc.TT _ -> Lazy.force coq_true + | Mc.FF _ -> Lazy.force coq_false + | Mc.AND (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_andb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.OR (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_orb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.IFF (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_eqb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.IMPL (_, x, _, y) -> + EConstr.mkApp + (Lazy.force coq_implb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.NOT (_, x) -> + EConstr.mkApp (Lazy.force coq_negb, [|xdump_bool pi xi x|]) + | Mc.EQ (x, y) -> assert false + | Mc.A (_, x, _) -> dump_cstr_bool xi x + | Mc.X (_, t) -> let idx = Env.get_rank props t in EConstr.mkRel (pi + idx) in @@ -1179,12 +1313,12 @@ module M = struct let idx = Env.get_rank props p in EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx)) in - let form' = Mc.mapX subst_prop form in + let form' = Mc.mapX (fun _ p -> subst_prop p) Mc.IsProp form in ( prodn nb_props (List.map (fun (x, y) -> (Name.Name x, y)) props_n) (prodn nb_vars (List.map (fun (x, y) -> (Name.Name x, y)) vars_n) - (xdump (List.length vars_n) 0 form)) + (xdump_prop (List.length vars_n) 0 form)) , List.rev props_n , List.rev var_name_pos , form' ) @@ -1339,7 +1473,9 @@ let qq_domain_spec = ; coeff_eq = Mc.qeq_bool } let max_tag f = - 1 + Tag.to_int (Mc.foldA (fun t1 (t2, _) -> Tag.max t1 t2) f (Tag.from 0)) + 1 + + Tag.to_int + (Mc.foldA (fun t1 (t2, _) -> Tag.max t1 t2) Mc.IsProp f (Tag.from 0)) (** Naive topological sort of constr according to the subterm-ordering *) @@ -1364,7 +1500,9 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*) (set [ ( "__ff" , ff - , EConstr.mkApp (Lazy.force coq_Formula, [|formula_typ|]) ) + , EConstr.mkApp + ( Lazy.force coq_Formula + , [|formula_typ; Lazy.force coq_IsProp|] ) ) ; ( "__varmap" , vm , EConstr.mkApp (Lazy.force coq_VarMap, [|spec.typ|]) ) @@ -1527,37 +1665,73 @@ let abstract_formula : TagSet.t -> 'a formula -> 'a formula = fun hyps f -> let to_constr = Mc. - { mkTT = Lazy.force coq_True - ; mkFF = Lazy.force coq_False - ; mkA = (fun a (tg, t) -> t) - ; mkCj = + { mkTT = + (let coq_True = Lazy.force coq_True in + let coq_true = Lazy.force coq_true in + function Mc.IsProp -> coq_True | Mc.IsBool -> coq_true) + ; mkFF = + (let coq_False = Lazy.force coq_False in + let coq_false = Lazy.force coq_false in + function Mc.IsProp -> coq_False | Mc.IsBool -> coq_false) + ; mkA = (fun k a (tg, t) -> t) + ; mkAND = (let coq_and = Lazy.force coq_and in - fun x y -> EConstr.mkApp (coq_and, [|x; y|])) - ; mkD = + let coq_andb = Lazy.force coq_andb in + fun k x y -> + EConstr.mkApp + ( (match k with Mc.IsProp -> coq_and | Mc.IsBool -> coq_andb) + , [|x; y|] )) + ; mkOR = (let coq_or = Lazy.force coq_or in - fun x y -> EConstr.mkApp (coq_or, [|x; y|])) - ; mkI = (fun x y -> EConstr.mkArrow x Sorts.Relevant y) - ; mkN = + let coq_orb = Lazy.force coq_orb in + fun k x y -> + EConstr.mkApp + ( (match k with Mc.IsProp -> coq_or | Mc.IsBool -> coq_orb) + , [|x; y|] )) + ; mkIMPL = + (fun k x y -> + match k with + | Mc.IsProp -> EConstr.mkArrow x Sorts.Relevant y + | Mc.IsBool -> EConstr.mkApp (Lazy.force coq_implb, [|x; y|])) + ; mkIFF = + (let coq_iff = Lazy.force coq_iff in + let coq_eqb = Lazy.force coq_eqb in + fun k x y -> + EConstr.mkApp + ( (match k with Mc.IsProp -> coq_iff | Mc.IsBool -> coq_eqb) + , [|x; y|] )) + ; mkNOT = (let coq_not = Lazy.force coq_not in - fun x -> EConstr.mkApp (coq_not, [|x|])) } + let coq_negb = Lazy.force coq_negb in + fun k x -> + EConstr.mkApp + ( (match k with Mc.IsProp -> coq_not | Mc.IsBool -> coq_negb) + , [|x|] )) + ; mkEQ = + (let coq_eq = Lazy.force coq_eq in + fun x y -> EConstr.mkApp (coq_eq, [|Lazy.force coq_bool; x; y|])) } in - Mc.abst_form to_constr (fun (t, _) -> TagSet.mem t hyps) true f + Mc.abst_form to_constr (fun (t, _) -> TagSet.mem t hyps) true Mc.IsProp f (* [abstract_wrt_formula] is used in contexts whre f1 is already an abstraction of f2 *) let rec abstract_wrt_formula f1 f2 = Mc.( match (f1, f2) with - | X c, _ -> X c + | X (b, c), _ -> X (b, c) | A _, A _ -> f2 - | Cj (a, b), Cj (a', b') -> - Cj (abstract_wrt_formula a a', abstract_wrt_formula b b') - | D (a, b), D (a', b') -> - D (abstract_wrt_formula a a', abstract_wrt_formula b b') - | I (a, _, b), I (a', x, b') -> - I (abstract_wrt_formula a a', x, abstract_wrt_formula b b') - | FF, FF -> FF - | TT, TT -> TT - | N x, N y -> N (abstract_wrt_formula x y) + | AND (b, f1, f2), AND (_, f1', f2') -> + AND (b, abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2') + | OR (b, f1, f2), OR (_, f1', f2') -> + OR (b, abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2') + | IMPL (b, f1, _, f2), IMPL (_, f1', x, f2') -> + IMPL (b, abstract_wrt_formula f1 f1', x, abstract_wrt_formula f2 f2') + | IFF (b, f1, f2), IFF (_, f1', f2') -> + IFF (b, abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2') + | EQ (f1, f2), EQ (f1', f2') -> + EQ (abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2') + | FF b, FF _ -> FF b + | TT b, TT _ -> TT b + | NOT (b, x), NOT (_, y) -> NOT (b, abstract_wrt_formula x y) | _ -> failwith "abstract_wrt_formula") (** @@ -1577,7 +1751,7 @@ let formula_hyps_concl hyps concl = (fun (id, f) (cc, ids) -> match f with | Mc.X _ -> (cc, ids) - | _ -> (Mc.I (f, Some id, cc), id :: ids)) + | _ -> (Mc.IMPL (Mc.IsProp, f, Some id, cc), id :: ids)) hyps (concl, []) (* let time str f x = @@ -1595,7 +1769,7 @@ let micromega_tauto pre_process cnf spec prover env let mt = CamlToCoq.positive (max_tag ff) in (* Construction of cnf *) let pre_ff = pre_process mt (ff : 'a formula) in - let cnf_ff, cnf_ff_tags = cnf pre_ff in + let cnf_ff, cnf_ff_tags = cnf Mc.IsProp pre_ff in match witness_list_tags prover cnf_ff with | Model m -> Model m | Unknown -> Unknown @@ -1621,7 +1795,7 @@ let micromega_tauto pre_process cnf spec prover env in let ff' = abstract_formula deps ff in let pre_ff' = pre_process mt ff' in - let cnf_ff', _ = cnf pre_ff' in + let cnf_ff', _ = cnf Mc.IsProp pre_ff' in if debug then begin output_string stdout "\n"; Printf.printf "TForm : %a\n" pp_formula ff; @@ -1647,7 +1821,7 @@ let micromega_tauto pre_process cnf spec prover env | Some res -> () end ; *) let res' = compact_proofs spec.coeff_eq cnf_ff res cnf_ff' in - let ff', res', ids = (ff', res', Mc.ids_of_formula ff') in + let ff', res', ids = (ff', res', Mc.ids_of_formula Mc.IsProp ff') in let res' = dump_list spec.proof_typ spec.dump_proof res' in Prf (ids, ff', res') @@ -1719,9 +1893,11 @@ let micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac = env' ff_arith ] in let goal_props = - List.rev (Env.elements (prop_env_of_formula gl0 ff')) + List.rev (List.map fst (Env.elements (prop_env_of_formula gl0 ff'))) + in + let goal_vars = + List.map (fun (_, i) -> fst (List.nth env (i - 1))) vars in - let goal_vars = List.map (fun (_, i) -> List.nth env (i - 1)) vars in let arith_args = goal_props @ goal_vars in let kill_arith = Tacticals.New.tclTHEN tac_arith tac in (* @@ -1773,7 +1949,9 @@ let micromega_order_changer cert env ff = (set [ ( "__ff" , ff - , EConstr.mkApp (Lazy.force coq_Formula, [|formula_typ|]) ) + , EConstr.mkApp + ( Lazy.force coq_Formula + , [|formula_typ; Lazy.force coq_IsProp|] ) ) ; ("__varmap", vm, EConstr.mkApp (Lazy.force coq_VarMap, [|typ|])) ; ("__wit", cert, cert_typ) ] (Tacmach.New.pf_concl gl)) @@ -1805,11 +1983,16 @@ let micromega_genr prover tac = let hyps' = List.map (fun (n, f) -> - (n, Mc.map_bformula (Micromega.map_Formula Micromega.q_of_Rcst) f)) + ( n + , Mc.map_bformula Mc.IsProp + (Micromega.map_Formula Micromega.q_of_Rcst) + f )) hyps in let concl' = - Mc.map_bformula (Micromega.map_Formula Micromega.q_of_Rcst) concl + Mc.map_bformula Mc.IsProp + (Micromega.map_Formula Micromega.q_of_Rcst) + concl in match micromega_tauto @@ -1847,9 +2030,11 @@ let micromega_genr prover tac = ; micromega_order_changer res' env' ff_arith ] in let goal_props = - List.rev (Env.elements (prop_env_of_formula gl0 ff')) + List.rev (List.map fst (Env.elements (prop_env_of_formula gl0 ff'))) + in + let goal_vars = + List.map (fun (_, i) -> fst (List.nth env (i - 1))) vars in - let goal_vars = List.map (fun (_, i) -> List.nth env (i - 1)) vars in let arith_args = goal_props @ goal_vars in let kill_arith = Tacticals.New.tclTHEN tac_arith tac in (* Tacticals.New.tclTHEN diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg index ab0c3bed26..0e5cac2d4a 100644 --- a/plugins/micromega/g_zify.mlg +++ b/plugins/micromega/g_zify.mlg @@ -14,24 +14,44 @@ open Ltac_plugin open Stdarg open Tacarg +let warn_deprecated_Spec = + CWarnings.create ~name:"deprecated-Zify-Spec" ~category:"deprecated" + (fun () -> + Pp.strbrk ("Show Zify Spec is deprecated. Use either \"Show Zify BinOpSpec\" or \"Show Zify UnOpSpec\".")) + +let warn_deprecated_Add = + CWarnings.create ~name:"deprecated-Zify-Add" ~category:"deprecated" + (fun () -> + Pp.strbrk ("Add <X> is deprecated. Use instead Add Zify <X>.")) + } DECLARE PLUGIN "zify_plugin" VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF -| ["Add" "InjTyp" constr(t) ] -> { Zify.InjTable.register t } -| ["Add" "BinOp" constr(t) ] -> { Zify.BinOp.register t } -| ["Add" "UnOp" constr(t) ] -> { Zify.UnOp.register t } -| ["Add" "CstOp" constr(t) ] -> { Zify.CstOp.register t } -| ["Add" "BinRel" constr(t) ] -> { Zify.BinRel.register t } -| ["Add" "PropOp" constr(t) ] -> { Zify.PropBinOp.register t } -| ["Add" "PropBinOp" constr(t) ] -> { Zify.PropBinOp.register t } -| ["Add" "PropUOp" constr(t) ] -> { Zify.PropUnOp.register t } -| ["Add" "Spec" constr(t) ] -> { Zify.Spec.register t } -| ["Add" "BinOpSpec" constr(t) ] -> { Zify.Spec.register t } -| ["Add" "UnOpSpec" constr(t) ] -> { Zify.Spec.register t } -| ["Add" "Saturate" constr(t) ] -> { Zify.Saturate.register t } +| ["Add" "Zify" "InjTyp" constr(t) ] -> { Zify.InjTable.register t } +| ["Add" "Zify" "BinOp" constr(t) ] -> { Zify.BinOp.register t } +| ["Add" "Zify" "UnOp" constr(t) ] -> { Zify.UnOp.register t } +| ["Add" "Zify" "CstOp" constr(t) ] -> { Zify.CstOp.register t } +| ["Add" "Zify" "BinRel" constr(t) ] -> { Zify.BinRel.register t } +| ["Add" "Zify" "PropOp" constr(t) ] -> { Zify.PropBinOp.register t } +| ["Add" "Zify" "PropBinOp" constr(t) ] -> { Zify.PropBinOp.register t } +| ["Add" "Zify" "PropUOp" constr(t) ] -> { Zify.PropUnOp.register t } +| ["Add" "Zify" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t } +| ["Add" "Zify" "UnOpSpec" constr(t) ] -> { Zify.UnOpSpec.register t } +| ["Add" "Zify" "Saturate" constr(t) ] -> { Zify.Saturate.register t } +| ["Add" "InjTyp" constr(t) ] -> { warn_deprecated_Add (); Zify.InjTable.register t } +| ["Add" "BinOp" constr(t) ] -> { warn_deprecated_Add (); Zify.BinOp.register t } +| ["Add" "UnOp" constr(t) ] -> { warn_deprecated_Add (); Zify.UnOp.register t } +| ["Add" "CstOp" constr(t) ] -> { warn_deprecated_Add (); Zify.CstOp.register t } +| ["Add" "BinRel" constr(t) ] -> { warn_deprecated_Add (); Zify.BinRel.register t } +| ["Add" "PropOp" constr(t) ] -> { warn_deprecated_Add (); Zify.PropBinOp.register t } +| ["Add" "PropBinOp" constr(t) ] -> { warn_deprecated_Add (); Zify.PropBinOp.register t } +| ["Add" "PropUOp" constr(t) ] -> { warn_deprecated_Add (); Zify.PropUnOp.register t } +| ["Add" "BinOpSpec" constr(t) ] -> { warn_deprecated_Add (); Zify.BinOpSpec.register t } +| ["Add" "UnOpSpec" constr(t) ] -> { warn_deprecated_Add (); Zify.UnOpSpec.register t } +| ["Add" "Saturate" constr(t) ] -> { warn_deprecated_Add (); Zify.Saturate.register t } END TACTIC EXTEND ITER @@ -51,5 +71,9 @@ VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF |[ "Show" "Zify" "UnOp" ] -> { Zify.UnOp.print () } |[ "Show" "Zify" "CstOp"] -> { Zify.CstOp.print () } |[ "Show" "Zify" "BinRel"] -> { Zify.BinRel.print () } -|[ "Show" "Zify" "Spec"] -> { Zify.Spec.print () } +|[ "Show" "Zify" "UnOpSpec"] -> { Zify.UnOpSpec.print() } +|[ "Show" "Zify" "BinOpSpec"] -> { Zify.BinOpSpec.print() } +|[ "Show" "Zify" "Spec"] -> { + warn_deprecated_Spec () ; + Zify.UnOpSpec.print() ; Zify.BinOpSpec.print ()} END diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index d17a0aabb7..b231779c7b 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -967,39 +967,49 @@ let rec norm_aux cO cI cadd cmul csub copp ceqb = function ppow_N cO cI cadd cmul ceqb (fun p -> p) (norm_aux cO cI cadd cmul csub copp ceqb pe1) n0 +type kind = +| IsProp +| IsBool + type ('tA, 'tX, 'aA, 'aF) gFormula = -| TT -| FF -| X of 'tX -| A of 'tA * 'aA -| Cj of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula -| D of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula -| N of ('tA, 'tX, 'aA, 'aF) gFormula -| I of ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option +| TT of kind +| FF of kind +| X of kind * 'tX +| A of kind * 'tA * 'aA +| AND of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula +| OR of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula +| NOT of kind * ('tA, 'tX, 'aA, 'aF) gFormula +| IMPL of kind * ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option * ('tA, 'tX, 'aA, 'aF) gFormula +| IFF of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula +| EQ of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula (** val mapX : - ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) - gFormula **) - -let rec mapX f = function -| X x -> X (f x) -| Cj (f1, f2) -> Cj ((mapX f f1), (mapX f f2)) -| D (f1, f2) -> D ((mapX f f1), (mapX f f2)) -| N f1 -> N (mapX f f1) -| I (f1, o, f2) -> I ((mapX f f1), o, (mapX f f2)) + (kind -> 'a2 -> 'a2) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, + 'a2, 'a3, 'a4) gFormula **) + +let rec mapX f _ = function +| X (k0, x) -> X (k0, (f k0 x)) +| AND (k0, f1, f2) -> AND (k0, (mapX f k0 f1), (mapX f k0 f2)) +| OR (k0, f1, f2) -> OR (k0, (mapX f k0 f1), (mapX f k0 f2)) +| NOT (k0, f1) -> NOT (k0, (mapX f k0 f1)) +| IMPL (k0, f1, o, f2) -> IMPL (k0, (mapX f k0 f1), o, (mapX f k0 f2)) +| IFF (k0, f1, f2) -> IFF (k0, (mapX f k0 f1), (mapX f k0 f2)) +| EQ (f1, f2) -> EQ ((mapX f IsBool f1), (mapX f IsBool f2)) | x -> x (** val foldA : - ('a5 -> 'a3 -> 'a5) -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 **) + ('a5 -> 'a3 -> 'a5) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 **) -let rec foldA f f0 acc = +let rec foldA f _ f0 acc = match f0 with - | A (_, an) -> f acc an - | Cj (f1, f2) -> foldA f f1 (foldA f f2 acc) - | D (f1, f2) -> foldA f f1 (foldA f f2 acc) - | N f1 -> foldA f f1 acc - | I (f1, _, f2) -> foldA f f1 (foldA f f2 acc) + | A (_, _, an) -> f acc an + | AND (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) + | OR (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) + | NOT (k0, f1) -> foldA f k0 f1 acc + | IMPL (k0, f1, _, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) + | IFF (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) + | EQ (f1, f2) -> foldA f IsBool f1 (foldA f IsBool f2 acc) | _ -> acc (** val cons_id : 'a1 option -> 'a1 list -> 'a1 list **) @@ -1009,37 +1019,50 @@ let cons_id id l = | Some id0 -> id0::l | None -> l -(** val ids_of_formula : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list **) +(** val ids_of_formula : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list **) -let rec ids_of_formula = function -| I (_, id, f') -> cons_id id (ids_of_formula f') +let rec ids_of_formula _ = function +| IMPL (k0, _, id, f') -> cons_id id (ids_of_formula k0 f') | _ -> [] -(** val collect_annot : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list **) +(** val collect_annot : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list **) -let rec collect_annot = function -| A (_, a) -> a::[] -| Cj (f1, f2) -> app (collect_annot f1) (collect_annot f2) -| D (f1, f2) -> app (collect_annot f1) (collect_annot f2) -| N f0 -> collect_annot f0 -| I (f1, _, f2) -> app (collect_annot f1) (collect_annot f2) +let rec collect_annot _ = function +| A (_, _, a) -> a::[] +| AND (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) +| OR (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) +| NOT (k0, f0) -> collect_annot k0 f0 +| IMPL (k0, f1, _, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) +| IFF (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) +| EQ (f1, f2) -> app (collect_annot IsBool f1) (collect_annot IsBool f2) | _ -> [] -type 'a bFormula = ('a, __, unit0, unit0) gFormula +type rtyp = __ + +type eKind = __ + +type 'a bFormula = ('a, eKind, unit0, unit0) gFormula (** val map_bformula : - ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, 'a5) - gFormula **) - -let rec map_bformula fct = function -| TT -> TT -| FF -> FF -| X p -> X p -| A (a, t0) -> A ((fct a), t0) -| Cj (f1, f2) -> Cj ((map_bformula fct f1), (map_bformula fct f2)) -| D (f1, f2) -> D ((map_bformula fct f1), (map_bformula fct f2)) -| N f0 -> N (map_bformula fct f0) -| I (f1, a, f2) -> I ((map_bformula fct f1), a, (map_bformula fct f2)) + kind -> ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, + 'a5) gFormula **) + +let rec map_bformula _ fct = function +| TT k -> TT k +| FF k -> FF k +| X (k, p) -> X (k, p) +| A (k, a, t0) -> A (k, (fct a), t0) +| AND (k0, f1, f2) -> + AND (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2)) +| OR (k0, f1, f2) -> + OR (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2)) +| NOT (k0, f0) -> NOT (k0, (map_bformula k0 fct f0)) +| IMPL (k0, f1, a, f2) -> + IMPL (k0, (map_bformula k0 fct f1), a, (map_bformula k0 fct f2)) +| IFF (k0, f1, f2) -> + IFF (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2)) +| EQ (f1, f2) -> + EQ ((map_bformula IsBool fct f1), (map_bformula IsBool fct f2)) type ('x, 'annot) clause = ('x * 'annot) list @@ -1147,7 +1170,7 @@ let is_cnf_ff = function let and_cnf_opt f1 f2 = if if is_cnf_ff f1 then true else is_cnf_ff f2 then cnf_ff - else and_cnf f1 f2 + else if is_cnf_tt f2 then f1 else and_cnf f1 f2 (** val or_cnf_opt : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, @@ -1158,36 +1181,89 @@ let or_cnf_opt unsat deduce f1 f2 = then cnf_tt else if is_cnf_ff f2 then f1 else or_cnf unsat deduce f1 f2 -(** val xcnf : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) - cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) - tFormula -> ('a2, 'a3) cnf **) - -let rec xcnf unsat deduce normalise1 negate0 pol0 = function -| TT -> if pol0 then cnf_tt else cnf_ff -| FF -> if pol0 then cnf_ff else cnf_tt -| X _ -> cnf_ff -| A (x, t0) -> if pol0 then normalise1 x t0 else negate0 x t0 -| Cj (e1, e2) -> +(** val mk_and : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, + 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) + +let mk_and unsat deduce rEC k pol0 f1 f2 = if pol0 - then and_cnf_opt (xcnf unsat deduce normalise1 negate0 pol0 e1) - (xcnf unsat deduce normalise1 negate0 pol0 e2) - else or_cnf_opt unsat deduce (xcnf unsat deduce normalise1 negate0 pol0 e1) - (xcnf unsat deduce normalise1 negate0 pol0 e2) -| D (e1, e2) -> + then and_cnf_opt (rEC pol0 k f1) (rEC pol0 k f2) + else or_cnf_opt unsat deduce (rEC pol0 k f1) (rEC pol0 k f2) + +(** val mk_or : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, + 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) + +let mk_or unsat deduce rEC k pol0 f1 f2 = if pol0 - then or_cnf_opt unsat deduce (xcnf unsat deduce normalise1 negate0 pol0 e1) - (xcnf unsat deduce normalise1 negate0 pol0 e2) - else and_cnf_opt (xcnf unsat deduce normalise1 negate0 pol0 e1) - (xcnf unsat deduce normalise1 negate0 pol0 e2) -| N e -> xcnf unsat deduce normalise1 negate0 (negb pol0) e -| I (e1, _, e2) -> + then or_cnf_opt unsat deduce (rEC pol0 k f1) (rEC pol0 k f2) + else and_cnf_opt (rEC pol0 k f1) (rEC pol0 k f2) + +(** val mk_impl : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, + 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) + +let mk_impl unsat deduce rEC k pol0 f1 f2 = if pol0 - then or_cnf_opt unsat deduce - (xcnf unsat deduce normalise1 negate0 (negb pol0) e1) - (xcnf unsat deduce normalise1 negate0 pol0 e2) - else and_cnf_opt (xcnf unsat deduce normalise1 negate0 (negb pol0) e1) - (xcnf unsat deduce normalise1 negate0 pol0 e2) + then or_cnf_opt unsat deduce (rEC (negb pol0) k f1) (rEC pol0 k f2) + else and_cnf_opt (rEC (negb pol0) k f1) (rEC pol0 k f2) + +(** val mk_iff : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, + 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) + +let mk_iff unsat deduce rEC k pol0 f1 f2 = + or_cnf_opt unsat deduce + (and_cnf_opt (rEC (negb pol0) k f1) (rEC false k f2)) + (and_cnf_opt (rEC pol0 k f1) (rEC true k f2)) + +(** val is_bool : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool option **) + +let is_bool _ = function +| TT _ -> Some true +| FF _ -> Some false +| _ -> None + +(** val xcnf : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) + cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4, + 'a5) tFormula -> ('a2, 'a3) cnf **) + +let rec xcnf unsat deduce normalise1 negate0 pol0 _ = function +| TT _ -> if pol0 then cnf_tt else cnf_ff +| FF _ -> if pol0 then cnf_ff else cnf_tt +| X (_, _) -> cnf_ff +| A (_, x, t0) -> if pol0 then normalise1 x t0 else negate0 x t0 +| AND (k0, e1, e2) -> + mk_and unsat deduce (fun x x0 x1 -> + xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2 +| OR (k0, e1, e2) -> + mk_or unsat deduce (fun x x0 x1 -> + xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2 +| NOT (k0, e) -> xcnf unsat deduce normalise1 negate0 (negb pol0) k0 e +| IMPL (k0, e1, _, e2) -> + mk_impl unsat deduce (fun x x0 x1 -> + xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2 +| IFF (k0, e1, e2) -> + (match is_bool k0 e2 with + | Some isb -> + xcnf unsat deduce normalise1 negate0 (if isb then pol0 else negb pol0) + k0 e1 + | None -> + mk_iff unsat deduce (fun x x0 x1 -> + xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2) +| EQ (e1, e2) -> + (match is_bool IsBool e2 with + | Some isb -> + xcnf unsat deduce normalise1 negate0 (if isb then pol0 else negb pol0) + IsBool e1 + | None -> + mk_iff unsat deduce (fun x x0 x1 -> + xcnf unsat deduce normalise1 negate0 x x0 x1) IsBool pol0 e1 e2) (** val radd_term : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) @@ -1271,141 +1347,311 @@ let ror_cnf_opt unsat deduce f1 f2 = let ratom c a = if if is_cnf_ff c then true else is_cnf_tt c then c,(a::[]) else c,[] -(** val rxcnf : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) - cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) - tFormula -> ('a2, 'a3) cnf * 'a3 list **) - -let rec rxcnf unsat deduce normalise1 negate0 polarity = function -| TT -> if polarity then cnf_tt,[] else cnf_ff,[] -| FF -> if polarity then cnf_ff,[] else cnf_tt,[] -| X _ -> cnf_ff,[] -| A (x, t0) -> ratom (if polarity then normalise1 x t0 else negate0 x t0) t0 -| Cj (e1, e2) -> - let e3,t1 = rxcnf unsat deduce normalise1 negate0 polarity e1 in - let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in +(** val rxcnf_and : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind -> + ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, + 'a3) cnf * 'a3 list **) + +let rxcnf_and unsat deduce rXCNF polarity k e1 e2 = + let e3,t1 = rXCNF polarity k e1 in + let e4,t2 = rXCNF polarity k e2 in if polarity then (and_cnf_opt e3 e4),(rev_append t1 t2) else let f',t' = ror_cnf_opt unsat deduce e3 e4 in f',(rev_append t1 (rev_append t2 t')) -| D (e1, e2) -> - let e3,t1 = rxcnf unsat deduce normalise1 negate0 polarity e1 in - let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in + +(** val rxcnf_or : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind -> + ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, + 'a3) cnf * 'a3 list **) + +let rxcnf_or unsat deduce rXCNF polarity k e1 e2 = + let e3,t1 = rXCNF polarity k e1 in + let e4,t2 = rXCNF polarity k e2 in if polarity then let f',t' = ror_cnf_opt unsat deduce e3 e4 in f',(rev_append t1 (rev_append t2 t')) else (and_cnf_opt e3 e4),(rev_append t1 t2) -| N e -> rxcnf unsat deduce normalise1 negate0 (negb polarity) e -| I (e1, _, e2) -> - let e3,t1 = rxcnf unsat deduce normalise1 negate0 (negb polarity) e1 in + +(** val rxcnf_impl : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind -> + ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, + 'a3) cnf * 'a3 list **) + +let rxcnf_impl unsat deduce rXCNF polarity k e1 e2 = + let e3,t1 = rXCNF (negb polarity) k e1 in if polarity then if is_cnf_ff e3 - then rxcnf unsat deduce normalise1 negate0 polarity e2 - else let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in + then rXCNF polarity k e2 + else let e4,t2 = rXCNF polarity k e2 in let f',t' = ror_cnf_opt unsat deduce e3 e4 in f',(rev_append t1 (rev_append t2 t')) - else let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in + else let e4,t2 = rXCNF polarity k e2 in (and_cnf_opt e3 e4),(rev_append t1 t2) -type ('term, 'annot, 'tX) to_constrT = { mkTT : 'tX; mkFF : 'tX; - mkA : ('term -> 'annot -> 'tX); - mkCj : ('tX -> 'tX -> 'tX); - mkD : ('tX -> 'tX -> 'tX); - mkI : ('tX -> 'tX -> 'tX); - mkN : ('tX -> 'tX) } +(** val rxcnf_iff : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind -> + ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, + 'a3) cnf * 'a3 list **) + +let rxcnf_iff unsat deduce rXCNF polarity k e1 e2 = + let c1,t1 = rXCNF (negb polarity) k e1 in + let c2,t2 = rXCNF false k e2 in + let c3,t3 = rXCNF polarity k e1 in + let c4,t4 = rXCNF true k e2 in + let f',t' = ror_cnf_opt unsat deduce (and_cnf_opt c1 c2) (and_cnf_opt c3 c4) + in + f',(rev_append t1 (rev_append t2 (rev_append t3 (rev_append t4 t')))) + +(** val rxcnf : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) + cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4, + 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list **) + +let rec rxcnf unsat deduce normalise1 negate0 polarity _ = function +| TT _ -> if polarity then cnf_tt,[] else cnf_ff,[] +| FF _ -> if polarity then cnf_ff,[] else cnf_tt,[] +| X (_, _) -> cnf_ff,[] +| A (_, x, t0) -> + ratom (if polarity then normalise1 x t0 else negate0 x t0) t0 +| AND (k0, e1, e2) -> + rxcnf_and unsat deduce (fun x x0 x1 -> + rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2 +| OR (k0, e1, e2) -> + rxcnf_or unsat deduce (fun x x0 x1 -> + rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2 +| NOT (k0, e) -> rxcnf unsat deduce normalise1 negate0 (negb polarity) k0 e +| IMPL (k0, e1, _, e2) -> + rxcnf_impl unsat deduce (fun x x0 x1 -> + rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2 +| IFF (k0, e1, e2) -> + rxcnf_iff unsat deduce (fun x x0 x1 -> + rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2 +| EQ (e1, e2) -> + rxcnf_iff unsat deduce (fun x x0 x1 -> + rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity IsBool e1 e2 + +type ('term, 'annot, 'tX) to_constrT = { mkTT : (kind -> 'tX); + mkFF : (kind -> 'tX); + mkA : (kind -> 'term -> 'annot -> + 'tX); + mkAND : (kind -> 'tX -> 'tX -> 'tX); + mkOR : (kind -> 'tX -> 'tX -> 'tX); + mkIMPL : (kind -> 'tX -> 'tX -> 'tX); + mkIFF : (kind -> 'tX -> 'tX -> 'tX); + mkNOT : (kind -> 'tX -> 'tX); + mkEQ : ('tX -> 'tX -> 'tX) } (** val aformula : - ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 **) - -let rec aformula to_constr = function -| TT -> to_constr.mkTT -| FF -> to_constr.mkFF -| X p -> p -| A (x, t0) -> to_constr.mkA x t0 -| Cj (f1, f2) -> - to_constr.mkCj (aformula to_constr f1) (aformula to_constr f2) -| D (f1, f2) -> to_constr.mkD (aformula to_constr f1) (aformula to_constr f2) -| N f0 -> to_constr.mkN (aformula to_constr f0) -| I (f1, _, f2) -> - to_constr.mkI (aformula to_constr f1) (aformula to_constr f2) - -(** val is_X : ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option **) - -let is_X = function -| X p -> Some p + ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 **) + +let rec aformula to_constr _ = function +| TT b -> to_constr.mkTT b +| FF b -> to_constr.mkFF b +| X (_, p) -> p +| A (b, x, t0) -> to_constr.mkA b x t0 +| AND (k0, f1, f2) -> + to_constr.mkAND k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2) +| OR (k0, f1, f2) -> + to_constr.mkOR k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2) +| NOT (k0, f0) -> to_constr.mkNOT k0 (aformula to_constr k0 f0) +| IMPL (k0, f1, _, f2) -> + to_constr.mkIMPL k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2) +| IFF (k0, f1, f2) -> + to_constr.mkIFF k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2) +| EQ (f1, f2) -> + to_constr.mkEQ (aformula to_constr IsBool f1) (aformula to_constr IsBool f2) + +(** val is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option **) + +let is_X _ = function +| X (_, p) -> Some p | _ -> None (** val abs_and : - ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, - 'a3, 'a4) tFormula -> (('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, - 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) - gFormula **) - -let abs_and to_constr f1 f2 c = - match is_X f1 with - | Some _ -> X (aformula to_constr (c f1 f2)) + ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> + ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> + ('a1, 'a3, 'a2, 'a4) gFormula **) + +let abs_and to_constr k f1 f2 c = + match is_X k f1 with + | Some _ -> X (k, (aformula to_constr k (c k f1 f2))) | None -> - (match is_X f2 with - | Some _ -> X (aformula to_constr (c f1 f2)) - | None -> c f1 f2) + (match is_X k f2 with + | Some _ -> X (k, (aformula to_constr k (c k f1 f2))) + | None -> c k f1 f2) (** val abs_or : - ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, - 'a3, 'a4) tFormula -> (('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, - 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) - gFormula **) + ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> + ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> + ('a1, 'a3, 'a2, 'a4) gFormula **) -let abs_or to_constr f1 f2 c = - match is_X f1 with +let abs_or to_constr k f1 f2 c = + match is_X k f1 with | Some _ -> - (match is_X f2 with - | Some _ -> X (aformula to_constr (c f1 f2)) - | None -> c f1 f2) - | None -> c f1 f2 + (match is_X k f2 with + | Some _ -> X (k, (aformula to_constr k (c k f1 f2))) + | None -> c k f1 f2) + | None -> c k f1 f2 + +(** val abs_not : + ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> + (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) + -> ('a1, 'a3, 'a2, 'a4) gFormula **) + +let abs_not to_constr k f1 c = + match is_X k f1 with + | Some _ -> X (k, (aformula to_constr k (c k f1))) + | None -> c k f1 (** val mk_arrow : - 'a4 option -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) - tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **) + 'a4 option -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, + 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **) -let mk_arrow o f1 f2 = +let mk_arrow o k f1 f2 = match o with - | Some _ -> (match is_X f1 with - | Some _ -> f2 - | None -> I (f1, o, f2)) - | None -> I (f1, None, f2) + | Some _ -> + (match is_X k f1 with + | Some _ -> f2 + | None -> IMPL (k, f1, o, f2)) + | None -> IMPL (k, f1, None, f2) + +(** val abst_simpl : + ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> kind -> ('a1, 'a2, 'a3, + 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **) + +let rec abst_simpl to_constr needA _ = function +| A (k, x, t0) -> + if needA t0 then A (k, x, t0) else X (k, (to_constr.mkA k x t0)) +| AND (k0, f1, f2) -> + AND (k0, (abst_simpl to_constr needA k0 f1), + (abst_simpl to_constr needA k0 f2)) +| OR (k0, f1, f2) -> + OR (k0, (abst_simpl to_constr needA k0 f1), + (abst_simpl to_constr needA k0 f2)) +| NOT (k0, f0) -> NOT (k0, (abst_simpl to_constr needA k0 f0)) +| IMPL (k0, f1, o, f2) -> + IMPL (k0, (abst_simpl to_constr needA k0 f1), o, + (abst_simpl to_constr needA k0 f2)) +| IFF (k0, f1, f2) -> + IFF (k0, (abst_simpl to_constr needA k0 f1), + (abst_simpl to_constr needA k0 f2)) +| EQ (f1, f2) -> + EQ ((abst_simpl to_constr needA IsBool f1), + (abst_simpl to_constr needA IsBool f2)) +| x -> x -(** val abst_form : - ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> ('a1, 'a2, 'a3, - 'a4) tFormula -> ('a1, 'a3, 'a2, 'a4) gFormula **) - -let rec abst_form to_constr needA pol0 = function -| TT -> if pol0 then TT else X to_constr.mkTT -| FF -> if pol0 then X to_constr.mkFF else FF -| X p -> X p -| A (x, t0) -> if needA t0 then A (x, t0) else X (to_constr.mkA x t0) -| Cj (f1, f2) -> - let f3 = abst_form to_constr needA pol0 f1 in - let f4 = abst_form to_constr needA pol0 f2 in +(** val abst_and : + ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) + tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2, + 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, + 'a4) tFormula **) + +let abst_and to_constr rEC pol0 k f1 f2 = if pol0 - then abs_and to_constr f3 f4 (fun x x0 -> Cj (x, x0)) - else abs_or to_constr f3 f4 (fun x x0 -> Cj (x, x0)) -| D (f1, f2) -> - let f3 = abst_form to_constr needA pol0 f1 in - let f4 = abst_form to_constr needA pol0 f2 in + then abs_and to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> + AND (x, x0, x1)) + else abs_or to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> AND + (x, x0, x1)) + +(** val abst_or : + ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) + tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2, + 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, + 'a4) tFormula **) + +let abst_or to_constr rEC pol0 k f1 f2 = if pol0 - then abs_or to_constr f3 f4 (fun x x0 -> D (x, x0)) - else abs_and to_constr f3 f4 (fun x x0 -> D (x, x0)) -| N f0 -> - let f1 = abst_form to_constr needA (negb pol0) f0 in - (match is_X f1 with - | Some a -> X (to_constr.mkN a) - | None -> N f1) -| I (f1, o, f2) -> - let f3 = abst_form to_constr needA (negb pol0) f1 in - let f4 = abst_form to_constr needA pol0 f2 in + then abs_or to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> OR + (x, x0, x1)) + else abs_and to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> OR + (x, x0, x1)) + +(** val abst_impl : + ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) + tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> 'a4 option -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> + ('a1, 'a2, 'a3, 'a4) tFormula **) + +let abst_impl to_constr rEC pol0 o k f1 f2 = if pol0 - then abs_or to_constr f3 f4 (mk_arrow o) - else abs_and to_constr f3 f4 (mk_arrow o) + then abs_or to_constr k (rEC (negb pol0) k f1) (rEC pol0 k f2) (mk_arrow o) + else abs_and to_constr k (rEC (negb pol0) k f1) (rEC pol0 k f2) (mk_arrow o) + +(** val or_is_X : + kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> + bool **) + +let or_is_X k f1 f2 = + match is_X k f1 with + | Some _ -> true + | None -> (match is_X k f2 with + | Some _ -> true + | None -> false) + +(** val abs_iff : + ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> + ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, + 'a2, 'a3, 'a4) tFormula -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, + 'a2, 'a3, 'a4) tFormula **) + +let abs_iff to_constr k nf1 ff2 f1 tf2 r def = + if (&&) (or_is_X k nf1 ff2) (or_is_X k f1 tf2) + then X (r, (aformula to_constr r def)) + else def + +(** val abst_iff : + ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, + 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> + ('a1, 'a2, 'a3, 'a4) tFormula **) + +let abst_iff to_constr needA rEC pol0 k f1 f2 = + abs_iff to_constr k (rEC (negb pol0) k f1) (rEC false k f2) (rEC pol0 k f1) + (rEC true k f2) k (IFF (k, (abst_simpl to_constr needA k f1), + (abst_simpl to_constr needA k f2))) + +(** val abst_eq : + ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, + 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> + ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, + 'a2, 'a3, 'a4) tFormula **) + +let abst_eq to_constr needA rEC pol0 f1 f2 = + abs_iff to_constr IsBool (rEC (negb pol0) IsBool f1) (rEC false IsBool f2) + (rEC pol0 IsBool f1) (rEC true IsBool f2) IsProp (EQ + ((abst_simpl to_constr needA IsBool f1), + (abst_simpl to_constr needA IsBool f2))) + +(** val abst_form : + ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> kind -> ('a1, 'a2, + 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **) + +let rec abst_form to_constr needA pol0 _ = function +| TT k -> if pol0 then TT k else X (k, (to_constr.mkTT k)) +| FF k -> if pol0 then X (k, (to_constr.mkFF k)) else FF k +| X (k, p) -> X (k, p) +| A (k, x, t0) -> + if needA t0 then A (k, x, t0) else X (k, (to_constr.mkA k x t0)) +| AND (k0, f1, f2) -> + abst_and to_constr (abst_form to_constr needA) pol0 k0 f1 f2 +| OR (k0, f1, f2) -> + abst_or to_constr (abst_form to_constr needA) pol0 k0 f1 f2 +| NOT (k0, f0) -> + abs_not to_constr k0 (abst_form to_constr needA (negb pol0) k0 f0) + (fun x x0 -> NOT (x, x0)) +| IMPL (k0, f1, o, f2) -> + abst_impl to_constr (abst_form to_constr needA) pol0 o k0 f1 f2 +| IFF (k0, f1, f2) -> + abst_iff to_constr needA (abst_form to_constr needA) pol0 k0 f1 f2 +| EQ (f1, f2) -> + abst_eq to_constr needA (abst_form to_constr needA) pol0 f1 f2 (** val cnf_checker : (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool **) @@ -1421,10 +1667,10 @@ let rec cnf_checker checker f l = (** val tauto_checker : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> - bool) -> ('a1, __, 'a3, unit0) gFormula -> 'a4 list -> bool **) + bool) -> ('a1, rtyp, 'a3, unit0) gFormula -> 'a4 list -> bool **) let tauto_checker unsat deduce normalise1 negate0 checker f w = - cnf_checker checker (xcnf unsat deduce normalise1 negate0 true f) w + cnf_checker checker (xcnf unsat deduce normalise1 negate0 true IsProp f) w (** val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool **) @@ -1969,10 +2215,11 @@ let negate t0 tg = if zunsat f then cnf_tt else cnf_of_list0 tg (xnegate0 f) (** val cnfZ : - (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 list **) + kind -> (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) + cnf * 'a1 list **) -let cnfZ f = - rxcnf zunsat zdeduce normalise0 negate true f +let cnfZ k f = + rxcnf zunsat zdeduce normalise0 negate true k f (** val ceiling : z -> z -> z **) @@ -2178,10 +2425,11 @@ let normQ = qminus qopp qeq_bool (** val cnfQ : - (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) cnf * 'a1 list **) + kind -> (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) + cnf * 'a1 list **) -let cnfQ f = - rxcnf qunsat qdeduce qnormalise qnegate true f +let cnfQ k f = + rxcnf qunsat qdeduce qnormalise qnegate true k f (** val qTautoChecker : q formula bFormula -> qWitness list -> bool **) @@ -2255,4 +2503,5 @@ let rdeduce = let rTautoChecker f w = tauto_checker runsat rdeduce rnormalise rnegate (fun cl -> - rWeakChecker (map fst cl)) (map_bformula (map_Formula q_of_Rcst) f) w + rWeakChecker (map fst cl)) + (map_bformula IsProp (map_Formula q_of_Rcst) f) w diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli index 4200c80574..53f62e0f5b 100644 --- a/plugins/micromega/micromega.mli +++ b/plugins/micromega/micromega.mli @@ -88,6 +88,15 @@ end val zeq_bool : z -> z -> bool +type 'c pExpr = + | PEc of 'c + | PEX of positive + | PEadd of 'c pExpr * 'c pExpr + | PEsub of 'c pExpr * 'c pExpr + | PEmul of 'c pExpr * 'c pExpr + | PEopp of 'c pExpr + | PEpow of 'c pExpr * n + type 'c pol = | Pc of 'c | Pinj of positive * 'c pol @@ -209,15 +218,6 @@ val psquare : -> 'a1 pol -> 'a1 pol -type 'c pExpr = - | PEc of 'c - | PEX of positive - | PEadd of 'c pExpr * 'c pExpr - | PEsub of 'c pExpr * 'c pExpr - | PEmul of 'c pExpr * 'c pExpr - | PEopp of 'c pExpr - | PEpow of 'c pExpr * n - val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol val ppow_pos : @@ -254,29 +254,46 @@ val norm_aux : -> 'a1 pExpr -> 'a1 pol +type kind = IsProp | IsBool + type ('tA, 'tX, 'aA, 'aF) gFormula = - | TT - | FF - | X of 'tX - | A of 'tA * 'aA - | Cj of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula - | D of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula - | N of ('tA, 'tX, 'aA, 'aF) gFormula - | I of - ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option * ('tA, 'tX, 'aA, 'aF) gFormula + | TT of kind + | FF of kind + | X of kind * 'tX + | A of kind * 'tA * 'aA + | AND of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula + | OR of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula + | NOT of kind * ('tA, 'tX, 'aA, 'aF) gFormula + | IMPL of + kind + * ('tA, 'tX, 'aA, 'aF) gFormula + * 'aF option + * ('tA, 'tX, 'aA, 'aF) gFormula + | IFF of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula + | EQ of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula val mapX : - ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) gFormula + (kind -> 'a2 -> 'a2) + -> kind + -> ('a1, 'a2, 'a3, 'a4) gFormula + -> ('a1, 'a2, 'a3, 'a4) gFormula + +val foldA : + ('a5 -> 'a3 -> 'a5) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 -val foldA : ('a5 -> 'a3 -> 'a5) -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 val cons_id : 'a1 option -> 'a1 list -> 'a1 list -val ids_of_formula : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list -val collect_annot : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list +val ids_of_formula : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list +val collect_annot : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list -type 'a bFormula = ('a, __, unit0, unit0) gFormula +type rtyp = __ +type eKind = __ +type 'a bFormula = ('a, eKind, unit0, unit0) gFormula val map_bformula : - ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, 'a5) gFormula + kind + -> ('a1 -> 'a2) + -> ('a1, 'a3, 'a4, 'a5) gFormula + -> ('a2, 'a3, 'a4, 'a5) gFormula type ('x, 'annot) clause = ('x * 'annot) list type ('x, 'annot) cnf = ('x, 'annot) clause list @@ -334,12 +351,55 @@ val or_cnf_opt : -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf +val mk_and : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) + -> kind + -> bool + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf + +val mk_or : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) + -> kind + -> bool + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf + +val mk_impl : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) + -> kind + -> bool + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf + +val mk_iff : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) + -> kind + -> bool + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf + +val is_bool : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool option + val xcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool + -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf @@ -387,49 +447,199 @@ val ror_cnf_opt : val ratom : ('a1, 'a2) cnf -> 'a2 -> ('a1, 'a2) cnf * 'a2 list +val rxcnf_and : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> ( bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list) + -> bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list + +val rxcnf_or : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> ( bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list) + -> bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list + +val rxcnf_impl : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> ( bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list) + -> bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list + +val rxcnf_iff : + ('a2 -> bool) + -> ('a2 -> 'a2 -> 'a2 option) + -> ( bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list) + -> bool + -> kind + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a1, 'a3, 'a4, 'a5) tFormula + -> ('a2, 'a3) cnf * 'a3 list + val rxcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool + -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list type ('term, 'annot, 'tX) to_constrT = - { mkTT : 'tX - ; mkFF : 'tX - ; mkA : 'term -> 'annot -> 'tX - ; mkCj : 'tX -> 'tX -> 'tX - ; mkD : 'tX -> 'tX -> 'tX - ; mkI : 'tX -> 'tX -> 'tX - ; mkN : 'tX -> 'tX } + { mkTT : kind -> 'tX + ; mkFF : kind -> 'tX + ; mkA : kind -> 'term -> 'annot -> 'tX + ; mkAND : kind -> 'tX -> 'tX -> 'tX + ; mkOR : kind -> 'tX -> 'tX -> 'tX + ; mkIMPL : kind -> 'tX -> 'tX -> 'tX + ; mkIFF : kind -> 'tX -> 'tX -> 'tX + ; mkNOT : kind -> 'tX -> 'tX + ; mkEQ : 'tX -> 'tX -> 'tX } val aformula : - ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 + ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 -val is_X : ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option +val is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option val abs_and : ('a1, 'a2, 'a3) to_constrT + -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula - -> ( ('a1, 'a2, 'a3, 'a4) tFormula + -> ( kind + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula val abs_or : ('a1, 'a2, 'a3) to_constrT + -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula - -> ( ('a1, 'a2, 'a3, 'a4) tFormula + -> ( kind + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula +val abs_not : + ('a1, 'a2, 'a3) to_constrT + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) + -> ('a1, 'a3, 'a2, 'a4) gFormula + val mk_arrow : 'a4 option + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + +val abst_simpl : + ('a1, 'a2, 'a3) to_constrT + -> ('a2 -> bool) + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + +val abst_and : + ('a1, 'a2, 'a3) to_constrT + -> ( bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula) + -> bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + +val abst_or : + ('a1, 'a2, 'a3) to_constrT + -> ( bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula) + -> bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + +val abst_impl : + ('a1, 'a2, 'a3) to_constrT + -> ( bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula) + -> bool + -> 'a4 option + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + +val or_is_X : + kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool + +val abs_iff : + ('a1, 'a2, 'a3) to_constrT + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + +val abst_iff : + ('a1, 'a2, 'a3) to_constrT + -> ('a2 -> bool) + -> ( bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula) + -> bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula + +val abst_eq : + ('a1, 'a2, 'a3) to_constrT + -> ('a2 -> bool) + -> ( bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula + -> ('a1, 'a2, 'a3, 'a4) tFormula) + -> bool -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula @@ -438,8 +648,9 @@ val abst_form : ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool + -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula - -> ('a1, 'a3, 'a2, 'a4) gFormula val cnf_checker : (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool @@ -450,7 +661,7 @@ val tauto_checker : -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> bool) - -> ('a1, __, 'a3, unit0) gFormula + -> ('a1, rtyp, 'a3, unit0) gFormula -> 'a4 list -> bool @@ -661,7 +872,9 @@ val xnegate0 : z nFormula -> z nFormula list val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf val cnfZ : - (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 list + kind + -> (z formula, 'a1, 'a2, 'a3) tFormula + -> (z nFormula, 'a1) cnf * 'a1 list val ceiling : z -> z -> z @@ -698,7 +911,9 @@ val qdeduce : q nFormula -> q nFormula -> q nFormula option val normQ : q pExpr -> q pol val cnfQ : - (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) cnf * 'a1 list + kind + -> (q formula, 'a1, 'a2, 'a3) tFormula + -> (q nFormula, 'a1) cnf * 'a1 list val qTautoChecker : q formula bFormula -> qWitness list -> bool diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 41579d5792..4e1f9a66ac 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -45,9 +45,7 @@ let op_iff = lazy (zify "iff") let op_iff_morph = lazy (zify "iff_morph") let op_not = lazy (zify "not") let op_not_morph = lazy (zify "not_morph") - -(* identity function *) -(*let identity = lazy (zify "identity")*) +let op_True = lazy (zify "True") let whd = Reductionops.clos_whd_flags CClosure.all (** [unsafe_to_constr c] returns a [Constr.t] without considering an evar_map. @@ -248,10 +246,12 @@ module EBinOpT = struct source1 : EConstr.t ; source2 : EConstr.t ; source3 : EConstr.t - ; target : EConstr.t - ; inj1 : EInjT.t (* InjTyp source1 target *) - ; inj2 : EInjT.t (* InjTyp source2 target *) - ; inj3 : EInjT.t (* InjTyp source3 target *) + ; target1 : EConstr.t + ; target2 : EConstr.t + ; target3 : EConstr.t + ; inj1 : EInjT.t (* InjTyp source1 target1 *) + ; inj2 : EInjT.t (* InjTyp source2 target2 *) + ; inj3 : EInjT.t (* InjTyp source3 target3 *) ; bop : EConstr.t (* BOP *) ; tbop : EConstr.t (* TBOP *) ; tbopinj : EConstr.t (* TBOpInj *) @@ -272,7 +272,8 @@ module EUnOpT = struct type t = { source1 : EConstr.t ; source2 : EConstr.t - ; target : EConstr.t + ; target1 : EConstr.t + ; target2 : EConstr.t ; uop : EConstr.t ; inj1_t : EInjT.t ; inj2_t : EInjT.t @@ -319,7 +320,8 @@ type decl_kind = | UnOp of EUnOpT.t decl | CstOp of ECstOpT.t decl | Saturate of ESatT.t decl - | Spec of ESpecT.t decl + | UnOpSpec of ESpecT.t decl + | BinOpSpec of ESpecT.t decl type term_kind = Application of EConstr.constr | OtherTerm of EConstr.constr @@ -353,6 +355,7 @@ let specs_cache = ref HConstr.empty (** Each type-class gives rise to a different table. They only differ on how projections are extracted. *) + module EInj = struct open EInjT @@ -363,6 +366,11 @@ module EInj = struct let cast x = InjTyp x let dest = function InjTyp x -> Some x | _ -> None + let is_cstr_true evd c = + match EConstr.kind evd c with + | Lambda (_, _, c) -> EConstr.eq_constr_nounivs evd c (Lazy.force op_True) + | _ -> false + let mk_elt evd i (a : EConstr.t array) = let isid = EConstr.eq_constr_nounivs evd a.(0) a.(1) in { isid @@ -370,7 +378,7 @@ module EInj = struct ; target = a.(1) ; inj = a.(2) ; pred = a.(3) - ; cstr = (if isid then None else Some a.(4)) } + ; cstr = (if is_cstr_true evd a.(3) then None else Some a.(4)) } let get_key = 0 end @@ -383,6 +391,28 @@ let get_inj evd c = failwith ("Cannot register term " ^ t) | Some a -> EInj.mk_elt evd c a +let rec decomp_type evd ty = + match EConstr.kind_of_type evd ty with + | EConstr.ProdType (_, t1, rst) -> t1 :: decomp_type evd rst + | _ -> [ty] + +let pp_type env evd l = + Pp.prlist_with_sep (fun _ -> Pp.str " -> ") (pr_constr env evd) l + +let check_typ evd expty op = + let env = Global.env () in + let ty = Retyping.get_type_of env evd op in + let ty = decomp_type evd ty in + if List.for_all2 (EConstr.eq_constr_nounivs evd) ty expty then () + else + raise + (CErrors.user_err + Pp.( + str ": Cannot register operator " + ++ pr_constr env evd op ++ str ". It has type " ++ pp_type env evd ty + ++ str " instead of expected type " + ++ pp_type env evd expty)) + module EBinOp = struct type elt = EBinOpT.t @@ -392,24 +422,28 @@ module EBinOp = struct let table = table let mk_elt evd i a = - let i1 = get_inj evd a.(5) in - let i2 = get_inj evd a.(6) in - let i3 = get_inj evd a.(7) in - let tbop = a.(8) in + let i1 = get_inj evd a.(7) in + let i2 = get_inj evd a.(8) in + let i3 = get_inj evd a.(9) in + let bop = a.(6) in + let tbop = a.(10) in + check_typ evd EInjT.[i1.source; i2.source; i3.source] bop; { source1 = a.(0) ; source2 = a.(1) ; source3 = a.(2) - ; target = a.(3) + ; target1 = a.(3) + ; target2 = a.(4) + ; target3 = a.(5) ; inj1 = i1 ; inj2 = i2 ; inj3 = i3 - ; bop = a.(4) - ; tbop = a.(8) - ; tbopinj = a.(9) + ; bop + ; tbop + ; tbopinj = a.(11) ; classify_binop = - classify_op (mkconvert_binop i1 i2 i3) i1.EInjT.inj a.(4) tbop } + classify_op (mkconvert_binop i1 i2 i3) i3.EInjT.inj a.(6) tbop } - let get_key = 4 + let get_key = 6 let cast x = BinOp x let dest = function BinOp x -> Some x | _ -> None end @@ -452,23 +486,25 @@ module EUnOp = struct let dest = function UnOp x -> Some x | _ -> None let mk_elt evd i a = - let i1 = get_inj evd a.(4) in - let i2 = get_inj evd a.(5) in - let uop = a.(3) in - let tuop = a.(6) in + let i1 = get_inj evd a.(5) in + let i2 = get_inj evd a.(6) in + let uop = a.(4) in + check_typ evd EInjT.[i1.source; i2.source] uop; + let tuop = a.(7) in { source1 = a.(0) ; source2 = a.(1) - ; target = a.(2) + ; target1 = a.(2) + ; target2 = a.(3) ; uop ; inj1_t = i1 ; inj2_t = i2 ; tuop - ; tuopinj = a.(7) + ; tuopinj = a.(8) ; is_construct = EConstr.isConstruct evd uop - ; classify_unop = classify_op (mkconvert_unop i1 i2) i1.EInjT.inj uop tuop + ; classify_unop = classify_op (mkconvert_unop i1 i2) i2.EInjT.inj uop tuop } - let get_key = 3 + let get_key = 4 end module EBinRel = struct @@ -485,6 +521,7 @@ module EBinRel = struct let i = get_inj evd a.(3) in let brel = a.(2) in let tbrel = a.(4) in + check_typ evd EInjT.[i.source; i.source; EConstr.mkProp] brel; { source = a.(0) ; target = a.(1) ; inj = get_inj evd a.(3) @@ -621,19 +658,32 @@ module ESat = struct let get_key = 1 end -module ESpec = struct +module EUnopSpec = struct open ESpecT type elt = ESpecT.t - let name = "Spec" + let name = "UnopSpec" let table = specs - let cast x = Spec x - let dest = function Spec x -> Some x | _ -> None - let mk_elt evd i a = {spec = a.(5)} + let cast x = UnOpSpec x + let dest = function UnOpSpec x -> Some x | _ -> None + let mk_elt evd i a = {spec = a.(4)} let get_key = 2 end +module EBinOpSpec = struct + open ESpecT + + type elt = ESpecT.t + + let name = "BinOpSpec" + let table = specs + let cast x = BinOpSpec x + let dest = function BinOpSpec x -> Some x | _ -> None + let mk_elt evd i a = {spec = a.(5)} + let get_key = 3 +end + module BinOp = MakeTable (EBinOp) module UnOp = MakeTable (EUnOp) module CstOp = MakeTable (ECstOp) @@ -641,7 +691,8 @@ module BinRel = MakeTable (EBinRel) module PropBinOp = MakeTable (EPropBinOp) module PropUnOp = MakeTable (EPropUnOp) module Saturate = MakeTable (ESat) -module Spec = MakeTable (ESpec) +module UnOpSpec = MakeTable (EUnopSpec) +module BinOpSpec = MakeTable (EBinOpSpec) let init_cache () = table_cache := !table; @@ -788,7 +839,8 @@ let app_unop evd src unop arg prf = ( force mkapp , [| unop.source1 ; unop.source2 - ; unop.target + ; unop.target1 + ; unop.target2 ; unop.uop ; unop.inj1_t.EInjT.inj ; unop.inj2_t.EInjT.inj @@ -859,7 +911,9 @@ let app_binop evd src binop arg1 prf1 arg2 prf2 = , [| binop.source1 ; binop.source2 ; binop.source3 - ; binop.target + ; binop.target1 + ; binop.target2 + ; binop.target3 ; binop.bop ; binop.inj1.EInjT.inj ; binop.inj2.EInjT.inj @@ -1366,7 +1420,7 @@ let rec spec_of_term env evd (senv : spec_env) t = with Not_found -> ( try match snd (HConstr.find c !specs_cache) with - | Spec s -> + | UnOpSpec s | BinOpSpec s -> let thm = EConstr.mkApp (s.deriv.ESpecT.spec, a') in register_constr senv' t' thm | _ -> (get_name t' senv', senv') diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli index 7960475def..537e652fd0 100644 --- a/plugins/micromega/zify.mli +++ b/plugins/micromega/zify.mli @@ -21,7 +21,8 @@ module CstOp : S module BinRel : S module PropBinOp : S module PropUnOp : S -module Spec : S +module BinOpSpec : S +module UnOpSpec : S module Saturate : S val zify_tac : unit Proofview.tactic diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v new file mode 100644 index 0000000000..8fd7398638 --- /dev/null +++ b/test-suite/micromega/zify.v @@ -0,0 +1,229 @@ +Require Import BinNums BinInt ZifyInst Zify. + +Definition pos := positive. + +Goal forall (x : pos), x = x. +Proof. + intros. + zify_op. + apply (@eq_refl Z). +Qed. + +Goal (1 <= Pos.to_nat 1)%nat. +Proof. + zify_op. + apply Z.le_refl. +Qed. + +Goal forall (x : positive), not (x = x) -> False. +Proof. + intros. zify_op. + apply H. + apply (@eq_refl Z). +Qed. + +Goal (0 <= 0)%nat. +Proof. + intros. + zify_op. + apply Z.le_refl. +Qed. + + +Lemma N : forall x, (0 <= Z.of_nat x)%Z. +Proof. + intros. + zify. exact cstr. +Defined. + +Lemma N_eq : N = +fun x : nat => let cstr : (0 <= Z.of_nat x)%Z := Znat.Nat2Z.is_nonneg x in cstr. +Proof. + reflexivity. +Qed. + +Goal (Z.of_nat 1 * 0 = 0)%Z. +Proof. + intros. + zify. + match goal with + | |- (1 * 0 = 0)%Z => reflexivity + end. +Qed. + +Lemma C : forall p, + Z.pos p~1 = Z.pos p~1. +Proof. + intros. + zify_op. + reflexivity. +Defined. + +Lemma C_eq : C = fun p : positive => +let cstr : (0 < Z.pos p)%Z := Pos2Z.pos_is_pos p in eq_refl. +Proof. +reflexivity. +Qed. + + +Goal forall p, + (Z.pos p~1 = 2 * Z.pos p + 1)%Z. +Proof. + intros. + zify_op. + reflexivity. +Qed. + +Goal forall z, + (2 * z = 2 * z)%Z. +Proof. + intros. + zify_op. + reflexivity. +Qed. + +Goal (-1= Z.opp 1)%Z. +Proof. + intros. + zify_op. + reflexivity. +Qed. + +Require Import Lia. + +Goal forall n n3, +S n + n3 >= 0 + n. +Proof. + intros. + lia. +Qed. + +Open Scope Z_scope. + +Goal forall p, + False -> + (Pos.to_nat p) = 0%nat. +Proof. + intros. + zify_op. + match goal with + | H : False |- Z.pos p = Z0 => tauto + end. +Qed. + +Goal forall + fibonacci + (p : positive) + (n : nat) + (b : Z) + (H : 0%nat = (S (Pos.to_nat p) - n)%nat) + (H0 : 0 < Z.pos p < b) + (H1 : Z.pos p < fibonacci (S n)), + Z.abs (Z.pos p) < Z.of_nat n. +Proof. + intros. + lia. +Qed. + + + +Section S. + Variable digits : positive. + Hypothesis digits_ne_1 : digits <> 1%positive. + + Lemma spec_more_than_1_digit : (1 < Z.pos digits)%Z. + Proof. lia. Qed. + + Let digits_gt_1 := spec_more_than_1_digit. + + Goal True. + Proof. + intros. + zify. + exact I. + Qed. + +End S. + + +Record Bla : Type := + mk + { + T : Type; + zero : T + }. + +Definition znat := mk nat 0%nat. + +Require Import ZifyClasses. +Require Import ZifyInst. + +Instance Zero : CstOp (@zero znat : nat) := Op_O. +Add CstOp Zero. + + +Goal @zero znat = 0%nat. + zify. + reflexivity. +Qed. + +Goal forall (x y : positive) (F : forall (P: Pos.le x y) , positive) (P : Pos.le x y), + (F P + 1 = 1 + F P)%positive. +Proof. + intros. + zify_op. + apply Z.add_comm. +Qed. + +Goal forall (x y : nat) (F : forall (P: le x y) , nat) (P : le x y), + (F P + 1 = 1 + F P)%nat. +Proof. + intros. + zify_op. + apply Z.add_comm. +Qed. + +Require Import Bool. + +Goal true && false = false. +Proof. + lia. +Qed. + +Goal forall p, p || true = true. +Proof. + lia. +Qed. + +Goal forall x y, Z.eqb x y = true -> x = y. +Proof. + intros. + lia. +Qed. + +Goal forall x, Z.leb x x = true. +Proof. + intros. + lia. +Qed. + +Goal forall x, Z.gtb x x = false. +Proof. + intros. + lia. +Qed. + +Require Import ZifyBool. + +Goal forall x y : nat, Nat.eqb x 1 = true -> + Nat.eqb y 0 = true -> + Nat.eqb (x + y) 1 = true. +Proof. + intros x y. + lia. +Qed. + +Goal forall (f : Z -> bool), negb (negb (f 0)) = f 0. +Proof. + intros. lia. +Qed. diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index d70978fabe..9e10786fcd 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -130,6 +130,8 @@ Definition eqb (b1 b2:bool) : bool := | false, false => true end. +Register eqb as core.bool.eqb. + Lemma eqb_subst : forall (P:bool -> Prop) (b1 b2:bool), eqb b1 b2 = true -> P b1 -> P b2. Proof. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index cba90043d5..8ab12ae534 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -73,6 +73,7 @@ Infix "&&" := andb : bool_scope. Register andb as core.bool.andb. Register orb as core.bool.orb. +Register implb as core.bool.implb. Register xorb as core.bool.xorb. Register negb as core.bool.negb. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 1729b9f85e..a566348dd5 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -47,6 +47,8 @@ Register mul as num.Z.mul. Register pow as num.Z.pow. Register of_nat as num.Z.of_nat. + + (** When including property functors, only inline t eq zero one two *) Set Inline Level 30. @@ -81,6 +83,11 @@ Register le as num.Z.le. Register lt as num.Z.lt. Register ge as num.Z.ge. Register gt as num.Z.gt. +Register leb as num.Z.leb. +Register ltb as num.Z.ltb. +Register geb as num.Z.geb. +Register gtb as num.Z.gtb. +Register eqb as num.Z.eqb. (** * Decidability of equality. *) diff --git a/theories/micromega/Lia.v b/theories/micromega/Lia.v index 3d955fec4f..b2c5884ed7 100644 --- a/theories/micromega/Lia.v +++ b/theories/micromega/Lia.v @@ -19,7 +19,6 @@ Require Import BinNums. Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". - Ltac zchecker := intros ?__wit ?__varmap ?__ff ; exact (ZTautoChecker_sound __ff __wit @@ -30,7 +29,6 @@ Ltac lia := Zify.zify; xlia zchecker. Ltac nia := Zify.zify; xnlia zchecker. - (* Local Variables: *) (* coding: utf-8 *) (* End: *) diff --git a/theories/micromega/QMicromega.v b/theories/micromega/QMicromega.v index 1fbc5a648a..1bb016da9a 100644 --- a/theories/micromega/QMicromega.v +++ b/theories/micromega/QMicromega.v @@ -10,7 +10,7 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* Frédéric Besson (Irisa/Inria) *) (* *) (************************************************************************) @@ -107,7 +107,7 @@ Proof. apply QNpower. Qed. -Definition Qeval_op2 (o : Op2) : Q -> Q -> Prop := +Definition Qeval_pop2 (o : Op2) : Q -> Q -> Prop := match o with | OpEq => Qeq | OpNEq => fun x y => ~ x == y @@ -117,13 +117,63 @@ match o with | OpGt => fun x y => Qlt y x end. -Definition Qeval_formula (e:PolEnv Q) (ff : Formula Q) := - let (lhs,o,rhs) := ff in Qeval_op2 o (Qeval_expr e lhs) (Qeval_expr e rhs). + +Definition Qlt_bool (x y : Q) := + (Qnum x * QDen y <? Qnum y * QDen x)%Z. + +Definition Qeval_bop2 (o : Op2) : Q -> Q -> bool := + match o with + | OpEq => Qeq_bool + | OpNEq => fun x y => negb (Qeq_bool x y) + | OpLe => Qle_bool + | OpGe => fun x y => Qle_bool y x + | OpLt => Qlt_bool + | OpGt => fun x y => Qlt_bool y x + end. + +Lemma Qlt_bool_iff : forall q1 q2, + Qlt_bool q1 q2 = true <-> q1 < q2. +Proof. + unfold Qlt_bool. + unfold Qlt. intros. + apply Z.ltb_lt. +Qed. + +Lemma pop2_bop2 : + forall (op : Op2) (q1 q2 : Q), is_true (Qeval_bop2 op q1 q2) <-> Qeval_pop2 op q1 q2. +Proof. + unfold is_true. + destruct op ; simpl; intros. + - apply Qeq_bool_iff. + - rewrite <- Qeq_bool_iff. + rewrite negb_true_iff. + destruct (Qeq_bool q1 q2) ; intuition congruence. + - apply Qle_bool_iff. + - apply Qle_bool_iff. + - apply Qlt_bool_iff. + - apply Qlt_bool_iff. +Qed. + +Definition Qeval_op2 (k:Tauto.kind) : Op2 -> Q -> Q -> Tauto.rtyp k:= + if k as k0 return (Op2 -> Q -> Q -> Tauto.rtyp k0) + then Qeval_pop2 else Qeval_bop2. + + +Lemma Qeval_op2_hold : forall k op q1 q2, + Tauto.hold k (Qeval_op2 k op q1 q2) <-> Qeval_pop2 op q1 q2. +Proof. + destruct k. + simpl ; tauto. + simpl. apply pop2_bop2. +Qed. + +Definition Qeval_formula (e:PolEnv Q) (k: Tauto.kind) (ff : Formula Q) := + let (lhs,o,rhs) := ff in Qeval_op2 k o (Qeval_expr e lhs) (Qeval_expr e rhs). Definition Qeval_formula' := eval_formula Qplus Qmult Qminus Qopp Qeq Qle Qlt (fun x => x) (fun x => x) (pow_N 1 Qmult). -Lemma Qeval_formula_compat : forall env f, Qeval_formula env f <-> Qeval_formula' env f. + Lemma Qeval_formula_compat : forall env b f, Tauto.hold b (Qeval_formula env b f) <-> Qeval_formula' env f. Proof. intros. unfold Qeval_formula. @@ -131,6 +181,8 @@ Proof. repeat rewrite Qeval_expr_compat. unfold Qeval_formula'. unfold Qeval_expr'. + simpl. + rewrite Qeval_op2_hold. split ; destruct Fop ; simpl; auto. Qed. @@ -186,10 +238,10 @@ Definition qdeduce := nformula_plus_nformula 0 Qplus Qeq_bool. Definition normQ := norm 0 1 Qplus Qmult Qminus Qopp Qeq_bool. Declare Equivalent Keys normQ RingMicromega.norm. -Definition cnfQ (Annot TX AF: Type) (f: TFormula (Formula Q) Annot TX AF) := +Definition cnfQ (Annot:Type) (TX: Tauto.kind -> Type) (AF: Type) (k: Tauto.kind) (f: TFormula (Formula Q) Annot TX AF k) := rxcnf qunsat qdeduce (Qnormalise Annot) (Qnegate Annot) true f. -Definition QTautoChecker (f : BFormula (Formula Q)) (w: list QWitness) : bool := +Definition QTautoChecker (f : BFormula (Formula Q) Tauto.isProp) (w: list QWitness) : bool := @tauto_checker (Formula Q) (NFormula Q) unit qunsat qdeduce (Qnormalise unit) @@ -208,8 +260,11 @@ Proof. destruct t. apply (check_inconsistent_sound Qsor QSORaddon) ; auto. - unfold qdeduce. intros. revert H. apply (nformula_plus_nformula_correct Qsor QSORaddon);auto. - - intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now eapply (cnf_normalise_correct Qsor QSORaddon);eauto. - - intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now eapply (cnf_negate_correct Qsor QSORaddon);eauto. + - intros. + rewrite Qeval_formula_compat. + eapply (cnf_normalise_correct Qsor QSORaddon) ; eauto. + - intros. rewrite Tauto.hold_eNOT. rewrite Qeval_formula_compat. + now eapply (cnf_negate_correct Qsor QSORaddon);eauto. - intros t w0. unfold eval_tt. intros. diff --git a/theories/micromega/RMicromega.v b/theories/micromega/RMicromega.v index fd8903eac9..7e2694a519 100644 --- a/theories/micromega/RMicromega.v +++ b/theories/micromega/RMicromega.v @@ -10,19 +10,18 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* Frédéric Besson (Irisa/Inria) *) (* *) (************************************************************************) Require Import OrderedRing. -Require Import RingMicromega. +Require Import QMicromega RingMicromega. Require Import Refl. -Require Import Raxioms Rfunctions RIneq Rpow_def. +Require Import Sumbool Raxioms Rfunctions RIneq Rpow_def. Require Import QArith. Require Import Qfield. Require Import Qreals. Require Import DeclConstant. -Require Import Ztac. Require Setoid. (*Declare ML Module "micromega_plugin".*) @@ -344,16 +343,17 @@ Proof. apply Qeq_bool_eq in C2. rewrite C2. simpl. - rewrite Qpower0. + assert (z <> 0%Z). + { intro ; subst. apply Z.lt_irrefl in C1. auto. } + rewrite Qpower0 by auto. apply Q2R_0. - intro ; subst ; slia C1 C1. + rewrite Q2RpowerRZ. rewrite IHc. reflexivity. rewrite andb_false_iff in C. destruct C. simpl. apply Z.ltb_ge in H. - right ; normZ. slia H H0. + right. Ztac.normZ. Ztac.slia H H0. left ; apply Qeq_bool_neq; auto. + simpl. rewrite <- IHc. @@ -382,7 +382,7 @@ Definition INZ (n:N) : R := Definition Reval_expr := eval_pexpr Rplus Rmult Rminus Ropp R_of_Rcst N.to_nat pow. -Definition Reval_op2 (o:Op2) : R -> R -> Prop := +Definition Reval_pop2 (o:Op2) : R -> R -> Prop := match o with | OpEq => @eq R | OpNEq => fun x y => ~ x = y @@ -392,27 +392,91 @@ Definition Reval_op2 (o:Op2) : R -> R -> Prop := | OpGt => Rgt end. +Definition sumboolb {A B : Prop} (x : @sumbool A B) : bool := + if x then true else false. -Definition Reval_formula (e: PolEnv R) (ff : Formula Rcst) := - let (lhs,o,rhs) := ff in Reval_op2 o (Reval_expr e lhs) (Reval_expr e rhs). + +Definition Reval_bop2 (o : Op2) : R -> R -> bool := + match o with + | OpEq => fun x y => sumboolb (Req_EM_T x y) + | OpNEq => fun x y => negb (sumboolb (Req_EM_T x y)) + | OpLe => fun x y => (sumboolb (Rle_lt_dec x y)) + | OpGe => fun x y => (sumboolb (Rge_gt_dec x y)) + | OpLt => fun x y => (sumboolb (Rlt_le_dec x y)) + | OpGt => fun x y => (sumboolb (Rgt_dec x y)) + end. + +Lemma pop2_bop2 : + forall (op : Op2) (r1 r2 : R), is_true (Reval_bop2 op r1 r2) <-> Reval_pop2 op r1 r2. +Proof. + unfold is_true. + destruct op ; simpl; intros; + match goal with + | |- context[sumboolb (?F ?X ?Y)] => + destruct (F X Y) ; simpl; intuition try congruence + end. + - apply Rlt_not_le in r. tauto. + - apply Rgt_not_ge in r. tauto. + - apply Rlt_not_le in H. tauto. +Qed. + +Definition Reval_op2 (k: Tauto.kind) : Op2 -> R -> R -> Tauto.rtyp k:= + if k as k0 return (Op2 -> R -> R -> Tauto.rtyp k0) + then Reval_pop2 else Reval_bop2. + +Lemma Reval_op2_hold : forall b op q1 q2, + Tauto.hold b (Reval_op2 b op q1 q2) <-> Reval_pop2 op q1 q2. +Proof. + destruct b. + simpl ; tauto. + simpl. apply pop2_bop2. +Qed. + +Definition Reval_formula (e: PolEnv R) (k: Tauto.kind) (ff : Formula Rcst) := + let (lhs,o,rhs) := ff in Reval_op2 k o (Reval_expr e lhs) (Reval_expr e rhs). Definition Reval_formula' := eval_sformula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt N.to_nat pow R_of_Rcst. -Definition QReval_formula := - eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt Q2R N.to_nat pow . +Lemma Reval_pop2_eval_op2 : forall o e1 e2, + Reval_pop2 o e1 e2 <-> + eval_op2 eq Rle Rlt o e1 e2. +Proof. + destruct o ; simpl ; try tauto. + split. + apply Rge_le. + apply Rle_ge. +Qed. -Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f. +Lemma Reval_formula_compat : forall env b f, Tauto.hold b (Reval_formula env b f) <-> Reval_formula' env f. Proof. intros. unfold Reval_formula. destruct f. unfold Reval_formula'. - unfold Reval_expr. - split ; destruct Fop ; simpl ; auto. - apply Rge_le. - apply Rle_ge. + simpl. + rewrite Reval_op2_hold. + apply Reval_pop2_eval_op2. +Qed. + +Definition QReval_expr := eval_pexpr Rplus Rmult Rminus Ropp Q2R to_nat pow. + +Definition QReval_formula (e: PolEnv R) (k: Tauto.kind) (ff : Formula Q) := + let (lhs,o,rhs) := ff in Reval_op2 k o (QReval_expr e lhs) (QReval_expr e rhs). + + +Definition QReval_formula' := + eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt Q2R N.to_nat pow. + +Lemma QReval_formula_compat : forall env b f, Tauto.hold b (QReval_formula env b f) <-> QReval_formula' env f. +Proof. + intros. + unfold QReval_formula. + destruct f. + unfold QReval_formula'. + rewrite Reval_op2_hold. + apply Reval_pop2_eval_op2. Qed. Definition Qeval_nformula := @@ -451,7 +515,7 @@ Definition runsat := check_inconsistent 0%Q Qeq_bool Qle_bool. Definition rdeduce := nformula_plus_nformula 0%Q Qplus Qeq_bool. -Definition RTautoChecker (f : BFormula (Formula Rcst)) (w: list RWitness) : bool := +Definition RTautoChecker (f : BFormula (Formula Rcst) Tauto.isProp) (w: list RWitness) : bool := @tauto_checker (Formula Q) (NFormula Q) unit runsat rdeduce (Rnormalise unit) (Rnegate unit) @@ -463,18 +527,20 @@ Proof. unfold RTautoChecker. intros TC env. apply tauto_checker_sound with (eval:=QReval_formula) (eval':= Qeval_nformula) (env := env) in TC. - - change (eval_f (fun x : Prop => x) (QReval_formula env)) + - change (eval_f e_rtyp (QReval_formula env)) with (eval_bf (QReval_formula env)) in TC. rewrite eval_bf_map in TC. unfold eval_bf in TC. rewrite eval_f_morph with (ev':= Reval_formula env) in TC ; auto. - intro. - unfold QReval_formula. - rewrite <- eval_formulaSC with (phiS := R_of_Rcst). - rewrite Reval_formula_compat. - tauto. - intro. rewrite Q_of_RcstR. reflexivity. + intros. + apply Tauto.hold_eiff. + rewrite QReval_formula_compat. + unfold QReval_formula'. + rewrite <- eval_formulaSC with (phiS := R_of_Rcst). + rewrite Reval_formula_compat. + tauto. + intro. rewrite Q_of_RcstR. reflexivity. - apply Reval_nformula_dec. - destruct t. @@ -482,8 +548,12 @@ Proof. - unfold rdeduce. intros. revert H. eapply (nformula_plus_nformula_correct Rsor QSORaddon); eauto. - - now apply (cnf_normalise_correct Rsor QSORaddon). - - intros. now eapply (cnf_negate_correct Rsor QSORaddon); eauto. + - + intros. + rewrite QReval_formula_compat. + eapply (cnf_normalise_correct Rsor QSORaddon) ; eauto. + - intros. rewrite Tauto.hold_eNOT. rewrite QReval_formula_compat. + now eapply (cnf_negate_correct Rsor QSORaddon); eauto. - intros t w0. unfold eval_tt. intros. diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v index 6e89089355..dddced5739 100644 --- a/theories/micromega/Tauto.v +++ b/theories/micromega/Tauto.v @@ -17,49 +17,64 @@ Require Import List. Require Import Refl. Require Import Bool. +Require Import Relation_Definitions Setoid. Set Implicit Arguments. +(** Formulae are either interpreted over Prop or bool. *) +Inductive kind : Type := +|isProp +|isBool. + +Register isProp as micromega.kind.isProp. +Register isBool as micromega.kind.isBool. + Section S. Context {TA : Type}. (* type of interpreted atoms *) - Context {TX : Type}. (* type of uninterpreted terms (Prop) *) + Context {TX : kind -> Type}. (* type of uninterpreted terms (Prop) *) Context {AA : Type}. (* type of annotations for atoms *) Context {AF : Type}. (* type of formulae identifiers *) - Inductive GFormula : Type := - | TT : GFormula - | FF : GFormula - | X : TX -> GFormula - | A : TA -> AA -> GFormula - | Cj : GFormula -> GFormula -> GFormula - | D : GFormula -> GFormula -> GFormula - | N : GFormula -> GFormula - | I : GFormula -> option AF -> GFormula -> GFormula. + Inductive GFormula : kind -> Type := + | TT : forall (k: kind), GFormula k + | FF : forall (k: kind), GFormula k + | X : forall (k: kind), TX k -> GFormula k + | A : forall (k: kind), TA -> AA -> GFormula k + | AND : forall (k: kind), GFormula k -> GFormula k -> GFormula k + | OR : forall (k: kind), GFormula k -> GFormula k -> GFormula k + | NOT : forall (k: kind), GFormula k -> GFormula k + | IMPL : forall (k: kind), GFormula k -> option AF -> GFormula k -> GFormula k + | IFF : forall (k: kind), GFormula k -> GFormula k -> GFormula k + | EQ : GFormula isBool -> GFormula isBool -> GFormula isProp. Register TT as micromega.GFormula.TT. Register FF as micromega.GFormula.FF. Register X as micromega.GFormula.X. Register A as micromega.GFormula.A. - Register Cj as micromega.GFormula.Cj. - Register D as micromega.GFormula.D. - Register N as micromega.GFormula.N. - Register I as micromega.GFormula.I. + Register AND as micromega.GFormula.AND. + Register OR as micromega.GFormula.OR. + Register NOT as micromega.GFormula.NOT. + Register IMPL as micromega.GFormula.IMPL. + Register IFF as micromega.GFormula.IFF. + Register EQ as micromega.GFormula.EQ. Section MAPX. - Variable F : TX -> TX. + Variable F : forall k, TX k -> TX k. - Fixpoint mapX (f : GFormula) : GFormula := + Fixpoint mapX (k:kind) (f : GFormula k) : GFormula k := match f with - | TT => TT - | FF => FF - | X x => X (F x) - | A a an => A a an - | Cj f1 f2 => Cj (mapX f1) (mapX f2) - | D f1 f2 => D (mapX f1) (mapX f2) - | N f => N (mapX f) - | I f1 o f2 => I (mapX f1) o (mapX f2) + | TT k => TT k + | FF k => FF k + | X x => X (F x) + | A k a an => A k a an + | AND f1 f2 => AND (mapX f1) (mapX f2) + | OR f1 f2 => OR (mapX f1) (mapX f2) + | NOT f => NOT (mapX f) + | IMPL f1 o f2 => IMPL (mapX f1) o (mapX f2) + | IFF f1 f2 => IFF (mapX f1) (mapX f2) + | EQ f1 f2 => EQ (mapX f1) (mapX f2) end. End MAPX. @@ -68,16 +83,17 @@ Section S. Variable ACC : Type. Variable F : ACC -> AA -> ACC. - Fixpoint foldA (f : GFormula) (acc : ACC) : ACC := + Fixpoint foldA (k: kind) (f : GFormula k) (acc : ACC) : ACC := match f with - | TT => acc - | FF => acc + | TT _ => acc + | FF _ => acc | X x => acc - | A a an => F acc an - | Cj f1 f2 - | D f1 f2 - | I f1 _ f2 => foldA f1 (foldA f2 acc) - | N f => foldA f acc + | A _ a an => F acc an + | AND f1 f2 + | OR f1 f2 + | IFF f1 f2 + | IMPL f1 _ f2 | EQ f1 f2 => foldA f1 (foldA f2 acc) + | NOT f => foldA f acc end. End FOLDANNOT. @@ -89,84 +105,212 @@ Section S. | Some id => id :: l end. - Fixpoint ids_of_formula f := + Fixpoint ids_of_formula (k: kind) (f:GFormula k) := match f with - | I f id f' => cons_id id (ids_of_formula f') + | IMPL f id f' => cons_id id (ids_of_formula f') | _ => nil end. - Fixpoint collect_annot (f : GFormula) : list AA := + Fixpoint collect_annot (k: kind) (f : GFormula k) : list AA := match f with - | TT | FF | X _ => nil - | A _ a => a ::nil - | Cj f1 f2 - | D f1 f2 - | I f1 _ f2 => collect_annot f1 ++ collect_annot f2 - | N f => collect_annot f + | TT _ | FF _ | X _ => nil + | A _ _ a => a ::nil + | AND f1 f2 + | OR f1 f2 + | IFF f1 f2 | EQ f1 f2 + | IMPL f1 _ f2 => collect_annot f1 ++ collect_annot f2 + | NOT f => collect_annot f end. - Variable ex : TX -> Prop. (* [ex] will be the identity *) + Definition rtyp (k: kind) : Type := if k then Prop else bool. - Section EVAL. + Variable ex : forall (k: kind), TX k -> rtyp k. (* [ex] will be the identity *) - Variable ea : TA -> Prop. + Section EVAL. - Fixpoint eval_f (f:GFormula) {struct f}: Prop := - match f with - | TT => True - | FF => False - | A a _ => ea a - | X p => ex p - | Cj e1 e2 => (eval_f e1) /\ (eval_f e2) - | D e1 e2 => (eval_f e1) \/ (eval_f e2) - | N e => ~ (eval_f e) - | I f1 _ f2 => (eval_f f1) -> (eval_f f2) - end. + Variable ea : forall (k: kind), TA -> rtyp k. + + Definition eTT (k: kind) : rtyp k := + if k as k' return rtyp k' then True else true. + + Definition eFF (k: kind) : rtyp k := + if k as k' return rtyp k' then False else false. + + Definition eAND (k: kind) : rtyp k -> rtyp k -> rtyp k := + if k as k' return rtyp k' -> rtyp k' -> rtyp k' + then and else andb. + + Definition eOR (k: kind) : rtyp k -> rtyp k -> rtyp k := + if k as k' return rtyp k' -> rtyp k' -> rtyp k' + then or else orb. + + Definition eIMPL (k: kind) : rtyp k -> rtyp k -> rtyp k := + if k as k' return rtyp k' -> rtyp k' -> rtyp k' + then (fun x y => x -> y) else implb. + + Definition eIFF (k: kind) : rtyp k -> rtyp k -> rtyp k := + if k as k' return rtyp k' -> rtyp k' -> rtyp k' + then iff else eqb. + + Definition eNOT (k: kind) : rtyp k -> rtyp k := + if k as k' return rtyp k' -> rtyp k' + then not else negb. + + Fixpoint eval_f (k: kind) (f:GFormula k) {struct f}: rtyp k := + match f in GFormula k' return rtyp k' with + | TT tk => eTT tk + | FF tk => eFF tk + | A k a _ => ea k a + | X p => ex p + | @AND k e1 e2 => eAND k (eval_f e1) (eval_f e2) + | @OR k e1 e2 => eOR k (eval_f e1) (eval_f e2) + | @NOT k e => eNOT k (eval_f e) + | @IMPL k f1 _ f2 => eIMPL k (eval_f f1) (eval_f f2) + | @IFF k f1 f2 => eIFF k (eval_f f1) (eval_f f2) + | EQ f1 f2 => (eval_f f1) = (eval_f f2) + end. + Lemma eval_f_rew : forall k (f:GFormula k), + eval_f f = + match f in GFormula k' return rtyp k' with + | TT tk => eTT tk + | FF tk => eFF tk + | A k a _ => ea k a + | X p => ex p + | @AND k e1 e2 => eAND k (eval_f e1) (eval_f e2) + | @OR k e1 e2 => eOR k (eval_f e1) (eval_f e2) + | @NOT k e => eNOT k (eval_f e) + | @IMPL k f1 _ f2 => eIMPL k (eval_f f1) (eval_f f2) + | @IFF k f1 f2 => eIFF k (eval_f f1) (eval_f f2) + | EQ f1 f2 => (eval_f f1) = (eval_f f2) + end. + Proof. + destruct f ; reflexivity. + Qed. End EVAL. + Definition hold (k: kind) : rtyp k -> Prop := + if k as k0 return (rtyp k0 -> Prop) then fun x => x else is_true. + Definition eiff (k: kind) : rtyp k -> rtyp k -> Prop := + if k as k' return rtyp k' -> rtyp k' -> Prop then iff else @eq bool. + Lemma eiff_refl : forall (k: kind) (x : rtyp k), + eiff k x x. + Proof. + destruct k ; simpl; tauto. + Qed. - Lemma eval_f_morph : - forall (ev ev' : TA -> Prop) (f : GFormula), - (forall a, ev a <-> ev' a) -> (eval_f ev f <-> eval_f ev' f). + Lemma eiff_sym : forall k (x y : rtyp k), eiff k x y -> eiff k y x. + Proof. + destruct k ; simpl; intros ; intuition. + Qed. + + Lemma eiff_trans : forall k (x y z : rtyp k), eiff k x y -> eiff k y z -> eiff k x z. + Proof. + destruct k ; simpl; intros ; intuition congruence. + Qed. + + Lemma hold_eiff : forall (k: kind) (x y : rtyp k), + (hold k x <-> hold k y) <-> eiff k x y. + Proof. + destruct k ; simpl. + - tauto. + - unfold is_true. + destruct x,y ; intuition congruence. + Qed. + + Instance eiff_eq (k: kind) : Equivalence (eiff k). + Proof. + constructor. + - exact (eiff_refl k). + - exact (eiff_sym k). + - exact (eiff_trans k). + Qed. + + Add Parametric Morphism (k: kind) : (@eAND k) with signature eiff k ==> eiff k ==> eiff k as eAnd_morph. + Proof. + intros. + destruct k ; simpl in *; intuition congruence. + Qed. + + Add Parametric Morphism (k: kind) : (@eOR k) with signature eiff k ==> eiff k ==> eiff k as eOR_morph. + Proof. + intros. + destruct k ; simpl in *; intuition congruence. + Qed. + + Add Parametric Morphism (k: kind) : (@eIMPL k) with signature eiff k ==> eiff k ==> eiff k as eIMPL_morph. + Proof. + intros. + destruct k ; simpl in *; intuition congruence. + Qed. + + Add Parametric Morphism (k: kind) : (@eIFF k) with signature eiff k ==> eiff k ==> eiff k as eIFF_morph. Proof. - induction f ; simpl ; try tauto. intros. - apply H. + destruct k ; simpl in *; intuition congruence. Qed. + Add Parametric Morphism (k: kind) : (@eNOT k) with signature eiff k ==> eiff k as eNOT_morph. + Proof. + intros. + destruct k ; simpl in *; intuition congruence. + Qed. + + Lemma eval_f_morph : + forall (ev ev' : forall (k: kind), TA -> rtyp k), + (forall k a, eiff k (ev k a) (ev' k a)) -> + forall (k: kind)(f : GFormula k), + (eiff k (eval_f ev f) (eval_f ev' f)). + Proof. + induction f ; simpl. + - reflexivity. + - reflexivity. + - reflexivity. + - apply H. + - rewrite IHf1. rewrite IHf2. reflexivity. + - rewrite IHf1. rewrite IHf2. reflexivity. + - rewrite IHf. reflexivity. + - rewrite IHf1. rewrite IHf2. reflexivity. + - rewrite IHf1. rewrite IHf2. reflexivity. + - simpl in *. intuition congruence. + Qed. End S. (** Typical boolean formulae *) -Definition BFormula (A : Type) := @GFormula A Prop unit unit. +Definition eKind (k: kind) := if k then Prop else bool. +Register eKind as micromega.eKind. + +Definition BFormula (A : Type) := @GFormula A eKind unit unit. Register BFormula as micromega.BFormula.type. Section MAPATOMS. Context {TA TA':Type}. - Context {TX : Type}. + Context {TX : kind -> Type}. Context {AA : Type}. Context {AF : Type}. -Fixpoint map_bformula (fct : TA -> TA') (f : @GFormula TA TX AA AF ) : @GFormula TA' TX AA AF := - match f with - | TT => TT - | FF => FF - | X p => X p - | A a t => A (fct a) t - | Cj f1 f2 => Cj (map_bformula fct f1) (map_bformula fct f2) - | D f1 f2 => D (map_bformula fct f1) (map_bformula fct f2) - | N f => N (map_bformula fct f) - | I f1 a f2 => I (map_bformula fct f1) a (map_bformula fct f2) - end. + Fixpoint map_bformula (k: kind)(fct : TA -> TA') (f : @GFormula TA TX AA AF k) : @GFormula TA' TX AA AF k:= + match f with + | TT k => TT k + | FF k => FF k + | X k p => X k p + | A k a t => A k (fct a) t + | AND f1 f2 => AND (map_bformula fct f1) (map_bformula fct f2) + | OR f1 f2 => OR (map_bformula fct f1) (map_bformula fct f2) + | NOT f => NOT (map_bformula fct f) + | IMPL f1 a f2 => IMPL (map_bformula fct f1) a (map_bformula fct f2) + | IFF f1 f2 => IFF (map_bformula fct f1) (map_bformula fct f2) + | EQ f1 f2 => EQ (map_bformula fct f1) (map_bformula fct f2) + end. End MAPATOMS. @@ -204,345 +348,458 @@ Section S. (** Our cnf is optimised and detects contradictions on the fly. *) Fixpoint add_term (t: Term' * Annot) (cl : clause) : option clause := - match cl with - | nil => - match deduce (fst t) (fst t) with - | None => Some (t ::nil) - | Some u => if unsat u then None else Some (t::nil) + match cl with + | nil => + match deduce (fst t) (fst t) with + | None => Some (t ::nil) + | Some u => if unsat u then None else Some (t::nil) + end + | t'::cl => + match deduce (fst t) (fst t') with + | None => + match add_term t cl with + | None => None + | Some cl' => Some (t' :: cl') end - | t'::cl => - match deduce (fst t) (fst t') with - | None => + | Some u => + if unsat u then None else match add_term t cl with | None => None | Some cl' => Some (t' :: cl') end - | Some u => - if unsat u then None else - match add_term t cl with - | None => None - | Some cl' => Some (t' :: cl') - end + end + end. + + Fixpoint or_clause (cl1 cl2 : clause) : option clause := + match cl1 with + | nil => Some cl2 + | t::cl => match add_term t cl2 with + | None => None + | Some cl' => or_clause cl cl' + end + end. + + Definition xor_clause_cnf (t:clause) (f:cnf) : cnf := + List.fold_left (fun acc e => + match or_clause t e with + | None => acc + | Some cl => cl :: acc + end) f nil . + + Definition or_clause_cnf (t: clause) (f:cnf) : cnf := + match t with + | nil => f + | _ => xor_clause_cnf t f + end. + + + Fixpoint or_cnf (f : cnf) (f' : cnf) {struct f}: cnf := + match f with + | nil => cnf_tt + | e :: rst => (or_cnf rst f') +++ (or_clause_cnf e f') + end. + + + Definition and_cnf (f1 : cnf) (f2 : cnf) : cnf := + f1 +++ f2. + + (** TX is Prop in Coq and EConstr.constr in Ocaml. + AF is unit in Coq and Names.Id.t in Ocaml + *) + Definition TFormula (TX: kind -> Type) (AF: Type) := @GFormula Term TX Annot AF. + + + Definition is_cnf_tt (c : cnf) : bool := + match c with + | nil => true + | _ => false + end. + + Definition is_cnf_ff (c : cnf) : bool := + match c with + | nil::nil => true + | _ => false + end. + + Definition and_cnf_opt (f1 : cnf) (f2 : cnf) : cnf := + if is_cnf_ff f1 || is_cnf_ff f2 + then cnf_ff + else + if is_cnf_tt f2 + then f1 + else and_cnf f1 f2. + + + Definition or_cnf_opt (f1 : cnf) (f2 : cnf) : cnf := + if is_cnf_tt f1 || is_cnf_tt f2 + then cnf_tt + else if is_cnf_ff f2 + then f1 else or_cnf f1 f2. + + Section REC. + Context {TX : kind -> Type}. + Context {AF : Type}. + + Variable REC : forall (pol : bool) (k: kind) (f : TFormula TX AF k), cnf. + + Definition mk_and (k: kind) (pol:bool) (f1 f2 : TFormula TX AF k):= + (if pol then and_cnf_opt else or_cnf_opt) (REC pol f1) (REC pol f2). + + Definition mk_or (k: kind) (pol:bool) (f1 f2 : TFormula TX AF k):= + (if pol then or_cnf_opt else and_cnf_opt) (REC pol f1) (REC pol f2). + + Definition mk_impl (k: kind) (pol:bool) (f1 f2 : TFormula TX AF k):= + (if pol then or_cnf_opt else and_cnf_opt) (REC (negb pol) f1) (REC pol f2). + + + Definition mk_iff (k: kind) (pol:bool) (f1 f2: TFormula TX AF k):= + or_cnf_opt (and_cnf_opt (REC (negb pol) f1) (REC false f2)) + (and_cnf_opt (REC pol f1) (REC true f2)). + + + End REC. + + Definition is_bool {TX : kind -> Type} {AF: Type} (k: kind) (f : TFormula TX AF k) := + match f with + | TT _ => Some true + | FF _ => Some false + | _ => None + end. + + Lemma is_bool_inv : forall {TX : kind -> Type} {AF: Type} (k: kind) (f : TFormula TX AF k) res, + is_bool f = Some res -> f = if res then TT _ else FF _. + Proof. + intros. + destruct f ; inversion H; reflexivity. + Qed. + + + Fixpoint xcnf {TX : kind -> Type} {AF: Type} (pol : bool) (k: kind) (f : TFormula TX AF k) {struct f}: cnf := + match f with + | TT _ => if pol then cnf_tt else cnf_ff + | FF _ => if pol then cnf_ff else cnf_tt + | X _ p => if pol then cnf_ff else cnf_ff (* This is not complete - cannot negate any proposition *) + | A _ x t => if pol then normalise x t else negate x t + | NOT e => xcnf (negb pol) e + | AND e1 e2 => mk_and xcnf pol e1 e2 + | OR e1 e2 => mk_or xcnf pol e1 e2 + | IMPL e1 _ e2 => mk_impl xcnf pol e1 e2 + | IFF e1 e2 => match is_bool e2 with + | Some isb => xcnf (if isb then pol else negb pol) e1 + | None => mk_iff xcnf pol e1 e2 + end + | EQ e1 e2 => + match is_bool e2 with + | Some isb => xcnf (if isb then pol else negb pol) e1 + | None => mk_iff xcnf pol e1 e2 + end + end. + + Section CNFAnnot. + + (** Records annotations used to optimise the cnf. + Those need to be kept when pruning the formula. + For efficiency, this is a separate function. + *) + + Fixpoint radd_term (t : Term' * Annot) (cl : clause) : clause + list Annot := + match cl with + | nil => (* if t is unsat, the clause is empty BUT t is needed. *) + match deduce (fst t) (fst t) with + | Some u => if unsat u then inr ((snd t)::nil) else inl (t::nil) + | None => inl (t::nil) + end + | t'::cl => (* if t /\ t' is unsat, the clause is empty BUT t & t' are needed *) + match deduce (fst t) (fst t') with + | Some u => if unsat u then inr ((snd t)::(snd t')::nil) + else match radd_term t cl with + | inl cl' => inl (t'::cl') + | inr l => inr l + end + | None => match radd_term t cl with + | inl cl' => inl (t'::cl') + | inr l => inr l + end end end. - Fixpoint or_clause (cl1 cl2 : clause) : option clause := + Fixpoint ror_clause cl1 cl2 := match cl1 with - | nil => Some cl2 - | t::cl => match add_term t cl2 with - | None => None - | Some cl' => or_clause cl cl' + | nil => inl cl2 + | t::cl => match radd_term t cl2 with + | inl cl' => ror_clause cl cl' + | inr l => inr l end end. - Definition xor_clause_cnf (t:clause) (f:cnf) : cnf := - List.fold_left (fun acc e => - match or_clause t e with - | None => acc - | Some cl => cl :: acc - end) f nil . + Definition xror_clause_cnf t f := + List.fold_left (fun '(acc,tg) e => + match ror_clause t e with + | inl cl => (cl :: acc,tg) + | inr l => (acc,tg+++l) + end) f (nil,nil). - Definition or_clause_cnf (t: clause) (f:cnf) : cnf := + Definition ror_clause_cnf t f := match t with - | nil => f - | _ => xor_clause_cnf t f + | nil => (f,nil) + | _ => xror_clause_cnf t f end. - Fixpoint or_cnf (f : cnf) (f' : cnf) {struct f}: cnf := + Fixpoint ror_cnf (f f':list clause) := match f with - | nil => cnf_tt - | e :: rst => (or_cnf rst f') +++ (or_clause_cnf e f') + | nil => (cnf_tt,nil) + | e :: rst => + let (rst_f',t) := ror_cnf rst f' in + let (e_f', t') := ror_clause_cnf e f' in + (rst_f' +++ e_f', t +++ t') end. + Definition annot_of_clause (l : clause) : list Annot := + List.map snd l. - Definition and_cnf (f1 : cnf) (f2 : cnf) : cnf := - f1 +++ f2. + Definition annot_of_cnf (f : cnf) : list Annot := + List.fold_left (fun acc e => annot_of_clause e +++ acc ) f nil. - (** TX is Prop in Coq and EConstr.constr in Ocaml. - AF i s unit in Coq and Names.Id.t in Ocaml - *) - Definition TFormula (TX: Type) (AF: Type) := @GFormula Term TX Annot AF. + Definition ror_cnf_opt f1 f2 := + if is_cnf_tt f1 + then (cnf_tt , nil) + else if is_cnf_tt f2 + then (cnf_tt, nil) + else if is_cnf_ff f2 + then (f1,nil) + else ror_cnf f1 f2. - Definition is_cnf_tt (c : cnf) : bool := - match c with - | nil => true - | _ => false - end. - Definition is_cnf_ff (c : cnf) : bool := - match c with - | nil::nil => true - | _ => false + Definition ocons {A : Type} (o : option A) (l : list A) : list A := + match o with + | None => l + | Some e => e ::l end. - Definition and_cnf_opt (f1 : cnf) (f2 : cnf) : cnf := - if is_cnf_ff f1 || is_cnf_ff f2 - then cnf_ff - else and_cnf f1 f2. - - Definition or_cnf_opt (f1 : cnf) (f2 : cnf) : cnf := - if is_cnf_tt f1 || is_cnf_tt f2 - then cnf_tt - else if is_cnf_ff f2 - then f1 else or_cnf f1 f2. + Definition ratom (c : cnf) (a : Annot) : cnf * list Annot := + if is_cnf_ff c || is_cnf_tt c + then (c,a::nil) + else (c,nil). (* t is embedded in c *) + + Section REC. + Context {TX : kind -> Type} {AF : Type}. + + Variable RXCNF : forall (polarity: bool) (k: kind) (f: TFormula TX AF k) , cnf * list Annot. + + Definition rxcnf_and (polarity:bool) (k: kind) (e1 e2 : TFormula TX AF k) := + let '(e1,t1) := RXCNF polarity e1 in + let '(e2,t2) := RXCNF polarity e2 in + if polarity + then (and_cnf_opt e1 e2, t1 +++ t2) + else let (f',t') := ror_cnf_opt e1 e2 in + (f', t1 +++ t2 +++ t'). + + Definition rxcnf_or (polarity:bool) (k: kind) (e1 e2 : TFormula TX AF k) := + let '(e1,t1) := RXCNF polarity e1 in + let '(e2,t2) := RXCNF polarity e2 in + if polarity + then let (f',t') := ror_cnf_opt e1 e2 in + (f', t1 +++ t2 +++ t') + else (and_cnf_opt e1 e2, t1 +++ t2). + + Definition rxcnf_impl (polarity:bool) (k: kind) (e1 e2 : TFormula TX AF k) := + let '(e1 , t1) := (RXCNF (negb polarity) e1) in + if polarity + then + if is_cnf_ff e1 + then + RXCNF polarity e2 + else (* compute disjunction *) + let '(e2 , t2) := (RXCNF polarity e2) in + let (f',t') := ror_cnf_opt e1 e2 in + (f', t1 +++ t2 +++ t') (* record the hypothesis *) + else + let '(e2 , t2) := (RXCNF polarity e2) in + (and_cnf_opt e1 e2, t1 +++ t2). + + Definition rxcnf_iff (polarity:bool) (k: kind) (e1 e2 : TFormula TX AF k) := + let '(c1,t1) := RXCNF (negb polarity) e1 in + let '(c2,t2) := RXCNF false e2 in + let '(c3,t3) := RXCNF polarity e1 in + let '(c4,t4) := RXCNF true e2 in + let (f',t') := ror_cnf_opt (and_cnf_opt c1 c2) (and_cnf_opt c3 c4) in + (f', t1+++ t2+++t3 +++ t4 +++ t') + . + + End REC. + + Fixpoint rxcnf {TX : kind -> Type} {AF: Type}(polarity : bool) (k: kind) (f : TFormula TX AF k) : cnf * list Annot := - Fixpoint xcnf {TX AF: Type} (pol : bool) (f : TFormula TX AF) {struct f}: cnf := match f with - | TT => if pol then cnf_tt else cnf_ff - | FF => if pol then cnf_ff else cnf_tt - | X p => if pol then cnf_ff else cnf_ff (* This is not complete - cannot negate any proposition *) - | A x t => if pol then normalise x t else negate x t - | N e => xcnf (negb pol) e - | Cj e1 e2 => - (if pol then and_cnf_opt else or_cnf_opt) (xcnf pol e1) (xcnf pol e2) - | D e1 e2 => (if pol then or_cnf_opt else and_cnf_opt) (xcnf pol e1) (xcnf pol e2) - | I e1 _ e2 - => (if pol then or_cnf_opt else and_cnf_opt) (xcnf (negb pol) e1) (xcnf pol e2) + | TT _ => if polarity then (cnf_tt,nil) else (cnf_ff,nil) + | FF _ => if polarity then (cnf_ff,nil) else (cnf_tt,nil) + | X b p => if polarity then (cnf_ff,nil) else (cnf_ff,nil) + | A _ x t => ratom (if polarity then normalise x t else negate x t) t + | NOT e => rxcnf (negb polarity) e + | AND e1 e2 => rxcnf_and rxcnf polarity e1 e2 + | OR e1 e2 => rxcnf_or rxcnf polarity e1 e2 + | IMPL e1 a e2 => rxcnf_impl rxcnf polarity e1 e2 + | IFF e1 e2 => rxcnf_iff rxcnf polarity e1 e2 + | EQ e1 e2 => rxcnf_iff rxcnf polarity e1 e2 end. - Section CNFAnnot. - - (** Records annotations used to optimise the cnf. - Those need to be kept when pruning the formula. - For efficiency, this is a separate function. - *) - - Fixpoint radd_term (t : Term' * Annot) (cl : clause) : clause + list Annot := - match cl with - | nil => (* if t is unsat, the clause is empty BUT t is needed. *) - match deduce (fst t) (fst t) with - | Some u => if unsat u then inr ((snd t)::nil) else inl (t::nil) - | None => inl (t::nil) - end - | t'::cl => (* if t /\ t' is unsat, the clause is empty BUT t & t' are needed *) - match deduce (fst t) (fst t') with - | Some u => if unsat u then inr ((snd t)::(snd t')::nil) - else match radd_term t cl with - | inl cl' => inl (t'::cl') - | inr l => inr l - end - | None => match radd_term t cl with - | inl cl' => inl (t'::cl') - | inr l => inr l - end - end - end. + Section Abstraction. + Variable TX : kind -> Type. + Variable AF : Type. - Fixpoint ror_clause cl1 cl2 := - match cl1 with - | nil => inl cl2 - | t::cl => match radd_term t cl2 with - | inl cl' => ror_clause cl cl' - | inr l => inr l - end - end. + Class to_constrT : Type := + { + mkTT : forall (k: kind), TX k; + mkFF : forall (k: kind), TX k; + mkA : forall (k: kind), Term -> Annot -> TX k; + mkAND : forall (k: kind), TX k -> TX k -> TX k; + mkOR : forall (k: kind), TX k -> TX k -> TX k; + mkIMPL : forall (k: kind), TX k -> TX k -> TX k; + mkIFF : forall (k: kind), TX k -> TX k -> TX k; + mkNOT : forall (k: kind), TX k -> TX k; + mkEQ : TX isBool -> TX isBool -> TX isProp - Definition xror_clause_cnf t f := - List.fold_left (fun '(acc,tg) e => - match ror_clause t e with - | inl cl => (cl :: acc,tg) - | inr l => (acc,tg+++l) - end) f (nil,nil). - - Definition ror_clause_cnf t f := - match t with - | nil => (f,nil) - | _ => xror_clause_cnf t f - end. + }. + Context {to_constr : to_constrT}. - Fixpoint ror_cnf (f f':list clause) := + Fixpoint aformula (k: kind) (f : TFormula TX AF k) : TX k := match f with - | nil => (cnf_tt,nil) - | e :: rst => - let (rst_f',t) := ror_cnf rst f' in - let (e_f', t') := ror_clause_cnf e f' in - (rst_f' +++ e_f', t +++ t') + | TT b => mkTT b + | FF b => mkFF b + | X b p => p + | A b x t => mkA b x t + | AND f1 f2 => mkAND (aformula f1) (aformula f2) + | OR f1 f2 => mkOR (aformula f1) (aformula f2) + | IMPL f1 o f2 => mkIMPL (aformula f1) (aformula f2) + | IFF f1 f2 => mkIFF (aformula f1) (aformula f2) + | NOT f => mkNOT (aformula f) + | EQ f1 f2 => mkEQ (aformula f1) (aformula f2) end. - Definition annot_of_clause (l : clause) : list Annot := - List.map snd l. - - Definition annot_of_cnf (f : cnf) : list Annot := - List.fold_left (fun acc e => annot_of_clause e +++ acc ) f nil. + Definition is_X (k: kind) (f : TFormula TX AF k) : option (TX k) := + match f with + | X _ p => Some p + | _ => None + end. - Definition ror_cnf_opt f1 f2 := - if is_cnf_tt f1 - then (cnf_tt , nil) - else if is_cnf_tt f2 - then (cnf_tt, nil) - else if is_cnf_ff f2 - then (f1,nil) - else ror_cnf f1 f2. + Definition is_X_inv : forall (k: kind) (f: TFormula TX AF k) x, + is_X f = Some x -> f = X k x. + Proof. + destruct f ; simpl ; try congruence. + Qed. + Variable needA : Annot -> bool. - Definition ocons {A : Type} (o : option A) (l : list A) : list A := - match o with - | None => l - | Some e => e ::l + Definition abs_and (k: kind) (f1 f2 : TFormula TX AF k) + (c : forall (k: kind), TFormula TX AF k -> TFormula TX AF k -> TFormula TX AF k) := + match is_X f1 , is_X f2 with + | Some _ , _ | _ , Some _ => X k (aformula (c k f1 f2)) + | _ , _ => c k f1 f2 end. - Definition ratom (c : cnf) (a : Annot) : cnf * list Annot := - if is_cnf_ff c || is_cnf_tt c - then (c,a::nil) - else (c,nil). (* t is embedded in c *) - - Fixpoint rxcnf {TX AF: Type}(polarity : bool) (f : TFormula TX AF) : cnf * list Annot := - match f with - | TT => if polarity then (cnf_tt,nil) else (cnf_ff,nil) - | FF => if polarity then (cnf_ff,nil) else (cnf_tt,nil) - | X p => if polarity then (cnf_ff,nil) else (cnf_ff,nil) - | A x t => ratom (if polarity then normalise x t else negate x t) t - | N e => rxcnf (negb polarity) e - | Cj e1 e2 => - let '(e1,t1) := rxcnf polarity e1 in - let '(e2,t2) := rxcnf polarity e2 in - if polarity - then (and_cnf_opt e1 e2, t1 +++ t2) - else let (f',t') := ror_cnf_opt e1 e2 in - (f', t1 +++ t2 +++ t') - | D e1 e2 => - let '(e1,t1) := rxcnf polarity e1 in - let '(e2,t2) := rxcnf polarity e2 in - if polarity - then let (f',t') := ror_cnf_opt e1 e2 in - (f', t1 +++ t2 +++ t') - else (and_cnf_opt e1 e2, t1 +++ t2) - | I e1 a e2 => - let '(e1 , t1) := (rxcnf (negb polarity) e1) in - if polarity - then - if is_cnf_ff e1 - then - rxcnf polarity e2 - else (* compute disjunction *) - let '(e2 , t2) := (rxcnf polarity e2) in - let (f',t') := ror_cnf_opt e1 e2 in - (f', t1 +++ t2 +++ t') (* record the hypothesis *) - else - let '(e2 , t2) := (rxcnf polarity e2) in - (and_cnf_opt e1 e2, t1 +++ t2) + Definition abs_or (k: kind) (f1 f2 : TFormula TX AF k) + (c : forall (k: kind), TFormula TX AF k -> TFormula TX AF k -> TFormula TX AF k) := + match is_X f1 , is_X f2 with + | Some _ , Some _ => X k (aformula (c k f1 f2)) + | _ , _ => c k f1 f2 end. + Definition abs_not (k: kind) (f1 : TFormula TX AF k) + (c : forall (k: kind), TFormula TX AF k -> TFormula TX AF k) := + match is_X f1 with + | Some _ => X k (aformula (c k f1 )) + | _ => c k f1 + end. - Section Abstraction. - Variable TX : Type. - Variable AF : Type. - - Class to_constrT : Type := - { - mkTT : TX; - mkFF : TX; - mkA : Term -> Annot -> TX; - mkCj : TX -> TX -> TX; - mkD : TX -> TX -> TX; - mkI : TX -> TX -> TX; - mkN : TX -> TX - }. - - Context {to_constr : to_constrT}. - - Fixpoint aformula (f : TFormula TX AF) : TX := - match f with - | TT => mkTT - | FF => mkFF - | X p => p - | A x t => mkA x t - | Cj f1 f2 => mkCj (aformula f1) (aformula f2) - | D f1 f2 => mkD (aformula f1) (aformula f2) - | I f1 o f2 => mkI (aformula f1) (aformula f2) - | N f => mkN (aformula f) - end. + Definition mk_arrow (o : option AF) (k: kind) (f1 f2: TFormula TX AF k) := + match o with + | None => IMPL f1 None f2 + | Some _ => if is_X f1 then f2 else IMPL f1 o f2 + end. - Definition is_X (f : TFormula TX AF) : option TX := - match f with - | X p => Some p - | _ => None - end. + Fixpoint abst_simpl (k: kind) (f : TFormula TX AF k) : TFormula TX AF k:= + match f with + | TT k => TT k + | FF k => FF k + | X k p => X k p + | A k x t => if needA t then A k x t else X k (mkA k x t) + | AND f1 f2 => AND (abst_simpl f1) (abst_simpl f2) + | OR f1 f2 => OR (abst_simpl f1) (abst_simpl f2) + | IMPL f1 o f2 => IMPL (abst_simpl f1) o (abst_simpl f2) + | NOT f => NOT (abst_simpl f) + | IFF f1 f2 => IFF (abst_simpl f1) (abst_simpl f2) + | EQ f1 f2 => EQ (abst_simpl f1) (abst_simpl f2) + end. - Definition is_X_inv : forall f x, - is_X f = Some x -> f = X x. - Proof. - destruct f ; simpl ; congruence. - Qed. + Section REC. + Variable REC : forall (pol : bool) (k: kind) (f : TFormula TX AF k), TFormula TX AF k. + Definition abst_and (pol : bool) (k: kind) (f1 f2:TFormula TX AF k) : TFormula TX AF k:= + (if pol then abs_and else abs_or) k (REC pol f1) (REC pol f2) AND. - Variable needA : Annot -> bool. + Definition abst_or (pol : bool) (k: kind) (f1 f2:TFormula TX AF k) : TFormula TX AF k:= + (if pol then abs_or else abs_and) k (REC pol f1) (REC pol f2) OR. - Definition abs_and (f1 f2 : TFormula TX AF) - (c : TFormula TX AF -> TFormula TX AF -> TFormula TX AF) := - match is_X f1 , is_X f2 with - | Some _ , _ | _ , Some _ => X (aformula (c f1 f2)) - | _ , _ => c f1 f2 - end. + Definition abst_impl (pol : bool) (o :option AF) (k: kind) (f1 f2:TFormula TX AF k) : TFormula TX AF k:= + (if pol then abs_or else abs_and) k (REC (negb pol) f1) (REC pol f2) (mk_arrow o). - Definition abs_or (f1 f2 : TFormula TX AF) - (c : TFormula TX AF -> TFormula TX AF -> TFormula TX AF) := + Definition or_is_X (k: kind) (f1 f2: TFormula TX AF k) : bool := match is_X f1 , is_X f2 with - | Some _ , Some _ => X (aformula (c f1 f2)) - | _ , _ => c f1 f2 + | Some _ , _ + | _ , Some _ => true + | _ , _ => false end. - Definition mk_arrow (o : option AF) (f1 f2: TFormula TX AF) := - match o with - | None => I f1 None f2 - | Some _ => if is_X f1 then f2 else I f1 o f2 - end. + Definition abs_iff (k: kind) (nf1 ff2 f1 tf2 : TFormula TX AF k) (r: kind) (def : TFormula TX AF r) : TFormula TX AF r := + if andb (or_is_X nf1 ff2) (or_is_X f1 tf2) + then X r (aformula def) + else def. - Fixpoint abst_form (pol : bool) (f : TFormula TX AF) := - match f with - | TT => if pol then TT else X mkTT - | FF => if pol then X mkFF else FF - | X p => X p - | A x t => if needA t then A x t else X (mkA x t) - | Cj f1 f2 => - let f1 := abst_form pol f1 in - let f2 := abst_form pol f2 in - if pol then abs_and f1 f2 Cj - else abs_or f1 f2 Cj - | D f1 f2 => - let f1 := abst_form pol f1 in - let f2 := abst_form pol f2 in - if pol then abs_or f1 f2 D - else abs_and f1 f2 D - | I f1 o f2 => - let f1 := abst_form (negb pol) f1 in - let f2 := abst_form pol f2 in - if pol - then abs_or f1 f2 (mk_arrow o) - else abs_and f1 f2 (mk_arrow o) - | N f => let f := abst_form (negb pol) f in - match is_X f with - | Some a => X (mkN a) - | _ => N f - end - end. + Definition abst_iff (pol : bool) (k: kind) (f1 f2: TFormula TX AF k) : TFormula TX AF k := + abs_iff (REC (negb pol) f1) (REC false f2) (REC pol f1) (REC true f2) (IFF (abst_simpl f1) (abst_simpl f2)). + Definition abst_eq (pol : bool) (f1 f2: TFormula TX AF isBool) : TFormula TX AF isProp := + abs_iff (REC (negb pol) f1) (REC false f2) (REC pol f1) (REC true f2) (EQ (abst_simpl f1) (abst_simpl f2)). + End REC. + Fixpoint abst_form (pol : bool) (k: kind) (f : TFormula TX AF k) : TFormula TX AF k:= + match f with + | TT k => if pol then TT k else X k (mkTT k) + | FF k => if pol then X k (mkFF k) else FF k + | X k p => X k p + | A k x t => if needA t then A k x t else X k (mkA k x t) + | AND f1 f2 => abst_and abst_form pol f1 f2 + | OR f1 f2 => abst_or abst_form pol f1 f2 + | IMPL f1 o f2 => abst_impl abst_form pol o f1 f2 + | NOT f => abs_not (abst_form (negb pol) f) NOT + | IFF f1 f2 => abst_iff abst_form pol f1 f2 + | EQ f1 f2 => abst_eq abst_form pol f1 f2 + end. - Lemma if_same : forall {A: Type} (b:bool) (t:A), - (if b then t else t) = t. - Proof. - destruct b ; reflexivity. - Qed. + Lemma if_same : forall {A: Type} (b: bool) (t:A), + (if b then t else t) = t. + Proof. + destruct b ; reflexivity. + Qed. - Lemma is_cnf_tt_cnf_ff : - is_cnf_tt cnf_ff = false. - Proof. - reflexivity. - Qed. + Lemma is_cnf_tt_cnf_ff : + is_cnf_tt cnf_ff = false. + Proof. + reflexivity. + Qed. - Lemma is_cnf_ff_cnf_ff : - is_cnf_ff cnf_ff = true. - Proof. - reflexivity. - Qed. + Lemma is_cnf_ff_cnf_ff : + is_cnf_ff cnf_ff = true. + Proof. + reflexivity. + Qed. Lemma is_cnf_tt_inv : forall f1, @@ -587,9 +844,9 @@ Section S. reflexivity. Qed. - Lemma abs_and_pol : forall f1 f2 pol, + Lemma abs_and_pol : forall (k: kind) (f1 f2: TFormula TX AF k) pol, and_cnf_opt (xcnf pol f1) (xcnf pol f2) = - xcnf pol (abs_and f1 f2 (if pol then Cj else D)). + xcnf pol (abs_and f1 f2 (if pol then AND else OR)). Proof. unfold abs_and; intros. destruct (is_X f1) eqn:EQ1. @@ -607,9 +864,9 @@ Section S. destruct pol ; simpl; auto. Qed. - Lemma abs_or_pol : forall f1 f2 pol, + Lemma abs_or_pol : forall (k: kind) (f1 f2:TFormula TX AF k) pol, or_cnf_opt (xcnf pol f1) (xcnf pol f2) = - xcnf pol (abs_or f1 f2 (if pol then D else Cj)). + xcnf pol (abs_or f1 f2 (if pol then OR else AND)). Proof. unfold abs_or; intros. destruct (is_X f1) eqn:EQ1. @@ -629,8 +886,8 @@ Section S. Variable needA_all : forall a, needA a = true. - Lemma xcnf_true_mk_arrow_l : forall o t f, - xcnf true (mk_arrow o (X t) f) = xcnf true f. + Lemma xcnf_true_mk_arrow_l : forall b o t (f:TFormula TX AF b), + xcnf true (mk_arrow o (X b t) f) = xcnf true f. Proof. destruct o ; simpl; auto. intros. rewrite or_cnf_opt_cnf_ff. reflexivity. @@ -647,8 +904,8 @@ Section S. apply if_cnf_tt. Qed. - Lemma xcnf_true_mk_arrow_r : forall o t f, - xcnf true (mk_arrow o f (X t)) = xcnf false f. + Lemma xcnf_true_mk_arrow_r : forall b o t (f:TFormula TX AF b), + xcnf true (mk_arrow o f (X b t)) = xcnf false f. Proof. destruct o ; simpl; auto. - intros. @@ -660,9 +917,167 @@ Section S. apply or_cnf_opt_cnf_ff_r. Qed. + Lemma and_cnf_opt_cnf_ff_r : forall f, + and_cnf_opt f cnf_ff = cnf_ff. + Proof. + intros. + unfold and_cnf_opt. + rewrite is_cnf_ff_cnf_ff. + rewrite orb_comm. reflexivity. + Qed. + + Lemma and_cnf_opt_cnf_ff : forall f, + and_cnf_opt cnf_ff f = cnf_ff. + Proof. + intros. + unfold and_cnf_opt. + rewrite is_cnf_ff_cnf_ff. + reflexivity. + Qed. + + + Lemma and_cnf_opt_cnf_tt : forall f, + and_cnf_opt f cnf_tt = f. + Proof. + intros. + unfold and_cnf_opt. + simpl. rewrite orb_comm. + simpl. + destruct (is_cnf_ff f) eqn:EQ ; auto. + apply is_cnf_ff_inv in EQ. + auto. + Qed. + + Lemma is_bool_abst_simpl : forall b (f:TFormula TX AF b), + is_bool (abst_simpl f) = is_bool f. + Proof. + induction f ; simpl ; auto. + rewrite needA_all. + reflexivity. + Qed. + + Lemma abst_simpl_correct : forall b (f:TFormula TX AF b) pol, + xcnf pol f = xcnf pol (abst_simpl f). + Proof. + induction f; simpl;intros; + unfold mk_and,mk_or,mk_impl, mk_iff; + rewrite <- ?IHf; + try (rewrite <- !IHf1; rewrite <- !IHf2); + try reflexivity. + - rewrite needA_all. + reflexivity. + - rewrite is_bool_abst_simpl. + destruct (is_bool f2); auto. + - rewrite is_bool_abst_simpl. + destruct (is_bool f2); auto. + Qed. + + Ltac is_X := + match goal with + | |-context[is_X ?X] => + let f := fresh "EQ" in + destruct (is_X X) eqn:f ; + [apply is_X_inv in f|] + end. + + Ltac cnf_simpl := + repeat match goal with + | |- context[and_cnf_opt cnf_ff _ ] => rewrite and_cnf_opt_cnf_ff + | |- context[and_cnf_opt _ cnf_ff] => rewrite and_cnf_opt_cnf_ff_r + | |- context[and_cnf_opt _ cnf_tt] => rewrite and_cnf_opt_cnf_tt + | |- context[or_cnf_opt cnf_ff _] => rewrite or_cnf_opt_cnf_ff + | |- context[or_cnf_opt _ cnf_ff] => rewrite or_cnf_opt_cnf_ff_r + end. + + Lemma or_is_X_inv : forall (k: kind) (f1 f2 : TFormula TX AF k), + or_is_X f1 f2 = true -> + exists k1, is_X f1 = Some k1 \/ is_X f2 = Some k1. + Proof. + unfold or_is_X. + intros k f1 f2. + repeat is_X. + exists t ; intuition. + exists t ; intuition. + exists t ; intuition. + congruence. + Qed. + + Lemma mk_iff_is_bool : forall (k: kind) (f1 f2:TFormula TX AF k) pol, + match is_bool f2 with + | Some isb => xcnf (if isb then pol else negb pol) f1 + | None => mk_iff xcnf pol f1 f2 + end = mk_iff xcnf pol f1 f2. + Proof. + intros. + destruct (is_bool f2) eqn:EQ; auto. + apply is_bool_inv in EQ. + subst. + unfold mk_iff. + destruct b ; simpl; cnf_simpl; reflexivity. + Qed. + + Lemma abst_iff_correct : forall + (k: kind) + (f1 f2 : GFormula k) + (IHf1 : forall pol : bool, xcnf pol f1 = xcnf pol (abst_form pol f1)) + (IHf2 : forall pol : bool, xcnf pol f2 = xcnf pol (abst_form pol f2)) + (pol : bool), + xcnf pol (IFF f1 f2) = xcnf pol (abst_iff abst_form pol f1 f2). + Proof. + intros; simpl. + assert (D1 :mk_iff xcnf pol f1 f2 = mk_iff xcnf pol (abst_simpl f1) (abst_simpl f2)). + { + simpl. + unfold mk_iff. + rewrite <- !abst_simpl_correct. + reflexivity. + } + rewrite mk_iff_is_bool. + unfold abst_iff,abs_iff. + destruct ( or_is_X (abst_form (negb pol) f1) (abst_form false f2) && + or_is_X (abst_form pol f1) (abst_form true f2) + ) eqn:EQ1. + + simpl. + rewrite andb_true_iff in EQ1. + destruct EQ1 as (EQ1 & EQ2). + apply or_is_X_inv in EQ1. + apply or_is_X_inv in EQ2. + destruct EQ1 as (b1 & EQ1). + destruct EQ2 as (b2 & EQ2). + rewrite if_same. + unfold mk_iff. + rewrite !IHf1. + rewrite !IHf2. + destruct EQ1 as [EQ1 | EQ1] ; apply is_X_inv in EQ1; + destruct EQ2 as [EQ2 | EQ2] ; apply is_X_inv in EQ2; + rewrite EQ1; rewrite EQ2; simpl; + repeat rewrite if_same ; cnf_simpl; auto. + + simpl. + rewrite mk_iff_is_bool. + unfold mk_iff. + rewrite <- ! abst_simpl_correct. + reflexivity. + Qed. + + Lemma abst_eq_correct : forall + (f1 f2 : GFormula isBool) + (IHf1 : forall pol : bool, xcnf pol f1 = xcnf pol (abst_form pol f1)) + (IHf2 : forall pol : bool, xcnf pol f2 = xcnf pol (abst_form pol f2)) + (pol : bool), + xcnf pol (EQ f1 f2) = xcnf pol (abst_form pol (EQ f1 f2)). + Proof. + intros. + change (xcnf pol (IFF f1 f2) = xcnf pol (abst_form pol (EQ f1 f2))). + rewrite abst_iff_correct by assumption. + simpl. unfold abst_iff, abst_eq. + unfold abs_iff. + destruct (or_is_X (abst_form (negb pol) f1) (abst_form false f2) && + or_is_X (abst_form pol f1) (abst_form true f2) + ) ; auto. + Qed. - Lemma abst_form_correct : forall f pol, + Lemma abst_form_correct : forall b (f:TFormula TX AF b) pol, xcnf pol f = xcnf pol (abst_form pol f). Proof. induction f;intros. @@ -671,27 +1086,24 @@ Section S. - simpl. reflexivity. - simpl. rewrite needA_all. reflexivity. - - simpl. + - simpl. unfold mk_and. specialize (IHf1 pol). specialize (IHf2 pol). rewrite IHf1. rewrite IHf2. destruct pol. - + - apply abs_and_pol; auto. - + - apply abs_or_pol; auto. - - simpl. + + apply abs_and_pol; auto. + + apply abs_or_pol. + - simpl. unfold mk_or. specialize (IHf1 pol). specialize (IHf2 pol). rewrite IHf1. rewrite IHf2. destruct pol. - + - apply abs_or_pol; auto. - + - apply abs_and_pol; auto. + + apply abs_or_pol; auto. + + apply abs_and_pol; auto. - simpl. + unfold abs_not. specialize (IHf (negb pol)). destruct (is_X (abst_form (negb pol) f)) eqn:EQ1. + apply is_X_inv in EQ1. @@ -699,381 +1111,438 @@ Section S. simpl in *. destruct pol ; auto. + simpl. congruence. - - simpl. + - simpl. unfold mk_impl. specialize (IHf1 (negb pol)). specialize (IHf2 pol). destruct pol. - + - simpl in *. - unfold abs_or. - destruct (is_X (abst_form false f1)) eqn:EQ1; - destruct (is_X (abst_form true f2)) eqn:EQ2 ; simpl. - * apply is_X_inv in EQ1. - apply is_X_inv in EQ2. - rewrite EQ1 in *. - rewrite EQ2 in *. - rewrite IHf1. rewrite IHf2. - simpl. reflexivity. - * apply is_X_inv in EQ1. - rewrite EQ1 in *. - rewrite IHf1. - simpl. - rewrite xcnf_true_mk_arrow_l. - rewrite or_cnf_opt_cnf_ff. - congruence. - * apply is_X_inv in EQ2. - rewrite EQ2 in *. - rewrite IHf2. - simpl. - rewrite xcnf_true_mk_arrow_r. - rewrite or_cnf_opt_cnf_ff_r. - congruence. - * destruct o ; simpl ; try congruence. - rewrite EQ1. - simpl. congruence. - + simpl in *. - unfold abs_and. - destruct (is_X (abst_form true f1)) eqn:EQ1; - destruct (is_X (abst_form false f2)) eqn:EQ2 ; simpl. - * apply is_X_inv in EQ1. + + + simpl in *. + unfold abs_or. + destruct (is_X (abst_form false f1)) eqn:EQ1; + destruct (is_X (abst_form true f2)) eqn:EQ2 ; simpl. + * apply is_X_inv in EQ1. + apply is_X_inv in EQ2. + rewrite EQ1 in *. + rewrite EQ2 in *. + rewrite IHf1. rewrite IHf2. + simpl. reflexivity. + * apply is_X_inv in EQ1. + rewrite EQ1 in *. + rewrite IHf1. + simpl. + rewrite xcnf_true_mk_arrow_l. + rewrite or_cnf_opt_cnf_ff. + congruence. + * apply is_X_inv in EQ2. + rewrite EQ2 in *. + rewrite IHf2. + simpl. + rewrite xcnf_true_mk_arrow_r. + rewrite or_cnf_opt_cnf_ff_r. + congruence. + * destruct o ; simpl ; try congruence. + rewrite EQ1. + simpl. congruence. + + simpl in *. + unfold abs_and. + destruct (is_X (abst_form true f1)) eqn:EQ1; + destruct (is_X (abst_form false f2)) eqn:EQ2 ; simpl. + * apply is_X_inv in EQ1. apply is_X_inv in EQ2. rewrite EQ1 in *. rewrite EQ2 in *. rewrite IHf1. rewrite IHf2. simpl. reflexivity. - * apply is_X_inv in EQ1. + * apply is_X_inv in EQ1. rewrite EQ1 in *. rewrite IHf1. simpl. reflexivity. - * apply is_X_inv in EQ2. + * apply is_X_inv in EQ2. rewrite EQ2 in *. rewrite IHf2. simpl. unfold and_cnf_opt. rewrite orb_comm. reflexivity. - * destruct o; simpl. - rewrite EQ1. simpl. - congruence. - congruence. - Qed. - - End Abstraction. - - - End CNFAnnot. - - - Lemma radd_term_term : forall a' a cl, radd_term a a' = inl cl -> add_term a a' = Some cl. - Proof. - induction a' ; simpl. - - intros. - destruct (deduce (fst a) (fst a)). - destruct (unsat t). congruence. - inversion H. reflexivity. - inversion H ;reflexivity. - - intros. - destruct (deduce (fst a0) (fst a)). - destruct (unsat t). congruence. - destruct (radd_term a0 a') eqn:RADD; try congruence. - inversion H. subst. - apply IHa' in RADD. - rewrite RADD. - reflexivity. - destruct (radd_term a0 a') eqn:RADD; try congruence. - inversion H. subst. - apply IHa' in RADD. - rewrite RADD. - reflexivity. - Qed. - - Lemma radd_term_term' : forall a' a cl, add_term a a' = Some cl -> radd_term a a' = inl cl. - Proof. - induction a' ; simpl. - - intros. - destruct (deduce (fst a) (fst a)). - destruct (unsat t). congruence. - inversion H. reflexivity. - inversion H ;reflexivity. - - intros. - destruct (deduce (fst a0) (fst a)). - destruct (unsat t). congruence. - destruct (add_term a0 a') eqn:RADD; try congruence. - inversion H. subst. - apply IHa' in RADD. - rewrite RADD. - reflexivity. - destruct (add_term a0 a') eqn:RADD; try congruence. - inversion H. subst. - apply IHa' in RADD. - rewrite RADD. - reflexivity. + * destruct o; simpl. + rewrite EQ1. simpl. + congruence. + congruence. + - apply abst_iff_correct; auto. + - apply abst_eq_correct; auto. Qed. - Lemma xror_clause_clause : forall a f, - fst (xror_clause_cnf a f) = xor_clause_cnf a f. - Proof. - unfold xror_clause_cnf. - unfold xor_clause_cnf. - assert (ACC: fst (@nil clause,@nil Annot) = nil). - reflexivity. - intros. - set (F1:= (fun '(acc, tg) (e : clause) => - match ror_clause a e with - | inl cl => (cl :: acc, tg) - | inr l => (acc, tg +++ l) - end)). - set (F2:= (fun (acc : list clause) (e : clause) => - match or_clause a e with - | Some cl => cl :: acc - | None => acc - end)). - revert ACC. - generalize (@nil clause,@nil Annot). - generalize (@nil clause). - induction f ; simpl ; auto. - intros. - apply IHf. - unfold F1 , F2. - destruct p ; simpl in * ; subst. - clear. - revert a0. - induction a; simpl; auto. - intros. - destruct (radd_term a a1) eqn:RADD. - apply radd_term_term in RADD. - rewrite RADD. - auto. - destruct (add_term a a1) eqn:RADD'. - apply radd_term_term' in RADD'. - congruence. - reflexivity. - Qed. + End Abstraction. - Lemma ror_clause_clause : forall a f, - fst (ror_clause_cnf a f) = or_clause_cnf a f. - Proof. - unfold ror_clause_cnf,or_clause_cnf. - destruct a ; auto. - apply xror_clause_clause. - Qed. - Lemma ror_cnf_cnf : forall f1 f2, fst (ror_cnf f1 f2) = or_cnf f1 f2. - Proof. - induction f1 ; simpl ; auto. - intros. - specialize (IHf1 f2). - destruct(ror_cnf f1 f2). - rewrite <- ror_clause_clause. - destruct(ror_clause_cnf a f2). - simpl. - rewrite <- IHf1. - reflexivity. - Qed. + End CNFAnnot. - Lemma ror_opt_cnf_cnf : forall f1 f2, fst (ror_cnf_opt f1 f2) = or_cnf_opt f1 f2. - Proof. - unfold ror_cnf_opt, or_cnf_opt. - intros. - destruct (is_cnf_tt f1). - - simpl ; auto. - - simpl. destruct (is_cnf_tt f2) ; simpl ; auto. - destruct (is_cnf_ff f2) eqn:EQ. - reflexivity. - apply ror_cnf_cnf. - Qed. - Lemma ratom_cnf : forall f a, - fst (ratom f a) = f. - Proof. - unfold ratom. - intros. - destruct (is_cnf_ff f || is_cnf_tt f); auto. - Qed. - - - - Lemma rxcnf_xcnf : forall {TX AF:Type} (f:TFormula TX AF) b, - fst (rxcnf b f) = xcnf b f. - Proof. - induction f ; simpl ; auto. - - destruct b; simpl ; auto. - - destruct b; simpl ; auto. - - destruct b ; simpl ; auto. - - intros. rewrite ratom_cnf. reflexivity. - - intros. - specialize (IHf1 b). - specialize (IHf2 b). - destruct (rxcnf b f1). - destruct (rxcnf b f2). - simpl in *. - subst. destruct b ; auto. - rewrite <- ror_opt_cnf_cnf. - destruct (ror_cnf_opt (xcnf false f1) (xcnf false f2)). - reflexivity. - - intros. - specialize (IHf1 b). - specialize (IHf2 b). - rewrite <- IHf1. - rewrite <- IHf2. - destruct (rxcnf b f1). - destruct (rxcnf b f2). - simpl in *. - subst. destruct b ; auto. - rewrite <- ror_opt_cnf_cnf. - destruct (ror_cnf_opt (xcnf true f1) (xcnf true f2)). - reflexivity. - - intros. - specialize (IHf1 (negb b)). - specialize (IHf2 b). - rewrite <- IHf1. - rewrite <- IHf2. - destruct (rxcnf (negb b) f1). - destruct (rxcnf b f2). - simpl in *. - subst. - destruct b;auto. - generalize (is_cnf_ff_inv (xcnf (negb true) f1)). - destruct (is_cnf_ff (xcnf (negb true) f1)). - + intros. - rewrite H by auto. - unfold or_cnf_opt. - simpl. - destruct (is_cnf_tt (xcnf true f2)) eqn:EQ;auto. - apply is_cnf_tt_inv in EQ; auto. - destruct (is_cnf_ff (xcnf true f2)) eqn:EQ1. - apply is_cnf_ff_inv in EQ1. congruence. - reflexivity. - + - rewrite <- ror_opt_cnf_cnf. - destruct (ror_cnf_opt (xcnf (negb true) f1) (xcnf true f2)). - intros. - reflexivity. - Qed. + Lemma radd_term_term : forall a' a cl, radd_term a a' = inl cl -> add_term a a' = Some cl. + Proof. + induction a' ; simpl. + - intros. + destruct (deduce (fst a) (fst a)). + destruct (unsat t). congruence. + inversion H. reflexivity. + inversion H ;reflexivity. + - intros. + destruct (deduce (fst a0) (fst a)). + destruct (unsat t). congruence. + destruct (radd_term a0 a') eqn:RADD; try congruence. + inversion H. subst. + apply IHa' in RADD. + rewrite RADD. + reflexivity. + destruct (radd_term a0 a') eqn:RADD; try congruence. + inversion H. subst. + apply IHa' in RADD. + rewrite RADD. + reflexivity. + Qed. + Lemma radd_term_term' : forall a' a cl, add_term a a' = Some cl -> radd_term a a' = inl cl. + Proof. + induction a' ; simpl. + - intros. + destruct (deduce (fst a) (fst a)). + destruct (unsat t). congruence. + inversion H. reflexivity. + inversion H ;reflexivity. + - intros. + destruct (deduce (fst a0) (fst a)). + destruct (unsat t). congruence. + destruct (add_term a0 a') eqn:RADD; try congruence. + inversion H. subst. + apply IHa' in RADD. + rewrite RADD. + reflexivity. + destruct (add_term a0 a') eqn:RADD; try congruence. + inversion H. subst. + apply IHa' in RADD. + rewrite RADD. + reflexivity. + Qed. - Variable eval' : Env -> Term' -> Prop. + Lemma xror_clause_clause : forall a f, + fst (xror_clause_cnf a f) = xor_clause_cnf a f. + Proof. + unfold xror_clause_cnf. + unfold xor_clause_cnf. + assert (ACC: fst (@nil clause,@nil Annot) = nil). + reflexivity. + intros. + set (F1:= (fun '(acc, tg) (e : clause) => + match ror_clause a e with + | inl cl => (cl :: acc, tg) + | inr l => (acc, tg +++ l) + end)). + set (F2:= (fun (acc : list clause) (e : clause) => + match or_clause a e with + | Some cl => cl :: acc + | None => acc + end)). + revert ACC. + generalize (@nil clause,@nil Annot). + generalize (@nil clause). + induction f ; simpl ; auto. + intros. + apply IHf. + unfold F1 , F2. + destruct p ; simpl in * ; subst. + clear. + revert a0. + induction a; simpl; auto. + intros. + destruct (radd_term a a1) eqn:RADD. + apply radd_term_term in RADD. + rewrite RADD. + auto. + destruct (add_term a a1) eqn:RADD'. + apply radd_term_term' in RADD'. + congruence. + reflexivity. + Qed. - Variable no_middle_eval' : forall env d, (eval' env d) \/ ~ (eval' env d). + Lemma ror_clause_clause : forall a f, + fst (ror_clause_cnf a f) = or_clause_cnf a f. + Proof. + unfold ror_clause_cnf,or_clause_cnf. + destruct a ; auto. + apply xror_clause_clause. + Qed. + Lemma ror_cnf_cnf : forall f1 f2, fst (ror_cnf f1 f2) = or_cnf f1 f2. + Proof. + induction f1 ; simpl ; auto. + intros. + specialize (IHf1 f2). + destruct(ror_cnf f1 f2). + rewrite <- ror_clause_clause. + destruct(ror_clause_cnf a f2). + simpl. + rewrite <- IHf1. + reflexivity. + Qed. - Variable unsat_prop : forall t, unsat t = true -> - forall env, eval' env t -> False. + Lemma ror_opt_cnf_cnf : forall f1 f2, fst (ror_cnf_opt f1 f2) = or_cnf_opt f1 f2. + Proof. + unfold ror_cnf_opt, or_cnf_opt. + intros. + destruct (is_cnf_tt f1). + - simpl ; auto. + - simpl. destruct (is_cnf_tt f2) ; simpl ; auto. + destruct (is_cnf_ff f2) eqn:EQ. + reflexivity. + apply ror_cnf_cnf. + Qed. + Lemma ratom_cnf : forall f a, + fst (ratom f a) = f. + Proof. + unfold ratom. + intros. + destruct (is_cnf_ff f || is_cnf_tt f); auto. + Qed. + Lemma rxcnf_and_xcnf : forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k) + (IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1) + (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2), + forall pol : bool, fst (rxcnf_and rxcnf pol f1 f2) = mk_and xcnf pol f1 f2. + Proof. + intros. + unfold mk_and, rxcnf_and. + specialize (IHf1 pol). + specialize (IHf2 pol). + destruct (rxcnf pol f1). + destruct (rxcnf pol f2). + simpl in *. + subst. destruct pol ; auto. + rewrite <- ror_opt_cnf_cnf. + destruct (ror_cnf_opt (xcnf false f1) (xcnf false f2)). + reflexivity. + Qed. - Variable deduce_prop : forall t t' u, - deduce t t' = Some u -> forall env, - eval' env t -> eval' env t' -> eval' env u. + Lemma rxcnf_or_xcnf : + forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k) + (IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1) + (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2), + forall pol : bool, fst (rxcnf_or rxcnf pol f1 f2) = mk_or xcnf pol f1 f2. + Proof. + intros. + unfold rxcnf_or, mk_or. + specialize (IHf1 pol). + specialize (IHf2 pol). + destruct (rxcnf pol f1). + destruct (rxcnf pol f2). + simpl in *. + subst. destruct pol ; auto. + rewrite <- ror_opt_cnf_cnf. + destruct (ror_cnf_opt (xcnf true f1) (xcnf true f2)). + reflexivity. + Qed. + Lemma rxcnf_impl_xcnf : + forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k) + (IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1) + (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2), + forall pol : bool, fst (rxcnf_impl rxcnf pol f1 f2) = mk_impl xcnf pol f1 f2. + Proof. + intros. + unfold rxcnf_impl, mk_impl, mk_or. + specialize (IHf1 (negb pol)). + specialize (IHf2 pol). + rewrite <- IHf1. + rewrite <- IHf2. + destruct (rxcnf (negb pol) f1). + destruct (rxcnf pol f2). + simpl in *. + subst. + destruct pol;auto. + generalize (is_cnf_ff_inv (xcnf (negb true) f1)). + destruct (is_cnf_ff (xcnf (negb true) f1)). + + intros. + rewrite H by auto. + unfold or_cnf_opt. + simpl. + destruct (is_cnf_tt (xcnf true f2)) eqn:EQ;auto. + apply is_cnf_tt_inv in EQ; auto. + destruct (is_cnf_ff (xcnf true f2)) eqn:EQ1. + apply is_cnf_ff_inv in EQ1. congruence. + reflexivity. + + + rewrite <- ror_opt_cnf_cnf. + destruct (ror_cnf_opt (xcnf (negb true) f1) (xcnf true f2)). + intros. + reflexivity. + Qed. - Definition eval_tt (env : Env) (tt : Term' * Annot) := eval' env (fst tt). - Definition eval_clause (env : Env) (cl : clause) := ~ make_conj (eval_tt env) cl. + Lemma rxcnf_iff_xcnf : + forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k) + (IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1) + (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2), + forall pol : bool, fst (rxcnf_iff rxcnf pol f1 f2) = mk_iff xcnf pol f1 f2. + Proof. + intros. + unfold rxcnf_iff. + unfold mk_iff. + rewrite <- (IHf1 (negb pol)). + rewrite <- (IHf1 pol). + rewrite <- (IHf2 false). + rewrite <- (IHf2 true). + destruct (rxcnf (negb pol) f1). + destruct (rxcnf false f2). + destruct (rxcnf pol f1). + destruct (rxcnf true f2). + destruct (ror_cnf_opt (and_cnf_opt c c0) (and_cnf_opt c1 c2)) eqn:EQ. + simpl. + change c3 with (fst (c3,l3)). + rewrite <- EQ. rewrite ror_opt_cnf_cnf. + reflexivity. + Qed. - Definition eval_cnf (env : Env) (f:cnf) := make_conj (eval_clause env) f. + Lemma rxcnf_xcnf : forall {TX : kind -> Type} {AF:Type} (k: kind) (f:TFormula TX AF k) pol, + fst (rxcnf pol f) = xcnf pol f. + Proof. + induction f ; simpl ; auto. + - destruct pol; simpl ; auto. + - destruct pol; simpl ; auto. + - destruct pol ; simpl ; auto. + - intros. rewrite ratom_cnf. reflexivity. + - apply rxcnf_and_xcnf; auto. + - apply rxcnf_or_xcnf; auto. + - apply rxcnf_impl_xcnf; auto. + - intros. + rewrite mk_iff_is_bool. + apply rxcnf_iff_xcnf; auto. + - intros. + rewrite mk_iff_is_bool. + apply rxcnf_iff_xcnf; auto. + Qed. - Lemma eval_cnf_app : forall env x y, eval_cnf env (x+++y) <-> eval_cnf env x /\ eval_cnf env y. - Proof. - unfold eval_cnf. - intros. - rewrite make_conj_rapp. - rewrite make_conj_app ; auto. - tauto. - Qed. + Variable eval' : Env -> Term' -> Prop. + Variable no_middle_eval' : forall env d, (eval' env d) \/ ~ (eval' env d). - Lemma eval_cnf_ff : forall env, eval_cnf env cnf_ff <-> False. - Proof. - unfold cnf_ff, eval_cnf,eval_clause. - simpl. tauto. - Qed. + Variable unsat_prop : forall t, unsat t = true -> + forall env, eval' env t -> False. - Lemma eval_cnf_tt : forall env, eval_cnf env cnf_tt <-> True. - Proof. - unfold cnf_tt, eval_cnf,eval_clause. - simpl. tauto. - Qed. + Variable deduce_prop : forall t t' u, + deduce t t' = Some u -> forall env, + eval' env t -> eval' env t' -> eval' env u. + Definition eval_tt (env : Env) (tt : Term' * Annot) := eval' env (fst tt). - Lemma eval_cnf_and_opt : forall env x y, eval_cnf env (and_cnf_opt x y) <-> eval_cnf env (and_cnf x y). - Proof. - unfold and_cnf_opt. - intros. - destruct (is_cnf_ff x) eqn:F1. - { apply is_cnf_ff_inv in F1. - simpl. subst. - unfold and_cnf. - rewrite eval_cnf_app. - rewrite eval_cnf_ff. - tauto. - } - simpl. - destruct (is_cnf_ff y) eqn:F2. - { apply is_cnf_ff_inv in F2. - simpl. subst. - unfold and_cnf. - rewrite eval_cnf_app. - rewrite eval_cnf_ff. - tauto. - } - tauto. - Qed. + Definition eval_clause (env : Env) (cl : clause) := ~ make_conj (eval_tt env) cl. + Definition eval_cnf (env : Env) (f:cnf) := make_conj (eval_clause env) f. + Lemma eval_cnf_app : forall env x y, eval_cnf env (x+++y) <-> eval_cnf env x /\ eval_cnf env y. + Proof. + unfold eval_cnf. + intros. + rewrite make_conj_rapp. + rewrite make_conj_app ; auto. + tauto. + Qed. - Definition eval_opt_clause (env : Env) (cl: option clause) := - match cl with - | None => True - | Some cl => eval_clause env cl - end. + Lemma eval_cnf_ff : forall env, eval_cnf env cnf_ff <-> False. + Proof. + unfold cnf_ff, eval_cnf,eval_clause. + simpl. tauto. + Qed. + Lemma eval_cnf_tt : forall env, eval_cnf env cnf_tt <-> True. + Proof. + unfold cnf_tt, eval_cnf,eval_clause. + simpl. tauto. + Qed. - Lemma add_term_correct : forall env t cl , eval_opt_clause env (add_term t cl) <-> eval_clause env (t::cl). + Lemma eval_cnf_and_opt : forall env x y, eval_cnf env (and_cnf_opt x y) <-> eval_cnf env (and_cnf x y). Proof. - induction cl. - - (* BC *) - simpl. - case_eq (deduce (fst t) (fst t)) ; try tauto. + unfold and_cnf_opt. intros. - generalize (@deduce_prop _ _ _ H env). - case_eq (unsat t0) ; try tauto. - { intros. - generalize (@unsat_prop _ H0 env). - unfold eval_clause. - rewrite make_conj_cons. - simpl; intros. + destruct (is_cnf_ff x) eqn:F1. + { apply is_cnf_ff_inv in F1. + simpl. subst. + unfold and_cnf. + rewrite eval_cnf_app. + rewrite eval_cnf_ff. tauto. } - - (* IC *) simpl. - case_eq (deduce (fst t) (fst a)); - intros. - generalize (@deduce_prop _ _ _ H env). - case_eq (unsat t0); intros. - { - generalize (@unsat_prop _ H0 env). - simpl. - unfold eval_clause. - repeat rewrite make_conj_cons. - tauto. - } - destruct (add_term t cl) ; simpl in * ; try tauto. - { - intros. - unfold eval_clause in *. - repeat rewrite make_conj_cons in *. + destruct (is_cnf_ff y) eqn:F2. + { apply is_cnf_ff_inv in F2. + simpl. subst. + unfold and_cnf. + rewrite eval_cnf_app. + rewrite eval_cnf_ff. tauto. } + destruct (is_cnf_tt y) eqn:F3. { - unfold eval_clause in *. - repeat rewrite make_conj_cons in *. + apply is_cnf_tt_inv in F3. + subst. + unfold and_cnf. + rewrite eval_cnf_app. + rewrite eval_cnf_tt. tauto. } - destruct (add_term t cl) ; simpl in *; - unfold eval_clause in * ; - repeat rewrite make_conj_cons in *; tauto. + tauto. + Qed. + + Definition eval_opt_clause (env : Env) (cl: option clause) := + match cl with + | None => True + | Some cl => eval_clause env cl + end. + + Lemma add_term_correct : forall env t cl , eval_opt_clause env (add_term t cl) <-> eval_clause env (t::cl). + Proof. + induction cl. + - (* BC *) + simpl. + case_eq (deduce (fst t) (fst t)) ; try tauto. + intros. + generalize (@deduce_prop _ _ _ H env). + case_eq (unsat t0) ; try tauto. + { intros. + generalize (@unsat_prop _ H0 env). + unfold eval_clause. + rewrite make_conj_cons. + simpl; intros. + tauto. + } + - (* IC *) + simpl. + case_eq (deduce (fst t) (fst a)); + intros. + generalize (@deduce_prop _ _ _ H env). + case_eq (unsat t0); intros. + { + generalize (@unsat_prop _ H0 env). + simpl. + unfold eval_clause. + repeat rewrite make_conj_cons. + tauto. + } + destruct (add_term t cl) ; simpl in * ; try tauto. + { + intros. + unfold eval_clause in *. + repeat rewrite make_conj_cons in *. + tauto. + } + { + unfold eval_clause in *. + repeat rewrite make_conj_cons in *. + tauto. + } + destruct (add_term t cl) ; simpl in *; + unfold eval_clause in * ; + repeat rewrite make_conj_cons in *; tauto. Qed. @@ -1096,10 +1565,10 @@ Section S. assert (eval_tt env a \/ ~ eval_tt env a) by (apply no_middle_eval'). destruct (add_term a cl'); simpl in *. + - rewrite IHcl. - unfold eval_clause in *. - rewrite !make_conj_cons in *. - tauto. + rewrite IHcl. + unfold eval_clause in *. + rewrite !make_conj_cons in *. + tauto. + unfold eval_clause in *. repeat rewrite make_conj_cons in *. tauto. @@ -1131,8 +1600,8 @@ Section S. generalize (or_clause_correct t a env). destruct (or_clause t a). + - rewrite make_conj_cons. - simpl. tauto. + rewrite make_conj_cons. + simpl. tauto. + simpl. tauto. } destruct t ; auto. @@ -1211,113 +1680,108 @@ Section S. } Qed. + Variable eval : Env -> forall (k: kind), Term -> rtyp k. - Variable eval : Env -> Term -> Prop. + Variable normalise_correct : forall env b t tg, eval_cnf env (normalise t tg) -> hold b (eval env b t). - Variable normalise_correct : forall env t tg, eval_cnf env (normalise t tg) -> eval env t. + Variable negate_correct : forall env b t tg, eval_cnf env (negate t tg) -> hold b (eNOT b (eval env b t)). - Variable negate_correct : forall env t tg, eval_cnf env (negate t tg) -> ~ eval env t. + Definition e_rtyp (k: kind) (x : rtyp k) : rtyp k := x. - Lemma xcnf_correct : forall (f : @GFormula Term Prop Annot unit) pol env, eval_cnf env (xcnf pol f) -> eval_f (fun x => x) (eval env) (if pol then f else N f). + Lemma hold_eTT : forall k, hold k (eTT k). Proof. - induction f. - - (* TT *) - unfold eval_cnf. - simpl. - destruct pol ; simpl ; auto. - - (* FF *) - unfold eval_cnf. - destruct pol; simpl ; auto. - unfold eval_clause ; simpl. - tauto. - - (* P *) - simpl. - destruct pol ; intros ;simpl. - unfold eval_cnf in H. - (* Here I have to drop the proposition *) - simpl in H. - unfold eval_clause in H ; simpl in H. - tauto. - (* Here, I could store P in the clause *) - unfold eval_cnf in H;simpl in H. - unfold eval_clause in H ; simpl in H. - tauto. - - (* A *) - simpl. - destruct pol ; simpl. - intros. - eapply normalise_correct ; eauto. - (* A 2 *) - intros. - eapply negate_correct ; eauto. - - (* Cj *) - destruct pol ; simpl. - + (* pol = true *) - intros. - rewrite eval_cnf_and_opt in H. - unfold and_cnf in H. - rewrite eval_cnf_app in H. - destruct H. - split. - apply (IHf1 _ _ H). - apply (IHf2 _ _ H0). - + (* pol = false *) - intros. - rewrite or_cnf_opt_correct in H. - rewrite or_cnf_correct in H. - destruct H as [H | H]. - generalize (IHf1 false env H). - simpl. - tauto. - generalize (IHf2 false env H). - simpl. - tauto. - - (* D *) - simpl. - destruct pol. - + (* pol = true *) - intros. - rewrite or_cnf_opt_correct in H. - rewrite or_cnf_correct in H. - destruct H as [H | H]. - generalize (IHf1 _ env H). - simpl. - tauto. - generalize (IHf2 _ env H). - simpl. - tauto. - + (* pol = true *) - intros. - rewrite eval_cnf_and_opt in H. - unfold and_cnf. - rewrite eval_cnf_app in H. - destruct H as [H0 H1]. - simpl. - generalize (IHf1 _ _ H0). - generalize (IHf2 _ _ H1). - simpl. - tauto. - - (**) - simpl. - destruct pol ; simpl. - intros. - apply (IHf false) ; auto. - intros. - generalize (IHf _ _ H). - tauto. - - (* I *) - simpl; intros. + destruct k ; simpl; auto. + Qed. + + Hint Resolve hold_eTT : tauto. + + Lemma hold_eFF : forall k, + hold k (eNOT k (eFF k)). + Proof. + destruct k ; simpl;auto. + Qed. + + Hint Resolve hold_eFF : tauto. + + Lemma hold_eAND : forall k r1 r2, + hold k (eAND k r1 r2) <-> (hold k r1 /\ hold k r2). + Proof. + destruct k ; simpl. + - intros. apply iff_refl. + - apply andb_true_iff. + Qed. + + Lemma hold_eOR : forall k r1 r2, + hold k (eOR k r1 r2) <-> (hold k r1 \/ hold k r2). + Proof. + destruct k ; simpl. + - intros. apply iff_refl. + - apply orb_true_iff. + Qed. + + Lemma hold_eNOT : forall k e, + hold k (eNOT k e) <-> not (hold k e). + Proof. + destruct k ; simpl. + - intros. apply iff_refl. + - intros. unfold is_true. + rewrite negb_true_iff. + destruct e ; intuition congruence. + Qed. + + Lemma hold_eIMPL : forall k e1 e2, + hold k (eIMPL k e1 e2) <-> (hold k e1 -> hold k e2). + Proof. + destruct k ; simpl. + - intros. apply iff_refl. + - intros. + unfold is_true. + destruct e1,e2 ; simpl ; intuition congruence. + Qed. + + Lemma hold_eIFF : forall k e1 e2, + hold k (eIFF k e1 e2) <-> (hold k e1 <-> hold k e2). + Proof. + destruct k ; simpl. + - intros. apply iff_refl. + - intros. + unfold is_true. + rewrite eqb_true_iff. + destruct e1,e2 ; simpl ; intuition congruence. + Qed. + + + + Lemma xcnf_impl : + forall + (k: kind) + (f1 : GFormula k) + (o : option unit) + (f2 : GFormula k) + (IHf1 : forall (pol : bool) (env : Env), + eval_cnf env (xcnf pol f1) -> + hold k (eval_f e_rtyp (eval env) (if pol then f1 else NOT f1))) + (IHf2 : forall (pol : bool) (env : Env), + eval_cnf env (xcnf pol f2) -> + hold k (eval_f e_rtyp (eval env) (if pol then f2 else NOT f2))), + forall (pol : bool) (env : Env), + eval_cnf env (xcnf pol (IMPL f1 o f2)) -> + hold k (eval_f e_rtyp (eval env) (if pol then IMPL f1 o f2 else NOT (IMPL f1 o f2))). + Proof. + simpl; intros. unfold mk_impl in H. destruct pol. + simpl. - intro. - rewrite or_cnf_opt_correct in H. - rewrite or_cnf_correct in H. - destruct H as [H | H]. - generalize (IHf1 _ _ H). - simpl in *. - tauto. - generalize (IHf2 _ _ H). - auto. + rewrite hold_eIMPL. + intro. + rewrite or_cnf_opt_correct in H. + rewrite or_cnf_correct in H. + destruct H as [H | H]. + generalize (IHf1 _ _ H). + simpl in *. + rewrite hold_eNOT. + tauto. + generalize (IHf2 _ _ H). + auto. + (* pol = false *) rewrite eval_cnf_and_opt in H. unfold and_cnf in H. @@ -1327,9 +1791,190 @@ Section S. generalize (IHf1 _ _ H0). generalize (IHf2 _ _ H1). simpl. + rewrite ! hold_eNOT. + rewrite ! hold_eIMPL. tauto. Qed. + Lemma hold_eIFF_IMPL : forall k e1 e2, + hold k (eIFF k e1 e2) <-> (hold k (eAND k (eIMPL k e1 e2) (eIMPL k e2 e1))). + Proof. + intros. + rewrite hold_eIFF. + rewrite hold_eAND. + rewrite! hold_eIMPL. + tauto. + Qed. + + Lemma hold_eEQ : forall e1 e2, + hold isBool (eIFF isBool e1 e2) <-> e1 = e2. + Proof. + simpl. + destruct e1,e2 ; simpl ; intuition congruence. + Qed. + + + Lemma xcnf_iff : forall + (k : kind) + (f1 f2 : @GFormula Term rtyp Annot unit k) + (IHf1 : forall (pol : bool) (env : Env), + eval_cnf env (xcnf pol f1) -> + hold k (eval_f e_rtyp (eval env) (if pol then f1 else NOT f1))) + (IHf2 : forall (pol : bool) (env : Env), + eval_cnf env (xcnf pol f2) -> + hold k (eval_f e_rtyp (eval env) (if pol then f2 else NOT f2))), + forall (pol : bool) (env : Env), + eval_cnf env (xcnf pol (IFF f1 f2)) -> + hold k (eval_f e_rtyp (eval env) (if pol then IFF f1 f2 else NOT (IFF f1 f2))). + Proof. + simpl. + intros. + rewrite mk_iff_is_bool in H. + unfold mk_iff in H. + destruct pol; + rewrite or_cnf_opt_correct in H; + rewrite or_cnf_correct in H; + rewrite! eval_cnf_and_opt in H; + unfold and_cnf in H; + rewrite! eval_cnf_app in H; + generalize (IHf1 false env); + generalize (IHf1 true env); + generalize (IHf2 false env); + generalize (IHf2 true env); + simpl. + - + rewrite hold_eIFF_IMPL. + rewrite hold_eAND. + rewrite! hold_eIMPL. + rewrite! hold_eNOT. + tauto. + - rewrite! hold_eNOT. + rewrite hold_eIFF_IMPL. + rewrite hold_eAND. + rewrite! hold_eIMPL. + tauto. + Qed. + + Lemma xcnf_correct : forall (k: kind) (f : @GFormula Term rtyp Annot unit k) pol env, + eval_cnf env (xcnf pol f) -> hold k (eval_f e_rtyp (eval env) (if pol then f else NOT f)). + Proof. + induction f. + - (* TT *) + unfold eval_cnf. + simpl. + destruct pol ; intros; simpl; auto with tauto. + rewrite eval_cnf_ff in H. tauto. + - (* FF *) + destruct pol ; simpl in *; intros; auto with tauto. + + rewrite eval_cnf_ff in H. tauto. + - (* P *) + simpl. + destruct pol ; intros ;simpl. + + rewrite eval_cnf_ff in H. tauto. + + rewrite eval_cnf_ff in H. tauto. + - (* A *) + simpl. + destruct pol ; simpl. + intros. + eapply normalise_correct ; eauto. + (* A 2 *) + intros. + eapply negate_correct ; eauto. + - (* AND *) + destruct pol ; simpl. + + (* pol = true *) + intros. + rewrite eval_cnf_and_opt in H. + unfold and_cnf in H. + rewrite eval_cnf_app in H. + destruct H. + apply hold_eAND; split. + apply (IHf1 _ _ H). + apply (IHf2 _ _ H0). + + (* pol = false *) + intros. + apply hold_eNOT. + rewrite hold_eAND. + rewrite or_cnf_opt_correct in H. + rewrite or_cnf_correct in H. + destruct H as [H | H]. + generalize (IHf1 false env H). + simpl. + rewrite hold_eNOT. + tauto. + generalize (IHf2 false env H). + simpl. + rewrite hold_eNOT. + tauto. + - (* OR *) + simpl. + destruct pol. + + (* pol = true *) + intros. unfold mk_or in H. + rewrite or_cnf_opt_correct in H. + rewrite or_cnf_correct in H. + destruct H as [H | H]. + generalize (IHf1 _ env H). + simpl. + rewrite hold_eOR. + tauto. + generalize (IHf2 _ env H). + simpl. + rewrite hold_eOR. + tauto. + + (* pol = true *) + intros. unfold mk_or in H. + rewrite eval_cnf_and_opt in H. + unfold and_cnf. + rewrite eval_cnf_app in H. + destruct H as [H0 H1]. + simpl. + generalize (IHf1 _ _ H0). + generalize (IHf2 _ _ H1). + simpl. + rewrite ! hold_eNOT. + rewrite ! hold_eOR. + tauto. + - (**) + simpl. + destruct pol ; simpl. + intros. + apply (IHf false) ; auto. + intros. + generalize (IHf _ _ H). + rewrite ! hold_eNOT. + tauto. + - (* IMPL *) + apply xcnf_impl; auto. + - apply xcnf_iff ; auto. + - simpl. + destruct (is_bool f2) eqn:EQ. + + apply is_bool_inv in EQ. + destruct b; subst; intros; + apply IHf1 in H; + destruct pol ; simpl in * ; auto. + * unfold is_true in H. + rewrite negb_true_iff in H. + congruence. + * + unfold is_true in H. + rewrite negb_true_iff in H. + congruence. + * unfold is_true in H. + congruence. + + intros. + rewrite <- mk_iff_is_bool in H. + apply xcnf_iff in H; auto. + simpl in H. + destruct pol ; simpl in *. + rewrite <- hold_eEQ. + simpl; auto. + rewrite <- hold_eEQ. + simpl; auto. + unfold is_true in *. + rewrite negb_true_iff in H. + congruence. + Qed. Variable Witness : Type. Variable checker : list (Term'*Annot) -> Witness -> bool. @@ -1370,28 +2015,26 @@ Section S. tauto. Qed. - - Definition tauto_checker (f:@GFormula Term Prop Annot unit) (w:list Witness) : bool := + Definition tauto_checker (f:@GFormula Term rtyp Annot unit isProp) (w:list Witness) : bool := cnf_checker (xcnf true f) w. - Lemma tauto_checker_sound : forall t w, tauto_checker t w = true -> forall env, eval_f (fun x => x) (eval env) t. + Lemma tauto_checker_sound : forall t w, tauto_checker t w = true -> forall env, eval_f e_rtyp (eval env) t. Proof. unfold tauto_checker. intros. - change (eval_f (fun x => x) (eval env) t) with (eval_f (fun x => x) (eval env) (if true then t else TT)). + change (eval_f e_rtyp (eval env) t) with (eval_f e_rtyp (eval env) (if true then t else TT isProp)). apply (xcnf_correct t true). eapply cnf_checker_sound ; eauto. Qed. - Definition eval_bf {A : Type} (ea : A -> Prop) (f: BFormula A) := eval_f (fun x => x) ea f. - + Definition eval_bf {A : Type} (ea : forall (k: kind), A -> rtyp k) (k: kind) (f: BFormula A k) := eval_f e_rtyp ea f. - Lemma eval_bf_map : forall T U (fct: T-> U) env f , - eval_bf env (map_bformula fct f) = eval_bf (fun x => env (fct x)) f. -Proof. - induction f ; simpl ; try (rewrite IHf1 ; rewrite IHf2) ; auto. - rewrite <- IHf. auto. -Qed. + Lemma eval_bf_map : forall T U (fct: T-> U) env (k: kind) (f:BFormula T k) , + eval_bf env (map_bformula fct f) = eval_bf (fun b x => env b (fct x)) f. + Proof. + induction f ; simpl ; try (rewrite IHf1 ; rewrite IHf2) ; auto. + rewrite <- IHf. auto. + Qed. End S. diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v index bff9671fee..935757f30a 100644 --- a/theories/micromega/ZMicromega.v +++ b/theories/micromega/ZMicromega.v @@ -176,7 +176,7 @@ Proof. rewrite ZNpower. congruence. Qed. -Definition Zeval_op2 (o : Op2) : Z -> Z -> Prop := +Definition Zeval_pop2 (o : Op2) : Z -> Z -> Prop := match o with | OpEq => @eq Z | OpNEq => fun x y => ~ x = y @@ -187,14 +187,62 @@ match o with end. -Definition Zeval_formula (env : PolEnv Z) (f : Formula Z):= +Definition Zeval_bop2 (o : Op2) : Z -> Z -> bool := +match o with +| OpEq => Z.eqb +| OpNEq => fun x y => negb (Z.eqb x y) +| OpLe => Z.leb +| OpGe => Z.geb +| OpLt => Z.ltb +| OpGt => Z.gtb +end. + +Lemma pop2_bop2 : + forall (op : Op2) (q1 q2 : Z), is_true (Zeval_bop2 op q1 q2) <-> Zeval_pop2 op q1 q2. +Proof. + unfold is_true. + destruct op ; simpl; intros. + - apply Z.eqb_eq. + - rewrite <- Z.eqb_eq. + rewrite negb_true_iff. + destruct (q1 =? q2) ; intuition congruence. + - apply Z.leb_le. + - rewrite Z.geb_le. rewrite Z.ge_le_iff. tauto. + - apply Z.ltb_lt. + - rewrite <- Zgt_is_gt_bool; tauto. +Qed. + +Definition Zeval_op2 (k: Tauto.kind) : Op2 -> Z -> Z -> Tauto.rtyp k:= + if k as k0 return (Op2 -> Z -> Z -> Tauto.rtyp k0) + then Zeval_pop2 else Zeval_bop2. + + +Lemma Zeval_op2_hold : forall k op q1 q2, + Tauto.hold k (Zeval_op2 k op q1 q2) <-> Zeval_pop2 op q1 q2. +Proof. + destruct k. + simpl ; tauto. + simpl. apply pop2_bop2. +Qed. + + +Definition Zeval_formula (env : PolEnv Z) (k: Tauto.kind) (f : Formula Z):= let (lhs, op, rhs) := f in - (Zeval_op2 op) (Zeval_expr env lhs) (Zeval_expr env rhs). + (Zeval_op2 k op) (Zeval_expr env lhs) (Zeval_expr env rhs). Definition Zeval_formula' := eval_formula Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt (fun x => x) (fun x => x) (pow_N 1 Z.mul). -Lemma Zeval_formula_compat' : forall env f, Zeval_formula env f <-> Zeval_formula' env f. +Lemma Zeval_formula_compat : forall env k f, Tauto.hold k (Zeval_formula env k f) <-> Zeval_formula env Tauto.isProp f. +Proof. + destruct k ; simpl. + - tauto. + - destruct f ; simpl. + rewrite <- Zeval_op2_hold with (k:=Tauto.isBool). + simpl. tauto. +Qed. + +Lemma Zeval_formula_compat' : forall env f, Zeval_formula env Tauto.isProp f <-> Zeval_formula' env f. Proof. intros. unfold Zeval_formula. @@ -312,7 +360,7 @@ Definition xnnormalise (t : Formula Z) : NFormula Z := Lemma xnnormalise_correct : forall env f, - eval_nformula env (xnnormalise f) <-> Zeval_formula env f. + eval_nformula env (xnnormalise f) <-> Zeval_formula env Tauto.isProp f. Proof. intros. rewrite Zeval_formula_compat'. @@ -393,6 +441,7 @@ Proof. Qed. + Require Import Coq.micromega.Tauto BinNums. Definition cnf_of_list {T: Type} (tg : T) (l : list (NFormula Z)) := @@ -435,7 +484,7 @@ Definition normalise {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T := if Zunsat f then cnf_ff _ _ else cnf_of_list tg (xnormalise f). -Lemma normalise_correct : forall (T: Type) env t (tg:T), eval_cnf eval_nformula env (normalise t tg) <-> Zeval_formula env t. +Lemma normalise_correct : forall (T: Type) env t (tg:T), eval_cnf eval_nformula env (normalise t tg) <-> Zeval_formula env Tauto.isProp t. Proof. intros. rewrite <- xnnormalise_correct. @@ -449,6 +498,7 @@ Proof. apply xnormalise_correct. Qed. + Definition xnegate (f:NFormula Z) : list (NFormula Z) := let (e,o) := f in match o with @@ -478,7 +528,7 @@ Proof. - tauto. Qed. -Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env t. +Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env Tauto.isProp t. Proof. intros. rewrite <- xnnormalise_correct. @@ -492,10 +542,10 @@ Proof. apply xnegate_correct. Qed. -Definition cnfZ (Annot: Type) (TX : Type) (AF : Type) (f : TFormula (Formula Z) Annot TX AF) := +Definition cnfZ (Annot: Type) (TX : Tauto.kind -> Type) (AF : Type) (k: Tauto.kind) (f : TFormula (Formula Z) Annot TX AF k) := rxcnf Zunsat Zdeduce normalise negate true f. -Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z)) : bool := +Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z) Tauto.isProp) : bool := @tauto_checker (Formula Z) (NFormula Z) unit Zunsat Zdeduce normalise negate ZWitness (fun cl => ZWeakChecker (List.map fst cl)) f w. (* To get a complete checker, the proof format has to be enriched *) @@ -1672,9 +1722,7 @@ Proof. apply Nat.lt_succ_diag_r. Qed. - - -Definition ZTautoChecker (f : BFormula (Formula Z)) (w: list ZArithProof): bool := +Definition ZTautoChecker (f : BFormula (Formula Z) Tauto.isProp) (w: list ZArithProof): bool := @tauto_checker (Formula Z) (NFormula Z) unit Zunsat Zdeduce normalise negate ZArithProof (fun cl => ZChecker (List.map fst cl)) f w. Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_bf (Zeval_formula env) f. @@ -1692,10 +1740,12 @@ Proof. - intros. rewrite normalise_correct in H. - auto. + rewrite Zeval_formula_compat; auto. - intros. rewrite negate_correct in H ; auto. + rewrite Tauto.hold_eNOT. + rewrite Zeval_formula_compat; auto. - intros t w0. unfold eval_tt. intros. @@ -1703,8 +1753,6 @@ Proof. eapply ZChecker_sound; eauto. tauto. Qed. - - Fixpoint xhyps_of_pt (base:nat) (acc : list nat) (pt:ZArithProof) : list nat := match pt with | DoneProof => acc diff --git a/theories/micromega/ZifyBool.v b/theories/micromega/ZifyBool.v index c693824f89..fa3f123b18 100644 --- a/theories/micromega/ZifyBool.v +++ b/theories/micromega/ZifyBool.v @@ -9,177 +9,83 @@ (************************************************************************) Require Import Bool ZArith. Require Import Zify ZifyClasses. +Require Import ZifyInst. Local Open Scope Z_scope. -(* Instances of [ZifyClasses] for dealing with boolean operators. - Various encodings of boolean are possible. One objective is to - have an encoding that is terse but also lia friendly. - *) +(* Instances of [ZifyClasses] for dealing with boolean operators. *) -(** [Z_of_bool] is the injection function for boolean *) -Definition Z_of_bool (b : bool) : Z := if b then 1 else 0. - -(** [bool_of_Z] is a compatible reverse operation *) -Definition bool_of_Z (z : Z) : bool := negb (Z.eqb z 0). - -Lemma Z_of_bool_bound : forall x, 0 <= Z_of_bool x <= 1. -Proof. - destruct x ; simpl; compute; intuition congruence. -Qed. - -Instance Inj_bool_Z : InjTyp bool Z := - { inj := Z_of_bool ; pred :=(fun x => 0 <= x <= 1) ; cstr := Z_of_bool_bound}. -Add InjTyp Inj_bool_Z. +Instance Inj_bool_bool : InjTyp bool bool := + { inj := (fun x => x) ; pred := (fun b => b = true \/ b = false) ; + cstr := (ltac:(intro b; destruct b; tauto))}. +Add Zify InjTyp Inj_bool_bool. (** Boolean operators *) Instance Op_andb : BinOp andb := - { TBOp := Z.min ; - TBOpInj := ltac: (destruct n,m; reflexivity)}. -Add BinOp Op_andb. + { TBOp := andb ; TBOpInj := fun _ _ => eq_refl}. +Add Zify BinOp Op_andb. Instance Op_orb : BinOp orb := - { TBOp := Z.max ; - TBOpInj := ltac:(destruct n,m; reflexivity)}. -Add BinOp Op_orb. + { TBOp := orb ; TBOpInj := fun _ _ => eq_refl}. +Add Zify BinOp Op_orb. Instance Op_implb : BinOp implb := - { TBOp := fun x y => Z.max (1 - x) y; - TBOpInj := ltac:(destruct n,m; reflexivity) }. -Add BinOp Op_implb. + { TBOp := implb; TBOpInj := fun _ _ => eq_refl }. +Add Zify BinOp Op_implb. + +Definition xorb_eq : forall b1 b2, + xorb b1 b2 = andb (orb b1 b2) (negb (eqb b1 b2)). +Proof. + destruct b1,b2 ; reflexivity. +Qed. Instance Op_xorb : BinOp xorb := - { TBOp := fun x y => Z.max (x - y) (y - x); - TBOpInj := ltac:(destruct n,m; reflexivity) }. -Add BinOp Op_xorb. + { TBOp := fun x y => andb (orb x y) (negb (eqb x y)); TBOpInj := xorb_eq }. +Add Zify BinOp Op_xorb. + +Instance Op_eqb : BinOp eqb := + { TBOp := eqb; TBOpInj := fun _ _ => eq_refl }. +Add Zify BinOp Op_eqb. Instance Op_negb : UnOp negb := - { TUOp := fun x => 1 - x ; TUOpInj := ltac:(destruct x; reflexivity)}. -Add UnOp Op_negb. + { TUOp := negb ; TUOpInj := fun _ => eq_refl}. +Add Zify UnOp Op_negb. Instance Op_eq_bool : BinRel (@eq bool) := - {TR := @eq Z ; TRInj := ltac:(destruct n,m; simpl ; intuition congruence) }. -Add BinRel Op_eq_bool. + {TR := @eq bool ; TRInj := ltac:(reflexivity) }. +Add Zify BinRel Op_eq_bool. Instance Op_true : CstOp true := - { TCst := 1 ; TCstInj := eq_refl }. -Add CstOp Op_true. + { TCst := true ; TCstInj := eq_refl }. +Add Zify CstOp Op_true. Instance Op_false : CstOp false := - { TCst := 0 ; TCstInj := eq_refl }. -Add CstOp Op_false. - -(** Comparisons are encoded using the predicates [isZero] and [isLeZero].*) - -Definition isZero (z : Z) := Z_of_bool (Z.eqb z 0). - -Definition isLeZero (x : Z) := Z_of_bool (Z.leb x 0). - -Instance Op_isZero : UnOp isZero := - { TUOp := isZero; TUOpInj := ltac: (reflexivity) }. -Add UnOp Op_isZero. - -Instance Op_isLeZero : UnOp isLeZero := - { TUOp := isLeZero; TUOpInj := ltac: (reflexivity) }. -Add UnOp Op_isLeZero. - -(* Some intermediate lemma *) - -Lemma Z_eqb_isZero : forall n m, - Z_of_bool (n =? m) = isZero (n - m). -Proof. - intros ; unfold isZero. - destruct ( n =? m) eqn:EQ. - - simpl. rewrite Z.eqb_eq in EQ. - rewrite EQ. rewrite Z.sub_diag. - reflexivity. - - - destruct (n - m =? 0) eqn:EQ'. - rewrite Z.eqb_neq in EQ. - rewrite Z.eqb_eq in EQ'. - apply Zminus_eq in EQ'. - congruence. - reflexivity. -Qed. - -Lemma Z_leb_sub : forall x y, x <=? y = ((x - y) <=? 0). -Proof. - intros. - destruct (x <=?y) eqn:B1 ; - destruct (x - y <=?0) eqn:B2 ; auto. - - rewrite Z.leb_le in B1. - rewrite Z.leb_nle in B2. - rewrite Z.le_sub_0 in B2. tauto. - - rewrite Z.leb_nle in B1. - rewrite Z.leb_le in B2. - rewrite Z.le_sub_0 in B2. tauto. -Qed. - -Lemma Z_ltb_leb : forall x y, x <? y = (x +1 <=? y). -Proof. - intros. - destruct (x <?y) eqn:B1 ; - destruct (x + 1 <=?y) eqn:B2 ; auto. - - rewrite Z.ltb_lt in B1. - rewrite Z.leb_nle in B2. - apply Zorder.Zlt_le_succ in B1. - unfold Z.succ in B1. - tauto. - - rewrite Z.ltb_nlt in B1. - rewrite Z.leb_le in B2. - apply Zorder.Zle_lt_succ in B2. - unfold Z.succ in B2. - apply Zorder.Zplus_lt_reg_r in B2. - tauto. -Qed. - + { TCst := false ; TCstInj := eq_refl }. +Add Zify CstOp Op_false. (** Comparison over Z *) Instance Op_Zeqb : BinOp Z.eqb := - { TBOp := fun x y => isZero (Z.sub x y) ; TBOpInj := Z_eqb_isZero}. + { TBOp := Z.eqb ; TBOpInj := fun _ _ => eq_refl }. +Add Zify BinOp Op_Zeqb. Instance Op_Zleb : BinOp Z.leb := - { TBOp := fun x y => isLeZero (x-y) ; - TBOpInj := - ltac: (intros;unfold isLeZero; - rewrite Z_leb_sub; - auto) }. -Add BinOp Op_Zleb. + { TBOp := Z.leb; TBOpInj := fun _ _ => eq_refl }. +Add Zify BinOp Op_Zleb. Instance Op_Zgeb : BinOp Z.geb := - { TBOp := fun x y => isLeZero (y-x) ; - TBOpInj := ltac:( - intros; - unfold isLeZero; - rewrite Z.geb_leb; - rewrite Z_leb_sub; - auto) }. -Add BinOp Op_Zgeb. + { TBOp := Z.geb; TBOpInj := fun _ _ => eq_refl }. +Add Zify BinOp Op_Zgeb. Instance Op_Zltb : BinOp Z.ltb := - { TBOp := fun x y => isLeZero (x+1-y) ; - TBOpInj := ltac:( - intros; - unfold isLeZero; - rewrite Z_ltb_leb; - rewrite <- Z_leb_sub; - reflexivity) }. + { TBOp := Z.ltb ; TBOpInj := fun _ _ => eq_refl }. +Add Zify BinOp Op_Zltb. Instance Op_Zgtb : BinOp Z.gtb := - { TBOp := fun x y => isLeZero (y-x+1) ; - TBOpInj := ltac:( - intros; - unfold isLeZero; - rewrite Z.gtb_ltb; - rewrite Z_ltb_leb; - rewrite Z_leb_sub; - rewrite Z.add_sub_swap; - reflexivity) }. -Add BinOp Op_Zgtb. + { TBOp := Z.gtb; TBOpInj := fun _ _ => eq_refl }. +Add Zify BinOp Op_Zgtb. (** Comparison over nat *) - Lemma Z_of_nat_eqb_iff : forall n m, (n =? m)%nat = (Z.of_nat n =? Z.of_nat m). Proof. @@ -211,68 +117,45 @@ Proof. Qed. Instance Op_nat_eqb : BinOp Nat.eqb := - { TBOp := fun x y => isZero (Z.sub x y) ; - TBOpInj := ltac:( - intros; simpl; - rewrite <- Z_eqb_isZero; - f_equal; apply Z_of_nat_eqb_iff) }. -Add BinOp Op_nat_eqb. + { TBOp := Z.eqb; TBOpInj := Z_of_nat_eqb_iff }. +Add Zify BinOp Op_nat_eqb. Instance Op_nat_leb : BinOp Nat.leb := - { TBOp := fun x y => isLeZero (x-y) ; - TBOpInj := ltac:( - intros; - rewrite Z_of_nat_leb_iff; - unfold isLeZero; - rewrite Z_leb_sub; - auto) }. -Add BinOp Op_nat_leb. + { TBOp := Z.leb; TBOpInj := Z_of_nat_leb_iff }. +Add Zify BinOp Op_nat_leb. Instance Op_nat_ltb : BinOp Nat.ltb := - { TBOp := fun x y => isLeZero (x+1-y) ; - TBOpInj := ltac:( - intros; - rewrite Z_of_nat_ltb_iff; - unfold isLeZero; - rewrite Z_ltb_leb; - rewrite <- Z_leb_sub; - reflexivity) }. -Add BinOp Op_nat_ltb. - -(** Injected boolean operators *) - -Lemma Z_eqb_ZSpec_ok : forall x, 0 <= isZero x <= 1 /\ - (x = 0 <-> isZero x = 1). + { TBOp := Z.ltb; TBOpInj := Z_of_nat_ltb_iff }. +Add Zify BinOp Op_nat_ltb. + +Lemma b2n_b2z : forall x, Z.of_nat (Nat.b2n x) = Z.b2z x. Proof. - intros. - unfold isZero. - destruct (x =? 0) eqn:EQ. - - apply Z.eqb_eq in EQ. - simpl. intuition try congruence; - compute ; congruence. - - apply Z.eqb_neq in EQ. - simpl. intuition try congruence; - compute ; congruence. + intro. destruct x ; reflexivity. Qed. +Instance Op_b2n : UnOp Nat.b2n := + { TUOp := Z.b2z; TUOpInj := b2n_b2z }. +Add Zify UnOp Op_b2n. -Instance Z_eqb_ZSpec : UnOpSpec isZero := - {| UPred := fun n r => 0 <= r <= 1 /\ (n = 0 <-> isZero n = 1) ; USpec := Z_eqb_ZSpec_ok |}. -Add Spec Z_eqb_ZSpec. +Instance Op_b2z : UnOp Z.b2z := + { TUOp := Z.b2z; TUOpInj := fun _ => eq_refl }. +Add Zify UnOp Op_b2z. -Lemma leZeroSpec_ok : forall x, x <= 0 /\ isLeZero x = 1 \/ x > 0 /\ isLeZero x = 0. +Lemma b2z_spec : forall b, (b = true /\ Z.b2z b = 1) \/ (b = false /\ Z.b2z b = 0). Proof. - intros. - unfold isLeZero. - destruct (x <=? 0) eqn:EQ. - - apply Z.leb_le in EQ. - simpl. intuition congruence. - - simpl. - apply Z.leb_nle in EQ. - apply Zorder.Znot_le_gt in EQ. - tauto. + destruct b ; simpl; intuition congruence. Qed. -Instance leZeroSpec : UnOpSpec isLeZero := - {| UPred := fun n r => (n<=0 /\ r = 1) \/ (n > 0 /\ r = 0) ; USpec := leZeroSpec_ok|}. -Add Spec leZeroSpec. +Instance b2zSpec : UnOpSpec Z.b2z := + { UPred := fun b r => (b = true /\ r = 1) \/ (b = false /\ r = 0); + USpec := b2z_spec + }. +Add Zify UnOpSpec b2zSpec. + +Ltac elim_bool_cstr := + repeat match goal with + | C : ?B = true \/ ?B = false |- _ => + destruct C as [C|C]; rewrite C in * + end. + +Ltac Zify.zify_post_hook ::= elim_bool_cstr. diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v index 3eb4c924ae..37eef12381 100644 --- a/theories/micromega/ZifyClasses.v +++ b/theories/micromega/ZifyClasses.v @@ -34,19 +34,19 @@ Class InjTyp (S : Type) (T : Type) := (** [BinOp Op] declares a source operator [Op: S1 -> S2 -> S3]. *) -Class BinOp {S1 S2 S3:Type} {T:Type} (Op : S1 -> S2 -> S3) {I1 : InjTyp S1 T} {I2 : InjTyp S2 T} {I3 : InjTyp S3 T} := +Class BinOp {S1 S2 S3 T1 T2 T3:Type} (Op : S1 -> S2 -> S3) {I1 : InjTyp S1 T1} {I2 : InjTyp S2 T2} {I3 : InjTyp S3 T3} := mkbop { (* [TBOp] is the target operator after injection of operands. *) - TBOp : T -> T -> T; + TBOp : T1 -> T2 -> T3; (* [TBOpInj] states the correctness of the injection. *) TBOpInj : forall (n:S1) (m:S2), inj (Op n m) = TBOp (inj n) (inj m) }. (** [Unop Op] declares a source operator [Op : S1 -> S2]. *) -Class UnOp {S1 S2 T:Type} (Op : S1 -> S2) {I1 : InjTyp S1 T} {I2 : InjTyp S2 T} := +Class UnOp {S1 S2 T1 T2:Type} (Op : S1 -> S2) {I1 : InjTyp S1 T1} {I2 : InjTyp S2 T2} := mkuop { (* [TUOp] is the target operator after injection of operands. *) - TUOp : T -> T; + TUOp : T1 -> T2; (* [TUOpInj] states the correctness of the injection. *) TUOpInj : forall (x:S1), inj (Op x) = TUOp (inj x) }. @@ -90,15 +90,15 @@ Class PropUOp (Op : Prop -> Prop) := NB1: The Ltac code is currently limited to (Op: Z -> Z -> Z) NB2: This is not sufficient to cope with [Z.div] or [Z.mod] *) -Class BinOpSpec {S T: Type} (Op : T -> T -> T) {I : InjTyp S T} := +Class BinOpSpec {T1 T2 T3: Type} (Op : T1 -> T2 -> T3) := mkbspec { - BPred : T -> T -> T -> Prop; + BPred : T1 -> T2 -> T3 -> Prop; BSpec : forall x y, BPred x y (Op x y) }. -Class UnOpSpec {S T: Type} (Op : T -> T) {I : InjTyp S T} := +Class UnOpSpec {T1 T2: Type} (Op : T1 -> T2) := mkuspec { - UPred : T -> T -> Prop; + UPred : T1 -> T2 -> Prop; USpec : forall x, UPred x (Op x) }. @@ -141,9 +141,6 @@ Record injprop := injprop_ok : source_prop <-> target_prop}. - - - (** Lemmas for building rewrite rules. *) Definition PropOp_iff (Op : Prop -> Prop -> Prop) := @@ -152,22 +149,22 @@ Definition PropOp_iff (Op : Prop -> Prop -> Prop) := Definition PropUOp_iff (Op : Prop -> Prop) := forall (p1 q1 :Prop), (p1 <-> q1) -> (Op p1 <-> Op q1). -Lemma mkapp2 (S1 S2 S3 T : Type) (Op : S1 -> S2 -> S3) - (I1 : S1 -> T) (I2 : S2 -> T) (I3 : S3 -> T) - (TBOP : T -> T -> T) +Lemma mkapp2 (S1 S2 S3 T1 T2 T3 : Type) (Op : S1 -> S2 -> S3) + (I1 : S1 -> T1) (I2 : S2 -> T2) (I3 : S3 -> T3) + (TBOP : T1 -> T2 -> T3) (TBOPINJ : forall n m, I3 (Op n m) = TBOP (I1 n) (I2 m)) - (s1 : S1) (t1 : T) (P1: I1 s1 = t1) - (s2 : S2) (t2 : T) (P2: I2 s2 = t2): I3 (Op s1 s2) = TBOP t1 t2. + (s1 : S1) (t1 : T1) (P1: I1 s1 = t1) + (s2 : S2) (t2 : T2) (P2: I2 s2 = t2): I3 (Op s1 s2) = TBOP t1 t2. Proof. subst. apply TBOPINJ. Qed. -Lemma mkapp (S1 S2 T : Type) (OP : S1 -> S2) - (I1 : S1 -> T) - (I2 : S2 -> T) - (TUOP : T -> T) +Lemma mkapp (S1 S2 T1 T2 : Type) (OP : S1 -> S2) + (I1 : S1 -> T1) + (I2 : S2 -> T2) + (TUOP : T1 -> T2) (TUOPINJ : forall n, I2 (OP n) = TUOP (I1 n)) - (s1: S1) (t1: T) (P1: I1 s1 = t1): I2 (OP s1) = TUOP t1. + (s1: S1) (t1: T1) (P1: I1 s1 = t1): I2 (OP s1) = TUOP t1. Proof. subst. apply TUOPINJ. Qed. @@ -223,8 +220,6 @@ Proof. exact (fun H => proj1 IFF H). Qed. -Definition identity (A : Type) : A -> A := fun x => x. - (** Registering constants for use by the plugin *) Register eq_iff as ZifyClasses.eq_iff. Register target_prop as ZifyClasses.target_prop. @@ -268,6 +263,4 @@ Register iff_morph as ZifyClasses.iff_morph. Register impl_morph as ZifyClasses.impl_morph. Register not as ZifyClasses.not. Register not_morph as ZifyClasses.not_morph. - -(** Identify function *) -Register identity as ZifyClasses.identity. +Register True as ZifyClasses.True. diff --git a/theories/micromega/ZifyComparison.v b/theories/micromega/ZifyComparison.v index 9b37f10841..a4ada571f1 100644 --- a/theories/micromega/ZifyComparison.v +++ b/theories/micromega/ZifyComparison.v @@ -28,30 +28,30 @@ Qed. Instance Inj_comparison_Z : InjTyp comparison Z := { inj := Z_of_comparison ; pred :=(fun x => -1 <= x <= 1) ; cstr := Z_of_comparison_bound}. -Add InjTyp Inj_comparison_Z. +Add Zify InjTyp Inj_comparison_Z. Definition ZcompareZ (x y : Z) := Z_of_comparison (Z.compare x y). Program Instance BinOp_Zcompare : BinOp Z.compare := { TBOp := ZcompareZ }. -Add BinOp BinOp_Zcompare. +Add Zify BinOp BinOp_Zcompare. Instance Op_eq_comparison : BinRel (@eq comparison) := {TR := @eq Z ; TRInj := ltac:(destruct n,m; simpl ; intuition congruence) }. -Add BinRel Op_eq_comparison. +Add Zify BinRel Op_eq_comparison. Instance Op_Eq : CstOp Eq := { TCst := 0 ; TCstInj := eq_refl }. -Add CstOp Op_Eq. +Add Zify CstOp Op_Eq. Instance Op_Lt : CstOp Lt := { TCst := -1 ; TCstInj := eq_refl }. -Add CstOp Op_Lt. +Add Zify CstOp Op_Lt. Instance Op_Gt : CstOp Gt := { TCst := 1 ; TCstInj := eq_refl }. -Add CstOp Op_Gt. +Add Zify CstOp Op_Gt. Lemma Zcompare_spec : forall x y, @@ -79,4 +79,4 @@ Instance ZcompareSpec : BinOpSpec ZcompareZ := /\ (x < y -> r = -1) ; BSpec := Zcompare_spec|}. -Add Spec ZcompareSpec. +Add Zify BinOpSpec ZcompareSpec. diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v index 5b15dc072a..0e135ba793 100644 --- a/theories/micromega/ZifyInst.v +++ b/theories/micromega/ZifyInst.v @@ -25,117 +25,117 @@ Ltac refl := Instance Inj_Z_Z : InjTyp Z Z := mkinj _ _ (fun x => x) (fun x => True ) (fun _ => I). -Add InjTyp Inj_Z_Z. +Add Zify InjTyp Inj_Z_Z. (** Support for nat *) Instance Inj_nat_Z : InjTyp nat Z := mkinj _ _ Z.of_nat (fun x => 0 <= x ) Nat2Z.is_nonneg. -Add InjTyp Inj_nat_Z. +Add Zify InjTyp Inj_nat_Z. (* zify_nat_rel *) Instance Op_ge : BinRel ge := {| TR := Z.ge; TRInj := Nat2Z.inj_ge |}. -Add BinRel Op_ge. +Add Zify BinRel Op_ge. Instance Op_lt : BinRel lt := {| TR := Z.lt; TRInj := Nat2Z.inj_lt |}. -Add BinRel Op_lt. +Add Zify BinRel Op_lt. Instance Op_Nat_lt : BinRel Nat.lt := Op_lt. -Add BinRel Op_Nat_lt. +Add Zify BinRel Op_Nat_lt. Instance Op_gt : BinRel gt := {| TR := Z.gt; TRInj := Nat2Z.inj_gt |}. -Add BinRel Op_gt. +Add Zify BinRel Op_gt. Instance Op_le : BinRel le := {| TR := Z.le; TRInj := Nat2Z.inj_le |}. -Add BinRel Op_le. +Add Zify BinRel Op_le. Instance Op_Nat_le : BinRel Nat.le := Op_le. -Add BinRel Op_Nat_le. +Add Zify BinRel Op_Nat_le. Instance Op_eq_nat : BinRel (@eq nat) := {| TR := @eq Z ; TRInj := fun x y : nat => iff_sym (Nat2Z.inj_iff x y) |}. -Add BinRel Op_eq_nat. +Add Zify BinRel Op_eq_nat. Instance Op_Nat_eq : BinRel (Nat.eq) := Op_eq_nat. -Add BinRel Op_Nat_eq. +Add Zify BinRel Op_Nat_eq. (* zify_nat_op *) Instance Op_plus : BinOp Nat.add := {| TBOp := Z.add; TBOpInj := Nat2Z.inj_add |}. -Add BinOp Op_plus. +Add Zify BinOp Op_plus. Instance Op_sub : BinOp Nat.sub := {| TBOp := fun n m => Z.max 0 (n - m) ; TBOpInj := Nat2Z.inj_sub_max |}. -Add BinOp Op_sub. +Add Zify BinOp Op_sub. Instance Op_mul : BinOp Nat.mul := {| TBOp := Z.mul ; TBOpInj := Nat2Z.inj_mul |}. -Add BinOp Op_mul. +Add Zify BinOp Op_mul. Instance Op_min : BinOp Nat.min := {| TBOp := Z.min ; TBOpInj := Nat2Z.inj_min |}. -Add BinOp Op_min. +Add Zify BinOp Op_min. Instance Op_max : BinOp Nat.max := {| TBOp := Z.max ; TBOpInj := Nat2Z.inj_max |}. -Add BinOp Op_max. +Add Zify BinOp Op_max. Instance Op_pred : UnOp Nat.pred := {| TUOp := fun n => Z.max 0 (n - 1) ; TUOpInj := Nat2Z.inj_pred_max |}. -Add UnOp Op_pred. +Add Zify UnOp Op_pred. Instance Op_S : UnOp S := {| TUOp := fun x => Z.add x 1 ; TUOpInj := Nat2Z.inj_succ |}. -Add UnOp Op_S. +Add Zify UnOp Op_S. Instance Op_O : CstOp O := {| TCst := Z0 ; TCstInj := eq_refl (Z.of_nat 0) |}. -Add CstOp Op_O. +Add Zify CstOp Op_O. Instance Op_Z_abs_nat : UnOp Z.abs_nat := { TUOp := Z.abs ; TUOpInj := Zabs2Nat.id_abs }. -Add UnOp Op_Z_abs_nat. +Add Zify UnOp Op_Z_abs_nat. (** Support for positive *) Instance Inj_pos_Z : InjTyp positive Z := {| inj := Zpos ; pred := (fun x => 0 < x ) ; cstr := Pos2Z.pos_is_pos |}. -Add InjTyp Inj_pos_Z. +Add Zify InjTyp Inj_pos_Z. Instance Op_pos_to_nat : UnOp Pos.to_nat := {TUOp := (fun x => x); TUOpInj := positive_nat_Z}. -Add UnOp Op_pos_to_nat. +Add Zify UnOp Op_pos_to_nat. Instance Inj_N_Z : InjTyp N Z := mkinj _ _ Z.of_N (fun x => 0 <= x ) N2Z.is_nonneg. -Add InjTyp Inj_N_Z. +Add Zify InjTyp Inj_N_Z. Instance Op_N_to_nat : UnOp N.to_nat := { TUOp := fun x => x ; TUOpInj := N_nat_Z }. -Add UnOp Op_N_to_nat. +Add Zify UnOp Op_N_to_nat. (* zify_positive_rel *) Instance Op_pos_ge : BinRel Pos.ge := {| TR := Z.ge; TRInj := fun x y => iff_refl (Z.pos x >= Z.pos y) |}. -Add BinRel Op_pos_ge. +Add Zify BinRel Op_pos_ge. Instance Op_pos_lt : BinRel Pos.lt := {| TR := Z.lt; TRInj := fun x y => iff_refl (Z.pos x < Z.pos y) |}. -Add BinRel Op_pos_lt. +Add Zify BinRel Op_pos_lt. Instance Op_pos_gt : BinRel Pos.gt := {| TR := Z.gt; TRInj := fun x y => iff_refl (Z.pos x > Z.pos y) |}. -Add BinRel Op_pos_gt. +Add Zify BinRel Op_pos_gt. Instance Op_pos_le : BinRel Pos.le := {| TR := Z.le; TRInj := fun x y => iff_refl (Z.pos x <= Z.pos y) |}. -Add BinRel Op_pos_le. +Add Zify BinRel Op_pos_le. Lemma eq_pos_inj : forall (x y:positive), x = y <-> Z.pos x = Z.pos y. Proof. @@ -145,36 +145,36 @@ Qed. Instance Op_eq_pos : BinRel (@eq positive) := { TR := @eq Z ; TRInj := eq_pos_inj }. -Add BinRel Op_eq_pos. +Add Zify BinRel Op_eq_pos. (* zify_positive_op *) Instance Op_Z_of_N : UnOp Z.of_N := { TUOp := (fun x => x) ; TUOpInj := fun x => eq_refl (Z.of_N x) }. -Add UnOp Op_Z_of_N. +Add Zify UnOp Op_Z_of_N. Instance Op_Z_to_N : UnOp Z.to_N := { TUOp := fun x => Z.max 0 x ; TUOpInj := ltac:(now intro x; destruct x) }. -Add UnOp Op_Z_to_N. +Add Zify UnOp Op_Z_to_N. Instance Op_Z_neg : UnOp Z.neg := { TUOp := Z.opp ; TUOpInj := (fun x => eq_refl (Zneg x))}. -Add UnOp Op_Z_neg. +Add Zify UnOp Op_Z_neg. Instance Op_Z_pos : UnOp Z.pos := { TUOp := (fun x => x) ; TUOpInj := (fun x => eq_refl (Z.pos x))}. -Add UnOp Op_Z_pos. +Add Zify UnOp Op_Z_pos. Instance Op_pos_succ : UnOp Pos.succ := { TUOp := fun x => x + 1; TUOpInj := Pos2Z.inj_succ }. -Add UnOp Op_pos_succ. +Add Zify UnOp Op_pos_succ. Instance Op_pos_pred_double : UnOp Pos.pred_double := { TUOp := fun x => 2 * x - 1; TUOpInj := ltac:(refl) }. -Add UnOp Op_pos_pred_double. +Add Zify UnOp Op_pos_pred_double. Instance Op_pos_pred : UnOp Pos.pred := { TUOp := fun x => Z.max 1 (x - 1) ; @@ -182,266 +182,266 @@ Instance Op_pos_pred : UnOp Pos.pred := (intros; rewrite <- Pos.sub_1_r; apply Pos2Z.inj_sub_max) }. -Add UnOp Op_pos_pred. +Add Zify UnOp Op_pos_pred. Instance Op_pos_predN : UnOp Pos.pred_N := { TUOp := fun x => x - 1 ; TUOpInj := ltac: (now destruct x; rewrite N.pos_pred_spec) }. -Add UnOp Op_pos_predN. +Add Zify UnOp Op_pos_predN. Instance Op_pos_of_succ_nat : UnOp Pos.of_succ_nat := { TUOp := fun x => x + 1 ; TUOpInj := Zpos_P_of_succ_nat }. -Add UnOp Op_pos_of_succ_nat. +Add Zify UnOp Op_pos_of_succ_nat. Instance Op_pos_of_nat : UnOp Pos.of_nat := { TUOp := fun x => Z.max 1 x ; TUOpInj := ltac: (now destruct x; [|rewrite <- Pos.of_nat_succ, <- (Nat2Z.inj_max 1)]) }. -Add UnOp Op_pos_of_nat. +Add Zify UnOp Op_pos_of_nat. Instance Op_pos_add : BinOp Pos.add := { TBOp := Z.add ; TBOpInj := ltac: (refl) }. -Add BinOp Op_pos_add. +Add Zify BinOp Op_pos_add. Instance Op_pos_add_carry : BinOp Pos.add_carry := { TBOp := fun x y => x + y + 1 ; TBOpInj := ltac:(now intros; rewrite Pos.add_carry_spec, Pos2Z.inj_succ) }. -Add BinOp Op_pos_add_carry. +Add Zify BinOp Op_pos_add_carry. Instance Op_pos_sub : BinOp Pos.sub := { TBOp := fun n m => Z.max 1 (n - m) ;TBOpInj := Pos2Z.inj_sub_max }. -Add BinOp Op_pos_sub. +Add Zify BinOp Op_pos_sub. Instance Op_pos_mul : BinOp Pos.mul := { TBOp := Z.mul ; TBOpInj := ltac: (refl) }. -Add BinOp Op_pos_mul. +Add Zify BinOp Op_pos_mul. Instance Op_pos_min : BinOp Pos.min := { TBOp := Z.min ; TBOpInj := Pos2Z.inj_min }. -Add BinOp Op_pos_min. +Add Zify BinOp Op_pos_min. Instance Op_pos_max : BinOp Pos.max := { TBOp := Z.max ; TBOpInj := Pos2Z.inj_max }. -Add BinOp Op_pos_max. +Add Zify BinOp Op_pos_max. Instance Op_pos_pow : BinOp Pos.pow := { TBOp := Z.pow ; TBOpInj := Pos2Z.inj_pow }. -Add BinOp Op_pos_pow. +Add Zify BinOp Op_pos_pow. Instance Op_pos_square : UnOp Pos.square := { TUOp := Z.square ; TUOpInj := Pos2Z.inj_square }. -Add UnOp Op_pos_square. +Add Zify UnOp Op_pos_square. Instance Op_xO : UnOp xO := { TUOp := fun x => 2 * x ; TUOpInj := ltac: (refl) }. -Add UnOp Op_xO. +Add Zify UnOp Op_xO. Instance Op_xI : UnOp xI := { TUOp := fun x => 2 * x + 1 ; TUOpInj := ltac: (refl) }. -Add UnOp Op_xI. +Add Zify UnOp Op_xI. Instance Op_xH : CstOp xH := { TCst := 1%Z ; TCstInj := ltac:(refl)}. -Add CstOp Op_xH. +Add Zify CstOp Op_xH. Instance Op_Z_of_nat : UnOp Z.of_nat:= { TUOp := fun x => x ; TUOpInj := (fun x : nat => @eq_refl Z (Z.of_nat x)) }. -Add UnOp Op_Z_of_nat. +Add Zify UnOp Op_Z_of_nat. (* zify_N_rel *) Instance Op_N_ge : BinRel N.ge := {| TR := Z.ge ; TRInj := N2Z.inj_ge |}. -Add BinRel Op_N_ge. +Add Zify BinRel Op_N_ge. Instance Op_N_lt : BinRel N.lt := {| TR := Z.lt ; TRInj := N2Z.inj_lt |}. -Add BinRel Op_N_lt. +Add Zify BinRel Op_N_lt. Instance Op_N_gt : BinRel N.gt := {| TR := Z.gt ; TRInj := N2Z.inj_gt |}. -Add BinRel Op_N_gt. +Add Zify BinRel Op_N_gt. Instance Op_N_le : BinRel N.le := {| TR := Z.le ; TRInj := N2Z.inj_le |}. -Add BinRel Op_N_le. +Add Zify BinRel Op_N_le. Instance Op_eq_N : BinRel (@eq N) := {| TR := @eq Z ; TRInj := fun x y : N => iff_sym (N2Z.inj_iff x y) |}. -Add BinRel Op_eq_N. +Add Zify BinRel Op_eq_N. (* zify_N_op *) Instance Op_N_N0 : CstOp N0 := { TCst := Z0 ; TCstInj := eq_refl }. -Add CstOp Op_N_N0. +Add Zify CstOp Op_N_N0. Instance Op_N_Npos : UnOp Npos := { TUOp := (fun x => x) ; TUOpInj := ltac:(refl) }. -Add UnOp Op_N_Npos. +Add Zify UnOp Op_N_Npos. Instance Op_N_of_nat : UnOp N.of_nat := { TUOp := fun x => x ; TUOpInj := nat_N_Z }. -Add UnOp Op_N_of_nat. +Add Zify UnOp Op_N_of_nat. Instance Op_Z_abs_N : UnOp Z.abs_N := { TUOp := Z.abs ; TUOpInj := N2Z.inj_abs_N }. -Add UnOp Op_Z_abs_N. +Add Zify UnOp Op_Z_abs_N. Instance Op_N_pos : UnOp N.pos := { TUOp := fun x => x ; TUOpInj := ltac:(refl)}. -Add UnOp Op_N_pos. +Add Zify UnOp Op_N_pos. Instance Op_N_add : BinOp N.add := {| TBOp := Z.add ; TBOpInj := N2Z.inj_add |}. -Add BinOp Op_N_add. +Add Zify BinOp Op_N_add. Instance Op_N_min : BinOp N.min := {| TBOp := Z.min ; TBOpInj := N2Z.inj_min |}. -Add BinOp Op_N_min. +Add Zify BinOp Op_N_min. Instance Op_N_max : BinOp N.max := {| TBOp := Z.max ; TBOpInj := N2Z.inj_max |}. -Add BinOp Op_N_max. +Add Zify BinOp Op_N_max. Instance Op_N_mul : BinOp N.mul := {| TBOp := Z.mul ; TBOpInj := N2Z.inj_mul |}. -Add BinOp Op_N_mul. +Add Zify BinOp Op_N_mul. Instance Op_N_sub : BinOp N.sub := {| TBOp := fun x y => Z.max 0 (x - y) ; TBOpInj := N2Z.inj_sub_max|}. -Add BinOp Op_N_sub. +Add Zify BinOp Op_N_sub. Instance Op_N_div : BinOp N.div := {| TBOp := Z.div ; TBOpInj := N2Z.inj_div|}. -Add BinOp Op_N_div. +Add Zify BinOp Op_N_div. Instance Op_N_mod : BinOp N.modulo := {| TBOp := Z.rem ; TBOpInj := N2Z.inj_rem|}. -Add BinOp Op_N_mod. +Add Zify BinOp Op_N_mod. Instance Op_N_pred : UnOp N.pred := { TUOp := fun x => Z.max 0 (x - 1) ; TUOpInj := ltac:(intros; rewrite N.pred_sub; apply N2Z.inj_sub_max) }. -Add UnOp Op_N_pred. +Add Zify UnOp Op_N_pred. Instance Op_N_succ : UnOp N.succ := {| TUOp := fun x => x + 1 ; TUOpInj := N2Z.inj_succ |}. -Add UnOp Op_N_succ. +Add Zify UnOp Op_N_succ. (** Support for Z - injected to itself *) (* zify_Z_rel *) Instance Op_Z_ge : BinRel Z.ge := {| TR := Z.ge ; TRInj := fun x y => iff_refl (x>= y)|}. -Add BinRel Op_Z_ge. +Add Zify BinRel Op_Z_ge. Instance Op_Z_lt : BinRel Z.lt := {| TR := Z.lt ; TRInj := fun x y => iff_refl (x < y)|}. -Add BinRel Op_Z_lt. +Add Zify BinRel Op_Z_lt. Instance Op_Z_gt : BinRel Z.gt := {| TR := Z.gt ;TRInj := fun x y => iff_refl (x > y)|}. -Add BinRel Op_Z_gt. +Add Zify BinRel Op_Z_gt. Instance Op_Z_le : BinRel Z.le := {| TR := Z.le ;TRInj := fun x y => iff_refl (x <= y)|}. -Add BinRel Op_Z_le. +Add Zify BinRel Op_Z_le. Instance Op_eqZ : BinRel (@eq Z) := { TR := @eq Z ; TRInj := fun x y => iff_refl (x = y) }. -Add BinRel Op_eqZ. +Add Zify BinRel Op_eqZ. Instance Op_Z_Z0 : CstOp Z0 := { TCst := Z0 ; TCstInj := eq_refl }. -Add CstOp Op_Z_Z0. +Add Zify CstOp Op_Z_Z0. Instance Op_Z_add : BinOp Z.add := { TBOp := Z.add ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_add. +Add Zify BinOp Op_Z_add. Instance Op_Z_min : BinOp Z.min := { TBOp := Z.min ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_min. +Add Zify BinOp Op_Z_min. Instance Op_Z_max : BinOp Z.max := { TBOp := Z.max ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_max. +Add Zify BinOp Op_Z_max. Instance Op_Z_mul : BinOp Z.mul := { TBOp := Z.mul ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_mul. +Add Zify BinOp Op_Z_mul. Instance Op_Z_sub : BinOp Z.sub := { TBOp := Z.sub ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_sub. +Add Zify BinOp Op_Z_sub. Instance Op_Z_div : BinOp Z.div := { TBOp := Z.div ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_div. +Add Zify BinOp Op_Z_div. Instance Op_Z_mod : BinOp Z.modulo := { TBOp := Z.modulo ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_mod. +Add Zify BinOp Op_Z_mod. Instance Op_Z_rem : BinOp Z.rem := { TBOp := Z.rem ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_rem. +Add Zify BinOp Op_Z_rem. Instance Op_Z_quot : BinOp Z.quot := { TBOp := Z.quot ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_quot. +Add Zify BinOp Op_Z_quot. Instance Op_Z_succ : UnOp Z.succ := { TUOp := fun x => x + 1 ; TUOpInj := ltac:(refl) }. -Add UnOp Op_Z_succ. +Add Zify UnOp Op_Z_succ. Instance Op_Z_pred : UnOp Z.pred := { TUOp := fun x => x - 1 ; TUOpInj := ltac:(refl) }. -Add UnOp Op_Z_pred. +Add Zify UnOp Op_Z_pred. Instance Op_Z_opp : UnOp Z.opp := { TUOp := Z.opp ; TUOpInj := ltac:(refl) }. -Add UnOp Op_Z_opp. +Add Zify UnOp Op_Z_opp. Instance Op_Z_abs : UnOp Z.abs := { TUOp := Z.abs ; TUOpInj := ltac:(refl) }. -Add UnOp Op_Z_abs. +Add Zify UnOp Op_Z_abs. Instance Op_Z_sgn : UnOp Z.sgn := { TUOp := Z.sgn ; TUOpInj := ltac:(refl) }. -Add UnOp Op_Z_sgn. +Add Zify UnOp Op_Z_sgn. Instance Op_Z_pow : BinOp Z.pow := { TBOp := Z.pow ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_pow. +Add Zify BinOp Op_Z_pow. Instance Op_Z_pow_pos : BinOp Z.pow_pos := { TBOp := Z.pow ; TBOpInj := ltac:(refl) }. -Add BinOp Op_Z_pow_pos. +Add Zify BinOp Op_Z_pow_pos. Instance Op_Z_double : UnOp Z.double := { TUOp := Z.mul 2 ; TUOpInj := Z.double_spec }. -Add UnOp Op_Z_double. +Add Zify UnOp Op_Z_double. Instance Op_Z_pred_double : UnOp Z.pred_double := { TUOp := fun x => 2 * x - 1 ; TUOpInj := Z.pred_double_spec }. -Add UnOp Op_Z_pred_double. +Add Zify UnOp Op_Z_pred_double. Instance Op_Z_succ_double : UnOp Z.succ_double := { TUOp := fun x => 2 * x + 1 ; TUOpInj := Z.succ_double_spec }. -Add UnOp Op_Z_succ_double. +Add Zify UnOp Op_Z_succ_double. Instance Op_Z_square : UnOp Z.square := { TUOp := fun x => x * x ; TUOpInj := Z.square_spec }. -Add UnOp Op_Z_square. +Add Zify UnOp Op_Z_square. Instance Op_Z_div2 : UnOp Z.div2 := { TUOp := fun x => x / 2 ; TUOpInj := Z.div2_div }. -Add UnOp Op_Z_div2. +Add Zify UnOp Op_Z_div2. Instance Op_Z_quot2 : UnOp Z.quot2 := { TUOp := fun x => Z.quot x 2 ; TUOpInj := Zeven.Zquot2_quot }. -Add UnOp Op_Z_quot2. +Add Zify UnOp Op_Z_quot2. Lemma of_nat_to_nat_eq : forall x, Z.of_nat (Z.to_nat x) = Z.max 0 x. Proof. @@ -455,49 +455,28 @@ Qed. Instance Op_Z_to_nat : UnOp Z.to_nat := { TUOp := fun x => Z.max 0 x ; TUOpInj := of_nat_to_nat_eq }. -Add UnOp Op_Z_to_nat. +Add Zify UnOp Op_Z_to_nat. (** Specification of derived operators over Z *) -Lemma z_max_spec : forall n m, - n <= Z.max n m /\ m <= Z.max n m /\ (Z.max n m = n \/ Z.max n m = m). -Proof. - intros. - generalize (Z.le_max_l n m). - generalize (Z.le_max_r n m). - generalize (Z.max_spec_le n m). - intuition idtac. -Qed. - Instance ZmaxSpec : BinOpSpec Z.max := {| BPred := fun n m r => n < m /\ r = m \/ m <= n /\ r = n ; BSpec := Z.max_spec|}. -Add Spec ZmaxSpec. - -Lemma z_min_spec : forall n m, - Z.min n m <= n /\ Z.min n m <= m /\ (Z.min n m = n \/ Z.min n m = m). -Proof. - intros. - generalize (Z.le_min_l n m). - generalize (Z.le_min_r n m). - generalize (Z.min_spec_le n m). - intuition idtac. -Qed. - +Add Zify BinOpSpec ZmaxSpec. Instance ZminSpec : BinOpSpec Z.min := {| BPred := fun n m r => n < m /\ r = n \/ m <= n /\ r = m ; BSpec := Z.min_spec |}. -Add Spec ZminSpec. +Add Zify BinOpSpec ZminSpec. Instance ZsgnSpec : UnOpSpec Z.sgn := {| UPred := fun n r : Z => 0 < n /\ r = 1 \/ 0 = n /\ r = 0 \/ n < 0 /\ r = - (1) ; USpec := Z.sgn_spec|}. -Add Spec ZsgnSpec. +Add Zify UnOpSpec ZsgnSpec. Instance ZabsSpec : UnOpSpec Z.abs := {| UPred := fun n r: Z => 0 <= n /\ r = n \/ n < 0 /\ r = - n ; USpec := Z.abs_spec|}. -Add Spec ZabsSpec. +Add Zify UnOpSpec ZabsSpec. (** Saturate positivity constraints *) @@ -508,7 +487,7 @@ Instance SatProd : Saturate Z.mul := PRes := fun r => 0 <= r; SatOk := Z.mul_nonneg_nonneg |}. -Add Saturate SatProd. +Add Zify Saturate SatProd. Instance SatProdPos : Saturate Z.mul := {| @@ -517,7 +496,7 @@ Instance SatProdPos : Saturate Z.mul := PRes := fun r => 0 < r; SatOk := Z.mul_pos_pos |}. -Add Saturate SatProdPos. +Add Zify Saturate SatProdPos. Lemma pow_pos_strict : forall a b, @@ -536,4 +515,4 @@ Instance SatPowPos : Saturate Z.pow := PRes := fun r => 0 < r; SatOk := pow_pos_strict |}. -Add Saturate SatPowPos. +Add Zify Saturate SatPowPos. |
