The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Hello,

when using the [rewrite] or [replace] tactic, new subgoals may be 
generated. These subgoals appear _after_ the current goal, instead of 
_before_ the new goal. This is rather awkward if one intends to write 
structured proof scripts. Consider:

  Require Import NPeano.
  Goal forall x y z : nat,
    x < y -> z + ((1 + y) + (x - (1 + y))) = x + z.
  intros x y z Hxy.
  rewrite <-Minus.le_plus_minus.
  (* 1st goal: [z + x = x + z],
       the goal in which the rewrite has been performed
     2nd goal: [1 + y <= x],
       the side condition of the rewrite *)

Since the subgoal for the side condition of the rewrite justifies the 
rewrite, it is much natural for it to appear first. That way, it is 
straight below the rewrite in the proof script. Especially when having 
multiple rewrites, the current behavior gives incomprehensible proof 
scripts, and having the subgoal for the side condition first would 
improve that a lot.

Besides, this behavior is inconsistent with other tactics as [assert] 
and [destruct], which put subgoals for their side conditions first. 
Also, it does not combine nicely with brackets in proof scripts. When 
performing a [destruct] I often write:

  destruct foo as [bar baz baq].
  { intros. (* prove side condition here *) }

whereas for rewrite that's not possible as the subgoals appear in the 
"wrong" order.

Is there any reason for this behavior, apart from backwards 
compatibility? Or is there a flag to change it?

Cheers,

Robbert

PS: I know of "[rewrite foo by tac]" but then I have to write the whole 
proof of the side condition using a single tactic.