Ssreflect Users Discussion List

[Benjamin Werner <>]

Hello,

I do not know all the tricks of reflect, but I think in this case you  
do not
need the anonymous selection thing.

Just

rewrite f_flat.

should work. If you want to be sure it rewrites precisely
the (f a)  (and not some (f b) ) you can do

rewrite (f_flat a)     ( or rewrite (@f_flat a) if you have
implicit arguments on).


From my understanding, the notation (_ : ee) is for when ee
is the equality statement and not its proof.

You seem to think of some notation (pr : ee) which, I think, is not
provided.


Best wishes,


Benjamin





Le 30 nov. 08 à 09:50, <> a écrit :

> Hello.
>
> I have a question about subgoal generating rewrite tactics.
> Is there a better way of do a similar thing to below?
>
>  Require Import ssreflect.
>
>  Variable f: nat -> nat.
>
>  Axiom  f_flat: forall a, a = 0 -> f a = 0.
>
>  Goal forall a, a*a = 0 -> f a + 1 = 1 .
>  move => a ha.
>  rewrite (_ : f_flat a _).
>
> The last line does not work.
> What I want is to rewrite the goal to "0 + 1 = 1"
> and generate subgoal "a = 0",
> although I somehow feel I am messing up something.
>
> By the way, the link to this mailing list from
> http://www.msr-inria.inria.fr/Projects/math-components
> seems broken; it refers to http instead of https.
>
>
> With best regards,
> Keiko