coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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?
- [Coq-Club] an awkward question about "case" tactic, Matej Kosik, 02/10/2015
- Re: [Coq-Club] an awkward question about "case" tactic, Jonathan Leivent, 02/10/2015
- Re: [Coq-Club] an awkward question about "case" tactic, Jean-Francois Monin, 02/10/2015
- Re: [Coq-Club] an awkward question about "case" tactic, Frederic Chyzak, 02/10/2015
- Re: [Coq-Club] an awkward question about "case" tactic, Enrico Tassi, 02/11/2015
- Re: [Coq-Club] an awkward question about "case" tactic, Jonathan Leivent, 02/10/2015
Archive powered by MHonArc 2.6.18.