続・Coqりさん Q.E.D.
Coqりさん 証明のかけら の続き (再挑戦)。
Require Import Arith. Fixpoint fib1 n:nat := match n with | 0 => 0 | 1 => 1 | S (S m as p) => fib1 p + fib1 m end. Fixpoint fib2 n a b:nat := match n with | 0 => a | S n => fib2 n b (a + b) end. Lemma plus_1_Sn : forall n:nat, n + 1 = S n. Proof. intro n. rewrite plus_n_O. rewrite plus_Snm_nSm. reflexivity. Qed. Lemma plus_2_SSn : forall n:nat, n + 2 = S (S n). Proof. intro n. rewrite plus_n_O. rewrite plus_Snm_nSm. rewrite plus_Snm_nSm. reflexivity. Qed. Theorem fib1_fib : forall n:nat, fib1 n + fib1 (n + 1) = fib1 (n + 2). Proof. intro n. rewrite plus_1_Sn. rewrite plus_2_SSn. simpl fib1. destruct n. reflexivity. ring. Qed. Theorem fib2_fib : forall n a b:nat, fib2 n a b + fib2 (n + 1) a b = fib2 (n + 2) a b. Proof. induction n. intros a b. reflexivity. intros a b. rewrite plus_Sn_m. rewrite plus_Sn_m. simpl. rewrite (IHn b (a + b)). reflexivity. Qed. Lemma fib1_eq_fib2_aux : forall n:nat, fib1 n = fib2 n 0 1 /\ fib1 (S n) = fib2 (S n) 0 1. Proof. induction n. split. reflexivity. reflexivity. destruct IHn. split. exact H0. rewrite <- plus_2_SSn. rewrite <- fib1_fib. rewrite <- fib2_fib. rewrite plus_1_Sn. rewrite <- H. rewrite <- H0. reflexivity. Qed. Theorem fib1_eq_fib2 : forall n:nat, fib1 n = fib2 n 0 1. Proof. intro n. destruct (fib1_eq_fib2_aux n). exact H. Qed.
で、できたー!
これまでは流れが追えるように . で書いてきたけど、そろそろ ; 使っていってもいいかもしれない。