Ssreflect Users Discussion List

[Georges Gonthier <>]

Hi,
 Just to add a little to Benjamin's response: there's nothing special about 
(_ : ee): it's just a very incomplete proof of the equality ee. You're at 
liberty to supply a more complete proof by writing (pr : ee), though in this 
case I'd rather use the redex selector [tt] to specify what I want to 
rewrite, as this is more "declarative", i.e., in your case,
  rewrite [f a]f_flat.

Best,
  Georges

-----Original Message-----
From: Benjamin Werner [] On Behalf Of Benjamin Werner
Sent: 30 November 2008 09:24
To: Keiko Nakata
Cc: 
Subject: Re: subgoal generating rewrite tactics

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