使用InteractionTrees库的[mrec]进行互递归定义报错求助

问题背景 #

我正在学习DeepSpec的InteractionTrees库（用于在Coq中表示递归和不纯程序），尝试文档中第一个[mrec]互递归示例时出现错误。此前已成功使用该库Interp模块的通用rec接口定义单递归函数，但找不到mrec的可用示例。

出错代码 #

Inductive D : Type -> Type :=
| Even : nat -> D bool
| Odd : nat -> D bool.

Definition def : D ~> itree (D +' void1) := fun _ d =>
  match d with
  | Even n => match n with
              | O => ret true
              | S m => ITree.trigger (Odd m)
              end
  | Odd n => match n with
             | O => ret false
             | S m => ITree.trigger (Even m)
             end
end. 

报错信息 #

Error:
In environment
T : Type
d : D T
n : nat
m : nat
The term "ITree.trigger (Odd m)" has type "itree (D +' void1) ?T0"
while it is expected to have type
 "itree (D +' void1) ?T@{T0:=T; T1:=bool}" (cannot satisfy constraint
"D bool" == "(D +' void1) ?T0").

解决方案 #

问题核心在于ITree.trigger的参数类型不匹配：def的类型要求返回的itree承载的请求是D +' void1类型，但原代码直接传入了D类型的构造子（如Odd m）。需要用inl将D类型的请求注入到D +' void1的左分支中，修改后的代码如下：

Inductive D : Type -> Type :=
| Even : nat -> D bool
| Odd : nat -> D bool.

Definition def : D ~> itree (D +' void1) := fun _ d =>
  match d with
  | Even n => match n with
              | O => ret true
              | S m => ITree.trigger (inl (Odd m))
              end
  | Odd n => match n with
             | O => ret false
             | S m => ITree.trigger (inl (Even m))
             end
end. 

原因说明 #

• D ~> itree (D +' void1)是一个自然变换，要求将任意D T映射为itree (D +' void1) T。
• ITree.trigger接收的参数必须是itree所承载的请求类型（即这里的D +' void1），而Odd m的类型是D bool，需要通过inl包装成(D +' void1) bool，才能满足类型约束。

内容的提问来源于stack exchange，提问作者Natasha Klaus