Ssreflect Users Discussion List

[Robbert Krebbers <>]

Dear Georges,

thanks a lot for your detailed analysis of the problem.

Could you explain a bit more about the need for the "hack retrofitting 
support for context management into the Coq proof engine API.", possibly 
by an example.

Robbert

On 01/13/2016 06:05 PM, Georges Gonthier wrote:
>    Dear all,
> It is, indeed a bug, but unfortunately not one that can be readily fixed in the ssreflect plugin alone, as 
> the blame is shared between the Coq proof engine, the setoid code, and the ssreflect "in" tactical. 
> Here's  what "do [<tactic>] in <hyps>" does:
>     1) unless there is a *, it replaces the goal with a new manifest constant 
> _the_hidden_goal_
>     2) it discharges (reverts) Hi in <hyps> using forall/let _discharged_Hi_.
>     3) it runs <tactic>
>     4) it introduces the discharged context for each main subgoal derived 
> from the initial goal, and undoes 1); nothing is done for side subgoals.
>    The "tampering" diagnostic indicates step 4) has encountered a goal that 
> has remnants of steps 1) or 2), but no longer has the same shape, which is usually a 
> sign that step 3) has interfered. The check is needed because of the flimsy connection 
> via bound names between the two phases of the tactical, which is a hack retrofitting 
> support for context management into the Coq proof engine API.
>     The "bug" below manifests itself because the setoid implementation does 
> gratuitous alpha-conversion in the goal, erasing any trace of step 2), so that step 4) 
> will either complain if it still detects step 1), or mistake the goal for a side condition 
> (and skip introductions) if there was a *. (To be fair, setoid rewrite in H can only work 
> for goals of the form H -> ... where the bound name is not displayed.)
>      As for the other issues you raise:
>   - It's not obvious to insert introduced definitions in their original positions in the context which 
> <tactic> can modify: using "set " to abbreviate subexpressions is common enough, and 
> forces all introductions to occur at the end (or after the set); even plain rewrite can insert 
> assumption or constants that are lower in the context. We could just try our best, at the expense of 
> underspecifying "in", but I must say that I've often found the current behaviour quite useful 
> in large proofs, as it prevents the assumption(s) you are working on from scrolling out of view.
>   - We use a function provided by the setoid API to determine whether 
> arguments to rewrite are valid relations; it has a history of falling back 
> behind the rest of the setoid library, unfortunately...
>
>      Cheers,
> Georges
>
> -----Original Message-----
> From: 
>
>  
> [mailto:]
>  On Behalf Of Robbert Krebbers
> Sent: 13 January 2016 14:44
> To: 
>
> Subject: Re: [ssreflect] [rewrite foo in hyp] weirdness
>
> Dear Emilio,
>
> Thanks for your reply.
>
> On 01/13/2016 01:16 PM, Emilio Jesús Gallego Arias wrote:
> > However it has some particularities, as your next example shows:
> >
> > > > rewrite H1 in H2.
> > > > (* Error: tampering with discharged assumptions of "in" tactical *)
> > This may be avoided using:
> >
> > > > rewrite H1 in H2 *.
> > The manual does a better job than I could ever do in explaining "in *".
>   From the ref man:
>
>     The operation described by tactic is
>     performed in the facts listed in ident +
>     and in the goal if a * ends the list.
>
> I do not necessarily want the rewrite to be performed in the goal as well, so 
> always using * seems not to be the solution.
>
> As Assia remarked here
> https://github.com/math-comp/math-comp/issues/16#issuecomment-171295569
> , it is probably a bug.
>
> Best,
>
> Robbert