时间戳

首页 > 解决方案 > 通过相互共游定义一对共定点

coq - 通过相互共游定义一对共定点

问题描述

有没有一种简单的方法可以定义两个 cofixpoints，让您同时输出它们？理想情况下，我想要以下内容：

Require Import Streams.

Definition alts : Stream bool * Stream bool :=
  cofix a := Cons false b with
        b := Cons true a for (a,b).

但是，似乎 Coq 只允许您从相互的 cofixes 块中返回其中一个标识符。我现在能做的最好的事情是：

Definition alts2 : Stream bool * Stream bool :=
  let a := cofix a := Cons false b with
                 b := Cons true a for a in (a,Cons true a).

当然，这并不理想，因为我需要重复b. 有没有更好的办法？

标签： coq

解决方案

一种解决方法是使用CoFixpoint相互定义a，b然后重用它们来定义alts。

CoFixpoint a : Stream bool := Cons false b
with b : Stream bool := Cons true a.

Definition alts : Stream bool * Stream bool := (a, b).

这种方法的缺点是我们用新名称a和b.

推荐阅读