やったー、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をきちんと勉強する場合ってなにがいいんでしょうねぇ。その場その場で適当にやっているからソースがデタラメすぎる。