The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 07/02/2016 21:44, Daniel Schepler wrote:
> According to https://coq.inria.fr/distrib/V8.5/CHANGES:
> 
> - Tactic "refine" has been changed back to the 8.4 behavior of shelving 
> subgoals
>   that occur in other subgoals. The "refine" tactic of 8.5beta3 has been
>   renamed "simple refine"; it does not shelve any subgoal.
> 
> However, in my experience, refine still behaves differently in Coq 8.5
> than it did in 8.4.  For example:
> 
> Goal forall f : nat -> nat,
>   (forall m n:nat, m <= n -> f m <= f n) ->
>   f 1 <= 5 -> f 0 <= 5.
> Proof.
> intros f fincr f1.
> refine (let H := fincr 0 1 _ in _).
> 
> In 8.4, this would produce two subgoals (Γ |- 0 <= 1; Γ, H : f 0 <= f
> 1 |- f 0 <= 5).  However, in 8.5 it produces a single goal (Γ, H :=
> fincr 0 1 ?existential |- f 0 <= 5).  It seems to get the 8.4 behavior
> back, I need "simple refine (let H := fincr 0 1 _ in _); [|clearbody
> H]", or the same with unshelve refine.
> 
> So, am I completely misunderstanding that CHANGES entry, or is it
> inaccurate?  (I'm using the Debian 8.5-2 packages.)

You are misunderstanding that CHANGES entry; it is accurate; it covers
only one aspect of refine.

What changed (and isn't explained by the CHANGES entry) is that refine
handles let-in differently. In particular, in 8.4, refine was behaving
as if clearbody was called on let-in variables (as you did with your
"simple refine" testcase). This is no longer the case in 8.5. As a
consequence, in 8.5, the variable occurs in other subgoals, contrarily
to 8.4, and thus it is shelved (as it would have been in 8.4, if it had
occurred the same way).

So the relevant CHANGES entry is the following one:

"The refine tactic is changed not to use an ad hoc typing algorithm to
generate subgoals. It also uses the dependent subgoal feature to
generate goals to materialize every existential variable which is
introduced by the refinement (source of incompatibilities)."

Best regards,

Guillaume