The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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