coinduction

2热度

1回答

鉴于这种情况下中间结果： open import IO open import Data.String open import Data.Unit open import Coinduction postulate A : Set f : String → A g₁ g₂ : A → String 比方说，我想let实现类似 foo : IO ⊤ fo

1热度

1回答

定义一个“头”用于Coq的coinductive类型的流（没有模式匹配）

1）I相信这是可以使用感应类型没有模式匹配。（仅使用_rec，_rect，_ind）。这是不透明的，复杂的，但可能的。 2）是否有可能使用带模式匹配的共诱导类型？有存在的函数从coinductive类型构造函数coinductive类型的结构域的结合。 Coq是否明确生成它？如果是，如何重写'hd'？ Section stream. Variable A : Type.

2热度

1回答

对应于* _rect系列功能的合作原理

定义一个新类型foo给出了递归原则foo_rect，其优雅地摘要了fix。是否可以通过“翻转箭头”来定义一个合作的等效物（摘自cofix）？

2热度

1回答

Ltac呼叫“cofix”失败。错误：所有方法都必须构建coinductive类型

元素 Require Import Streams. CoFixpoint map {X Y : Type} (f : X -> Y) (s : Stream X) : Stream Y := Cons (f (hd s)) (map f (tl s)). CoFixpoint interleave {X : Type} (s : Stream X * Stream X) : S

5热度

2回答

是一个健全的无限列表？

在Prolog中，统一X = [1|X]是获得无限列表的理想方式吗？ SWI-Prolog没有任何问题，但是GNU Prolog只是简单的挂起。我知道，在大多数情况下，我可以 one(1). one(X) :- one(X). 更换名单，但我的问题是明确的，如果人们可以在“理智”的Prolog实现中使用的表达X = [1|X], member(Y, X), Y = 1。

2热度

2回答

Coinduction和从属类型

我试图编写一个Coq函数，它需要一个Stream和一个谓词并返回，作为list，该属性拥有的流的最长前缀。这是我有： Require Import List Streams. Require Import Lt. Import ListNotations. Local Open Scope list_scope. Section TakeWhile. Context {A : Ty

2热度

1回答

共同感应，类型不匹配

我一直在尝试共同诱导类型，并决定定义自然数和向量的共同诱导版本（与他们的大小类型列表）。我确定他们和无限多的像这样： CoInductive conat : Set := | cozero : conat | cosuc : conat -> conat. CoInductive covec (A : Set) : conat -> Set := | conil : covec A co

3热度

1回答

为什么我无法定义以下CoFixpoint？

我使用： $ coqtop -v The Coq Proof Assistant, version 8.4pl5 (February 2015) compiled on Feb 06 2015 17:44:41 with OCaml 4.02.1 予定义的下列CoInductive类型，stream： $ coqtop Welcome to Coq 8.4pl5 (February 20

1热度

1回答

证明共同自然数的coinduction原理

我不得不承认，我不是很擅长coinduction。我试图在共自然数上展示一个互模拟原则，但我被困在一对（对称）情况下。 CoInductive conat := | cozero : conat | cosucc : conat -> conat. CoInductive conat_eq : conat -> conat -> Prop := | eqbase

3热度

1回答

在Coq中证明Co-Inductive属性（词汇顺序是传递性的）

我试图证明Coq中的"Practical Coinduction"中的第一个示例。第一个例子是证明无限流整数上的词典排序是可传递的。我一直没能制定的证明，以绕过Guardedness condition 这里是我发展至今。首先是无限流的通常定义。然后定义称为lex的词典顺序。最后，传递性定理的失败证明。 Require Import Omega. Section stream. V