aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/cc/cctac.ml26
-rw-r--r--contrib/cc/cctac.mli2
-rw-r--r--contrib/cc/g_congruence.ml44
-rw-r--r--contrib/interface/depends.ml3
-rw-r--r--contrib/interface/xlate.ml2
-rw-r--r--doc/refman/RefMan-tac.tex114
-rw-r--r--parsing/g_tactic.ml41
-rw-r--r--parsing/pptactic.ml2
-rw-r--r--proofs/tacexpr.ml1
-rw-r--r--tactics/hiddentac.ml3
-rw-r--r--tactics/hiddentac.mli2
-rw-r--r--tactics/tacinterp.ml3
-rw-r--r--tactics/tactics.ml55
-rw-r--r--tactics/tactics.mli4
-rw-r--r--test-suite/success/dependentind.v6
-rw-r--r--test-suite/success/specialize.v48
-rw-r--r--theories/FSets/FMapFacts.v4
-rw-r--r--theories/FSets/FSetDecide.v21
-rw-r--r--theories/Init/Tactics.v126
-rw-r--r--theories/Sets/Infinite_sets.v2
-rw-r--r--theories/Sets/Integers.v6
-rw-r--r--theories/Sets/Relations_2_facts.v6
22 files changed, 256 insertions, 185 deletions
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index e90e7afaa2..8eda68e106 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -430,3 +430,29 @@ let congruence_tac depth l =
tclORELSE
(tclTHEN (tclREPEAT introf) (cc_tactic depth l))
cc_fail
+
+(* The [f_equal] tactic.
+
+ It mimics the use of lemmas [f_equal], [f_equal2], etc.
+ This isn't particularly related with congruence, apart from
+ the fact that congruence is called internally.
+*)
+
+let f_equal gl =
+ let cut_eq c1 c2 =
+ tclTHENTRY
+ (Tactics.cut (mkApp (Lazy.force _eq, [| pf_type_of gl c1; c1; c2|])))
+ reflexivity
+ in
+ try match kind_of_term (pf_concl gl) with
+ | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) ->
+ begin match kind_of_term t, kind_of_term t' with
+ | App (f,v), App (f',v') when Array.length v = Array.length v' ->
+ let rec cuts i =
+ if i < 0 then tclTRY (congruence_tac 1000 [])
+ else tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
+ in cuts (Array.length v - 1) gl
+ | _ -> tclIDTAC gl
+ end
+ | _ -> tclIDTAC gl
+ with Type_errors.TypeError _ -> tclIDTAC gl
diff --git a/contrib/cc/cctac.mli b/contrib/cc/cctac.mli
index 0235252975..7cdd46ab4a 100644
--- a/contrib/cc/cctac.mli
+++ b/contrib/cc/cctac.mli
@@ -18,3 +18,5 @@ val cc_tactic : int -> constr list -> tactic
val cc_fail : tactic
val congruence_tac : int -> constr list -> tactic
+
+val f_equal : tactic
diff --git a/contrib/cc/g_congruence.ml4 b/contrib/cc/g_congruence.ml4
index 5b2cff9c27..f23ed49b6e 100644
--- a/contrib/cc/g_congruence.ml4
+++ b/contrib/cc/g_congruence.ml4
@@ -23,3 +23,7 @@ TACTIC EXTEND cc
|[ "congruence" integer(n) "with" ne_constr_list(l) ] ->
[ congruence_tac n l ]
END
+
+TACTIC EXTEND f_equal
+ [ "f_equal" ] -> [ f_equal ]
+END
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index a0cbe22b36..16357fc472 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -340,7 +340,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
| TacClear _
| TacClearBody _
| TacMove _
- | TacRename _ -> acc
+ | TacRename _
+ | TacRevert _ -> acc
(* Constructors *)
| TacLeft cb
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index c5a8c756a8..2219e327ca 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1187,6 +1187,7 @@ and xlate_tac =
let idl' = List.map xlate_hyp idl in
CT_clear (CT_id_ne_list (xlate_hyp id, idl'))
| TacClear (true,_) -> xlate_error "TODO: 'clear - idl' and 'clear'"
+ | TacRevert _ -> xlate_error "TODO: revert"
| (*For translating tactics/Inv.v *)
TacInversion (NonDepInversion (k,idl,l),quant_hyp) ->
CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp,
@@ -1248,6 +1249,7 @@ and xlate_tac =
(CT_formula_list
(List.map xlate_formula
(out_gen (wit_list0 rawwit_constr) args)))
+ | TacExtend (_, "f_equal", _) -> xlate_error "TODO: f_equal"
| TacExtend (_,id, l) ->
print_endline ("Extratactics : "^ id);
CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l))
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 342b20cb57..e7ee8b1a4d 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -386,8 +386,8 @@ second-order pattern-matching problem into a first-order one.
:= {\term$_n$})}
This also provides {\tt apply} with values for instantiating
- premises. But variables are referred by names and non dependent
- products by order (see syntax in Section~\ref{Binding-list}).
+ premises. Here, variables are referred by names and non-dependent
+ products by increasing numbers (see syntax in Section~\ref{Binding-list}).
\item {\tt eapply \term}\tacindex{eapply}\label{eapply}
@@ -558,44 +558,37 @@ in the list of subgoals remaining to prove.
\item \texttt{pose proof {\term} as {\ident}}
- This tactic behaves like \texttt{assert ({\ident:T} by exact {\term}} where
+ This tactic behaves like \texttt{assert ({\ident:T}) by exact {\term}} where
\texttt{T} is the type of {\term}.
-\end{Variants}
+\item {\tt specialize ({\ident} \term$_1$ {\ldots} \term$_n$)} \\
+ {\tt specialize {\ident} with \bindinglist}
+
+ The tactic {\tt specialize} works on local hypothesis \ident.
+ The premises of this hypothesis (either universal
+ quantifications or non-dependent implications) are instantiated
+ by concrete terms coming either from arguments \term$_1$
+ $\ldots$ \term$n$ or from a bindings list (see
+ Section~\ref{Binding-list} for more about bindings lists). In the
+ second form, all instantiation elements must be given, whereas
+ in the first form the application to \term$_1$ {\ldots}
+ \term$_n$ can be partial. The first form is equivalent to
+ {\tt assert (\ident':=\ident \term$_1$ {\ldots} \term$_n$);
+ clear \ident; rename \ident' into \ident}.
+
+ The name {\ident} can also refer to a global lemma or
+ hypothesis. In this case, for compatibility reasons, the
+ behavior of {\tt specialize} is close to the one of {\tt
+ generalize}: the instantiated statement becomes an additional
+ premise of the goal.
+
+%% Moreover, the old syntax allows the use of a number after {\tt specialize}
+%% for controlling the number of premises to instantiate. Giving this
+%% number should not be mandatory anymore (automatic detection of how
+%% many premises can be eaten without leaving meta-variables). Hence
+%% no documentation for this integer optional argument of specialize
-% PAS CLAIR;
-% DEVRAIT AU MOINS FAIRE UN INTRO;
-% DEVRAIT ETRE REMPLACE PAR UN LET;
-% MESSAGE D'ERREUR STUPIDE
-% POURQUOI Specialize trans_equal ECHOUE ?
-%\begin{Variants}
-%\item {\tt Specialize \term}
-% \tacindex{Specialize} \\
-% The argument {\tt t} should be a well-typed
-% term of type {\tt T}. This tactics is to make a cut of a
-% proposition when you have already the proof of this proposition
-% (for example it is a theorem applied to variables of local
-% context). It is equivalent to {\tt Assert T. exact t}.
-%
-%\item {\tt Specialize {\term} with \vref$_1$ := {\term$_1$} \dots
-% \vref$_n$ := \term$_n$}
-% \tacindex{Specialize \dots\ with} \\
-% It is to provide the tactic with some explicit values to instantiate
-% premises of {\term} (see Section~\ref{Binding-list}).
-% Some other premises are inferred using type information and
-% unification. The resulting well-formed
-% term being {\tt (\term~\term'$_1$\dots\term'$_k$)}
-% this tactic behaves as is used as
-% {\tt Specialize (\term~\term'$_1$\dots\term'$_k$)} \\
-%
-% \ErrMsg {\tt Metavariable wasn't in the metamap} \\
-% Arises when the information provided in the bindings list is not
-% sufficient.
-%\item {\tt Specialize {\num} {\term} with \vref$_1$ := {\term$_1$} \dots\
-% \vref$_n$:= \term$_n$}\\
-% The behavior is the same as before but only \num\ premises of
-% \term\ will be kept.
-%\end{Variants}
+\end{Variants}
\subsection{{\tt apply {\term} in {\ident}}
\tacindex{apply {\ldots} in}}
@@ -674,9 +667,11 @@ to $T$.
This generalizes {\term} but also {\em all} hypotheses which depend
on {\term}. It clears the generalized hypotheses.
-\item {\tt revert \term$_1$ \dots\ \term$_n$}\tacindex{revert}
+\item {\tt revert \ident$_1$ \dots\ \ident$_n$}\tacindex{revert}
- This is equivalent to a {\tt generalize} followed by a {\tt clear}.
+ This is equivalent to a {\tt generalize} followed by a {\tt clear}
+ on the given hypotheses. This tactic can be seem as reciprocal to
+ {\tt intros}.
\end{Variants}
@@ -795,14 +790,34 @@ the local context.
This tactic applies to any goal. The {\tt contradiction} tactic
attempts to find in the current context (after all {\tt intros}) one
-which is equivalent to {\tt False}. It permits to prune irrelevant
-cases. This tactic is a macro for the tactics sequence {\tt intros;
- elimtype False; assumption}.
+hypothesis which is equivalent to {\tt False}. It permits to prune
+irrelevant cases. This tactic is a macro for the tactics sequence
+{\tt intros; elimtype False; assumption}.
\begin{ErrMsgs}
\item \errindex{No such assumption}
\end{ErrMsgs}
+\begin{Variants}
+\item {\tt contradiction \ident}
+
+The proof of {\tt False} is searched in the hypothesis named \ident.
+\end{Variants}
+
+\subsection {\tt contradict \ident}
+\label{contradict}
+\tacindex{contradict}
+
+This tactic allows to manipulate negated hypothesis and goals. The
+name \ident\ should correspond to an hypothesis. With
+{\tt contradict H}, the current goal and context is transformed in
+the following way:
+\begin{itemize}
+\item {\tt H:$\neg$A $\vd$ B} \ becomes \ {\tt $\vd$ A}
+\item {\tt H:$\neg$A $\vd$ $\neg$B} \ becomes \ {\tt H: B $\vd$ A }
+\item {\tt H: A $\vd$ B} \ becomes \ {\tt $\vd$ $\neg$A}
+\item {\tt H: A $\vd$ $\neg$B} \ becomes \ {\tt H: B $\vd$ $\neg$A}
+\end{itemize}
\section{Conversion tactics
\index{Conversion tactics}
@@ -1294,12 +1309,13 @@ and {\tt induction {\term} as {\intropattern}}.
\ErrMsg \errindex{Not the right number of dependent arguments}
-\item{\tt elim {\term} with {\vref$_1$} := {\term$_1$} \dots\ {\vref$_n$}
- := {\term$_n$}}
+\item{\tt elim {\term} with ({\vref$_1$} := {\term$_1$}) \dots\ ({\vref$_n$}
+ := {\term$_n$}})
- Provides also {\tt elim} with values for instantiating premises by
- associating explicitly variables (or non dependent products) with
- their intended instance.
+ Also provides {\tt elim} with values for instantiating premises by
+ associating explicitly variables (or non-dependent products) with
+ their intended instance (see \ref{Binding-list} for more details
+ about bindings list).
\item{\tt elim {\term$_1$} using {\term$_2$}}
\tacindex{elim \dots\ using}
@@ -1978,10 +1994,6 @@ subgoals $f=f'$ and $a_1=a'_1$ and so on up to $a_n=a'_n$. Amongst
these subgoals, the simple ones (e.g. provable by
reflexivity or congruence) are automatically solved by {\tt f\_equal}.
-\Rem {\tt f\_equal} currently handles goals with only up to 5 arguments
-(i.e. $n\leq 5$).
-
-
\section{Equality and inductive sets}
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 96db00e3e4..b076220b45 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -458,6 +458,7 @@ GEXTEND Gram
| IDENT "move"; id1 = id_or_meta; IDENT "after"; id2 = id_or_meta ->
TacMove (true,id1,id2)
| IDENT "rename"; l = LIST1 rename SEP "," -> TacRename l
+ | IDENT "revert"; l = LIST1 id_or_meta -> TacRevert l
(* Constructors *)
| IDENT "left"; bl = with_bindings -> TacLeft bl
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 448b78e262..7775dc9816 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -787,6 +787,8 @@ and pr_atom1 = function
(fun (i1,i2) ->
pr_ident i1 ++ spc () ++ str "into" ++ spc () ++ pr_ident i2)
l)
+ | TacRevert l ->
+ hov 1 (str "revert" ++ spc () ++ prlist_with_sep spc pr_ident l)
(* Constructors *)
| TacLeft l -> hov 1 (str "left" ++ pr_bindings l)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index f74413704b..5ddebf3c99 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -175,6 +175,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
| TacClearBody of 'id list
| TacMove of bool * 'id * 'id
| TacRename of ('id *'id) list
+ | TacRevert of 'id list
(* Constructors *)
| TacLeft of 'constr bindings
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index f5c54a5336..60f1ccf0ca 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -83,7 +83,7 @@ let h_new_induction ev c e idl =
let h_new_destruct ev c e idl =
abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,Option.map inj_open_wb e,idl))
(new_destruct ev c e idl)
-let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (new_hyp n d)
+let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (specialize n d)
let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c)
(* Context management *)
@@ -94,6 +94,7 @@ let h_move dep id1 id2 =
abstract_tactic (TacMove (dep,id1,id2)) (move_hyp dep id1 id2)
let h_rename l =
abstract_tactic (TacRename l) (rename_hyp l)
+let h_revert l = abstract_tactic (TacRevert l) (revert l)
(* Constructors *)
let h_left l = abstract_tactic (TacLeft l) (left_with_ebindings l)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 87232988b8..909d294cf6 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -76,7 +76,7 @@ val h_clear : bool -> identifier list -> tactic
val h_clear_body : identifier list -> tactic
val h_move : bool -> identifier -> identifier -> tactic
val h_rename : (identifier*identifier) list -> tactic
-
+val h_revert : identifier list -> tactic
(* Constructors *)
val h_constructor : int -> open_constr bindings -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3245c31c7e..821586e7f0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -718,6 +718,7 @@ let rec intern_atomic lf ist x =
TacRename (List.map (fun (id1,id2) ->
intern_hyp_or_metaid ist id1,
intern_hyp_or_metaid ist id2) l)
+ | TacRevert l -> TacRevert (List.map (intern_hyp_or_metaid ist) l)
(* Constructors *)
| TacLeft bl -> TacLeft (intern_bindings ist bl)
@@ -2079,6 +2080,7 @@ and interp_atomic ist gl = function
h_rename (List.map (fun (id1,id2) ->
interp_hyp ist gl id1,
interp_fresh_ident ist gl (snd id2)) l)
+ | TacRevert l -> h_revert (interp_hyp_list ist gl l)
(* Constructors *)
| TacLeft bl -> h_left (interp_bindings ist gl bl)
@@ -2386,6 +2388,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacClearBody l as x -> x
| TacMove (dep,id1,id2) as x -> x
| TacRename l as x -> x
+ | TacRevert _ as x -> x
(* Constructors *)
| TacLeft bl -> TacLeft (subst_bindings subst bl)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6119185438..5f919a4dbe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -725,25 +725,41 @@ let rec intros_clearing = function
tclTHENLIST
[ intro; onLastHyp (fun id -> clear [id]); intros_clearing tl]
-(* Adding new hypotheses *)
-
-let new_hyp mopt (c,lbind) g =
- let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
- let clause = clenv_unify_meta_types clause in
- let (thd,tstack) = whd_stack (clenv_value clause) in
- let nargs = List.length tstack in
- let cut_pf =
- applist(thd,
- match mopt with
- | Some m -> if m < nargs then list_firstn m tstack else tstack
- | None -> tstack)
+(* Modifying/Adding an hypothesis *)
+
+let specialize mopt (c,lbind) g =
+ let evars, term =
+ if lbind = NoBindings then None, c
+ else
+ let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
+ let clause = clenv_unify_meta_types clause in
+ let (thd,tstack) = whd_stack (clenv_value clause) in
+ let nargs = List.length tstack in
+ let tstack = match mopt with
+ | Some m ->
+ if m < nargs then list_firstn m tstack else tstack
+ | None ->
+ let rec chk = function
+ | [] -> []
+ | t::l -> if occur_meta t then [] else t :: chk l
+ in chk tstack
+ in
+ let term = applist(thd,tstack) in
+ if occur_meta term then
+ errorlabstrm "" (str "Cannot infer an instance for " ++
+ pr_name (meta_name clause.evd (List.hd (collect_metas term))));
+ Some (evars_of clause.evd), term
in
- if occur_meta cut_pf then
- errorlabstrm "" (str "Cannot infer an instance for " ++
- pr_name (meta_name clause.evd (List.hd (collect_metas cut_pf))));
- (tclTHENLAST (tclTHEN (tclEVARS (evars_of clause.evd))
- (cut (pf_type_of g cut_pf)))
- ((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g
+ tclTHEN
+ (match evars with Some e -> tclEVARS e | _ -> tclIDTAC)
+ (match kind_of_term (fst (decompose_app c)) with
+ | Var id when List.exists (fun (i,_,_)-> i=id) (pf_hyps g) ->
+ let id' = fresh_id [] id g in
+ tclTHENS (internal_cut id' (pf_type_of g term))
+ [ exact_no_check term;
+ tclTHEN (clear [id]) (rename_hyp [id',id]) ]
+ | _ -> tclTHENLAST (cut (pf_type_of g term)) (exact_no_check term))
+ g
(* Keeping only a few hypotheses *)
@@ -1084,6 +1100,9 @@ let generalize lconstr gl =
let newcl = List.fold_right (generalize_goal gl) lconstr (pf_concl gl) in
apply_type newcl lconstr gl
+let revert hyps gl =
+ tclTHEN (generalize (List.map mkVar hyps)) (clear hyps) gl
+
(* Faudra-t-il une version avec plusieurs args de generalize_dep ?
Cela peut-être troublant de faire "Generalize Dependent H n" dans
"n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index eb62f602aa..3a3bf6de51 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -156,11 +156,13 @@ val clear : identifier list -> tactic
val clear_body : identifier list -> tactic
val keep : identifier list -> tactic
-val new_hyp : int option -> constr with_ebindings -> tactic
+val specialize : int option -> constr with_ebindings -> tactic
val move_hyp : bool -> identifier -> identifier -> tactic
val rename_hyp : (identifier * identifier) list -> tactic
+val revert : identifier list -> tactic
+
(*s Resolution tactics. *)
val apply_type : constr -> constr list -> tactic
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index f45b592af8..77bc295fd8 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -67,7 +67,7 @@ Proof with simpl in * ; auto ; simpl_depind.
apply ax.
destruct D...
- narrow IHterm with G empty...
+ specialize (IHterm G empty)...
apply weak...
apply weak...
@@ -76,7 +76,7 @@ Proof with simpl in * ; auto ; simpl_depind.
apply weak ; apply abs ; apply H.
apply abs...
- narrow IHterm with G0 (D, t, tau)...
+ specialize (IHterm G0 (D, t, tau))...
apply app with tau...
Qed.
@@ -97,7 +97,7 @@ Proof with simpl in * ; simpl_depind ; auto.
apply weak...
apply abs...
- narrow IHterm with G0 (D, tau)...
+ specialize (IHterm G0 (D, tau))...
eapply app with tau...
Save.
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
new file mode 100644
index 0000000000..4929ae4c0c
--- /dev/null
+++ b/test-suite/success/specialize.v
@@ -0,0 +1,48 @@
+
+Goal forall a b c : nat, a = b -> b = c -> forall d, a+d=c+d.
+intros.
+
+(* "compatibility" mode: specializing a global name
+ means a kind of generalize *)
+
+specialize trans_equal. intros _.
+specialize trans_equal with (1:=H)(2:=H0). intros _.
+specialize trans_equal with (x:=a)(y:=b)(z:=c). intros _.
+specialize trans_equal with (1:=H)(z:=c). intros _.
+specialize trans_equal with nat a b c. intros _.
+specialize (@trans_equal nat). intros _.
+specialize (@trans_equal _ a b c). intros _.
+specialize (trans_equal (x:=a)). intros _.
+specialize (trans_equal (x:=a)(y:=b)). intros _.
+specialize (trans_equal H H0). intros _.
+specialize (trans_equal H0 (z:=b)). intros _.
+
+(* local "in place" specialization *)
+assert (Eq:=trans_equal).
+
+specialize Eq.
+specialize Eq with (1:=H)(2:=H0). Undo.
+specialize Eq with (x:=a)(y:=b)(z:=c). Undo.
+specialize Eq with (1:=H)(z:=c). Undo.
+specialize Eq with nat a b c. Undo.
+specialize (Eq nat). Undo.
+specialize (Eq _ a b c). Undo.
+(* no implicit argument for Eq, hence no (Eq (x:=a)) *)
+specialize (Eq _ _ _ _ H H0). Undo.
+specialize (Eq _ _ _ b H0). Undo.
+
+(*
+(** strange behavior to inspect more precisely *)
+
+(* 1) proof aspect : let H:= ... in (fun H => ..) H
+ presque ok... *)
+
+(* 2) echoue moins lorsque zero premise de mangé *)
+specialize trans_equal with (1:=Eq). (* mal typé !! *)
+
+(* 3) *)
+specialize trans_equal with _ a b c. intros _.
+(* Anomaly: Evar ?88 was not declared. Please report. *)
+*)
+
+Abort. \ No newline at end of file
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 993f1ae79a..832829135b 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -584,8 +584,8 @@ Proof.
rewrite in_find_iff, in_find_iff, H; intuition.
rewrite find_mapsto_iff in H0,H1; congruence.
destruct H.
- narrow H with y.
- narrow H0 with y.
+ specialize (H y).
+ specialize (H0 y).
do 2 rewrite in_find_iff in H.
generalize (find_mapsto_iff m y)(find_mapsto_iff m' y).
do 2 destruct find; auto; intros.
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 1c8bac6d97..e8d639003b 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -387,19 +387,6 @@ the above form:
end);
cbv zeta beta in *.
- (** If you have a negated goal and [H] is a negated
- hypothesis, then [contra H] exchanges your goal and [H],
- removing the negations. (Just like [swap] but reuses
- the same name. *)
- Ltac contra H :=
- let J := fresh in
- unfold not;
- unfold not in H;
- intros J;
- apply H;
- clear H;
- rename J into H.
-
(** [decompose records] calls [decompose record H] on every
relevant hypothesis [H]. *)
Tactic Notation "decompose" "records" :=
@@ -704,15 +691,15 @@ the above form:
unfold not in *;
match goal with
| H: (In ?x ?r) -> False |- (In ?x ?s) -> False =>
- contra H; fsetdec_body
+ contradict H; fsetdec_body
| H: (In ?x ?r) -> False |- (E.eq ?x ?y) -> False =>
- contra H; fsetdec_body
+ contradict H; fsetdec_body
| H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False =>
- contra H; fsetdec_body
+ contradict H; fsetdec_body
| H: ?P -> False |- ?Q -> False =>
if prop (FSet_elt_Prop P) holds by
(auto 100 with FSet_Prop)
- then (contra H; fsetdec_body)
+ then (contradict H; fsetdec_body)
else fsetdec_body
| |- _ =>
fsetdec_body
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index f61e9422e2..50653c4200 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -11,43 +11,43 @@
Require Import Notations.
Require Import Logic.
-(** Useful tactics *)
-
-(* A shorter name for generalize + clear, can be seen as an anti-intro *)
-
-Tactic Notation "revert" ne_hyp_list(l) := generalize l; clear l.
-
-(**************************************
- A tactic for proof by contradiction
- with contradict H
- H: ~A |- B gives |- A
- H: ~A |- ~ B gives H: B |- A
- H: A |- B gives |- ~ A
- H: A |- B gives |- ~ A
- H: A |- ~ B gives H: A |- ~ A
-**************************************)
-
-Ltac contradict name :=
- let term := type of name in (
- match term with
- (~_) =>
- match goal with
- |- ~ _ => let x := fresh in
- (intros x; case name;
- generalize x; clear x name;
- intro name)
- | |- _ => case name; clear name
- end
- | _ =>
- match goal with
- |- ~ _ => let x := fresh in
- (intros x; absurd term;
- [idtac | exact name]; generalize x; clear x name;
- intros name)
- | |- _ => generalize name; absurd term;
- [idtac | exact name]; clear name
- end
- end).
+(** * Useful tactics *)
+
+(** A tactic for proof by contradiction. With contradict H,
+ - H:~A |- B gives |- A
+ - H:~A |- ~B gives H: B |- A
+ - H: A |- B gives |- ~A
+ - H: A |- ~B gives H: B |- ~A
+ Moreover, negations may be in unfolded forms,
+ and A or B may live in Type *)
+
+Ltac contradict H :=
+ let save tac H := let x:=fresh in intro x; tac H; rename x into H
+ in
+ let negpos H := case H; clear H
+ in
+ let negneg H := save negpos H
+ in
+ let pospos H :=
+ let A := type of H in (elimtype False; revert H; try fold (~A))
+ in
+ let posneg H := save pospos H
+ in
+ let neg H := match goal with
+ | |- (~_) => negneg H
+ | |- (_->False) => negneg H
+ | |- _ => negpos H
+ end in
+ let pos H := match goal with
+ | |- (~_) => posneg H
+ | |- (_->False) => posneg H
+ | |- _ => pospos H
+ end in
+ match type of H with
+ | (~_) => neg H
+ | (_->False) => neg H
+ | _ => pos H
+ end.
(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
@@ -55,62 +55,22 @@ Ltac swap H :=
idtac "swap is OBSOLETE: use contradict instead.";
intro; apply H; clear H.
-(* to contradict an hypothesis without copying its type. *)
+(* To contradict an hypothesis without copying its type. *)
-Ltac absurd_hyp h :=
+Ltac absurd_hyp H :=
idtac "absurd_hyp is OBSOLETE: use contradict instead.";
- let T := type of h in
+ let T := type of H in
absurd T.
-(* A useful complement to contradict. Here t : ~ A where H : A. *)
+(* A useful complement to contradict. Here H : A and G allows to conclude ~A *)
-Ltac false_hyp h t :=
- let T := type of h in absurd T; [ apply t | assumption ].
+Ltac false_hyp H G :=
+ let T := type of H in absurd T; [ apply G | assumption ].
(* A case with no loss of information. *)
Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x.
-(* A tactic for easing the use of lemmas f_equal, f_equal2, ... *)
-
-Ltac f_equal :=
- let cg := try congruence in
- let r := try reflexivity in
- match goal with
- | |- ?f ?a = ?f' ?a' => cut (a=a'); [cg|r]
- | |- ?f ?a ?b = ?f' ?a' ?b' =>
- cut (b=b');[cut (a=a');[cg|r]|r]
- | |- ?f ?a ?b ?c = ?f' ?a' ?b' ?c'=>
- cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]
- | |- ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d'=>
- cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]
- | |- ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e'=>
- cut (e=e');[cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]|r]
- | |- ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g' =>
- cut (f=f');[cut (e=e');[cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]|r]|r]
- | _ => idtac
- end.
-
-(* Specializing universal hypothesis.
- The word "specialize" is already used for a not-documented-anymore
- tactic still used in some users contribs. Any idea for a better name?
-*)
-
-Tactic Notation "narrow" hyp(H) "with" constr(x) :=
- generalize (H x); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) :=
- generalize (H x y); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z):=
- generalize (H x y z); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z) constr(t):=
- generalize (H x y z t); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z) constr(t) constr(u):=
- generalize (H x y z t u); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z) constr(t) constr(u) constr(v) :=
- generalize (H x y z t u v); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z) constr(t) constr(u) constr(v) constr(w) :=
- generalize (H x y z t u v w); clear H; intro H.
-
(* Rewriting in all hypothesis several times everywhere *)
Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index f30c5b7630..6b02e8383f 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -162,7 +162,7 @@ Section Infinite_sets.
generalize (H'3 x).
intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ];
auto with sets.
- specialize 5Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
+ specialize Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ];
auto with sets.
intros x1 H'4; try assumption.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 88cdabe3ff..ec44a6e582 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -87,7 +87,7 @@ Section Integers_sect.
apply Totally_ordered_definition.
simpl in |- *.
intros H' x y H'0.
- specialize 2le_or_lt with (n := x) (m := y); intro H'2; elim H'2.
+ elim le_or_lt with (n := x) (m := y).
intro H'1; left; auto with sets arith.
intro H'1; right.
cut (y <= x); auto with sets arith.
@@ -142,8 +142,8 @@ Section Integers_sect.
elim H'0; intros H'1 H'2.
cut (In nat Integers (S x)).
intro H'3.
- specialize 1H'2 with (y := S x); intro H'4; lapply H'4;
- [ intro H'5; clear H'4 | try assumption; clear H'4 ].
+ specialize H'2 with (y := S x); lapply H'2;
+ [ intro H'5; clear H'2 | try assumption; clear H'2 ].
simpl in H'5.
absurd (S x <= x); auto with arith.
apply triv_nat.
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index a7da7db9a4..d5257c12c1 100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -140,10 +140,10 @@ intros U R H' x b H'0; elim H'0.
intros x0 a H'1; exists a; auto with sets.
intros x0 y z H'1 H'2 H'3 a H'4.
red in H'.
-specialize 3H' with (x := x0) (a := a) (b := y); intro H'7; lapply H'7;
+specialize H' with (x := x0) (a := a) (b := y); lapply H';
[ intro H'8; lapply H'8;
- [ intro H'9; try exact H'9; clear H'8 H'7 | clear H'8 H'7 ]
- | clear H'7 ]; auto with sets.
+ [ intro H'9; try exact H'9; clear H'8 H' | clear H'8 H' ]
+ | clear H' ]; auto with sets.
elim H'9.
intros t H'5; elim H'5; intros H'6 H'7; try exact H'6; clear H'5.
elim (H'3 t); auto with sets.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 12:43:05 +0000