Theory Lucas_Sequences

theory Lucas_Sequences
  imports Main HOL.Parity
begin

section ‹Lucas Sequences›

fun ψ :: "int ⇒ nat ⇒ int" where
"ψ A 0 = 0"|
"ψ A (Suc 0) = 1"|
"ψ A (Suc (Suc n)) = A * (ψ A (Suc n)) - (ψ A n)"

fun χ :: "int ⇒ nat ⇒ int" where
"χ A 0 = 2"|
"χ A (Suc 0) = A"|
"χ A (Suc (Suc n)) = A * (χ A (Suc n)) - (χ A n)"

subsection ‹Elementary properties›

theorem ψ_induct [consumes 0, case_names 0 1 sucsuc]:
  "P 0 ⟹ P 1 ⟹ (⋀n. P (n + 1) ⟹ P n ⟹ P (n + 2)) ⟹ P (n::nat)"
  apply (induct rule: ψ.induct)
  by simp_all

theorem ψ_induct_strict [consumes 0, case_names 0 1 2 sucsuc]:
  "P 0 ⟹ P 1 ⟹ P 2 ⟹ (⋀n. n>0 ⟹ P (n + 1) ⟹ P n ⟹ P (n + 2)) ⟹  P (n::nat)"
  apply (induct rule: χ.induct)
  apply simp
  apply (metis One_nat_def)
  by (metis One_nat_def Suc_1 Suc_eq_plus1 add_2_eq_Suc' bot_nat_0.not_eq_extremum)

lemma lem0: "n≥2 ⟹ ∃m. n = Suc (Suc m)"
  by (simp add: nat_le_iff_add)

lemma ψ_reverse:
  assumes "n≥1"
  shows "ψ A (n-1) = A * (ψ A n) - (ψ A (n+1))"
proof -
  obtain m where "Suc (Suc m) = n+1"
    by (metis Suc_eq_plus1 add_eq_if assms not_one_le_zero)
  then show ?thesis by auto
qed

text ‹Strict monotonicity›
lemma lucas_strict_monotonicity: "A>1 ⟹ ψ A (Suc n) > ψ A n ∧ ψ A (Suc n) > 0"
proof (induction n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  from Suc have "A*ψ A (Suc n)>(ψ A n+ψ A (Suc n))" 
    proof -
      from Suc have b1:"A*ψ A (Suc n)≥2*ψ A (Suc n)"
        by simp
      from Suc have b2:"2*ψ A (Suc n)>ψ A n+ψ A (Suc n)"
        by simp
      from b1 b2 show ?thesis
        using less_le_trans by blast
    qed
  from this and Suc show ?case
    by auto
qed

lemma lucas_monotone1:
  fixes A
  assumes "A>1"
  shows "n≥2 ⟶ ψ A n ≥ A"
proof (induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  note HR = this
  consider (0) "n=0" | (1) "n=1" | (2)"n≥2" by fastforce
  then show ?case
  proof cases
    case 0
    then show ?thesis by simp
  next
    case 1
    then show ?thesis by simp
  next
    case 2
    then show ?thesis using HR lucas_strict_monotonicity[of "A" "n"] assms by simp
  qed
qed

lemma lucas_monotone2:
  fixes A n m
  assumes "A>1"
  shows "ψ A n ≤ ψ A (n+m)"
proof (induction m)
  case 0
  then show ?case using assms by auto
next
  case (Suc m)
  then show ?case using lucas_strict_monotonicity[of A "n+m"] assms by auto
qed

lemma lucas_monotone3:
  fixes A n
  assumes "A > 1"
  shows "ψ A n ≥ int n"
proof (induction n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  then show ?case using lucas_strict_monotonicity[of A n] assms by auto
qed

lemma lucas_monotone4:
  fixes A n m
  assumes "A>1" and "n ≤ m"
  shows "ψ A n ≤ ψ A m"
proof -
  obtain k where "m = n + k" using assms less_eqE by blast
  thus ?thesis using lucas_monotone2[of A n k]  assms by auto
qed


(* Exponential growth *)
lemma lucas_exp_growth_lt:
  fixes A::int and n::nat
  assumes "A>1"
  shows "ψ A (Suc (Suc (Suc n))) < A^(n+2)"
proof (induction n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  note t = this
  have " ψ A m ≥ 0" for m
  proof (cases m)
    case 0
    then show ?thesis by auto
  next
    case (Suc nat)
    then show ?thesis using assms lucas_strict_monotonicity[of A nat] by auto
  qed
  then have maj1 : "⋀m. m>0 ⟹  ψ A (Suc (Suc m)) ≤ A * ψ A (Suc m)"
    by (simp add: lucas_strict_monotonicity)
  have triv : "A^(Suc n +2) = A* A^(n+2)" by auto
  have maj2 : "ψ A (Suc (Suc (Suc (Suc n))))
    ≤ A * ψ A (Suc (Suc (Suc n)))"
    apply (rule maj1[of "Suc (Suc n)"]) by auto
  have maj3 : "A * ψ A (Suc (Suc (Suc n))) < A* A^(n+2)"
    using t assms by auto
  have maj4 : "ψ A (Suc (Suc (Suc (Suc n)))) < A* A^(n+2)"
    using maj2 maj3 by auto
then show ?case using maj4 triv by auto
qed

lemma lucas_exp_growth_le:
  fixes A::int and n::nat
  assumes "A>1"
  shows "ψ A (Suc (Suc n)) ≤ A^(n+1)"
proof (induction n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  note t = this
  have " ψ A m ≥ 0" for m
  proof (cases m)
    case 0
    then show ?thesis by auto
  next
    case (Suc nat)
    then show ?thesis using assms lucas_strict_monotonicity[of A nat] by auto
  qed
  then have maj1 : "⋀m. m>0 ⟹  ψ A (Suc (Suc m)) ≤ A * ψ A (Suc m)"
    by (simp add: lucas_strict_monotonicity)
  have triv : "A^(Suc n +2) = A* A^(n+2)" by auto
  have maj2 : "ψ A (Suc  (Suc (Suc n)))
    ≤ A * ψ A (Suc (Suc n))"
    apply (rule maj1[of "Suc n"]) by auto
  have maj3 : "A * ψ A  (Suc (Suc n)) ≤ A* A^(n+1)"
    using t assms by auto
  have maj4 : "ψ A (Suc (Suc (Suc n))) ≤ A* A^(n+1)"
    using maj2 maj3 by auto
then show ?case using maj4 triv by auto
qed

lemma lucas_exp_growth_gt:
  fixes A::int and n::nat
  assumes "A>1"
  shows "ψ A (Suc (Suc n)) > (A-1)^(n+1)"
proof (induction n rule: ψ_induct)
  case 0
  then show ?case by auto
next
  case 1
  have "1 - 2*A < -1" using assms by auto
  then have m1:  "A*A - 2*A + 1 < A*A - 1" by auto
  moreover have m2: "(A-1)^(1+1) = A*A - 2 * A + 1"
    apply simp
    by (smt (verit, ccfv_SIG) mult_cancel_left2 square_diff_square_factored)
  moreover have "ψ A (Suc (Suc 1)) = A*A - 1" by auto
  then show ?case using m1 m2 by auto
next
  case (sucsuc n)
  note t = this
  have m1: "⋀m. ψ A (m+1) ≥  ψ A m "
    using assms lucas_strict_monotonicity[of A m]
    by (metis Suc_eq_plus1_left add.commute lucas_strict_monotonicity not_le_imp_less not_less_iff_gr_or_eq)
  have m2: "ψ A (Suc (Suc (n+1))) ≥  ψ A (Suc (Suc n))"
    using m1[of "Suc (Suc n)"] by auto
  then have m3: "ψ A (Suc (Suc (n+1))) - ψ A (Suc (Suc (n)))≥ 0"
    by auto
  have m4: "⋀m. m ≥ 0 ⟹ m + (A-1) * ψ A (Suc (Suc (n+1))) ≥ (A-1) * ψ A (Suc (Suc (n+1)))"
    by auto
  have "A*ψ A (Suc (Suc (n+1))) - ψ A (Suc (Suc n)) ≥ (A-1) * ψ A (Suc (Suc (n+1)))"
    using m4[of "ψ A (Suc (Suc (n+1))) - ψ A (Suc (Suc (n)))"]
    by (smt (z3) left_diff_distrib' m3 mult_cancel_right1)
  then have m5: "ψ A (Suc (Suc (n+2))) ≥ (A-1) * ψ A (Suc (Suc (n+1)))"
    by auto
  have triv: "⋀m k. m≥k ⟹ (A-1)*m ≥ (A-1)*k"
    using assms by auto
  have "(A-1) * ψ A (Suc (Suc (n+1))) ≥ (A-1) * (A-1) ^ (n + 1 + 1)"
   using triv[of "ψ A (Suc (Suc (n+1)))" "(A-1) ^(n + 1 + 1)"] t assms by auto
  then have m6: "ψ A (Suc (Suc (n+2))) ≥ (A-1)*(A - 1) ^ (n + 1 + 1)"
    using m5 by auto 
  then have m7: "(A-1)*(A - 1) ^ (n + 1 + 1) = (A-1)^(n+2+1)"
    by auto
  then show ?case using m6 m7
    by (smt (verit, best) assms m5 mult_strict_left_mono t(1))
qed

(* Symmetry in A *)
lemma lucas_symmetry_A:
  fixes A::int and n::nat
  assumes "A ≥ 2"
  shows "(ψ A n) = (if (odd n) then ψ (-A) n else - ψ (-A) n)"
proof -
  consider (0) "n=0" | (1) "n=1" | (suc) "n≥2" by fastforce
  then show ?thesis
  proof cases
    case 0
    then show ?thesis by simp
  next
    case 1
    then show ?thesis by simp
  next
    case suc
    then show ?thesis
    proof (induction n rule: full_nat_induct)
      case (1 n)
      then show ?case
        using assms lem0[of n] "1.prems"
        using le_Suc_eq by auto
      qed
  qed
qed

lemma lucas_symmetry_A2: "-ψ A n = (-1::int)^n * ψ (-A) n"
proof(induction n rule: ψ_induct)
  case 0
  then show ?case by simp
next
  case 1
  then show ?case by simp
next
  case (sucsuc n)
  then show ?case 
    by (auto simp add: algebra_simps)
qed

lemma lucas_symmetry_A_abs: assumes "abs A > 1" shows "abs (ψ A n) = ψ (abs A) n"
proof (cases "n=0")
  case True
  then show ?thesis by simp
next
  case False
  then show ?thesis using lucas_strict_monotonicity[of "abs A" "n-1"] lucas_symmetry_A2[of "A" n] assms
    by (smt (z3) One_nat_def Suc_pred lucas_symmetry_A not_gr_zero)
qed

(* Special behavior for A=2 *)
lemma lucas_A_eq_2:
  fixes  n::nat
  shows "(ψ 2 n) = (int n)"
proof -
  consider (0) "n=0" | (1) "n=1" | (suc) "n≥2" by fastforce
  then show ?thesis
  proof cases
    case 0
      then show ?thesis by simp
    next
      case 1
      then show ?thesis by simp
    next
      case suc
      then show ?thesis
      proof (induction n rule: full_nat_induct)
        case (1 n)
        then show ?case
          using lem0[of n]
          using "1.prems" ψ.simps(2) eq_numeral_Suc le_Suc_eq le_simps(1) lessI numeral_Bit0
                of_nat_0
          by fastforce     
      qed
   qed
 qed

(* Behavior modulo N *)
lemma lucas_periodic_modN:
  fixes N::int
  assumes "N > 0"
  shows "∃T≥1. ∀n. (ψ A (T + n)) mod N = (ψ A n) mod N"
proof -
  define f where "f ≡ (λr. ((ψ A r) mod N, (ψ A (r+1)) mod N))"
  then have 0: "f ` {1..(nat(N^2)+1)} ⊆ ({0..(N-1)} × {0..(N-1)})"
    using pos_mod_bound pos_mod_sign assms
    by auto
  have "finite ({0..(N-1)} × {0..(N-1)})"
    by auto
  then have 1: "card(f ` {1..(nat(N^2)+1)}) ≤ card (({0..(N-1)} × {0..(N-1)}))"
    using 0 Finite_Set.card_mono
    by blast
  have "card ({0..(N-1)} × {0..(N-1)}) = nat(N^2)"
    apply simp
    by (smt (verit, del_insts) assms nat_power_eq power2_eq_square)
  then have 2: "card(f ` {1..(nat(N^2)+1)}) < card({1..(nat(N^2)+1)})"
    using 0 1
    by auto
  then have "¬ inj_on f {1..(nat(N^2)+1)}"
    using Finite_Set.pigeonhole
    by blast
  then have 3: "∃r∈{1..(nat(N^2)+1)}. ∃s∈{1..(nat(N^2)+1)}. (f r = f s) ∧ r ≠ s"
    using inj_on_def
    by blast
  then obtain r s where def_rs:"(f r = f s) ∧ r ≠ s" by auto
  define b a where def_b: "b ≡ max r s" and def_a: "a ≡ min r s"
  then have prop_ab:"f a = f b ∧ a < b"
    using def_rs
    by (simp add: max_def min_def)
  have prop_rec_desc: "∀k. k≤a ⟶ f (b-k) = f(a-k)"
  proof
    fix k
    show "k≤a ⟶ f (b-k) = f(a-k)"
    proof (induction k)
      case 0
      then show ?case using prop_ab by simp
    next
      case (Suc k)
      then show ?case
      (* Distinguishing whethe 0=a-k is reached or not *)
      proof (cases "k=a")
        case True
        then show ?thesis by auto
      next
        case False
        assume HR: "k ≤ a ⟶ f (b - k) = f (a - k)"
        assume "k≠a"
        have "Suc k ≤ a ⟹ f (b - Suc k) = f (a - Suc k)"
        proof -
          assume k_small_a: "(Suc k) ≤ a"
          (* Trivial inequalities that simplify lemma applications later *)
          then have k_small: "a-k ≥ 1" "b-k ≥ 1" using prop_ab by auto
          have "k≤a" using k_small_a by simp
          (* Beginning of calculations *)
          then have eg1: "(ψ A (a-k)) mod N = (ψ A (b-k)) mod N ∧ ψ A (a-k+1) mod N = (ψ A (b-k+1)) mod N"
            using HR f_def by force
          have eg2: "ψ A (a-k-1) = A * ψ A (a-k) - ψ A (a-k+1) ∧ ψ A (b-k-1) = A * ψ A (b-k) - ψ A (b-k+1)"
            using k_small ψ_reverse[of "a-k" "A"] ψ_reverse[of "b-k" "A"]
            by auto
          then have "(ψ A (a-k-1)) mod N = (A * ψ A (a-k) - ψ A (a-k+1)) mod N"
            by presburger
          also have "... = (A * ψ A (b-k) - ψ A (b-k+1)) mod N"
            using eg1 by (metis mod_diff_cong mod_mult_cong)
          finally have eg3: "(ψ A (a-k-1)) mod N = (ψ A (b-k-1)) mod N" 
            using eg2 by presburger
          then show  "f (b - Suc k) = f (a - Suc k)" using eg1 k_small
            by (smt (z3) diff_Suc_eq_diff_pred diff_commute f_def le_add_diff_inverse2)
        qed
        then show ?thesis by (rule impI)
      qed
    qed
  qed
  define T where def_T: "T ≡ b-a"
  then have T1: "T≥1" using prop_ab
    by (simp add: Suc_leI)
  have "f T = f 0" using prop_rec_desc def_T by auto
  then have 0: "(ψ A T) mod N = (ψ A 0) mod N ∧ (ψ A (T+1)) mod N = (ψ A 1) mod N"
    using f_def by simp
  have "∀k. (ψ A (T+k)) mod N = (ψ A k) mod N"
  proof
    fix k
    show "(ψ A (T+k)) mod N = (ψ A k) mod N" using 0
    proof (induction k rule:ψ_induct)
    case 0
      then show ?case by simp
    next
      case 1
      then show ?case by simp
    next
      case (sucsuc n)
      then have n:"ψ A (T+n) mod N = ψ A (n) mod N"
        using sucsuc.IH(1) sucsuc.prems by simp
      then have n1:"ψ A (T+(Suc n)) mod N = ψ A (Suc n) mod N"
        using sucsuc.IH(1) sucsuc.prems by simp
      have "ψ A (T+(Suc (Suc n))) mod N = (A * ψ A (Suc (T + n)) - ψ A (T + n)) mod N"
        by simp
      also have "... = (A * ψ A (Suc (T + n)) mod N - ψ A (T + n) mod N) mod N"
        by (metis mod_diff_eq)
      also have "... = (A * ψ A (Suc (n)) mod N - ψ A (n) mod N) mod N"
        using n n1 by (metis add_Suc_right mod_mult_cong)
      also have "... = (A * ψ A (Suc (n)) - ψ A (n)) mod N"
        by (metis mod_diff_eq)
      finally have "ψ A (T+(Suc (Suc n))) mod N = ψ A ((Suc (Suc n))) mod N" by simp
      then show ?case using add_2_eq_Suc' by presburger
    qed
  qed
  then show ?thesis using T1 by auto
qed

(* Lemma 3.1, sublemma 8 *)
lemma lucas_modN:
  fixes N::int
  assumes "N>0" 
  shows "∀n. ∃k≥n. ψ A k mod N = 0"
proof
  fix n
  have "∃T≥1. ∀n. (ψ A (T + n)) mod N = (ψ A n) mod N"
    using lucas_periodic_modN assms
    by blast
  then obtain T where def_T: "∀n. (ψ A (T+n)) mod N = (ψ A n) mod N ∧ T≥1"
    by auto
  have 0: "∀k. (ψ A (T * k)) mod N = 0"
  proof
    fix k
    show "(ψ A (T * k)) mod N = 0"
    proof (induction k)
      case 0
      then show ?case by simp
    next
      case (Suc k)
      then show ?case using def_T by simp
    qed
  qed
  define K where def_K : "K ≡ T * n"
  then have 1: "K≥n" using def_T by auto
  have "(ψ A K) mod N = 0" using 0 def_K by auto
  then show "∃k≥n. ψ A k mod N = 0" using 1 by auto
qed

(* Parity *)
lemma lucas_parity:
  fixes A::int and B::nat
  assumes "even A"
  shows "even (ψ A B) = even B"
proof(induction B rule: ψ_induct)
  case 0
  then show ?case
    by simp
next
  case 1
  then show ?case
    by simp
next
  case (sucsuc n)
  then show ?case 
    by (auto simp add: assms)
qed

corollary lucas_parity2:
  fixes A::int and B::nat
  assumes "even A"
  shows "even (ψ A B - int B)"
  by (simp add: assms lucas_parity)


(* Monotonicity in A *)
lemma lucas_monotone_A:
  assumes "1<A" "A≤A'"
  shows "ψ A n ≤ ψ A' n"
proof (induction n rule:ψ_induct)
  case 0
  then show ?case by simp
next
  case 1
  then show ?case by simp
next
  case (sucsuc n)
  note HR = this
  consider (equal) "A=A'" | (strict) "A<A'" using assms by fastforce
  then show ?case
  proof cases
    case equal
    then show ?thesis by simp
  next
    case strict
    have "ψ A n ≥ 0"
    proof (cases "n=0")
      case True
      then show ?thesis by simp
    next
      case False
      then show ?thesis using lucas_strict_monotonicity[of "A" "n-1"] assms by auto
    qed
    then have "ψ A (n + 2) = A * ψ A (n+1) - ψ A n" by simp
    also have "... ≤ A * ψ A (n+1)" using ‹ψ A n ≥ 0› by simp
    also have "... ≤ (A' - 1) * ψ A (n+1)" using ‹A<A'› assms(1) lucas_strict_monotonicity by auto
    also have "... ≤ (A' - 1) * ψ A' (n+1)" using assms HR by simp
    also have "... ≤ A' * ψ A' (n+1) - ψ A' n" using lucas_strict_monotonicity[of "A'" "n"] assms Suc_eq_plus1 int_distrib(3) by fastforce
    finally have "ψ A (n + 2) ≤ ψ A' (n+2)" by simp
    then show ?thesis by simp
  qed
qed

(* Lemma 3.5 *)
lemma lucas_congruence:
  fixes A::int and B::int and n::int
  assumes "n=n ∧ A mod n = B mod n"
  shows "(ψ A m) mod n = (ψ B m) mod n"
proof (induction m rule: ψ_induct)
  case 0
  then show ?case by auto
next
  case 1
  then show ?case by auto
next
  case (sucsuc m)
  note t = this
  have e1: "(A * ψ A (m + 1)) mod n = (B * ψ B (m + 1)) mod n"
    using assms mod_mult_cong sucsuc.IH(1) by blast
  then have e2: "⋀k l. k mod n = l mod n ⟹ (A * ψ A (m + 1) - k) mod n =  (B * ψ B (m + 1) - l) mod n"
    using mod_diff_cong by blast
  have e3: "(A * ψ A (m + 1) - ψ A m) mod n = (B * ψ B (m + 1) - ψ B m) mod n"
    using t e2[of "ψ A m" "ψ B m"] by blast
  then show ?case by auto
qed

(* Corollary 3.6 *)
corollary lucas_congruence2:
  fixes α::int and m::nat
  shows "ψ α m mod (α - 2) = int m mod (α - 2)"
proof -
  have fac1: "ψ 2 a = int a" for a
  proof (induction a rule: ψ_induct)
    case 0
    then show ?case by auto
  next
    case 1
    then show ?case by auto
  next
    case (sucsuc n)
  then show ?case by auto
qed
  have "α mod (α - 2) = 2 mod (α -2)"
    by (smt (z3) minus_mod_self2)
  then have fac2: "ψ α m mod (α - 2) = ψ 2 m mod (α - 2)"
    using lucas_congruence[of "α - 2" α 2 m] by auto
  then show ?thesis using fac2 fac1 by auto
qed

end