Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?

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 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



Archive powered by MHonArc 2.6.18.

Top of Page