The Coq mailing list

["Andrew McCreight" <continuation AT gmail.com>]

Make sure that the goal (and not the hypotheses) has n.  When you apply induction, you want it to look something like this:

t : A
----------------------
forall n, B n -> my_pred n t

If you do "induction t" when n is a hypotheses, then n is fixed for all instances of the induction.


Andrew

On Fri, Oct 24, 2008 at 9:04 AM, Flavio L. C. de Moura <flaviomoura AT unb.br> wrote:

Hello,

  This is probably a simple question, but I didn't manage to solve it...
  I have a binary predicate, say my_pred n t. The first argument is a natural and the second is an term of inductive type. In the induction step I get an _expression_ of the form my_pred (n+1) t' where t' is simpler than t, and hence I can apply the induction hypothesis, but the induction hypothesis refers to the _expression_ my_pred n t'. In a paper and pencil proof this step is trivial, but how can I instruct Coq to apply the induction hypothesis correctly?
Thank you in advance!

Best regards,

Flávio.

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
        http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club