Require Export Arith. Require Export ArithRing. Require Export ZArith. Fixpoint fib (n:nat) : nat := match n with 0 => 1 | 1 => 1 | S ((S p) as q) => fib p + fib q end. Theorem fib_ind : forall P : nat -> Prop, P 0 -> P 1 -> (forall n, P n -> P (S n) -> P (S (S n)))-> forall n, P n. Proof. intros P H0 H1 Hstep n. assert (P n/\P(S n)). elim n; intuition. intuition. Qed. Theorem fib_unroll : forall n, fib (S (S n)) = fib n + fib (S n). Proof. auto. Qed. Theorem fib_n_p : forall n p, fib (n + p + 2) = fib (n + 1) * fib (p + 1) + fib n * fib p. Proof. intros n; elim n using fib_ind. intros p; replace (0 + p+2) with (S (S p)). replace (p+1) with (S p). rewrite fib_unroll. simpl (fib 0). simpl (fib (0+1)). ring. ring. ring. intros p; replace (1+p+2) with (S (S (S p))). repeat rewrite fib_unroll. simpl (fib (1+1)). simpl (fib 1). replace (p+1) with (S p). ring. ring. ring. intros n' IHn' IHn'1 p. replace (S (S n') + p + 2) with (S (S (n'+p + 2))). simpl (S (S n') + 1). repeat rewrite fib_unroll. replace (S (n'+p+2)) with (S n' +p+2). rewrite IHn'1. rewrite IHn'. replace (S n'+1) with (S (S n')). replace (S (n'+1)) with (S (S n')). rewrite fib_unroll. ring. ring. ring. ring. ring. Qed. Theorem fib_monotonic : forall n, fib n <= fib (n+1). Proof. intros n; elim n using fib_ind; auto with arith. intros n' H1 H2; replace (S (S n')+1) with (S (S (S n'))). rewrite (fib_unroll (S n')). auto with arith. ring. Qed. Theorem fib_n_p' : forall n p, fib (n + p) = fib n * fib p + (fib (n+1) - fib n)*(fib (p+1) - fib p). Proof. intros n; elim n using fib_ind. intros p; simpl; ring. intros p; replace (1 + p) with (p + 1); simpl. ring_simplify. (* ring_simplify. *) (*rewrite <- (plus_comm (fib p)).*) rewrite le_plus_minus_r. auto. apply fib_monotonic. rewrite plus_comm. auto. intros n' IHn' IHn'1 p. simpl (S (S n') + p). rewrite fib_unroll. replace (S (n' + p)) with (S n' + p). rewrite IHn'. rewrite IHn'1. simpl (S (S n')+1). replace (S n' + 1) with (S (S n')). replace (S (n' + 1)) with (S (S n')). repeat rewrite fib_unroll. rewrite (plus_comm (fib (S n')) (fib n' + fib (S n'))). rewrite minus_plus. rewrite (plus_comm (fib n')(fib (S n'))). rewrite minus_plus. rewrite mult_minus_distr_r. replace (fib n' * fib p + (fib (n' + 1) * (fib (p + 1) - fib p) - fib n' * (fib (p + 1) - fib p)) + (fib (S n') * fib p + fib n' * (fib (p + 1) - fib p))) with (fib n' * fib p + (fib n' * (fib (p + 1) - fib p) + (fib (n' + 1) * (fib (p + 1) - fib p) - fib n' * (fib (p + 1) - fib p))) + fib (S n') * fib p). rewrite (le_plus_minus_r). replace (n' + 1) with (S n'). ring. ring. apply mult_le_compat_r. apply fib_monotonic. ring. ring. ring. ring. Qed. Theorem fib_2n : forall n, fib (2*n) = fib (n) * fib (n) + (fib (n+1) - fib n)*(fib (n+1) - fib n). Proof. intros n; replace (2*n) with (n+n). apply fib_n_p'. ring. Qed. Theorem fib_2n_plus_1 : forall n, fib (2*n+1) = 2 * fib n * fib (n+1) - fib n * fib n. Proof. intros n; replace (2*n+1) with (n + (n + 1)). rewrite fib_n_p'. replace (n + 1 + 1) with (S (S n)). rewrite fib_unroll. replace (S n) with (n + 1). rewrite (plus_comm (fib n) (fib (n + 1))). rewrite minus_plus. apply plus_reg_l with (fib n * fib n). rewrite le_plus_minus_r. rewrite plus_permute. rewrite mult_minus_distr_r. rewrite le_plus_minus_r. ring. apply mult_le_compat_r. apply fib_monotonic. replace (fib n * fib n) with (1 * (fib n * fib n)). rewrite mult_assoc_reverse. apply mult_le_compat. auto with arith. apply mult_le_compat_l. apply fib_monotonic. ring. ring. ring. ring. Qed. Theorem fib_2n_plus_2 : forall n, fib (S (2*n+1)) = fib (n+1) * (fib (n+1)) + fib n * fib n. Proof. intros n; replace (S (2*n+1)) with ((n+1)+(n+1)). rewrite fib_n_p'. replace (n + 1 + 1) with (S (S n)). rewrite fib_unroll. replace (S n) with (n + 1). rewrite (plus_comm (fib n) (fib (n + 1))). rewrite minus_plus. auto. ring. ring. ring. Qed. Theorem th_fib_positive1 : forall p : positive, forall u v : nat, u = fib (nat_of_P p) /\ v = fib (S (nat_of_P p)) -> 2*u*v - u*u = fib(nat_of_P (xI p)) /\ v*v + u*u = fib(S (nat_of_P (xI p))). Proof. intros p u v [Hu Hv]; rewrite Hu; rewrite Hv. rewrite nat_of_P_xI. replace (S (2* nat_of_P p)) with (2*nat_of_P p + 1). rewrite fib_2n_plus_1. rewrite fib_2n_plus_2. replace (S (nat_of_P p)) with (nat_of_P p + 1). auto. ring. ring. Qed. Theorem th_fib_positive0 : forall p : positive, forall u v : nat, u = fib (nat_of_P p) /\ v = fib (S (nat_of_P p)) -> u*u + (v-u)*(v-u) = fib (nat_of_P (xO p)) /\ 2*u*v - u*u = fib (S (nat_of_P (xO p))). Proof. intros p u v [Hu Hv]; subst. rewrite nat_of_P_xO. rewrite fib_2n. replace (S (nat_of_P p)) with (nat_of_P p + 1). replace (S (2*nat_of_P p)) with (2*nat_of_P p+1). rewrite fib_2n_plus_1. auto. ring. ring. Qed. Fixpoint Fib2 (p:positive) : {u:nat & { v : nat | u = fib (nat_of_P p) /\ v = fib (S (nat_of_P p))}} := match p return {u:nat & { v : nat | u = fib (nat_of_P p) /\ v = fib (S (nat_of_P p))}} with xH => (existS (fun u=> { v : nat | u = 1 /\ v = 2}) 1 (exist (fun v => 1 = 1 /\ v = 2) 2 (conj (refl_equal 1) (refl_equal 2)))) | xI p' => match Fib2 p' with (existS u (exist v h)) => (existS (fun u => { v: nat | u = fib (nat_of_P (xI p')) /\ v = fib (S (nat_of_P (xI p')))}) (2*u*v - u*u) (exist (fun w=> 2*u*v-u*u = fib (nat_of_P (xI p')) /\ w= fib (S (nat_of_P (xI p')))) (v*v + u*u) (th_fib_positive1 p' u v h))) end | xO p' => match Fib2 p' with (existS u (exist v h)) => (existS (fun u => { v: nat | u = fib (nat_of_P (xO p')) /\ v = fib (S (nat_of_P (xO p')))}) (u*u+(v-u)*(v-u)) (exist (fun w => u*u+(v-u)*(v-u) = fib (nat_of_P (xO p'))/\ w = fib (S (nat_of_P (xO p')))) (2*u*v-u*u) (th_fib_positive0 p' u v h))) end end. Definition Fib3 (p:positive) : {u:nat & { v : nat | u = fib (nat_of_P p) /\ v = fib (S (nat_of_P p))}}. Proof. fix Fib3 1. intro p. case p. intro. generalize (Fib3 p0). intros [u [v H]]. do 2 econstructor. apply th_fib_positive1. apply H. intro. generalize (Fib3 p0). intros [u [v H]]. do 2 econstructor. apply th_fib_positive0. apply H. simpl; eauto. Defined. Print Fib3. Definition Fib4 (p:positive) : {u:nat & { v : nat | u = fib (nat_of_P p) /\ v = fib (S (nat_of_P p))}}. refine (fix Fib4 (p:positive) : {u:nat & { v : nat | u = fib (nat_of_P p) /\ v = fib (S (nat_of_P p))}} := match p with xH => existT _ _ (exist _ _ _) | xI p' => let (u, H') := Fib4 p' in let (v, H) := H' in existT _ _ (exist _ _ _) | xO p' => let (u, H') := Fib4 p' in let (v, H) := H' in existT _ _ (exist _ _ _) (* | xI p' | xO p' => let (u, H') := Fib4 p' in let (v, H) := H' in existT _ _ (exist _ _ _) *) end). apply th_fib_positive1; eassumption. apply th_fib_positive0; eassumption. simpl; auto. Defined. Print Fib4. Definition fib' : forall n:nat, {u : nat &{v : nat | u = fib n /\ v = fib (S n)}}. Proof. intros n; case n. exists 1; exists 1; auto. intros n'; elim (Fib2 (P_of_succ_nat n')); intros u [v [Hu Hv]]. exists u; exists v. rewrite Hu; rewrite Hv; rewrite nat_of_P_o_P_of_succ_nat_eq_succ. auto. Qed. Require Import Program. Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 1+ 2 * x } := match n with | S (S p) => let d:= div2 p in S d | _ => O end. Next Obligation. destruct (div2 p). simpl. omega. Defined. Next Obligation. destruct n. auto. destruct n. auto. destruct (H n). trivial. Defined. Print div2. Definition pnat := (nat * nat)%type. Program Fixpoint Fib5 (p:positive) : {d : pnat | let (u,v):=d in u = fib (nat_of_P p) /\ v = fib (S (nat_of_P p))} := match p with | xH => (1, 2) | xO p' => (fun d : pnat => let (u, v) := d in (u*u + (v-u)*(v-u), 2*u*v - u*u)) (Fib5 p') (* let d' := Fib5 p' in let (u, v) := d' in (u*u + (v-u)*(v-u), 2*u*v - u*u) *) | xI p' => (fun d : pnat => let (u, v) := d in (2*u*v - u*u, v*v + u*u)) (Fib5 p') end. Next Obligation. destruct (Fib5 p') as [d H]. simpl. destruct d as [u v]. apply th_fib_positive0. exact H. Defined. Next Obligation. destruct (Fib5 p') as [d H]. simpl. destruct d as [u v]. pose proof th_fib_positive1. simpl in H0. apply H0. exact H. Defined. Print Fib5. Extraction Fib5. Extraction Inline proj1_sig. Set Extraction AutoInline. Extract Inductive prod => "(*)" [ "(,)" ]. Extract Inductive sigT => "(*)" [ "(,)" ]. (* Extract Inlined Constant minus => "(-)". Extract Inlined Constant plus => "(+)". Extract Inlined Constant mult => "( * )". *) Extract Inlined Constant minus => "(-/)". Extract Inlined Constant plus => "(+/)". Extract Inlined Constant mult => "( */ )". Extract Inductive nat => "int" ["(Int 0)" "(+/) (Int 1)"]. Recursive Extraction Fib5. Eval cbv beta iota zeta delta -[fib] in let (d,_) := Fib5 23 in d.