Theory Linear_Diophantine_Eq_Finder
subsection ‹Algorithm to Detect Implicit Equalities in ‹ℤ››
text ‹Use the rational equality finder to identify integer equalities.
Basically, this is just a conversion between the different types of constraints.›
theory Linear_Diophantine_Eq_Finder
imports
Linear_Polynomial_Impl
Equality_Detection_Impl
Diophantine_Tightening
begin
definition linear_poly_of_lpoly :: "(int,var)lpoly ⇒ linear_poly" where
[code del]: "linear_poly_of_lpoly p = (let cxs = map (λ v. (v, coeff_l p v)) (vars_l_list p)
in sum_list (map (λ (x,c). lp_monom (of_int c) x) cxs))"
lemma linear_poly_of_lpoly_impl[code]:
"linear_poly_of_lpoly (lpoly_of p) = (let cxs = vars_coeffs_impl p
in sum_list (map (λ (x,c). lp_monom (of_int c) x) cxs))"
unfolding linear_poly_of_lpoly_def vars_coeffs_impl(5) ..
lemma valuate_sum_list: "valuate (sum_list ps) α = sum_list (map (λ p. valuate p α) ps)"
by (induct ps, auto simp: valuate_zero valuate_add)
lemma linear_poly_of_lpoly: "rat_of_int (eval_l α p) = of_int (constant_l p) + valuate (linear_poly_of_lpoly p) (λ x. of_int (α x))"
unfolding eval_l_def of_int_add
unfolding linear_poly_of_lpoly_def Let_def map_map o_def split valuate_sum_list valuate_lp_monom
unfolding of_int_mult[symmetric] of_int_sum
unfolding vars_l_list_def
by (subst sum_list_distinct_conv_sum_set, auto)
definition dleq_to_constraint :: "var dleq ⇒ constraint" where
"dleq_to_constraint p = EQ (linear_poly_of_lpoly p) (of_int (- constant_l p))"
lemma dleq_to_constraint: "satisfies_dleq α e ⟷ satisfies_constraint (λ x. rat_of_int (α x)) (dleq_to_constraint e)"
proof -
have "satisfies_dleq α e ⟷ rat_of_int (eval_l α e) = 0"
unfolding satisfies_dleq_def by blast
also have "… ⟷ satisfies_constraint (λ x. rat_of_int (α x)) (dleq_to_constraint e)"
unfolding linear_poly_of_lpoly[of α e] dleq_to_constraint_def
by auto
finally show ?thesis .
qed
definition dlineq_to_constraint :: "var dlineq ⇒ constraint" where
"dlineq_to_constraint p = LEQ (linear_poly_of_lpoly p) (of_int (- constant_l p))"
lemma dlineq_to_constraint: "satisfies_dlineq α e ⟷
satisfies_constraint (λ x. rat_of_int (α x)) (dlineq_to_constraint e)"
proof -
have "satisfies_dlineq α e ⟷ rat_of_int (eval_l α e) ≤ 0"
unfolding satisfies_dlineq_def by simp
also have "… ⟷ satisfies_constraint (λ x. rat_of_int (α x)) (dlineq_to_constraint e)"
unfolding linear_poly_of_lpoly[of α e] dlineq_to_constraint_def
by auto
finally show ?thesis .
qed
definition eq_finder_int :: "var dlineq list ⇒
(var dleq list × var dlineq list) option" where
[code del]: "eq_finder_int ineqs = (case
eq_finder_rat (map dlineq_to_constraint ineqs) of
None ⇒ None
| Some (idx_eq, _) ⇒ let I = set idx_eq;
ics = zip [0..< length ineqs] ineqs
in case List.partition (λ (i,c). i ∈ I) ics
of (eqs2, ineqs2) ⇒ Some (map snd eqs2, map snd ineqs2))"
lemma classify_dlineq_to_constraint[simp]:
"¬ is_strict (dlineq_to_constraint c)"
"¬ is_equality (dlineq_to_constraint c)"
"is_nstrict (dlineq_to_constraint c)"
by (auto simp: dlineq_to_constraint_def)
lemma init_constraints_ineqs:
"init_constraints (map dlineq_to_constraint ineqs) =
(let idx = [0..<length ineqs];
ics' = zip idx
(map dlineq_to_constraint ineqs);
ics = concat (map index_constraint ics')
in (ics, idx, [], []))"
unfolding init_constraints_def length_map Let_def
apply (clarsimp simp flip: set_empty, intro conjI)
subgoal apply (subst filter_True)
subgoal by (auto dest!: set_zip_rightD)
subgoal by auto
done
by (auto dest!: set_zip_rightD)
lemmas eq_finder_int_code[code] =
eq_finder_int_def[unfolded eq_finder_rat_def init_eq_finder_rat_def, unfolded init_constraints_ineqs]
lemma eq_finder_int: assumes
res: "eq_finder_int ineqs = res"
shows "res = None ⟹ ∄ α. α ⊨⇩d⇩i⇩o ({}, set ineqs)"
"res = Some (eqs, ineqs') ⟹ α ⊨⇩d⇩i⇩o ({}, set ineqs) ⟷ α ⊨⇩d⇩i⇩o (set eqs, set ineqs')"
"res = Some (eqs, ineqs') ⟹ ∃ α. α ⊨⇩c⇩s (make_strict ` dlineq_to_constraint ` set ineqs')"
"res = Some (eqs, ineqs') ⟹ length ineqs = length eqs + length ineqs'"
proof (atomize(full), goal_cases)
case 1
define cs where "cs = map dlineq_to_constraint ineqs"
let ?sat = "λ α eqs ineqs. Ball (set eqs) (satisfies_dleq α) ∧ Ball (set ineqs) (satisfies_dlineq α)"
note defs = dlineq_to_constraint dleq_to_constraint
note defs2 = satisfies_dlineq_def satisfies_dleq_def
note defs3 = dlineq_to_constraint_def dleq_to_constraint_def
note res = res[unfolded eq_finder_int_def, folded cs_def]
show ?case
proof (cases "eq_finder_rat cs")
case None
with res have res: "res = None" by auto
from eq_finder_rat(1)[OF None, unfolded cs_def]
have "∄ α. ?sat α [] ineqs" unfolding defs by auto
with res show ?thesis by auto
next
case (Some pair)
then obtain eq_idx sol where eq: "eq_finder_rat cs = Some (eq_idx, sol)" by (cases pair, auto)
define ics where "ics = zip [0 ..< length ineqs] ineqs"
let ?I = "set eq_idx"
let ?part = "List.partition (λ(i, c). i ∈ ?I) ics"
obtain ineqs2 eqs2 where part: "?part = (eqs2, ineqs2)" by force
let ?ineqs2 = "map snd ineqs2"
let ?eqs2 = "map snd eqs2"
have ics: "ics = map (λ i. (i, ineqs ! i)) [0 ..< length ineqs]"
unfolding ics_def by (intro nth_equalityI, auto)
from part have eqs2: "?eqs2 = map ((!) ineqs) (filter (λ i. i ∈ ?I) [0 ..< length ineqs])"
unfolding ics by (auto simp: filter_map o_def)
from part have ineqs2: "?ineqs2 = map ((!) ineqs) (filter (λ i. i ∉ ?I) [0 ..< length ineqs])"
unfolding ics by (auto simp: filter_map o_def)
note res = res[unfolded eq option.simps split Let_def, folded ics_def,
unfolded part split]
from eq_finder_rat(2)[OF eq]
have eq_finder2: "{i. i < length cs ∧ is_equality (cs ! i)} ⊆ ?I"
"?I ⊆ {0..<length cs}"
"distinct eq_idx" by auto
have len: "length ineqs = length cs" unfolding cs_def by auto
from eq_finder2 have filter: "{x ∈ set [0..<length ineqs]. x ∈ ?I} = ?I"
unfolding len by force
from eq_finder2 have filter': "set (filter (λi. i ∉ ?I) [0..<length ineqs]) = {0 ..< length cs} - ?I"
unfolding len by force
have eqs2': "set (map dleq_to_constraint ?eqs2) = make_equality ` (!) cs ` ?I"
unfolding set_map eqs2 set_filter image_comp filter o_def using eq_finder2
by (intro image_cong[OF refl])
(auto simp: cs_def nth_append defs3)
have ineqs2': "set (map dlineq_to_constraint ?ineqs2) = (!) cs ` ({0..<length cs} - ?I)"
unfolding set_map ineqs2 filter' image_comp o_def
apply (intro image_cong[OF refl])
subgoal for i using set_mp[OF eq_finder2(1), of i]
unfolding defs2 by (auto simp: cs_def nth_append defs3)
done
from eq_finder_rat(3)[OF eq eqs2' ineqs2'] have
equiv: "⋀ v. v ⊨⇩c⇩s set cs = v ⊨⇩c⇩s (dleq_to_constraint ` set ?eqs2 ∪ dlineq_to_constraint ` set ?ineqs2)"
and strict: "sol ⊨⇩c⇩s (set (map dleq_to_constraint ?eqs2) ∪ make_strict ` set (map dlineq_to_constraint ?ineqs2))"
unfolding set_map by metis+
from strict have strict: "sol ⊨⇩c⇩s (make_strict ` dlineq_to_constraint ` set ?ineqs2)" by auto
{
let ?α = "λ x :: var. rat_of_int (α x)"
have "?sat α [] ineqs ⟷ ?α ⊨⇩c⇩s set cs" unfolding cs_def
by (auto simp: defs)
also have "… ⟷ ?sat α ?eqs2 ?ineqs2" unfolding equiv
using defs[of α] by fastforce
finally have "?sat α [] ineqs ⟷ ?sat α ?eqs2 ?ineqs2" .
} note eq = this
have "length ineqs = length ics" unfolding ics_def by auto
also have "… = length eqs2 + length ineqs2" using part[simplified]
by (smt (verit) comp_def filter_cong sum_length_filter_compl)
finally show ?thesis using eq res strict by fastforce
qed
qed
end