The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thu, Nov 3, 2011 at 2:46 PM, Edward Z. Yang <ezyang AT mit.edu> wrote:

OK, I could see how that works.  But barring a major benefit I would
probably not bother with cop' then, and always write out my equalities
in the long form...

Edward

You might also look at the "dependent induction" tactic, which in many cases can do the appropriate generalizations and generating equalities.  My (somewhat silly) example:

Require Import Program.

Lemma le_respects_S_conv: forall m n:nat,
  S m <= S n -> m <= n.
Proof.
intros.
dependent induction H.
  constructor 1.

  destruct n.
    inversion H.

    constructor 2; apply IHle; trivial.
Qed.
-- 
Daniel Schepler