Ssreflect Users Discussion List

[Enrico Tassi <>]

On Thu, Apr 17, 2014 at 11:39:00AM +0200, Ralf Jung wrote:
> In the first proof, this results in three goals being opened instead of
> two, so the "first" tactical selects a different goal in the newer
> version, which breaks the script.

Hello Ralf, indeed version 1.5 behaves differently w.r.t. version 1.4 in
this case.  I'm sorry for the incompatibility, but I believe the new
behavior is the correct one.  If you have a huge codebase, I can offer a
retro compatibility flag to let you migrate less painfully (a 1.5pl1 is
already on its way, so adding one boolean flag is not going to be a
problem).

Now the explanation.  Ssr always played "safe" with evars: no ssr tactic
is supposed to instantiate already existing evars, nor to create new
evars and leave them in a generated goal.
I think you already encountered the phenomenon, since your second apply
is not followed by ":" hence you are calling standard Coq apply to use
an hypothesis of type "P w'" on a goal like "P ?57".

Your stripped lemma is so stripped that is hard for me to suggest how
to reformulate things, but I'll try anyway:

> Goal forall (P:prop) (w w':world), wle w w' -> P w ->
>    (forall (w : world), P w -> forall (w' : world), wle w w' -> P w') -> 
>     P w'.
> Proof.
> move => P w w' H_wle HP.

The lemma you want to use on "P w'" has type "forall x, P x -> forall y,
wle x y -> P y".  By unifying the conclusion of the lemma with the goal
one fixes y to w' but not x, hence the evar.  You can pass a value for x
explicitly as in:

  move=> Pmono; apply: (Pmono w).

or you can pass HP (of type "P w") explicitly 

  move=> Pmono; apply: (Pmono _ HP).

Note that if Pmono is a lemma, you can declare x as implicit, and hence
pass HP directly:

  apply: (Pmono HP).

Or use apply: with multiple argument and let it pad _ for you:

  apply: Pmono HP _ _.  (* that is expanded to apply: Pmono _ HP _ _. *)

I think that the rule of thumb is to state lemmas so that you can
use them easily.  If a lemma is meant to be applied then make the
assumption that is most likely to be available in your context the first
one, so that you can pass it explicitly and fix all arguments not fixed
by the unification of the lemma conclusion with the goal.

I think you could also try to use the lemma Pmono as a view.
For example you can specialize Pmono with

  move/Pmono: HP.

You can also chain lemmas as views, for example this solves your goal

  apply/Pmono/H_wle/HP.  (* add one at a time to see what happens *).

> by apply; first by apply HP.

One last thing: the leading "by" applies to the whole line, and "by
apply" is very much like "exists". 

I've probably put too much on your plate, don't be afraid to ask for
more explanations.

Ciao
-- 
Enrico Tassi