Coq proofs for addition/multiplication laws based on Software Foundations

add_mul_laws.v

Theorem plus_n_Sm: forall (n m : nat),
    S(n + m) = n + (S m).
Proof.
  intros n m.
  induction n as [| n' IHn'].
  { reflexivity. }
  { simpl.
    rewrite -> IHn'.
    reflexivity. }
Qed.

Theorem plus_identity_l: forall (n : nat), 0 + n = n.
Proof.
  simpl.
  reflexivity.
Qed.

Theorem plus_identity_r: forall (n : nat), n + 0 = n.
Proof.
  intros n.
  induction n as [| n' IHn'].
  { reflexivity. }
  { simpl.
    rewrite -> IHn'.
    reflexivity. }
Qed.

Theorem plus_commutative: forall (n m : nat), n + m = m + n.
Proof.
  intros n m.
  induction n as [| n' IHn'].
  { simpl.
    rewrite -> plus_identity_r.
    reflexivity. }
  { simpl.
    rewrite -> IHn'.
    rewrite -> plus_n_Sm.
    reflexivity. }
Qed.

Theorem plus_associative: forall (n m p : nat),
    (n + m) + p = n + (m + p).
Proof.
  intros n m p.
  induction n as [| n' IHn'].
  { reflexivity. }
  { simpl.
    rewrite -> IHn'.
    reflexivity. }
Qed.

Theorem plus_swap: forall (n m p : nat),
    n + (m + p) = m + (n + p).
Proof.
  intros n m p.
  rewrite <- plus_associative.
  replace (n + m) with (m + n).
  rewrite -> plus_associative.
  reflexivity.
  { rewrite -> plus_commutative.
    reflexivity. }
Qed.

Theorem plus_move: forall (n m : nat),
    n + (S m) = (S n) + m.
Proof.
  intros n m.
  rewrite <- plus_n_Sm.
  rewrite -> plus_commutative.
  rewrite -> plus_n_Sm.
  rewrite -> plus_commutative.
  reflexivity.
Qed.

Theorem mult_n_Sm: forall (n m : nat),
    n * (S m) = n + n * m.
Proof.
  intros n m.
  induction n as [| n' IHn'].
  { reflexivity. }
  { simpl.
    rewrite -> IHn'.
    rewrite -> plus_swap.
    reflexivity. }
Qed.

Theorem mult_identity_l: forall (n : nat), 0 * n = 0.
Proof.
  reflexivity.
Qed.

Theorem mult_identity_r: forall (n : nat), n * 0 = 0.
Proof.
  intros n.
  induction n as [| n' IHn'].
  { reflexivity. }
  { simpl.
    rewrite -> IHn'.
    reflexivity. }
Qed.

Theorem mult_commutative: forall (n m : nat), n * m = m * n.
Proof.
  intros n m.
  induction n as [| n' IHn'].
  { simpl.
    rewrite -> mult_identity_r.
    reflexivity. }
  { simpl.
    rewrite -> IHn'.
    rewrite -> mult_n_Sm.
    reflexivity. }
Qed.

Theorem mult_distributive_l: forall (n m p : nat),
    n * (m + p) = n * m + n * p.
Proof.
  intros n m p.
  induction n as [| n' IHn'].
  { reflexivity. }
  { simpl.
    rewrite -> plus_swap.
    replace (p + (m + n' * m + n' * p)) with (m + p + (n' * m + n' * p)).
    rewrite <- IHn'.
    reflexivity.
    { rewrite -> plus_associative.
      rewrite -> plus_associative.
      rewrite -> plus_swap.
      reflexivity. }}
Qed.

Theorem mult_distributive_r: forall (n m p: nat),
    (n + m) * p = n * p + m * p.
Proof.
  intros n m p.
  rewrite -> mult_commutative.
  rewrite -> mult_distributive_l.
  rewrite -> mult_commutative.
  replace (p * m) with (m * p).
  reflexivity.
  { rewrite -> mult_commutative.
    reflexivity. }
Qed.

Theorem mult_associative: forall (n m p : nat),
    (n * m) * p = n * (m * p).
Proof.
  intros n m p.
  induction n as [| n' IHn'].
  { reflexivity. }
  { simpl.
    rewrite -> mult_distributive_r.
    rewrite <- IHn'.
    reflexivity. }
Qed.