Theory Matiyasevich_Polynomial

theory Matiyasevich_Polynomial
  imports M3_Polynomial Digit_Expansions.Binary_Operations Pi_to_M3_rat
begin

subsection ‹The key property of $M_3$›

context matiyasevich_polynomial
begin

(* The comments in the following lemma explain what the syntax abstraction
   used here means under the hood. *)
lemma relation_combining':
  fixes R S T A1 A2 A3 :: int
  assumes "S≠0"
  (* defines "γ' ≡ (λn. (λ_. 0)(1 := A1, 2 := A2, 3 := A3, 4 := S, 5 := T, 6 := R, 11 := n))" *)
  defines "γ' ≡ λ(n :: int) fn. fn A1 A2 A3 S T R n :: int"
  (* shows "(S dvd T ∧ R > 0 ∧ is_square A1 ∧ is_square A2 ∧ is_square A3)
       = (∃n. n≥0 ∧ insertion (γ' n) M3_poly = 0)" (is "?LHS = ?RHS") *)
  shows "(S dvd T ∧ R > 0 ∧ is_square A1 ∧ is_square A2 ∧ is_square A3)
       = (∃n. n≥0 ∧ (γ' n) M3 = 0)" (is "?LHS = ?RHS")
proof -

  have U_not_0: "S^2 * (2*R - 1) ≠ 0"
    using ‹S ≠ 0› apply simp by presburger

  define φ :: "nat ⇒ int mpoly" where
    "φ = (λ_. 0)(0 := Var 0, 1 := Const A1, 2 := Const A2, 3 := Const A3)"
  define ℱ where "ℱ ≡ poly_subst φ J3"
  define r where "r ≡ MPoly_Type.degree ℱ 0"
  define Π where "Π ≡ pi_relations.Π ℱ 0"

  define X where "X ≡ 1 + A1^2 + A2^2 + A3^2"
  define I where "I ≡ X^3"

  have F_repr: "ℱ = ((x^2+Const A1+Const A2*(Const X^2)-Const A3*(Const X^4))^2 + 4*x^2*Const A1
                      - 4*x^2*Const A2*Const X^2 - 4*Const A1*Const A2*Const X^2)^2
              - Const A1 * ((4*x*(x^2+Const A1+Const A2*Const X^2 - Const A3*Const X^4)
                              -  8*x*Const A2*Const X^2))^2"
    unfolding ℱ_def φ_def J3_def X_def
    unfolding power2_eq_square power4_eq_xxxx section5_given.defs
    by (simp add: Const_add[symmetric] Const_mult[symmetric])

  have F_zeros_bound: "∀x. insertion (λ_. x) ℱ = 0 ⟶ - I < x" 
  proof - 
    have aux0: "⋀x. (λ_. 0::int)(0 := x, 1 := A1, 2 := A2, 3 := A3)
                     = insertion (λ_. x) ∘ φ"
      unfolding φ_def by auto

    show ?thesis
      using J3_zeros_bound aux0[symmetric]
      unfolding ℱ_def I_def X_def insertion_poly_subst comp_def
      by simp
  qed

  have deg_phi: "MPoly_Type.degree (φ i) 0 = (1 when i = 0)" for i
      unfolding φ_def by simp

  have aux5: "MPoly_Type.degree P2 v2 ≤ k ⟹
      MPoly_Type.degree Q2 v2 ≤ k ⟹ MPoly_Type.degree (Q2 + P2) v2 ≤ k" for k v2
    and P2 Q2 :: "int mpoly"
    by (simp add: le_trans[OF degree_add max.boundedI])

  have "r ≤ 8"
    unfolding r_def F_repr power2_eq_square
    apply (simp add: algebra_simps)
    apply (simp add: power2_eq_square[symmetric] power_Suc[symmetric] mult.assoc[symmetric])
    unfolding x_def Const_power Const_numeral[symmetric] mult.assoc Const_mult
    apply (rule le_trans[OF degree_diff max.boundedI])
    apply (rule aux5)+
    unfolding degree_Const apply simp_all
    apply (subst le_trans[OF degree_mult] le_trans[OF degree_pow]; simp)+
    apply (rule aux5)+
    unfolding degree_Const apply simp_all
    by (subst le_trans[OF degree_mult] le_trans[OF degree_pow]; simp)+

  have eq_coeff: "MPoly_Type.coeff ℱ (Poly_Mapping.single 0 8) = 1"
    unfolding F_repr power2_eq_square
    apply (simp add: algebra_simps)
    unfolding Notation.coeff_minus[symmetric] More_MPoly_Type.coeff_add[symmetric]
    apply (simp add: power2_eq_square[symmetric] power_Suc[symmetric] mult.assoc[symmetric])
    unfolding x_def
    apply (subst coeff_var_power_eq)
    apply (subst mult.assoc)+
    apply (subst coeff_var_power_le; simp)+
    unfolding Const_power Const_mult Const_numeral[symmetric]
    by (subst coeff_const; simp)+

  hence "MPoly_Type.degree ℱ 0 ≥ 8"
    unfolding MPoly_Type.degree.rep_eq apply (intro Max_ge)
    subgoal by simp
    apply (rule insertI2)
    unfolding keys.rep_eq image_iff bex_simps(6) coeff_def
    apply (rule exI[of _ "Poly_Mapping.single 0 8"])
    by simp

  with ‹r ≤ 8› r_def have "r = 8" by auto
  
  interpret pi_relations: pi_relations ℱ 0
  proof (unfold_locales)
    show "vars ℱ ⊆ {0}"
      unfolding ℱ_def
      apply (rule subset_trans[OF vars_poly_subst[of φ J3]])
      unfolding φ_def
      using J3_vars by auto
  next
    have "MPoly_Type.coeff ℱ (Poly_Mapping.single 0 r) = 1"
      by (simp add: `r=8` eq_coeff)

    thus "MPoly_Type.coeff ℱ (Abs_poly_mapping (λk. MPoly_Type.degree ℱ 0 when k = 0)) = 1"
      unfolding r_def single.abs_eq by simp
  qed

  define η :: "nat ⇒ nat ⇒ int" where "η ≡ λn. (λ_. 0)(4:=S, 5:=T, 6:=R, 7:=I, 11:=n)"

  have insertion_F_squares:
    "(∃x. insertion (λ_. x) ℱ = 0) = (is_square A1 ∧ is_square A2 ∧ is_square A3)"
  proof - 
    have insertion_equivalence: "insertion (λ_. x) ∘ φ 
                               = (λ_. 0)(0 := x, 1 := A1, 2 := A2, 3 := A3)" for x
        unfolding φ_def comp_def by auto

    have "(∃x. insertion (λ_. x) ℱ = 0)
        = (∃y. insertion ((λ_. 0)(0 := y, 1 := A1, 2 := A2, 3 := A3)) J3 = 0)" (is "?F = ?J3")
    proof (rule iffI) 
      assume ?F
      then obtain x where x: "0 = insertion (λ_. x) (poly_subst φ J3)"
        unfolding ℱ_def by auto

      hence "insertion (insertion (λ_. x) ∘ φ) J3 = 0"        
        using insertion_poly_subst[of "λ_. x" φ J3] by auto

      with insertion_equivalence have 
        "insertion ((λ_. 0)(0 := x, 1 := A1, 2 := A2, 3 := A3)) J3 = 0"
        by auto 

      thus ?J3 by auto
    next 
      assume ?J3
      then obtain y where "insertion ((λ_. 0)(0 := y, 1 := A1, 2 := A2, 3 := A3)) J3 = 0"
        by auto

      hence "insertion (λ_. y) (poly_subst φ J3) = 0"
        unfolding insertion_poly_subst insertion_equivalence by auto

      thus ?F unfolding ℱ_def by auto
    qed

    thus ?thesis
      unfolding J3_encodes_three_squares by auto
  qed

  hence M3_Π_equivalence: "insertion ((λ_. 0)(4:=S, 5:=T, 6:=R, 7:=I, 11:=n)) Π  
                          = M3 π" for n 
    unfolding Π_def I_def X_def
    using U0_def Pi_equals_M3_rationals[of A1 A2 A3 S T R]
    using U_not_0
    unfolding U0_def X0_def
    using pi_relations.F_monom_over_v local.pi_relations.F_one
    unfolding ℱ_def φ_def
    using ‹r = 8›
    unfolding r_def ℱ_def φ_def
    by simp

  have direct_imp: "?LHS ⟶ ?RHS"
  proof
    assume asm: "?LHS"
    have "S dvd T" using asm by auto
    have "R > 0" using asm by auto
    have "∃y. insertion (λ_. y) ℱ = 0"
      using insertion_F_squares asm by auto

    then obtain y where "insertion (λ_. y) ℱ = 0" by auto

    then obtain n where pi_result: "insertion (η n) Π = 0 
                                 ∧ int n = (2 * R - 1) * (y + I + T2) - (T div S)2"
      using pi_relations.Π_encodes_correctly[of S I T R, OF ‹S ≠ 0› F_zeros_bound ‹S dvd T› ‹R > 0›]
      unfolding η_def Π_def by auto

    show "?RHS" 
      apply (rule exI[of _ "int n"], simp)
      unfolding γ'_def
      unfolding M3_Π_equivalence[symmetric] 
      using pi_result unfolding η_def by auto
  qed
  
  have recipr_imp: "?RHS ⟶ ?LHS"
  proof (rule impI) 
    assume "?RHS"
    then obtain n where "n≥0 ∧ M3 π = 0"
      unfolding γ'_def by auto

    hence "insertion (η (nat n)) Π = 0"
      unfolding η_def using M3_Π_equivalence by auto

    hence pi_relations: "S dvd T ∧ 0 < R ∧ (∃x. insertion (λ_. x) ℱ = 0)"
      using pi_relations.Π_encodes_correctly_2[of S I T R, OF ‹S ≠ 0› F_zeros_bound]
      unfolding Π_def[symmetric] η_def by blast

    show "?LHS" using pi_relations insertion_F_squares by auto
  qed

  then show ?thesis using direct_imp by blast
qed

lemma relation_combining:
  assumes "S≠0"
  shows "(S dvd T ∧ R > 0 ∧ is_square A1 ∧ is_square A2 ∧ is_square A3)
         = (∃n≥0. M3 A1 A2 A3 S T R n = 0)"
  using relation_combining' assms by auto
end

end