Fixing injection in the presence of let-in in constructors.

This also fixes decide equality, discriminate, ... (see e.g. #5279).

5 files changed, 35 insertions, 5 deletions

diff --git a/kernel/vars.ml b/kernel/vars.ml
index b27e27fda..4affb5f9f 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -181,6 +181,15 @@ let subst_of_rel_context_instance sign l =
 let adjust_subst_to_rel_context sign l =
   List.rev (subst_of_rel_context_instance sign l)
 
+let adjust_rel_to_rel_context sign n =
+  let rec aux sign =
+    let open RelDecl in
+    match sign with
+    | LocalAssum _ :: sign' -> let (n',p) = aux sign' in (n'+1,p)
+    | LocalDef (_,c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p)
+    | [] -> (0,n)
+  in snd (aux sign)
+
 (* (thin_val sigma) removes identity substitutions from sigma *)
 
 let rec thin_val = function
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 574d50ecc..f7535e6d8 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -73,6 +73,10 @@ val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl
 (** For compatibility: returns the substitution reversed *)
 val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list
 
+(** Take an index in an instance of a context and returns its index wrt to
+    the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *)
+val adjust_rel_to_rel_context : Context.Rel.t -> int -> int
+
 (** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an]
     for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
     accordingly indexes in [an],...,[a1] and [c]. In terms of typing, if
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a0d2da863..d44dcf10d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -725,7 +725,7 @@ let find_positions env sigma t1 t2 =
     let hd1,args1 = whd_all_stack env sigma t1 in
     let hd2,args2 = whd_all_stack env sigma t2 in
     match (kind_of_term hd1, kind_of_term hd2) with
-      | Construct (sp1,_), Construct (sp2,_)
+      | Construct ((ind1,i1 as sp1),u1), Construct (sp2,_)
           when Int.equal (List.length args1) (constructor_nallargs_env env sp1)
             ->
 	  let sorts' =
@@ -734,11 +734,14 @@ let find_positions env sigma t1 t2 =
           (* both sides are fully applied constructors, so either we descend,
              or we can discriminate here. *)
 	  if eq_constructor sp1 sp2 then
-	    let nrealargs = constructor_nrealargs_env env sp1 in
-	    let rargs1 = List.lastn nrealargs args1 in
-	    let rargs2 = List.lastn nrealargs args2 in
+	    let nparams = inductive_nparams_env env ind1 in
+	    let params1,rargs1 = List.chop nparams args1 in
+	    let _,rargs2 = List.chop nparams args2 in
+            let (mib,mip) = lookup_mind_specif env ind1 in
+            let ctxt = (get_constructor ((ind1,u1),mib,mip,params1) i1).cs_args in
+            let adjust i = Vars.adjust_rel_to_rel_context ctxt (i+1) - 1 in
             List.flatten
-	      (List.map2_i (fun i -> findrec sorts' ((sp1,i)::posn))
+	      (List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn))
 		0 rargs1 rargs2)
 	  else if Sorts.List.mem InType sorts'
           then (* see build_discriminator *)
diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v
index a75967411..6abfca4c3 100644
--- a/test-suite/success/Discriminate.v
+++ b/test-suite/success/Discriminate.v
@@ -38,3 +38,10 @@ Abort.
 Goal ~ identity 0 1.
 discriminate.
 Qed.
+
+(* Check discriminate on types with local definitions *)
+
+Inductive A := B (T := unit) (x y : bool) (z := x).
+Goal forall x y, B x true = B y false -> False.
+discriminate.
+Qed.
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index da2183841..78652fb64 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -150,6 +150,13 @@ match goal with
 end.
 Abort.
 
+(* Injection in the presence of local definitions *)
+Inductive A := B (T := unit) (x y : bool) (z := x).
+Goal forall x y x' y', B x y = B x' y' -> y = y'.
+intros * [= H1 H2].
+exact H2.
+Qed.
+
 (* Injection does not project at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.