proof of plus associativity in a single gallina term

plus_assoc.v

Definition plus_assoc : forall a b, a + b = b + a :=
  nat_ind (fun n => forall b, n + b = b + n)
          (nat_ind (fun n => n = n + 0) eq_refl (fun n => eq_S _ _))
          (fun n H b => eq_trans (eq_S _ _ (H b))
            (nat_ind (fun b => S (b + n) = b + S n) 
                     eq_refl 
                     (fun _ => eq_S _ _) b) : S (n + b) = b + S n).

- eq_S : forall x y : nat, x = y -> S x = S y
- nat_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
- eq_trans : forall (A : Type) (x y z : A), x = y -> y = z -> x = z
- eq_refl : forall (A : Type) (x : A), x = x

(*
Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : eq _ x x.
Notation "a = b" := (eq _ a b) (at level 70).
Arguments eq_refl {_ _}.
*)

Definition eq_trans : forall {A : Type} {x y z : A}, x = y -> y = z -> x = z :=
  fun A x y z H1 H2 => match H1 in (_=a) return (a=z->x=z) with eq_refl => fun H=>H end H2.

Definition f_equal : forall {A B : Type} (f : A -> B) {x y : A}, x = y -> f x = f y :=
fun A B f x y H => match H in (_=a) return (f x = f a) with | eq_refl => eq_refl end.

(*
Inductive nat := O : nat | S (n:nat): nat.
Definition plus := fix plus a b :=  match a with | O => b | S a' => S (plus a' b) end.
Notation "a + b" := (plus a b).
*)

Definition nat_ind : forall P : nat -> Prop, P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n :=
  fun P P0 IH => fix F n := match n with O => P0 | S n' => IH n' (F n') end.

Definition plus_assoc : forall a b, a + b = b + a :=
  nat_ind (fun n => forall b, n + b = b + n)
          (nat_ind (fun n => n = n + 0) eq_refl (fun _ => f_equal S))
          (fun n H b => eq_trans (f_equal S (H b))
            (nat_ind (fun b => S (b + n) = b + S n) 
                     eq_refl 
                     (fun _ => f_equal S) b) : S (n + b) = b + S n).