Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.

7 files changed, 83 insertions, 26 deletions

diff --git a/CHANGES b/CHANGES
index 289b7d5d2..c9197fb36 100644
--- a/CHANGES
+++ b/CHANGES
@@ -40,6 +40,8 @@ Tactics
 - Added tactic optimize_heap, analogous to the Vernacular Optimize
   Heap, which performs a major garbage collection and heap compaction
   in the OCaml run-time system.
+- The tactics "dtauto", "dintuition", "firstorder" now handle inductive types
+  with let bindings in the parameters.
 
 Focusing
 
diff --git a/engine/termops.ml b/engine/termops.ml
index a71bdff31..40b3d0d8b 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1463,6 +1463,18 @@ let prod_applist sigma c l =
     | _ -> anomaly (Pp.str "Not enough prod's.") in
   app [] c l
 
+let prod_applist_assum sigma n c l =
+  let open EConstr in
+  let rec app n subst c l =
+    if Int.equal n 0 then
+      if l == [] then Vars.substl subst c
+      else anomaly (Pp.str "Not enough arguments.")
+    else match EConstr.kind sigma c, l with
+    | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l
+    | LetIn(_,b,_,c), _ -> app (n-1) (Vars.substl subst b::subst) c l
+    | _ -> anomaly (Pp.str "Not enough prod/let's.") in
+  app n [] c l
+
 (* Combinators on judgments *)
 
 let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
diff --git a/engine/termops.mli b/engine/termops.mli
index c1600abe8..a3559a693 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -159,8 +159,18 @@ val eta_reduce_head : Evd.evar_map -> constr -> constr
 (** Flattens application lists *)
 val collapse_appl : Evd.evar_map -> constr -> constr
 
+(** [prod_applist] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *)
 val prod_applist : Evd.evar_map -> constr -> constr list -> constr
 
+(** In [prod_applist_assum n c args], [c] is supposed to have the
+    form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it
+    returns [c] with the assumptions of [Γ] instantiated by [args] and
+    the local definitions of [Γ] expanded.
+    Note that [n] counts both let-ins and prods, while the length of [args]
+    only counts prods. In other words, varying [n] changes how many
+    trailing let-ins are expanded. *)
+val prod_applist_assum : Evd.evar_map -> int -> constr -> constr list -> constr
+
 (** Remove recursively the casts around a term i.e.
    [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
 val strip_outer_cast : Evd.evar_map -> constr -> constr
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index c55040df0..4c59996aa 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -55,7 +55,8 @@ let ind_hyps env sigma nevar ind largs =
   let types= Inductiveops.arities_of_constructors env ind in
   let myhyps t =
     let t = EConstr.of_constr t in
-    let t1=Termops.prod_applist sigma t largs in
+    let nparam_decls = Context.Rel.length (fst (Global.lookup_inductive (fst ind))).mind_params_ctxt in
+    let t1=Termops.prod_applist_assum sigma nparam_decls t largs in
     let t2=snd (decompose_prod_n_assum sigma nevar t1) in
       fst (decompose_prod_assum sigma t2) in
     Array.map myhyps types
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index a3a3e0a9e..11ac16680 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -111,7 +111,8 @@ let match_with_one_constructor sigma style onlybinary allow_rec t =
 	    Some (hdapp,args)
 	  else None
 	else
-	  let ctyp = Termops.prod_applist sigma (EConstr.of_constr mip.mind_nf_lc.(0)) args in
+          let ctyp = Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt)
+                       (EConstr.of_constr mip.mind_nf_lc.(0)) args in
 	  let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in
 	  if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then
 	    (* Record or non strict conjunction *)
@@ -364,36 +365,39 @@ let is_forall_term sigma c = op2bool (match_with_forall_term sigma c)
 
 let match_with_nodep_ind sigma t =
   let (hdapp,args) = decompose_app sigma t in
-    match EConstr.kind sigma hdapp with
-      | Ind (ind, _)  ->
-          let (mib,mip) = Global.lookup_inductive ind in
-	    if Array.length (mib.mind_packets)>1 then None else
-	      let nodep_constr c = has_nodep_prod_after mib.mind_nparams sigma (EConstr.of_constr c) in
-		if Array.for_all nodep_constr mip.mind_nf_lc then
-		  let params=
-		    if Int.equal mip.mind_nrealargs 0 then args else
-		      fst (List.chop mib.mind_nparams args) in
-		    Some (hdapp,params,mip.mind_nrealargs)
-		else
-		  None
-      | _ -> None
+  match EConstr.kind sigma hdapp with
+  | Ind (ind, _)  ->
+     let (mib,mip) = Global.lookup_inductive ind in
+     if Array.length (mib.mind_packets)>1 then None else
+       let nodep_constr c =
+         has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma (EConstr.of_constr c) in
+       if Array.for_all nodep_constr mip.mind_nf_lc then
+         let params=
+           if Int.equal mip.mind_nrealargs 0 then args else
+             fst (List.chop mib.mind_nparams args) in
+         Some (hdapp,params,mip.mind_nrealargs)
+       else
+         None
+  | _ -> None
 
 let is_nodep_ind sigma t = op2bool (match_with_nodep_ind sigma t)
 
 let match_with_sigma_type sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
-    | Ind (ind, _) ->
-        let (mib,mip) = Global.lookup_inductive ind in
-          if Int.equal (Array.length (mib.mind_packets)) 1 &&
-	    (Int.equal mip.mind_nrealargs 0) &&
-	    (Int.equal (Array.length mip.mind_consnames)1) &&
-	    has_nodep_prod_after (mib.mind_nparams+1) sigma (EConstr.of_constr mip.mind_nf_lc.(0)) then
-	      (*allowing only 1 existential*)
-	      Some (hdapp,args)
-	  else
-	    None
-    | _ -> None
+  | Ind (ind, _) ->
+     let (mib,mip) = Global.lookup_inductive ind in
+     if Int.equal (Array.length (mib.mind_packets)) 1
+        && (Int.equal mip.mind_nrealargs 0)
+        && (Int.equal (Array.length mip.mind_consnames)1)
+        && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) sigma
+             (EConstr.of_constr mip.mind_nf_lc.(0))
+     then
+       (*allowing only 1 existential*)
+       Some (hdapp,args)
+     else
+       None
+  | _ -> None
 
 let is_sigma_type sigma t = op2bool (match_with_sigma_type sigma t)
 
diff --git a/test-suite/bugs/closed/6490.v b/test-suite/bugs/closed/6490.v
new file mode 100644
index 000000000..dcf9ff29e
--- /dev/null
+++ b/test-suite/bugs/closed/6490.v
@@ -0,0 +1,4 @@
+Inductive Foo (A' := I) (B : Type) := foo : Foo B.
+
+Goal Foo True. dtauto. Qed.
+Goal Foo True. firstorder. Qed.
diff --git a/test-suite/success/dtauto-let-deps.v b/test-suite/success/dtauto-let-deps.v
new file mode 100644
index 000000000..094b2f8b3
--- /dev/null
+++ b/test-suite/success/dtauto-let-deps.v
@@ -0,0 +1,24 @@
+(*
+This test is sensitive to changes in which let-ins are expanded when checking
+for dependencies in constructors.
+If the (x := X) is not reduced, Foo1 won't be recognized as a conjunction,
+and if the (y := X) is reduced, Foo2 will be recognized as a conjunction.
+
+This tests the behavior of engine/termops.ml : prod_applist_assum,
+which is currently specified to reduce exactly the parameters.
+
+If dtauto is changed to reduce lets in constructors before checking dependency,
+this test will need to be changed.
+*)
+
+Context (P Q : Type).
+Inductive Foo1 (X : Type) (x := X) := foo1 : let y := X in P -> Q -> Foo1 x.
+Inductive Foo2 (X : Type) (x := X) := foo2 : let y := X in P -> Q -> Foo2 y.
+
+Goal P -> Q -> Foo1 nat.
+solve [dtauto].
+Qed.
+
+Goal P -> Q -> Foo2 nat.
+Fail solve [dtauto].
+Abort.