The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 12/02/2015 12:37 PM, Patricia Peratto wrote:
> I want to prove (using nat_ind) the following proposition.
> I adjoin the proof I have written myself.
>
> Definition aux1b (n:nat) : forall m:nat,
> forall (e:n=m),S n = S m.
> nat_ind (fun n:nat =>
> (forall m:nat, forall e:n=m, S n = S m))

In the above, you initiated proof mode - by ending the Definition spec 
with a "." without assigning it a body (as with ":=").  In that case, 
Coq expects that the next symbol will be a tactic name, not a lemma name 
- they are in separate name spaces.

-- Jonathan

> (fun m:nat, fun e:O=m,
> (f_equal nat nat S O m e))
>
> (fun p:nat, fun q:(forall m:nat,
> forall e:p = m, S p = S m) =>
> (fun m2:nat =>
> (fun e2:(S p)=m2 =>
> (f_equal nat nat S (S p) m2 e2))))
> n.
>
> I have proved it using "induction" but I want to
> find the proof using nat_ind.
>
> I have gotten the following message:
>
> Error: The reference nat_ind was not found in the current environment.
>
> Someone can say me where I'm wrong?
>
> Regards
>
> Patricia