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
  TA.Simplex
  "HOL-Library.Mapping" 
begin

no_notation Simplex.curr_val_satisfies_state ("⊨")

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,show} ipoly ⇒ shows check"
where
"poly_is_negative_constant f
 =  do { 
   check (poly_vars_list f = []) (shows ''polynomial is not a constant'');
   check (eval_poly (λ _. 0) f < 0) (shows ''polynomial is not a negative constant'')
  } <+? (λ s. shows ''could not that '' o shows_poly f o shows '' is a negative constant'' o shows_nl o s)"

subsubsection ‹Via Simplex›

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 ((mon,c) # rest) = do {
     (p,d) ← ipoly_to_linear_poly rest;
     case monom_linearity mon 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_simplex_constraint :: "'v poly_constraint ⇒ constraint list" where
  "to_simplex_constraint (Poly_Ge p) = (case ipoly_to_linear_poly p of None ⇒ []
       | Some (q,c) ⇒ [GEQ q (of_int (- c))])" 
| "to_simplex_constraint (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 α n = of_int (α (τ 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
  thus ?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)
    thus ?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] ac_simps)
  qed (insert Cons, auto simp: xc split: bind_splits)
qed

lemma to_simplex_constraint:
  assumes "interpret_poly_constraint α c"
    and "(⋀ v. v ∈ vars_poly_constraint c ⟹ τ (ρ v) = v)" 
    and cc: "cc ∈ set (to_simplex_constraint 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_simplex_constraint_unsat: 
  assumes "simplex (concat (map to_simplex_constraint φs)) = None" 
    and "⋀ φ. φ ∈ set φs ⟹ interpret_poly_constraint α φ" 
    and renaming: "(⋀ v φ. v ∈ vars_poly_constraint φ ⟹ φ ∈ set φs ⟹ τ (ρ v) = v)" 
  shows False
proof -
  from to_simplex_constraint[OF assms(2) renaming] 
  have "⋀ φ c. φ ∈ set φs ⟹ c ∈ set (to_simplex_constraint φ) ⟹ β ⊨⇩c c" by auto
  hence "β ⊨⇩c⇩s concat (map to_simplex_constraint φs)" by simp
  with simplex(2)[OF assms(1)] show False by auto
qed
end
end

definition unsat_via_simplex :: "'v :: {linorder,show} poly_constraint list ⇒ bool" where
  "unsat_via_simplex 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_simplex_constraint ren_fun) les)
    in simplex cs = None)" 

lemma unsat_via_simplex: assumes unsat: "unsat_via_simplex les" 
  and sat: "⋀ φ. φ ∈ set les ⟹ interpret_poly_constraint α φ"
shows False
proof -
  obtain vs ren_fun inv 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: "inv = (λ i. vs ! i)" by auto  
  have dist: "distinct vs" unfolding vs by auto
  {
    fix v φ
    assume "v ∈ vars_poly_constraint φ" "φ ∈ set les" 
    hence "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
    hence "ren_fun (vs ! i) = i" unfolding ren_fun using dist by simp
    hence "inv (ren_fun v) = v" unfolding v inv by simp
  } note inv = this        
  from unsat[unfolded unsat_via_simplex_def Let_def lookup_of_alist, folded vs, folded ren_fun]
  have unsat: "simplex (concat (map (to_simplex_constraint ren_fun) les)) = None" by auto
  from to_simplex_constraint_unsat[OF refl unsat sat inv] show False .
qed

end

datatype hints = Hints "int list" | Simplex

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

derive "show" hints

context IA_locale begin

definition unsat_checker :: "hints ⇒ 'v :: {show,linorder} poly_constraint list ⇒ shows check" where
  "unsat_checker hints cnjs = (case hints of 
    Hints coeffs ⇒ or_ok 
    (poly_is_negative_constant ( (apply_hint (0 # coeffs) cnjs))) (* needed? *)
    (poly_is_negative_constant ( (apply_hint (1 # coeffs) cnjs))) 
  | Simplex ⇒ check (unsat_via_simplex cnjs) (shows ''could not use simplex algorithm to prove unsatisfiability''))
  <+? (λ s. shows ''The linear inequalities⏎  '' ∘ shows_sep shows_poly_constraint (shows ''⏎  '') cnjs ∘
     shows ''⏎cannot be proved unsatisfiable via hints⏎  '' ∘ shows hints ∘ shows_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
  hence "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 Simplex
  with ok have "unsat_via_simplex cnjs" by (auto simp: unsat_checker_def)
  from unsat_via_simplex[OF this assms(2)] show False by auto
qed

subsection ‹Encoding entailment checking as UNSAT-problems›

fun negate :: "'v::show 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::{show,linorder}) IA_formula ⇒ shows check"
where "check_clause hints φ ≡
    let es = map IA_exp_to_poly_constraint (translate_conj (¬⇩f φ)) in 
    unsat_checker hints es
       <+? (λ s. shows ''Could not prove unsatisfiability of IA conjunction '' o shows_nl 
     ∘ shows_list_gen shows_poly_constraint ''False'' [] '' && '' [] es ∘ shows_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 :: show 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"
  thus "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
    hence "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 φ :: "(sig,'a::{linorder,show},ty) exp 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 shows_atom = show_IA_exp
    and negate_atom = negate
  by (unfold_locales, auto simp: check_clause negate_negates negate_preserves_is_bool mono_negate)

end
end