The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Tue, 02 Aug 2011 23:04:43 -0700,
S3 
<scubed2 AT gmail.com>
 a écrit :

> 
> Thanks.  That's neat.  I didn't realize you can use
> left and right on things other than \/.  That makes
> for a very short proof.
> 

Ok, so you should be interested by this generalization:

split applies to 1-constructor inductives, that is for instance:
 * A /\ B
 * a = b
 * True
 * point
   (assuming you have defined point as "Record point := {x:ℝ;y:ℝ}.")
 * Acc
 * Stream

left and right apply to 2-constructor inductives
 (left for the first and right for the second)

constructor [n] apply to [m]-constructor inductives (where m≥n)

so that:
* left and split can be replaced by "constructor 1"
* right can be replaced by "constructor 2"

when there is need of some parameter, you can use the
"[constructor-tactic] with [arg(s)]".

So that "exists x." can be replaced by "split with x."


there are also existential versions of these tactics which allow you
to omit the "with" part:
econstructor, eleft, eright, esplit

so that "eexists." can be replaced with "esplit."