证明在 Isabelle 中划分列表的算法的正确性
Proving the correctness of an algorithm to partition lists in Isabelle
我试图证明在线性时间内将整数列表拆分为总和相等的子列表的算法是正确的。 你可以看到我选择的算法。
我想得到一些关于以下内容的反馈：
我定义分裂函数的方便
在我的情况下使用的 "induction" 假设。
请记住，到目前为止我只使用过应用脚本而不是 Isar 证明。
这里是算法的初步实现和正确性定义：
definition
"ex_balanced_sum xs = (∃ ys zs. sum_list ys = sum_list zs ∧
xs = ys @ zs ∧ ys ≠ [] ∧ zs ≠ [])"
fun check_list :: "int list ⇒ int ⇒ int ⇒ bool" where
"check_list [] n acc = False" |
"check_list (x#xs) n acc = (if n = acc then True else (check_list xs (n-x) (acc+x)))"
fun linear_split :: "int list ⇒ bool" where
"linear_split [] = False" |
"linear_split [x] = False" |
"linear_split (x # xs) = check_list xs (sum_list xs) x"
需证明的定理如下：
lemma linear_correct: "linear_split xs ⟷ ex_balanced_sum xs"
例如，如果我将第一个含义推理为：
lemma linear_correct_1: "linear_split xs ⟹ ex_balanced_sum xs"
apply(induction xs rule: linear_split.induct)
然后我得到一个我认为不合适的子目标列表：
- linear_split[]⟹ex_balanced_sum[]
- ⋀x。 linear_split [x] ⟹ ex_balanced_sum [x]
- ⋀x v va。 linear_split (x # v # va) ⟹ ex_balanced_sum (x # v # va)
特别是，这些子目标没有归纳假设！ （我对吗？）。我试图通过只写 apply(induction xs) 来执行不同的归纳，但目标看起来是：
- linear_split[]⟹ex_balanced_sum[]
- ⋀一个xs。 (linear_split xs ⟹ ex_balanced_sum xs) ⟹ linear_split (a # xs) ⟹ ex_balanced_sum (a # xs)
这里的假设也不是归纳假设，因为它假设了蕴涵。
那么，定义此函数以获得良好归纳假设的最佳方法是什么？
编辑（单功能版）
fun check :: "int list ⇒ int ⇒ int ⇒ bool" where
"check [] n acc = False" |
"check [x] n acc = False" |
"check (x # y # xs) n acc = (if n-x = acc+x then True else check (y # xs) (n-x) (acc+x))"
definition "linear_split xs = check xs (sum_list xs) 0"
背景
我能够证明函数 (splitl) 的定理 linear_correct 与问题陈述中的函数 check 非常相似。不幸的是，我不想尝试将证明转换为应用脚本。
下面的证明是我开始研究这个问题后想到的第一个证明。因此，可能存在更好的证明。
证明大纲
证明是基于列表长度的归纳。特别是，假设
splitl xs (sum_list xs) 0 ⟹ ex_balanced_sum xs
适用于所有长度小于 l 的列表。如果l = 1，那么结果很容易显示。假设 l>=2。那么这个列表可以用x#v#xs的形式来表示。在这种情况下，如果可以使用 splitl 拆分列表，则可以显示 (splitl_reduce)
"splitl ((x + v)#xs) (sum_list ((x + v)#xs)) 0" (1)
或
"x = sum_list (v#xs)" (2)。
这样，(1)和(2)的证明就分情况进行了。对于（1），列表的长度是(x + v)#xs)是l-1。因此，根据归纳假设ex_balanced_sum (x + v)#xs)。因此，根据ex_balanced_sum的定义，也就是ex_balanced_sum x#v#xs。对于（2），很容易看出列表可以表示为[x]@(v#xs)，在这种情况下，给定（2），它根据定义满足ex_balanced_sum的条件。
另一个方向的证明是类似的，并且基于上面与 (1) 和 (2) 相关的引理的逆：如果 "splitl ((x + v)#xs) (sum_list ((x + v)#xs)) 0" 或 "x = sum_list (v#xs)"，则 "splitl (x#v#xs) (sum_list (x#v#xs)) 0".
theory so_ptcoaatplii
imports Complex_Main
begin
definition
"ex_balanced_sum xs =
(∃ ys zs. sum_list ys = sum_list zs ∧ xs = ys @ zs ∧ ys ≠ [] ∧ zs ≠ [])"
fun splitl :: "int list ⇒ int ⇒ int ⇒ bool" where
"splitl [] s1 s2 = False" |
"splitl [x] s1 s2 = False" |
"splitl (x # xs) s1 s2 = ((s1 - x = s2 + x) ∨ splitl xs (s1 - x) (s2 + x))"
lemma splitl_reduce:
assumes "splitl (x#v#xs) (sum_list (x#v#xs)) 0"
shows "splitl ((x + v)#xs) (sum_list ((x + v)#xs)) 0 ∨ x = sum_list (v#xs)"
proof -
from assms have prem_cases:
"((x = sum_list (v#xs)) ∨ splitl (v#xs) (sum_list (v#xs)) x)" by auto
{
assume "splitl (v#xs) (sum_list (v#xs)) x"
then have "splitl ((x + v)#xs) (sum_list ((x + v)#xs)) 0"
proof(induction xs arbitrary: x v)
case Nil then show ?case by simp
next
case (Cons a xs) then show ?case by simp
qed
}
with prem_cases show ?thesis by auto
qed
(*Sledgehammered*)
lemma splitl_expand:
assumes "splitl ((x + v)#xs) (sum_list ((x + v)#xs)) 0 ∨ x = sum_list (v#xs)"
shows "splitl (x#v#xs) (sum_list (x#v#xs)) 0"
by (smt assms list.inject splitl.elims(2) splitl.simps(3) sum_list.Cons)
lemma splitl_to_sum: "splitl xs (sum_list xs) 0 ⟹ ex_balanced_sum xs"
proof(induction xs rule: length_induct)
case (1 xs) show ?case
proof-
obtain x v xst where x_xst: "xs = x#v#xst"
by (meson "1.prems" splitl.elims(2))
have main_cases:
"splitl ((x + v)#xst) (sum_list ((x + v)#xst)) 0 ∨ x = sum_list (v#xst)"
by (rule splitl_reduce, insert x_xst "1.prems", rule subst)
{
assume "splitl ((x + v)#xst) (sum_list ((x + v)#xst)) 0"
with "1.IH" x_xst have "ex_balanced_sum ((x + v)#xst)" by simp
then obtain yst zst where
yst_zst: "(x + v)#xst = yst@zst"
and sum_yst_eq_sum_zst: "sum_list yst = sum_list zst"
and yst_ne: "yst ≠ []"
and zst_ne: "zst ≠ []"
unfolding ex_balanced_sum_def by auto
then obtain ystt where ystt: "yst = (x + v)#ystt"
by (metis append_eq_Cons_conv)
with sum_yst_eq_sum_zst have "sum_list (x#v#ystt) = sum_list zst" by simp
moreover have "xs = (x#v#ystt)@zst" using x_xst yst_zst ystt by auto
moreover have "(x#v#ystt) ≠ []" by simp
moreover with zst_ne have "zst ≠ []" by simp
ultimately have "ex_balanced_sum xs" unfolding ex_balanced_sum_def by blast
}
note prem = this
{
assume "x = sum_list (v#xst)"
then have "sum_list [x] = sum_list (v#xst)" by auto
moreover with x_xst have "xs = [x] @ (v#xst)" by auto
ultimately have "ex_balanced_sum xs" using ex_balanced_sum_def by blast
}
with prem main_cases show ?thesis by blast
qed
qed
lemma sum_to_splitl: "ex_balanced_sum xs ⟹ splitl xs (sum_list xs) 0"
proof(induction xs rule: length_induct)
case (1 xs) show ?case
proof -
from "1.prems" ex_balanced_sum_def obtain ys zs where
ys_zs: "xs = ys@zs"
and sum_ys_eq_sum_zs: "sum_list ys = sum_list zs"
and ys_ne: "ys ≠ []"
and zs_ne: "zs ≠ []"
by blast
have prem_cases: "∃y v yst. ys = (y#v#yst) ∨ (∃y. ys = [y])"
by (metis remdups_adj.cases ys_ne)
{
assume "∃y. ys = [y]"
then have "splitl xs (sum_list xs) 0"
using splitl.elims(3) sum_ys_eq_sum_zs ys_zs zs_ne by fastforce
}
note prem = this
{
assume "∃y v yst. ys = (y#v#yst)"
then obtain y v yst where y_v_yst: "ys = (y#v#yst)" by auto
then have
"sum_list ((y + v)#yst) = sum_list zs ∧ ((y + v)#yst) ≠ [] ∧ zs ≠ []"
using sum_ys_eq_sum_zs zs_ne by auto
then have ebs_ypv: "ex_balanced_sum (((y + v)#yst)@zs)"
using ex_balanced_sum_def by blast
have l_ypv: "length (((y + v)#yst)@zs) < length xs"
by (simp add: y_v_yst ys_zs)
from l_ypv ebs_ypv have
"splitl (((y + v)#yst)@zs) (sum_list (((y + v)#yst)@zs)) 0"
by (rule "1.IH"[THEN spec, rule_format])
with splitl_expand have splitl_ys_exp:
"splitl ((y#v#yst)@zs) (sum_list ((y#v#yst)@zs)) 0"
by (metis Cons_eq_appendI)
from ys_zs have "splitl xs (sum_list xs) 0"
by (rule ssubst, insert y_v_yst splitl_ys_exp, simp)
}
with prem prem_cases show ?thesis by auto
qed
qed
lemma linear_correct: "ex_balanced_sum xs ⟷ splitl xs (sum_list xs) 0"
using splitl_to_sum sum_to_splitl by auto
end
我试图证明在线性时间内将整数列表拆分为总和相等的子列表的算法是正确的。
我想得到一些关于以下内容的反馈：
我定义分裂函数的方便
在我的情况下使用的 "induction" 假设。
请记住，到目前为止我只使用过应用脚本而不是 Isar 证明。
这里是算法的初步实现和正确性定义：
definition
"ex_balanced_sum xs = (∃ ys zs. sum_list ys = sum_list zs ∧
xs = ys @ zs ∧ ys ≠ [] ∧ zs ≠ [])"
fun check_list :: "int list ⇒ int ⇒ int ⇒ bool" where
"check_list [] n acc = False" |
"check_list (x#xs) n acc = (if n = acc then True else (check_list xs (n-x) (acc+x)))"
fun linear_split :: "int list ⇒ bool" where
"linear_split [] = False" |
"linear_split [x] = False" |
"linear_split (x # xs) = check_list xs (sum_list xs) x"
需证明的定理如下：
lemma linear_correct: "linear_split xs ⟷ ex_balanced_sum xs"
例如，如果我将第一个含义推理为：
lemma linear_correct_1: "linear_split xs ⟹ ex_balanced_sum xs"
apply(induction xs rule: linear_split.induct)
然后我得到一个我认为不合适的子目标列表：
- linear_split[]⟹ex_balanced_sum[]
- ⋀x。 linear_split [x] ⟹ ex_balanced_sum [x]
- ⋀x v va。 linear_split (x # v # va) ⟹ ex_balanced_sum (x # v # va)
特别是，这些子目标没有归纳假设！ （我对吗？）。我试图通过只写 apply(induction xs) 来执行不同的归纳，但目标看起来是：
- linear_split[]⟹ex_balanced_sum[]
- ⋀一个xs。 (linear_split xs ⟹ ex_balanced_sum xs) ⟹ linear_split (a # xs) ⟹ ex_balanced_sum (a # xs)
这里的假设也不是归纳假设，因为它假设了蕴涵。
那么，定义此函数以获得良好归纳假设的最佳方法是什么？
编辑（单功能版）
fun check :: "int list ⇒ int ⇒ int ⇒ bool" where
"check [] n acc = False" |
"check [x] n acc = False" |
"check (x # y # xs) n acc = (if n-x = acc+x then True else check (y # xs) (n-x) (acc+x))"
definition "linear_split xs = check xs (sum_list xs) 0"
背景
我能够证明函数 (splitl) 的定理 linear_correct 与问题陈述中的函数 check 非常相似。不幸的是，我不想尝试将证明转换为应用脚本。
下面的证明是我开始研究这个问题后想到的第一个证明。因此，可能存在更好的证明。
证明大纲
证明是基于列表长度的归纳。特别是，假设
splitl xs (sum_list xs) 0 ⟹ ex_balanced_sum xs
适用于所有长度小于 l 的列表。如果l = 1，那么结果很容易显示。假设 l>=2。那么这个列表可以用x#v#xs的形式来表示。在这种情况下，如果可以使用 splitl 拆分列表，则可以显示 (splitl_reduce)
"splitl ((x + v)#xs) (sum_list ((x + v)#xs)) 0" (1)
或
"x = sum_list (v#xs)" (2)。
这样，(1)和(2)的证明就分情况进行了。对于（1），列表的长度是(x + v)#xs)是l-1。因此，根据归纳假设ex_balanced_sum (x + v)#xs)。因此，根据ex_balanced_sum的定义，也就是ex_balanced_sum x#v#xs。对于（2），很容易看出列表可以表示为[x]@(v#xs)，在这种情况下，给定（2），它根据定义满足ex_balanced_sum的条件。
另一个方向的证明是类似的，并且基于上面与 (1) 和 (2) 相关的引理的逆：如果 "splitl ((x + v)#xs) (sum_list ((x + v)#xs)) 0" 或 "x = sum_list (v#xs)"，则 "splitl (x#v#xs) (sum_list (x#v#xs)) 0".
theory so_ptcoaatplii
imports Complex_Main
begin
definition
"ex_balanced_sum xs =
(∃ ys zs. sum_list ys = sum_list zs ∧ xs = ys @ zs ∧ ys ≠ [] ∧ zs ≠ [])"
fun splitl :: "int list ⇒ int ⇒ int ⇒ bool" where
"splitl [] s1 s2 = False" |
"splitl [x] s1 s2 = False" |
"splitl (x # xs) s1 s2 = ((s1 - x = s2 + x) ∨ splitl xs (s1 - x) (s2 + x))"
lemma splitl_reduce:
assumes "splitl (x#v#xs) (sum_list (x#v#xs)) 0"
shows "splitl ((x + v)#xs) (sum_list ((x + v)#xs)) 0 ∨ x = sum_list (v#xs)"
proof -
from assms have prem_cases:
"((x = sum_list (v#xs)) ∨ splitl (v#xs) (sum_list (v#xs)) x)" by auto
{
assume "splitl (v#xs) (sum_list (v#xs)) x"
then have "splitl ((x + v)#xs) (sum_list ((x + v)#xs)) 0"
proof(induction xs arbitrary: x v)
case Nil then show ?case by simp
next
case (Cons a xs) then show ?case by simp
qed
}
with prem_cases show ?thesis by auto
qed
(*Sledgehammered*)
lemma splitl_expand:
assumes "splitl ((x + v)#xs) (sum_list ((x + v)#xs)) 0 ∨ x = sum_list (v#xs)"
shows "splitl (x#v#xs) (sum_list (x#v#xs)) 0"
by (smt assms list.inject splitl.elims(2) splitl.simps(3) sum_list.Cons)
lemma splitl_to_sum: "splitl xs (sum_list xs) 0 ⟹ ex_balanced_sum xs"
proof(induction xs rule: length_induct)
case (1 xs) show ?case
proof-
obtain x v xst where x_xst: "xs = x#v#xst"
by (meson "1.prems" splitl.elims(2))
have main_cases:
"splitl ((x + v)#xst) (sum_list ((x + v)#xst)) 0 ∨ x = sum_list (v#xst)"
by (rule splitl_reduce, insert x_xst "1.prems", rule subst)
{
assume "splitl ((x + v)#xst) (sum_list ((x + v)#xst)) 0"
with "1.IH" x_xst have "ex_balanced_sum ((x + v)#xst)" by simp
then obtain yst zst where
yst_zst: "(x + v)#xst = yst@zst"
and sum_yst_eq_sum_zst: "sum_list yst = sum_list zst"
and yst_ne: "yst ≠ []"
and zst_ne: "zst ≠ []"
unfolding ex_balanced_sum_def by auto
then obtain ystt where ystt: "yst = (x + v)#ystt"
by (metis append_eq_Cons_conv)
with sum_yst_eq_sum_zst have "sum_list (x#v#ystt) = sum_list zst" by simp
moreover have "xs = (x#v#ystt)@zst" using x_xst yst_zst ystt by auto
moreover have "(x#v#ystt) ≠ []" by simp
moreover with zst_ne have "zst ≠ []" by simp
ultimately have "ex_balanced_sum xs" unfolding ex_balanced_sum_def by blast
}
note prem = this
{
assume "x = sum_list (v#xst)"
then have "sum_list [x] = sum_list (v#xst)" by auto
moreover with x_xst have "xs = [x] @ (v#xst)" by auto
ultimately have "ex_balanced_sum xs" using ex_balanced_sum_def by blast
}
with prem main_cases show ?thesis by blast
qed
qed
lemma sum_to_splitl: "ex_balanced_sum xs ⟹ splitl xs (sum_list xs) 0"
proof(induction xs rule: length_induct)
case (1 xs) show ?case
proof -
from "1.prems" ex_balanced_sum_def obtain ys zs where
ys_zs: "xs = ys@zs"
and sum_ys_eq_sum_zs: "sum_list ys = sum_list zs"
and ys_ne: "ys ≠ []"
and zs_ne: "zs ≠ []"
by blast
have prem_cases: "∃y v yst. ys = (y#v#yst) ∨ (∃y. ys = [y])"
by (metis remdups_adj.cases ys_ne)
{
assume "∃y. ys = [y]"
then have "splitl xs (sum_list xs) 0"
using splitl.elims(3) sum_ys_eq_sum_zs ys_zs zs_ne by fastforce
}
note prem = this
{
assume "∃y v yst. ys = (y#v#yst)"
then obtain y v yst where y_v_yst: "ys = (y#v#yst)" by auto
then have
"sum_list ((y + v)#yst) = sum_list zs ∧ ((y + v)#yst) ≠ [] ∧ zs ≠ []"
using sum_ys_eq_sum_zs zs_ne by auto
then have ebs_ypv: "ex_balanced_sum (((y + v)#yst)@zs)"
using ex_balanced_sum_def by blast
have l_ypv: "length (((y + v)#yst)@zs) < length xs"
by (simp add: y_v_yst ys_zs)
from l_ypv ebs_ypv have
"splitl (((y + v)#yst)@zs) (sum_list (((y + v)#yst)@zs)) 0"
by (rule "1.IH"[THEN spec, rule_format])
with splitl_expand have splitl_ys_exp:
"splitl ((y#v#yst)@zs) (sum_list ((y#v#yst)@zs)) 0"
by (metis Cons_eq_appendI)
from ys_zs have "splitl xs (sum_list xs) 0"
by (rule ssubst, insert y_v_yst splitl_ys_exp, simp)
}
with prem prem_cases show ?thesis by auto
qed
qed
lemma linear_correct: "ex_balanced_sum xs ⟷ splitl xs (sum_list xs) 0"
using splitl_to_sum sum_to_splitl by auto
end