Theory Equality_Detection_Theory

section ‹Detection of Implicit Equalities›

subsection ‹Main Abstract Reasoning Step›

text ‹The abstract reasoning steps is due to Bromberger and Weidenbach.
  Make all inequalities strict and detect a minimal unsat core; all inequalities
  in this core are implied equalities.›

theory Equality_Detection_Theory
  imports 
    Farkas.Farkas
    Jordan_Normal_Form.Matrix
begin

lemma lec_rel_sum_list: "lec_rel (sum_list cs) = 
  (if (∃ c ∈ set cs. lec_rel c = Lt_Rel) then Lt_Rel else Leq_Rel)" 
proof (induct cs)
  case Nil
  thus ?case by (auto simp: zero_le_constraint_def)
next
  case (Cons c cs)
  thus ?case by (cases "sum_list cs"; cases c; cases "lec_rel c"; auto)
qed


lemma equality_detection_rat: fixes cs :: "rat le_constraint set"
    and p ::  "'i ⇒ linear_poly" 
    and co ::  "'i ⇒ rat" 
    and I :: "'i set" 
  defines "n ≡ λ i. Le_Constraint Leq_Rel (p i) (co i)" (* non-strict *)
    and "s ≡ λ i. Le_Constraint Lt_Rel (p i) (co i)"    (* strict *)
  assumes fin: "finite cs" "finite I" 
    and C: "C ⊆ cs ∪ s ` I" 
    and unsat: "∄ v. ∀ c ∈ C. v ⊨⇩l⇩e c" 
    and min: "⋀ D. D ⊂ C ⟹ ∃ v. ∀ c ∈ D. v ⊨⇩l⇩e c" 
    and sol: "∀ c ∈ cs ∪ n ` I. v ⊨⇩l⇩e c" 
    and i: "i ∈ I" "s i ∈ C" 
  shows "(p i)⦃v⦄ = co i" 
proof -
  have "finite ((cs ∪ s ` I) ∩ C)" using fin by auto
  with C have finC: "finite C" by (simp add: inf_absorb2)
  from Motzkin's_transposition_theorem[OF this] unsat
  obtain D const rel where valid: "∀(r, c)∈set D. 0 < r ∧ c ∈ C" and
        eq: "(∑(r, c)←D. Le_Constraint (lec_rel c) (r *R lec_poly c) (r *R lec_const c)) =
              Le_Constraint rel 0 const"
        and ineq: "rel = Leq_Rel ∧ const < 0 ∨ rel = Lt_Rel ∧ const ≤ 0" by auto
  let ?expr = "(∑(r, c)←D. Le_Constraint (lec_rel c) (r *R lec_poly c) (r *R lec_const c))" 
  {
    assume "s i ∉ snd ` set D"
    with valid have valid: "∀(r, c)∈set D. 0 < r ∧ c ∈ C - {s i}"
      by force
    from finC have "finite (C - {s i})" by auto
    from Motzkin's_transposition_theorem[OF this] valid eq ineq
    have "∄ v. ∀c∈C - {s i}. v ⊨⇩l⇩e c" by blast
    with min[of "C - {s i}"] i(2) have False by auto
  }
  hence mem: "s i ∈ snd ` set D" by auto
  from i(1) sol have "v ⊨⇩l⇩e  n i" by auto
  from this[unfolded n_def] have piv: "(p i) ⦃ v ⦄ ≤ co i" by simp
  from ineq have const0: "const ≤ 0" by auto
  define I' where "I' = cs ∪ n ` I"
  define f where "f c = (if c ∈ insert (s i) I' then c else (n (SOME j. j ∈ I ∧ s j = c)))" for c
  let ?C = "insert (s i) I'" 
  {
    fix c
    assume "c ∈ C" 
    hence c: "c ∈ cs ∪ s ` I" using C by auto
    hence "f c ∈ ?C ∧ lec_poly (f c) = lec_poly c ∧ lec_const (f c) = lec_const c"
    proof (cases "c ∈ cs ∪ n ` I ∪ {s i}")
      case True
      thus ?thesis unfolding f_def I'_def by auto
    next
      case False
      define j where "j = (SOME x. x ∈ I ∧ s x = c)" 
      from False have "∃ j. j ∈ I ∧ s j = c" using c by auto
      from someI_ex[OF this, folded j_def] have j: "j ∈ I" and c: "c = s j" by auto
      from False have fc: "f c = n j" unfolding f_def j_def[symmetric] I'_def by auto
      show ?thesis using j c fc by (auto simp: n_def s_def I'_def)
    qed
    hence "f c ∈ insert (s i) I'" "lec_poly (f c) = lec_poly c" "lec_const (f c) = lec_const c" 
      by auto
  } note f = this
  
  show ?thesis
  proof (rule ccontr)
    assume "¬ ?thesis" 
    with piv have "(p i)⦃ v ⦄ < co i" by simp
    hence vsi: "v ⊨⇩l⇩e s i" unfolding s_def by auto  
    with sol have sol: "(∃ v. ∀c ∈ insert (s i) I'. v ⊨⇩l⇩e c) = True" unfolding I'_def by auto
    let ?D = "map (map_prod id f) D" 
    have fin: "finite (insert (s i) I')" unfolding I'_def using fin by auto
    from valid f(1)
    have valid': "∀(r, c)∈set ?D. 0 < r ∧ c ∈ ?C" by force
    let ?expr' = "∑(r, c)←?D. Le_Constraint (lec_rel c) (r *R lec_poly c) (r *R lec_const c)" 
    have "lec_const ?expr' = lec_const ?expr" 
      unfolding sum_list_lec
      apply simp
      apply (rule arg_cong[of _ _ sum_list])
      apply (rule map_cong[OF refl])
      using f valid by auto
    also have "… = const" unfolding eq by simp
    finally have const: "lec_const ?expr' = const" by auto
    have "lec_poly ?expr' = lec_poly ?expr" 
      unfolding sum_list_lec
      apply simp
      apply (rule arg_cong[of _ _ sum_list])
      apply (rule map_cong[OF refl])
      using f valid by auto
    also have "… = 0" unfolding eq by simp
    finally have poly: "lec_poly ?expr' = 0" by auto
    from mem obtain c where "(c, s i) ∈ set D" by auto
    hence "(c, f (s i)) ∈ set ?D" by force
    hence mem: "(c, s i) ∈ set ?D" unfolding f_def by auto
    moreover have "lec_rel (s i) = Lt_Rel" unfolding s_def by auto
    ultimately 
    have rel: "lec_rel ?expr' = Lt_Rel" 
      unfolding lec_rel_sum_list using split_list[OF mem] by fastforce
    have eq': "?expr' = Le_Constraint Lt_Rel 0 const" 
      using const poly rel by (simp add: sum_list_lec) 

    from valid' eq' Motzkin's_transposition_theorem[OF fin, unfolded sol] const0
    show False by blast
  qed
qed 

end