手始めにコラッツ数列を計算する関数。

Require Import Coq.Program.Wf.
Require Import Omega.

Program Fixpoint collatz03 (x y : nat) {measure y} : list nat :=
match y with
| 0 => 0::nil
| _ => match x with
| 0 => 0::nil
| 1 => 1::nil
| _ => if Nat.odd x then (3*x+1) :: collatz03 (3*x+1) (y-1)
else (x/2) :: collatz03 (x/2) (y-1)
end
end.
Next Obligation.
omega.
Qed.
Next Obligation.
omega.
Qed.

ここまでで3日かかりました。www