The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

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 ?

Actually, I found that by reading Petar Maksimovic's answer. In the lemma
he proposes, he wrote "forall b a", inverting the natural order "a b". His
proof works only in that order. I found this trick to invert them, allowing
therefore to start with "forall a b".

> fix 2 (* better practice: use "refine", but I'm lazy *).

So, "fix 2" does the same trick?

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?

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

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/