Merge PR #18601: Fix refolding of named mutual fix/cofix defined in a…

… section for "cbn"

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

doc/changelog/04-tactics/18601-master+fix17897-cbn-wrong-canonical-name-refolding.rst

@@ -0,0 +1,6 @@
+- **Fixed:**
+  Support for refolding reduced global mutual fixpoints/cofixpoints
+  with parameters in :tacn:`cbn`
+  (`#18601 <https://github.com/coq/coq/pull/18601>`_,
+  fixes part of `#4056 <https://github.com/coq/coq/issues/4056>`_,
+  by Hugo Herbelin).

tactics/cbn.ml

@@ -70,7 +70,7 @@ module Cst_stack = struct
     | _ -> None
 
   let reference sigma t = match best_cst t with
-    | Some (c, _) when isConst sigma c -> Some (fst (destConst sigma c))
+    | Some (c, params) when isConst sigma c -> Some (fst (destConst sigma c), params)
     | _ -> None
 
   (** [best_replace d cst_l c] makes the best replacement for [d]
@@ -435,7 +435,7 @@ let apply_subst env sigma cst_l t stack =
     f x := t. End M. Definition f := u. and say goodbye to any hope
     of refolding M.f this way ...
 *)
-let magically_constant_of_fixbody env sigma reference bd = function
+let magically_constant_of_fixbody env sigma (reference, params) bd = function
   | Name.Anonymous -> bd
   | Name.Name id ->
     let open UnivProblem in
@@ -446,7 +446,7 @@ let magically_constant_of_fixbody env sigma reference bd = function
       match constant_opt_value_in env (cst,u) with
       | None -> bd
       | Some t ->
-        let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in
+        let csts = EConstr.eq_constr_universes env sigma (Reductionops.beta_applist sigma (EConstr.of_constr t, params)) bd in
         begin match csts with
           | Some csts ->
             let addqs l r (qs,us) = Sorts.QVar.Map.add l r qs, us in
@@ -471,7 +471,7 @@ let magically_constant_of_fixbody env sigma reference bd = function
                 csts UVars.empty_sort_subst
             in
             let inst = UVars.subst_sort_level_instance subst u in
-            mkConstU (cst, EInstance.make inst)
+            applist (mkConstU (cst, EInstance.make inst), params)
           | None -> bd
         end
 

test-suite/success/cbn.v

@@ -39,3 +39,35 @@ Proof.
   cbn.
   match goal with |- _ + _ = _ => idtac end.
 Abort.
+
+Module MutualFixCoFixInSection.
+
+Section S.
+Variable p:nat.
+Fixpoint f n := match n with 0 => p | S n => f n + g n end
+with g n := match n with 0 => p | S n => f n + g n end.
+End S.
+
+Goal forall n, f n (S n) = g 0 (S n).
+intros. cbn.
+match goal with [ |- f n n + g n n = f 0 n + g 0 n ] => idtac end.
+Abort.
+
+CoInductive stream {A:Type} : Type :=
+  | scons: A->stream->stream.
+Definition stream_unfold {A} (s: @ stream A) := match s with
+| scons a s' => (a, scons a s')
+end.
+
+Section C.
+Variable (x:nat).
+CoFixpoint mut_stream1 (n:nat) := scons n (mut_stream2 (n+x))
+with mut_stream2 (n:nat) :=  scons n (mut_stream1  (n+x)).
+End C.
+
+Goal (forall x n, stream_unfold (mut_stream1 x n) = stream_unfold (mut_stream2 x n)).
+intros. cbn.
+match goal with [ |- (n, scons n (mut_stream2 x (n + x))) = (n, scons n (mut_stream1 x (n + x))) ] => idtac end.
+Abort.
+
+End MutualFixCoFixInSection.