The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

On 12/02/2015 06: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.

aux1b is an instance of a much more general result
which derives from the inductive definition of
(Leibniz) equality "=". "=" is itself a notation for

      eq : forall X : Type, X -> X -> Prop)

Fact f__equal X Y (f : X -> Y) (n m : X) : n = m -> f n = f m.
Proof.
  induction 1; reflexivity.
Qed.

or using eq_ind directly

Fact f__equal X Y (f : X -> Y) (n m : X) : n = m -> f n = f m.
Proof.
  apply eq_ind with (P := fun y => f n = f y).
  reflexivity.
Qed.

or by pattern matching (which is how eq_ind/eq_rect are defined)

Definition f__equal X Y (f : X -> Y) (n m : X) (H : n = m) : f n = f m :=
  match H with
    eq_refl => @eq_refl _ (f n)
  end.

Regards,

Dominique