coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jean-Francois Monin <jean-francois.monin AT imag.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] an awkward question about "case" tactic
- Date: Tue, 10 Feb 2015 18:11:23 +0100
- Mailscanner-null-check: 1424193086.00509@C5xyv+hvbcl0crS8QPtU2g
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
- [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.