The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

On Thursday 01 April 2010 21:40:23 Z wrote:
> 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.

Hi,

In addition to the other reply, you can use the "Show Proof" command to see 
what the tactic you just called contributed to the proof to help you 
understand how that tactic behaves e.g.

Goal forall n, n = n + 0.
Show Proof.
induction n.
Show Proof.
Admitted.

Goal forall n, n = n + 0.
Show Proof.
intros.
Show Proof.
induction n.
Show Proof.
Admitted.

You can see from the above that the partial proofs generated from each proof 
attempt are the same.

Bye,

Sean Wilson