Idris中流函数性质的证明
Idris是一种依赖类型的编程语言，它支持函数式编程和证明辅助工具。流函数性质是指在Idris中，函数可以被视为流（stream）的一种形式，具有一些特定的性质。
流函数性质的证明可以通过以下步骤进行：
- 首先，我们需要定义流函数。在Idris中，流函数可以通过递归定义来表示。例如，我们可以定义一个简单的自然数流函数：
natStream : Stream Nat
natStream = 0 :: map (+1) natStream这个函数定义了一个自然数流，从0开始，每个元素都是前一个元素加1。这个定义使用了::操作符将0作为流的第一个元素，然后使用map函数将加1的操作应用于整个流。
- 接下来，我们可以证明流函数的性质。例如，我们可以证明这个自然数流函数是无限的，即它包含无穷多个元素。
infiniteStream : (s : Stream a) -> (n : Nat) -> In s n
infiniteStream s Z = Here
infiniteStream (x :: xs) (S k) = There (infiniteStream xs k)
natStreamInfinite : (n : Nat) -> In natStream n
natStreamInfinite = infiniteStream natStream这个证明使用了In类型来表示一个元素在流中的存在性。In类型是一个归纳类型，它有两个构造器：Here表示元素在流的头部，There表示元素在流的尾部。通过递归地应用In类型，我们可以证明一个元素在流中的存在性。
在这个证明中，我们定义了一个辅助函数infiniteStream，它接受一个流s和一个自然数n作为参数，并返回一个证明，证明了元素n在流s中的存在性。然后，我们使用infiniteStream函数证明了自然数流函数natStream是无限的。
- 最后，我们可以应用流函数的性质来解决特定的问题。例如，我们可以使用自然数流函数来生成一个无限的斐波那契数列。
fibStream : Stream Nat
fibStream = 0 :: 1 :: zipWith (+) fibStream (tail fibStream)这个定义使用了zipWith函数来将两个流按照某个操作符进行组合。在这个例子中，我们将斐波那契数列的前两个元素（0和1）作为流的头部，然后使用zipWith函数将斐波那契数列的当前元素和下一个元素相加，得到下一个元素。
通过以上步骤，我们可以证明Idris中流函数的性质，并应用它们来解决各种问题。在实际应用中，可以根据具体需求选择合适的流函数，并结合腾讯云提供的相关产品来实现相应的功能。
相关·内容
我正在用Idris编写一个基本的一元解析器，以适应Haskell的语法和不同之处。我很好地掌握了这方面的基础知识，但我仍然无法尝试为解析器创建VerifiedSemigroup和VerifiedMonoid实例。
这是解析器类型、半群和Monoid实例，以及VerifiedSemigroup实例的开始。
data ParserM a = Parser (String -> List (a, String))
parse : ParserM a -> String -> List (a, String)
parse (Par
浏览 3提问于2014-08-07得票数 14
回答已采纳
Idris具有非常简单的cong函数。
cong : {f : t -> u} -> a = b -> f a = f b
cong Refl = Refl
如果我为超过零的加法创建一个特殊形式的cong，它不能进行类型检查。
cong0 : {f : Nat -> Nat} -> a + Z = a -> f (a + Z) = f a
cong0 Refl = Refl
在Idris 1中，我得到了
When checking left hand side of cong0:
When checking an application of Main.co
浏览 14提问于2021-05-21得票数 1
如何让Idris自动证明两个值不相等？
p : Not (Int = String)
p = \Refl impossible
如何让Idris自动生成此证明？auto似乎无法证明涉及Not的语句。我的最终目标是让Idris自动证明向量中的所有元素都是唯一的，并且两个向量是不相交的。
namespace IsSet
data IsSet : List t -> Type where
Nil : IsSet []
(::) : All (\a => Not (a = x)) xs -> IsSet xs -> IsSet (x ::
浏览 1提问于2017-09-30得票数 8
回答已采纳
1回答
我有一个函数，它返回一个应该是非零的整数，并且希望通过它的返回类型来保证这一点。在Idris中，如何表示非零整数的类型？
浏览 0提问于2018-01-19得票数 4
回答已采纳
1回答
如果我正确理解它(主要是从applyTactic函数的存在)，就有可能为Idris中的定理证明器编写自定义策略。我可以用哪些(或哪里)例子来学习如何做到这一点？
浏览 1提问于2014-04-13得票数 7
回答已采纳
1回答
平等模式匹配
、、
我对伊德里斯有点陌生。我以前用过一点agda，我在GHC Haskell有很强的背景。我试着去理解为什么在GHC Haskell中工作的东西在Idris不起作用。以下代码未编译(idris版本0.12.3，nobuiltins，noprelude)：
data Nat = S Nat | Z
plus : Nat -> Nat -> Nat
plus Z right = right
plus (S left) right = S (plus left right)
rightIdentityAlt : (n : Nat) -> n = (plus n Z)
浏览 1提问于2018-01-19得票数 11
回答已采纳
1回答
我定义了一个操作符+- (忽略可怕的名称)如下：
infixr 10 +-
(+-) : Fin (S n) -> Fin (S m) -> Fin (S (n + m))
(+-) {n} {m} FZ f' = rewrite plusCommutative n m in weakenN n f'
(+-) {n = S n} (FS f) f' = FS (f +- f')
其意图是它的行为与在+上定义的Fin完全一样，但是结果的上限是1，据我所知，它正确工作。
我遇到的问题是试图证明(FZ +- f) = f适用于任何f : Fin n。我并
浏览 0提问于2015-07-24得票数 3
回答已采纳
2回答
我试图比较String和String，期待True。
Idris> String == String
Can't find implementation for Eq Type
然后，当我将一个False与一个Bool进行比较时，我期望得到Bool。
Idris> String /= Bool
Can't find implementation for Eq Type
我是不是错过了一个import
浏览 2提问于2016-04-11得票数 6
回答已采纳
2回答
我开始深入研究依赖类型编程，并发现Agda和Idris语言最接近Haskell，所以我从那里开始。
我的问题是:它们之间的主要区别是什么？类型系统在这两种语言中的表现形式是否相同？如果能有一个全面的比较和关于好处的讨论，那就太好了。
我已经发现了一些：
Idris有类似于Haskell的类型类，而Agda使用实例argumentsIdris包括一元和应用符号，它们似乎都有某种可重新绑定的语法，尽管不能真正确定它们是否相同。
编辑:这个问题的Reddit页面上有更多的答案：
浏览 75提问于2012-02-28得票数 181
回答已采纳
1回答
Idris Dec诉也许
、、、
一个人能用Dec而不是Maybe在Idris上表达什么样的东西？
或者换句话说:何时选择Dec，何时选择Maybe
浏览 2提问于2017-03-24得票数 4
回答已采纳
1回答
基于范数约束向量的类型
、、、、
在Haskell或Idris这样的语言中，是否可以创建一个数据类型来检查一个函数的输入向量是否是酉的？也就是说，我是否可以创建一个数据类型SumsToOne来检查向量是否加为1，等等？
浏览 3提问于2022-04-08得票数 3
回答已采纳
1回答
在Idris中，您可以在Fin n和(x ** So (x < n))之间建立同构吗？(我实际上并不了解Idris，因此这些类型可能无效。一般的想法是，我们有一个通过构造保证小于n的数据类型，另一个通过测试保证小于n的数据类型。)
浏览 3提问于2016-03-22得票数 0
1回答
Agda使用以下操作符显示集合之间的逆：
_↔_ : ∀ {f t} → Set f → Set t → Set _
在Idris中也有类似的吗？我试图在列表中定义包的相等性
data Elem : a -> List a -> Type where
Here : {xs : List a} -> Elem x (x :: xs)
There : {xs : List a} -> Elem x xs -> Elem x (y :: xs)
(~~) : List a -> List a -> Type
xs ~~ ys {a} = Elem
浏览 2提问于2014-12-03得票数 6
回答已采纳
1回答
将Coq源转换为Idris的一些有用的指导方针是什么(例如，它们的类型系统有多相似，以及如何翻译这些证据)？据我所知，Idris的内置战术库是最小的，但也是可以扩展的，所以我认为，通过一些额外的工作，这应该是可能的。
浏览 3提问于2014-05-02得票数 13
回答已采纳
如何使用Idris调用FPtr类型为空参数的函数？我查看了这个库，它看起来既没有空指针，也没有将整数转换为指针的方法。
浏览 3提问于2014-11-01得票数 1
回答已采纳
我刚开始玩idris和定理证明。我可以在互联网上学习大多数基本事实的证据，所以我想尝试一些我自己的武断的东西。因此，我想为map的以下基本属性编写一个验证项：
map : (a -> b) -> List a -> List b
prf : map id = id
直觉上，我可以想象证明应该如何工作:取一个任意的列表l并分析映射id l的可能性。当l是空的时候，很明显；当l是非空的时候，它是基于函数应用程序保持相等的概念。所以，我可以这样做：
prf' : (l : List a) -> map id l = id l
这就像对所有人的陈述。我怎样才能把它变成有
浏览 2提问于2015-09-27得票数 10
回答已采纳
3回答
Agda和Idris都有效地禁止了Type类型值的模式匹配。看起来Agda总是在第一种情况下匹配，而Idris只是抛出一个错误。
那么，为什么打字是件坏事？它会破坏一致性吗？我还没有找到很多关于这个话题的信息。
浏览 8提问于2014-04-22得票数 50
回答已采纳
1回答
有关于Idris中postulate构造的性质和使用的最新信息吗？在教程/手册中没有任何关于这个主题的内容，我似乎也无法在wiki中找到任何东西。蒂娅。
浏览 1提问于2015-01-17得票数 13
回答已采纳
1回答
我试图在Idris中定义一个函数(congruentialMethod)，其中包括对函数提供的一些参数应用模数算法。模数算法要求第二个参数为非零，因此我尝试利用modNatNZ并向函数类型签名中添加一个证明。然而，我觉得我的尝试很笨拙。
首先，当我定义作为模数函数(let m : Nat = 2147483647)的第二个arg的值时，-I必须执行一些笨拙的案例匹配，以使Idris相信这个值大于零。如果我不这样做，那么类型检查将花费很长时间。
其次，我真的不明白为什么当我调用函数(congruentialMethod)时必须提供一个证据。我在函数签名中将该证明指定为auto，认为Idris可以
浏览 1提问于2018-05-26得票数 1
回答已采纳
2回答
从哪里开始依赖类型编程？
、、、、
有一个Idris教程，一个Agda教程和许多其他教程风格的论文和介绍性材料，没有结束的参考资料，但仍有待学习。我在这些过程中爬来爬去，大多数时候，我被数学符号和新术语困住了，没有任何解释。也许我的数学糟透了-)
是否有任何有纪律的方法来处理依赖类型编程？就像当您想学习Haskell时，您先从"Teach yourself“开始，当您想学习Scala时，您可以从Odersky的书开始，对于Ruby来说，您读过带有变异bug的奇怪教程。但我不能从他们的书开始Agda或Idris。它们远远高于我的脑袋。我试过Coq，被困在它的全面气象证明风格。Agda需要一个庞大的数学背景，Idris，好吧
浏览 7提问于2012-11-21得票数 44
3回答
例如：
intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
intersectBy _ [] _ = []
intersectBy _ _ [] = []
intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]
[]有额外的模式，看起来它们在Haskell Data.List中使用，但是这是什么样的优化呢？和伊德里斯有什么区别？
我之所以这样问，是因为我听说“这会使对它的推理变得更加困难”，还有一个说我没有时间
浏览 5提问于2015-04-22得票数 8
回答已采纳
我试着把不同类型的东西放到一个列表中，用字符串标记。
我想要的是这样的东西：
arr1 : ?what_should_that_be
arr1 = [("num" ** 1), ("str" ** "hello")]
所以我试图证明我给出的标记实际上是一个有效的标记(通过提供IsTag tag的证明)，但是似乎编译器没有得到它，那么我现在该怎么办呢？
data IsTag : String -> Type where
NumIsTag : IsTag "num"
StrIsTag : IsTag "s
浏览 16提问于2018-01-09得票数 0
下面的Idris证明没有打打字机。
hts : (s : Stream a) -> (head s :: tail s = s)
hts (x::xs) = Refl
我得到的错误是：
Type mismatch between
x :: Delay xs = x :: Delay xs
and
x :: Delay (tail (x :: Delay xs)) = x :: Delay xs
对于非空的Vect的打字机也有类似的证明：
import Data.Vect
htv : (s : Vect (S k) a) -&
浏览 3提问于2018-01-03得票数 6
我想知道如何证明(So (not (y == y)))是Uninhabited的一个实例，但我不确定该怎么做。它在Idris中是可证明的，还是由于y的一个奇怪的Eq实现的可能性而不可证明？
浏览 13提问于2017-07-02得票数 3
回答已采纳
1回答
Idris可以将.idr编译成C代码(JS，NodeJS)。有没有可能以相反的方向将C代码编译成Idris格式？或者，在Idris代码中直接使用C函数？
浏览 0提问于2018-09-30得票数 2
我正在尝试将Idris与原生脚本结合使用，通过使用Idris codegen FFI并使用JavaScript作为JavaScript目标。但是，原生脚本似乎使用了全局变量，例如一个名为global的对象。我如何才能在Idris中使用该对象？
浏览 7提问于2018-02-12得票数 3
我用Idris写了以下证明：
n : Nat
n = S (k + k)
lemma: n * n = ((k * n) + k) + (1 + (((k * n) + k) + 0))
lemma = sym $
rewrite plusZeroRightNeutral ((k * n) + k) in
rewrite plusAssociative ((k * n) + k) 1 ((k * n) + k) in
rewrite plusCommutative ((k * n) + k) 1 in
rewrite mult2 ((k *
浏览 5提问于2017-10-03得票数 3
回答已采纳
我预期这个值为3，但得到了一个错误：
Idris> :let x = Just 2
Idris> 1 + !x
(input):1:3-4:When checking an application of function Prelude.Interfaces.+:
Type mismatch between
Integer (Type of (_bindApp0))
and
Maybe b (Expected type)
我也试过这个，没有一个托普莱尔绑定，并得到
Idris> l
浏览 3提问于2017-03-23得票数 3
回答已采纳
我正在学习idris，并且对证明列表的性质非常感兴趣。 如果你看一下standard library，就会发现“两个列表是相等的，如果它们的头是相等的，它们的尾是相等的”。 consCong2 : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
x = y -> xs = ys -> x :: xs = y :: ys
consCong2 Refl Refl = Refl 我们也可以证明另一个方向 consCong2' : {x : a} -> {xs : List a} -&g
浏览 15提问于2019-09-12得票数 1
回答已采纳
目前，我在使用随nixpkg一起安装的Idris包时遇到了一些问题，该包位于依赖它的另一个Idris包中。这两个包都已经在Debian系统上进行了测试，所以问题不在于Idris代码本身，而在于它们在NixOS系统上的安装方式。我相信我可以通过调用nix-env -f math.nix -i idris_math成功安装第一个包，其中math.nix的定义如下：
with import <nixpkgs> { };
stdenv.mkDerivation rec {
name = "idris_math";
idris = haskellPackages.i
浏览 0提问于2017-03-18得票数 3
2回答
Idris向量与链表
、、、
Idris在向量的掩护下做了什么优化吗？因为从外观上看，Idris向量只是一个已知大小的链表(编译时已知)。实际上，一般来说，您似乎可以表示以下等价性(我猜在语法上有一点)：
Vector : Nat -> Type -> Type
Vector n t = (l: List t ** length l = n)
因此，虽然这在防止距离误差方面很好，但向量的真正优势(在传统术语的用法中)是在性能方面，特别是在O(1)随机访问方面。idris向量似乎不支持这种功能(如何编写索引函数以获得这种性能？)
假设在引擎盖下没有魔法(就像Nat一样)来重新配置Vector，Idris中是否
浏览 3提问于2014-12-18得票数 21
回答已采纳
我编写了一个函数doSomething，它使用一个打开或关闭的括号并返回相应的Int。
doSomething : (c : Char) -> {auto isPar : c == '(' || c == ')' = True} -> Int
doSomething '(' {isPar = Refl} = 1
doSomething ')' {isPar = Refl} = -1
使用isPar时，我希望确保只有括号和其他字符才能传递给doSomething。但伊德里斯抱怨道：
Error: doSomething
浏览 10提问于2022-05-04得票数 3
3回答
我只是在想，是否有可能在Idris，Agda，Coq和类似的地方推导出教会编码的Nat类型。注意，这与在CoC (众所周知是不可能的)上做这件事不同，因为我们对这些元素有更多的表现力(例如，我们能够提取Sigma的第二个元素)。
下面是关于Idris的一个糟糕的证明草图(有很多语法问题)：
CN : Type
CN = (t : Type) -> t -> (t -> t) -> t
CS : CN -> CN
CS n t z s = s (n t z s)
CZ : CN
CZ t z s = z
ind :
(p : CN -> Type)
浏览 1提问于2018-01-12得票数 7
回答已采纳
1回答
我是伊德里斯的新手。我需要创建一个描述有界数字的数据。因此，我使用这样的构造函数创建了这样的数据：
data BoundedDouble : (a, b : Double) -> Type where
MkBoundedDouble : (x : Double) ->
{auto p : a <= x && x <= b = True} ->
BoundedDouble a b
它似乎在a和b之间创建了一个b。下面是一个简单的使用示例：
test : Bound
浏览 0提问于2016-05-31得票数 2
回答已采纳
在下面的代码中，Idris报告了countSingleton_rhs非常复杂的类型(这是试图解决列表中“软件基础”一章中的一个练习)。该类型包括一个以以下为核心的复杂表达式：case decEq x x of ...。
module CountSingleton
data NatList : Type where
Nil : NatList
(::) : Nat -> NatList -> NatList
-- count occurrences of a value in a list
count : (v : Nat) -> (s : NatList) -&g
浏览 1提问于2019-07-16得票数 2
回答已采纳
我想把一个向量划分成两个新的向量。
我们不能知道单个向量的长度，但是结果向量的和必须等于参数。我试图按以下方式捕获此属性：
partition : (a -> Bool) -> Vect (m+n) a -> (Vect m a, Vect n a)
partition p [] = ([], [])
partition p (x::xs)
= let (ys,zs) = partition p xs
in case p xs of
True => (x::ys, zs)
False => (ys, zs)
但是Idris报告(指向“分区
浏览 5提问于2014-05-05得票数 5
回答已采纳
我发现Nat的Nat函数是用实现的。
total plus : (n, m : Nat) -> Nat
plus Z right = right
plus (S left) right = S (plus left right)
我想知道是否有特别的理由不对第二个论点进行模式匹配，就像下面这样：
total plus : (n, m : Nat) -> Nat
plus Z right = right
plus left Z = left
plus (S left) right = S (plus left right)
正如我目前所看到
浏览 0提问于2018-03-18得票数 3
回答已采纳
我在试着让伊德里斯模式发挥作用。我正在使用来自和的HEAD。每当我执行C (idris-load-file)时，我就会得到这个错误。
Debugger entered--Lisp error: (file-error "make client process failed" "connection refused" :name "Idris Ideslave" :buffer "*idris-connection*" :host "127.0.0.1" :service 0 :nowait nil)
make-
浏览 2提问于2015-03-13得票数 3
回答已采纳
1回答
import Data.Vect
import Data.Vect.Quantifiers
sameKeys : Vect n (lbl, Type) -> Vect n (lbl, Type) -> Type
sameKeys xs ys = All (uncurry (=)) (zip (map fst xs) (map fst ys))
g : {xs,ys : Vect n (lbl, Type)} -> sameKeys xs ys -> map (\b => fst b) xs = map (\b => fst b) ys
g {xs = [
浏览 1提问于2017-10-04得票数 3
回答已采纳
1回答
我对Idris (和依赖类型)非常陌生。我试着写一个程序来检查一个字符串是否是非回文。为此，我决定计算字符串的长度，并计算
q,r = (strlen `div` 2, strlen `mod` 2)
然后按如下方式拆分字符串：
lhalf,rhalf = (substr 0 (q+r) str, substr (q-r) (q+r) str)
这可以同时处理奇数和偶数长度的字符串。问题是Idris需要证明r<q，因为q和r都是Nat。
我的问题是:我如何表达r的事实？
下面是我的代码的完整示例：
module Main
isPalindrome : (str : String) -&
浏览 2提问于2017-10-01得票数 0
1回答
我希望在编译时加载(二进制)文件，并将其存储在类型的toplevel变量中：
module FileProvider
import Data.Bits
import Data.Bytes
import Data.Buffer
%default total
export
loadImage : String -> IO (Provider Bytes)
loadImage fileName = do
Right file <- openFile fileName Read
| Left err => pure (Error $ show err)
浏览 1提问于2018-04-28得票数 1
回答已采纳
2回答
“建筑微积分中的反思？”
、、、、
在具有类型扩展的语言(如Agda、Idris或Haskell )中，有一种=类型，如下所示
data a :~: b where
Refl :: a :~: a
a :~: b意味着a和b是相同的。
这种类型是否可以在或 (即基于构造演算的编程语言)中定义？
浏览 5提问于2016-03-23得票数 10
回答已采纳
我有一个例子
o : Type
Hom : o -> o -> Type
Id : (a : o) -> Hom a a
Comp : Hom a b -> Hom b c -> Hom a c
IdRight : (f : Hom a b) -> Comp f (Id b) = f
IdLeft : (f : Hom a b) -> Comp (Id a) f = f
Assoc : (f : Hom a b) ->
(g : Hom b c) ->
(h : Hom
浏览 0提问于2015-07-02得票数 1
我正在做Idris中9.1节中的练习2，我不知道如何填补最后一个漏洞(见下面的notInTail )。
我读过的答案，但我被困在了另一个地方。
data Last : List a -> a -> Type where
LastOne : Last [value] value
LastCons : (prf : Last xs value) -> Last (x :: xs) value
notInNil : Last [] value -> Void
notInNil LastOne impossible
notInNil (LastCons _
浏览 0提问于2019-05-14得票数 0
回答已采纳
我目前正在尝试下载和使用Idris for Atom，并使用它的编辑器。我从那里下载了Hackage，然后在我的计算机上安装了idris，然后在atom上安装了idris包，当我在程序中输入类似idris应该突出显示的内容时，但是当我输入检查时，我得到了两个错误：“无法找到idris可执行文件:无法在”Idris“和”idris编译器被关闭或崩溃:它(可能)被错误代码：-2“崩溃。
浏览 1提问于2018-03-12得票数 0
回答已采纳
为什么Idris要求函数按照其定义和用mutual声明的相互递归的顺序显示
我希望Idris执行函数之间的第一次依赖分析，并自动重新排序。我一直相信Haskell会这么做。为什么在伊德里斯不可能这样做？
浏览 3提问于2014-11-01得票数 14
回答已采纳
2回答
我对Idris非常陌生，我正在尝试捕捉基本的概念和语法。
即使这听起来可能毫无意义，但我正在尝试定义一个half函数，它将自然值减半。
我想提出这样的建议：
half : (n : Nat) -> (k : Nat) -> (n = k + k) -> (k : Nat)
但当然不管用了。具体而言，我得到：
错误:预期:依赖类型签名
-> (k : Nat) -> (n =k+ k) -> (k : Nat)
有可能吗？
谢谢。
浏览 1提问于2016-11-30得票数 4
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
实时音视频
对象存储
即时通信 IM活动推荐
腾讯云开发者
