The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

Hello, 


On Tue, Feb 10, 2015 at 11:37:43AM -0500, Jonathan Leivent wrote:
> 
> On 02/10/2015 11:33 AM, Matej Kosik wrote:
> >Hello,
> >
> >If my context is:
> >
> >     a : nat
> >
> >and my goal is:
> >
> >     (fun c : nat => c + a + a = 42) a
> >
> >then when I use the
> >
> >     case a
> >
> >tactic, the original goal is replaced with the following two subgoals:
> >
> >     0 + a + a = 42
> >
> >     forall n : nat, S n + a + a = 42
> >
> >This effect is plausible;
> >the usefulness of it is documented (e.g. in Coq'Art);
> >but I am not able to explain why "case a" must have in this case this 
> >effect and not some other effect.
> >
> >For example, why doesn't Coq generated the following subgoals instead:
> >
> >     0 + 0 + 0 = 42
> >
> >     forall n : nat, S n + S n + S n = 42
> >
> >?
> >
> >Why is the third occurrence of the free variable "a" in the original goal 
> >treated in a different way than its first and the second occurrences?
> 
> I don't know about the "why" - but you can get around it by using
> [pattern a] before [case a].
> 
> -- Jonathan

This behavior is precisely on purpose, with "pattern" in mind:
the role of pattern is to point out positions where some tactic is
expected to apply using a suitable abstraction: first you get a
(fun x => ... x ... x ...) A,
where occurrences of x are the expected positions;
then the tactic (e.g. rewrite, case, etc.) is applied *on the argument A 
only*, 
followed by a beta reduction.
for instance, if you want perform "case a" on the first occurrence of
  a + a + a = 42
you can type:
pattern a at 1. case a.
The intermediate goal provides your original situation.

JF