Why rewrite works one way with replace but both way with assert?

Using Rocq
1

Hi,

I noticed difference in the behavior of rewrite tactic.
Code snippets are based on Software Foundation volume 2.

Basically, the rewrite with assert works both ways:

    assert (A1Prime: aeval st a1 = aeval st a1') by (
      subst a1';
      rewrite fold_constants_aexp_sound;
      reflexivity).

    rewrite A1Prime.

Meanwhile rewrite tactic works with replace tactic in the left direction:

    replace (aeval st a1) with (aeval st a1') by
        (subst a1'; rewrite <- fold_constants_aexp_sound; reflexivity).

Default rewrite direction breaks:

    replace (aeval st a1) with (aeval st a1') by
        (subst a1'; rewrite fold_constants_aexp_sound; reflexivity).

Unable to unify “aeval st a1” with “aeval st (fold_constants_aexp (fold_constants_aexp a1))”.

Is there Rocq configuration option that can make these snippets to behave equivalently?

rocq-core9.1-stdlib-9.0.0

2

I guess if you prove an equality you have a = b so rewrite H can apply in a or b so the direction does not matter so much, however, if you work on a then the direction matter as the lemma says H : b = a so rewrite H fails since a is not b but rewrite <- H succeeds as it is the same as rewrite (eq_sym H) with eq_sym H : a = b