From b789f40f7616e3a159b43356cb314ff53e329fc9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 1 Nov 2023 19:29:45 +0100 Subject: [PATCH] Followup of #17993, fixes #18239: anomaly on triggering conditions 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-#17993 bug. --- ...lowup-17993-simpl-triggering-condition.rst | 10 +++ pretyping/tacred.ml | 45 ++++++----- test-suite/success/simpl.v | 75 +++++++++++++++++++ 3 files changed, 111 insertions(+), 19 deletions(-) create mode 100644 doc/changelog/04-tactics/18243-master+fix18239-followup-17993-simpl-triggering-condition.rst diff --git a/doc/changelog/04-tactics/18243-master+fix18239-followup-17993-simpl-triggering-condition.rst b/doc/changelog/04-tactics/18243-master+fix18239-followup-17993-simpl-triggering-condition.rst new file mode 100644 index 000000000000..2744494a32a6 --- /dev/null +++ b/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 `_, + fixes `#18239 `_, + by Hugo Herbelin). + +- **Changed:** + :tacn:`simpl` tries to reduce named mutual fixpoints also when they return functions + (`#18243 `_, + by Hugo Herbelin). diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index c44cf9980bf9..a1d349153780 100644 --- a/pretyping/tacred.ml +++ b/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 diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v index 6faf3f026970..03f46046cc48 100644 --- a/test-suite/success/simpl.v +++ b/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.