Another Test Problem for Kelly's Group

To run the proof below, you'll need Coq . You can read more about the Coq Proof Assistant on Wikipedia

We shall begin by defining the natural numbers along with two and four .

1
2
3
4
5
6

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

Definition two : nat := S (S O). 
Definition four : nat := S (S (S (S O))).

We then, define plus

1
2
3
4
5

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

Now, we can prove the theorem we desire.

1
2

Theorem two_plus_two_four : plus two two = four.
Proof. simpl. reflexivity. Qed.

And we are done!

Alternately, you could also use this:

1
2

Theorem two_plus_two_four : plus two two = four.
Proof. trivial. Qed.

Of course, here is a much less direct proof: Link