The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Sun, Jul 14, 2013 at 8:47 PM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:

> 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

It seems like that has pretty much the same problem as a simple match
on `x`: I lose interactive mode during the entire pattern matching
process.

> Alternatively, if [a] and [b] don't both solve all the goals, you could do
> something like [case x; (exact a || exact b)].

I'm afraid this doesn't work for two reasons: (1) `a` is a constructor
argument and (2) `exact b` always applies to the goal, but I don't
always want it to.

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

Proof tactics are actually quite useful for building specific (proof
relevant) definitions. It is recommended practice in ITPaPD (the Coq
book by Yves Bertot and Pierre Castéran). The advantage is that you
get continuous feedback about the context while writing. You just have
to be careful with auto-proof-searching tactics if you're implementing
a weak specification.

--
www.mhelvens.net