问题标签 [coinduction]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
coq - 对应于 *_rect 函数族的感应原理
定义一个新类型foo给了我一个递归原则foo_rect，它优雅地抽象了过来fix。cofix是否可以通过某种方式“翻转箭头”来定义同义等价物（抽象）？
coq - Ltac 调用“cofix”失败。错误：所有方法都必须在互归纳类型中构造元素
输出：
我不确定这意味着什么 - 两者map都是interleave直接的核心递归函数，用于构建共归纳类型的值。有什么问题？
coq - 证明共自然数的共归纳原理
我不得不承认我不是很擅长共同归纳。我试图展示关于自然数的互模拟原理，但我被困在一对（对称）案例上。
当关注第一个被承认的案例时，上下文是这样的：
想法？
coq - Coq 上的共归纳，类型不匹配
我一直在尝试互感类型，并决定定义自然数和向量的互感版本（列表及其类型中的大小）。我将它们和无限数定义为：
除了我为无限协向量给出的定义之外，这一切都有效
这给出了以下类型不匹配
我认为编译器会接受这个定义，因为根据定义，infnum = cosuc infnum。如何让编译器理解这些表达式是相同的？
io - Agda：如何在没有（不推荐使用的？）∞风格的共归纳的情况下进行非终止 IO（getLine）？
在这个关于如何getLine在 Agda 中做的问题中，主要答案建议使用偏性 monad 来处理可能不终止使用生成的 Costring 的情况。
另一方面，在 2.5.3 版本中，Coinduction的手册页建议不要使用 ∞，称它可以用来证明荒谬。但是 ∞ 用于IO.IO 和 IO.run的定义以及偏性monad。
问题：
- 是否可以使用没有 ∞ 的标准库来进行偏心和非终止 IO？如果没有，有什么替代方案？
- 标准库/文档是否过时？
- ∞ 的问题是由于与大小类型的交互吗？
谢谢！
coq - 定义无限树的等式关系
在 coq 中，我可以为成分是对的协推类型定义等式关系：
我也可以对组件是函数的类型执行此操作：
但我似乎无法为其组件是函数对的类型定义类似的关系：
我得到错误：
有什么方法可以为 InfiniteTree 类型定义明确的相等关系？
agda - 抽象呼叫站点后终止检查器失败
问题
我有一个简单的共归纳记录，其中包含一个 sum 类型的单个字段。Unit给了我们一个简单的类型来玩。
作品
valid通过终止检查：
休息
但是假设我想消除该Maybe Unit成员，并且只有在我有just.
现在终止检查器很不高兴！
为什么这不满足终止检查器？有没有办法解决这个问题，还是我的概念理解不正确？
背景
agda --version产量Agda version 2.6.0-7ae3882。我只使用默认选项进行编译。
的输出在-v term:100这里：https ://gist.github.com/emilyhorsman/f6562489b82624a5644ed78b21366239
尝试的解决方案
- 使用
Agda version 2.5.4.2. 不修复。 - 使用
--termination-depth=10. 不修复。
coq - Coq：证明 conat 是有限的或无限的
我有一个conat可以表示有限值和无限值的定义、从 的转换nat、无穷大的定义和互模拟关系：
我想证明它conat是有限的还是无限的（我不是 100% 确定这是正确的公式）：
到目前为止我无法证明它，但我可以证明另一个陈述，如果 aconat不是有限的，它是无限的（同样，不是 100% 确定公式）：
我不知道如何从not_fin_then_inf到fin_or_inf。
我的定义
fin_or_inf正确吗？我可以证明
fin_or_inf使用not_fin_then_inf或不使用它吗？
此外，我发现弥合这两个定理之间的差距涉及双模拟（或其扩展）的可判定性。我认为可判定性定理可以表述为
- 我可以证明
bisim_dec或任何类似的关于双模拟的陈述吗？
编辑
证明“有限或无限”的最初动机是证明 的交换性和结合性coplus：
nat采用与's相同的方式+不起作用，因为它需要==具有类似于 的引理的传递性plus_n_Sm，这使得 cofix 调用不受保护。否则，我必须同时破坏nand m，然后我就卡在了目标上n ~+ S' m == m ~+ S' n。
如果我选择另一种定义coplus：
然后coplus_comm很容易，但反而coplus_assoc变得几乎不可能证明。
- 我真的可以
coplus_comm用 的第一个定义coplus或coplus_assoc第二个定义来证明吗？
proof - CoNat : 证明 0 在左边是中性的
我正在试验Jesper Cockx 和 Andreas AbelCoNat的这篇论文中的定义：
我定义zero和plus：
我定义了双相似性：
但我坚持plus zero n与n. 我的猜测是，在证明中我应该（至少）有一个 with 子句iszero n：
但是 Agda 抱怨以下错误消息：
我怎样才能做出这个证明？
agda - 在 Agda 中，我如何证明在 uncons over coinductive list（aka Stream）之后的 cons 是身份？
我正在通过https://agda.readthedocs.io/en/v2.6.0.1/language/coinduction.html研究共归纳和共模。我以为我理解了文章代码，所以我决定研究以下命题。
我认为这个命题和文章问题非常相似，也可以证明，但我不能很好地证明。 这是我写的代码。
我认为可以对其进行细化，cons-uncons-id (tl xs)因为该类型与 merge-split-id 非常相似，但 Agda 不接受它。
这是我自己想到的一个问题，所以我觉得是对的，当然也有误解的可能。但是，uncons 和 cons 会按原样返回是很自然的。
如果您应该能够在不被误解的情况下证明它，请告诉我您如何证明它。
你能解释一下为什么你不能像 merge-split-id 一样证明它吗？
问候，谢谢！