The Coq mailing list

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

Le Tue, 22 May 2012 17:36:58 +0200,
Paolo Herms 
<paolo.herms AT cea.fr>
 a écrit :

> 
> On Tuesday 22 May 2012 15:19:10 Francois Pottier wrote:
> > > econstuctor (solve [eauto]).
> > > I don't think it's documented; I've found it by idly reading the
> > > Coq source
> > > code.
> > 
> > !!
> 
> Of course, this is documented as part of the tactic language
> http://coq.inria.fr/refman/Reference-Manual012.html

Well, that is ok if your goal is easily solvable.

But when you have something like:

Inductive X : nat → Prop :=
| XO : hard_to_prove_1 → X O
| XS1 : ∀ n, impossible_to_prove n → X (S n)
| XS2 : ∀ n, hard_to_prove_2 n → X (S n)
.

Then if you want to prove "∀ n, X n",

you start doing "induction n."

then:

"constructor. ..."
"constructor 3. ..."

But in this case, you may wish to have a
"induction n; try constructor only_possible_one." tactic which will
perform constructor 1 for the first case, but won't do anything in the
second case, since there are two choices.

Such a tactic could be done in Ocaml, it would count all the cases
where "constructor <n>" succeds and check that only one case is ok.
If many solutions are found, nothing is done and if none, a failure
should be returned.

The interest of such a tactic is to be a non-blocking one; that is
using it won't lead you to a place where you are stuck even if you
weren't in the first place.