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.

  Fixpoint nextN (n:nat) (m:number) : number :=
    match n with
    | O => m
    | S k => Next (nextN k m)
    end.

  (* N から始まると解釈した上での加算 *)
  Fixpoint add (N: nat)(n m: number): number :=
    match n with
    | Base => nextN N m
    | Next n' =>  Next (add N n' m)
    end.

  Lemma num2nat_nextN : forall N n m,
    num2nat N (nextN n m) = n + num2nat N m.
  Proof.
    intros N n.
    induction n as [ | n' IHn']. 
    +
      simpl; reflexivity.
    +
      intros m.
      simpl.
      rewrite -> IHn'.
      reflexivity.
  Qed.

  Lemma add_valid:
    forall N n m,
      num2nat N (add N n m) = (num2nat N n) + (num2nat N m).
  Proof.
    intros N n m.
    induction n as [ | n' IHn'].
    +
      simpl.
      apply num2nat_nextN.
    +
      simpl.
      rewrite -> IHn'.
      reflexivity.
  Qed.
  Lemma num2nat_lowerbound : forall N n,
    N <= num2nat N n.
  
  Proof.
    intros N n.
    induction n as [ | n' IHn'].
    +
      simpl.
      SearchPattern (_ <= _).
      apply le_n.
    +
      simpl.
      apply le_S.
      apply IHn'.
  Qed.
  Search le.
  Lemma num2nat_when : forall N n,
    N = num2nat N n -> n = Base.
  Proof.
    intros N n H.
    induction n as [ | k].
    +
      reflexivity.
    +
      simpl in H.
      -
        simpl in H.
        assert (N <= num2nat N k) as LBound.
        apply num2nat_lowerbound.
        apply le_lt_or_eq in LBound.
        destruct LBound as [P|Q].
        *
          assert (S (num2nat N k) < num2nat N k) as Foo.
          rewrite <- H.
          apply P.
          apply lt_asym in Foo.
          assert (num2nat N k < S (num2nat N k)).
          SearchPattern ( _ < S _).
          apply lt_n_Sn.
          (* FIXME !!!!! *)
          contradiction.
        *
          rewrite <- Q in H.
          assert (N <> S N).
          SearchPattern (_ <> S _).
          apply n_Sn.
          contradiction.
        destruct H.
  Qed.

  Lemma num2nat_valid: forall N n m,
    num2nat N n = num2nat N m -> n = m.
  Proof.
    intros N n.
    induction n as [ | n' IHn'].
    +
      simpl.
      intros m H.
      destruct m as [ | m'].
      -
        reflexivity.
      -
        simpl in H.
        assert (N <= num2nat N m') as LBound.
        apply num2nat_lowerbound.
        apply le_lt_or_eq in LBound.
        destruct LBound as [P|Q].
        *
          apply lt_S in P.
          rewrite <- H in P.
          assert (~ N < N) as IRF.
          apply lt_irrefl.
          elimtype False.
          apply IRF.
          apply P.
        *
          rewrite <- Q in H.
          SearchPattern (_ <> S _).
          apply n_Sn in H.
          destruct H.
    +
      intros m H.
      simpl in H.
      destruct m as [ | k].
      -
        simpl in H.
        assert (N <= num2nat N n') as LBound.
        apply num2nat_lowerbound.
        apply le_lt_or_eq in LBound.
        destruct LBound as [P | Q].
        *
          (* rewrite <- H in P. 行き過ぎる*)
          assert (S(num2nat N n') < num2nat N n') as Foo.
          rewrite -> H.
          apply P.
          admit.
        *
          rewrite <- Q in H.
          symmetry in H.
          apply n_Sn in H.
          destruct H.
      -
        simpl in H.
        inversion H.
        (* TODO : inversion as *)
        assert (n'= k) as Bar.
        apply IHn'.
        apply H1.
        rewrite Bar.
        reflexivity.
  Qed.
  Lemma add_comm:
    forall N n m, add N n m = add N m n.
  Proof.
    intros N n m.
    induction n as [ | n' IHn'].
    +
      simpl.
      reflexivity.
  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.