建立树和减少修复的参数
我正在尝试使用Coq中的以下函数实现一个函数来构建一个包含n个元素的Braun树，但Coq给我的错误是它无法猜测fix的递减参数：
Fixpoint copy (x : V) (n : nat) : BraunTree :=
let
fix copy2 (a : V) (i : nat) : (BraunTree * BraunTree) :=
match i with
| 0 => (T a E E,E)
| _ => match Nat.odd i with
| true => let m := ((i - 1) / 2) in
let (s,t) := copy2 a m in
((T a s t),(T a t t))
| false => let m := ((i - 2) / 2) in
let (s,t) := copy2 a m in
((T a s s),(T a s t))
end
end
in
match copy2 x n with
|(_,snd) => snd
end.我知道这不是单独的偶数和奇数情况的问题，因为当我删除偶数/奇数情况时，它给出了相同的错误：
Fixpoint copy (x : V) (n : nat) : BraunTree :=
let
fix copy2 (a : V) (i : nat) : (BraunTree * BraunTree) :=
match i with
| 0 => (T a E E,E)
| _ => let m := ((i - 1) / 2) in
let (s,t) := copy2 a m in
((T a s t),(T a t t))
end
in
match copy2 x n with
|(_,snd) => snd
end.我如何才能让Coq相信我实际上是一个递减的参数呢？
编辑BraunTree类型：
Inductive BraunTree : Type :=
| E : BraunTree
| T: V -> BraunTree -> BraunTree -> BraunTree.回答 1
Stack Overflow用户
发布于 2019-05-15 07:29:33
Fixpoint/fix只允许对语法较小的参数进行递归调用。
Fixpoint example (n : nat) :=
... (* There must be a match on [n] somewhere *)
... match n with
| O => base_case (* no recursive call allowed *)
| S m =>
... (example m)
(* We can only call [example] on [m], or some even smaller value obtained by matching on [m] *)
end ...特别是，不允许对通过某个任意函数(在本例中为copy2 a ((i-1) / 2)中的div和sub )获得的值进行递归调用。
这里有三个选项：
- 选择了自然数的另一种表示，这样它上的模式匹配就会自然地分解成所需定义的不同分支(基本情况(零)，偶数，奇数)。
- 利用了递归深度实际上由
n限定的事实，所以我们可以使用n作为“燃料”，我们知道在我们进行递减参数的子项之前，n实际上不会耗尽。这个解决方案比以前的解决方案不那么通用和健壮；它与终止检查器的斗争要困难得多。
另一种表示
我们有三种情况:零、偶数和奇数。幸运的是，标准库有一个结构几乎相同的类型，即positive
Inductive positive := (* p > 0 *)
| xH (* 1 *)
| xI (p : positive) (* 2p + 1 *)
| xO (p : positive) (* 2p *)
.用一个额外的零指向类型positive，我们得到N
Inductive N :=
| N0 (* 0 *)
| Npos (p : positive) (* p > 0 *)
.还有一个转换函数N.of_nat : nat -> N，不过，如果转换变得太烦人，使用N而不是nat也可能是个好主意。
最终的定义从N上的用例分析开始，揭示positive编号的用例由fix-point处理，其中基本用例是1而不是0。我们必须转移一些细节，因为偶数情况是2p而不是2p+2，所以我们必须做(i-1，i)而不是一对大小为(i+1，i)的树。但总体而言，递归用例仍然自然地符合非正式规范：
Require Import NArith PArith.
Parameter V : Type.
Inductive BraunTree : Type :=
| E : BraunTree
| T: V -> BraunTree -> BraunTree -> BraunTree.
Definition copy (x : V) (n : N) : BraunTree :=
match n with
| N0 => E
| Npos p =>
let
(* copy2 a i : a tree of (i-1) copies of a, and another of i copies of a *)
fix copy2 (a : V) (i : positive) : (BraunTree * BraunTree) :=
match i with
| xH => (* i = 1 *)
(E, T a E E)
| xI p => (* i = 2p + 1 *)
let (s,t) := copy2 a p in
((T a t s),(T a t t))
| xO p => (* i = 2p *)
let (s,t) := copy2 a p in
((T a s s),(T a t s))
end
in
match copy2 x p with
|(_,snd) => snd
end
end.刚好足够的燃料
我们将燃料作为递减参数添加到fix中。我们只能在n = i = 0的情况下运行，所以我们知道结果应该是什么。
(* note: This doesn't need to be a Fixpoint *)
Definition copy (x : V) (n : nat) : BraunTree :=
let
fix copy2 (a : V) (n : nat) (i : nat) : (BraunTree * BraunTree) :=
match n with
| O => (T a E E,E)
| S n' =>
match i with
| O => (T a E E,E)
| _ =>
if Nat.odd i then
let m := div2 ((i - 1) / 2) in
let (s,t) := copy2 a n' m in
((T a s t),(T a t t))
else
let m := div2 ((i - 2) / 2) in
let (s,t) := copy2 a n' m in
((T a s s),(T a s t))
end
end
in
match copy2 x n n with
|(_,snd) => snd
end.这在以下情况下工作得很好：
- ，我们可以计算出所需的燃料量；
- ，当我们耗尽燃料时，有一个可以预测的答案。
如果这两个假设中的任何一个都不成立，我们就需要使用option来丢弃我们的代码。
嵌套递归
正如前面提到的，Coq对减少参数有严格的规则。通常的解释是，我们只能对通过模式匹配递减参数(或递归地，它的一个子项)获得的子项进行递归调用。
一个明显的限制是，因为条件是语法的(即，Coq查看定义来跟踪递减参数的出处)，参数n最多只能减少一个常数(相对于n是常数)，因为在一个定义中只有有限多个match。特别是，无法对除以2的结果进行递归调用，因为这表示递减n/2，这是n中的一个线性值。
不管是好是坏，Coq的终止标准实际上比这更聪明:可以将递减参数传递给嵌套固定点，“子项”关系将通过它进行跟踪。
Cons-free除法
实际上，Peano nat的除法可以这样定义，即Coq可以判断结果是被除数的子项：
Definition div2 (n : nat) :=
let fix d2 (n1 : nat) (n2 : nat) {struct n1} :=
match n2 with
| S (S n2') =>
match n1 with
| O => n1
| S n1' => d2 n1' n2'
end
| _ => n1
end
in d2 n n.我们的想法是编写一个包含两个参数的代码解决方案(有点像燃料解决方案)，它们以相等(d2 n n)开头，并且我们从其中一个(n2)中删除两个 S构造函数(n2)，为我们从另一个(<>D54>)中删除一个代码( S )。重要细节：
- 在所有非递归的情况下，我们返回
n1(在任何情况下都不是0)，然后保证它是最上面的 - 的子项。函数必须在
n2(我们返回的项)中递减，而不是
(Coq只跟踪递减参数的子项)。
所有这些都确保了div2 n是n的子术语(而不是严格的子术语(或专有的子术语)，因为n可以是O)。
这与以前的基于燃料的解决方案有相似之处，但在这里，递减的论点比欺骗类型检查器的设备更相关。
这种技术是cons-free编程的一种变体。(但请注意，这些约束与文献中讨论的约束并不完全相同，例如，当重点放在避免内存分配而不是通过结构良好来确保终止时。)
结论：copy的定义
一旦我们有了div2，我们就可以通过一些调整来定义copy，以获得i-1和i-2作为i的适当子项，同样是通过模式匹配。下面，i'和i''是i (通过视觉检查)的适当子项，div2 i'和div2 i''是i'和i'' (根据div2的定义)的子项。通过传递性，它们是i的真子项，因此终止检查器接受。
Definition copy (x : V) (n : nat) : BraunTree :=
let
fix copy2 (a : V) (i : nat) : (BraunTree * BraunTree) :=
match i with
| 0 => (T a E E,E)
| S i' => (* i' = i-1 *)
if Nat.odd i then
let m := div2 i' in
let (s,t) := copy2 a m in
((T a s t),(T a t t))
else
match i' with
| O => (* Unreachable *) (E, E)
| S i'' => (* i'' = i-2 *)
let m := div2 i'' in
let (s,t) := copy2 a m in
((T a s s),(T a s t))
end
end
in
match copy2 x n with
|(_,snd) => snd
end.https://stackoverflow.com/questions/56132183
复制相似问题