diff options
Diffstat (limited to 'plugins/btauto')
| -rw-r--r-- | plugins/btauto/Algebra.v | 36 | ||||
| -rw-r--r-- | plugins/btauto/Reflect.v | 23 | ||||
| -rw-r--r-- | plugins/btauto/g_btauto.mlg (renamed from plugins/btauto/g_btauto.ml4) | 6 | ||||
| -rw-r--r-- | plugins/btauto/plugin_base.dune | 5 | ||||
| -rw-r--r-- | plugins/btauto/refl_btauto.ml | 97 | ||||
| -rw-r--r-- | plugins/btauto/refl_btauto.mli | 11 |
6 files changed, 103 insertions, 75 deletions
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v index ee7341a4a2..638a4cef21 100644 --- a/plugins/btauto/Algebra.v +++ b/plugins/btauto/Algebra.v @@ -1,4 +1,4 @@ -Require Import Bool PArith DecidableClass Omega ROmega. +Require Import Bool PArith DecidableClass Omega Lia. Ltac bool := repeat match goal with @@ -10,7 +10,7 @@ end. Arguments decide P /H. -Hint Extern 5 => progress bool. +Hint Extern 5 => progress bool : core. Ltac define t x H := set (x := t) in *; assert (H : t = x) by reflexivity; clearbody x. @@ -84,9 +84,9 @@ Ltac case_decide := match goal with let H := fresh "H" in define (@decide P D) b H; destruct b; try_decide | [ |- context [Pos.compare ?x ?y] ] => - destruct (Pos.compare_spec x y); try (exfalso; zify; romega) + destruct (Pos.compare_spec x y); try lia | [ X : context [Pos.compare ?x ?y] |- _ ] => - destruct (Pos.compare_spec x y); try (exfalso; zify; romega) + destruct (Pos.compare_spec x y); try lia end. Section Definitions. @@ -147,7 +147,7 @@ Qed. (** * The core reflexive part. *) -Hint Constructors valid. +Hint Constructors valid : core. Fixpoint beq_poly pl pr := match pl with @@ -315,7 +315,7 @@ Section Validity. (* Decision procedure of validity *) -Hint Constructors valid linear. +Hint Constructors valid linear : core. Lemma valid_le_compat : forall k l p, valid k p -> (k <= l)%positive -> valid l p. Proof. @@ -325,13 +325,13 @@ Qed. Lemma linear_le_compat : forall k l p, linear k p -> (k <= l)%positive -> linear l p. Proof. -intros k l p H; revert l; induction H; constructor; eauto; zify; romega. +intros k l p H; revert l; induction H; constructor; eauto; lia. Qed. Lemma linear_valid_incl : forall k p, linear k p -> valid k p. Proof. intros k p H; induction H; constructor; auto. -eapply valid_le_compat; eauto; zify; romega. +eapply valid_le_compat; eauto; lia. Qed. End Validity. @@ -417,18 +417,18 @@ Qed. Hint Extern 5 => match goal with | [ |- (Pos.max ?x ?y <= ?z)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (?z <= Pos.max ?x ?y)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (Pos.max ?x ?y < ?z)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (?z < Pos.max ?x ?y)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | _ => zify; omega -end. -Hint Resolve Pos.le_max_r Pos.le_max_l. +end : core. +Hint Resolve Pos.le_max_r Pos.le_max_l : core. -Hint Constructors valid linear. +Hint Constructors valid linear : core. (* Compatibility of validity w.r.t algebraic operations *) @@ -445,8 +445,8 @@ intros kl kr pl pr Hl Hr; revert kr pr Hr; induction Hl; intros kr pr Hr; simpl. now rewrite <- (Pos.max_id i); intuition. destruct (Pos.compare_spec i i0); subst; try case_decide; repeat (constructor; intuition). + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. - + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; zify; romega. - + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; zify; romega. + + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; lia. + + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; lia. + apply (valid_le_compat (Pos.max (Pos.succ i) i0)); intuition. + apply (valid_le_compat (Pos.max i (Pos.succ i0))); intuition. } @@ -456,7 +456,7 @@ Lemma poly_mul_cst_valid_compat : forall k v p, valid k p -> valid k (poly_mul_c Proof. intros k v p H; induction H; simpl; [now auto|]. case_decide; [|now auto]. -eapply (valid_le_compat i); [now auto|zify; romega]. +eapply (valid_le_compat i); [now auto|lia]. Qed. Lemma poly_mul_mon_null_compat : forall i p, null (poly_mul_mon i p) -> null p. diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v index 3bd7cd622c..98f5ab067a 100644 --- a/plugins/btauto/Reflect.v +++ b/plugins/btauto/Reflect.v @@ -1,4 +1,4 @@ -Require Import Bool DecidableClass Algebra Ring PArith ROmega Omega. +Require Import Bool DecidableClass Algebra Ring PArith Omega. Section Bool. @@ -77,10 +77,10 @@ intros var f; induction f; simpl poly_of_formula; simpl formula_eval; auto. end. Qed. -Hint Extern 5 => change 0 with (min 0 0). -Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat. -Local Hint Constructors valid. -Hint Extern 5 => zify; omega. +Hint Extern 5 => change 0 with (min 0 0) : core. +Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat : core. +Local Hint Constructors valid : core. +Hint Extern 5 => zify; omega : core. (* Compatibility with validity *) @@ -396,3 +396,16 @@ lazymatch goal with end | _ => fail "Cannot recognize a boolean equality" end. *) + +Register formula_var as plugins.btauto.f_var. +Register formula_btm as plugins.btauto.f_btm. +Register formula_top as plugins.btauto.f_top. +Register formula_cnj as plugins.btauto.f_cnj. +Register formula_dsj as plugins.btauto.f_dsj. +Register formula_neg as plugins.btauto.f_neg. +Register formula_xor as plugins.btauto.f_xor. +Register formula_ifb as plugins.btauto.f_ifb. + +Register formula_eval as plugins.btauto.eval. +Register boolean_witness as plugins.btauto.witness. +Register reduce_poly_of_formula_sound_alt as plugins.btauto.soundness. diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.mlg index 3ae0f45cb7..312ef1e555 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.mlg @@ -8,11 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin +} + DECLARE PLUGIN "btauto_plugin" TACTIC EXTEND btauto -| [ "btauto" ] -> [ Refl_btauto.Btauto.tac ] +| [ "btauto" ] -> { Refl_btauto.Btauto.tac } END diff --git a/plugins/btauto/plugin_base.dune b/plugins/btauto/plugin_base.dune new file mode 100644 index 0000000000..6a024358c3 --- /dev/null +++ b/plugins/btauto/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name btauto_plugin) + (public_name coq.plugins.btauto) + (synopsis "Coq's btauto plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index a09abfa193..07f50f6cd5 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -1,16 +1,16 @@ -let contrib_name = "btauto" +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) -let init_constant dir s = - let find_constant contrib dir s = - Universes.constr_of_global (Coqlib.find_reference contrib dir s) - in - find_constant contrib_name dir s +open Constr -let get_constant dir s = lazy (Universes.constr_of_global @@ Coqlib.coq_reference contrib_name dir s) - -let get_inductive dir s = - let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in - Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ())) +let bt_lib_constr n = lazy (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref n) let decomp_term sigma (c : Constr.t) = Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c))) @@ -19,27 +19,23 @@ let lapp c v = Constr.mkApp (Lazy.force c, v) let (===) = Constr.equal + module CoqList = struct - let path = ["Init"; "Datatypes"] - let typ = get_constant path "list" - let _nil = get_constant path "nil" - let _cons = get_constant path "cons" + let _nil = bt_lib_constr "core.list.nil" + let _cons = bt_lib_constr "core.list.cons" let cons ty h t = lapp _cons [|ty; h ; t|] let nil ty = lapp _nil [|ty|] let rec of_list ty = function | [] -> nil ty | t::q -> cons ty t (of_list ty q) - let type_of_list ty = lapp typ [|ty|] end module CoqPositive = struct - let path = ["Numbers"; "BinNums"] - let typ = get_constant path "positive" - let _xH = get_constant path "xH" - let _xO = get_constant path "xO" - let _xI = get_constant path "xI" + let _xH = bt_lib_constr "num.pos.xH" + let _xO = bt_lib_constr "num.pos.xO" + let _xI = bt_lib_constr "num.pos.xI" (* A coq nat from an int *) let rec of_int n = @@ -79,14 +75,14 @@ end module Bool = struct - let typ = get_constant ["Init"; "Datatypes"] "bool" - let ind = get_inductive ["Init"; "Datatypes"] "bool" - let trueb = get_constant ["Init"; "Datatypes"] "true" - let falseb = get_constant ["Init"; "Datatypes"] "false" - let andb = get_constant ["Init"; "Datatypes"] "andb" - let orb = get_constant ["Init"; "Datatypes"] "orb" - let xorb = get_constant ["Init"; "Datatypes"] "xorb" - let negb = get_constant ["Init"; "Datatypes"] "negb" + let ind = lazy (Globnames.destIndRef (Coqlib.lib_ref "core.bool.type")) + let typ = bt_lib_constr "core.bool.type" + let trueb = bt_lib_constr "core.bool.true" + let falseb = bt_lib_constr "core.bool.false" + let andb = bt_lib_constr "core.bool.andb" + let orb = bt_lib_constr "core.bool.orb" + let xorb = bt_lib_constr "core.bool.xorb" + let negb = bt_lib_constr "core.bool.negb" type t = | Var of int @@ -106,7 +102,7 @@ module Bool = struct let negb = Lazy.force negb in let rec aux c = match decomp_term sigma c with - | Term.App (head, args) -> + | App (head, args) -> if head === andb && Array.length args = 2 then Andb (aux args.(0), aux args.(1)) else if head === orb && Array.length args = 2 then @@ -116,9 +112,9 @@ module Bool = struct else if head === negb && Array.length args = 1 then Negb (aux args.(0)) else Var (Env.add env c) - | Term.Case (info, r, arg, pats) -> + | Case (info, r, arg, pats) -> let is_bool = - let i = info.Term.ci_ind in + let i = info.ci_ind in Names.eq_ind i (Lazy.force ind) in if is_bool then @@ -138,21 +134,20 @@ module Btauto = struct open Pp - let eq = get_constant ["Init"; "Logic"] "eq" - - let f_var = get_constant ["btauto"; "Reflect"] "formula_var" - let f_btm = get_constant ["btauto"; "Reflect"] "formula_btm" - let f_top = get_constant ["btauto"; "Reflect"] "formula_top" - let f_cnj = get_constant ["btauto"; "Reflect"] "formula_cnj" - let f_dsj = get_constant ["btauto"; "Reflect"] "formula_dsj" - let f_neg = get_constant ["btauto"; "Reflect"] "formula_neg" - let f_xor = get_constant ["btauto"; "Reflect"] "formula_xor" - let f_ifb = get_constant ["btauto"; "Reflect"] "formula_ifb" + let eq = bt_lib_constr "core.eq.type" - let eval = get_constant ["btauto"; "Reflect"] "formula_eval" - let witness = get_constant ["btauto"; "Reflect"] "boolean_witness" + let f_var = bt_lib_constr "plugins.btauto.f_var" + let f_btm = bt_lib_constr "plugins.btauto.f_btm" + let f_top = bt_lib_constr "plugins.btauto.f_top" + let f_cnj = bt_lib_constr "plugins.btauto.f_cnj" + let f_dsj = bt_lib_constr "plugins.btauto.f_dsj" + let f_neg = bt_lib_constr "plugins.btauto.f_neg" + let f_xor = bt_lib_constr "plugins.btauto.f_xor" + let f_ifb = bt_lib_constr "plugins.btauto.f_ifb" - let soundness = get_constant ["btauto"; "Reflect"] "reduce_poly_of_formula_sound_alt" + let eval = bt_lib_constr "plugins.btauto.eval" + let witness = bt_lib_constr "plugins.btauto.witness" + let soundness = bt_lib_constr "plugins.btauto.soundness" let rec convert = function | Bool.Var n -> lapp f_var [|CoqPositive.of_int n|] @@ -176,9 +171,9 @@ module Btauto = struct let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in let var = EConstr.Unsafe.to_constr var in let rec to_list l = match decomp_term (Tacmach.project gl) l with - | Term.App (c, _) + | App (c, _) when c === (Lazy.force CoqList._nil) -> [] - | Term.App (c, [|_; h; t|]) + | App (c, [|_; h; t|]) when c === (Lazy.force CoqList._cons) -> if h === (Lazy.force Bool.trueb) then (true :: to_list t) else if h === (Lazy.force Bool.falseb) then (false :: to_list t) @@ -212,13 +207,13 @@ module Btauto = struct Tacticals.tclFAIL 0 msg gl let try_unification env = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in let concl = EConstr.Unsafe.to_constr concl in let t = decomp_term (Tacmach.New.project gl) concl in match t with - | Term.App (c, [|typ; p; _|]) when c === eq -> + | App (c, [|typ; p; _|]) when c === eq -> (* should be an equality [@eq poly ?p (Cst false)] *) let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in tac @@ -228,7 +223,7 @@ module Btauto = struct end let tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let concl = EConstr.Unsafe.to_constr concl in let sigma = Tacmach.New.project gl in @@ -236,7 +231,7 @@ module Btauto = struct let bool = Lazy.force Bool.typ in let t = decomp_term sigma concl in match t with - | Term.App (c, [|typ; tl; tr|]) + | App (c, [|typ; tl; tr|]) when typ === bool && c === eq -> let env = Env.empty () in let fl = Bool.quote env sigma tl in diff --git a/plugins/btauto/refl_btauto.mli b/plugins/btauto/refl_btauto.mli new file mode 100644 index 0000000000..5478fddba5 --- /dev/null +++ b/plugins/btauto/refl_btauto.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +module Btauto : sig val tac : unit Proofview.tactic end |