Lambda.v

Inductive natural : Type :=
  | zero
  | succ (n : natural).

Fixpoint add (x y : natural) : natural :=
  match x with
  | zero => y
  | succ n => succ (add n y)
  end.

Infix "+" := add.

Inductive equal {A : Type} (x : A) : A → Type :=
  | refl : equal x.

Infix "≡" := equal (at level 100).

Program Instance equal_Transitive {A : Type} :
  Transitive (@equal A).
Next Obligation.
  destruct X; auto.
Qed.

Definition add_succ (x y : natural) :
  equal (succ x + y) (succ (x + y)) :=
  match x with
  | zero   => refl _
  | succ n => refl _
  end.

Definition add_succ2 (x y : natural) :
  x + succ y ≡ succ (x + y).
Proof.
  induction x; simpl.
  - apply refl.
  - rewrite IHx.
    apply refl.
Qed.

Print natural_rect.
Print add_succ2.

Definition add_zero (x : natural) :
  x + zero ≡ x.
Proof.
  induction x; simpl.
  - construct.
  - rewrite IHx.
    construct.
Qed.

Definition add_comm (x y : natural) :
  x + y ≡ y + x.
Proof.
  generalize dependent y.
  induction x; intros.
  - simpl.
    rewrite add_zero.
    construct.
  - simpl.
    rewrite IHx.
    rewrite <- add_succ2.
    construct.
Qed.