Ssreflect Users Discussion List

[Maxime Dénès <>]

On 04/17/2014 12:37 PM, Enrico Tassi wrote:
> 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 guess Enrico meant "exact" here. However, while "by apply: H" and 
"exact: H" are the same, I don't think that "by apply H" and "exact H" are.

Maxime.

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