The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Mon, 3 Jun 2013 10:28:52 -0700,
Valentin ROBERT 
<vrobert AT cs.ucsd.edu>
 a écrit :

> Hello Marcus,
> 
> This pattern is described here:
> http://coq.inria.fr/distrib/8.4/refman/Reference-Manual010.html#hevea_tactic35
> (the "a disjunction of lists of patterns" part is relevant)
> 
> It basically allows you to destruct the introduced element as it is
> being introduced. Here the argument following x seems to be of a type
> with two constructors containing one element each (something like sum
> or sumbool). The syntax is similar to what you can use with the
> tactic destruct for instance.
> 
> It should therefore leave you in a state with two subgoals, each one
> containing a hypothesis H1 accounting for the two possibilities.
> 
> - Valentin

Yes, and there is also a pattern I often use with this feature:

Imagine you have a "P x" hypothesis and your goal is "x = y → P y".

x : X
H : P x
===============
x = y → P y

The proof is trivial, here: "intros Heq; rewrite Heq; exact H." for
instance. But with the destruct feature of intro(s), you can do even
faster: "intros []; exact H."

I think lot of us will discourage you to use this feature. But I find
it often convenient.

Same for "False → P", here you can do "intros []." which is faster (at
least to write) than "discriminate." for instance, and without
wondering if "auto" can or cannot deal with it.