Skip to Content.
Sympa Menu

coq-club - [Coq-Club] an awkward question about "case" tactic

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] an awkward question about "case" tactic


Chronological Thread 
  • From: Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: [Coq-Club] an awkward question about "case" tactic
  • Date: Tue, 10 Feb 2015 16:33:01 +0000

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?



Archive powered by MHonArc 2.6.18.

Top of Page