Software Foundations: Proof by Induction

Induction.v

Lemma add_n_O : forall n : nat, n + O = n.
Proof.
  intros n.
  induction n.
  - reflexivity.
  - simpl. rewrite -> IHn. reflexivity.
Qed.

Lemma add_n_Sm : forall n m : nat, n + S m = S (n + m).
Proof.
  intros n m.
  induction n.
  - reflexivity.
  - simpl. rewrite -> IHn. reflexivity.
Qed.

Theorem add_comm : forall n m : nat, n + m = m + n.
Proof.
  intros n m.
  induction n.
  - simpl. rewrite -> add_n_O. reflexivity.
  - simpl. rewrite -> add_n_Sm. rewrite -> IHn. reflexivity.
Qed.

Theorem add_assoc : forall n m p : nat, n + (m + p) = (n + m) + p.
Proof.
  intros n m p.
  induction n.
  - reflexivity.
  - simpl. rewrite -> IHn. reflexivity.
Qed.

Lemma mul_n_O : forall n : nat, n * O = O.
Proof.
  intros n.
  induction n.
  - reflexivity.
  - simpl. rewrite -> IHn. reflexivity.
Qed.

Lemma mul_n_Sm : forall n m : nat, n * S m = n + n * m.
Proof.
  intros n m.
  induction n.
  - reflexivity.
  - simpl. rewrite -> IHn.
    rewrite -> add_assoc, add_assoc.
    assert (H : m + n = n + m). { rewrite -> add_comm. reflexivity. }
    rewrite -> H. reflexivity.
Qed.

Theorem mul_comm : forall n m : nat, n * m = m * n.
Proof.
  intros n m.
  induction n.
  - simpl. rewrite -> mul_n_O. reflexivity.
  - simpl. rewrite -> mul_n_Sm. rewrite -> IHn. reflexivity.
Qed.

Theorem mul_distrib : forall n m p : nat, (n + m) * p = (n * p) + (m * p).
Proof.
  intros n m p.
  induction n.
  - reflexivity.
  - simpl. rewrite <- add_assoc. rewrite <- IHn. reflexivity.
Qed.

Theorem mul_assoc : forall n m p : nat, n * (m * p) = (n * m) * p.
Proof.
  intros n m p.
  induction n.
  - reflexivity.
  - simpl. rewrite -> mul_distrib. rewrite -> IHn. reflexivity.
Qed.