Theory Simplex_for_Reals

(* Author: R. Thiemann *)

section ‹Unsatisfiability over the Reals›

text ‹By using Farkas' Lemma we prove that a finite set of 
  linear rational inequalities is satisfiable over the rational numbers
  if and only if it is satisfiable over the real numbers.
  Hence, the simplex algorithm either gives a rational solution or
  shows unsatisfiability over the real numbers.›

theory Simplex_for_Reals
  imports 
    Farkas
    Simplex.Simplex_Incremental
begin


instantiation real :: lrv
begin
definition scaleRat_real :: "rat ⇒ real ⇒ real" where
  [simp]: "x *R y = real_of_rat x * y"
instance by standard (auto simp add: field_simps of_rat_mult of_rat_add)
end

abbreviation real_satisfies_constraints :: "real valuation ⇒ constraint set ⇒ bool" (infixl "⊨⇩r⇩c⇩s" 100) where
  "v ⊨⇩r⇩c⇩s cs ≡ ∀ c ∈ cs. v ⊨⇩c c"

definition of_rat_val :: "rat valuation ⇒ real valuation" where
  "of_rat_val v x = of_rat (v x)" 

lemma of_rat_val_eval: "p ⦃of_rat_val v⦄ = of_rat (p ⦃v⦄)" 
  unfolding of_rat_val_def linear_poly_sum of_rat_sum 
  by (rule sum.cong, auto simp: of_rat_mult)

lemma of_rat_val_constraint: "of_rat_val v ⊨⇩c c ⟷ v ⊨⇩c c" 
  by (cases c, auto simp: of_rat_val_eval of_rat_less of_rat_less_eq)

lemma of_rat_val_constraints: "of_rat_val v ⊨⇩r⇩c⇩s cs ⟷ v ⊨⇩c⇩s cs" 
  using of_rat_val_constraint by auto

lemma sat_scale_rat_real: assumes "(v :: real valuation) ⊨⇩c c"
  shows "v ⊨⇩c (r *R c)"
proof -
  have "r < 0 ∨ r = 0 ∨ r > 0" by auto
  then show ?thesis using assms by (cases c, simp_all add: right_diff_distrib 
        valuate_minus valuate_scaleRat scaleRat_leq1 scaleRat_leq2 valuate_zero
        of_rat_less of_rat_mult)
qed

fun of_rat_lec :: "rat le_constraint ⇒ real le_constraint" where
  "of_rat_lec (Le_Constraint r p c) = Le_Constraint r p (of_rat c)" 

lemma lec_of_constraint_real: 
  assumes "is_le c"
  shows "(v ⊨⇩l⇩e of_rat_lec (lec_of_constraint c)) ⟷ (v ⊨⇩c c)"
  using assms by (cases c, auto)

lemma of_rat_lec_add: "of_rat_lec (c + d) = of_rat_lec c + of_rat_lec d" 
  by (cases c; cases d, auto simp: of_rat_add)

lemma of_rat_lec_zero: "of_rat_lec 0 = 0" 
  unfolding zero_le_constraint_def by simp

lemma of_rat_lec_sum: "of_rat_lec (sum_list c) = sum_list (map of_rat_lec c)" 
  by (induct c, auto simp: of_rat_lec_zero of_rat_lec_add)

text ‹This is the main lemma: a finite set of linear constraints is 
  satisfiable over Q if and only if it is satisfiable over R.›
lemma rat_real_conversion: assumes "finite cs" 
  shows "(∃ v :: rat valuation. v ⊨⇩c⇩s cs) ⟷ (∃ v :: real valuation. v ⊨⇩r⇩c⇩s cs)" 
proof
  show "∃v. v ⊨⇩c⇩s cs ⟹ ∃v. v ⊨⇩r⇩c⇩s cs" using of_rat_val_constraint by auto
  assume "∃v. v ⊨⇩r⇩c⇩s cs" 
  then obtain v where *: "v ⊨⇩r⇩c⇩s cs" by auto
  show "∃v. v ⊨⇩c⇩s cs" 
  proof (rule ccontr)
    assume "∄v. v ⊨⇩c⇩s cs" 
    from farkas_coefficients[OF assms] this
    obtain C where "farkas_coefficients cs C" by auto
    from this[unfolded farkas_coefficients_def]
    obtain d rel where
      isleq: "(∀(r,c) ∈ set C. c ∈ cs ∧ is_le (r *R c) ∧ r ≠ 0)" and
      leq: "(∑ (r,c) ← C. lec_of_constraint (r *R c)) = Le_Constraint rel 0 d" and
      choice: "rel = Lt_Rel ∧ d ≤ 0 ∨ rel = Leq_Rel ∧ d < 0" by blast
    {
      fix r c
      assume c: "(r,c) ∈ set C" 
      from c * isleq have "v ⊨⇩c c" by auto
      hence v: "v ⊨⇩c (r *R c)" by (rule sat_scale_rat_real)
      from c isleq have "is_le (r *R c)" by auto
      from lec_of_constraint_real[OF this] v 
      have "v ⊨⇩l⇩e of_rat_lec (lec_of_constraint (r *R c))" by blast
    } note v = this
    have "Le_Constraint rel 0 (of_rat d) = of_rat_lec (∑ (r,c) ← C. lec_of_constraint (r *R c))" 
      unfolding leq by simp
    also have "… = (∑ (r,c) ← C. of_rat_lec (lec_of_constraint (r *R c)))" (is "_ = ?sum")
      unfolding of_rat_lec_sum map_map o_def by (rule arg_cong[of _ _ sum_list], auto)
    finally have leq: "Le_Constraint rel 0 (of_rat d) = ?sum" by simp
    have "v ⊨⇩l⇩e Le_Constraint rel 0 (of_rat d)" unfolding leq
      by (rule satisfies_sumlist_le_constraints, insert v, auto)
    with choice show False by (auto simp: linear_poly_sum)
  qed
qed

text ‹The main result of simplex, now using unsatisfiability over the reals.›

fun i_satisfies_cs_real (infixl "⊨⇩r⇩i⇩c⇩s" 100) where
  "(I,v) ⊨⇩r⇩i⇩c⇩s cs ⟷ v ⊨⇩r⇩c⇩s Simplex.restrict_to I cs"

lemma simplex_index_real:
  "simplex_index cs = Unsat I ⟹ set I ⊆ fst ` set cs ∧ ¬ (∃ v. (set I, v) ⊨⇩r⇩i⇩c⇩s set cs) ∧ 
     (distinct_indices cs ⟶ (∀ J ⊂ set I. (∃ v. (J, v) ⊨⇩i⇩c⇩s set cs)))" ― ‹minimal unsat core over the reals›
  "simplex_index cs = Sat v ⟹ ⟨v⟩ ⊨⇩c⇩s (snd ` set cs)" ― ‹satisfying assingment›
  using simplex_index(1)[of cs I] simplex_index(2)[of cs v] 
    rat_real_conversion[of "Simplex.restrict_to (set I) (set cs)"]
  by auto


lemma simplex_real:
  "simplex cs = Unsat I ⟹ ¬ (∃ v. v ⊨⇩r⇩c⇩s set cs)" ― ‹unsat of original constraints over the reals›
  "simplex cs = Unsat I ⟹ set I ⊆ {0..<length cs} ∧ ¬ (∃ v. v ⊨⇩r⇩c⇩s {cs ! i | i. i ∈ set I})
    ∧ (∀J⊂set I. ∃v. v ⊨⇩c⇩s {cs ! i |i. i ∈ J})" ― ‹minimal unsat core over reals›
  "simplex cs = Sat v ⟹ ⟨v⟩ ⊨⇩c⇩s set cs"  ― ‹satisfying assignment over the rationals›
proof (intro simplex(1)[unfolded rat_real_conversion[OF finite_set]])
  assume unsat: "simplex cs = Inl I" 
  have "finite {cs ! i |i. i ∈ set I}" by auto
  from simplex(2)[OF unsat, unfolded rat_real_conversion[OF this]]
  show "set I ⊆ {0..<length cs} ∧ ¬ (∃ v. v ⊨⇩r⇩c⇩s {cs ! i | i. i ∈ set I})
    ∧ (∀J⊂set I. ∃v. v ⊨⇩c⇩s {cs ! i |i. i ∈ J})" by auto
qed (insert simplex(3), auto)

text ‹Define notion of minimal unsat core over the reals:
  the subset has to be unsat over the reals, and every proper subset has
  to be satisfiable over the rational numbers.›

definition minimal_unsat_core_real :: "'i set ⇒ 'i i_constraint list ⇒ bool" where
  "minimal_unsat_core_real I ics  = ((I ⊆ fst ` set ics) ∧ (¬ (∃ v. (I,v) ⊨⇩r⇩i⇩c⇩s set ics))
     ∧ (distinct_indices ics ⟶ (∀ J. J ⊂ I ⟶ (∃ v. (J,v) ⊨⇩i⇩c⇩s set ics))))"

text ‹Because of equi-satisfiability the two notions of minimal unsat cores coincide.›
lemma minimal_unsat_core_real_conv: "minimal_unsat_core_real I ics = minimal_unsat_core I ics" 
proof 
  show "minimal_unsat_core_real I ics ⟹ minimal_unsat_core I ics" 
    unfolding minimal_unsat_core_real_def minimal_unsat_core_def
    using of_rat_val_constraint by simp metis
next
  assume "minimal_unsat_core I ics"     
  thus "minimal_unsat_core_real I ics" 
    unfolding minimal_unsat_core_real_def minimal_unsat_core_def
    using rat_real_conversion[of "Simplex.restrict_to I (set ics)"]
    by auto
qed

text ‹Easy consequence: The incremental simplex algorithm is also sound wrt. 
  minimal-unsat-cores over the reals.›
lemmas incremental_simplex_real = 
  init_simplex
  assert_simplex_ok
  assert_simplex_unsat[folded minimal_unsat_core_real_conv]
  assert_all_simplex_ok
  assert_all_simplex_unsat[folded minimal_unsat_core_real_conv]
  check_simplex_ok
  check_simplex_unsat[folded minimal_unsat_core_real_conv]
  solution_simplex
  backtrack_simplex
  checked_invariant_simplex

end