coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?
Chronological Thread
- From: Jason Gross <jasongross9 AT gmail.com>
- To: Michiel Helvensteijn <mhelvens AT gmail.com>
- Cc: Adam Chlipala <adamc AT csail.mit.edu>, coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?
- Date: Sun, 14 Jul 2013 14:47:22 -0400
If you can infer which case you're in by the type of your goal, or the existence of certain-shaped hypotheses, then you could do something like
case x;
match goal with
| [ |- <shape of goal 1> ] => exact a
| _ => exact b
end
Alternatively, if [a] and [b] don't both solve all the goals, you could do something like [case x; (exact a || exact b)].
And if you can't infer which case you're in from the shape of your goal, and both [a] and [b] are valid at solving the goal, then I question your use of tactics; I think tactics are most useful when discharging proof-irrelevant goals, i.e., goals where you don't care what valid solution you get, as long as you get some valid solution.
-Jason
On Sunday, July 14, 2013, Michiel Helvensteijn wrote:
On Sunday, July 14, 2013, Michiel Helvensteijn wrote:
On Sun, Jul 14, 2013 at 7:04 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:
> Maybe, though, your problem domain actually admits some simple proof
> automation, such that there's no need to think about case split details
> yourself.
Well, I'll certainly have a look at Chapter 14 (and perhaps earlier
chapters) to see if it fits my situation. Thanks!
In the meantime, if anyone has a direct answer to my question —like a
specific tactic that does what I need— I'd still like to know.
--
www.mhelvens.net
- [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Adam Chlipala, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Adam Chlipala, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Jason Gross, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Jason Gross, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Adam Chlipala, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Adam Chlipala, 07/14/2013
Archive powered by MHonArc 2.6.18.