Ssreflect Users Discussion List

[Georges Gonthier <>]

  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