有限集上的递归函数 - 如何证明终止

Question

我（仍然）正在努力解决有限集上的递归函数。我想在有限（有限）集合上定义一个特殊的笛卡尔积。我想要实现的一个简化示例是下面的

pcart

函数：

theory Simplified
  imports Main "HOL-Library.FSet"
begin

inductive_set Fin where
  emptyI: "{} ∈ Fin" | 
  insertI: "A ∈ Fin ⟹ insert a A ∈ Fin"

lemma Fin_is_finite: "x ∈ Fin ⟹ finite x"
  using Fin.inducts by auto

lemma finite_is_Fin: "finite x ⟹ x ∈ Fin"
  by (metis Fin.simps Finp_Fin_eq finite_ne_induct)

definition ext :: "nat set ⇒ nat set set" where 
  "ext X = {{x}| x. x ∈ X}"

function pcart :: "nat set fset ⇒ nat set set" where 
  "pcart {||} = {}" | 
  "pcart (finsert a A) = ext a ∪ pcart A ∪ {{x}∪y| x y. x ∈ a ∧ y ∈ pcart A}"
  apply blast
  apply blast
  apply blast

问题是证明的最后一个子目标，我不知道如何处理：

 ⋀a A aa Aa.
       finsert a A = finsert aa Aa ⟹
       ext a ∪ pcart_sumC A ∪ {{x} ∪ y |x y. x ∈ a ∧ y ∈ pcart_sumC A} =
       ext aa ∪ pcart_sumC Aa ∪ {{x} ∪ y |x y. x ∈ aa ∧ y ∈ pcart_sumC Aa}

我的问题有三层：

1. 是否有更简单的方法来定义我的递归函数，以便我可以显示它终止？
2. 如果没有，有没有办法证明我的版本终止了？我错过了什么？
3. 如果 1 或 2 是可能的，并且我获得了一个递归终止函数

   pcart

   - 我该如何去展示

   pcart {||} = {}

   ？我用

   sorry

   假终止我当前的版本，然后尝试在我能想到的最简单的引理中使用它：

   lemma "pcart {||} = {}"

   。我没有得到任何证据。在这一点上，我不确定是否是因为

   pcart

   的定义有缺陷（我希望是这样），还是因为我不知道的其他一些问题。

任何建议都将受到高度赞赏和欢迎。 谢谢你

Answer 1

这不是终止问题。证明这个函数的终止实际上应该很容易。这里的问题是你必须证明你的函数的明确定义，即结果不依赖于它的处理顺序。这是因为

insert

不是一个自由构造函数，即

finsert x A = finsert y B

并不意味着

x = y

和

A = B

。

我必须承认，我真的不知道如何针对像您这样的递归函数规范执行此操作。我什至不确定这是否可能。即使是这样，我的建议是不要递归地定义函数，而是找到另一个更简单的定义，然后推导出递归方程作为推论。

我认为你想在这里指定的是：

pcart A

由所有集合

X

组成，这样就存在一个单射函数

f : X → A

，使得

f(x) ∈ x

。所以基本上，我的解释是你想要

pcart {{1}, {2,3}, {4,5}} =
  {{}, {1}, {2}, {3}, {4}, {5},
   {1,2}, {1,3}, {1,4}, {1,5}, {2,4}, {2,5}, {3,4}, {4,5}, 
   {1,2,4}, {1,3,4}, {1,2,5}, {1,3,5}}

这就是你想要的吗？

如果是，我想知道你为什么指定

pcart {||} = {}

而不是

pcart {||} = {{}}

。

我也想知道你是否打算写：

a |∉| A ⟹ pcart (finsert a A) = ext a ∪ pcart A ∪ {{x}∪y| x y. x ∈ a ∧ y ∈ pcart A}

我确实认为这会有所不同。

所以，如果我正确理解你想要什么，我会像这样指定它（在这种情况下也不需要使用 FSets）：

definition pcart :: "nat set set ⇒ nat set set" where
  "pcart A = {X. ∃f. f ∈ X → A ∧ inj_on f X ∧ (∀x∈X. x ∈ f x)}"

由此，可证明以下递归规范：

lemma "pcart {} = {{}}"

lemma
  assumes "a ∉ A"
  shows "pcart (insert a A) = pcart A ∪ {insert x y |x y. x ∈ a ∧ y ∈ pcart A}"

即使这不完全是您想要的，我认为应该可以对其进行调整，以便您确实得到您想要的。