Theory IA_Checker

(*
Author:  Sebastiaan Joosten (2016-2017)
Author:  René Thiemann (2016-2017)
Author:  Akihisa Yamada (2016-2017)
License: LGPL (see file COPYING.LESSER)
*)
theory IA_Checker
imports
  Integer_Arithmetic
  Branch_and_Bound
  "HOL-Library.Mapping"
begin

no_notation Simplex.curr_val_satisfies_state ("⊨")
hide_const (open) eval_poly

subsection ‹Validity checking functionality›

datatype 'v linearity = Non_Linear | One | Variable 'v

fun monom_list_linearity :: "'v monom_list ⇒ 'v linearity" where
  "monom_list_linearity [] = One"
| "monom_list_linearity [(x,n)] = (if n = 1 then Variable x else Non_Linear)"
| "monom_list_linearity _ = Non_Linear"

lift_definition monom_linearity :: "'v :: linorder monom ⇒ 'v linearity" is monom_list_linearity .

lemma monom_linearity: "monom_linearity m = One ⟹ eval_monom α m = 1"
  "monom_linearity (m :: 'v :: linorder monom) = Variable x ⟹ eval_monom α m = α x"
  "monom_linearity (m :: 'v :: linorder monom) = Variable x ⟹ monom_vars_list m = [x]"
proof (atomize (full), transfer fixing: x α)
  fix m :: "'v monom_list"
  show "(monom_list_linearity m = linearity.One ⟶ eval_monom_list α m = 1) ∧
         (monom_list_linearity m = Variable x ⟶ eval_monom_list α m = α x) ∧
         (monom_list_linearity m = Variable x ⟶ map fst m = [x])"
    by (cases m, force, cases "tl m", cases "hd m", auto)
qed

context IA_locale begin

subsubsection ‹Via hints›
fun apply_hint :: "int list ⇒ 'v :: linorder poly_constraint list ⇒ 'v ipoly" where
  "apply_hint (Cons n ns) (Cons (Poly_Ge a) as) = poly_add (poly_mult (poly_const (abs n)) a) (apply_hint ns as)" |
  "apply_hint (Cons n ns) (Cons (Poly_Eq a) as) = poly_add (poly_mult (poly_const n) a) (apply_hint ns as)" |
  "apply_hint [] (Cons (Poly_Ge a) as) = poly_add a (apply_hint [] as)" |
  "apply_hint [] (Cons (Poly_Eq a) as) = poly_add a (apply_hint [] as)" |
  "apply_hint _ [] = poly_const 0"

definition poly_is_negative_constant :: "'v :: {linorder,showl} ipoly ⇒ showsl check"
where
"poly_is_negative_constant f
 =  do {
   check (poly_vars_list f = []) (showsl_lit (STR ''polynomial is not a constant''));
   check (eval_poly (λ _. 0) f < 0) (showsl_lit (STR ''polynomial is not a negative constant''))
  } <+? (λ s. showsl_lit (STR ''could not that '') o showsl_poly f o showsl_lit (STR '' is a negative constant⏎'') o s)"

subsubsection ‹Via Branch-and-Bound›

context
  fixes ρ :: "'v :: linorder ⇒ nat" (* renamings between variables *)
    and τ :: "nat ⇒ 'v"
begin
fun ipoly_to_linear_poly :: "'v ipoly ⇒ (linear_poly × int) option" where
  "ipoly_to_linear_poly [] = Some (0,0)"
| "ipoly_to_linear_poly ((monomial,c) # rest) = do {
     (p,d) ← ipoly_to_linear_poly rest;
     case monom_linearity monomial of
       One ⇒ Some (p,c + d)
     | Variable x ⇒ Some (lp_monom (of_int c) (ρ x) + p, d)
     | Non_Linear ⇒ None
  }"

definition True_constraint :: constraint where "True_constraint = GEQ 0 0"

lemma True_constraint[simp]: "a ⊨⇩c True_constraint"
  unfolding True_constraint_def by (auto, transfer, auto)

primrec to_linear_constraints :: "'v poly_constraint ⇒ constraint list" where
  "to_linear_constraints (Poly_Ge p) = (case ipoly_to_linear_poly p of None ⇒ []
       | Some (q,c) ⇒ [GEQ q (of_int (- c))])"
| "to_linear_constraints (Poly_Eq p) = (case ipoly_to_linear_poly p of None ⇒ []
       | Some (q,c) ⇒ [EQ q (of_int (- c))])"

definition to_rat_assignment :: "('v ⇒ int) ⇒ (nat ⇒ rat)" where
  "to_rat_assignment α = rat_of_int o (λ n. α (τ n))"

context
  fixes α :: "'v :: linorder ⇒ int"
    and β :: "nat ⇒ rat"
  assumes beta: "β = to_rat_assignment α"
begin

lemma ipoly_to_linear_poly: "(⋀ v. v ∈ poly_vars p ⟹ τ (ρ v) = v)
  ⟹ ipoly_to_linear_poly p = Some (q, c)
  ⟹ of_int (eval_poly α p) =  (q ⦃β⦄ + of_int c)"
proof (induct p arbitrary: q c)
  case Nil
  then show ?case by (simp add: valuate_zero)
next
  case (Cons xc p qq e)
  obtain xs c where xc: "xc = (xs,c)" by force
  from Cons(3) xc obtain q d where p: "ipoly_to_linear_poly p = Some (q,d)" by (auto split: bind_splits)
  from Cons(1)[OF Cons(2) this] have IH: "of_int (eval_poly α p) = q ⦃ β ⦄ + of_int d" by (auto simp: poly_vars_def)
  show ?case
  proof (cases "monom_linearity xs")
    case One
    with Cons(3) p xc have id: "qq = q" "e = d + c" by auto
    show ?thesis unfolding id xc One using IH monom_linearity(1)[OF One] by auto
  next
    case (Variable x)
    note xs = monom_linearity(2-3)[OF Variable]
    from Cons(3) p xc Variable have id: "qq = lp_monom (rat_of_int c) (ρ x) + q" "e = d" by auto
    from Cons(2)[of x] have "τ (ρ x) = x" unfolding xc poly_vars_def by (auto simp: xs)
    then show ?thesis unfolding id xc using IH xs(1)[of α]
      by (simp add: Cons xc valuate_add valuate_lp_monom beta to_rat_assignment_def[abs_def] o_def ac_simps)
  qed (insert Cons, auto simp: xc split: bind_splits)
qed

lemma to_linear_constraints:
  assumes "interpret_poly_constraint α c"
    and "(⋀ v. v ∈ vars_poly_constraint c ⟹ τ (ρ v) = v)"
    and cc: "cc ∈ set (to_linear_constraints c)"
  shows "β ⊨⇩c cc"
proof (cases c)
  case (Poly_Ge p)
  let ?c = "ipoly_to_linear_poly p"
  show ?thesis
  proof (cases ?c)
    case (Some qc)
    then obtain q d where c: "?c = Some (q,d)" by (cases qc, auto)
    with Poly_Ge cc have id: "cc = GEQ q (of_int (- d))" by auto
    from Poly_Ge assms(2) have "⋀ v. v ∈ poly_vars p ⟹ τ (ρ v) = v" by auto
    from ipoly_to_linear_poly[OF this c]
    have id': "of_int (eval_poly α p) = q ⦃ β ⦄ + of_int d" by auto
    from assms(1)[unfolded Poly_Ge, simplified] have ge: "eval_poly α p ≥ 0" by auto
    show ?thesis unfolding id using ge id' by auto
  qed (insert Poly_Ge cc, auto)
next
  case (Poly_Eq p)
  let ?c = "ipoly_to_linear_poly p"
  show ?thesis
  proof (cases ?c)
    case (Some qc)
    then obtain q d where c: "?c = Some (q,d)" by (cases qc, auto)
    with Poly_Eq cc have id: "cc = EQ q (of_int (- d))" by auto
    from Poly_Eq assms(2) have "⋀ v. v ∈ poly_vars p ⟹ τ (ρ v) = v" by auto
    from ipoly_to_linear_poly[OF this c]
    have id': "of_int (eval_poly α p) = q ⦃ β ⦄ + of_int d" by auto
    from assms(1)[unfolded Poly_Eq, simplified] have eq: "eval_poly α p = 0" by auto
    show ?thesis unfolding id using eq id' by auto
  qed (insert Poly_Eq cc, auto)
qed

lemma to_linear_constraints_unsat:
  assumes "bnb_incr_int (concat (map to_linear_constraints φs)) = None"
    and "⋀ φ. φ ∈ set φs ⟹ interpret_poly_constraint α φ"
    and renaming: "(⋀ v φ. v ∈ vars_poly_constraint φ ⟹ φ ∈ set φs ⟹ τ (ρ v) = v)"
  shows False
proof -
  from to_linear_constraints[OF assms(2) renaming]
  have "⋀ φ c. φ ∈ set φs ⟹ c ∈ set (to_linear_constraints φ) ⟹ β ⊨⇩c c" by auto
  then have "β ⊨⇩c⇩s set (concat (map to_linear_constraints φs))" by simp
  with bnb_incr_int_unsat[OF assms(1)]
  have "β ≠ rat_of_int ∘ v" for v by auto
  thus False unfolding beta to_rat_assignment_def by auto
qed
end
end

definition unsat_via_branch_and_bound :: "'v :: linorder poly_constraint list ⇒ bool" where
  "unsat_via_branch_and_bound les = (let vs = remdups (concat (map vars_poly_constraint_list les));
     ren_map = Mapping.of_alist (zip vs [0 ..< length vs]);
     ren_fun = (λ v. case Mapping.lookup ren_map v of None ⇒ 0 | Some n ⇒ n);
     cs = concat (map (to_linear_constraints ren_fun) les)
    in case bnb_incr_int cs of None ⇒ True | Some β ⇒ False)"

lemma unsat_via_branch_and_bound: assumes unsat: "unsat_via_branch_and_bound les"
  and sat: "⋀ φ. φ ∈ set les ⟹ interpret_poly_constraint α φ"
shows False
proof -
  obtain vs ren_fun invi where
    vs: "vs = remdups (concat (map vars_poly_constraint_list les))" and
    ren_fun: "ren_fun = (λ v. case map_of (zip vs [0 ..< length vs]) v of None ⇒ 0 | Some n ⇒ n)" and
    inv: "invi = (λ i. vs ! i)" by auto
  have dist: "distinct vs" unfolding vs by auto
  {
    fix v φ
    assume "v ∈ vars_poly_constraint φ" "φ ∈ set les"
    then have "v ∈ set vs" unfolding vs by auto
    then obtain i where i: "i < length vs" and v: "v = vs ! i" unfolding set_conv_nth by auto
    then have "ren_fun (vs ! i) = i" unfolding ren_fun using dist by simp
    then have "invi (ren_fun v) = v" unfolding v inv by simp
  } note inv = this
  from unsat[unfolded unsat_via_branch_and_bound_def Let_def lookup_of_alist, folded vs, folded ren_fun]
  have unsat: "bnb_incr_int (concat (map (to_linear_constraints ren_fun) les)) = None"
    by (auto split: option.splits)
  from to_linear_constraints_unsat[OF refl unsat sat inv] show False .
qed

end

datatype hints = Hints "int list" | Branch_and_Bound

instantiation hints :: default begin
  definition "default = Branch_and_Bound"
  instance ..
end

instantiation hints :: showl
begin
fun showsl_hints where
  "showsl_hints (Hints xs) = showsl_lit (STR ''Linear-Combination: '') o showsl_list xs"
| "showsl_hints Branch_and_Bound = showsl_lit (STR ''Simplex'')"
definition "showsl_list (xs :: hints list) = default_showsl_list showsl xs"
instance ..
end

context IA_locale begin

definition unsat_checker :: "hints ⇒ 'v :: {showl,linorder} poly_constraint list ⇒ showsl check" where
  "unsat_checker hints cnjs = (case hints of
    Hints hints ⇒ or_ok
    (poly_is_negative_constant ( (apply_hint (0 # hints) cnjs))) ― ‹ needed? ›
    (poly_is_negative_constant ( (apply_hint (1 # hints) cnjs)))
  | Simplex ⇒ check (unsat_via_branch_and_bound cnjs) (showsl_lit (STR ''could not use simplex algorithm to prove unsatisfiability'')))
  <+? (λ s. showsl_lit (STR ''The linear inequalities⏎  '') ∘ showsl_sep showsl_poly_constraint (showsl_lit (STR ''⏎  '')) cnjs ∘
     showsl_lit (STR ''⏎cannot be proved unsatisfiable via hints⏎  '') ∘ showsl hints ∘ showsl_nl ∘ s)"

(* definitions to avoid the need for existential quantification *)
fun hd2 where "hd2 [] = 1" | "hd2 (Cons a _) = a"


lemma apply_hint_ok:
  assumes "Ball (set lst) (interpret_poly_constraint α)"
  shows "eval_poly α (apply_hint h lst) ≥ 0"
  using assms by (induct h lst rule: apply_hint.induct, auto)

(* Show that there exists an assignment α *)
fun some_alpha::"'a × ty ⇒ val" where
  "some_alpha (v,IntT) = Int 0" |
  "some_alpha (v,BoolT) = Bool True"

lemma some_alpha:"assignment some_alpha"
proof
  fix x t show "some_alpha (x::'a, t) ∈ Values_of_type t" by (cases t; simp)
qed

lemma lin_exp_is_negative_constant_unsat:
  assumes "isOK (poly_is_negative_constant p)"
  shows "¬ eval_poly α p ≥ 0"
proof -
  note ok = assms[unfolded poly_is_negative_constant_def, simplified]
  from ok have vars: "poly_vars_list p = []" and eval: "eval_poly (λ _. 0) p < 0"  by auto
  from arg_cong[OF vars, of set] have "poly_vars p = {}" by auto
  then have "eval_poly α p = eval_poly (λ _. 0) p" using eval_poly_vars[of p] by auto
  with eval show ?thesis by auto
qed

lemma entailment_checker_content_checks_for_False:
  assumes "isOK (poly_is_negative_constant (apply_hint h φs))"
  and "∀ φ ∈ set φs. interpret_poly_constraint α φ"
  shows False
proof -
  from assms have "Ball (set φs) (interpret_poly_constraint α)" by auto
  from apply_hint_ok[OF this, of h] lin_exp_is_negative_constant_unsat[OF assms(1)]
  show False by blast
qed

lemma unsat_checker:
  assumes ok: "isOK(unsat_checker h cnjs)"
  and "⋀ c. c ∈ set cnjs ⟹ interpret_poly_constraint α c"
shows False
proof (cases h)
  case (Hints hh)
  from ok obtain h2 where isok:"isOK (poly_is_negative_constant
              ( (apply_hint h2 cnjs)))"
    using assms(1) or_is_or unfolding unsat_checker_def hints.simps Hints isOK_update_error by blast
  from entailment_checker_content_checks_for_False[OF this, of α] assms(2)
  show False by auto
next
  case Branch_and_Bound
  with ok have "unsat_via_branch_and_bound cnjs" by (auto simp: unsat_checker_def)
  from unsat_via_branch_and_bound[OF this assms(2)] show False by auto
qed

subsection ‹Encoding entailment checking as UNSAT-problems›

fun negate :: "'v IA.exp ⇒ 'v IA.formula"
where "negate (Fun LessF [a,b]) = Atom (Fun LeF [b,a])"
    | "negate (Fun LeF [a,b]) = Atom (Fun LessF [b,a])"
    | "negate (Fun EqF [a,b]) = Disjunction [Atom (Fun LessF [a,b]), Atom (Fun LessF [b,a])]"
    | "negate _ = Conjunction []"

lemma is_boolE:
  assumes e: "is_bool e"
  and "⋀ s e1 e2. e = Fun s [e1,e2] ⟹ s ∈ {LessF, LeF, EqF} ⟹ e1 :⇩f IntT ⟹ e2 :⇩f IntT ⟹ thesis"
  shows "thesis"
proof -
  from e[unfolded is_bool_def] obtain ty where ty: "e :⇩f ty" "ty ∈ {BoolT}" "is_Fun e" by auto
  from ty assms(2) show thesis by (induct e ty rule: has_type_induct, auto)
qed

lemma negate_negates:
  assumes α: "assignment α" and e: "is_bool e"
  shows "α ⊨ negate e ⟷ ¬ α ⊨ Atom e"
  using assms by (elim is_boolE, auto)

lemma negate_preserves_is_bool:
  assumes e: "is_bool e"
  shows "formula (negate e)"
  using assms by (elim is_boolE, auto simp: all_less_two)

lemma mono_negate: "mono_formula True (negate e)"
  by (induct e rule: negate.induct, auto)

fun translate_atom
where "translate_atom (Atom e) = e"

definition "translate_atoms = map translate_atom"

fun translate_conj
where "translate_conj (Conjunction φs) = translate_atoms φs"

definition check_clause :: "hints ⇒ 'v::{showl,linorder} IA.formula ⇒ showsl check"
where "check_clause hints φ ≡
    let es = map IA_exp_to_poly_constraint (translate_conj (¬⇩f φ)) in
    unsat_checker hints es
       <+? (λ s. showsl_lit (STR ''Could not prove unsatisfiability of IA conjunction⏎'')
     ∘ showsl_list_gen showsl_poly_constraint (STR ''False'') (STR '''') (STR '' && '') (STR '''') es ∘ showsl_nl ∘ s)"

lemma translate_atom:
  assumes "translate_atom φ = e" and "formula φ" and "is_Atom φ"
  shows "φ ⟺⇩f Atom e" by (cases φ, insert assms, auto)

lemma translate_conj:
  assumes es: "translate_conj (φ :: 'v IA.formula) = es"
      and φ: "formula φ" "is_conj_atoms φ"
  shows "φ ⟺⇩f conj_atoms es" "e ∈ set es ⟹ is_bool e"
proof-
  from φ(2,1) obtain ls where φ: "φ = Conjunction ls" and l: "⋀ l. l ∈ set ls ⟹ is_Atom l ∧ formula l"
    by (cases, auto)
  with es have es: "es = map translate_atom ls" by (auto simp: translate_atoms_def)
  show "φ ⟺⇩f conj_atoms es"
    using l unfolding φ translate_conj.simps translate_atoms_def es
  proof (induct ls)
    case (Cons l ls)
    from Cons(2)[of l] have "formula l" "is_Atom l" by auto
    from translate_atom[OF refl this] Cons(1)[OF Cons(2)]
    show ?case by auto
  qed auto
  assume "e ∈ set es"
  then show "is_bool e" using l unfolding φ translate_conj.simps translate_atoms_def es
  proof (induct ls)
    case (Cons l ls)
    from Cons(3)[of l] have "formula l" "is_Atom l" by auto
    then have "is_bool (translate_atom l)"
      by (cases l, auto)
    with Cons(1)[OF _ Cons(3)] Cons(2) show ?case by auto
  qed auto
qed

lemma check_clause:
  fixes φ :: "'a::{linorder,showl} IA.formula"
  assumes ok: "isOK (check_clause h φ)" and φ: "formula φ" and clause: "is_neg_atom_clause φ"
  shows "⊨⇩f φ"
proof
  fix α :: "'a × ty ⇒ val"
  assume α: "assignment α"
  show "satisfies α φ"
    proof (rule ccontr)
    assume not: "¬ ?thesis"
    from ok obtain es
    where es: "translate_conj (¬⇩fφ) = es"
      and ok: "isOK (unsat_checker h (map IA_exp_to_poly_constraint es))"
      by (unfold check_clause_def, force)
    have "¬⇩f φ ⟺⇩f conj_atoms es" by (intro translate_conj[OF es], simp add: φ clause,
       rule is_neg_atom_clause.induct[OF clause], auto simp: is_conj_atoms.simps)
    from this α not have sat: "α ⊨ conj_atoms es" by (auto simp:satisfies_Language)
    show False
    proof(rule unsat_checker[OF ok])
      fix v
      assume v: "v ∈ set (map IA_exp_to_poly_constraint es)"
      then obtain w where w: "w ∈ set es" and v: "v = IA_exp_to_poly_constraint w" by force
      from sat w have eval: "α ⊨ Atom w" by auto
      from φ translate_conj(2)[OF es _ _ w] clause
      have "is_bool w" by auto
      from IA_exp_to_poly_constraint[OF α this] eval
      show "interpret_poly_constraint (λa. to_int (α (a, IntT))) v"
        by (auto simp: v)
    qed
  qed
qed

sublocale logic_checker
  where type_fixer = "TYPE(_)"
    and I = I
    and type_of_fun = type_of_fun
    and Values_of_type = Values_of_type
    and Bool_types = "{BoolT}"
    and to_bool = to_bool
    and logic_checker = check_clause
    and showsl_atom = showsl_IA_exp
    and negate_atom = negate
  by (unfold_locales, auto simp: check_clause negate_negates negate_preserves_is_bool mono_negate)

end
end