Proof of the closed form formula for triangular numbers

triangular.v

Require Import Coq.Arith.Div2.
Require Import Coq.Arith.Mult.
Require Import Coq.Arith.Even.
Require Import ArithRing.

Fixpoint triangular (n: nat) :=
  match n with
  | 0 => 0
  | S n => (S n) + triangular (n)
  end.

Definition triangular_closed (n: nat) :=
  div2(n*(n+1)).

Lemma sqr_add_even : forall (n: nat), even (n*n+n).

Proof.
  intros.
  destruct even_or_odd with (n := n).
    (* even *)
    apply even_even_plus.
    apply even_mult_l.
    assumption.
    assumption.
    (* odd *)
    apply odd_even_plus.
    apply odd_mult.
    assumption.
    assumption.
    assumption.
Qed.

Lemma sqr_add_eq_dist : forall (n: nat), n*n+n = n*(n+1).

Proof.
  intros.
  ring.
Qed.

Lemma div2_even_plus : forall (n m: nat), even n -> even m ->
  div2 (n + m) = div2 n + div2 m.

Proof.
  intros n m.
  apply ind_0_1_SS with 
    (P := fun n => even n -> even m -> div2 (n + m) = div2 n + div2 m).
    (* start 0 *)
    trivial.
    (* start 1 *)
    intros even_1.
    exfalso.
    apply not_even_and_odd with (n := 1).
    exact even_1.
    apply odd_S.
    apply even_O.
    (* step *)
    clear.
    intros n IH0 even_SSN even_m.
    assert (even n) as even_n.
    apply even_plus_even_inv_r with (n := 2) (m := n).
    trivial.
    apply even_S; apply odd_S; apply even_O.
    assert (div2 (n + m) = div2 n + div2 m) as IH.
    apply IH0.
    exact even_n.
    exact even_m.
    clear IH0.
    rewrite -> plus_Sn_m;rewrite -> plus_Sn_m.
    (* Move S outside of LHS *)
    assert (div2 (n + m) = div2 (S (n + m))) as splitl0.
    apply even_div2.
    apply even_even_plus. exact even_n. exact even_m.
    assert (S (div2 (S (n + m))) = div2 (S(S (n + m)))) as splitl1.
    apply odd_div2.
    apply odd_S.
    apply even_even_plus. exact even_n. exact even_m.
    assert (S (div2 (n + m)) = div2 (S (S (n + m)))) as splitl.
    rewrite splitl0.
    exact splitl1.
    clear splitl0 splitl1.
    (* Move S outside of RHS *)
    assert (div2 n = div2 (S n)) as splitr0.
    apply even_div2.
    exact even_n.
    assert (S (div2(S n)) = div2 (S (S n))) as splitr1.
    apply odd_div2.
    apply odd_S.
    exact even_n.
    assert (S (div2 n) = div2 (S (S n))) as splitr.
    rewrite splitr0.
    exact splitr1.
    clear splitr0 splitr1.
    (* Final rewrites *)
    rewrite <- splitl.
    rewrite <- splitr.
    rewrite plus_Sn_m.
    f_equal.
    exact IH.
Qed.

Theorem triangular_closed_form :
 forall n, triangular n = triangular_closed n.

Proof.
  intros.
  apply nat_ind with
    (P := fun n => triangular n = triangular_closed n).
    clear n.
    (* Induction start*)
    assert (triangular 0 = 0).
    unfold triangular.
    exact eq_refl.
    assert (triangular_closed 0 = 0).
    unfold triangular_closed.
    assert ((0*(0+1)) = 0).
    apply mult_0_l.
    apply f_equal with (y := 0).
    exact H0.
    apply eq_trans with (y := 0).
    exact H.
    apply eq_sym.
    exact H0.
    (* Induction step *)
    clear n.
    intros.
    change (S n + triangular n = triangular_closed (S n)).
    unfold triangular_closed.
    assert (S n + triangular n = S n + triangular_closed n).
    apply f_equal with (y := triangular_closed n).
    exact H.
    apply eq_trans with (y := S n + triangular_closed n).
    exact H0.
    clear H0.
    unfold triangular_closed.
    clear H.
    assert ((2 * (S n) + n * (n + 1)) = (S n) * (S n + 1))
      as double_eq.
    ring.
    assert (div2 (2 * (S n) + n * (n+1)) = div2 ((S n) * (S n + 1)))
      as undist_eq.
    apply f_equal with (f := fun n => div2 n).
    exact double_eq.
    clear double_eq.

    assert (even (n*(n+1))) as is_even.
    rewrite <- sqr_add_eq_dist.
    apply sqr_add_even.

    assert (div2 (2 * S n) + div2 (n * (n + 1)) = div2 (S n * (S n + 1)))
      as dist_eq.
    rewrite <- div2_even_plus.
    exact undist_eq.
    firstorder.
    exact is_even.
    clear undist_eq.
    rewrite div2_double in dist_eq.
    exact dist_eq.
Qed.