gistfile1.coq

Module PlayGround1.

Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.

Definition pred (n : nat) : nat :=
  match n with
    | O => O
    | S n' => n'
  end.

Module PlayGround2.

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

Definition _0 : nat := O.
Definition _1 : nat := S O.
Definition _2 : nat := S (S O).
Definition _3 : nat := plus _1 _2.
Definition _4 : nat := plus _2 _2.
Definition _5 : nat := plus _3 _2.
Definition _6 : nat := plus _3 _3.
Definition _7 : nat := plus _4 _3.
Definition _8 : nat := plus _4 _4.
Definition _9 : nat := plus _5 _4.

Lemma plus_0_n : forall n : nat, plus O n = n.
Proof.
  intros.
  reflexivity.
Qed.

Lemma plus_n_0 : forall n : nat, plus n O = n.
Proof.
  intros.
  induction n as [| n'].
  reflexivity.
  simpl.
  rewrite -> IHn'.
  reflexivity.
Qed.

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

Theorem plus_comm : forall n m : nat, plus n m = plus m n.
Proof.
  intros.
  induction n as [| n'].
  simpl.
  rewrite -> plus_n_0.
  reflexivity.
  simpl.
  rewrite <- plus_n_Sm.
  rewrite -> IHn'.
  reflexivity.
Qed.