summaryrefslogtreecommitdiff
path: root/tactics/tauto.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tauto.ml4')
-rw-r--r--tactics/tauto.ml4356
1 files changed, 225 insertions, 131 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 042e2a7d..4b03ff24 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -1,48 +1,58 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4deps: "grammar/grammar.cma" i*)
open Term
open Hipattern
open Names
-open Libnames
open Pp
-open Proof_type
-open Tacticals
+open Genarg
+open Stdarg
open Tacinterp
open Tactics
+open Errors
open Util
-open Genarg
+
+DECLARE PLUGIN "tauto"
let assoc_var s ist =
- match List.assoc (Names.id_of_string s) ist.lfun with
- | VConstr ([],c) -> c
- | _ -> failwith "tauto: anomaly"
+ let v = Id.Map.find (Names.Id.of_string s) ist.lfun in
+ match Value.to_constr v with
+ | Some c -> c
+ | None -> failwith "tauto: anomaly"
(** Parametrization of tauto *)
+type tauto_flags = {
+
(* Whether conjunction and disjunction are restricted to binary connectives *)
-(* (this is the compatibility mode) *)
-let binary_mode = true
+ binary_mode : bool;
+
+(* Whether compatibility for buggy detection of binary connective is on *)
+ binary_mode_bugged_detection : bool;
(* Whether conjunction and disjunction are restricted to the connectives *)
(* having the structure of "and" and "or" (up to the choice of sorts) in *)
-(* contravariant position in an hypothesis (this is the compatibility mode) *)
-let strict_in_contravariant_hyp = true
+(* contravariant position in an hypothesis *)
+ strict_in_contravariant_hyp : bool;
(* Whether conjunction and disjunction are restricted to the connectives *)
(* having the structure of "and" and "or" (up to the choice of sorts) in *)
(* an hypothesis and in the conclusion *)
-let strict_in_hyp_and_ccl = false
+ strict_in_hyp_and_ccl : bool;
(* Whether unit type includes equality types *)
-let strict_unit = false
+ strict_unit : bool;
+}
+
+(* Whether inner not are unfolded *)
+let negation_unfolding = ref true
(* Whether inner iff are unfolded *)
let iff_unfolding = ref false
@@ -54,13 +64,26 @@ let _ =
declare_bool_option
{ optsync = true;
optdepr = false;
- optname = "unfolding of iff and not in intuition";
+ optname = "unfolding of not in intuition";
+ optkey = ["Intuition";"Negation";"Unfolding"];
+ optread = (fun () -> !negation_unfolding);
+ optwrite = (:=) negation_unfolding }
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "unfolding of iff in intuition";
optkey = ["Intuition";"Iff";"Unfolding"];
optread = (fun () -> !iff_unfolding);
optwrite = (:=) iff_unfolding }
(** 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 is_empty ist =
if is_empty_type (assoc_var "X1" ist) then
<:tactic<idtac>>
@@ -69,8 +92,8 @@ let is_empty ist =
(* 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 =
- let test = if strict_unit then is_unit_type else is_unit_or_eq_type in
+let is_unit_or_eq flags 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
<:tactic<idtac>>
else
@@ -79,18 +102,18 @@ let is_unit_or_eq ist =
let is_record t =
let (hdapp,args) = decompose_app t in
match (kind_of_term hdapp) with
- | Ind ind ->
+ | Ind (ind,u) ->
let (mib,mip) = Global.lookup_inductive ind in
- mib.Declarations.mind_record
+ mib.Declarations.mind_record <> None
| _ -> false
-let is_binary t =
+let bugged_is_binary t =
isApp t &&
let (hdapp,args) = decompose_app t in
match (kind_of_term hdapp) with
- | Ind ind ->
+ | Ind (ind,u) ->
let (mib,mip) = Global.lookup_inductive ind in
- mib.Declarations.mind_nparams = 2
+ Int.equal mib.Declarations.mind_nparams 2
| _ -> false
let iter_tac tacl =
@@ -98,70 +121,76 @@ let iter_tac tacl =
(** Dealing with conjunction *)
-let is_conj ist =
+let is_conj flags ist =
let ind = assoc_var "X1" ist in
- if (not binary_mode || is_binary ind) (* && not (is_record ind) *)
- && is_conjunction ~strict:strict_in_hyp_and_ccl ind
+ if (not flags.binary_mode_bugged_detection || bugged_is_binary ind) &&
+ is_conjunction
+ ~strict:flags.strict_in_hyp_and_ccl
+ ~onlybinary:flags.binary_mode ind
then
<:tactic<idtac>>
else
<:tactic<fail>>
-let flatten_contravariant_conj ist =
+let flatten_contravariant_conj flags ist =
let typ = assoc_var "X1" ist in
let c = assoc_var "X2" ist in
let hyp = assoc_var "id" ist in
- match match_with_conjunction ~strict:strict_in_contravariant_hyp typ with
+ match match_with_conjunction
+ ~strict:flags.strict_in_contravariant_hyp
+ ~onlybinary:flags.binary_mode typ
+ with
| Some (_,args) ->
- let i = List.length args in
- if not binary_mode || i = 2 then
- let newtyp = valueIn (VConstr ([],List.fold_right mkArrow args c)) in
- let hyp = valueIn (VConstr ([],hyp)) in
- let intros =
- iter_tac (List.map (fun _ -> <:tactic< intro >>) args)
- <:tactic< idtac >> in
- <:tactic<
- let newtyp := $newtyp in
- let hyp := $hyp in
- assert newtyp by ($intros; apply hyp; split; assumption);
- clear hyp
- >>
- else
- <:tactic<fail>>
+ let newtyp = valueIn (Value.of_constr (List.fold_right mkArrow args c)) in
+ let hyp = valueIn (Value.of_constr hyp) in
+ let intros =
+ iter_tac (List.map (fun _ -> <:tactic< intro >>) args)
+ <:tactic< idtac >> in
+ <:tactic<
+ let newtyp := $newtyp in
+ let hyp := $hyp in
+ assert newtyp by ($intros; apply hyp; split; assumption);
+ clear hyp
+ >>
| _ ->
<:tactic<fail>>
(** Dealing with disjunction *)
-let is_disj ist =
+let constructor i =
+ let name = { Tacexpr.mltac_plugin = "coretactics"; mltac_tactic = "constructor" } in
+ let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in
+ Tacexpr.TacML (Loc.ghost, name, [i])
+
+let is_disj flags ist =
let t = assoc_var "X1" ist in
- if (not binary_mode || is_binary t) &&
- is_disjunction ~strict:strict_in_hyp_and_ccl t
+ if (not flags.binary_mode_bugged_detection || bugged_is_binary t) &&
+ is_disjunction
+ ~strict:flags.strict_in_hyp_and_ccl
+ ~onlybinary:flags.binary_mode t
then
<:tactic<idtac>>
else
<:tactic<fail>>
-let flatten_contravariant_disj ist =
+let flatten_contravariant_disj flags ist =
let typ = assoc_var "X1" ist in
let c = assoc_var "X2" ist in
let hyp = assoc_var "id" ist in
- match match_with_disjunction ~strict:strict_in_contravariant_hyp typ with
+ match match_with_disjunction
+ ~strict:flags.strict_in_contravariant_hyp
+ ~onlybinary:flags.binary_mode
+ typ with
| Some (_,args) ->
- let i = List.length args in
- if not binary_mode || i = 2 then
- let hyp = valueIn (VConstr ([],hyp)) in
- iter_tac (list_map_i (fun i arg ->
- let typ = valueIn (VConstr ([],mkArrow arg c)) in
- let i = Tacexpr.Integer i in
- <:tactic<
- let typ := $typ in
- let hyp := $hyp in
- let i := $i in
- assert typ by (intro; apply hyp; constructor i; assumption)
- >>) 1 args) <:tactic< let hyp := $hyp in clear hyp >>
- else
- <:tactic<fail>>
+ let hyp = valueIn (Value.of_constr hyp) in
+ iter_tac (List.map_i (fun i arg ->
+ let typ = valueIn (Value.of_constr (mkArrow arg c)) in
+ let ci = constructor i in
+ <:tactic<
+ let typ := $typ in
+ let hyp := $hyp in
+ assert typ by (intro; apply hyp; $ci; assumption)
+ >>) 1 args) <:tactic< let hyp := $hyp in clear hyp >>
| _ ->
<:tactic<fail>>
@@ -171,30 +200,30 @@ let flatten_contravariant_disj ist =
let not_dep_intros ist =
<:tactic<
repeat match goal with
- | |- (?X1 -> ?X2) => intro
- | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1
- | H:(Coq.Init.Logic.not _)|-_ => unfold Coq.Init.Logic.not at 1 in H
- | H:(Coq.Init.Logic.not _)->_|-_ => unfold Coq.Init.Logic.not at 1 in H
+ | |- (forall (_: ?X1), ?X2) => intro
+ | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1; intro
end >>
-let axioms ist =
- let t_is_unit_or_eq = tacticIn is_unit_or_eq
+let axioms flags ist =
+ let t_is_unit_or_eq = tacticIn (is_unit_or_eq flags)
and t_is_empty = tacticIn is_empty in
+ let c1 = constructor 1 in
<:tactic<
match reverse goal with
- | |- ?X1 => $t_is_unit_or_eq; constructor 1
+ | |- ?X1 => $t_is_unit_or_eq; $c1
| _:?X1 |- _ => $t_is_empty; elimtype X1; assumption
| _:?X1 |- ?X1 => assumption
end >>
-let simplif ist =
- let t_is_unit_or_eq = tacticIn is_unit_or_eq
- and t_is_conj = tacticIn is_conj
- and t_flatten_contravariant_conj = tacticIn flatten_contravariant_conj
- and t_flatten_contravariant_disj = tacticIn flatten_contravariant_disj
- and t_is_disj = tacticIn is_disj
+let simplif flags ist =
+ let t_is_unit_or_eq = tacticIn (is_unit_or_eq flags)
+ and t_is_conj = tacticIn (is_conj flags)
+ and t_flatten_contravariant_conj = tacticIn (flatten_contravariant_conj flags)
+ and t_flatten_contravariant_disj = tacticIn (flatten_contravariant_disj flags)
+ and t_is_disj = tacticIn (is_disj flags)
and t_not_dep_intros = tacticIn not_dep_intros in
+ let c1 = constructor 1 in
<:tactic<
$t_not_dep_intros;
repeat
@@ -203,25 +232,25 @@ let simplif ist =
| 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: ?X1 -> ?X2, id1: ?X1|- _ =>
+ | 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: ?X1 -> ?X2|- _ =>
+ | id: forall (_ : ?X1), ?X2|- _ =>
$t_is_unit_or_eq; cut X2;
[ intro; clear id
- | (* id : ?X1 -> ?X2 |- ?X2 *)
- cut X1; [exact id| constructor 1; fail]
+ | (* id : forall (_: ?X1), ?X2 |- ?X2 *)
+ cut X1; [exact id| $c1; fail]
]
- | id: ?X1 -> ?X2|- _ =>
+ | id: forall (_ : ?X1), ?X2|- _ =>
$t_flatten_contravariant_conj
(* moved from "id:(?A/\?B)->?X2|-" to "?A->?B->?X2|-" *)
- | id: (Coq.Init.Logic.iff ?X1 ?X2) -> ?X3|- _ =>
- assert ((X1 -> X2) -> (X2 -> X1) -> X3)
+ | 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: ?X1 -> ?X2|- _ =>
+ | id: forall (_:?X1), ?X2|- _ =>
$t_flatten_contravariant_disj
(* moved from "id:(?A\/?B)->?X2|-" to "?A->?X2,?B->?X2|-" *)
| |- ?X1 => $t_is_conj; split
@@ -230,75 +259,140 @@ let simplif ist =
end;
$t_not_dep_intros) >>
-let rec tauto_intuit t_reduce solver ist =
- let t_axioms = tacticIn axioms
- and t_simplif = tacticIn simplif
- and t_is_disj = tacticIn is_disj
- and t_tauto_intuit = tacticIn (tauto_intuit t_reduce solver) in
- let t_solver = globTacticIn (fun _ist -> solver) in
- <:tactic<
+let rec tauto_intuit flags t_reduce solver =
+ let t_axioms = tacticIn (axioms flags)
+ and t_simplif = tacticIn (simplif flags)
+ and t_is_disj = tacticIn (is_disj flags) in
+ let lfun = make_lfun [("t_solver", solver)] 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:(?X1 -> ?X2)-> ?X3|- _ =>
+ | id:forall(_: forall (_: ?X1), ?X2), ?X3|- _ =>
cut X3;
- [ intro; clear id; $t_tauto_intuit
- | cut (X1 -> X2);
+ [ 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 ]]]
+ 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]
+ $t_is_disj; solve [left;t_tauto_intuit | right;t_tauto_intuit]
end
||
(* NB: [|- _ -> _] matches any product *)
- match goal with | |- _ -> _ => intro; $t_tauto_intuit
- | |- _ => $t_reduce;$t_solver
+ match goal with | |- forall (_ : _), _ => intro; t_tauto_intuit
+ | |- _ => $t_reduce;t_solver
end
||
- $t_solver
- ) >>
-
-let reduction_not _ist =
- if unfold_iff () then
- <:tactic< unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in * >>
- else
- <:tactic< unfold Coq.Init.Logic.not in * >>
-
-let t_reduction_not = tacticIn reduction_not
-
-let intuition_gen tac =
- interp (tacticIn (tauto_intuit t_reduction_not tac))
-
-let tauto_intuitionistic g =
- try intuition_gen <:tactic<fail>> g
- with
- Refiner.FailError _ | UserError _ ->
- errorlabstrm "tauto" (str "tauto failed.")
+ t_solver
+ ) in t_tauto_intuit >>)
+
+let reduction_not_iff _ist =
+ 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
+
+let intuition_gen ist flags tac =
+ Proofview.Goal.enter begin fun gl ->
+ let tac = Value.of_closure ist tac in
+ 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 =
+ Proofview.tclORELSE
+ (intuition_gen (default_ist ()) flags <:tactic<fail>>)
+ begin function (e, info) -> match e with
+ | Refiner.FailError _ | UserError _ ->
+ Proofview.tclZERO (UserError ("tauto" , str "tauto failed."))
+ | e -> Proofview.tclZERO ~info e
+ end
let coq_nnpp_path =
- let dir = List.map id_of_string ["Classical_Prop";"Logic";"Coq"] in
- Libnames.make_path (make_dirpath dir) (id_of_string "NNPP")
-
-let tauto_classical nnpp g =
- try tclTHEN (apply nnpp) tauto_intuitionistic g
- with UserError _ -> errorlabstrm "tauto" (str "Classical tauto failed.")
+ 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 _ -> Proofview.tclZERO (UserError ("tauto" , str "Classical tauto failed."))
+ | e -> Proofview.tclZERO ~info e
+ end
-let tauto g =
- try
- let nnpp = constr_of_global (Nametab.global_of_path coq_nnpp_path) in
+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. *)
+ 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 *)
- tclORELSE tauto_intuitionistic (tauto_classical nnpp) g
- with Not_found ->
- tauto_intuitionistic g
-
+ Tacticals.New.tclORELSE (tauto_intuitionistic flags) (tauto_classical flags nnpp)
+ with Not_found ->
+ tauto_intuitionistic flags
+ end
let default_intuition_tac = <:tactic< auto with * >>
+(* 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. *)
+let tauto_uniform_unit_flags = {
+ binary_mode = true;
+ binary_mode_bugged_detection = false;
+ strict_in_contravariant_hyp = true;
+ strict_in_hyp_and_ccl = true;
+ strict_unit = false
+}
+
+(* This is the compatibility mode (not used) *)
+let tauto_legacy_flags = {
+ binary_mode = true;
+ binary_mode_bugged_detection = true;
+ strict_in_contravariant_hyp = true;
+ strict_in_hyp_and_ccl = false;
+ strict_unit = false
+}
+
+(* This is the improved mode *)
+let tauto_power_flags = {
+ binary_mode = false; (* support n-ary connectives *)
+ binary_mode_bugged_detection = false;
+ strict_in_contravariant_hyp = false; (* supports non-regular connectives *)
+ strict_in_hyp_and_ccl = false;
+ 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 ]
+END
+
TACTIC EXTEND intuition
-| [ "intuition" ] -> [ intuition_gen default_intuition_tac ]
-| [ "intuition" tactic(t) ] -> [ intuition_gen t ]
+| [ "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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 02:43:53 +0000