是否可以向 Isabelle 中的函数域添加假设?
Is it possible to add assumptions to the domain of a function in Isabelle?
我不确定 post 这样的后续问题是否可以,但无论如何我都会这样做。
所以几天前我post编辑了这个问题:
我认为答案很好,但在试图证明引理时
lemma "applied1 {#''a'',''a'',''d'',''c'',''a'',''a'',''d'',''c''#} {#''a'',''a'',''c''#} ''f'' = {#''f'',''f'',''d'',''d''#}"
我真的卡住了。我发现在展开 def 并应用一些简单的自动化后我不能简单地做到这一点。所以我回到我原来的函数并对它做了一些调整,这样如果输入导致无限循环,它 returns 什么都没有。我以为这次会成功,但伊莎贝尔仍然无法证明终止。我敢肯定,很明显 size x
不断减少 size y
并且不能为负数,因此它最终必须在 size x = 0
或 y 不再是时终止x 的子集。
fun applied2 :: "'a multiset ⇒ 'a multiset ⇒ 'a ⇒ 'a multiset option" where
"applied2 x y z = (if z ∈# y ∨ y = {#} then None else (if y ⊆# x then Some (plus {#z#} (the (applied2 (x - y) y z))) else Some x))"
是否可以说服 Isabelle 使用 function
而不是 fun
来终止此函数?还是我必须考虑其他限制条件?
如果我不应该 post 提出这样的问题,我真的很抱歉。我对 Isabelle 仍然缺乏经验,我希望我能坚持自己的目标,尽我所能地学习这门语言。提前致谢!
我相信查看 documentation 会给您正确的语法。
function applied2 :: "'a multiset ⇒ 'a multiset ⇒ 'a ⇒ 'a multiset option" where
"applied2 x y z = (if z ∈# y ∨ y = {#} then None else (if y ⊆# x then Some (plus {#z#} (the (applied2 (x - y) y z))) else Some x))"
by pat_completeness auto
termination
by (relation "measure (λ(x,y,z). size x)")
(auto simp: mset_subset_eq_exists_conv nonempty_has_size)
如果问题是证明,sledgehammer 会为您找到它。
但是,我看不出您打算如何从 applied2 转到您真正想要的功能。真正的问题是确定性:你需要一个命令来查看子集。 Manuel 的解决方案是使用 Sup,但这确实不可执行。
如果非递归定义的唯一问题是如何将其应用于具体输入,我仍然认为我所说的可执行的替代定义是可行的方法。下面证明我给的两个非递归定义是等价的,以及对你上面给的例子的应用:
definition applied :: "'a multiset ⇒ 'a multiset ⇒ 'a ⇒ 'a multiset" where
"applied ms xs y = (if xs = {#} then ms else
(let n = Max {n. repeat_mset n xs ⊆# ms}
in ms - repeat_mset n xs + replicate_mset n y))"
lemma count_le_size: "count M x ≤ size M"
by (induction M) auto
lemma applied_code [code]:
"applied ms xs y = (if xs = {#} then ms else
(let n = (MIN x ∈set_mset xs. count ms x div count xs x)
in ms - repeat_mset n xs + replicate_mset n y))"
unfolding applied_def
proof (intro if_cong let_cong refl)
assume ne: "xs ≠ {#}"
have subset: "{n. repeat_mset n xs ⊆# ms} ⊆ {..size ms}"
proof safe
fix n assume n: "repeat_mset n xs ⊆# ms"
from ne obtain x where x: "x ∈# xs"
by auto
have "n * 1 ≤ n * count xs x"
using x by (intro mult_left_mono) auto
also have "… = count (repeat_mset n xs) x"
by simp
also have "… ≤ count ms x"
using n by (intro mset_subset_eq_count)
also have "… ≤ size ms"
by (rule count_le_size)
finally show "n ≤ size ms" by simp
qed
hence finite: "finite {n. repeat_mset n xs ⊆# ms}"
by (rule finite_subset) auto
show "Max {n. repeat_mset n xs ⊆# ms} = (MIN x∈set_mset xs. count ms x div count xs x)"
proof (intro antisym)
show "Max {n. repeat_mset n xs ⊆# ms} ≤ (MIN x∈set_mset xs. count ms x div count xs x)"
proof (rule Max.boundedI)
show "{n. repeat_mset n xs ⊆# ms} ≠ {}"
by (auto intro: exI[of _ 0])
next
fix n assume n: "n ∈ {n. repeat_mset n xs ⊆# ms}"
show "n ≤ (MIN x∈set_mset xs. count ms x div count xs x)"
proof (safe intro!: Min.boundedI)
fix x assume x: "x ∈# xs"
have "count (repeat_mset n xs) x ≤ count ms x"
using n by (intro mset_subset_eq_count) auto
also have "count (repeat_mset n xs) x = n * count xs x"
by simp
finally show "n ≤ count ms x div count xs x"
by (metis count_eq_zero_iff div_le_mono nonzero_mult_div_cancel_right x)
qed (use ne in auto)
qed (fact finite)
next
define m where "m = (MIN x∈set_mset xs. count ms x div count xs x)"
show "m ≤ Max {n. repeat_mset n xs ⊆# ms}"
proof (rule Max.coboundedI[OF finite], safe)
show "repeat_mset m xs ⊆# ms"
proof (rule mset_subset_eqI)
fix x
show "count (repeat_mset m xs) x ≤ count ms x"
proof (cases "x ∈# xs")
case True
have "count (repeat_mset m xs) x = m * count xs x"
by simp
also have "… ≤ (count ms x div count xs x) * count xs x"
unfolding m_def using ‹x ∈# xs› by (intro mult_right_mono Min.coboundedI) auto
also have "… ≤ count ms x"
by simp
finally show ?thesis .
next
case False
hence "count xs x = 0"
by (meson not_in_iff)
thus ?thesis by simp
qed
qed
qed
qed
qed
lemma replicate_mset_unfold:
assumes "n > 0"
shows "replicate_mset n x = {#x#} + replicate_mset (n - 1) x"
using assms by (cases n) auto
lemma
assumes "a ≠ c" "a ≠ f" "c ≠ f"
shows "applied {#a,a,c,a,a,c#} {#a,a,c#} f = mset [f, f]"
using assms
by (simp add: applied_code replicate_mset_unfold flip: One_nat_def)
value
命令对该示例不起作用,因为 a
、c
等是自由变量。但是如果你例如为他们制作一个特别的数据类型,它有效:
datatype test = a | b | c | f
value "applied {#a,a,c,a,a,c#} {#a,a,c#} f"
(* "mset [f, f]" :: "test multiset" *)
我不确定 post 这样的后续问题是否可以,但无论如何我都会这样做。
所以几天前我post编辑了这个问题:
我认为答案很好,但在试图证明引理时
lemma "applied1 {#''a'',''a'',''d'',''c'',''a'',''a'',''d'',''c''#} {#''a'',''a'',''c''#} ''f'' = {#''f'',''f'',''d'',''d''#}"
我真的卡住了。我发现在展开 def 并应用一些简单的自动化后我不能简单地做到这一点。所以我回到我原来的函数并对它做了一些调整,这样如果输入导致无限循环,它 returns 什么都没有。我以为这次会成功,但伊莎贝尔仍然无法证明终止。我敢肯定,很明显 size x
不断减少 size y
并且不能为负数,因此它最终必须在 size x = 0
或 y 不再是时终止x 的子集。
fun applied2 :: "'a multiset ⇒ 'a multiset ⇒ 'a ⇒ 'a multiset option" where
"applied2 x y z = (if z ∈# y ∨ y = {#} then None else (if y ⊆# x then Some (plus {#z#} (the (applied2 (x - y) y z))) else Some x))"
是否可以说服 Isabelle 使用 function
而不是 fun
来终止此函数?还是我必须考虑其他限制条件?
如果我不应该 post 提出这样的问题,我真的很抱歉。我对 Isabelle 仍然缺乏经验,我希望我能坚持自己的目标,尽我所能地学习这门语言。提前致谢!
我相信查看 documentation 会给您正确的语法。
function applied2 :: "'a multiset ⇒ 'a multiset ⇒ 'a ⇒ 'a multiset option" where
"applied2 x y z = (if z ∈# y ∨ y = {#} then None else (if y ⊆# x then Some (plus {#z#} (the (applied2 (x - y) y z))) else Some x))"
by pat_completeness auto
termination
by (relation "measure (λ(x,y,z). size x)")
(auto simp: mset_subset_eq_exists_conv nonempty_has_size)
如果问题是证明,sledgehammer 会为您找到它。
但是,我看不出您打算如何从 applied2 转到您真正想要的功能。真正的问题是确定性:你需要一个命令来查看子集。 Manuel 的解决方案是使用 Sup,但这确实不可执行。
如果非递归定义的唯一问题是如何将其应用于具体输入,我仍然认为我所说的可执行的替代定义是可行的方法。下面证明我给的两个非递归定义是等价的,以及对你上面给的例子的应用:
definition applied :: "'a multiset ⇒ 'a multiset ⇒ 'a ⇒ 'a multiset" where
"applied ms xs y = (if xs = {#} then ms else
(let n = Max {n. repeat_mset n xs ⊆# ms}
in ms - repeat_mset n xs + replicate_mset n y))"
lemma count_le_size: "count M x ≤ size M"
by (induction M) auto
lemma applied_code [code]:
"applied ms xs y = (if xs = {#} then ms else
(let n = (MIN x ∈set_mset xs. count ms x div count xs x)
in ms - repeat_mset n xs + replicate_mset n y))"
unfolding applied_def
proof (intro if_cong let_cong refl)
assume ne: "xs ≠ {#}"
have subset: "{n. repeat_mset n xs ⊆# ms} ⊆ {..size ms}"
proof safe
fix n assume n: "repeat_mset n xs ⊆# ms"
from ne obtain x where x: "x ∈# xs"
by auto
have "n * 1 ≤ n * count xs x"
using x by (intro mult_left_mono) auto
also have "… = count (repeat_mset n xs) x"
by simp
also have "… ≤ count ms x"
using n by (intro mset_subset_eq_count)
also have "… ≤ size ms"
by (rule count_le_size)
finally show "n ≤ size ms" by simp
qed
hence finite: "finite {n. repeat_mset n xs ⊆# ms}"
by (rule finite_subset) auto
show "Max {n. repeat_mset n xs ⊆# ms} = (MIN x∈set_mset xs. count ms x div count xs x)"
proof (intro antisym)
show "Max {n. repeat_mset n xs ⊆# ms} ≤ (MIN x∈set_mset xs. count ms x div count xs x)"
proof (rule Max.boundedI)
show "{n. repeat_mset n xs ⊆# ms} ≠ {}"
by (auto intro: exI[of _ 0])
next
fix n assume n: "n ∈ {n. repeat_mset n xs ⊆# ms}"
show "n ≤ (MIN x∈set_mset xs. count ms x div count xs x)"
proof (safe intro!: Min.boundedI)
fix x assume x: "x ∈# xs"
have "count (repeat_mset n xs) x ≤ count ms x"
using n by (intro mset_subset_eq_count) auto
also have "count (repeat_mset n xs) x = n * count xs x"
by simp
finally show "n ≤ count ms x div count xs x"
by (metis count_eq_zero_iff div_le_mono nonzero_mult_div_cancel_right x)
qed (use ne in auto)
qed (fact finite)
next
define m where "m = (MIN x∈set_mset xs. count ms x div count xs x)"
show "m ≤ Max {n. repeat_mset n xs ⊆# ms}"
proof (rule Max.coboundedI[OF finite], safe)
show "repeat_mset m xs ⊆# ms"
proof (rule mset_subset_eqI)
fix x
show "count (repeat_mset m xs) x ≤ count ms x"
proof (cases "x ∈# xs")
case True
have "count (repeat_mset m xs) x = m * count xs x"
by simp
also have "… ≤ (count ms x div count xs x) * count xs x"
unfolding m_def using ‹x ∈# xs› by (intro mult_right_mono Min.coboundedI) auto
also have "… ≤ count ms x"
by simp
finally show ?thesis .
next
case False
hence "count xs x = 0"
by (meson not_in_iff)
thus ?thesis by simp
qed
qed
qed
qed
qed
lemma replicate_mset_unfold:
assumes "n > 0"
shows "replicate_mset n x = {#x#} + replicate_mset (n - 1) x"
using assms by (cases n) auto
lemma
assumes "a ≠ c" "a ≠ f" "c ≠ f"
shows "applied {#a,a,c,a,a,c#} {#a,a,c#} f = mset [f, f]"
using assms
by (simp add: applied_code replicate_mset_unfold flip: One_nat_def)
value
命令对该示例不起作用,因为 a
、c
等是自由变量。但是如果你例如为他们制作一个特别的数据类型,它有效:
datatype test = a | b | c | f
value "applied {#a,a,c,a,a,c#} {#a,a,c#} f"
(* "mset [f, f]" :: "test multiset" *)