The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Try "remember <your complex expression> as n" before doing "induction n".
What it essentially does is :

set (n := your complex expression) in *;
assert (Heqn : n = your complex expression); [reflexivity|];
clearbody n.

Stéphane L.

On Tue, Apr 14, 2009 at 2:44 PM, dimitrisg7 
<dvekris AT hotmail.com>
 wrote:
>
> I want to have an induction on an complex expression, which is of type nat.
> But I also want to have a hypothesis during my induction process that would
> say that my complex expression is equal to "n" ("n" is used by Coq for the
> induction). Case_eq does that. Unfortunately I do not want a simple case
> analysis, but an induction schema as well.
>
> Thanks!
> --
> View this message in context: 
> http://www.nabble.com/About-induction-tp23038763p23038763.html
> Sent from the Coq mailing list archive at Nabble.com.
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.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
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06