Proof that Multiplication is commutative

comm.v

Require String. Open Scope string_scope.

Ltac move_to_top x :=
  match reverse goal with
  | H : _ |- _ => try move x after H
  end.

Tactic Notation "assert_eq" ident(x) constr(v) :=
  let H := fresh in
  assert (x = v) as H by reflexivity;
  clear H.

Tactic Notation "Case_aux" ident(x) constr(name) :=
  first [
    set (x := name); move_to_top x
  | assert_eq x name; move_to_top x
  | fail 1 "because we are working on a different case" ].

Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.

Theorem brack_help : forall n m p: nat,
  n + (m + p) = n + m + p.
Proof.
  intros n m p.
  induction n as [| n'].
  Case "n = 0".
    simpl.
    reflexivity.
  Case "n = S n'".
    simpl.
    rewrite -> IHn'.
    reflexivity.
Qed.

Lemma plus_help: forall n m: nat,
  S (n + m) = n + S m.
Proof.
  intros n m.
  induction n as [| n].
  Case "n = 0".
    simpl.
    reflexivity.
  Case "n = S n".
    simpl.
    rewrite -> IHn.
    reflexivity.
Qed.

Theorem mult_0_r : forall n:nat,
  n * 0 = 0.
Proof.
  intros n.
  induction n as [|n'].
  Case "n = 0".
    simpl.
    reflexivity.
  Case "n = S n'".
    simpl.
    rewrite -> IHn'.
    reflexivity.
Qed.

Theorem plus_comm : forall n m : nat,
  n + m = m + n.
Proof.
  intros n m.
  induction n as [| n].
  Case "n = 0".
    simpl.
    rewrite <- plus_n_O.
    reflexivity.
  Case "n = S n".
    simpl.
    rewrite -> IHn.
    rewrite -> plus_help.
    reflexivity.
Qed.

Theorem plus_swap : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.  
  intros n m p.
  rewrite -> brack_help.
  assert (H: n + m = m + n).
    Case "Proof of assertion".
    rewrite -> plus_comm.
    reflexivity.
  rewrite -> H.
  rewrite <- brack_help.
  reflexivity.
Qed.

Lemma mult_help : forall m n : nat,
  m + (m * n) = m * (S n).
Proof.
  intros m n.
  induction m as [| m'].
  Case "m = 0".
    simpl.
    reflexivity.
  Case "m = S m'".
    simpl.
    rewrite <- IHm'.
    rewrite -> plus_swap.
    reflexivity.
Qed.    

Lemma mult_identity : forall m : nat,
 m * 1 = m.
Proof.
  intros m.
  induction m as [| m'].
  Case "m = 0".
    simpl.
    reflexivity.
  Case "m = S m'".
    simpl.
    rewrite -> IHm'.
    reflexivity.
Qed.

Lemma plus_0_r : forall m : nat,
 m + 0 = m.
Proof.
  intros m.
  induction m as [| m'].
  Case "m = 0".
    simpl.
    reflexivity.
  Case "m = S m'".
    simpl.
    rewrite -> IHm'.
    reflexivity.
Qed.

Theorem mult_comm_helper : forall m n : nat,
  m * S n = m + m * n.
Proof.
  intros m n.
  simpl.
  induction n as [| n'].
  Case "n = 0".
    assert (H: m * 0 = 0).
    rewrite -> mult_0_r.
    reflexivity.
    rewrite -> H.
    rewrite -> mult_identity.
    assert (H2: m + 0 = m).
    rewrite -> plus_0_r.
    reflexivity.
    rewrite -> H2.
    reflexivity.
  Case "n = S n'".
    rewrite -> IHn'.
    assert (H3: m + m * n' = m * S n').
    rewrite -> mult_help.
    reflexivity.
    rewrite -> H3.
    assert (H4: m + m * S n' = m * S (S n')).
    rewrite -> mult_help.
    reflexivity.
    rewrite -> H4.
    reflexivity.
Qed.

Theorem mult_comm : forall m n : nat,
 m * n = n * m.
Proof.
  intros m n.
  induction n as [| n'].
  Case "n = 0".
    simpl.
    rewrite -> mult_0_r.
    reflexivity.
  Case "n = S n'".
    simpl.
    rewrite <- IHn'.
    rewrite -> mult_comm_helper.
    reflexivity.
Qed.