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