如何证明2在Idris中是素数？

文章/答案/技术大牛

发布

1回答

proof、idris

我现在是Idris的初学者，所以我想寻求帮助。data DividesNat : (a : Nat) -> (b : Nat) -> Type where ConsPrime : LTE 2 p -> ((d : Nat) ->DividesNat p d -

浏览 17提问于2020-03-28得票数 2

回答已采纳

1回答

如何让Idris自动证明两个值不相等？

proof、idris

如何让Idris自动证明两个值不相等？p = \Refl impossible f : (x

浏览 1提问于2017-09-30得票数 8

回答已采纳

1回答

这个问题最简单的例子(但不是我能展示的唯一例子)是:假设我得到一个更高阶的函数f : (a -> b) -> c。我想证明f = (\g => f (\x => g x))。在我自己的推理中，它应该非常简单:只需应用两次eta等价(一次在内部，然后在外部)。如果我想证明f = (\x => f x)，一个简单的Refl就足够了:这让我想到"Idris知道eta等价“。在这一点上，我尝试使用rewrite，但找不到在(\g =&g

浏览 63提问于2019-10-23得票数 0

回答已采纳

2回答

如何证明一种类型的布尔不等式在Idris中是无人居住的？

dependent-type、idris

我想知道如何证明(So (not (y == y)))是Uninhabited的一个实例，但我不确定该怎么做。它在Idris中是可证明的，还是由于y的一个奇怪的Eq实现的可能性而不可证明？

浏览 13提问于2017-07-02得票数 3

回答已采纳

1回答

Idris案例/归纳策略

algebraic-data-types、idris、formal-verification

它们是在Idris 0.9.14中实现的，我成功地使用了induction作为一些证明。但是，它们只适用于某些库类型；例如，Vect支持它们，而几乎同构的All不支持它们： -Main.h2> induction ys1 INTERNAL ERROR: induction needs anPlease consider reporting at https://github.com/idris-lang/Idris<

浏览 1提问于2014-12-11得票数 3

回答已采纳

2回答

Agda和Idris的区别

agda、type-theory、idris

我开始深入研究依赖类型编程，并发现Agda和Idris语言最接近Haskell，所以我从那里开始。Idris有类似于Haskell的类型类，而Agda使用实例argumentsIdris包括一元和应用符号，它们似乎都有某种可重新绑定的语法，尽管不能真正确定它们是否相同。

浏览 75提问于2012-02-28得票数 181

回答已采纳

1回答

idris中列表的简单等式证明(证明xs ++ [x] = ys ++ [y] -> x=y -> xs = ys)

idris、dependent-type、theorem-proving

我正在学习idris，并且对证明列表的性质非常感兴趣。如果你看一下standard library，就会发现“两个列表是相等的，如果它们的头是相等的，它们的尾是相等的”。: List b} ->consCong2' Refl Refl = Refl 或者更明确地说，我们可以在方程的两边放下头来得到证明consCong2' pr

浏览 15提问于2019-09-12得票数 1

回答已采纳

1回答

如何在向量长度上说服Idris

idris、dependent-type

刚开始在Idris (如果它重要的话是Idris 2)，并偶然发现这个问题。我正在尝试实现一个函数，该函数返回所有Fibonacci数的向量，直到给定的n。我知道我需要向Idris证明fibs k的长度至少为2，但我无法理解如何做到这一点，以及为什么在现有定义中不明显。对我来说，看起来fibs (S k)中的fibs (S k)肯定是>= 1，因为否则fibs Z或fibs

浏览 3提问于2020-04-06得票数 1

回答已采纳

1回答

为什么Idris中的特殊形式的cong无法进行类型检查？

types、proof、idris、dependent-type

cong0 : {f : Nat -> Nat} -> a + Z = a -> f (a + Z) = f a在Idris 1中，我得到了 a plus a 0Can't

浏览 14提问于2021-05-21得票数 1

1回答

如何证明相等是不可能的

coq、idris

1 subgoalH : TApp a b = aFalse (其中TApp是一个构造函数) 在Idris中，可以用\Refl => impossible来证明这一点，但我还没有设法在Coq中为它编写任何证明。有没有简单的方法来证明这一点？

浏览 16提问于2019-04-01得票数 1

回答已采纳

1回答

在Idris中，我是否可以证明自由定理，例如“t -> t”型t‘的唯一(全)函数是’is‘？

idris、parametric-polymorphism、free-theorem

例如，类型为forall t. t -> t的唯一总函数是标识函数id。%default total GenericEndomorphismid_is_the_on

浏览 5提问于2017-05-27得票数 13

1回答

Idris中产品的模式匹配

pattern-matching、idris

定义 ZZ : TypeZZ_greater_than_zero (Z, Z)

浏览 16提问于2020-03-26得票数 1

1回答

Idris的自定义证明策略

theorem-proving、idris

如果我正确理解它(主要是从applyTactic函数的存在)，就有可能为Idris中的定理证明器编写自定义策略。我可以用哪些(或哪里)例子来学习如何做到这一点？

浏览 1提问于2014-04-13得票数 7

回答已采纳

1回答

如何在Idris* 1.3.2中使用归纳？*

idris

我正在学习Idris，特别是我想学习如何证明陈述。当然，所有练习中最愚蠢的是自然数之和的结合性，我对理论和我将使用的证明风格(第一次论证和重写归纳)很满意，但由于教程中使用的Idris版本和我的版本(1.3.2)之间可能存在一些不兼容性，我陷入了困境。hole_2 intros rewrite plusAssoc' k c r

浏览 2提问于2019-08-20得票数 1

回答已采纳

2回答

在Idris中是否支持正则表达式？

regex、idris

我在Idris文档中没有看到正则表达式，有没有以某种(最好是可移植的)方式支持它？或者这是有计划的？

浏览 0提问于2015-03-22得票数 2

1回答

我能证明(s : Stream a) -> (头s :：尾s= s)在Idris中吗？

lazy-evaluation、idris

下面的Idris证明没有打打字机。hts : (s : Stream a) -> (head s :: tail s = s)我得到的错误是： and对于非空的Vect的打字机也有类似的证明我的工作理论是，Idris不喜欢简化Delay内

浏览 3提问于2018-01-03得票数 6

3回答

依赖于其备选方案排序的函数的证明

pattern-matching、dependent-type、idris、theorem-proving

在Haskell有相当多的经验，我最近才开始使用Idris来证明定理。这是一个很小的例子，说明了我在试图证明相当简单的语句时遇到的一个问题。Specifically: n test nle

浏览 1提问于2016-06-29得票数 4

回答已采纳

3回答

安装Idris2时Chez方案的实时路径错误

macos、idris、chez-scheme

到目前为止我所做的是输入check花了一些时间，然后它开始使用Chez做一些事情以下是错误发生前的最后几行输出

浏览 5提问于2020-05-03得票数 1

回答已采纳

1回答

无法使用IdrisNet2创建简单的二进制数据结构

idris

我使用Idris 0.9.17.1并提交了IdrisNet2的262b746c9a2405e43d1de6a48de44ac2fd19932。putStrLn "hello" Can't solve goal 问题到底是什么，我该如何解决呢我猜我需要向编译器证明16大于0，但我不知道如何在Idris中这样做，

浏览 4提问于2015-04-03得票数 3

回答已采纳

1回答

如何通过自定义Idris* FFI传递函数？*

idris

我正试图为我的编码元实现FFI部分，虽然传递像Int这样的值是可行的，但我最大的问题是如何传递函数。function twice(f, x) {}twice : (Int -> Int) -> Int -JS中获得的。{auto fty : FTy f [] ty}

浏览 2提问于2020-03-15得票数 2

点击加载更多