Theory Virtual_Substitution.EqualityVS

subsection "Overall Equality VS Proofs"
theory EqualityVS
  imports EliminateVariable LuckyFind
begin


lemma degree_find_eq :
  assumes "find_eq var L = (A,L')"
  shows "∀p∈set(A). MPoly_Type.degree p var = 1 ∨ MPoly_Type.degree p var = 2" using assms(1)
proof(induction L arbitrary: A L')
  case Nil
  then show ?case by auto
next
  case (Cons a L)
  then show ?case proof(cases a)
    case (Less p)
    {fix A' L' 
      assume h : "find_eq var L = (A', L')"
      have "A=A'"
        using Less Cons h by(simp)
      then have "∀p∈set A. MPoly_Type.degree p var = 1 ∨ MPoly_Type.degree p var = 2"
        using Cons h by auto
    }
    then show ?thesis by (meson surj_pair)
  next
    case (Eq p)
    then show ?thesis proof(cases "MPoly_Type.degree p var = 1 ∨ MPoly_Type.degree p var = 2")
      case True
      {fix A' L' 
        assume h : "find_eq var L = (A', L')"
        have "A= (p#A')"
          using Eq Cons h True by auto
        then have "∀p∈set A. MPoly_Type.degree p var = 1 ∨ MPoly_Type.degree p var = 2"
          using Cons h True by auto
      }
      then show ?thesis by (meson surj_pair)
    next
      case False
      {fix A' L' 
        assume h : "find_eq var L = (A', L')"
        have "A=A'"
          using Eq Cons h False
          by (smt One_nat_def case_prod_conv find_eq.simps(3) less_2_cases less_SucE numeral_2_eq_2 numeral_3_eq_3 prod.sel(1))
        then have "∀p∈set A. MPoly_Type.degree p var = 1 ∨ MPoly_Type.degree p var = 2"
          using Cons h by auto
      }
      then show ?thesis by (meson surj_pair)
    qed
  next
    case (Leq p)
    {fix A' L' 
      assume h : "find_eq var L = (A', L')"
      have "A=A'"
        using Leq Cons h by(simp)
      then have "∀p∈set A. MPoly_Type.degree p var = 1 ∨ MPoly_Type.degree p var = 2"
        using Cons h by auto
    }
    then show ?thesis by (meson surj_pair)
  next
    case (Neq p)
    {fix A' L' 
      assume h : "find_eq var L = (A', L')"
      have "A=A'"
        using Neq Cons h by(simp)
      then have "∀p∈set A. MPoly_Type.degree p var = 1 ∨ MPoly_Type.degree p var = 2"
        using Cons h by auto
    }
    then show ?thesis by (meson surj_pair)
  qed
qed

lemma list_in_find_eq :
  assumes "find_eq var L = (A,L')"
  shows "set(map Eq A @ L') = set L"using assms(1)
proof(induction L arbitrary: A L')
  case Nil
  then show ?case by auto
next
  case (Cons a L)
  then show ?case proof(cases a)
    case (Less p)
    {fix A' L'' 
      assume h : "find_eq var L = (A', L'')"
      have A : "A=A'"
        using Less Cons h by(simp)
      have L : "L'=Less p # L''"
        using Less Cons h by simp
      have "set (map Eq A @ L') = set (a # L)"
        apply(simp add: A L Less) using Cons(1)[OF h] by auto
    }
    then show ?thesis by (meson surj_pair)
  next
    case (Eq p)
    then show ?thesis proof(cases "MPoly_Type.degree p var = 1 ∨ MPoly_Type.degree p var = 2")
      case True
      {fix A' L'' 
        assume h : "find_eq var L = (A', L'')"
        have A : "A=(p#A')"
          using Eq Cons h True by auto
        have L : "L'= L''"
          using Eq Cons h True by auto 
        have "set (map Eq A @ L') = set (a # L)"
          apply(simp add: A L Eq) using Cons(1)[OF h] by auto
      }
      then show ?thesis by (meson surj_pair)
    next
      case False
      {fix A' L'' 
        assume h : "find_eq var L = (A', L'')"
        have A : "A=A'"
          using Eq Cons h False
          by (smt case_prod_conv degree_find_eq find_eq.simps(3) list.set_intros(1) prod.sel(1))
        have L : "L'=Eq p # L''"
          using Eq Cons h
          by (smt A case_prod_conv find_eq.simps(3) not_Cons_self2 prod.sel(1) prod.sel(2)) 
        have "set (map Eq A @ L') = set (a # L)"
          apply(simp add: A L Eq) using Cons(1)[OF h] by auto
      }
      then show ?thesis by (meson surj_pair)
    qed
  next
    case (Leq p)
    {fix A' L'' 
      assume h : "find_eq var L = (A', L'')"
      have A : "A=A'"
        using Leq Cons h by(simp)
      have L : "L'=Leq p # L''"
        using Leq Cons h by simp
      have "set (map Eq A @ L') = set (a # L)"
        apply(simp add: A L Leq) using Cons(1)[OF h] by auto
    }
    then show ?thesis by (meson surj_pair)
  next
    case (Neq p)
    {fix A' L'' 
      assume h : "find_eq var L = (A', L'')"
      have A : "A=A'"
        using Neq Cons h by(simp)
      have L : "L'=Neq p # L''"
        using Neq Cons h by simp
      have "set (map Eq A @ L') = set (a # L)"
        apply(simp add: A L Neq) using Cons(1)[OF h] by auto
    }
    then show ?thesis by (meson surj_pair)
  qed
qed


lemma qe_eq_one_eval :
  assumes hlength : "length xs = var"
  shows "(∃x. (eval (list_conj ((map Atom L) @ F)) (xs @ (x#Γ)))) = (∃x.(eval (qe_eq_one var L F) (xs @ (x#Γ))))"
proof(cases "find_eq var L")
  case (Pair A L')
  then show ?thesis proof(cases A)
    case Nil
    show ?thesis proof safe
      fix x
      assume h : "eval (list_conj (map fm.Atom L @ F)) (xs @ x # Γ)"
      show "∃x. eval (qe_eq_one var L F) (xs @ x # Γ)" apply(simp) using Nil Pair h by auto 
    next
      fix x
      assume h : "eval (qe_eq_one var L F) (xs @ x # Γ)"
      show "∃x. eval (list_conj (map fm.Atom L @ F)) (xs @ x # Γ)"
        apply(rule exI[where x="x"]) using Nil Pair h by auto
    qed
  next
    case (Cons p A')
    have "set(map Eq (p # A') @ L') = set L"
      using list_in_find_eq[OF Pair] Cons by auto
    then have in_p: "Eq p ∈ set (L)"
      by auto
    have "p∈(set A)" using Cons by auto
    then have low_pow : "MPoly_Type.degree p var = 1 ∨ MPoly_Type.degree p var = 2" 
      using degree_find_eq[OF Pair] by auto
    have "(∃x.(eval (qe_eq_one var L F) (xs @ (x#Γ)))) = 
          (∃x.(eval (Or (And (Neg (split_p var p))
                      ((elimVar var L F) (Eq p))
                    )
                    (And (split_p var p) 
                      (list_conj (map Atom ((map Eq A')  @ L') @ F))
                    )) (xs @ (x#Γ))))"
      apply(rule ex_cong1) apply(simp only: qe_eq_one.simps) using Pair Cons  by auto
    also have "... = (∃x. ((¬eval (split_p var p) (xs @ x # Γ)) ∧ eval (elimVar var L F (Eq p)) (xs @ x # Γ)) ∨
         eval (split_p var p) (xs @ x # Γ) ∧
         (∀f∈set (map fm.Atom (map Eq A' @ L') @ F). eval f (xs @ x # Γ)))"
      by(simp add: eval_list_conj)
    also have "... = (∃x. eval (list_conj (map fm.Atom L @ F)) (xs @ x # Γ))"
    proof(cases "∀x. insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var 2) ≠ 0 ∨
      insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var 1) ≠ 0 ∨
      insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var 0) ≠ 0")
      case True
      have "(∃x. ((¬eval (split_p var p) (xs @ x # Γ)) ∧ eval (elimVar var L F (Eq p)) (xs @ x # Γ)) ∨
         eval (split_p var p) (xs @ x # Γ) ∧
         (∀f∈set (map fm.Atom (map Eq A' @ L') @ F). eval f (xs @ x # Γ))) =
        (∃x. eval (elimVar var L F (Eq p)) (xs @ x # Γ))"
      proof safe
        fix x
        assume "eval (elimVar var L F (Eq p)) (xs @ x # Γ)"
        then show "∃x. eval (elimVar var L F (Eq p)) (xs @ x # Γ)" by auto
      next
        fix x
        assume h : "eval (split_p var p) (xs @ x # Γ)"
        have "¬ eval (split_p var p) (xs @ x # Γ)"
          using True by simp 
        then show "∃x. eval (elimVar var L F (Eq p)) (xs @ x # Γ)" using h by simp
      next
        fix x
        assume "eval (elimVar var L F (Eq p)) (xs @ x # Γ)"
        then show "∃x. ¬ eval (split_p var p) (xs @ x # Γ) ∧ eval (elimVar var L F (Eq p)) (xs @ x # Γ) ∨
             eval (split_p var p) (xs @ x # Γ) ∧
             (∀f∈set (map fm.Atom (map Eq A' @ L') @ F). eval f (xs @ x # Γ))"
          by auto
      qed
      then show ?thesis using elimVar_eq_2[OF hlength in_p low_pow True] by simp
    next
      case False
      have h1: "∀x. eval (split_p var p) (xs @ x # Γ)"
        using False apply(simp) using not_in_isovarspar
        by (metis hlength insertion_lowerPoly1)
      have "set(map Eq (p # A') @ L') = set L"
        using list_in_find_eq[OF Pair] Cons by auto
      then have h5 : "set(map fm.Atom (map Eq (p # A') @ L') @ F) = set(map fm.Atom L @ F)"
        by auto
      have h4 : "(∃x. (aEval (Eq p) (xs @ x # Γ)) ∧
         (∀f∈set (map fm.Atom (map Eq A' @ L') @ F). eval f (xs @ x # Γ))) = 
          (∃x.(∀f∈set (map fm.Atom (map Eq (p#A') @ L') @ F). eval f (xs @ x # Γ)))"
        by(simp)
      have h2 : "(∃x. eval (list_conj (map fm.Atom L @ F)) (xs @ x # Γ)) = (∃x. (aEval (Eq p) (xs @ x # Γ)) ∧
         (∀f∈set (map fm.Atom (map Eq A' @ L') @ F). eval f (xs @ x # Γ)))"
        by(simp only: h4 h5 eval_list_conj) 
      have h3 : "∀x. (aEval (Eq p) (xs @ x # Γ))"
      proof-
        define A where "A = (isolate_variable_sparse p var 2)"
        define B where "B = (isolate_variable_sparse p var 1)"
        define C where "C = (isolate_variable_sparse p var 0)"
        have freeA : "var ∉ vars A"
          unfolding A_def
          by (simp add: not_in_isovarspar)
        have freeB : "var ∉ vars B"
          unfolding B_def
          by (simp add: not_in_isovarspar)
        have freeC : "var ∉ vars C"
          unfolding C_def
          by (simp add: not_in_isovarspar)
        have express_p : "p = A*(Var var)^2+B*(Var var)+C"
          using express_poly[OF low_pow] unfolding A_def B_def C_def
          by fastforce
        have xlength : "∀x. (insertion (nth_default 0 (xs @ x # Γ)) (Var var))= x" 
          using hlength insertion_var
          by (metis add.commute add_strict_increasing length_append length_greater_0_conv list.distinct(1) list_update_id nth_append_length order_refl)
        fix x
        define c where "c i = (insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var i))" for i
        have c2 : "∀x. insertion (nth_default 0 (xs @ x # Γ)) A = c 2" 
          using freeA apply(simp add: A_def c_def)
          by (simp add: hlength insertion_lowerPoly1)
        have c1 : "∀x. insertion (nth_default 0 (xs @ x # Γ)) B = c 1"
          using freeB apply(simp add: B_def c_def)
          by (simp add: hlength insertion_lowerPoly1)
        have c0 : "∀x. insertion (nth_default 0 (xs @ x # Γ)) C = c 0"
          using freeC apply(simp add: C_def c_def)
          by (simp add: hlength insertion_lowerPoly1)
        have sum : "∀x. c 2 * x⇧2 + c (Suc 0) * x + c 0 = (∑i≤2. c i * x ^ i)"
          by (simp add: numerals(2))  
        show ?thesis unfolding express_p apply(simp add:insertion_add insertion_mult insertion_pow xlength)
          apply(simp add:c2 c1 c0 sum polyfun_eq_0[where c="c", where n="2"])
          using False apply(simp)
          by (metis A_def B_def C_def One_nat_def c0 c1 c2 le_SucE le_zero_eq numeral_2_eq_2)
      qed
      show ?thesis apply(simp only: h1 h2) using h3 by(simp)
    qed
    finally show ?thesis by auto
  qed
qed    




lemma qe_eq_repeat_helper_eval_case1 :
  assumes hlength : "length xs = var"
  assumes degreeGood : "∀p∈set(A). MPoly_Type.degree p var = 1 ∨ MPoly_Type.degree p var = 2"
  shows "((eval (list_conj ((map (Atom o Eq)  A) @ (map Atom L) @ F)) (xs @ (x#Γ)))) 
        ⟹ (eval (qe_eq_repeat_helper var A L F) (xs @ x # Γ))"
proof(induction A rule : in_list_induct)
  case Nil
  then show ?case by auto
next
  case (Cons p A')
  assume assm : "((eval (list_conj ((map (Atom o Eq) (p#A')) @ (map Atom L) @ F)) (xs @ (x#Γ)))) "
  then have h :  "insertion (nth_default 0 (xs @ x # Γ)) p = 0 ∧ (eval (qe_eq_repeat_helper var A' L F) (xs @ x # Γ))"
    using Cons by(simp add: eval_list_conj)
  have "¬ eval (split_p var p) (xs @ x # Γ) ∧ eval (elimVar var ((map Eq (p# A')) @ L) F (Eq p)) (xs @ x # Γ) ∨
    eval (split_p var p) (xs @ x # Γ) ∧ eval (qe_eq_repeat_helper var A' L F) (xs @ x # Γ)"
  proof(cases "eval (split_p var p) (xs @ x # Γ)")
    case True
    then show ?thesis using h by blast
  next
    case False
    have all0 :  " ∀x. insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var 2) ≠ 0 ∨
      insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var 1) ≠ 0 ∨
      insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var 0) ≠ 0"
      using False  apply(simp) using not_in_isovarspar
      by (metis hlength insertion_lowerPoly1)
    have in_p : "Eq p∈set((map Eq (p # A') @ L))"
      by auto
    have "p∈(set A)" using Cons by auto
    then have low_pow : "MPoly_Type.degree p var = 1 ∨ MPoly_Type.degree p var = 2" 
      using degreeGood by auto
    have list_manipulate : "map fm.Atom (map Eq (p # A') @ L) = map (fm.Atom ∘ Eq) (p # A') @ map fm.Atom L"
      by(simp)
    have "eval (elimVar var ((map Eq (p# A')) @ L) F (Eq p)) (xs @ x # Γ)"
      using elimVar_eq_2[OF hlength in_p low_pow all0, where F="F"] apply(simp only: list_manipulate) 
      using assm freeIn_elimVar_eq[where var="var", where L="(map Eq (p # A') @ L)", where F="F", where p="p"]
      by (metis append.assoc hlength list_update_length var_not_in_eval)
    then show ?thesis apply(simp only: False) by blast
  qed
  then show ?case by(simp only: qe_eq_repeat_helper.simps eval.simps)
qed

lemma qe_eq_repeat_helper_eval_case2 :
  assumes hlength : "length xs = var"
  assumes degreeGood : "∀p∈set(A). MPoly_Type.degree p var = 1 ∨ MPoly_Type.degree p var = 2"
  shows "(eval (qe_eq_repeat_helper var A L F) (xs @ x # Γ))
        ⟹ ∃x. ((eval (list_conj ((map (Atom o Eq)  A) @ (map Atom L) @ F)) (xs @ (x#Γ))))"
proof(induction A rule : in_list_induct)
  case Nil
  then show ?case apply(simp) apply(rule exI[where x=x]) by simp
next
  case (Cons p A')
  have h : "¬ eval (split_p var p) (xs @ x # Γ) ∧ eval (elimVar var ((map Eq (p# A')) @ L) F (Eq p)) (xs @ x # Γ) ∨
    eval (split_p var p) (xs @ x # Γ) ∧ eval (qe_eq_repeat_helper var A' L F) (xs @ x # Γ)"
    using Cons by(simp only:qe_eq_repeat_helper.simps eval.simps)
  have "p∈set(A)" using Cons(1) .
  then have degp : "MPoly_Type.degree p var = 1 ∨ MPoly_Type.degree p var = 2" 
    using degreeGood by auto
  show ?case proof(cases "eval (split_p var p) (xs @ x # Γ)")
    case True
    have "∃x. eval (list_conj (map (fm.Atom ∘ Eq) A' @ map fm.Atom L @ F)) (xs @ x # Γ)"
      using h True Cons by blast
    then obtain x where x_def : "eval (list_conj (map (fm.Atom ∘ Eq) A' @ map fm.Atom L @ F)) (xs @ x # Γ)" by metis
    define A where "A = (isolate_variable_sparse p var 2)"
    define B where "B = (isolate_variable_sparse p var 1)"
    define C where "C = (isolate_variable_sparse p var 0)"
    have express_p : "p = A * Var var ^2+B * Var var+C"
    proof(cases "MPoly_Type.degree p var = 1")
      case True
      have a0 : "A = 0" apply(simp add: A_def) using True
        by (simp add: isovar_greater_degree) 
      show ?thesis using sum_over_zero[where mp="p", where x="var"] apply(subst (asm) True) by(simp add:a0 B_def C_def add.commute)
    next
      case False
      then have deg : "MPoly_Type.degree p var = 2" using degp by blast
      have flip : "A * (Var var)⇧2 + B * Var var + C = C + B * Var var + A * (Var var)^2" using add.commute by auto
      show ?thesis using sum_over_zero[where mp="p", where x="var"] apply(subst (asm) deg) apply(simp add: flip) apply(simp add: A_def B_def C_def)
        by (simp add: numeral_2_eq_2)
    qed
    have insert_x : "insertion (nth_default 0 (xs @ x # Γ)) (Var var) = x" using hlength
      by (metis add.commute add_strict_increasing insertion_var length_append length_greater_0_conv list.distinct(1) list_update_id nth_append_length order_refl)

    have h : "(aEval (Eq p) (xs @ x # Γ))"
    proof-
      have freeA : "var ∉ vars A"
        unfolding A_def
        by (simp add: not_in_isovarspar)
      have freeB : "var ∉ vars B"
        unfolding B_def
        by (simp add: not_in_isovarspar)
      have freeC : "var ∉ vars C"
        unfolding C_def
        by (simp add: not_in_isovarspar)
      have xlength : "(insertion (nth_default 0 (xs @ x # Γ)) (Var var))= x" 
        using hlength insertion_var
        using insert_x by blast
      define c where "c i = (insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var i))" for i
      have c2 : "∀x. insertion (nth_default 0 (xs @ x # Γ)) A = c 2" 
        using freeA apply(simp add: A_def c_def)
        by (simp add: hlength insertion_lowerPoly1)
      have c1 : "∀x. insertion (nth_default 0 (xs @ x # Γ)) B = c 1"
        using freeB apply(simp add: B_def c_def)
        by (simp add: hlength insertion_lowerPoly1)
      have c0 : "∀x. insertion (nth_default 0 (xs @ x # Γ)) C = c 0"
        using freeC apply(simp add: C_def c_def)
        by (simp add: hlength insertion_lowerPoly1)
      have sum : "c 2 * x⇧2 + c (Suc 0) * x + c 0 = (∑i≤2. c i * x ^ i)"
        by (simp add: numerals(2))  
      show ?thesis apply(subst express_p) apply(simp add:insertion_add insertion_mult insertion_pow xlength)
        apply(simp add:c2 c1 c0 sum polyfun_eq_0[where c="c", where n="2"])
        using True apply(simp) using le_SucE numeral_2_eq_2
        by (metis (no_types) A_def B_def C_def One_nat_def add.left_neutral c0 c1 c2 mult_zero_class.mult_zero_left sum)
    qed
    show ?thesis apply(rule exI[where x=x]) using x_def h apply(simp only:eval_list_conj) by(simp)
  next
    case False
    have all0 :  " ∀x. insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var 2) ≠ 0 ∨
      insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var 1) ≠ 0 ∨
      insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var 0) ≠ 0"
      using False  apply(simp) using not_in_isovarspar
      by (metis hlength insertion_lowerPoly1)
    have h : "eval (elimVar var ((map Eq (p# A')) @ L) F (Eq p)) (xs @ x # Γ)"
      using False h by blast
    have in_list : "Eq p ∈ set (((map Eq (p# A')) @ L))"
      by(simp)
    show ?thesis using elimVar_eq_2[OF hlength in_list, where F="F", OF degp all0] h
      by (metis append_assoc map_append map_map)
  qed
qed



lemma qe_eq_repeat_eval :
  assumes hlength : "length xs = var"
  shows "(∃x. (eval (list_conj ((map Atom L) @ F)) (xs @ (x#Γ)))) = (∃x.(eval (qe_eq_repeat var L F) (xs @ (x#Γ))))"
proof(cases "luckyFind var L F")
  case None
  then show ?thesis proof(cases "find_eq var L")
    case (Pair A L')
    have degGood : "∀p∈set A. MPoly_Type.degree p var = 1 ∨ MPoly_Type.degree p var = 2"
      using degree_find_eq[OF Pair] .
    have "(∃x. eval (qe_eq_repeat var L F) (xs @ x # Γ)) =(∃x. eval
        (qe_eq_repeat_helper var A L' F)
        (xs @ x # Γ))"
      using Pair None by auto
    also have "...
      = (∃x. ((eval (list_conj ((map (Atom o Eq)  A) @ (map Atom L') @ F)) (xs @ (x#Γ)))))"
      using qe_eq_repeat_helper_eval_case1[OF hlength degGood, where L="L'", where F="F", where Γ="Γ"]
        qe_eq_repeat_helper_eval_case2[OF hlength degGood, where L="L'", where F="F", where Γ="Γ"]
      by blast
    also have "... = (∃x. (eval (list_conj ((map Atom L) @ F)) (xs @ (x#Γ))))"
    proof-
      have list_manipulate : "map (fm.Atom ∘ Eq) A @ map fm.Atom L' = map fm.Atom (map Eq A @ L')"
        by simp
      have changeA :  "map (fm.Atom ∘ Eq) A = map Atom (map Eq A)" by auto
      have split : "(∃x. ∀f∈set ((map (fm.Atom ∘ Eq) A) @
                (map fm.Atom L') @ F).
          eval f (xs @ x # Γ)) = (∃x. ∀f∈ (Atom ` set ((map (Eq) A) @ L')) ∪ set(F).
          eval f (xs @ x # Γ))"
        apply (rule ex_cong1)
        apply(subst changeA)
        by auto
      show ?thesis apply(simp only: eval_list_conj split list_in_find_eq[OF Pair]) by auto
    qed
    finally have ?thesis by simp
    then show ?thesis by auto
  qed
next
  case (Some a)
  then show ?thesis using luckyFind_eval[OF Some assms(1)] by auto
qed


end