0 なのか 1 なのか、そういうのめんどくさいので任意の自然数 N から始まる "自然数" を考えました。循環じゃなくて重複です。つきましては、 加算と乗算を定義し、それらが正しいものであることを証明してみましょう。ついでに可換律と結合律も。http://qiita.com/advent-calendar/2015/theorem-prover で書くのはこれの解説 "ではありません"。

adv_cal_2015_1205_question.v

Set Implicit Arguments.
Unset Strict Implicit.

Require Import Arith.

(* Base "から" 始まる "自然数" *)
Inductive number :=
| Base: number 
| Next: number -> number.

Module Number.
  
  (* N から始まる "自然数" から [nat] への変換 *)
  Fixpoint num2nat (N: nat)(n: number): nat :=
    match n with
    | Base => N
    | Next n' => S (num2nat N n')
    end.

  (* N から始まると解釈した上での加算 *)
  Fixpoint add (N: nat)(n m: number): number.
  Admitted.

  Lemma add_valid:
    forall N n m,
      num2nat N (add N n m) = (num2nat N n) + (num2nat N m).
  Proof.
  Admitted.

  Lemma add_comm:
    forall N n m, add N n m = add N m n.
  Proof.
  Admitted.

  Lemma add_assoc:
    forall N n m p,
      add N n (add N m p) = add N (add N n m) p.
  Proof.
  Admitted.


  (* N から始まると解釈した上での乗算 *)
  Fixpoint mul (N: nat)(n m: number): number.
  Admitted.

  Lemma mul_valid:
    forall N n m,
      num2nat N (mul N n m) = (num2nat N n) * (num2nat N m).
  Proof.
  Admitted.

  Lemma mul_comm:
    forall N n m, mul N n m = mul N m n.
  Proof.
  Admitted.

  Lemma mul_assoc:
    forall N n m p, mul N n (mul N m p) = mul N (mul N n m) p.
  Proof.
  Admitted.
End Number.