我很难证明以下函数的终止：
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.
其中CCD_ 1是正则表达式的类型，而CCD_。资料来源于本文件第五页。该函数作为正则表达式的规范化函数的一部分出现(在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来证明终止。然而，我很难想出正确的衡量标准(基于操作员数量的尝试都没有成功)。我曾尝试将工作分解为单独的函数，但也遇到了类似的问题。如有任何帮助，或提示，我们将不胜感激。
您的代码比通常用measure函数处理的代码更复杂，因为您在下面的行中有一个嵌套的递归调用：
Union u v, w => norm_union u (norm_union v w) (* line 5 *)
我建议您不应该在类型regex中返回值，而应该在{r : regex | size r < combined_size u v}中返回size和regex0的适当概念。
在对您的问题进行了几个小时的研究后，还发现您的递归依赖于参数的词汇顺序。norm_union v w很可能返回Union v w，因此您需要参数对(u, Union v w)小于(Union u v, w)。因此，如果你真的想使用度量，你需要左手边的重量大于右手边的重量，并且你需要Union的一个分量的度量小于整体的度量。
由于词汇排序的性质，我选择不使用度量，而是使用一个有充分依据的顺序。此外，我对Program Fixpoint还不够了解，所以我使用另一个工具为您的问题开发了一个解决方案。我提出的解决方案可以在github上看到。至少这显示了所有需要证明的递减条件。
经过一天的额外工作，我现在对这个问题有了更完整的答案。它在这个链接上仍然可见。这个解决方案值得一些评论。
首先，我使用的是一个名为Fix的函数构造函数(长名称为Coq.Init.Wf.Fix。这是一个高阶函数，可以通过有充分根据的递归来定义函数。为此，我需要一个有充分依据的顺序，这个顺序被称为order。有充分理由的顺序在21世纪初被深入研究，它们仍然是le_regex0命令的基础。
其次，您编写的代码同时对两个类型为regex的值执行大小写分析，因此这导致了36个大小写(少了一点，因为当第一个参数为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的类型规定它只能用于小于名为order的顺序的初始参数p的regex项对。在这个类型描述中，我们还看到我选择表示递归调用的返回类型不是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的函数的调用表示，也证明递归调用的输入确实小于初始输入。所有的证明都在完全发展中。
可能会使用类似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)).
你可能仍然怀疑这是正确的功能，你要求的功能。为了说服我们自己，我们将证明一个引理，它准确地表达了你在定义中所说的话。
我们首先证明了CCD_ 47的相应引理。这依赖于一个与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的顺序对这些并集进行排序，同时在发现重复项时立即删除它们。这样的实现可以解决嵌套递归的需要。
如果你仍然想坚持嵌套递归，并且需要参考这里描述的技术，它首先由Balaa和Bertot在TPHOLs2000发表在一篇论文中。这篇论文很难阅读，因为它是在Coq使用不同语法的时候写的。