aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/g_tactic.ml44
-rw-r--r--parsing/pptactic.ml4
-rw-r--r--proofs/tacexpr.ml1
-rw-r--r--tactics/auto.ml76
-rw-r--r--tactics/auto.mli11
-rw-r--r--tactics/tacinterp.ml7
-rw-r--r--test-suite/complexity/autodecomp.v11
-rw-r--r--theories/Arith/Div2.v26
-rw-r--r--theories/Logic/ChoiceFacts.v12
9 files changed, 26 insertions, 126 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index ddff97128..79783fd3f 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -610,10 +610,6 @@ GEXTEND Gram
| d = trivial; lems = auto_using; db = hintbases -> TacTrivial (d,lems,db)
| d = auto; n = OPT int_or_var; lems = auto_using; db = hintbases ->
TacAuto (d,n,lems,db)
- | d = auto; IDENT "decomp"; p = OPT natural; lems = auto_using ->
- TacDAuto (d,None,p,lems)
- | d = auto; n = OPT int_or_var; IDENT "decomp"; p = OPT natural;
- lems = auto_using -> TacDAuto (d,n,p,lems)
(* Context management *)
| IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index c4c8579d9..513034194 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -748,10 +748,6 @@ and pr_atom1 = function
hov 0 (str (string_of_debug d ^ "auto") ++
pr_opt (pr_or_var int) n ++
pr_auto_using pr_constr lems ++ pr_hintbases db)
- | TacDAuto (d,n,p,lems) ->
- hov 1 (str (string_of_debug d ^ "auto") ++
- pr_opt (pr_or_var int) n ++ str "decomp" ++
- pr_opt int p ++ pr_auto_using pr_constr lems)
(* Context management *)
| TacClear (true,[]) as t -> pr_atom0 t
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index cec6fd419..b48605657 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -177,7 +177,6 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
(* Automation tactics *)
| TacTrivial of debug * 'constr list * string list option
| TacAuto of debug * int or_var option * 'constr list * string list option
- | TacDAuto of debug * int or_var option * int option * 'constr list
(* Context management *)
| TacClear of bool * 'id list
diff --git a/tactics/auto.ml b/tactics/auto.ml
index cedec80a1..8b4f5eb61 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1405,51 +1405,23 @@ let decomp_empty_term dbg (id,_,typc) gl =
let extend_local_db gl decl db =
Hint_db.add_list (make_resolve_hyp (pf_env gl) (project gl) decl) db
-(* Try to decompose hypothesis [decl] into atomic components of a
- conjunction with maximum depth [p] (or solve the goal from an
- empty type) then call the continuation tactic with hint db extended
- with the obtained not-further-decomposable hypotheses *)
-
-let rec decomp_and_register_decl dbg p kont (id,_,_ as decl) db gl =
- if p = 0 then
- kont (extend_local_db gl decl db) gl
- else
- tclORELSE0
- (decomp_empty_term dbg decl)
- (decomp_unary_term_then dbg decl (intros_decomp dbg (p-1) kont [] db)
- (kont (extend_local_db gl decl db))) gl
-
-(* Introduce [n] hypotheses, then decompose then with maximum depth [p] and
- call the continuation tactic [kont] with the hint db extended
- with the so-obtained not-further-decomposable hypotheses *)
-
-and intros_decomp dbg p kont decls db n =
- if n = 0 then
- decomp_and_register_decls dbg p kont decls db
- else
- tclTHEN (dbg_intro dbg) (onLastDecl (fun d ->
- (intros_decomp dbg p kont (d::decls) db (n-1))))
-
-(* Decompose hypotheses [hyps] with maximum depth [p] and
- call the continuation tactic [kont] with the hint db extended
- with the so-obtained not-further-decomposable hypotheses *)
-
-and decomp_and_register_decls dbg p kont decls =
- List.fold_left (decomp_and_register_decl dbg p) kont decls
+(* Introduce an hypothesis, then call the continuation tactic [kont]
+ with the hint db extended with the so-obtained hypothesis *)
+let intro_register dbg kont db =
+ tclTHEN (dbg_intro dbg)
+ (onLastDecl (fun decl gl -> kont (extend_local_db gl decl db) gl))
-(* decomp is an natural number giving an indication on decomposition
- of conjunction in hypotheses, 0 corresponds to no decomposition *)
(* n is the max depth of search *)
(* local_db contains the local Hypotheses *)
exception Uplift of tactic list
-let search_gen d p n mod_delta db_list local_db =
+let search d n mod_delta db_list local_db =
let rec search d n local_db =
if n=0 then (fun gl -> error "BOUND 2") else
tclORELSE0 (dbg_assumption d)
- (tclORELSE0 (intros_decomp d p (search d n) [] local_db 1)
+ (tclORELSE0 (intro_register d (search d n) local_db)
(fun gl ->
let d' = incr_dbg d in
tclFIRST
@@ -1459,8 +1431,6 @@ let search_gen d p n mod_delta db_list local_db =
in
search d n local_db
-let search dbg = search_gen dbg 0
-
let default_search_depth = ref 5
let delta_auto ?(debug=Off) mod_delta n lems dbnames gl =
@@ -1499,35 +1469,3 @@ let inj_or_var = Option.map (fun n -> ArgArg n)
let h_auto ?(debug=Off) n lems l =
Refiner.abstract_tactic (TacAuto (debug,inj_or_var n,List.map snd lems,l))
(gen_auto ~debug n lems l)
-
-(**************************************************************************)
-(* The "destructing Auto" from Eduardo *)
-(**************************************************************************)
-
-(* Depth of search after decomposition of hypothesis, by default
- one look for an immediate solution *)
-let default_search_decomp = ref 20
-
-let destruct_auto d p lems n gl =
- decomp_and_register_decls d p (fun local_db gl ->
- search_gen d p n false (List.map searchtable_map ["core";"extcore"])
- (add_hint_lemmas false lems local_db gl) gl)
- (pf_hyps gl)
- (Hint_db.empty empty_transparent_state false)
- gl
-
-let dautomatic ?(debug=Off) des_opt lems n =
- let d = mk_auto_dbg debug in
- tclTRY_dbg d (destruct_auto d des_opt lems n)
-
-let dauto ?(debug=Off) (n,p) lems =
- let p = match p with Some p -> p | None -> !default_search_decomp in
- let n = match n with Some n -> n | None -> !default_search_depth in
- dautomatic ~debug p lems n
-
-let default_dauto = dauto (None,None) []
-
-let h_dauto ?(debug=Off) (n,p) lems =
- Refiner.abstract_tactic
- (TacDAuto (debug,inj_or_var n,p,List.map snd lems))
- (dauto ~debug (n,p) lems)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 69a526e5a..49a7ef305 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -264,17 +264,6 @@ val h_trivial : ?debug:Tacexpr.debug ->
val pr_autotactic : 'a auto_tactic -> Pp.std_ppcmds
-(** Destructing Auto *)
-
-(** DAuto *)
-val dauto : ?debug:Tacexpr.debug ->
- int option * int option -> open_constr list -> tactic
-val default_search_decomp : int ref
-val default_dauto : tactic
-
-val h_dauto : ?debug:Tacexpr.debug ->
- int option * int option -> open_constr list -> tactic
-
(** Hook for changing the initialization of auto *)
val add_auto_init : (unit -> unit) -> unit
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index db6a45e1e..1dc0f6589 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -718,9 +718,6 @@ let rec intern_atomic lf ist x =
| TacAuto (d,n,lems,l) ->
TacAuto (d,Option.map (intern_or_var ist) n,
List.map (intern_constr ist) lems,l)
- | TacDAuto (d,n,p,lems) ->
- TacDAuto (d,Option.map (intern_or_var ist) n,p,
- List.map (intern_constr ist) lems)
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) ->
@@ -2413,9 +2410,6 @@ and interp_atomic ist gl tac =
Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n)
(interp_auto_lemmas ist env sigma lems)
(Option.map (List.map (interp_hint_base ist)) l)
- | TacDAuto (debug,n,p,lems) ->
- Auto.h_dauto ~debug (Option.map (interp_int_or_var ist) n,p)
- (interp_auto_lemmas ist env sigma lems)
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) ->
@@ -2855,7 +2849,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* Automation tactics *)
| TacTrivial (d,lems,l) -> TacTrivial (d,List.map (subst_glob_constr subst) lems,l)
| TacAuto (d,n,lems,l) -> TacAuto (d,n,List.map (subst_glob_constr subst) lems,l)
- | TacDAuto (d,n,p,lems) -> TacDAuto (d,n,p,List.map (subst_glob_constr subst) lems)
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) as x -> x
diff --git a/test-suite/complexity/autodecomp.v b/test-suite/complexity/autodecomp.v
deleted file mode 100644
index 85589ff79..000000000
--- a/test-suite/complexity/autodecomp.v
+++ /dev/null
@@ -1,11 +0,0 @@
-(* This example used to be in (at least) exponential time in the number of
- conjunctive types in the hypotheses before revision 11713 *)
-(* Expected time < 1.50s *)
-
-Goal
-True/\True->
-True/\True->
-True/\True->
-False/\False.
-
-Timeout 5 Time auto decomp.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 24cbc3f93..da1d9e989 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -11,7 +11,7 @@ Require Import Plus.
Require Import Compare_dec.
Require Import Even.
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
Implicit Type n : nat.
@@ -69,24 +69,24 @@ Proof.
(* S n *) inversion_clear H. apply even_div2 in H0 as <-. trivial.
Qed.
-Lemma div2_even : forall n, div2 n = div2 (S n) -> even n
-with div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n.
+Lemma div2_even n : div2 n = div2 (S n) -> even n
+with div2_odd n : S (div2 n) = div2 (S n) -> odd n.
Proof.
- destruct n; intro H.
- (* 0 *) constructor.
- (* S n *) constructor. apply div2_odd. rewrite H. trivial.
- destruct n; intro H.
- (* 0 *) discriminate.
- (* S n *) constructor. apply div2_even. injection H as <-. trivial.
+{ destruct n; intro H.
+ - constructor.
+ - constructor. apply div2_odd. rewrite H. trivial. }
+{ destruct n; intro H.
+ - discriminate.
+ - constructor. apply div2_even. injection H as <-. trivial. }
Qed.
Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
-Lemma even_odd_div2 :
- forall n,
- (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)).
+Lemma even_odd_div2 n :
+ (even n <-> div2 n = div2 (S n)) /\
+ (odd n <-> S (div2 n) = div2 (S n)).
Proof.
- auto decomp using div2_odd, div2_even, odd_div2, even_div2.
+ split; split; auto using div2_odd, div2_even, odd_div2, even_div2.
Qed.
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 8d82bc8ea..02eadf091 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -385,7 +385,7 @@ Qed.
Lemma subset_types_imp_guarded_rel_choice_iff_rel_choice :
ProofIrrelevance -> (GuardedRelationalChoice <-> RelationalChoice).
Proof.
- auto decomp using
+ intuition auto using
guarded_rel_choice_imp_rel_choice,
rel_choice_and_proof_irrel_imp_guarded_rel_choice.
Qed.
@@ -439,7 +439,7 @@ Corollary fun_choice_and_indep_general_prem_iff_guarded_fun_choice :
FunctionalChoiceOnInhabitedSet /\ IndependenceOfGeneralPremises
<-> GuardedFunctionalChoice.
Proof.
- auto decomp using
+ intuition auto using
guarded_fun_choice_imp_indep_of_general_premises,
guarded_fun_choice_imp_fun_choice,
fun_choice_and_indep_general_prem_imp_guarded_fun_choice.
@@ -480,7 +480,7 @@ Corollary fun_choice_and_small_drinker_iff_omniscient_fun_choice :
FunctionalChoiceOnInhabitedSet /\ SmallDrinker'sParadox
<-> OmniscientFunctionalChoice.
Proof.
- auto decomp using
+ intuition auto using
omniscient_fun_choice_imp_small_drinker,
omniscient_fun_choice_imp_fun_choice,
fun_choice_and_small_drinker_imp_omniscient_fun_choice.
@@ -547,7 +547,7 @@ Theorem constructive_indefinite_description_and_small_drinker_iff_epsilon :
(EpsilonStatement ->
SmallDrinker'sParadox * ConstructiveIndefiniteDescription).
Proof.
- auto decomp using
+ intuition auto using
epsilon_imp_constructive_indefinite_description,
constructive_indefinite_description_and_small_drinker_imp_epsilon,
epsilon_imp_small_drinker.
@@ -689,7 +689,7 @@ Qed.
Corollary dep_iff_non_dep_functional_rel_reification :
FunctionalRelReification <-> DependentFunctionalRelReification.
Proof.
- auto decomp using
+ intuition auto using
non_dep_dep_functional_rel_reification,
dep_non_dep_functional_rel_reification.
Qed.
@@ -814,7 +814,7 @@ Corollary fun_reification_descr_computational_excluded_middle_in_prop_context :
(forall P:Prop, P \/ ~ P) ->
forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C.
Proof.
- intros FunReify EM C; auto decomp using
+ intros FunReify EM C; intuition auto using
constructive_definite_descr_excluded_middle,
(relative_non_contradiction_of_definite_descr (C:=C)).
Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 21:48:16 +0000