Merge PR#276: Stopping injection not to work on discriminable atoms (see #4890).

3 files changed, 29 insertions, 32 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 87b9e4914..fc3fdd002 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2187,32 +2187,24 @@ the given bindings to instantiate parameters or hypotheses of {\term}.
 \label{injection}
 \tacindex{injection}
 
-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.
+The {\tt injection} tactic exploits the property that constructors of
+inductive types are injective, i.e. that if $c$ is a constructor
+of an inductive type and $c~\vec{t_1}$ and $c~\vec{t_2}$ are equal
+then $\vec{t_1}$ and $\vec{t_2}$ are equal too.
 
 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 {\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 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.
-\end{itemize}
-If these conditions are satisfied, then, the tactic derives the
-equality of all the subterms of {\term$_1$} and {\term$_2$} placed in
-the same positions and puts them as antecedents of the current goal.
+then {\tt injection} applies the injectivity of constructors as deep as possible to
+derive the equality of all the subterms of {\term$_1$} and {\term$_2$} at positions
+where {\term$_1$} and {\term$_2$} start to differ.
+For example, from {\tt (S p, S n) = (q, S (S m)} we may derive {\tt S
+  p = q} and {\tt n = S m}. For this tactic to work, {\term$_1$} and
+{\term$_2$} should be typed with an inductive
+type and they should be neither convertible, nor having a different
+head constructor. If these conditions are satisfied, the tactic
+derives the equality of all the subterms of {\term$_1$} and
+{\term$_2$} at positions where they differ and adds them as
+antecedents to the conclusion of the current goal.
 
 \Example Consider the following goal:
 
@@ -2251,6 +2243,7 @@ context using \texttt{intros until \ident}.
 \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}
+\item \errindex{Nothing to inject}
 \end{ErrMsgs}
 
 \begin{Variants}
diff --git a/tactics/equality.ml b/tactics/equality.ml
index cc7701ad5..18a1f0201 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -736,7 +736,7 @@ let _ =
       optread  = (fun () -> !keep_proof_equalities_for_injection) ;
       optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
 
-let find_positions env sigma t1 t2 =
+let find_positions env sigma ~no_discr t1 t2 =
   let project env sorts posn t1 t2 =
     let ty1 = get_type_of env sigma t1 in
     let s = get_sort_family_of env sigma ty1 in
@@ -767,7 +767,7 @@ let find_positions env sigma t1 t2 =
             List.flatten
 	      (List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn))
 		0 rargs1 rargs2)
-	  else if Sorts.List.mem InType sorts'
+	  else if Sorts.List.mem InType sorts' && not no_discr
           then (* see build_discriminator *)
 	    raise (DiscrFound (List.rev posn,sp1,sp2))
 	  else 
@@ -791,13 +791,14 @@ let find_positions env sigma t1 t2 =
     Inl (path,c1,c2)
 
 let discriminable env sigma t1 t2 =
-  match find_positions env sigma t1 t2 with
+  match find_positions env sigma ~no_discr:false t1 t2 with
     | Inl _ -> true
     | _ -> false
 
 let injectable env sigma t1 t2 =
-    match find_positions env sigma t1 t2 with
-    | Inl _ | Inr [] | Inr [([],_,_)] -> false
+    match find_positions env sigma ~no_discr:true t1 t2 with
+    | Inl _ -> assert false
+    | Inr [] | Inr [([],_,_)] -> false
     | Inr _ -> true
 
 
@@ -1032,7 +1033,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
-    match find_positions env sigma t1 t2 with
+    match find_positions env sigma ~no_discr:false t1 t2 with
     | Inr _ ->
 	tclZEROMSG (str"Not a discriminable equality.")
     | Inl (cpath, (_,dirn), _) ->
@@ -1414,9 +1415,9 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
 let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
   let env = eq_clause.env in
-  match find_positions env sigma t1 t2 with
+  match find_positions env sigma ~no_discr:true t1 t2 with
   | Inl _ ->
-     tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.")
+     assert false
   | Inr [] ->
      let suggestion =
          if !keep_proof_equalities_for_injection then
@@ -1483,7 +1484,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
   Proofview.Goal.enter { enter = begin fun gl ->
     let sigma =  clause.evd in
     let env = Proofview.Goal.env gl in
-      match find_positions env sigma t1 t2 with
+      match find_positions env sigma ~no_discr:false t1 t2 with
       | Inl (cpath, (_,dirn), _) ->
 	  discr_positions env sigma u clause cpath dirn
       | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index d979c580a..b47be3bbc 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -96,7 +96,10 @@ val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic
 val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic
 val rewriteInConcl : bool -> constr -> unit Proofview.tactic
 
+(* Tells if tactic "discriminate" is applicable *)
 val discriminable : env -> evar_map -> constr -> constr -> bool
+
+(* Tells if tactic "injection" is applicable *)
 val injectable : env -> evar_map -> constr -> constr -> bool
 
 (* Subst *)