Theory Hilbert10_to_Inequality

section ‹Hilbert's 10th Problem to Linear Inequality›

theory Hilbert10_to_Inequality
  imports 
    Preliminaries_on_Polynomials_1
begin

definition hilbert10_problem :: "int mpoly ⇒ bool" where
  "hilbert10_problem p = (∃ α. insertion α p = 0)" 

text ‹A polynomial is positive, if every coefficient is positive.
  Since the ‹@{const coeff}›-function of ‹'a mpoly› maps a coefficient
  to every monomial, this means that positiveness is expressed as
  @{term "coeff p m ≠ 0 ⟶ coeff p m > 0"} for monomials ‹m›. 
  However, this condition is equivalent to just demand @{term "coeff p m ≥ 0"}
  for all ‹m›.

  This is the reason why ‹positive polynomials› are defined in the same way
  as one would define ‹non-negative polynomials›.›
definition positive_poly :: "'a :: linordered_idom mpoly ⇒ bool" where
  "positive_poly p = (∀ m. coeff p m ≥ 0)" 

definition positive_interpr :: "(var ⇒ 'a :: linordered_idom) ⇒ bool" where
  "positive_interpr α = (∀ x. α x > 0)" 

definition positive_poly_problem :: "'a :: linordered_idom mpoly ⇒ 'a mpoly ⇒ bool" where
  "positive_poly p ⟹ positive_poly q ⟹ positive_poly_problem p q = 
    (∃ α. positive_interpr α ∧ insertion α p ≥ insertion α q)" 

datatype flag = Positive | Negative | Zero

fun flag_of :: "'a :: {ord,zero} ⇒ flag" where
  "flag_of x = (if x < 0 then Negative else if x > 0 then Positive else Zero)" 

definition subst_flag :: "var set ⇒ (var ⇒ flag) ⇒ var ⇒ 'a :: comm_ring_1 mpoly" where
  "subst_flag V flag x = (if x ∈ V then (case flag x of
      Positive ⇒ Var x
    | Negative ⇒ - Var x
    | Zero ⇒ 0)
     else 0)" 

definition assignment_flag :: "var set ⇒ (var ⇒ flag) ⇒ (var ⇒ 'a :: comm_ring_1) ⇒ (var ⇒ 'a)" where
  "assignment_flag V flag α x = (if x ∈ V then (case flag x of
      Positive ⇒ α x
    | Negative ⇒ - α x
    | Zero ⇒ 1)
    else 1)"

definition correct_flags :: "var set ⇒ (var ⇒ flag) ⇒ (var ⇒ 'a :: ordered_comm_ring) ⇒ bool" where
  "correct_flags V flag α = (∀ x ∈ V. flag x = flag_of (α x))" 

lemma correct_flag_substitutions: fixes p :: "'a :: linordered_idom mpoly" 
  assumes "vars p ⊆ V" 
    and beta: "β = assignment_flag V flag α" 
    and sigma: "σ = subst_flag V flag" 
    and q: "q = substitute σ p"  
    and corr: "correct_flags V flag α"
  shows "insertion β q = insertion α p" "positive_interpr β"
proof -
  show "insertion β q = insertion α p" unfolding q insertion_substitute
  proof (rule insertion_irrelevant_vars)
    fix x
    assume "x ∈ vars p" 
    with assms have x: "x ∈ V" by auto
    with corr have flag: "flag x = flag_of (α x)" unfolding correct_flags_def by auto
    
    show "insertion β (σ x) = α x" 
      unfolding beta sigma assignment_flag_def subst_flag_def using x flag
      by (cases "flag x", auto split: if_splits simp: insertion_Var insertion_uminus)
  qed
  show "positive_interpr β" using corr
    unfolding positive_interpr_def beta assignment_flag_def correct_flags_def
    by auto
qed

definition hilbert_encode1 :: "int mpoly ⇒ int mpoly list" where
  "hilbert_encode1 r = (let r2 = r^2;
     V = vars_list r2;
     flag_lists = product_lists (map (λ x. map (λ f. (x,f)) [Positive,Negative,Zero]) V);
     subst = (λ fl. subst_flag (set V) (λ x. case map_of fl x of Some f ⇒ f | None ⇒ Zero))
    in map (λ fl. substitute (subst fl) r2) flag_lists)"  

lemma hilbert_encode1: 
  "hilbert10_problem r ⟷ (∃ p ∈ set (hilbert_encode1 r). ∃ α. positive_interpr α ∧ insertion α p ≤ 0)" 
proof 
  define r2 where "r2 = r^2" 
  define V where "V = vars_list r2" 
  define flag_list where "flag_list = product_lists (map (λ x. map (λ f. (x,f)) [Positive,Negative,Zero]) V)" 
  define subst where "subst = (λ fl. subst_flag (set V) (λ x. case map_of fl x of Some f ⇒ f | None ⇒ Zero) :: var ⇒ int mpoly)" 
  have hilb_enc: "hilbert_encode1 r = map (λ fl. substitute (subst fl) r2) flag_list" 
    unfolding subst_def flag_list_def V_def r2_def Let_def hilbert_encode1_def ..
  have "hilbert10_problem r ⟷ (∃ α. insertion α r = 0)" unfolding hilbert10_problem_def by auto
  also have "… ⟷ (∃ α. (insertion α r)^2 ≤ 0)" 
    by (intro ex_cong1, auto)
  also have "… ⟷ (∃ α. insertion α r2 ≤ 0)" 
    by (intro ex_cong1, auto simp: power2_eq_square insertion_mult r2_def)
  finally have hilb: "hilbert10_problem r = (∃α. insertion α r2 ≤ 0)" (is "?h1 = ?h2") .
  let ?r1 = "(∃ p ∈ set (hilbert_encode1 r). ∃ α. positive_interpr α ∧ insertion α p ≤ 0)" 
  {
    assume ?r1
    from this[unfolded hilb_enc]
    show "hilbert10_problem r" unfolding hilb by (auto simp add: insertion_substitute)
  }
  {
    assume ?h1
    with hilb obtain α where solution: "insertion α r2 ≤ 0" by auto
    define fl where "fl = map (λ x. (x, flag_of (α x))) V" 
    define flag where "flag = (λ x. case map_of fl x of Some f ⇒ f | None ⇒ Zero)" 
    have vars: "vars r2 ⊆ set V" unfolding V_def by simp
    have fl: "fl ∈ set flag_list" unfolding flag_list_def product_lists_set fl_def
      apply (simp add: list_all2_map2 list_all2_map1, intro list_all2_refl)
      by auto
    have mem: "substitute (subst_flag (set V) flag) r2 ∈ set (hilbert_encode1 r)" 
      unfolding hilb_enc subst_def flag_def using fl by auto
    have corr: "correct_flags (set V) flag α" unfolding correct_flags_def flag_def fl_def
      by (auto split: option.splits dest!: map_of_SomeD simp: map_of_eq_None_iff image_comp)
    show ?r1 using solution correct_flag_substitutions[OF vars refl refl refl corr]
      by (intro bexI[OF _ mem], auto)
  }
qed

lemma pos_neg_split: "mpoly_coeff_filter (λ x. (x :: 'a :: linordered_idom) > 0) p + mpoly_coeff_filter (λ x. x < 0) p = p" (is "?l + ?r = p")
proof -
  {
    fix m
    let ?c = "coeff p m" 
    have "coeff (?l + ?r) m = coeff ?l m + coeff ?r m" by (simp add: coeff_add)
    also have "… = coeff p m" unfolding mpoly_coeff_filter 
      by (cases "?c < 0"; cases "?c > 0"; cases "?c = 0", auto)
    finally have "coeff (?l + ?r) m = coeff p m" .
  }
  thus ?thesis using coeff_eq by blast
qed

definition hilbert_encode2 :: "int mpoly ⇒ int mpoly × int mpoly" where
  "hilbert_encode2 p = 
     (- mpoly_coeff_filter (λ x. x < 0) p, mpoly_coeff_filter (λ x. x > 0) p)" 

lemma hilbert_encode2: assumes "hilbert_encode2 p = (r,s)" 
  shows "positive_poly r" "positive_poly s" "insertion α p ≤ 0 ⟷ insertion α r ≥ insertion α s" 
proof -
  from assms[unfolded hilbert_encode2_def, simplified]
  have s: "s = mpoly_coeff_filter (λ x. x > 0) p" 
    and r: "r = - mpoly_coeff_filter (λ x. x < 0) p" (is "_ = - ?q") by auto
  have "p = s + ?q" unfolding s using pos_neg_split[of p] by simp
  also have "… = s - r" unfolding s r by simp
  finally have "insertion α p ≤ 0 ⟷ insertion α (s - r) ≤ 0" by simp
  also have "insertion α (s - r) = insertion α s - insertion α r" 
    by (metis add_uminus_conv_diff insertion_add insertion_uminus)
  finally show "insertion α p ≤ 0 ⟷ insertion α r ≥ insertion α s" by auto
  show "positive_poly s" unfolding positive_poly_def s using mpoly_coeff_filter[of "(λ x. x > 0)" p]
    by (auto simp: when_def)
  show "positive_poly r" unfolding positive_poly_def r coeff_uminus using mpoly_coeff_filter[of "(λ x. x < 0)" p]
    by (auto simp: when_def)
qed

definition hilbert_encode :: "int mpoly ⇒ (int mpoly × int mpoly)list" where
  "hilbert_encode = map hilbert_encode2 o hilbert_encode1" 

text ‹Lemma 2.2 in paper›

lemma hilbert_encode_positive: "hilbert10_problem p 
  ⟷ (∃ (r,s) ∈ set (hilbert_encode p). positive_poly_problem r s)"
proof -
  have "hilbert10_problem p ⟷ (∃p'∈set (hilbert_encode1 p). ∃α. positive_interpr α ∧ insertion α p' ≤ 0)" 
    using hilbert_encode1[of p] by blast
  also have "… ⟷ (∃ (r,s) ∈ set (hilbert_encode p). positive_poly_problem r s)" (is "?l = ?r")
  proof
    assume ?l
    then obtain p' α where mem: "p'∈set (hilbert_encode1 p)" and sol: "positive_interpr α" "insertion α p' ≤ 0" by blast
    obtain r s where 2: "hilbert_encode2 p' = (r,s)" by force
    from mem 2 have mem: "(r,s) ∈ set (hilbert_encode p)" unfolding hilbert_encode_def o_def by force
    from hilbert_encode2[OF 2] sol have "positive_poly_problem r s" using positive_poly_problem_def[of r s] by force
    with mem show ?r by blast
  next
    assume ?r
    then obtain r s where mem: "(r,s) ∈ set (hilbert_encode p)" and sol: "positive_poly_problem r s" by auto
    from mem[unfolded hilbert_encode_def o_def] obtain p' where 
      mem: "p' ∈ set (hilbert_encode1 p)" 
      and "hilbert_encode2 p' = (r,s)" by force
    from hilbert_encode2[OF this(2)] sol positive_poly_problem_def[of r s]
    have "(∃α. positive_interpr α ∧ insertion α p' ≤ 0)" by auto
    with mem hilbert_encode1[of p] show ?l by auto
  qed
  finally show ?thesis .
qed

end