diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-21 17:13:26 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-22 22:28:17 +0100 |
commit | 33fe6e61ff2f1f8184373ed8fccc403591c4605a (patch) | |
tree | 4c1e0602138994d92be25ba71d80da4e6f0dece0 | |
parent | f358d7b4c962f5288ad9ce2dc35802666c882422 (diff) |
Moving the Tauto tactic to proper Ltac.
This gets rid of brittle code written in ML files through Ltac quotations, and
reduces the dependance of Coq to such a feature. This also fixes the particular
instance of bug #2800, although the underlying issue is still there.
-rw-r--r-- | plugins/funind/invfun.ml | 11 | ||||
-rw-r--r-- | tactics/tauto.ml4 | 249 | ||||
-rw-r--r-- | tactics/tauto.mli | 0 | ||||
-rw-r--r-- | test-suite/bugs/closed/2800.v (renamed from test-suite/bugs/opened/2800.v) | 2 | ||||
-rw-r--r-- | theories/Init/Notations.v | 1 | ||||
-rw-r--r-- | theories/Init/Prelude.v | 1 | ||||
-rw-r--r-- | theories/Init/Tauto.v | 101 | ||||
-rw-r--r-- | theories/Init/vo.itarget | 3 | ||||
-rw-r--r-- | theories/Logic/Decidable.v | 2 |
9 files changed, 156 insertions, 214 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index cdb9c5067..6a5a5ad53 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -474,6 +474,15 @@ let generalize_dependent_of x hyp g = (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis (unfolding, substituting, destructing cases \ldots) *) +let tauto = + let dp = List.map Id.of_string ["Tauto" ; "Init"; "Coq"] in + let mp = ModPath.MPfile (DirPath.make dp) in + let kn = KerName.make2 mp (Label.make "tauto") in + Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> + let body = Tacenv.interp_ltac kn in + Tacinterp.eval_tactic body + end + let rec intros_with_rewrite g = observe_tac "intros_with_rewrite" intros_with_rewrite_aux g and intros_with_rewrite_aux : tactic = @@ -530,7 +539,7 @@ and intros_with_rewrite_aux : tactic = ] g end | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> - Proofview.V82.of_tactic Tauto.tauto g + Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENSEQ[ Proofview.V82.of_tactic (simplest_case v); diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 5485f344b..e0427ae89 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -14,6 +14,7 @@ open Names open Pp open Genarg open Stdarg +open Misctypes open Tacexpr open Tacinterp open Tactics @@ -90,6 +91,7 @@ let _ = (** Base tactics *) +let loc = Loc.ghost let idtac = Proofview.tclUNIT () let fail = Proofview.tclINDEPENDENT (tclFAIL 0 (Pp.mt ())) @@ -112,38 +114,9 @@ let split = Tactics.split_with_bindings false [Misctypes.NoBindings] (** Test *) -let make_lfun l = - let fold accu (id, v) = Id.Map.add (Id.of_string id) v accu in - List.fold_left fold Id.Map.empty l - -let register_tauto_tactic tac name = - let name = { mltac_plugin = "tauto"; mltac_tactic = name; } in - let entry = { mltac_name = name; mltac_index = 0 } in - Tacenv.register_ml_tactic name [| tac |]; - TacML (Loc.ghost, entry, []) - -let tacticIn_ist tac name = - let tac _ ist = - let avoid = Option.default [] (TacStore.get ist.extra f_avoid_ids) in - let debug = Option.default Tactic_debug.DebugOff (TacStore.get ist.extra f_debug) in - let (tac, ist) = tac ist in - interp_tac_gen ist.lfun avoid debug tac - in - register_tauto_tactic tac name - -let tacticIn tac name = - tacticIn_ist (fun ist -> tac ist, ist) name - -let push_ist ist args = - let fold accu (id, arg) = Id.Map.add (Id.of_string id) arg accu in - let lfun = List.fold_left fold ist.lfun args in - { ist with lfun = lfun } - let is_empty _ ist = if is_empty_type (assoc_var "X1" ist) then idtac else fail -let t_is_empty = register_tauto_tactic is_empty "is_empty" - (* Strictly speaking, this exceeds the propositional fragment as it matches also equality types (and solves them if a reflexivity) *) let is_unit_or_eq _ ist = @@ -151,16 +124,6 @@ let is_unit_or_eq _ ist = let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in if test (assoc_var "X1" ist) then idtac else fail -let t_is_unit_or_eq = register_tauto_tactic is_unit_or_eq "is_unit_or_eq" - -let is_record t = - let (hdapp,args) = decompose_app t in - match (kind_of_term hdapp) with - | Ind (ind,u) -> - let (mib,mip) = Global.lookup_inductive ind in - mib.Declarations.mind_record <> None - | _ -> false - let bugged_is_binary t = isApp t && let (hdapp,args) = decompose_app t in @@ -182,8 +145,6 @@ let is_conj _ ist = then idtac else fail -let t_is_conj = register_tauto_tactic is_conj "is_conj" - let flatten_contravariant_conj _ ist = let flags = assoc_flags ist in let typ = assoc_var "X1" ist in @@ -200,18 +161,8 @@ let flatten_contravariant_conj _ ist = tclTHENLIST [assert_ ~by newtyp; clear (destVar hyp)] | _ -> fail -let t_flatten_contravariant_conj = - register_tauto_tactic flatten_contravariant_conj "flatten_contravariant_conj" - (** Dealing with disjunction *) -let constructor i = - let name = { Tacexpr.mltac_plugin = "coretactics"; mltac_tactic = "constructor" } in - (** Take care of the index: this is the second entry in constructor. *) - let name = { Tacexpr.mltac_name = name; mltac_index = 1 } in - let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in - Tacexpr.TacML (Loc.ghost, name, [TacGeneric i]) - let is_disj _ ist = let flags = assoc_flags ist in let t = assoc_var "X1" ist in @@ -222,8 +173,6 @@ let is_disj _ ist = then idtac else fail -let t_is_disj = register_tauto_tactic is_disj "is_disj" - let flatten_contravariant_disj _ ist = let flags = assoc_flags ist in let typ = assoc_var "X1" ist in @@ -245,159 +194,30 @@ let flatten_contravariant_disj _ ist = tclTHEN (tclTHENLIST tacs) tac0 | _ -> fail -let t_flatten_contravariant_disj = - register_tauto_tactic flatten_contravariant_disj "flatten_contravariant_disj" - -(** Main tactic *) - -let not_dep_intros ist = - <:tactic< - repeat match goal with - | |- (forall (_: ?X1), ?X2) => intro - | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1; intro - end >> - -let t_not_dep_intros = tacticIn not_dep_intros "not_dep_intros" - -let axioms ist = - let c1 = constructor 1 in - <:tactic< - match reverse goal with - | |- ?X1 => $t_is_unit_or_eq; $c1 - | _:?X1 |- _ => $t_is_empty; elimtype X1; assumption - | _:?X1 |- ?X1 => assumption - end >> - -let t_axioms = tacticIn axioms "axioms" - -let simplif ist = - let c1 = constructor 1 in - <:tactic< - $t_not_dep_intros; - repeat - (match reverse goal with - | id: ?X1 |- _ => $t_is_conj; elim id; do 2 intro; clear id - | id: (Coq.Init.Logic.iff _ _) |- _ => elim id; do 2 intro; clear id - | id: (Coq.Init.Logic.not _) |- _ => red in id - | id: ?X1 |- _ => $t_is_disj; elim id; intro; clear id - | id0: (forall (_: ?X1), ?X2), id1: ?X1|- _ => - (* generalize (id0 id1); intro; clear id0 does not work - (see Marco Maggiesi's bug PR#301) - so we instead use Assert and exact. *) - assert X2; [exact (id0 id1) | clear id0] - | id: forall (_ : ?X1), ?X2|- _ => - $t_is_unit_or_eq; cut X2; - [ intro; clear id - | (* id : forall (_: ?X1), ?X2 |- ?X2 *) - cut X1; [exact id| $c1; fail] - ] - | id: forall (_ : ?X1), ?X2|- _ => - $t_flatten_contravariant_conj - (* moved from "id:(?A/\?B)->?X2|-" to "?A->?B->?X2|-" *) - | id: forall (_: Coq.Init.Logic.iff ?X1 ?X2), ?X3|- _ => - assert (forall (_: forall _:X1, X2), forall (_: forall _: X2, X1), X3) - by (do 2 intro; apply id; split; assumption); - clear id - | id: forall (_:?X1), ?X2|- _ => - $t_flatten_contravariant_disj - (* moved from "id:(?A\/?B)->?X2|-" to "?A->?X2,?B->?X2|-" *) - | |- ?X1 => $t_is_conj; split - | |- (Coq.Init.Logic.iff _ _) => split - | |- (Coq.Init.Logic.not _) => red - end; - $t_not_dep_intros) >> - -let t_simplif = tacticIn simplif "simplif" - -let tauto_intuit flags t_reduce solver = - let flags = Genarg.Val.Dyn (Genarg.val_tag (topwit wit_tauto_flags), flags) in - let lfun = make_lfun [("t_solver", solver); ("tauto_flags", flags)] in - let ist = { default_ist () with lfun = lfun; } in - let vars = [Id.of_string "t_solver"] in - (vars, ist, <:tactic< - let rec t_tauto_intuit := - ($t_simplif;$t_axioms - || match reverse goal with - | id:forall(_: forall (_: ?X1), ?X2), ?X3|- _ => - cut X3; - [ intro; clear id; t_tauto_intuit - | cut (forall (_: X1), X2); - [ exact id - | generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id; - solve [ t_tauto_intuit ]]] - | id:forall (_:not ?X1), ?X3|- _ => - cut X3; - [ intro; clear id; t_tauto_intuit - | cut (not X1); [ exact id | clear id; intro; solve [t_tauto_intuit ]]] - | |- ?X1 => - $t_is_disj; solve [left;t_tauto_intuit | right;t_tauto_intuit] - end - || - (* NB: [|- _ -> _] matches any product *) - match goal with | |- forall (_ : _), _ => intro; t_tauto_intuit - | |- _ => $t_reduce;t_solver - end - || - t_solver - ) in t_tauto_intuit >>) - -let reduction_not_iff _ist = - match !negation_unfolding, unfold_iff () with +let reduction_not_iff _ ist = + let avoid = Option.default [] (TacStore.get ist.extra f_avoid_ids) in + let debug = Option.default Tactic_debug.DebugOff (TacStore.get ist.extra f_debug) in + let tac = match !negation_unfolding, unfold_iff () with | true, true -> <:tactic< unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in * >> | true, false -> <:tactic< unfold Coq.Init.Logic.not in * >> | false, true -> <:tactic< unfold Coq.Init.Logic.iff in * >> | false, false -> <:tactic< idtac >> - -let t_reduction_not_iff = tacticIn reduction_not_iff "reduction_not_iff" - -let intuition_gen ist flags tac = - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let vars, ist, intuition = tauto_intuit flags t_reduction_not_iff tac in - let glb_intuition = Tacintern.glob_tactic_env vars env intuition in - eval_tactic_ist ist glb_intuition - end } - -let tauto_intuitionistic flags = - let fail = Value.of_closure (default_ist ()) <:tactic<fail>> in - Proofview.tclORELSE - (intuition_gen (default_ist ()) flags fail) - begin function (e, info) -> match e with - | Refiner.FailError _ | UserError _ -> - Tacticals.New.tclZEROMSG (str "tauto failed.") - | e -> Proofview.tclZERO ~info e - end + in + interp_tac_gen ist.lfun avoid debug tac let coq_nnpp_path = let dir = List.map Id.of_string ["Classical_Prop";"Logic";"Coq"] in Libnames.make_path (DirPath.make dir) (Id.of_string "NNPP") -let tauto_classical flags nnpp = - Proofview.tclORELSE - (Tacticals.New.tclTHEN (apply nnpp) (tauto_intuitionistic flags)) - begin function (e, info) -> match e with - | UserError _ -> Tacticals.New.tclZEROMSG (str "Classical tauto failed.") - | e -> Proofview.tclZERO ~info e - end - -let tauto_gen flags = - (* spiwack: I use [tclBIND (tclUNIT ())] as a way to delay the effect - (in [constr_of_global]) to the application of the tactic. *) +let apply_nnpp _ ist = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> try let nnpp = Universes.constr_of_global (Nametab.global_of_path coq_nnpp_path) in - (* try intuitionistic version first to avoid an axiom if possible *) - Tacticals.New.tclORELSE (tauto_intuitionistic flags) (tauto_classical flags nnpp) - with Not_found -> - tauto_intuitionistic flags + apply nnpp + with Not_found -> tclFAIL 0 (Pp.mt ()) end -let default_intuition_tac = - let tac _ _ = Auto.h_auto None [] None in - let tac = register_tauto_tactic tac "auto_with" in - Value.of_closure (default_ist ()) tac - (* This is the uniform mode dealing with ->, not, iff and types isomorphic to /\ and *, \/ and +, False and Empty_set, True and unit, _and_ eq-like types. For the moment not and iff are still always unfolded. *) @@ -427,23 +247,34 @@ let tauto_power_flags = { strict_unit = false } -let tauto = tauto_gen tauto_uniform_unit_flags -let dtauto = tauto_gen tauto_power_flags - -TACTIC EXTEND tauto -| [ "tauto" ] -> [ tauto ] -END - -TACTIC EXTEND dtauto -| [ "dtauto" ] -> [ dtauto ] +let with_flags flags ist tac = + let f = (loc, Id.of_string "f") in + let x = (loc, Id.of_string "x") in + let arg = Val.Dyn (val_tag (topwit wit_tauto_flags), flags) in + let ist = { ist with lfun = Id.Map.add (snd f) tac (Id.Map.add (snd x) arg ist.lfun) } in + eval_tactic_ist ist (TacArg (loc, TacCall (loc, ArgVar f, [Reference (ArgVar x)]))) + +TACTIC EXTEND with_flags +| [ "with_uniform_flags" tactic(tac) ] -> [ with_flags tauto_uniform_unit_flags ist tac ] +| [ "with_legacy_flags" tactic(tac) ] -> [ with_flags tauto_legacy_flags ist tac ] +| [ "with_power_flags" tactic(tac) ] -> [ with_flags tauto_power_flags ist tac ] END -TACTIC EXTEND intuition -| [ "intuition" ] -> [ intuition_gen ist tauto_uniform_unit_flags default_intuition_tac ] -| [ "intuition" tactic(t) ] -> [ intuition_gen ist tauto_uniform_unit_flags t ] -END - -TACTIC EXTEND dintuition -| [ "dintuition" ] -> [ intuition_gen ist tauto_power_flags default_intuition_tac ] -| [ "dintuition" tactic(t) ] -> [ intuition_gen ist tauto_power_flags t ] -END +let register_tauto_tactic_ tac name0 args = + let ids = List.map (fun id -> Id.of_string id) args in + let ids = List.map (fun id -> Some id) ids in + let name = { mltac_plugin = "tauto"; mltac_tactic = name0 ^ "_"; } in + let entry = { mltac_name = name; mltac_index = 0 } in + let () = Tacenv.register_ml_tactic name [| tac |] in + let tac = TacFun (ids, TacML (loc, entry, [])) in + let obj () = Tacenv.register_ltac true true (Id.of_string name0) tac in + Mltop.declare_cache_obj obj "tauto" + +let () = register_tauto_tactic_ is_empty "is_empty" ["tauto_flags"; "X1"] +let () = register_tauto_tactic_ is_unit_or_eq "is_unit_or_eq" ["tauto_flags"; "X1"] +let () = register_tauto_tactic_ is_disj "is_disj" ["tauto_flags"; "X1"] +let () = register_tauto_tactic_ is_conj "is_conj" ["tauto_flags"; "X1"] +let () = register_tauto_tactic_ flatten_contravariant_disj "flatten_contravariant_disj" ["tauto_flags"; "X1"; "X2"; "id"] +let () = register_tauto_tactic_ flatten_contravariant_conj "flatten_contravariant_conj" ["tauto_flags"; "X1"; "X2"; "id"] +let () = register_tauto_tactic_ apply_nnpp "apply_nnpp" [] +let () = register_tauto_tactic_ reduction_not_iff "reduction_not_iff" [] diff --git a/tactics/tauto.mli b/tactics/tauto.mli new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/tactics/tauto.mli diff --git a/test-suite/bugs/opened/2800.v b/test-suite/bugs/closed/2800.v index c559ab0c1..2ee438934 100644 --- a/test-suite/bugs/opened/2800.v +++ b/test-suite/bugs/closed/2800.v @@ -1,6 +1,6 @@ Goal False. -Fail intuition +intuition match goal with | |- _ => idtac " foo" end. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index e1ddaeaef..55eb699be 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -90,4 +90,3 @@ Declare ML Module "eauto". Declare ML Module "g_class". Declare ML Module "g_eqdecide". Declare ML Module "g_rewrite". -Declare ML Module "tauto". diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 04a263ad9..03f2328de 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -15,6 +15,7 @@ Require Coq.Init.Nat. Require Export Peano. Require Export Coq.Init.Wf. Require Export Coq.Init.Tactics. +Require Export Coq.Init.Tauto. (* Initially available plugins (+ nat_syntax_plugin loaded in Datatypes) *) Declare ML Module "extraction_plugin". diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v new file mode 100644 index 000000000..e0949eb73 --- /dev/null +++ b/theories/Init/Tauto.v @@ -0,0 +1,101 @@ +Require Import Notations. +Require Import Datatypes. +Require Import Logic. + +Local Declare ML Module "tauto". + +Local Ltac not_dep_intros := + repeat match goal with + | |- (forall (_: ?X1), ?X2) => intro + | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1; intro + end. + +Local Ltac axioms flags := + match reverse goal with + | |- ?X1 => is_unit_or_eq flags X1; constructor 1 + | _:?X1 |- _ => is_empty flags X1; elimtype X1; assumption + | _:?X1 |- ?X1 => assumption + end. + +Local Ltac simplif flags := + not_dep_intros; + repeat + (match reverse goal with + | id: ?X1 |- _ => is_conj flags X1; elim id; do 2 intro; clear id + | id: (Coq.Init.Logic.iff _ _) |- _ => elim id; do 2 intro; clear id + | id: (Coq.Init.Logic.not _) |- _ => red in id + | id: ?X1 |- _ => is_disj flags X1; elim id; intro; clear id + | id0: (forall (_: ?X1), ?X2), id1: ?X1|- _ => + (* generalize (id0 id1); intro; clear id0 does not work + (see Marco Maggiesi's bug PR#301) + so we instead use Assert and exact. *) + assert X2; [exact (id0 id1) | clear id0] + | id: forall (_ : ?X1), ?X2|- _ => + is_unit_or_eq flags X1; cut X2; + [ intro; clear id + | (* id : forall (_: ?X1), ?X2 |- ?X2 *) + cut X1; [exact id| constructor 1; fail] + ] + | id: forall (_ : ?X1), ?X2|- _ => + flatten_contravariant_conj flags X1 X2 id + (* moved from "id:(?A/\?B)->?X2|-" to "?A->?B->?X2|-" *) + | id: forall (_: Coq.Init.Logic.iff ?X1 ?X2), ?X3|- _ => + assert (forall (_: forall _:X1, X2), forall (_: forall _: X2, X1), X3) + by (do 2 intro; apply id; split; assumption); + clear id + | id: forall (_:?X1), ?X2|- _ => + flatten_contravariant_disj flags X1 X2 id + (* moved from "id:(?A\/?B)->?X2|-" to "?A->?X2,?B->?X2|-" *) + | |- ?X1 => is_conj flags X1; split + | |- (Coq.Init.Logic.iff _ _) => split + | |- (Coq.Init.Logic.not _) => red + end; + not_dep_intros). + +Local Ltac tauto_intuit flags t_reduce t_solver := + let rec t_tauto_intuit := + (simplif flags; axioms flags + || match reverse goal with + | id:forall(_: forall (_: ?X1), ?X2), ?X3|- _ => + cut X3; + [ intro; clear id; t_tauto_intuit + | cut (forall (_: X1), X2); + [ exact id + | generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id; + solve [ t_tauto_intuit ]]] + | id:forall (_:not ?X1), ?X3|- _ => + cut X3; + [ intro; clear id; t_tauto_intuit + | cut (not X1); [ exact id | clear id; intro; solve [t_tauto_intuit ]]] + | |- ?X1 => + is_disj flags X1; solve [left;t_tauto_intuit | right;t_tauto_intuit] + end + || + (* NB: [|- _ -> _] matches any product *) + match goal with | |- forall (_ : _), _ => intro; t_tauto_intuit + | |- _ => t_reduce;t_solver + end + || + t_solver + ) in t_tauto_intuit. + +Local Ltac intuition_gen flags solver := tauto_intuit flags reduction_not_iff solver. +Local Ltac tauto_intuitionistic flags := intuition_gen flags fail || fail "tauto failed". +Local Ltac tauto_classical flags := + (apply_nnpp || fail "tauto failed"); (tauto_intuitionistic flags || fail "Classical tauto failed"). +Local Ltac tauto_gen flags := tauto_intuitionistic flags || tauto_classical flags. + +Ltac tauto := with_uniform_flags (fun flags => tauto_gen flags). +Ltac dtauto := with_power_flags (fun flags => tauto_gen flags). + +Ltac intuition := with_uniform_flags (fun flags => intuition_gen flags ltac:(auto with *)). +Local Ltac intuition_then tac := with_uniform_flags (fun flags => intuition_gen flags tac). + +Ltac dintuition := with_power_flags (fun flags => intuition_gen flags ltac:(auto with *)). +Local Ltac dintuition_then tac := with_power_flags (fun flags => intuition_gen flags tac). + +Tactic Notation "intuition" := intuition. +Tactic Notation "intuition" tactic(t) := intuition_then t. + +Tactic Notation "dintuition" := dintuition. +Tactic Notation "dintuition" tactic(t) := dintuition_then t. diff --git a/theories/Init/vo.itarget b/theories/Init/vo.itarget index cc62e66cc..99877065e 100644 --- a/theories/Init/vo.itarget +++ b/theories/Init/vo.itarget @@ -7,4 +7,5 @@ Prelude.vo Specif.vo Tactics.vo Wf.vo -Nat.vo
\ No newline at end of file +Nat.vo +Tauto.vo diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index 2ba7253c4..8b6054f9d 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -50,7 +50,7 @@ Qed. Theorem dec_iff : forall A B:Prop, decidable A -> decidable B -> decidable (A<->B). Proof. -unfold decidable; tauto. +unfold decidable. tauto. Qed. Theorem not_not : forall P:Prop, decidable P -> ~ ~ P -> P. |