Followup of coq#17993, fixes coq#18239: anomaly on triggering conditi…

…ons for simpl.

We ensure that there are enough arguments in the original applied
constant, in addition to ensuring enough arguments in the constant
that immediately surrounds a global mutual fixpoint.

This incidentally fixes a pre-coq#17993 bug.

doc/changelog/04-tactics/18243-master+fix18239-followup-17993-simpl-triggering-condition.rst

@@ -0,0 +1,10 @@
+- **Fixed:**
+  Anomaly of :tacn:`simpl` on partially applied named mutual fixpoints
+  (`#18243 <https://github.com/coq/coq/pull/18243>`_,
+  fixes `#18239 <https://github.com/coq/coq/issues/18239>`_,
+  by Hugo Herbelin).
+
+- **Changed:**
+  :tacn:`simpl` tries to reduce named mutual fixpoints also when they return functions
+  (`#18243 <https://github.com/coq/coq/pull/18243>`_,
+  by Hugo Herbelin).

pretyping/tacred.ml

@@ -233,7 +233,7 @@ let compute_fix_reversibility sigma labs args fix =
     labs;
   typed_reversible_args, nlam, nargs
 
-let check_fix_reversibility env sigma ref u labs args refs ((lv,i),_ as fix) =
+let check_fix_reversibility env sigma ref u labs args minarg refs ((lv,i),_ as fix) =
   let li, nlam, nargs = compute_fix_reversibility sigma labs args (mkFix fix) in
   let k = lv.(i) in
   let refolding_data = {
@@ -247,13 +247,13 @@ let check_fix_reversibility env sigma ref u labs args refs ((lv,i),_ as fix) =
       EliminationFix (n-p+1,(li,n))
 *)
       EliminationFix {
-        trigger_min_args = nlam;
+        trigger_min_args = max minarg nlam;
         refolding_target = ref;
         refolding_data;
         }
   else
     EliminationFix {
-        trigger_min_args = nlam - nargs + k + 1;
+        trigger_min_args = max minarg (nlam - nargs + k + 1);
         refolding_target = ref;
         refolding_data;
         }
@@ -305,42 +305,49 @@ let deactivate_delta allowed_reds =
   (* Act both on Delta and transparent state as not all reduction functions work the same *)
   RedFlags.(red_add_transparent (red_sub allowed_reds fDELTA) TransparentState.empty)
 
-(* [compute_consteval] expands and refolds an arbitrary long sequence
-   of reversible constants for unary fixpoints but consider the last
-   constant before revealing a Fix if the latter is mutually defined *)
+(* [compute_consteval] stepwise expands an arbitrary long sequence of
+    reversible constants, eventually refolding to the initial constant
+    for unary fixpoints and to the last constant encapsulating the Fix
+    for mutual fixpoints *)
 
 let compute_consteval allowed_reds env sigma ref u =
   let allowed_reds_no_delta = deactivate_delta allowed_reds in
-  let rec srec env n labs lastref lastu onlyproj c =
-    let c',l = whd_stack_gen allowed_reds_no_delta env sigma c in
+  let rec srec env all_abs lastref lastu onlyproj c =
+    let c', args = whd_stack_gen allowed_reds_no_delta env sigma c in
+    (* We now know that the initial [ref] evaluates to [fun all_abs => c' args] *)
+    (* and that the last visited name in the evaluation is [lastref] *)
     match EConstr.kind sigma c' with
-      | Lambda (id,t,g) when List.is_empty l && not onlyproj ->
+      | Lambda (id,t,g) when not onlyproj ->
+          assert (List.is_empty args);
           let open Context.Rel.Declaration in
-          srec (push_rel (LocalAssum (id,t)) env) (n+1) (t::labs) lastref lastu onlyproj g
+          srec (push_rel (LocalAssum (id,t)) env) (t::all_abs) lastref lastu onlyproj g
       | Fix ((lv,i),(names,_,_) as fix) when not onlyproj ->
+          let n_all_abs = List.length all_abs in
           let nbfix = Array.length lv in
           (if nbfix = 1 then
+            (* Try to refold to [ref] *)
             let names = [|Some (ref,u)|] in
-            try check_fix_reversibility env sigma ref u labs l names fix
+            try check_fix_reversibility env sigma ref u all_abs args n_all_abs names fix
             with Elimconst -> NotAnElimination
           else
-            let labs, l, names = invert_names allowed_reds env sigma lastref lastu names i in
-            try check_fix_reversibility env sigma lastref lastu labs l names fix
+            (* Try to refold to [lastref] *)
+            let last_labs, last_args, names = invert_names allowed_reds env sigma lastref lastu names i in
+            try check_fix_reversibility env sigma lastref lastu last_labs last_args n_all_abs names fix
             with Elimconst -> NotAnElimination)
-      | Case (_,_,_,_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n
-      | Case (_,_,_,_,_,d,_) -> srec env n labs lastref lastu true d
-      | Proj (p, d) when isRel sigma d -> EliminationProj n
+      | Case (_,_,_,_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases (List.length all_abs)
+      | Case (_,_,_,_,_,d,_) -> srec env all_abs lastref lastu true d
+      | Proj (p, d) when isRel sigma d -> EliminationProj (List.length all_abs)
       | _ when isTransparentEvalRef env sigma (RedFlags.red_transparent allowed_reds) c' ->
-          (* Forget all \'s and args and do as if we had started with c' *)
+          (* Continue stepwise unfolding from [c' args] *)
           let ref, u = destEvalRefU sigma c' in
           (match reference_opt_value env sigma ref u with
             | None -> NotAnElimination (* e.g. if a rel *)
-            | Some c -> srec env n labs ref u onlyproj (applist (c,l)))
+            | Some c -> srec env all_abs ref u onlyproj (applist (c, args)))
       | _ -> NotAnElimination
   in
   match reference_opt_value env sigma ref u with
     | None -> NotAnElimination
-    | Some c -> srec env 0 [] ref u false c
+    | Some c -> srec env [] ref u false c
 
 let reference_eval allowed_reds env sigma ref u =
   match ref with

test-suite/success/simpl.v

@@ -189,3 +189,78 @@ match goal with [ |- g a c n = g a c n ] => idtac end.
 Abort.
 
 End WithLetMutual.
+
+Module IotaTrigger1.
+
+Definition a x := match x with true => tt | false => tt end.
+Definition b x (y : unit) := a x.
+Definition c x := b x tt.
+Goal a true = tt. simpl. match goal with [ |- tt = tt ] => idtac end. Abort.
+Goal b true = fun _ => tt. simpl. match goal with [ |- b true = _ ] => idtac end. Abort.
+Goal c true = tt. simpl. match goal with [ |- tt = tt ] => idtac end. Abort.
+
+End IotaTrigger1.
+
+Module IotaTrigger2.
+
+Definition a x := match x with true => fun _ => tt | false => fun _ => tt end tt.
+Definition b x (y : unit) := a x.
+Definition c x := b x tt.
+Goal a true = tt. simpl. match goal with [ |- tt = tt ] => idtac end. Abort.
+Goal b true = fun _ => tt. simpl. match goal with [ |- b true = _ ] => idtac end. Abort.
+Goal c true = tt. simpl. match goal with [ |- tt = tt ] => idtac end. Abort.
+
+End IotaTrigger2.
+
+Module IotaTrigger3.
+
+Fixpoint f_fix_fun n := match n with 0 => fun _ : unit => true | S n => f_fix_fun n end.
+Definition test_fix_fun n := f_fix_fun n.
+Goal test_fix_fun 2 = fun _ => true. simpl. match goal with [ |- (fun _ => true) = _ ] => idtac end. Abort.
+Goal forall x, test_fix_fun (S x) = fun _ => true. intro. simpl. match goal with [ |- test_fix_fun x = _ ] => idtac end. Abort.
+(* REDUCED *)
+
+Definition test_fix_fun_partial n (x:unit) := f_fix_fun n.
+Goal test_fix_fun_partial 2 = fun _ _ => true. simpl. match goal with [ |- test_fix_fun_partial 2 = _ ] => idtac end. Abort.
+Goal forall x, test_fix_fun_partial (S x) = fun _ _ => true. intro. simpl. match goal with [ |- test_fix_fun_partial (S x) = _ ] => idtac end. Abort.
+(* NOT REDUCED: design choice that it is not enough fully applied to trigger the reduction *)
+(* remark: the presence of an inner "fun" does not matter *)
+
+Fixpoint f_fix n := match n with 0 => fun _ : unit => true | S n => f_fix n end.
+Definition test_fix n := f_fix n tt.
+Goal test_fix 2 = true. simpl. match goal with [ |- test_fix 2 = _ ] => idtac end. Abort.
+Goal forall x, test_fix (S x) = true. intro. simpl. match goal with [ |- test_fix (S x) = _ ] => idtac end. Abort.
+(* NOT REDUCED: design choice that we couldn't refold to test_fix after reduction *)
+
+Fixpoint f_mutual_fix n := match n with 0 => true | S n => g n end
+with g n := match n with 0 => true | S n => f_mutual_fix n end.
+Definition test_mutual_fix n := f_mutual_fix n.
+Goal test_mutual_fix 2 = true. simpl. match goal with [ |- true = _ ] => idtac end. Abort.
+Goal forall x, test_mutual_fix (S x) = true. intro. simpl. match goal with [ |- g x = _ ] => idtac end. Abort.
+(* REDUCED: design choice that mutual fixpoints refold to last encapsulating name *)
+
+Definition test_mutual_fix_partial n (x:unit) := f_mutual_fix n.
+Goal test_mutual_fix_partial 2 = fun _ => true. simpl. match goal with [ |- test_mutual_fix_partial 2 = _ ] => idtac end. Abort.
+Goal forall x, test_mutual_fix_partial (S x) = fun _ => true. intro. simpl. match goal with [ |- test_mutual_fix_partial (S x) = _ ] => idtac end. Abort.
+(* NOT REDUCED: design choice that it is not enough fully applied to trigger the reduction *)
+(* Moreover, was failing between #17993 and #18243 (see #18239) *)
+
+Fixpoint f_mutual_fix_cut n := match n with 0 => fun _ : unit => true | S n => g_cut n end
+with g_cut n := match n with 0 => fun _ : unit => true | S n => f_mutual_fix_cut n end.
+Definition test_mutual_fix_cut n := f_mutual_fix_cut n tt.
+Goal test_mutual_fix_cut 2 = true. simpl. match goal with [ |- true = _ ] => idtac end. Abort.
+Goal forall x, test_mutual_fix_cut (S x) = true. intro. simpl. match goal with [ |- g_cut x tt = _ ] => idtac end. Abort.
+(* REDUCED: by consistency with test_mutual_fix, which itself already differs from the case of a unary fix (new behavior from #18243) *)
+
+Definition test_mutual_fix_cut_partial n (x:unit) := f_mutual_fix_cut n x.
+Goal test_mutual_fix_cut_partial 2 = fun _ => true. simpl. match goal with [ |- test_mutual_fix_cut_partial 2 = _ ] => idtac end. Abort.
+Goal forall x, test_mutual_fix_cut_partial (S x) = fun _ => true. intro. simpl. match goal with [ |- test_mutual_fix_cut_partial (S x) = _ ] => idtac end. Abort.
+(* NOT REDUCED: by consistency with test_fix_fun_partial and test_mutual_fix_cut_partial *)
+(* Moreover was failing before #18243 (see #18239) *)
+
+Definition f_case n := match n with 0 => fun _ : unit => true | S n => fun _ => true end.
+Definition test_case n := f_case n tt.
+Goal test_case 2 = true. simpl. match goal with [ |- true = _ ] => idtac end. Abort.
+(* REDUCED *)
+
+End IotaTrigger3.