Theory Renegar_Modified

(* This file generalizes the previous univariate formalization of BKR
and Renegar (see https://www.isa-afp.org/entries/BenOr_Kozen_Reif.html) 
so as not to use the Cauchy root bound, which is specific to univariate 
polynomials and does not generalize to our multivariate setting.
 *)

theory Renegar_Modified

imports "BenOr_Kozen_Reif.Renegar_Decision"

begin

definition poly_f_nocrb :: "real poly list ⇒ real poly"
  where
    "poly_f_nocrb ps = 
  (if (check_all_const_deg ps = True) then  [:0, 1:] else 
  (pderiv (prod_list_var ps)) * (prod_list_var ps))"

lemma root_set_nocrb:
  assumes is_not_const: "check_all_const_deg qs = False"
  shows "{x. poly (poly_f qs) x = 0}
 = {x. poly (poly_f_nocrb qs) x = 0} ∪ {-(crb (prod_list_var qs)), (crb (prod_list_var qs))}"
proof - 
  have "∀x ∈ {x. poly (poly_f qs) x = 0}. poly (poly_f qs) x = 0" by auto
  then have all: "∀x ∈ {x. poly (poly_f qs) x = 0}. poly ((pderiv (prod_list_var qs)) * (prod_list_var qs)* ([:-(crb (prod_list_var qs)),1:]) * ([:(crb (prod_list_var qs)),1:])) x = 0"
    unfolding poly_f_def using is_not_const by presburger 
  have all1: "∀x ∈ {x. poly (poly_f qs) x = 0}.
    ((poly ((pderiv (prod_list_var qs)) * (prod_list_var qs)) x = 0)
    ∨ (poly (([:-(crb (prod_list_var qs)),1:]) * ([:(crb (prod_list_var qs)),1:])) x = 0))"
  proof clarsimp
    fix x
    assume inset: "poly (poly_f qs) (real_of_int x) = 0 "
    assume "poly (pderiv (prod_list_var qs)) (real_of_int x) ≠ 0"
    assume "x * x ≠ crb (prod_list_var qs) * crb (prod_list_var qs)"
    have "poly ((pderiv (prod_list_var qs)) * (prod_list_var qs)* ([:-(crb (prod_list_var qs)),1:]) * ([:(crb (prod_list_var qs)),1:])) x = 0"
      using all inset by auto
    then show "poly (prod_list_var qs) (real_of_int x) = 0" using assms
      by (smt (verit, del_insts) ‹poly (pderiv (prod_list_var qs)) (real_of_int x) ≠ 0› ‹x * x ≠ crb (prod_list_var qs) * crb (prod_list_var qs)› mult.commute mult_eq_0_iff mult_minus_left of_int_eq_iff of_int_minus poly_mult poly_root_factor(3))
  qed
  have "∀x. (poly (([:-(crb (prod_list_var qs)),1:]) * ([:(crb (prod_list_var qs)),1:])) x = 0 ⟶
  (x = -(crb (prod_list_var qs)) ∨ x = (crb (prod_list_var qs))))"
    by (simp add: square_eq_iff)
  then have "∀x ∈ {x. poly (poly_f qs) x = 0}.
    ((poly (poly_f_nocrb qs) x = 0)
    ∨ (x = -(crb (prod_list_var qs)) ∨ x = (crb (prod_list_var qs))))"
    using all1 unfolding poly_f_nocrb_def
    by (smt (verit, del_insts) all is_not_const of_int_minus poly_root_factor(2)) 
  then have subset1: "{x. poly (poly_f qs) x = 0}
 ⊆ {x. poly (poly_f_nocrb qs) x = 0} ∪ {-(crb (prod_list_var qs)), (crb (prod_list_var qs))}"
    using UnCI is_not_const mem_Collect_eq by fastforce
  have subset2: "{x. poly (poly_f_nocrb qs) x = 0} ∪ {-(crb (prod_list_var qs)), (crb (prod_list_var qs))} ⊆
   {x. poly (poly_f qs) x = 0}"
    using Un_insert_right insert_iff is_not_const mem_Collect_eq of_int_minus poly_f_def poly_f_nocrb_def by auto
  then show ?thesis using subset1 subset2 by auto
qed

lemma nonzcrb_helper:
  assumes q_in: "q ∈ set qs"
  assumes qnonz: "q ≠ 0"
  assumes lengt: "length (sorted_list_of_set {(x::real). (∃q ∈ set(qs). (q ≠ 0 ∧ poly q x = 0))} :: real list) > 0"
  shows " ¬(∃x ≥ (real_of_int (crb (prod_list_var qs))). poly q x = 0)" 
proof clarsimp 
  fix x
  assume xgt: "real_of_int (crb (prod_list_var qs)) ≤ x" 
  assume pqz: "poly q x = 0"
  let ?zer_list = "sorted_list_of_set {(x::real). (∃q ∈ set(qs). (q ≠ 0 ∧ poly q x = 0))} :: real list"
  have strict_sorted_h: "sorted_wrt (<) ?zer_list" using sorted_sorted_list_of_set
      strict_sorted_iff by auto
  have finset: "finite  {x. ∃q∈set qs. q ≠ 0 ∧ poly q x = 0}"
  proof - 
    have "∀q ∈ set qs.  q≠ 0 ⟶ finite {x. poly q x = 0} "
      using poly_roots_finite by auto
    then show ?thesis by auto
  qed
  have all_prop: "∀x ∈ {x. ∃q∈set qs. q ≠ 0 ∧ poly q x = 0}. poly (prod_list_var qs) x = 0"
    using q_dvd_prod_list_var_prop
    by fastforce 
  then have "poly (prod_list_var qs) (sorted_list_of_set {x. ∃q∈set qs. q ≠ 0 ∧ poly q x = 0} ! 0) = 0"
    using finset set_sorted_list_of_set
    by (metis (no_types, lifting) lengt nth_mem) 
  then have crbgt: "crb (prod_list_var qs) > ?zer_list ! (length ?zer_list - 1)" using prod_list_var_nonzero crb_lem_pos[of "prod_list_var qs" "?zer_list ! (length ?zer_list - 1)"]
    by (metis (no_types, lifting) all_prop diff_less finset lengt less_numeral_extra(1) nth_mem set_sorted_list_of_set) 
  have x_in: "x ∈ {x. ∃q∈set qs. q ≠ 0 ∧ poly q x = 0}"
    using pqz q_in qnonz 
    by auto
  then have "x ∈ set ?zer_list"
    by (smt (verit, best) finset in_set_member mem_Collect_eq set_sorted_list_of_set) 
  then have "x ≤ ?zer_list ! (length ?zer_list - 1)" using strict_sorted_h
    by (meson all_prop x_in crb_lem_pos not_less prod_list_var_nonzero xgt)
  then show "False" using xgt crbgt 
    by auto
qed

lemma root_set_nocrb_var:
  assumes is_not_const: "check_all_const_deg qs = False"
  shows "({x. poly (poly_f qs) x = 0}::real set)
 = {x. poly (poly_f_nocrb qs) x = 0} ∪ (({-(crb (prod_list_var qs)), (crb (prod_list_var qs))})::real set)"
  using root_set_nocrb apply (auto)
     apply (smt (verit) of_int_minus poly_f_def poly_f_nocrb_def poly_root_factor(2))
    apply (simp add: is_not_const poly_f_def)
  using is_not_const apply blast
  by (metis (no_types, lifting) poly_f_def poly_f_nocrb_def poly_root_factor(2))

lemma nonzcrb:
  assumes q_in: "q ∈ set qs"
  assumes qnonz: "q ≠ 0"
  shows " ¬(∃x ≥ (real_of_int (crb (prod_list_var qs))). poly q x = 0)" 
proof - 
  let ?zer_list = "(sorted_list_of_set {(x::real). (∃q ∈ set(qs). (q ≠ 0 ∧ poly q x = 0))} :: real list)"
  have eo: "length ?zer_list = 0 ∨ length ?zer_list > 0"
    by auto 
  have h1: "length ?zer_list = 0 ⟶ ¬(∃x ≥ (real_of_int (crb (prod_list_var qs))). poly q x = 0)"
    by (metis crb_lem_pos dvdE linorder_not_less mult_zero_left poly_mult prod_list_var_nonzero q_dvd_prod_list_var_prop q_in qnonz)
  have h2: "length ?zer_list > 0 ⟶ ¬(∃x ≥ (real_of_int (crb (prod_list_var qs))). poly q x = 0)"
    using nonzcrb_helper assms
    by blast 
  show ?thesis using eo h1 h2 
    by auto 
qed

definition sgn_pos_inf_rat_list:: "real poly list ⇒ int list"
  where "sgn_pos_inf_rat_list l = map (λx.  (Sturm_Tarski.sign (sgn_pos_inf x))) l"

definition sgn_neg_inf_rat_list:: "real poly list ⇒ int list"
  where "sgn_neg_inf_rat_list l = map (λx.  (Sturm_Tarski.sign (sgn_neg_inf x))) l"

definition sgn_neg_inf_rat_list2:: "real poly list ⇒ rat list"
  where "sgn_neg_inf_rat_list2 l = map (λx.  ((rat_of_int ∘ Sturm_Tarski.sign) (sgn_neg_inf x))) l"

definition sgn_pos_inf_rat_list2:: "real poly list ⇒ rat list"
  where "sgn_pos_inf_rat_list2 l = map (λx.  ((rat_of_int ∘ Sturm_Tarski.sign) (sgn_pos_inf x))) l"

lemma root_ub_restate:
  fixes p:: "real poly"
  assumes pnonz: "p ≠ 0"
  fixes z::"real"
  assumes zgt: "∀x. poly p x=0 ⟶ x < z"
  shows "x≥z ⟹ sgn (poly p x) = Sturm_Tarski.sign (sgn_pos_inf p)"
proof - 
  assume xgt: "x≥z"
  have allx: "∀x ≥ z. sgn (poly p x) = sgn (poly p z)"
  proof clarsimp 
    fix x
    assume zleq: "z ≤ x"
    then have xnonz: "sgn (poly p x) ≠ 0"
      using zgt unfolding sgn_def by auto
    have znonz: "sgn (poly p z) ≠ 0"
      using zgt unfolding sgn_def by auto 
    have "Matrix_Equation_Construction.sgn (poly p x) ≠ Matrix_Equation_Construction.sgn (poly p z) ⟹ False"
    proof - 
      assume neq: "Matrix_Equation_Construction.sgn (poly p x) ≠ Matrix_Equation_Construction.sgn (poly p z)"
      then have z_lt: "z < x" using zleq
        using less_eq_real_def by force
      have h1: "z < x ⟹
        Matrix_Equation_Construction.sgn (poly p z) ≠ 0 ⟹
        Matrix_Equation_Construction.sgn (poly p x) ≠ 0 ⟹
        ¬ poly p x < 0 ⟹ 0 < poly p x"
        using zgt by fastforce
      have h2: "z < x ⟹
        Matrix_Equation_Construction.sgn (poly p z) ≠ 0 ⟹
        Matrix_Equation_Construction.sgn (poly p x) ≠ 0 ⟹
        ¬ poly p x < 0 ⟹ poly p z < 0"
        by (metis neq sgn_def)
      have h3: "z < x ⟹
        Matrix_Equation_Construction.sgn (poly p z) ≠ 0 ⟹
        Matrix_Equation_Construction.sgn (poly p x) ≠ 0 ⟹
        ¬ 0 < poly p z ⟹ 0 < poly p x"
        by (metis neq sgn_def) 
      have h4: "z < x ⟹
        Matrix_Equation_Construction.sgn (poly p z) ≠ 0 ⟹
        Matrix_Equation_Construction.sgn (poly p x) ≠ 0 ⟹
        ¬ 0 < poly p z ⟹ poly p z < 0"
        using h2 h3 by linarith
       have "((poly p x) > 0 ∧ (poly p z) < 0) ∨ ((poly p x) < 0 ∧ (poly p z) > 0) "
         using z_lt znonz xnonz h1 h2 h3 h4
         by auto
      then have "∃w. w > x ∧ w < z ∧ (poly p w = 0)"
        using poly_IVT_pos[of z x] poly_IVT_neg[of z x]
        by (metis ‹z < x› not_less_iff_gr_or_eq zgt) 
      then show "False"
        using zgt
        using zleq by linarith 
    qed
    then show "Matrix_Equation_Construction.sgn (poly p x) = Matrix_Equation_Construction.sgn (poly p z)"
      by auto
  qed
  have "(∃ub.
          (∀x≥ub. sgn_class.sgn (poly p x) = sgn_pos_inf p))"
    using root_ub[of p] pnonz 
    by meson 
  then obtain ub where ub_prop: "(∀x≥ub. sgn_class.sgn (poly p x) = sgn_pos_inf p)"
    by auto
  let ?ub2 = "max ub (z+1)"
  have "(∀x≥?ub2. sgn_class.sgn (poly p x) = sgn_pos_inf p) ∧ (?ub2 > z)"
    using ub_prop by auto
  then have h1: "(Sturm_Tarski.sign(sgn_class.sgn (poly p ?ub2)::real)) = Sturm_Tarski.sign(sgn_pos_inf p) ∧ (?ub2 > z)"
    by auto
  have "(Sturm_Tarski.sign(sgn_class.sgn (poly p ?ub2)::real)) = (sgn (poly p ?ub2))"
    unfolding sign_def sgn_def by auto
  then have "(sgn (poly p ?ub2)) = (Sturm_Tarski.sign(sgn_pos_inf p)) ∧ (?ub2 > z)" 
    using h1
    by metis 
  then have "∀x≥z. sgn (poly p x) = Sturm_Tarski.sign (sgn_pos_inf p)"
    using allx 
    by (metis dual_order.refl max.absorb3 max.bounded_iff) 
  then show ?thesis using xgt
    by auto
qed

lemma limit_pos_infinity_helper1:
  assumes q_in: "q ∈ set qs"
  assumes qnonz: "q ≠ 0"
  assumes "x = (crb (prod_list_var qs))"
  shows "(if (poly q x > 0) then (1::int) else (if (poly q x = 0) then (0::rat) else (-1::rat))) 
    = ((Sturm_Tarski.sign (sgn_pos_inf q))::int)"
  using poly_sgn_eventually_at_top[unfolded eventually_at_top_linorder] 
proof - 
  have "(∃ub. (∀x. poly q x = 0 ⟶ x < ub ⟶
          (∀x≥ub. sgn_class.sgn (poly q x) = sgn_pos_inf q)))"
    using root_ub[of q] qnonz 
    by meson 
  then obtain ub where ub_prop: "(∀x. poly q x = 0 ⟶ x < ub ⟶
          (∀x≥ub. sgn_class.sgn (poly q x) = sgn_pos_inf q))"
    by auto
  show ?thesis
    proof -
    have "q ∈ set qs ∧ q ≠ 0"
      using q_in qnonz by blast
    then have f1: "∀r. ¬ real_of_int (crb (prod_list_var qs)) ≤ r ∨ 0 ≠ poly q r"
      by (metis (no_types) nonzcrb[of q])
    have f2: "real_of_int (crb (prod_list_var qs)) ≤ real_of_int x"
      using assms(3) by force
    then have f3: "0 ≠ poly q (real_of_int x)"
      using f1 by blast
    have comb1: "⋀z x. ⟦q ≠ 0; ∀x. poly q x = 0 ⟶ x < z; z ≤ x⟧ ⟹ of_rat (Matrix_Equation_Construction.sgn (poly q x)) = complex_of_int (Sturm_Tarski.sign (sgn_pos_inf q))"
       using assms(2) root_ub_restate[of q] by auto
    obtain rr :: real where
      "q ≠ 0 ∧ (0 = poly q rr ⟶ rr < real_of_int (crb (prod_list_var qs))) ∧ real_of_int (crb (prod_list_var qs)) ≤ real_of_int x ⟶ Sturm_Tarski.sign (sgn_pos_inf q) = Matrix_Equation_Construction.sgn (poly q (real_of_int x))"
      by (metis comb1)
    then have f4: "Sturm_Tarski.sign (sgn_pos_inf q) = Matrix_Equation_Construction.sgn (poly q (real_of_int x))"
      using f2 f1 linorder_not_less qnonz by blast
    have "Matrix_Equation_Construction.sgn (poly q (real_of_int x)) = (if 0 < poly q (real_of_int x) then 1 else if poly q (real_of_int x) < 0 then - 1 else 0) ∧ (if 0 < poly q (real_of_int x) then (1::rat) = (if 0 < poly q (real_of_int x) then 1 else if poly q (real_of_int x) < 0 then - 1 else 0) else (if 0 < poly q (real_of_int x) then 1::rat else if poly q (real_of_int x) < 0 then - 1 else 0) = (if poly q (real_of_int x) < 0 then - 1 else 0)) ∧ (if poly q (real_of_int x) < 0 then - (1::rat) = (if poly q (real_of_int x) < 0 then - 1 else 0) else (0::rat) = (if poly q (real_of_int x) < 0 then - 1 else 0))"
      by (simp add: sgn_def)
    moreover
    { assume "- (1::int) ≠ (if poly q (real_of_int x) < 0 then - 1 else 0)"
      then have "0 < poly q (real_of_int x)"
        using f3 by (metis (no_types) not_less_iff_gr_or_eq) }
    ultimately show ?thesis
      by (smt (verit) Rat.of_rat_1 f4 of_int_hom.hom_one) 
  qed
qed

lemma limit_pos_infinity_helper2:
  assumes q_in: "q ∈ set qs"
  assumes qnonz: "q = 0"
  assumes "x = (crb (prod_list_var qs))"
  shows "(if (poly q x > 0) then (1::rat) else (if (poly q x = 0) then (0::rat) else (-1::rat))) 
    = ((Sturm_Tarski.sign (sgn_pos_inf q))::int)"
proof - 
  have "0 = ((Sturm_Tarski.sign (sgn_pos_inf q)))"
    by (simp add: qnonz sgn_pos_inf_def) 
  then show ?thesis using qnonz
    by auto 
qed

lemma limit_pos_infinity_helper:
  assumes q_in: "q ∈ set qs"
  assumes "x = (crb (prod_list_var qs))"
  shows "(if (poly q x > 0) then (1::int) else (if (poly q x = 0) then 0 else -1)) 
    = ((Sturm_Tarski.sign (sgn_pos_inf q)))"
  using limit_pos_infinity_helper1 limit_pos_infinity_helper2 assms(2) q_in
  by (smt (verit) Rat.of_rat_1 Sturm_Tarski.sign_cases of_int_eq_iff of_int_hom.hom_one of_int_hom.hom_zero of_rat_0 of_rat_neg_one one_neq_neg_one zero_neq_neg_one)

lemma Sturm_Tarski_casting:
  shows "((Sturm_Tarski.sign x)) = rat_of_int (Sturm_Tarski.sign x)"
  by (simp add: Sturm_Tarski.sign_def)

lemma limit_pos_infinity:
  shows "consistent_sign_vec qs (crb (prod_list_var qs)) = sgn_pos_inf_rat_list qs"
  unfolding consistent_sign_vec_def sgn_pos_inf_rat_list_def 
  using limit_pos_infinity_helper Sturm_Tarski_casting
  apply (auto) 
    apply fastforce
   apply presburger
  by (metis of_int_hom.hom_one of_int_minus)

lemma nonzcrb_helper_neg:
  assumes q_in: "q ∈ set qs"
  assumes qnonz: "q ≠ 0"
  assumes lengt: "length (sorted_list_of_set {(x::real). (∃q ∈ set(qs). (q ≠ 0 ∧ poly q x = 0))} :: real list) > 0"
  shows " ¬(∃x ≤ (real_of_int (-crb (prod_list_var qs))). poly q x = 0)" 
proof clarsimp 
  fix x
  assume xlt: "x ≤ - real_of_int (crb (prod_list_var qs))" 
  assume pqz: "poly q x = 0"
  let ?zer_list = "sorted_list_of_set {(x::real). (∃q ∈ set(qs). (q ≠ 0 ∧ poly q x = 0))} :: real list"
  have strict_sorted_h: "sorted_wrt (<) ?zer_list" using sorted_sorted_list_of_set
      strict_sorted_iff by auto
  have finset: "finite  {x. ∃q∈set qs. q ≠ 0 ∧ poly q x = 0}"
  proof - 
    have all_q: "∀q ∈ set qs.  q≠ 0 ⟶ finite {x. poly q x = 0} "
      using poly_roots_finite by auto
    then show ?thesis by auto
  qed
  have all_x: "∀x ∈ {x. ∃q∈set qs. q ≠ 0 ∧ poly q x = 0}. poly (prod_list_var qs) x = 0"
    using q_dvd_prod_list_var_prop
    by fastforce 
  then have "poly (prod_list_var qs) (sorted_list_of_set {x. ∃q∈set qs. q ≠ 0 ∧ poly q x = 0} ! 0) = 0"
    using finset set_sorted_list_of_set
    by (metis (no_types, lifting) lengt nth_mem) 
  then have crbgt: "-crb (prod_list_var qs) < ?zer_list ! 0" using prod_list_var_nonzero crb_lem_pos[of "prod_list_var qs" "?zer_list ! (length ?zer_list - 1)"]
    using crb_lem_neg by blast
  have x_in: "x ∈ {x. ∃q∈set qs. q ≠ 0 ∧ poly q x = 0}"
    using pqz q_in qnonz 
    by auto
  then have "x ∈ set ?zer_list"
    by (smt (verit, best) finset in_set_member mem_Collect_eq set_sorted_list_of_set) 
  then have "x ≥ ?zer_list ! 0" using strict_sorted_h
    by (smt (verit) all_x x_in crb_lem_neg linorder_not_le of_int_hom.hom_uminus prod_list_var_nonzero xlt) 
  then show "False" using xlt crbgt 
    by auto
qed

lemma nonzcrb_neg:
  assumes q_in: "q ∈ set qs"
  assumes qnonz: "q ≠ 0"
  shows " ¬(∃x ≤ (real_of_int (-crb (prod_list_var qs))). poly q x = 0)" 
proof - 
  let ?zer_list = "(sorted_list_of_set {(x::real). (∃q ∈ set(qs). (q ≠ 0 ∧ poly q x = 0))} :: real list)"
  have eo: "length ?zer_list = 0 ∨ length ?zer_list > 0"
    by auto 
  have h1: "length ?zer_list = 0 ⟶ ¬(∃x ≤ (real_of_int (-crb (prod_list_var qs))). poly q x = 0)"
    by (metis crb_lem_neg dvdE linorder_not_less mult_zero_left poly_mult prod_list_var_nonzero q_dvd_prod_list_var_prop q_in qnonz)
  have h2: "length ?zer_list > 0 ⟶ ¬(∃x ≤ (real_of_int (-crb (prod_list_var qs))). poly q x = 0)"
    using nonzcrb_helper_neg assms
    by blast 
  show ?thesis using eo h1 h2 
    by auto 
qed

lemma root_lb_restate:
  fixes p:: "real poly"
  assumes pnonz: "p ≠ 0"
  fixes z::"real"
  assumes zgt: "∀x. poly p x=0 ⟶ x > z"
  shows "x≤z ⟹ sgn (poly p x) = Sturm_Tarski.sign (sgn_neg_inf p)"
proof - 
  assume xlt: "x ≤ z"
  have allx: "∀x ≤ z. sgn (poly p x) = sgn (poly p z)"
  proof clarsimp 
    fix x
    assume zleq: "x ≤ z"
    then have xnonz: "sgn (poly p x) ≠ 0"
      using zgt unfolding sgn_def by auto
    have znonz: "sgn (poly p z) ≠ 0"
      using zgt unfolding sgn_def by auto 
    have "Matrix_Equation_Construction.sgn (poly p x) ≠ Matrix_Equation_Construction.sgn (poly p z) ⟹ False"
    proof - 
      assume neq: "Matrix_Equation_Construction.sgn (poly p x) ≠ Matrix_Equation_Construction.sgn (poly p z)"
      then have "x < z" using zleq
        using less_eq_real_def by force
      then have "((poly p x) > 0 ∧ (poly p z) < 0) ∨ ((poly p x) < 0 ∧ (poly p z) > 0) "
        using znonz xnonz zgt neq sgn_def
        by metis
      then have "∃w. w < x ∧ w > z ∧ (poly p w = 0)"
        using poly_IVT_pos[of x z] poly_IVT_neg[of x z]
        by (metis ‹x < z› not_less_iff_gr_or_eq zgt) 
      then show "False"
        using zgt zleq 
        by linarith 
    qed
    then show "Matrix_Equation_Construction.sgn (poly p x) = Matrix_Equation_Construction.sgn (poly p z)"
      by auto
  qed
  have "(∃ub. (∀x≤ub. sgn_class.sgn (poly p x) = sgn_neg_inf p))"
    using root_lb[of p] pnonz 
    by meson 
  then obtain lb where ub_prop: "(∀x≤lb. sgn_class.sgn (poly p x) = sgn_neg_inf p)"
    by auto
  let ?ub2 = "min lb (z-1)"
  have "(∀x≤?ub2. sgn_class.sgn (poly p x) = sgn_neg_inf p) ∧ (?ub2 < z)"
    using ub_prop by auto
  then have h1: "(Sturm_Tarski.sign(sgn_class.sgn (poly p ?ub2)::real)) = Sturm_Tarski.sign(sgn_neg_inf p) ∧ (?ub2 < z)"
    by auto
  have "(Sturm_Tarski.sign(sgn_class.sgn (poly p ?ub2)::real)) = (sgn (poly p ?ub2))"
    unfolding sign_def sgn_def by auto
  then have "(sgn (poly p ?ub2)) = (Sturm_Tarski.sign(sgn_neg_inf p)) ∧ (?ub2 < z)" 
    using h1 by metis
  then show ?thesis using allx xlt
    by (metis min.absorb3 min.cobounded2)
qed

lemma limit_neg_infinity_helper1:
  assumes q_in: "q ∈ set qs"
  assumes qnonz: "q ≠ 0"
  assumes "x = -(crb (prod_list_var qs))"
  shows "(if (poly q x > 0) then 1 else (if (poly q x = 0) then 0 else -1)) 
    = ((Sturm_Tarski.sign (sgn_neg_inf q)))"
proof - 
  have "(∃ub. (∀x. poly q x = 0 ⟶ x < ub ⟶
          (∀x≥ub. sgn_class.sgn (poly q x) = sgn_neg_inf q)))"
    using root_lb[of q] qnonz
    by (meson not_less_iff_gr_or_eq)  
  then obtain ub where ub_prop: "(∀x. poly q x = 0 ⟶ x < ub ⟶
          (∀x≥ub. sgn_class.sgn (poly q x) = sgn_neg_inf q))"
    by auto
  show ?thesis
  proof -
    have "q ∈ set qs ∧ q ≠ 0"
      using ‹q ∈ set qs› ‹q ≠ 0› by blast
    then have f1: "∀r. ¬ r ≤ real_of_int (- crb (prod_list_var qs)) ∨ 0 ≠ poly q r"
      using nonzcrb_neg[of q] by auto
    have f2: "real_of_int x ≤ real_of_int (- crb (prod_list_var qs))"
      using ‹x = - crb (prod_list_var qs)› by fastforce
    obtain rr :: real where
      f3: "q ≠ 0 ∧ (0 = poly q rr ⟶ real_of_int (- crb (prod_list_var qs)) < rr) ∧ real_of_int x ≤ real_of_int (- crb (prod_list_var qs)) ⟶ Sturm_Tarski.sign (sgn_neg_inf q) = Matrix_Equation_Construction.sgn (poly q (real_of_int x))"
      by (metis assms(2) root_lb_restate[of q])
    have "¬ rr ≤ real_of_int (- crb (prod_list_var qs)) ∨ 0 ≠ poly q rr"
      using f1 by blast
    then have "Sturm_Tarski.sign (sgn_neg_inf q) = Matrix_Equation_Construction.sgn (poly q (real_of_int x))"
      using f3 f2 ‹q ≠ 0› by linarith
    then show ?thesis
      by (smt (verit, best) Sturm_Tarski.sign_def of_int_eq_iff of_int_hom.hom_one of_int_hom.hom_zero of_rat_hom.hom_0_iff of_rat_hom.hom_1_iff of_rat_neg_one sgn_def)
  qed
    (*  by (smt (verit, del_insts) linorder_not_less of_rat_hom.eq_iff of_rat_of_int_eq sgn_def)  *)
qed

lemma limit_neg_infinity_helper2:
  assumes q_in: "q ∈ set qs"
  assumes qnonz: "q = 0"
  assumes "x = (-crb (prod_list_var qs))"
  shows "(if (poly q x > 0) then 1 else (if (poly q x = 0) then 0 else -1)) 
    = Sturm_Tarski.sign (sgn_neg_inf q)"
proof - 
  have " 0 = Sturm_Tarski.sign (sgn_neg_inf q)"
    by (simp add: qnonz sgn_neg_inf_def) 
  then show ?thesis using qnonz 
    by auto 
qed

lemma limit_neg_infinity_helper_var:
  assumes q_in: "q ∈ set qs"
  assumes "x = (-crb (prod_list_var qs))"
  shows "(if (poly q x > 0) then 1 else (if (poly q x = 0) then 0 else -1)) 
    = Sturm_Tarski.sign (sgn_neg_inf q)"
  using limit_neg_infinity_helper1 limit_neg_infinity_helper2  assms(2) q_in
  by blast

lemma limit_neg_infinity_helper:
  assumes q_in: "q ∈ set qs"
  assumes "x = (-crb (prod_list_var qs))"
  shows "(if (poly q x > 0) then 1 else (if (poly q x = 0) then 0 else -1)) 
    = (Sturm_Tarski.sign (sgn_neg_inf q))"
  using limit_neg_infinity_helper_var Sturm_Tarski_casting[of "(sgn_neg_inf q)"]
  using assms(2) q_in by presburger 

lemma limit_neg_infinity:
  shows "consistent_sign_vec qs (-(crb (prod_list_var qs))) = sgn_neg_inf_rat_list qs"
  using limit_neg_infinity_helper Sturm_Tarski_casting
    consistent_sign_vec_def sgn_neg_inf_rat_list_def
  apply (auto) apply fastforce apply presburger
  by (metis (mono_tags, opaque_lifting) of_int_eq_1_iff of_int_minus)

lemma csv_signs_at_same:
  shows "consistent_sign_vec qs x = signs_at qs x"
  unfolding consistent_sign_vec_def signs_at_def squash_def by auto

lemma complex_real_int_casting:
  fixes z:: "int"
  shows "(complex_of_real ∘ real_of_int) z = complex_of_int z"
  by auto

lemma poly_f_ncrb_constant_connection:
  assumes is_const: "check_all_const_deg qs = True"
  shows "set (characterize_consistent_signs_at_roots (poly_f qs) qs) 
    = set (characterize_consistent_signs_at_roots (poly_f_nocrb qs) qs) ∪ {sgn_neg_inf_rat_list qs, sgn_pos_inf_rat_list qs}"
proof -  
  have h1: "(poly_f qs)  = [:0, 1:] "
    using assms unfolding poly_f_def by auto 
  have h2: "(poly_f_nocrb qs)  = [:0, 1:] "
    using assms unfolding poly_f_nocrb_def by auto 
  then have same_set1: "set (characterize_consistent_signs_at_roots (poly_f qs) qs) 
    = set (characterize_consistent_signs_at_roots (poly_f_nocrb qs) qs)"
    using h1 h2
    by auto
  have "{x. poly (poly_f qs) x = 0} = {0}"
    using h1 by auto
  then have "(characterize_root_list_p (poly_f qs)) = [0]"
    using h1 unfolding characterize_root_list_p_def  by auto 
  then have "(characterize_consistent_signs_at_roots (poly_f qs) qs)
    = (remdups (map (signs_at qs) [0]))"
    unfolding characterize_consistent_signs_at_roots_def by auto 
  then have "(characterize_consistent_signs_at_roots (poly_f qs) qs) = [signs_at qs 0]"
    by auto
  then have same_set2: "set (characterize_consistent_signs_at_roots (poly_f_nocrb qs) qs) = {signs_at qs 0}"
    using same_set1
    by auto
  have same1: "sgn_neg_inf_rat_list qs = sgn_pos_inf_rat_list qs"
    using is_const unfolding sgn_neg_inf_rat_list_def sgn_pos_inf_rat_list_def 
    unfolding sgn_neg_inf_def sgn_pos_inf_def
    using check_all_const_deg_prop by auto 
  have "⋀q. q ∈ set qs ⟹ poly q 0 = lead_coeff q"
    using is_const check_all_const_deg_prop
    by (metis poly_0_coeff_0) 
  then have same2_h: "map (λx. rat_of_int (Sturm_Tarski.sign (sgn_class.sgn (lead_coeff x)))) qs =  
    map ((λx. if 0 < x then 1 else if x < 0 then - 1 else 0) ∘ (λq. poly q 0)) qs"
    by simp
  then have "map rat_of_int (sgn_pos_inf_rat_list qs) = (signs_at qs 0)"
    using is_const check_all_const_deg_prop 
    unfolding sgn_pos_inf_rat_list_def sgn_pos_inf_def signs_at_def squash_def 
    by auto
  then have " map real_of_rat (map rat_of_int (sgn_pos_inf_rat_list qs)) =
    map of_rat (signs_at qs 0)"
    by auto
  then have "map real_of_int (sgn_pos_inf_rat_list qs) = map of_rat (signs_at qs 0)"
    by auto 
  then have "map complex_of_real (map real_of_int (sgn_pos_inf_rat_list qs)) = map of_rat (signs_at qs 0)"
    by auto
  then have same2: "(sgn_pos_inf_rat_list qs) = (signs_at qs 0)"
    using complex_real_int_casting
    by (metis list.map_comp map_eq_conv)
  show ?thesis
    using same_set1 same_set2 same1 same2  
    by auto
qed

lemma poly_f_ncrb_nonconstant_connection:
  assumes is_not_const: "check_all_const_deg qs = False"
  shows "set (characterize_consistent_signs_at_roots (poly_f qs) qs) 
    = set (characterize_consistent_signs_at_roots (poly_f_nocrb qs) qs) ∪ {sgn_neg_inf_rat_list qs, sgn_pos_inf_rat_list qs}"
proof - 
  let ?s1 = "{x. poly (poly_f qs) x = 0}"
  let ?s2 = "({x. poly (poly_f_nocrb qs) x = 0} ∪ ({-(crb (prod_list_var qs)), (crb (prod_list_var qs))}::real set))" 
  have same_set: "?s1 = ?s2"
    using root_set_nocrb_var[of qs] is_not_const 
    by auto
  then have same_map: "(λx. (signs_at qs x)) ` ?s1 = (λx. (signs_at qs x)) ` ?s2"
    by presburger
  have "set (characterize_consistent_signs_at_roots (poly_f qs) qs) = 
  set (map (signs_at qs) (characterize_root_list_p (poly_f qs)))"
    using characterize_consistent_signs_at_roots_def by auto
  then have "set (characterize_consistent_signs_at_roots (poly_f qs) qs) = 
  (λx. (signs_at qs x)) ` {x. poly (poly_f qs) x = 0}"
    by (simp add: characterize_root_list_p_def poly_f_nonzero poly_roots_finite)
  then have "set (characterize_consistent_signs_at_roots (poly_f qs) qs) = 
  (λx. (signs_at qs x)) ` ({x. poly (poly_f_nocrb qs) x = 0} ∪ ({-(crb (prod_list_var qs)), (crb (prod_list_var qs))}::real set))"
    using  same_map by auto 
  then have bigeq: "set (characterize_consistent_signs_at_roots (poly_f qs) qs) = 
  (λx. (signs_at qs x)) ` {x. poly (poly_f_nocrb qs) x = 0} ∪ (λx. (signs_at qs x)) ` ({-(crb (prod_list_var qs)), (crb (prod_list_var qs))}::real set)"
    by (metis image_Un)
  have crb_seteq: "(λx. (signs_at qs x)) ` ({-(crb (prod_list_var qs)), (crb (prod_list_var qs))}::real set) =
    (λx. (signs_at qs x)) ` ({-(crb (prod_list_var qs))}::real set) ∪
    (λx. (signs_at qs x)) ` ({(crb (prod_list_var qs))}::real set)"
    by blast
  have neg: "(λx. (signs_at qs x)) ` ({-(crb (prod_list_var qs))}::real set) ={sgn_neg_inf_rat_list qs}"
    using limit_neg_infinity[of qs] csv_signs_at_same by auto
  have pos: "(λx. (signs_at qs x)) ` ({(crb (prod_list_var qs))}::real set) ={sgn_pos_inf_rat_list qs}"
    using limit_pos_infinity[of qs] csv_signs_at_same by auto
  have "(λx. (signs_at qs x)) ` ({-(crb (prod_list_var qs)), (crb (prod_list_var qs))}::real set) = {sgn_neg_inf_rat_list qs} ∪ {sgn_pos_inf_rat_list qs}"
    using crb_seteq neg pos by auto 
  then have "(λx. (signs_at qs x)) ` ({-(crb (prod_list_var qs)), (crb (prod_list_var qs))}::real set)
    = {sgn_neg_inf_rat_list qs, sgn_pos_inf_rat_list qs}"
    by auto
  then have biggereq: "set (characterize_consistent_signs_at_roots (poly_f qs) qs) =
    signs_at qs ` {x. poly (poly_f_nocrb qs) x = 0} ∪
    {sgn_neg_inf_rat_list qs, sgn_pos_inf_rat_list qs}"
    using bigeq by auto
  have key: "signs_at qs ` {x. poly (poly_f_nocrb qs) x = 0} = set (characterize_consistent_signs_at_roots (poly_f_nocrb qs) qs)"
    using characterize_consistent_signs_at_roots_def
      Groups.mult_ac(2) characterize_root_list_p_def is_not_const list.set_map mult_cancel_left mult_cancel_left1 poly_f_def poly_f_nocrb_def poly_f_nonzero poly_roots_finite set_remdups sorted_list_of_set(1)
  proof -
    have "poly_f_nocrb qs ≠ 0"
      by (metis mult_cancel_left1 poly_f_def poly_f_nocrb_def poly_f_nonzero)
    then have "set (remdups (map (signs_at qs) (sorted_list_of_set {r. poly (poly_f_nocrb qs) r = 0}))) = signs_at qs ` {r. poly (poly_f_nocrb qs) r = 0}"
      by (simp add: poly_roots_finite)
    then show ?thesis
      using characterize_consistent_signs_at_roots_def characterize_root_list_p_def by presburger
  qed
  then show ?thesis using biggereq
    by (metis image_image list.set_map)
qed

lemma poly_f_ncrb_connection:
  shows "set (characterize_consistent_signs_at_roots (poly_f qs) qs) 
    = set (characterize_consistent_signs_at_roots (poly_f_nocrb qs) qs) ∪ {sgn_neg_inf_rat_list qs, sgn_pos_inf_rat_list qs}"
  using poly_f_ncrb_nonconstant_connection poly_f_ncrb_constant_connection
  by blast

end