当试图mod : Nat -> (m : Nat) -> Fin m在 Idris上实现一个函数时，我注意到明显的算法不起作用，因为当循环和增加结果时，Idris 不会相信它仍在范围内。这段代码解释了这个问题：
-- (M : Nat) is the modulus, doesn't change
-- (r : Fin M) is the result, increases as you recurse
-- (n : Nat) is the dividend, the recursion stops when it is 0
-- (m : Nat) is the modulus index, when it is Zero, the result loops around
modAux : (M : Nat) -> (r : Fin M) -> (n : Nat) -> …我正在尝试学习 Agda。任何人都可以完成这个证明（如果它在正确的轨道上）或指向我现有的文章？我进行了广泛的搜索。
sum : ? ? ?
sum 0 = 0
sum (suc a) = (suc a) + sum a
prove2*Sumn=n*sucn : (n : ?) ? ((sum n) * 2) ? (n * (suc n))
prove2*Sumn=n*sucn zero = refl
prove2*Sumn=n*sucn (suc a) = {! !}
TL;DR：在 Agda 中，给定a : A和proof : A == B，我可以获得一个元素a : B吗？
在我不断尝试学习 Agda 的过程中，我创建了以下Prime : nat -> Set数据类型，它见证了自然的原始性。
Prime zero = False
Prime (succ zero) = False
Prime (succ (succ n)) = forall {i : nat} -> divides i p -> i <N p -> zero <N i -> i == (succ zero)
where
p = succ (succ n)
这里：
False 是没有构造函数的数据类型；divides a b是一种数据类型，包含k对以下事实的见证a * k = …我想将二进制值加一，但我仍然不太熟悉 agda 中递归的工作原理。
为什么我在这里没有得到正确的输出？
Bin 类型定义
data Bin : Set where
?? : Bin
_O : Bin ? Bin
_I : Bin ? Bin
我的增量函数
inc : Bin ? Bin
inc ?? = ?? I
inc (x O) = ?? I
inc (x I) = (inc x) I
data MinList (min : ?) : Set where
[] : MinList min
_??_?_ : (x : ?) -> min ? x -> MinList x -> MinList min
什么是<< >>意味着什么？
或者是什么意思
_??_?_ : (x : ?) -> min ? x -> MinList x -> MinList min
谢谢
我正在尝试对依赖函数进行证明,而且我遇到了障碍.
所以我们假设我们有一个f-相等的定理
f-equal : ? {A B} {f : A ? B} {x y : A} ? x ? y ? f x ? f y
f-equal refl = refl
我试图证明一个关于依赖函数的平等保存的更普遍的概念,并遇到障碍.即,类型
?-equal : ? {A} {B : A ? Set} {f : {a : A} ? B a} {x y : A} ?
x ? y ? f x ? f y
让编译器不高兴,因为它无法弄清楚fx和fy属于同一类型.这似乎是一个可以修复的问题.是吗？
注意; 使用的等价关系定义如下:
data _?_ {A : Set}(x : A) : A ? Set where
refl : x …我发现了一个方便的功能:
coerce : ? {?} {A B : Set ?} ? A ? B ? A ? B
coerce refl x = x
在使用索引类型定义函数时.在索引在定义上不相等的情况下,i,e,必须使用引理来显示类型匹配.
zipVec : ? {a b n m } {A : Set a} {B : Set b} ? Vec A n ? Vec B m ? Vec (A × B) (n ? m)
zipVec [] _ = []
zipVec {n = n} _ [] = coerce (cong (Vec _) (0?n?0 n)) []
zipVec (x ? xs) (y …作为一种学习经验,我试图在Agda中使用延续传递方式实现经过验证的正则表达式匹配器,基于本文提出的方法.
我有一个像这样定义的正则表达式的类型:
data RE : Set where
? : RE
? : RE
Lit : Char -> RE
_+_ : RE -> RE -> RE
_·_ : RE -> RE -> RE
_* : RE -> RE
还有一个类型,用于证明字符串与RE匹配,如下所示:
data REMatch : List Char -> RE -> Set where
EmptyMatch : REMatch [] ?
LitMatch : (c : Char) -> REMatch (c ? []) (Lit c)
...
ConcatMatch :
(s1 : List Char) (s2 : List Char ) (r1 …对不起我的英语不好.我用谷歌翻译.
是否真的可以证明任意类型(X:Set)？
double-negation : ? X ? ¬ (¬ X)
double-negation = ?
哪里:
data ? : Set where
data ¬_ (X : Set) : Set where
¬-constructor : (X ? ?) ? ¬ X
例如,证明ℕ很简单:
data ? : Set where
zero : ?
suc : ? ? ?
double-negation : ? ? ¬ (¬ ?)
double-negation n =
¬-constructor negation-contradiction
where
negation-contradiction : ¬ ? ? ?
negation-contradiction (¬-constructor ?) = ? n
但更换后?使用X,它不能被选中(由于n型是未知的,因此输入的negation-contradiction …
不小心,我设法让实例搜索成功,但我不明白为什么.
在下面的代码中,为什么test2成功但test1失败(有未解决的元数据和约束)？如何添加? isRelation ?参数来IsSymmetric2帮助？我认为它必须以某种方式与一些metas得到解决,因此允许实例搜索成功,但除此之外,我很有雾.
有人能否说明这里的工作机制？
有一个答案在这里触及我的问题(以下简称"弱点"一节)上,但没有解释出现的解决方法是如何工作的力学.我猜这个问题的答案将帮助我更好地理解这种解决方法.
{-# OPTIONS --show-implicit #-}
record IsSymmetric1 {A : Set} (F : A ? A ? A) (Q : A ? A ? Set) : Set where
field
symmetry1 : ? {x y} ? Q (F x y) (F y x)
open IsSymmetric1 ? … ?
record IsRelation {A : Set} (Q : A ? A ? Set) : Set where
no-eta-equality
record IsSymmetric2 {A …