- Implantation de la suggestion 1873 sur discriminate. Au final,

  discriminate/injection/simplify_eq acceptent maintenant un terme
  comme argument. Les clauses "with" et les variantes "e" sont aussi
  acceptées. Aussi, discriminate sans argument essaie maintenant
  toutes les hyps quantifiées (au lieu de traiter seulement les buts
  t1<>t2).

--This line, and those below, will be ignored--

M    doc/refman/RefMan-tac.tex
M    CHANGES
M    pretyping/evd.ml
M    pretyping/termops.ml
M    pretyping/termops.mli
M    pretyping/clenv.ml
M    tactics/extratactics.ml4
M    tactics/inv.ml
M    tactics/equality.ml
M    tactics/tactics.mli
M    tactics/equality.mli
M    tactics/tacticals.ml
M    tactics/eqdecide.ml4
M    tactics/tacinterp.ml
M    tactics/tactics.ml
M    tactics/extratactics.mli
M    toplevel/auto_ind_decl.ml
M    contrib/funind/invfun.ml
M    test-suite/success/Discriminate.v
M    test-suite/success/Injection.v
M    proofs/clenvtac.mli
M    proofs/clenvtac.ml


git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@11159 85f007b7-540e-0410-9357-904b9bb8a0f7

Author: herbelin

Diff for: CHANGES

@@ -202,6 +202,9 @@ Tactics
 - Slight improvement of the hnf and simpl tactics when applied on
   expressions with explicit occurrences of match or fix.
 - New tactics "eapply in", "erewrite", "erewrite in".
+- New tactics "ediscriminate", "einjection", "esimplify_eq".
+- Tactics "discriminate", "injection", "simplify_eq" now support any
+  term as argument. Clause "with" is also supported.
 - Unfoldable references can be given by notation's string rather than by name 
   in unfold.
 - The "with" arguments are now typed using informations from the current goal:

Diff for: contrib/funind/invfun.ml

@@ -573,9 +573,9 @@ let rec reflexivity_with_destruct_cases g =
 	       match kind_of_term  (pf_type_of g (mkVar id)) with 
 		 | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> 
 		     if Equality.discriminable (pf_env g) (project g) t1 t2 
-		     then Equality.discr id g
+		     then Equality.discrHyp id g
 		     else if Equality.injectable (pf_env g) (project g) t1 t2
-		     then tclTHENSEQ [Equality.inj [] id;thin [id];intros_with_rewrite]  g
+		     then tclTHENSEQ [Equality.injHyp id;thin [id];intros_with_rewrite]  g
 		     else tclIDTAC g
 		 | _ -> tclIDTAC g
     )

Diff for: doc/refman/RefMan-tac.tex

@@ -993,7 +993,7 @@ \subsection{\tt contradiction
 \tacindex{contradict}
 
 This tactic allows to manipulate negated hypothesis and goals. The
-name \ident\ should correspond to an hypothesis. With 
+name \ident\ should correspond to a hypothesis. With 
 {\tt contradict H}, the current goal and context is transformed in
 the following way: 
 \begin{itemize}
@@ -2395,17 +2395,20 @@ \subsection{\tt compare \term$_1$ \term$_2$
 of \term$_1$ and \term$_2$ must satisfy the same restrictions as in the tactic
 \texttt{decide equality}.
 
-\subsection{\tt discriminate {\ident}
+\subsection{\tt discriminate {\term}
 \label{discriminate}
-\tacindex{discriminate}}
+\tacindex{discriminate}
+\tacindex{ediscriminate}}
 
-This tactic proves any goal from an absurd hypothesis stating that two
+This tactic proves any goal from an assumption stating that two
 structurally different terms of an inductive set are equal. For
-example, from the hypothesis {\tt (S (S O))=(S O)} we can derive by
-absurdity any proposition.  Let {\ident} be a hypothesis of type
-{\tt{\term$_1$} = {\term$_2$}} in the local context, {\term$_1$} and
+example, from {\tt (S (S O))=(S O)} we can derive by absurdity any
+proposition.
+
+The argument {\term} is assumed to be a proof of a statement
+of conclusion {\tt{\term$_1$} = {\term$_2$}} with {\term$_1$} and
 {\term$_2$} being elements of an inductive set.  To build the proof,
-the tactic traverses the normal forms\footnote{Recall: opaque
+the tactic traverses the normal forms\footnote{Reminder: opaque
   constants will not be expanded by $\delta$ reductions} of
 {\term$_1$} and {\term$_2$} looking for a couple of subterms {\tt u}
 and {\tt w} ({\tt u} subterm of the normal form of {\term$_1$} and
@@ -2414,55 +2417,70 @@ \subsection{\tt discriminate {\ident}
 such a couple of subterms exists, then the proof of the current goal
 is completed, otherwise the tactic fails.
 
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
-latter is first introduced in the local context using
-\texttt{intros until \ident}.
+\Rem The syntax {\tt discriminate {\ident}} can be used to refer to a
+hypothesis quantified in the goal. In this case, the quantified
+hypothesis whose name is {\ident} is first introduced in the local
+context using \texttt{intros until \ident}.
 
 \begin{ErrMsgs}
-\item {\ident} \errindex{Not a discriminable equality} \\
-  occurs when the type of the specified hypothesis is not an equation.
+\item \errindex{No primitive equality found}
+\item \errindex{Not a discriminable equality}
 \end{ErrMsgs}  
 
 \begin{Variants}
-\item \texttt{discriminate} \num\\
-  This does the same thing as \texttt{intros until \num} then
-\texttt{discriminate \ident} where {\ident} is the identifier for the last
-introduced hypothesis.
-\item {\tt discriminate}\\
-  It applies to a goal of the form {\tt
-    \verb=~={\term$_1$}={\term$_2$}} and it is equivalent to: 
-  {\tt unfold not; intro {\ident}}; {\tt discriminate
-    {\ident}}.
+\item \texttt{discriminate} \num
+
+  This does the same thing as \texttt{intros until \num} followed by
+  \texttt{discriminate \ident} where {\ident} is the identifier for
+  the last introduced hypothesis.
+
+\item \texttt{discriminate} {\term} {\tt with} {\bindinglist}
+
+  This does the same thing as \texttt{discriminate {\term}} but using
+the given bindings to instantiate parameters or hypotheses of {\term}.
+
+\item \texttt{ediscriminate} \num\\
+      \texttt{ediscriminate} {\term} \zeroone{{\tt with} {\bindinglist}}
+
+  This works the same as {\tt discriminate} but if the type of {\term},
+  or the type of the hypothesis referred to by {\num}, has uninstantiated
+  parameters, these parameters are left as existential variables.
+
+\item \texttt{discriminate}
+
+  This looks for a quantified or not quantified hypothesis {\ident} on
+  which {\tt discriminate {\ident}} is applicable.
 
   \begin{ErrMsgs}
   \item \errindex{No discriminable equalities} \\
   occurs when the goal does not verify the expected preconditions.
   \end{ErrMsgs}
 \end{Variants}
 
-\subsection{\tt injection {\ident}
+\subsection{\tt injection {\term}
 \label{injection}
-\tacindex{injection}}
+\tacindex{injection}
+\tacindex{einjection}}
 
 The {\tt injection} tactic is based on the fact that constructors of
 inductive sets are injections. That means that if $c$ is a constructor
 of an inductive set, and if $(c~\vec{t_1})$ and $(c~\vec{t_2})$ are two
 terms that are equal then $~\vec{t_1}$ and $~\vec{t_2}$ are equal
 too.
 
-If {\ident} is an hypothesis of type {\tt {\term$_1$} = {\term$_2$}},
-then {\tt injection} behaves as applying injection as deep as possible to
+If {\term} is a proof of a statement of conclusion
+ {\tt {\term$_1$} = {\term$_2$}},
+then {\tt injection} applies injectivity as deep as possible to
 derive the equality of all the subterms of {\term$_1$} and {\term$_2$}
-placed in the same positions. For example, from the hypothesis {\tt (S
+placed in the same positions. For example, from {\tt (S
   (S n))=(S (S (S m))} we may derive {\tt n=(S m)}.  To use this
 tactic {\term$_1$} and {\term$_2$} should be elements of an inductive
 set and they should be neither explicitly equal, nor structurally
 different. We mean by this that, if {\tt n$_1$} and {\tt n$_2$} are
 their respective normal forms, then:
 \begin{itemize}
 \item {\tt n$_1$} and {\tt n$_2$} should not be syntactically equal,
-\item there must not exist any couple of subterms {\tt u} and {\tt w},
+\item there must not exist any pair of subterms {\tt u} and {\tt w},
   {\tt u} subterm of {\tt n$_1$} and {\tt w} subterm of {\tt n$_2$} ,
   placed in the same positions and having different constructors as
   head symbols.
@@ -2501,69 +2519,94 @@ \subsection{\tt injection {\ident}
 To define such an equality, you have to use the {\tt Scheme} command 
 (see \ref{Scheme}).
 
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
-latter is first introduced in the local context using
-\texttt{intros until \ident}.
+\Rem If some quantified hypothesis of the goal is named {\ident}, then
+{\tt injection {\ident}} first introduces the hypothesis in the local
+context using \texttt{intros until \ident}.
 
 \begin{ErrMsgs}
-\item {\ident} \errindex{is not a projectable equality} 
-  occurs when the type of
-  the hypothesis $id$ does not verify the preconditions.
-\item \errindex{Not an equation} occurs when the type of the
-  hypothesis $id$ is not an equation.
+\item \errindex{Not a projectable equality but a discriminable one}
+\item \errindex{Nothing to do, it is an equality between convertible terms}
+\item \errindex{Not a primitive equality}
 \end{ErrMsgs}
 
 \begin{Variants}
 \item \texttt{injection} \num{}
 
-  This does the same thing as \texttt{intros until \num} then
+  This does the same thing as \texttt{intros until \num} followed by
 \texttt{injection \ident} where {\ident} is the identifier for the last
 introduced hypothesis.
 
-\item{\tt injection}\tacindex{injection} 
+\item \texttt{injection} \term{} {\tt with} {\bindinglist}
+
+  This does the same as \texttt{injection {\term}} but using
+  the given bindings to instantiate parameters or hypotheses of {\term}.
+
+\item \texttt{einjection} \num\\
+      \texttt{einjection} \term{} \zeroone{{\tt with} {\bindinglist}}
+
+  This works the same as {\tt injection} but if the type of {\term},
+  or the type of the hypothesis referred to by {\num}, has uninstantiated
+  parameters, these parameters are left as existential variables.
+
+\item{\tt injection}
 
   If the current goal is of the form {\term$_1$} {\tt <>} {\term$_2$},
-  the tactic computes the head normal form of the goal and then
-  behaves as the sequence: {\tt unfold not; intro {\ident}; injection
-  {\ident}}.
+  this behaves as {\tt intro {\ident}; injection {\ident}}.
 
   \ErrMsg \errindex{goal does not satisfy the expected preconditions}
 
-\item \texttt{injection} \ident{} \texttt{as} \nelist{\intropattern}{}\\
+\item \texttt{injection} \term{} \zeroone{{\tt with} {\bindinglist}} \texttt{as} \nelist{\intropattern}{}\\
 \texttt{injection} \num{} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
 \texttt{injection} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
+\texttt{einjection} \term{} \zeroone{{\tt with} {\bindinglist}} \texttt{as} \nelist{\intropattern}{}\\
+\texttt{einjection} \num{} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
+\texttt{einjection} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
 \tacindex{injection \ldots{} as}
 
-These variants apply \texttt{intros} \nelist{\intropattern}{} after the call to \texttt{injection}.
+These variants apply \texttt{intros} \nelist{\intropattern}{} after
+the call to \texttt{injection} or \texttt{einjection}.
 
 \end{Variants}
 
-\subsection{\tt simplify\_eq {\ident}
+\subsection{\tt simplify\_eq {\term}
 \tacindex{simplify\_eq}
+\tacindex{esimplify\_eq}
 \label{simplify-eq}}
 
-Let {\ident} be the name of an hypothesis of type {\tt
-  {\term$_1$}={\term$_2$}} in the local context. If {\term$_1$} and
+Let {\term} be the proof of a statement of conclusion {\tt
+  {\term$_1$}={\term$_2$}}. If {\term$_1$} and
 {\term$_2$} are structurally different (in the sense described for the
 tactic {\tt discriminate}), then the tactic {\tt simplify\_eq} behaves as {\tt
-  discriminate {\ident}} otherwise it behaves as {\tt injection
-  {\ident}}.
+  discriminate {\term}}, otherwise it behaves as {\tt injection
+  {\term}}.
 
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
-latter is first introduced in the local context using
-\texttt{intros until \ident}.
+\Rem If some quantified hypothesis of the goal is named {\ident}, then
+{\tt simplify\_eq {\ident}} first introduces the hypothesis in the local
+context using \texttt{intros until \ident}.
 
 \begin{Variants}
 \item \texttt{simplify\_eq} \num
 
   This does the same thing as \texttt{intros until \num} then
 \texttt{simplify\_eq \ident} where {\ident} is the identifier for the last
 introduced hypothesis.
+
+\item \texttt{simplify\_eq} \term{} {\tt with} {\bindinglist}
+
+  This does the same as \texttt{simplify\_eq {\term}} but using
+  the given bindings to instantiate parameters or hypotheses of {\term}.
+
+\item \texttt{esimplify\_eq} \num\\
+      \texttt{esimplify\_eq} \term{} \zeroone{{\tt with} {\bindinglist}}
+
+  This works the same as {\tt simplify\_eq} but if the type of {\term},
+  or the type of the hypothesis referred to by {\num}, has uninstantiated
+  parameters, these parameters are left as existential variables.
+
 \item{\tt simplify\_eq}
-If the current goal has form $\verb=~=t_1=t_2$, then this tactic does 
-\texttt{hnf; intro {\ident}; simplify\_eq {\ident}}.
+
+If the current goal has form $t_1\verb=<>=t_2$, it behaves as
+\texttt{intro {\ident}; simplify\_eq {\ident}}.
 \end{Variants}
 
 \subsection{\tt dependent rewrite -> {\ident}
@@ -2599,8 +2642,8 @@ \subsection{\tt inversion {\ident}
 conditions that should hold for the instance $(I~\vec{t})$ to be
 proved by $c_i$.
 
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
+\Rem If {\ident} does not denote a hypothesis in the local context
+but refers to a hypothesis quantified in the goal, then the
 latter is first introduced in the local context using
 \texttt{intros until \ident}.
 
@@ -3242,7 +3285,7 @@ \subsection{\tt congruence
 (see \ref{injection} and \ref{discriminate}).
 If the goal is a non-quantified equality, {\tt congruence} tries to
 prove it with non-quantified equalities in the context. Otherwise it
-tries to infer a discriminable equality from those in the context. Alternatively, congruence tries to prove that an hypothesis is equal to the goal or to the negation of another hypothesis.
+tries to infer a discriminable equality from those in the context. Alternatively, congruence tries to prove that a hypothesis is equal to the goal or to the negation of another hypothesis.
 
 {\tt congruence} is also able to take advantage of hypotheses stating quantified equalities, you have to provide a bound for the number of extra equalities generated that way. Please note that one of the members of the equality must contain all the quantified variables in order for {\tt congruence} to match against it. 
 

Diff for: pretyping/clenv.ml

@@ -222,13 +222,24 @@ let dependent_metas clenv mvs conclmetas =
        Metaset.union deps (clenv_metavars clenv.evd mv))
     mvs conclmetas
 
+let duplicated_metas c = 
+  let rec collrec (one,more as acc) c =
+    match kind_of_term c with
+    | Meta mv -> if List.mem mv one then (one,mv::more) else (mv::one,more)
+    | _       -> fold_constr collrec acc c
+  in
+  snd (collrec ([],[]) c)
+
 let clenv_dependent hyps_only clenv =
   let mvs = undefined_metas clenv.evd in
   let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
   let deps = dependent_metas clenv mvs ctyp_mvs in
+  let nonlinear = duplicated_metas (clenv_value clenv) in
+  (* Make the assumption that duplicated metas have internal dependencies *)
   List.filter
-    (fun mv -> Metaset.mem mv deps &&
-               not (hyps_only && Metaset.mem mv ctyp_mvs))
+    (fun mv -> (Metaset.mem mv deps &&
+                not (hyps_only && Metaset.mem mv ctyp_mvs))
+               or List.mem mv nonlinear) 
     mvs
 
 let clenv_missing ce = clenv_dependent true ce

Diff for: pretyping/evd.ml

@@ -643,6 +643,20 @@ type unsolvability_explanation = SeveralInstancesFound of int
 (**********************************************************)
 (* Pretty-printing *)
 
+let pr_instance_status (sc,typ) =
+  begin match sc with
+  | IsSubType -> str " [or a subtype of it]"
+  | IsSuperType -> str " [or a supertype of it]"
+  | ConvUpToEta 0 -> mt ()
+  | UserGiven -> mt ()
+  | ConvUpToEta n -> str" [or an eta-expansion up to " ++ int n ++ str" of it]"
+  end ++
+  begin match typ with
+  | CoerceToType -> str " [up to coercion]"
+  | TypeNotProcessed -> mt ()
+  | TypeProcessed -> str " [type is checked]"
+  end
+
 let pr_meta_map mmap =
   let pr_name = function
       Name id -> str"[" ++ pr_id id ++ str"]"
@@ -652,10 +666,10 @@ let pr_meta_map mmap =
       	hov 0 
 	  (pr_meta mv ++ pr_name na ++ str " : " ++
            print_constr b.rebus ++ fnl ())
-    | (mv,Clval(na,(b,_),_)) ->
+    | (mv,Clval(na,(b,s),_)) ->
       	hov 0 
 	  (pr_meta mv ++ pr_name na ++ str " := " ++
-           print_constr b.rebus ++ fnl ())
+           print_constr b.rebus ++ spc () ++ pr_instance_status s ++ fnl ())
   in
   prlist pr_meta_binding (metamap_to_list mmap)
 

Diff for: pretyping/termops.ml

@@ -275,6 +275,11 @@ let rec strip_head_cast c = match kind_of_term c with
   | Cast (c,_,_) -> strip_head_cast c
   | _ -> c
 
+(* Get the last arg of an application *)
+let last_arg c = match kind_of_term c with
+  | App (f,cl) -> array_last cl
+  | _ -> anomaly "last_arg"
+
 (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
    subterms of [c]; it carries an extra data [l] (typically a name
    list) which is processed by [g na] (which typically cons [na] to

Diff for: pretyping/termops.mli

@@ -185,6 +185,9 @@ val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr
 val it_mkProd_or_LetIn_name   : env -> types -> rel_context -> types
 val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
 
+(* Get the last arg of a constr intended to be nn application *)
+val last_arg : constr -> constr
+
 (* name contexts *)
 type names_context = name list
 val add_name : name -> names_context -> names_context

Diff for: proofs/clenvtac.ml

@@ -60,6 +60,9 @@ let clenv_cast_meta clenv =
   in 
   crec
 
+let clenv_value_cast_meta clenv =
+    clenv_cast_meta clenv (clenv_value clenv)
+
 let clenv_pose_dependent_evars with_evars clenv =
   let dep_mvs = clenv_dependent false clenv in
   if dep_mvs <> [] & not with_evars then

Diff for: proofs/clenvtac.mli

@@ -27,6 +27,7 @@ val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify
 val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
 
 val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
+val clenv_value_cast_meta : clausenv -> constr
 
 (* Compatibility, use res_pf ?with_evars:true instead *)
 val e_res_pf : clausenv -> tactic