The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

On Mon, Dec 13, 2010 at 10:30:55AM +0100, Daniel de Rauglaudre wrote:
> Hi,
> 
> On Mon, Dec 13, 2010 at 05:26:01AM +0100, Jean-Francois Monin wrote:
> 
> > It is also a good opportunity to interpret this as a concrete
> > application of Curry-Howard.  Making the induction over a quantified
> > formula is more than a trick [...]
> 
> I suppose you say that because I used:
>    intros a b; generalize a; generalize b; clear ?

Yes. A recent and convenient tactic to get the same effect is revert. 
Something like
  intros a b; revert a; induction b etc.

> 
> [...]
> 
> > fix 2 (* better practice: use "refine", but I'm lazy *).
> 
> So, "fix 2" does the same trick?

Forgot to explain fix 2 : it is an undocumented tactic 
for a reason you will better understand by trying it. 
The bottom line is roughly:
  induction H = generalize H + fix 1 + destruct.
The tactic fix n allows you to use the function-theorem you are defining
in the body, provided you call it with a structurally smaller 
nth argument (here = 2). 
You have to know what you are doing, and some tactics like auto
become dangerous. If you forget the guard condition 
(and auto will happily forget it), you will "finish" the proof
and Qed will "surprisingly" refuse your attempt.
A useful command to know is "Guarded", to be used after a suspicious
recursive call for instance.
Refine has not this drawback, but it is heavier.

> I did not know "fix" nor "refine". I am looking at them.
> 
> But is not "refine" difficult to use, since you must give the explicit
> lambda term of the proof.

Only for the first step.

> 
> And why "fix 2" is a so bad practice?

It is a common opinion, see above why.  Matter of taste...
I prefer to be explicit with uses of induction hypotyheses
in my scripts, but when dealing with large inductive types
it can be tedious, here induction + automation is more convenient.

JF