coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] "intros n. induction n." == "induction n."?

From: Z <zell08v AT orange.fr>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] "intros n. induction n." == "induction n."?
Date: Thu, 1 Apr 2010 22:40:23 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=lIfz5rLje6ZIsotYpDM+lhsnMKLxXpc/CjAzfGI4DOaOGcqQpOaif9mjEyRR2qXSnZ r7lfnFd+sqYziYiE463izE43AuHzcuzZv3TyDWB4fAzZX9c8C3HEYLc/xoNT6t30UQjX 0ioudKcLi6VC8Z6X1r7Yo4loNcXYvoVTGZVPU=

Hello everyone,

I may have a quite superficial question here,

Apparently it makes no difference to put or not put an "intros n"
before "induction n"
Is this affirmation right?

For instance, in the proof below, to remove intros n does not change
anything.

Theorem mytest: forall n: nat, my_eq_nat n n= true.
Proof.
intros n. (* It seems " intros n " is optional here*)
simpl.
induction n.
Show 2.
simpl.
reflexivity.
simpl. rewrite IHn. simpl. reflexivity.
Qed.

Thanks for your ideas.
Z.

[Coq-Club] "intros n. induction n." == "induction n."?, Z
- Re: [Coq-Club] "intros n. induction n." == "induction n."?, Adam Chlipala
- Re: [Coq-Club] "intros n. induction n." == "induction n."?, Sean Wilson