Merge PR #18243: Followup of #17993, fixes #18239: anomaly on trigger…

…ing conditions for simpl on encapsulated mutual fixpoints

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

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.