在 Coq 中证明函数终止
Proving Termination of Function in Coq
我无法证明以下函数的终止：
Fixpoint norm_union u v : regex :=
match u, v with
| Empty , v => v
| u , Empty => u
| Union u v, w => norm_union u (norm_union v w)
| u , Union v w => if eq_regex_dec u v
then Union v w
else if le_regex u v
then Union u (Union v w)
else Union v (norm_union u w)
| u , v => if eq_regex_dec u v
then u
else if le_regex u v
then Union u v
else Union v u
end.
其中 regex 是正则表达式的类型，le_regex 实现对正则表达式的总排序。来源是 this 文档的第五页。该函数作为正则表达式规范化函数的一部分出现（在 Isabelle/HOL 中形式化）。 le_regex 函数改编自同一篇论文。我正在使用 ascii 来避免通过可确定的总排序对 regex 进行参数化（并希望提取程序）。
Inductive regex : Set :=
| Empty : regex
| Epsilon : regex
| Symbol : ascii -> regex
| Union : regex -> regex -> regex
| Concat : regex -> regex -> regex
| Star : regex -> regex.
Lemma eq_regex_dec : forall u v : regex, {u = v} + {u <> v}.
Proof. decide equality; apply ascii_dec. Defined.
Fixpoint le_regex u v : bool :=
match u, v with
| Empty , _ => true
| _ , Empty => false
| Epsilon , _ => true
| _ , Epsilon => false
| Symbol a , Symbol b => nat_of_ascii a <=? nat_of_ascii b
| Symbol _ , _ => true
| _ , Symbol _ => false
| Star u , Star v => le_regex u v
| Star u , _ => true
| _ , Star v => false
| Union u1 u2 , Union v1 v2 => if eq_regex_dec u1 v1
then le_regex u2 v2
else le_regex u1 v1
| Union _ _ , _ => true
| _ , Union _ _ => false
| Concat u1 u2, Concat v1 v2 => if eq_regex_dec u1 v1
then le_regex u2 v2
else le_regex u1 v1
end.
我认为正确的做法是定义一个递减的度量并使用Program Fixpoint来证明终止。但是，我在想出正确的措施时遇到了麻烦（基于操作员数量的尝试没有成功）。我曾尝试将工作分解为单独的函数，但 运行 出现了类似的问题。任何帮助，或指向正确方向的提示，我们将不胜感激。
您的代码比通常使用度量函数处理的代码更复杂，因为您在以下行中有嵌套的递归调用：
Union u v, w => norm_union u (norm_union v w) (* line 5 *)
我建议您不应该 return 类型 regex 的值，而是 {r : regex | size r < combined_size u v} 类型的值以获得 size 和 combined_size 的合适概念。
在对您的问题进行了几个小时的研究之后，还发现您的递归依赖于参数的词法排序。 norm_union v w 可能 return Union v w，所以你需要参数对 (u, Union v w) 小于 (Union u v, w)。
所以如果真的要用一个measure，就需要左边的权值大于右边的权值，并且需要a Union的一个分量的measure是小于整体的尺度。
由于词汇排序的性质，我选择不使用度量而是使用有根据的顺序。另外，我不太了解 Program Fixpoint，所以我使用其他工具开发了解决您问题的方法。我想出的解决方案可以看here on github。至少这表明了所有需要证明的减少条件。
经过多一天的工作，我现在对这个问题有了更完整的回答。它在 this link 处仍然可见。这个解决方案值得一些评论。
首先，我使用了一个名为 Fix 的函数构造函数（长名称是 Coq.Init.Wf.Fix。这是一个高阶函数，可用于通过有根据的递归定义函数。我为此需要一个有根据的命令，这个命令叫做 order。有根据的命令在 2000 年代初期被深入研究，它们仍然是 Program Fixpoint 命令的基础。
其次，你写的代码同时对两个regex类型的值进行了case分析，所以这导致了36个case（少了一点，因为第一个参数没有对第二个参数进行case分析）一个是 Empty)。您在代码中看不到 36 种情况，因为多个构造函数都包含在相同的规则中，其中模式只是一个变量。为了避免这种情况的增加，我设计了一个特定的归纳类型
案例分析。我称这个特定类型为arT。然后我定义了一个函数 ar，它将 regex 类型的任何元素映射到 arT 的相应元素。类型 arT 具有三个构造函数，而不是六个，因此模式处理表达式将包含更少的代码，并且证明将不那么冗长。
然后我开始使用Fix定义norm_union。和 Coq（以及大多数定理证明器，包括 Isabelle）一样，语言
递归定义确保递归函数总是终止。在这种情况下，这是通过强制递归调用仅发生在比函数输入 小 的参数上来完成的。在这种情况下，这是通过一个函数描述递归函数的主体来完成的，该函数将初始输入作为第一个参数，将用于表示递归调用的函数作为第二个参数。这个函数的名字是norm_union_F，它的类型如下：
forall p : regex * regex,
forall g : (forall p', order p' p ->
{r : regex | size_regex r <= size_2regex p'}),
{r : regex | size_regex r <= size_2regex p}
在这个类型描述中，用来表示递归调用的函数名是g，我们看到g的类型规定它只能用在regex 项小于名为 order 的订单的初始参数 p。在这个类型描述中，我们也看到我选择表达递归调用的返回类型不是regex而是{r : regex | size_regex r <= size_2regex p'}。这是因为我们必须处理 嵌套递归 ，其中递归调用的输出将用作其他递归调用的输入。 这是这个答案的主要技巧。
然后我们有norm_union_F函数的主体：
Definition norm_union_F : forall p : regex * regex,
forall g : (forall p', order p' p ->
{r : regex | size_regex r <= size_2regex p'}),
{r : regex | size_regex r <= size_2regex p} :=
fun p norm_union =>
match ar (fst p) with
arE _ eq1 => exist _ (snd p) (th1 p)
| arU _ u v eq1 =>
match ar (snd p) with
arE _ eq2 => exist _ (Union u v) (th2' _ _ _ eq1)
| _ => exist _ (proj1_sig
(norm_union (u,
proj1_sig (norm_union (v, snd p)
(th3' _ _ _ eq1)))
(th4' _ _ _ eq1 (th3' _ _ _ eq1)
(proj1_sig (norm_union (v, snd p) (th3' _ _ _ eq1)))
_)))
(th5' _ _ _ eq1
(proj1_sig (norm_union (v, snd p)
(th3' _ _ _ eq1)))
(proj2_sig (norm_union (v, snd p)
(th3' _ _ _ eq1)))
(proj1_sig
(norm_union
(u, proj1_sig (norm_union (v, snd p)
(th3' _ _ _ eq1)))
(th4' _ _ _ eq1 (th3' _ _ _ eq1)
(proj1_sig (norm_union (v, snd p) (th3' _ _ _ eq1)))
(proj2_sig (norm_union (v, snd p) (th3' _ _ _ eq1))))))
(proj2_sig
(norm_union
(u, proj1_sig (norm_union (v, snd p)
(th3' _ _ _ eq1)))
(th4' _ _ _ eq1 (th3' _ _ _ eq1)
(proj1_sig (norm_union (v, snd p) (th3' _ _ _ eq1)))
(proj2_sig (norm_union (v, snd p) (th3' _ _ _ eq1)))))))
end
| arO _ d1 d2 =>
match ar (snd p) with
arE _ eq2 => exist _ (fst p) (th11' _)
| arU _ v w eq2 =>
if eq_regex_dec (fst p) v then
exist _ (Union v w) (th7' _ _ _ eq2)
else if le_regex (fst p) v then
exist _ (Union (fst p) (Union v w)) (th8' _ _ _ eq2)
else exist _ (Union v (proj1_sig (norm_union (fst p, w)
(th9' _ _ _ eq2))))
(th10' _ _ _ eq2
(proj1_sig (norm_union (fst p, w)
(th9' _ _ _ eq2)))
(proj2_sig (norm_union (fst p, w)
(th9' _ _ _ eq2))))
| arO _ d1 d2 =>
if eq_regex_dec (fst p) (snd p) then
exist _ (fst p) (th11' _)
else if le_regex (fst p) (snd p) then
exist _ (Union (fst p) (snd p)) (th12' _)
else exist _ (Union (snd p) (fst p)) (th13' _)
end
end.
在此代码中，所有输出值都在 exist _ 上下文中：我们不仅生成输出值，而且还表明该值的大小小于输入的组合大小对值。此外，所有递归调用都在 proj1_sig 上下文中，因此我们在构造输出值时忘记了大小信息。而且，所有递归调用（此处以调用名为 norm_union 的函数表示）也证明递归调用的输入确实小于初始输入。所有证明都在the complete development.
大概可以用refine这样的策略来定义norm_union_F，请大家探讨
然后我们定义真正的递归函数norm_union_1
Definition norm_union_1 : forall p : regex*regex,
{x | size_regex x <= size_2regex p} :=
Fix well_founded_order (fun p => {x | size_regex x <= size_2regex p})
norm_union_F.
请注意 norm_union_1 的输出类型为 {x | size_regex x <= size_2regex p}。这不是您要求的类型。所以我们定义了一个新的函数，它确实是你想要的，只需忘记输出的大小小于输入的逻辑信息。
Definition norm_union u v : regex := proj1_sig (norm_union_1 (u, v)).
您可能仍然怀疑这是您要求的正确功能。为了说服我们自己，我们将证明一个引理，它可以准确表达您在定义中所说的内容。
我们首先证明norm_union_1的相应引理。这依赖于与 Fix 函数相关的定理，名称 Fix_eq。需要完成的证明是相当常规的（它总是如此，它可以自动完成，但我从来没有想过为此开发自动工具）。
然后我们以最有趣的引理结束，norm_union。这是声明：
Lemma norm_union_eqn u v :
norm_union u v =
match u, v with
| Empty , v => v
| u , Empty => u
| Union u v, w => norm_union u (norm_union v w)
| u , Union v w => if eq_regex_dec u v
then Union v w
else if le_regex u v
then Union u (Union v w)
else Union v (norm_union u w)
| u , v => if eq_regex_dec u v
then u
else if le_regex u v
then Union u v
else Union v u
end.
请注意，这个等式的右边正是您在初始问题中给出的代码（我只是简单地复制粘贴了它）。这个大定理的证明也比较系统
现在，我完全按照您的要求做了努力，但事后我发现有一个使用三个递归函数的简单实现，可以实现相同的功能。第一个将 Union 的二叉树展平，使它们看起来像列表，而另外两个则根据 le_regex 的顺序对这些并集进行排序，同时在发现重复项后立即将其删除。这样的实现将解决嵌套递归的需要。
如果您仍然想坚持使用嵌套递归并需要参考这里描述的技术，它最初发表在 TPHOLs2000 上 Balaa 和 Bertot 的论文中。那篇论文很难读，因为它是在 Coq 使用不同语法的时候写的。
我无法证明以下函数的终止：
Fixpoint norm_union u v : regex :=
match u, v with
| Empty , v => v
| u , Empty => u
| Union u v, w => norm_union u (norm_union v w)
| u , Union v w => if eq_regex_dec u v
then Union v w
else if le_regex u v
then Union u (Union v w)
else Union v (norm_union u w)
| u , v => if eq_regex_dec u v
then u
else if le_regex u v
then Union u v
else Union v u
end.
其中 regex 是正则表达式的类型，le_regex 实现对正则表达式的总排序。来源是 this 文档的第五页。该函数作为正则表达式规范化函数的一部分出现（在 Isabelle/HOL 中形式化）。 le_regex 函数改编自同一篇论文。我正在使用 ascii 来避免通过可确定的总排序对 regex 进行参数化（并希望提取程序）。
Inductive regex : Set :=
| Empty : regex
| Epsilon : regex
| Symbol : ascii -> regex
| Union : regex -> regex -> regex
| Concat : regex -> regex -> regex
| Star : regex -> regex.
Lemma eq_regex_dec : forall u v : regex, {u = v} + {u <> v}.
Proof. decide equality; apply ascii_dec. Defined.
Fixpoint le_regex u v : bool :=
match u, v with
| Empty , _ => true
| _ , Empty => false
| Epsilon , _ => true
| _ , Epsilon => false
| Symbol a , Symbol b => nat_of_ascii a <=? nat_of_ascii b
| Symbol _ , _ => true
| _ , Symbol _ => false
| Star u , Star v => le_regex u v
| Star u , _ => true
| _ , Star v => false
| Union u1 u2 , Union v1 v2 => if eq_regex_dec u1 v1
then le_regex u2 v2
else le_regex u1 v1
| Union _ _ , _ => true
| _ , Union _ _ => false
| Concat u1 u2, Concat v1 v2 => if eq_regex_dec u1 v1
then le_regex u2 v2
else le_regex u1 v1
end.
我认为正确的做法是定义一个递减的度量并使用Program Fixpoint来证明终止。但是，我在想出正确的措施时遇到了麻烦（基于操作员数量的尝试没有成功）。我曾尝试将工作分解为单独的函数，但 运行 出现了类似的问题。任何帮助，或指向正确方向的提示，我们将不胜感激。
您的代码比通常使用度量函数处理的代码更复杂，因为您在以下行中有嵌套的递归调用：
Union u v, w => norm_union u (norm_union v w) (* line 5 *)
我建议您不应该 return 类型 regex 的值，而是 {r : regex | size r < combined_size u v} 类型的值以获得 size 和 combined_size 的合适概念。
在对您的问题进行了几个小时的研究之后，还发现您的递归依赖于参数的词法排序。 norm_union v w 可能 return Union v w，所以你需要参数对 (u, Union v w) 小于 (Union u v, w)。
所以如果真的要用一个measure，就需要左边的权值大于右边的权值，并且需要a Union的一个分量的measure是小于整体的尺度。
由于词汇排序的性质，我选择不使用度量而是使用有根据的顺序。另外，我不太了解 Program Fixpoint，所以我使用其他工具开发了解决您问题的方法。我想出的解决方案可以看here on github。至少这表明了所有需要证明的减少条件。
经过多一天的工作，我现在对这个问题有了更完整的回答。它在 this link 处仍然可见。这个解决方案值得一些评论。
首先，我使用了一个名为 Fix 的函数构造函数（长名称是 Coq.Init.Wf.Fix。这是一个高阶函数，可用于通过有根据的递归定义函数。我为此需要一个有根据的命令，这个命令叫做 order。有根据的命令在 2000 年代初期被深入研究，它们仍然是 Program Fixpoint 命令的基础。
其次，你写的代码同时对两个regex类型的值进行了case分析，所以这导致了36个case（少了一点，因为第一个参数没有对第二个参数进行case分析）一个是 Empty)。您在代码中看不到 36 种情况，因为多个构造函数都包含在相同的规则中，其中模式只是一个变量。为了避免这种情况的增加，我设计了一个特定的归纳类型
案例分析。我称这个特定类型为arT。然后我定义了一个函数 ar，它将 regex 类型的任何元素映射到 arT 的相应元素。类型 arT 具有三个构造函数，而不是六个，因此模式处理表达式将包含更少的代码，并且证明将不那么冗长。
然后我开始使用Fix定义norm_union。和 Coq（以及大多数定理证明器，包括 Isabelle）一样，语言
递归定义确保递归函数总是终止。在这种情况下，这是通过强制递归调用仅发生在比函数输入 小 的参数上来完成的。在这种情况下，这是通过一个函数描述递归函数的主体来完成的，该函数将初始输入作为第一个参数，将用于表示递归调用的函数作为第二个参数。这个函数的名字是norm_union_F，它的类型如下：
forall p : regex * regex,
forall g : (forall p', order p' p ->
{r : regex | size_regex r <= size_2regex p'}),
{r : regex | size_regex r <= size_2regex p}
在这个类型描述中，用来表示递归调用的函数名是g，我们看到g的类型规定它只能用在regex 项小于名为 order 的订单的初始参数 p。在这个类型描述中，我们也看到我选择表达递归调用的返回类型不是regex而是{r : regex | size_regex r <= size_2regex p'}。这是因为我们必须处理 嵌套递归 ，其中递归调用的输出将用作其他递归调用的输入。 这是这个答案的主要技巧。
然后我们有norm_union_F函数的主体：
Definition norm_union_F : forall p : regex * regex,
forall g : (forall p', order p' p ->
{r : regex | size_regex r <= size_2regex p'}),
{r : regex | size_regex r <= size_2regex p} :=
fun p norm_union =>
match ar (fst p) with
arE _ eq1 => exist _ (snd p) (th1 p)
| arU _ u v eq1 =>
match ar (snd p) with
arE _ eq2 => exist _ (Union u v) (th2' _ _ _ eq1)
| _ => exist _ (proj1_sig
(norm_union (u,
proj1_sig (norm_union (v, snd p)
(th3' _ _ _ eq1)))
(th4' _ _ _ eq1 (th3' _ _ _ eq1)
(proj1_sig (norm_union (v, snd p) (th3' _ _ _ eq1)))
_)))
(th5' _ _ _ eq1
(proj1_sig (norm_union (v, snd p)
(th3' _ _ _ eq1)))
(proj2_sig (norm_union (v, snd p)
(th3' _ _ _ eq1)))
(proj1_sig
(norm_union
(u, proj1_sig (norm_union (v, snd p)
(th3' _ _ _ eq1)))
(th4' _ _ _ eq1 (th3' _ _ _ eq1)
(proj1_sig (norm_union (v, snd p) (th3' _ _ _ eq1)))
(proj2_sig (norm_union (v, snd p) (th3' _ _ _ eq1))))))
(proj2_sig
(norm_union
(u, proj1_sig (norm_union (v, snd p)
(th3' _ _ _ eq1)))
(th4' _ _ _ eq1 (th3' _ _ _ eq1)
(proj1_sig (norm_union (v, snd p) (th3' _ _ _ eq1)))
(proj2_sig (norm_union (v, snd p) (th3' _ _ _ eq1)))))))
end
| arO _ d1 d2 =>
match ar (snd p) with
arE _ eq2 => exist _ (fst p) (th11' _)
| arU _ v w eq2 =>
if eq_regex_dec (fst p) v then
exist _ (Union v w) (th7' _ _ _ eq2)
else if le_regex (fst p) v then
exist _ (Union (fst p) (Union v w)) (th8' _ _ _ eq2)
else exist _ (Union v (proj1_sig (norm_union (fst p, w)
(th9' _ _ _ eq2))))
(th10' _ _ _ eq2
(proj1_sig (norm_union (fst p, w)
(th9' _ _ _ eq2)))
(proj2_sig (norm_union (fst p, w)
(th9' _ _ _ eq2))))
| arO _ d1 d2 =>
if eq_regex_dec (fst p) (snd p) then
exist _ (fst p) (th11' _)
else if le_regex (fst p) (snd p) then
exist _ (Union (fst p) (snd p)) (th12' _)
else exist _ (Union (snd p) (fst p)) (th13' _)
end
end.
在此代码中，所有输出值都在 exist _ 上下文中：我们不仅生成输出值，而且还表明该值的大小小于输入的组合大小对值。此外，所有递归调用都在 proj1_sig 上下文中，因此我们在构造输出值时忘记了大小信息。而且，所有递归调用（此处以调用名为 norm_union 的函数表示）也证明递归调用的输入确实小于初始输入。所有证明都在the complete development.
大概可以用refine这样的策略来定义norm_union_F，请大家探讨
然后我们定义真正的递归函数norm_union_1
Definition norm_union_1 : forall p : regex*regex,
{x | size_regex x <= size_2regex p} :=
Fix well_founded_order (fun p => {x | size_regex x <= size_2regex p})
norm_union_F.
请注意 norm_union_1 的输出类型为 {x | size_regex x <= size_2regex p}。这不是您要求的类型。所以我们定义了一个新的函数，它确实是你想要的，只需忘记输出的大小小于输入的逻辑信息。
Definition norm_union u v : regex := proj1_sig (norm_union_1 (u, v)).
您可能仍然怀疑这是您要求的正确功能。为了说服我们自己，我们将证明一个引理，它可以准确表达您在定义中所说的内容。
我们首先证明norm_union_1的相应引理。这依赖于与 Fix 函数相关的定理，名称 Fix_eq。需要完成的证明是相当常规的（它总是如此，它可以自动完成，但我从来没有想过为此开发自动工具）。
然后我们以最有趣的引理结束，norm_union。这是声明：
Lemma norm_union_eqn u v :
norm_union u v =
match u, v with
| Empty , v => v
| u , Empty => u
| Union u v, w => norm_union u (norm_union v w)
| u , Union v w => if eq_regex_dec u v
then Union v w
else if le_regex u v
then Union u (Union v w)
else Union v (norm_union u w)
| u , v => if eq_regex_dec u v
then u
else if le_regex u v
then Union u v
else Union v u
end.
请注意，这个等式的右边正是您在初始问题中给出的代码（我只是简单地复制粘贴了它）。这个大定理的证明也比较系统
现在，我完全按照您的要求做了努力，但事后我发现有一个使用三个递归函数的简单实现，可以实现相同的功能。第一个将 Union 的二叉树展平，使它们看起来像列表，而另外两个则根据 le_regex 的顺序对这些并集进行排序，同时在发现重复项后立即将其删除。这样的实现将解决嵌套递归的需要。
如果您仍然想坚持使用嵌套递归并需要参考这里描述的技术，它最初发表在 TPHOLs2000 上 Balaa 和 Bertot 的论文中。那篇论文很难读，因为它是在 Coq 使用不同语法的时候写的。