The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

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?