The Coq mailing list

[James Wilcox <wilcoxjay AT gmail.com>]

Also note that this is provable without induction (your proof doesn't use the induction hypothesis q). For example, it follows directly from f_equal.

Definition aux1b (n : nat) : forall m : nat, forall e : n = m, S n = S m := 

  fun m e => f_equal S e.

On Wed, Dec 2, 2015 at 9:58 AM, Pierre Casteran <pierre.casteran AT labri.fr> wrote:

Perhaps it's just a syntax error, if you put nat_ind at a place where a tactic is expected.

You should try to write something like :

exact (nat_ind ... ...)
or
apply nat_ind with ...
or
intros n; pattern; apply nat_ind.

Pierre

Quoting Patricia Peratto <psperatto AT vera.com.uy>:

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))

(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