Coqりさん 証明のかけら
Coq りさん Coq りさん、フィボナッチ数列の末尾再帰にしたやつって、本当に元のと同じなんですか?
Fixpoint fib1 (n : nat) : nat := match n with | 0 => 0 | 1 => 1 | S n => fib1 n + fib1 (pred n) end. Fixpoint fib2 (a b n : nat) : nat := match n with | 0 => a | S n => fib2 b (a + b) n end. Theorem fib_eq : forall (n:nat), fib1 n = fib2 0 1 n. Proof. intro n. induction n. simpl. reflexivity. (*´・ω・`*) Qed.