やったー、Coqでのたらい回し関数の停止性証明できたよー

Call-by-name版なので簡単ですけど。ものすごく下手なソースだと思いますが、一応晒しておきます。

Require Import ZArith.
Require Import List. 

Open Scope Z_scope.

Fixpoint ntarai3 (n : nat) (a b c : option Z) :=
match a with 
| None => None
| Some av =>
  match b with 
  | None => None
  | Some bv => 
      if Z_le_dec av bv then b else
      match n with 
      | 0%nat => None
      | S np => 
          match c with 
          | None => None
          | Some cv => 
              (ntarai3 np 
                (ntarai3 np (Some (av-1)) b c)
                (ntarai3 np (Some (bv-1)) c a)
                (ntarai3 np (Some (cv-1)) a b))
          end 
      end
  end
end.

Definition ntarai3v (n : nat) (av bv cv : Z):=
ntarai3 n (Some av) (Some bv) (Some cv). 

Lemma lem_a_must_be_defined : 
forall (a b c : option Z), forall (n : nat), 
ntarai3 n a b c <> None 
-> a <> None. 
intros. 
induction a. 
discriminate. 
elim H.
unfold ntarai3.
elim n. 
auto. 
intros. 
auto.
Qed. 

Lemma lem_b_must_be_defined : 
forall (a b c : option Z), forall (n : nat), 
ntarai3 n a b c <> None 
-> b <> None. 
induction b.
intros. 
discriminate. 
intros. 
elim H. 
unfold ntarai3. 
elim n.
destruct a.
auto. 
auto. 
intros. 
destruct a. 
auto. 
auto.
Qed.  

Lemma lem_a_le_b : forall (n : nat), forall (c : option Z), 
forall (av bv : Z), 
av<=bv -> (ntarai3 n (Some av) (Some bv) c) = Some bv.
intros.
unfold ntarai3.
elim n. 
case (Z_le_dec av bv). 
auto.
intro. 
contradiction. 
intros.  
case (Z_le_dec av bv). 
auto. 
intro. 
contradiction. 
Qed. 

Lemma lem_a_gt_b_then_c_must_be_defined : 
forall (n : nat), forall (av bv : Z), forall (c : option Z), 
av > bv -> 
ntarai3 n (Some av) (Some bv) c <> None ->
c <> None. 
intros. 
induction c. 
discriminate. 
elim H0. 

unfold ntarai3.
induction n. 
case (Z_le_dec av bv).
intro. 
absurd (av<=bv). 
omega. 
exact z.
intro. 
auto. 
case (Z_le_dec av bv).
intro. 
absurd (av<=bv). 
omega. 
exact z. 
intro. 
trivial. 
Qed. 

Lemma lem_a_gt_b_n_eq_0 : forall (av bv : Z), forall c : option Z, 
av>bv -> 
ntarai3 0 (Some av) (Some bv) c = None. 
intros. 
unfold ntarai3. 
case (Z_le_dec av bv). 
intro. 
absurd (av<=bv). 
omega. 
auto. 
intro.
auto. 
Qed. 

Lemma lem_a_gt_b : forall (n : nat), 
forall (av bv cv : Z), 
av>bv -> 
ntarai3 (S n) (Some av) (Some bv) (Some cv) = 
 ntarai3 n 
  (ntarai3 n (Some (av-1)) (Some bv) (Some cv))
  (ntarai3 n (Some (bv-1)) (Some cv) (Some av))
  (ntarai3 n (Some (cv-1)) (Some av) (Some bv)).
intros. 
simpl.
case (Z_le_dec av bv). 
intro. 
absurd (av<=bv). 
omega. 
auto. 
intro. 
auto. 
Qed. 

Lemma lem_n_indep : forall (m n: nat), 
(n<=m)%nat -> 
forall (av bv cv : Z), 
ntarai3 n (Some av) (Some bv) (Some cv)<> None
-> ntarai3 n (Some av) (Some bv) (Some cv)
=ntarai3 m (Some av) (Some bv) (Some cv).
intro. 
induction m. 

(* case m=0 *)
intros. 
assert (n=0%nat).
omega. 
rewrite H1. 
auto.

(* induction for m *)  
intros.
assert (av<=bv \/ av>bv). 
omega.
case H1. 
intro. 
rewrite lem_a_le_b. 
rewrite lem_a_le_b. 

auto. 
auto. 
auto. 

intro.
induction n. 
absurd (ntarai3 0 (Some av) (Some bv) (Some cv)=None).
 
auto.
auto.  
apply lem_a_gt_b_n_eq_0. 
auto.
 
rewrite lem_a_gt_b. 
rewrite lem_a_gt_b.

assert (ntarai3 n (Some (av-1)) (Some bv) (Some cv)<> None).  
rewrite lem_a_gt_b in H0. 
apply lem_a_must_be_defined with 
 (ntarai3 n (Some (bv-1)) (Some cv) (Some av))
 (ntarai3 n (Some (cv-1)) (Some av) (Some bv)) n. 
auto. 
auto.

assert (ntarai3 n (Some (bv-1)) (Some cv) (Some av)<> None). 
rewrite lem_a_gt_b in H0. 
apply lem_b_must_be_defined with 
 (ntarai3 n (Some (av-1)) (Some bv) (Some cv))
 (ntarai3 n (Some (cv-1)) (Some av) (Some bv)) n. 
auto. 
auto.

assert (exists ya : option Z, 
 ntarai3 n (Some (av-1)) (Some bv) (Some cv)=ya). 
exists (ntarai3 n (Some (av-1)) (Some bv) (Some cv)). 
auto. 
elim H5.
intro ya.
intro.   

assert (exists yav : Z, ya=(Some yav)).
induction ya. 
exists a. 
auto. 
absurd (ntarai3 n (Some (av-1)) (Some bv) (Some cv)=None).
auto. 
auto. 
elim H7.
intro yav. 
intro. 
  
assert (exists yb : option Z, 
 ntarai3 n (Some (bv-1)) (Some cv) (Some av)=yb). 
exists (ntarai3 n (Some (bv-1)) (Some cv) (Some av)). 
auto. 
elim H9.
intro yb.
intro.

assert (exists ybv : Z, yb=(Some ybv)).
induction yb. 
exists a. 
auto. 
absurd (ntarai3 n (Some (bv-1)) (Some cv) (Some av)=None).
auto. 
auto. 
elim H11.
intro ybv. 
intro.

rewrite H8 in H6. 
rewrite H12 in H10. 

assert (ntarai3 n (Some (av-1)) (Some bv) (Some cv)=
ntarai3 m (Some (av-1)) (Some bv) (Some cv)).
apply IHm. 
omega.
auto.  

assert (ntarai3 n (Some (bv-1)) (Some cv) (Some av)
 = ntarai3 m (Some (bv-1)) (Some cv) (Some av)).
apply IHm. 
omega.
auto.

rewrite <- H13. 
rewrite <- H14. 
rewrite H6. 
rewrite H10. 

assert (yav<=ybv \/ yav>ybv). 
omega. 
case H15. 
intro. 

assert (ntarai3 n (Some yav) (Some ybv) 
 (ntarai3 n (Some (cv-1)) (Some av) (Some bv))=(Some ybv)). 
apply lem_a_le_b. 
auto. 
rewrite H17. 

assert (ntarai3 m (Some yav) (Some ybv) 
 (ntarai3 m (Some (cv-1)) (Some av) (Some bv))=(Some ybv)).
apply lem_a_le_b. 
auto. 
rewrite H18. 
auto. 

intro. 

rewrite lem_a_gt_b in H0.
rewrite H6 in H0.  
rewrite H10 in H0.  

assert (ntarai3 n (Some (cv-1)) (Some av) (Some bv)<>None).
apply lem_a_gt_b_then_c_must_be_defined with 
 n yav ybv. 
auto. 
auto. 

assert (exists yc : option Z, 
ntarai3 n (Some (cv-1)) (Some av) (Some bv)=yc).
exists (ntarai3 n (Some (cv-1)) (Some av) (Some bv)).
auto. 
elim H18. 
intro yc. 
intro.

assert (exists ycv : Z, yc = (Some ycv)).  
induction yc.
exists a. 
auto. 
elim H17. 
elim H19.
auto. 
elim H20. 
intro ycv. 
intro. 
rewrite H21 in H19. 
rewrite H19. 

assert (ntarai3 n (Some (cv-1)) (Some av) (Some bv)
=ntarai3 m (Some (cv-1)) (Some av) (Some bv)). 
apply IHm. 
omega. 
apply H17. 
rewrite <-H22. 
rewrite H19. 
auto. 

apply IHm.
omega.
rewrite H19 in H0. 
auto. 
auto. 
auto. 
auto. 
Qed. 

Lemma lem1_a_gt_b_le_c : 
forall (bv cv :Z), forall (m : nat),  
bv<=cv -> (m>0)%nat -> exists n : nat,  
(ntarai3 n (Some (bv+Z_of_nat(m)))
  (Some bv) (Some cv))=(Some cv).
intro. 
intro. 
intro. 
intro. 
induction m.
intro.
absurd (0>0)%nat.
omega. 
auto.


induction m. 
intro.
exists 1%nat. 
rewrite inj_S.
rewrite lem_a_gt_b. 

rewrite inj_0. 
assert (bv+Zsucc 0-1=bv). 
omega. 
rewrite H1. 
rewrite lem_a_le_b. 

rewrite lem_a_le_b. 

case (Z_le_dec bv cv). 
auto.
intuition.

apply lem_a_le_b. 
auto.
intro.
absurd (bv<=cv). 
auto. 
auto.  
omega.
omega. 
omega. 
intros. 

assert (exists n : nat, 
 ntarai3 n (Some (bv+Z_of_nat(S m))) (Some bv) (Some cv)=Some cv).
apply IHm.
omega. 
elim H1. 
intro n0. 
intro. 
exists (S n0).

rewrite lem_a_gt_b. 

assert (Z_of_nat (S (S m))=Zsucc (Z_of_nat(S m))).
rewrite inj_S. 
auto. 

assert (bv + Z_of_nat (S (S m))-1=bv+Z_of_nat(S m)). 
rewrite H3.
omega. 
rewrite H4. 
rewrite H2. 

assert (ntarai3 n0 (Some (bv-1)) (Some cv) 
 (Some (bv + Z_of_nat(S (S m))))=(Some cv)).
rewrite lem_a_le_b. 
auto.
omega. 
rewrite H5. 
apply lem_a_le_b.
omega. 
rewrite inj_S. 
omega. 
Qed. 

Lemma lem_a_gt_b_le_c : forall (av bv cv : Z), 
av>bv /\ bv<=cv -> 
exists n : nat, 
(ntarai3 n (Some av) (Some bv) (Some cv))=(Some cv).
intros. 
elim H. 
intros. 

assert (exists m : nat, av-bv=Z_of_nat m). 
apply Z_of_nat_complete.
omega. 
elim H2. 
intro m. 
intro. 

assert (av=bv+Z_of_nat m). 
omega. 

rewrite H4. 
apply lem1_a_gt_b_le_c. 
auto.
omega. 
Qed. 

Lemma lem1_a_gt_b_gt_c : forall (bv cv : Z), 
bv>cv -> 
forall (d : nat), 
(d>0)%nat ->  
exists n : nat, 
ntarai3 n (Some (bv+Z_of_nat(d))) 
 (Some bv) (Some cv) = (Some (bv+Z_of_nat(d))).
intros.
induction d.
absurd (0>0)%nat. 
omega. 
auto.
 
induction d.

assert (bv-1<=cv \/ bv-1>cv). 
omega. 
elim H1. 
intro. 

assert (exists n0 : nat,  ntarai3 n0 (Some (bv-1)) 
 (Some cv) (Some (bv+1))=(Some cv)).
exists 0%nat. 
apply lem_a_le_b. 
auto.

elim H3. 
intro n0. 
intro.

assert (exists n1 : nat, ntarai3 n1 (Some bv) (Some cv) 
 (Some (bv+1))=Some (bv+1)). 
apply lem_a_gt_b_le_c. 
omega. 
elim H5. 
intro n1. 
intro. 

exists (S (n0+n1))%nat. 
simpl. 

case (Z_le_dec (bv+1) bv). 
intro. 
absurd (bv+1<=bv). 
omega. 
auto. 
intro. 
 
assert (bv+1-1=bv). 
omega. 
rewrite H7. 
rewrite lem_a_le_b. 

assert (ntarai3 (n0+n1) 
 (Some (cv-1)) (Some (bv+1)) (Some bv)=(Some (bv+1))).  
apply lem_a_le_b.
omega.
rewrite H8. 

assert (ntarai3 n0 (Some (bv-1)) (Some cv)
 (Some (bv+1))=
 ntarai3 (n0+n1) (Some (bv-1)) (Some cv) (Some (bv+1))).
apply lem_n_indep.
omega. 
rewrite H4. 
discriminate. 
rewrite <- H9. 
rewrite H4. 

assert (ntarai3 n1 (Some bv) (Some cv) (Some (bv+1))
 = ntarai3 (n0+n1) (Some bv) (Some cv) (Some (bv+1))). 
apply lem_n_indep. 
omega. 
rewrite H6. 
discriminate. 
rewrite <- H10.
apply H6.
omega. 

(* the case of bv-1<=cv was done *)

(* the case bv-1>cv *)
intro. 
simpl. 

assert (exists n0 : nat, 
 ntarai3 n0 (Some (bv-1)) (Some cv) (Some (bv+1))
 = Some (bv+1)). 
apply lem_a_gt_b_le_c. 
omega. 
elim H3. 
intro n0. 
intro.

exists (S n0)%nat. 
simpl. 

case (Z_le_dec (bv+1) bv). 
intro. 
absurd (bv+1<=bv). 
omega.
auto. 

intro. 

assert (bv+1-1=bv). 
omega. 
rewrite H5. 
rewrite lem_a_le_b. 
rewrite H4. 

rewrite lem_a_le_b. 
auto. 
omega. 
omega.  

assert (exists n0: nat, 
 ntarai3 n0 (Some (bv+ Z_of_nat (S d))) (Some bv) (Some cv)
 = (Some (bv+ Z_of_nat (S d)))).
apply IHd. 
omega. 
elim H1. 
intro n0. 
intro. 

assert (exists n1:nat, 
 ntarai3 n1 (Some (bv-1)) (Some cv) 
  (Some (bv + Z_of_nat (S (S d))))= (Some cv) 
  \/ ntarai3 n1 (Some (bv-1)) (Some cv) 
  (Some (bv + Z_of_nat (S (S d))))= 
  (Some (bv + Z_of_nat (S (S d))))).
assert (bv-1<=cv \/ bv-1>cv). 
omega. 
case H3. 
intro. 
exists 0%nat. 
left. 
apply lem_a_le_b. 
auto. 
intro. 
assert (exists n1: nat, ntarai3 n1 (Some (bv-1)) (Some cv) 
  (Some (bv + Z_of_nat (S (S d))))= 
  (Some (bv + Z_of_nat (S (S d))))). 
apply lem_a_gt_b_le_c. 
split. 
auto. 
omega. 
elim H5. 
intro n1. 
intro. 
exists n1.
right. 
auto. 

elim H3. 
intro n1. 
intro.

assert (exists n2 : nat, 
 ntarai3 n2 (Some (bv+Z_of_nat (S d))) 
 (Some cv) (Some (bv+Z_of_nat (S (S d))))
 =(Some (bv+Z_of_nat (S (S d))))). 
apply lem_a_gt_b_le_c. 
omega. 
elim H5. 
intro n2. 
intro. 

exists (S (n0+n1+n2))%nat. 
rewrite lem_a_gt_b.

assert (bv+Z_of_nat(S (S d))-1=bv+Z_of_nat(S d)). 
rewrite inj_S. 
omega.
rewrite H7. 

assert (ntarai3 n0 (Some (bv+Z_of_nat (S d))) 
 (Some bv) (Some cv) = 
 ntarai3 (n0+n1+n2) (Some (bv+Z_of_nat (S d))) 
 (Some bv) (Some cv)). 
apply lem_n_indep.
omega.
rewrite H2. 
discriminate. 
rewrite <- H8. 
rewrite H2. 

assert (ntarai3 (n0+n1+n2) (Some (cv-1)) 
 (Some (bv+Z_of_nat (S (S d)))) (Some bv)
 = (Some (bv+Z_of_nat (S (S d))))). 
apply lem_a_le_b. 
omega. 
rewrite H9. 

elim H4. 
intro.

assert (ntarai3 n1 (Some (bv-1)) (Some cv)
 (Some (bv+Z_of_nat (S (S d))))=
 ntarai3 (n0+n1+n2) (Some (bv-1)) (Some cv)
 (Some (bv+Z_of_nat (S (S d))))). 
apply lem_n_indep. 
omega.
rewrite H10. 
discriminate. 

rewrite <- H11.
rewrite H10.  

assert(ntarai3 n2 (Some (bv+Z_of_nat (S d)))
 (Some cv) (Some (bv+ Z_of_nat (S (S d)))) 
 =ntarai3 (n0+n1+n2) (Some (bv+Z_of_nat (S d)))
 (Some cv) (Some (bv+ Z_of_nat (S (S d))))). 
apply lem_n_indep. 
omega. 
rewrite H6. 
discriminate.
 
rewrite <- H12.
rewrite H6. 
auto. 

intro. 
assert (ntarai3 n1 (Some (bv-1)) (Some cv) 
 (Some (bv+Z_of_nat (S (S d))))
 =ntarai3 (n0+n1+n2) (Some (bv-1)) (Some cv) 
 (Some (bv+Z_of_nat (S (S d))))). 
apply lem_n_indep. 
omega. 
rewrite H10. 
discriminate. 
rewrite <- H11. 
rewrite H10. 

apply lem_a_le_b. 
omega.
rewrite inj_S.  
rewrite inj_S.  
omega. 
Qed. 

Lemma lem_a_gt_b_gt_c : forall (av bv cv : Z), 
av>bv -> bv>cv -> 
exists n : nat, 
ntarai3 n (Some av) (Some bv) (Some cv)=(Some av). 
intros. 
assert (exists d: nat, 
av-bv=Z_of_nat d). 
apply Z_of_nat_complete. 
omega. 

elim H1. 
intro d. 
intro. 

assert (av=bv+Z_of_nat d).
omega. 
rewrite H3. 

apply lem1_a_gt_b_gt_c. 
omega. 
omega. 
Qed. 

Theorem tarai3_terminates : 
forall (av bv cv : Z), 
exists n: nat, 
ntarai3 n (Some av) (Some bv) (Some cv)<>None. 
intros. 

assert (av<=bv \/ av>bv). 
omega. 
elim H. 
intro. 
exists 0%nat. 
rewrite lem_a_le_b. 
discriminate. 
auto. 

intro. 
assert (bv<=cv \/ bv>cv). 
omega. 
elim H1. 
intro. 

assert (exists n: nat, 
 ntarai3 n (Some av) (Some bv) (Some cv)=(Some cv)). 
apply lem_a_gt_b_le_c. 
omega. 
elim H3. 
intro n. 
intro. 
exists n. 
rewrite H4. 
discriminate. 
intro. 

assert (exists n: nat, 
 ntarai3 n (Some av) (Some bv) (Some cv)
 = (Some av)). 
apply lem_a_gt_b_gt_c. 
omega. 
omega. 
elim H3. 
intro n. 
intro. 
exists n. 
rewrite H4.
discriminate. 
Qed.  

Coqをきちんと勉強する場合ってなにがいいんでしょうねぇ。その場その場で適当にやっているからソースがデタラメすぎる。