The Coq mailing list

[gallego AT cri.ensmp.fr (Emilio Jesús Gallego Arias)]

Hello Patricia,

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

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

My guess is that you may want to tweak your definition a bit and use
Definition aux1b ... := nat_ind ...

Definition aux1b n : forall m, n = m -> S n = S m :=
 nat_ind (fun n:nat => (forall m:nat, forall e:n=m, S n = S m))
         (fun m (e:O=m) => (@f_equal nat nat S O m e))
         (fun p (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.

Note that have to write @f_equal due to implicit arguments. You can do a
bit more compactly by leveraging on Coq's type inference:

Definition aux1b n : forall m, n = m -> S n = S m :=
  nat_ind (fun n => forall m, n = m -> S n = S m)
          (fun       m => f_equal S (y:=m))
          (fun n ihn m => f_equal S (y:=m)) n.

Apart from this, IMHO may want to prove your goal using "rewrite"
instead of induction. This would be:

Definition aux1b (n m : nat) (e : n = m) : S n = S m :=
  match e with
  | eq_refl => eq_refl
  end.

or:

Definition aux1b n m : n = m -> S n = S m := @f_equal _ _ S _ m.

or:

Definition aux1b n m : n = m -> S n = S m := f_equal S (y:=m).

It seems is common for non experts to over use induction, indeed, it is
tempting to use it everywhere at the beginning. I take a different
approach: I try to avoid using induction at all costs, either by
encapsulating the induction in the most possible general lemma, or by
tweaking definitions not to be "obviously" recursive.

Best regards,
Emilio