inconsistent results with simpl, cofix, and section variables

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4056
From: @siegebell
Reported version: 8.5
CC: @ppedrot

[coqbot]

Comment author: @siegebell

Depending on whether a variable is provided with a definition or given as a section variable, the results of simpl on a cofix can differ. This happens with both 8.4 and trunk. However, cbn gives consistent results.

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 A.
  CoFixpoint inf_stream1 (x:nat) (n:nat) :=
    scons n (inf_stream1 x (n+x)).
End A.

Section B.
  Variable (x:nat).
  CoFixpoint inf_stream2 (n:nat) :=
    scons n (inf_stream2 (n+x)).
End B.


Goal (forall x n, stream_unfold (inf_stream1 x n) = stream_unfold (inf_stream2 2 n)).
(* simpl exposes the cofix on the rhs but not the lhs *)
simpl.
(* ... inf_stream1 x (n + x))... = ...(cofix inf_stream2 n0 := ...) ... *)
Abort.

[coqbot]

Comment author: @ppedrot

I think that the one sensible answer is: use cbn. The current simpl tactic is going to be deprecated some day anyway.

[herbelin]

Proper fix in #18576.

[herbelin]

For the record, note that cbn does not (yet) refold mutual fixpoints defined with section variables while simpl does in #18576.

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.
(*
(n,
 scons n
   ((cofix mut_stream1 (n0 : nat) : stream :=
       scons n0 (mut_stream2 (n0 + x))
     with mut_stream2 (n0 : nat) : stream :=
       scons n0 (mut_stream1 (n0 + x))
     for
     mut_stream2) (n + x))) =
(n,
 scons n
   ((cofix mut_stream1 (n0 : nat) : stream :=
       scons n0 (mut_stream2 (n0 + x))
     with mut_stream2 (n0 : nat) : stream :=
       scons n0 (mut_stream1 (n0 + x))
     for
     mut_stream1) (n + x)))
*)