Ssreflect Users Discussion List

[Georges Gonthier <>]

  Hello,

 First, the ":" tactical works with apply (p. 27 of the manual), with a 
special behaviour of matching (p. 29). You can write
   apply: a1a2 h.
The linear use of assumptions in ":" only applies to variables; to keep, 
e.g., h, you can write (bottom of p. 28)
   apply: a1a2 (h).
The ":" tactical is essentially "generalize", just as "=>" is "intros"; 
"move" is basically "idtac", a placeholder on which ":" and "=>" are grafted 
(p. 25). You can use views (p. 55) to generalize after application:
   move/a1a2: h.
or to generalize a specialized version (p. 56)
   move/(_ h): a1a2.
The former clears h, and the latter would clear a1a2 if it were a proof 
assumption. When you don't want any clears, I recommend using the forward 
chaining tactic "have" (pp. 40 - 41)
   have:= a1a2 h.

Best,
  Georges


-----Original Message-----
From:  []
Sent: 24 June 2008 12:15
To: 
Subject: apply [term] + move

Hello.

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.

In fact, I could do equivalently:

Goal al a1 -> al a2.
intro h. move: h; apply a1a2

But I prefer the former since it manifests
that the application of a1a2 consumes h with the consice syntax.

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.

The semantics I envisage is:

Goal al a1 -> al a2.
intro h. generalize (a1a2 h); clear h.

While it does not use move, the behavior appears similar to me,
that is, the generalization of a1a2 consumes h.

I often do forward reasoning where I use this pattern.
I hope this is not against the design principles of ssr :-)

With best regards,
Keiko