Annotated version of the warmup from Adam Chipala's _Certified Programming with Dependent Types_.

CPDT.warmup.v

Require Import String.
(* Examples by Adam Chlipala *)
(** * Warm-up: natural numbers *)

Inductive nat := O | S (n : nat).

Fixpoint plus (n m : nat) : nat :=
  match n with
    | O => m
    | S n' => S (plus n' m)
  end.

(* TACTICS:
 * [reflexivity]: prove an equality goal that follows by normalizing terms.
 *)

Lemma O_plus : forall n,
  plus O n = n.
Proof.
  (* I need to show that adding 0 to any [n] is the same as n.
     Let [n] be a fixed number. *)
  intros.
  (* The [O] constructor applied to [n] yields [n]. *)
  simpl.
  (* And [n] is the same as [n]. *)
  reflexivity.
Qed.
  
(* TACTICS:
 * [induction x]: prove goal by induction on quantified variable [x].
 *    CAVEATS: All variables appearing _before_ [x] will remain _fixed_ throughout the induction!
 * [simpl]: apply standard heuristics for computational simplification in conclusion.
 * [rewrite H]: use (potentially quantified) equality [H] to rewrite in the conclusion.
 *)

 Lemma plus_O : forall n,
  plus n O = n.
Proof.
  (* I need to show that adding [n] to [0] is the same as [n].
     Let [n] be a fixed number. *)
  intros.
  (* Let's do induction on [n]. *)
  induction n.
  - (* Base case: plus O O = O.
       This is evident from the constructor of [plus O]. *)
    reflexivity.
  - (* Inductive case: [plus (S n) O = S n].
       Assume that [plus n O = n] (the induction hypothesis [IHn]). *)
    (* Reduce [plus (S n)] by the constructor in [plus]. *)
    simpl.
    (* Now we have [S (plus n O) = S n]. 
       By the induction hypothess, [plus n O] is the same as [n]. So rewrite it: *)
    rewrite IHn.
    (* Now we have [S n] on both sides. *)
    reflexivity.
Qed.   

(* TACTICS:
 * [intros]: move quantified variables and/or hypotheses "above the double line."
 *)

Theorem plus_assoc : forall n m o,
  plus (plus n m) o = plus n (plus m o).
Proof.
  (* I must show that addition is associative. *)
  (* Let [n], [m], and [o] be fixed numbers. *)
  intros n m o.
  (* Let us proceed by induction on [n]. *)
  induction n.
  - (* Base case: [plus (plus O m) o = plus O (plus m o)]. *)
    Print O_plus.
    (* [O_plus] says that [plus O n] is the same as [n].
       If we apply that theorem, Coq solves the goal. But here's how.
       We can use [O_plus] to replace [plus O m] on the left side with [m],
       which yields [plus m o] on the left side. We can also apply [O_plus] on the
       right side, where [n] in the theorem is here the whole of [(plus m o)]. That
       yields [plus m o] on the right. Now both sides of the equation are the same,
       and presumably [apply] applies [reflexivity], so it solves the goal. *)
    apply O_plus.
  - (* Induction case.
       I must show that [plus (plus (S n) m) o] is the same as
       [plus (S n) (plus m o)], given the induction hypothesis
       that [plus (plus n m) o] is the same as [plus n (plus m o)]. *)
    (* First, let's apply the constructors for plus. The [S n] case in
       the [plus] constructor is matched here, so that pulls out [S] to the
       front on both sides of the equation. *)
    simpl.
    (* Now I have [plus (plus n m) o] on the left side, and [plus n (plus m o)] on the
       right. According to the induction hypothesis, those are the same, so we can
       rewrite one for the other, to make them the same. *)
    rewrite IHn.
    (* Now both sides of the equation are the same. *)
    reflexivity.
Qed.

Lemma plus_S : forall n m,
  S (plus n m) = plus n (S m).
Proof.
  intros.
  induction n.
  - (* Base case. *)
    Print O_plus.
    (* Applying [O_plus] does substitutions on both sides
       of the equation, and then applies [reflexivity], just as in
       the previous proof. On the left side, it unifies [plus O n] with [n = m],
       and replaces [plus O m] with [m], so we get [S m] on the left side. 
       On the right, it unifies [plus O n] with [n = (S m)], and it replaces
       [plus O (S m)] with [S m], so we get [S m] on the right side.
       Then it applies [reflexivity] to solve the goal. *)
    apply O_plus.
  - (* Inductive case. *)
    (* We solve this just as in the last proof. By applying [simpl], we apply the 
       constructors for [plus], which pull [S] out to the front of the expressions on
       both sides of the equation. *)
    simpl.
    (* Then we have parts of the expressions that match the inductive hypothesis,
       so we can rewrite them to be the same on both sides. *)
    rewrite IHn.
    (* And now both sides of the equation are the same. *)
    reflexivity.
Qed.

(* TACTICS:
 * [apply thm]: apply a named theorem, reducing the goal into one new subgoal
 *              for each of the theorem's hypotheses, if any.
 *)

Theorem plus_comm : forall n m,
  plus n m = plus m n.
Proof.
  intros n m.  
  induction n.
  - (* Base case. Adding [O] to [m]. *)
    rewrite plus_O.
    rewrite O_plus.
    reflexivity.
  - (* Inductive case. *)
    simpl.
    rewrite IHn.    
    rewrite plus_S.
    reflexivity.
Qed.