Ssreflect Users Discussion List

[(François Garillot)]

Hello,

 wrote today: 

> Is there a way to combine "apply [term]" and the move tactic ":"
> as in the following example?
>
> Variables a1 a2: nat.
> Variable al: nat -> Prop.
> Axiom a1a2: al a1 -> al a2.
>
> Goal al a1 -> al a2.
> intro h. (apply a1a2): h.

Yes, there is.

As per section 7.2 of the manual:

"Interpreting an assumption in the context of a proof is applying it a
correspondence lemma before generalising, and/or decomposing it. (...)
This operation is so common that the tactic shell has specific syntax for
it. (...)"

The application to your specific example is the following:

Goal al a1 -> al a2.
move => h. move/a1a2: h.

> Furthermore, it would be nice if I could combine "generalize [term]" and 
> move
> as in the following example.
>
> Goal al a1 -> al a2.
> intro h. (generalize a1a2): h.

It seems that what you are looking for is again the interpretation of
assumptions through views. I'd advise you to have a look at section 7.6 of
the manual, in the paragraph starting by 'Interpreting assumptions'.

The current syntax for what you envision seems to be:

Goal al a1 -> al a2.
move=> h. move/a1a2: h.

Or more simply:

Goal al a1 -> al a2.
move/a1a2.

(which simply replaces the named hypothesis h by the implicit default
'top' in the following)

Which 1/ introduces 'top'
      2/ generalises a term of the form (a1a2 top)
      3/ clears 'top'.

Regards,
-- 
François Garillot