Ssreflect Users Discussion List

[Pierre-Yves Strub <>]

Dear all,

While porting some dev. from Coq 8.3 to 8.4, I found a strange behavior 
that I have been able to reduce to the following code.

After the rewrite in the first proof script, the goal is: P (f x + f y 
- f z)

After the rewrite in the second proof script, the goal is:  P (f x + f 
y + f (- z)). Meaning that fB has not been successfully used. (`rewrite 
fB fD' succeeds as expected).

Any hint on that ? I'm using the v8.4 plugin found in the repository 
with Coq 8.4pl2 and the trunk standard library.

Best,
    Pierre-Yves.

Parameter rT : ringType.
Parameter f  : {additive rT -> rT}.
Parameter P  : rT -> Prop.

Lemma fD: {morph f : x y / x + y >-> x + y}.
Proof. by apply raddfD. Qed.

Lemma fB: {morph f : x y / x - y >-> x - y}.
Proof. by apply raddfB. Qed.

Goal forall x y z, P (f (x + y - z)).
Proof.
  move=> x y z; rewrite !(raddfB, raddfD).
Abort.

Goal forall x y z, P (f (x + y - z)).
Proof.
  move=> x y z; rewrite !(fB, fD).
Abort.