Jon*_*her 2 agda dependent-type
我从"残酷的Agda简介"中了解到这一点http://oxij.org/note/BrutalDepTypes/
假设我们想要在偶数上定义除以2.我们可以这样做:
div : (n : N) -> even n -> N
div zero p = zero
div (succ (succ n)) p= succ (div n p)
div (succ zero) ()
N是自然数,甚至是以下"命题"
even : N -> Set
even zero = \top
even (succ zero) = \bot
even (succ (succ n)) = even n
data \bot : Set where
record \top : Set where
当你评估表达式div(succ(succ zero))你得到\ p - > succ零这是你所期望的.但是,我不明白的是如何解释\ p.我也不明白代码f:\ bot - > N f = div(succ zero)的意思.据我所知,\ bot暗示A代表任何A ......所以类型是有效的.我想我认为依赖类型将允许我以这样的方式写div:div(succ zero)将更明确地失败类型检查.
任何人都可以提出如何在agda中使用和查看谓词的建议吗？
在p您的例子是,你将(数字证明n),确实是even.如果您想使用您的div功能划分数字,仅提供数字是不够的!Agda通过向您返回另一个函数来表示 - 这个函数使用2的证明even并返回1.
让我们写几个测试来看看它是如何工作的:
test? : ?
test? = div 4 ?
在这种情况下,孔的类型是毫无疑问的?.even 4减少到?两步,所以你可以轻松填写空记录或只是给一个下划线 - 只有一个可能的值,Agda可以填写:
test? = div 4 _
另一方面,当你给它一个奇数时,例如:
test? : ?
test? = div 3 ?
孔的类型减少到?.?是空的类型; 给出这种类型的价值相当于证明你的逻辑中存在矛盾.所以我们被困在这里 - 这正是我们想要的.
现在,你想让它感觉更多......隐含的,当我们尝试给它一个奇数时,可能会引入编译错误.
Agda只能通过统一来填充隐含的东西.虽然统一可以做一些复杂的事情,但有一些问题无法帮助; 猜测证据就是其中之一.如果我们想隐瞒证据,我们必须保持简单.even这是一个很好的例子:我们可以从我们正在划分的数字中完全计算它,并且它?可以返回(可以简单填写)或?(这意味着有些错误).
div-implicit : (n : ?) {p : even n} ? ?
div-implicit n {p} = div n p
偶数也很好:
test? : ?
test? = div-implicit 4
奇数会给出编译错误,请参阅我之前关于此问题的答案.我们得到明亮的黄色,我不知道填写错误:
___10 : ? [ at D:\Agda\SO6.agda:27,9-23 ]
这是一本关于如何通过Agda猜测琐碎证明义务的食谱:
首先,我们需要一个函数来确定参数是否正常.通常,这是一个返回a Bool或的函数Dec.
check : ? ? Bool
接下来,我们将其Bool转换为命题:
-- The Bool is true.
True : Bool ? Set
True true = ?
True false = ?
-- The Bool is false.
False : Bool ? Set
False true = ?
False false = ?
最后,我们可以包含一个隐含的参数,如果参数是正确的,Agda将填写或返回亮黄色:
f : (n : ?) {p : True (check n)} ? ?
如果您发现其中一个参数没有意义,Agda允许您省略函数方程的右侧,可以这么说.从技术上讲,当你写下()一个模式时,你断言任何人都无法提供该类型的参数 - 如果没有人能够用这些参数调用这些函数,为什么还要写右手？考虑一个例子:
f : (m n : ?) ? m ? n ? ?
f zero (suc zero) p = ?
f _ _ _ = ?
是什么类型的p？这证明0 ? 1- 这显然是一个废话,没有人可以打电话f 0 1给出证据0 ? 1.我们有理由更换p与()和离开了右边:
f zero (suc zero) ()
将此应用于div示例:
div (suc zero) p = ?
现在,类型p是?.任何人都无法给出类型的价值?.再说一遍,我们告知Agda这个案子是不可能的:
div (suc zero) ()
现在,那些问号是什么？好处agda-mode是它可以帮助您以合作的方式构建您的程序.当你在?某个地方写作时,你会说agda-mode"我不知道这里发生了什么,让我们一起找出来".
当你通过C-c C-lAgda 检查文件时?,将它们转换为空洞(这些就是{ }0你所看到的).你可以在一个程序中有一个以上的洞,这解释了背后的数字.
现在,我说这些允许你以合作方式建立计划,合作在哪里？你可以通过一些洞来做很多动作.例如,您可以询问其类型(via C-c C-,):
div : (n : ?) ? even n ? ?
div zero p = zero
div (suc (suc n)) p = { }0
div (suc zero) ()
-- Agda information buffer
Goal: ?
————————————————————————————————————————————————————————————
p : even n
n : ?
这三行告诉您,您最终必须写下类型?(目标)的表达以及p类型even n和n类型的范围?.
你甚至可以在洞内写东西,询问你目前写的是什么类型(通过C-c C-.):
div (suc (suc n)) p = {n }0
-- Agda information buffer
Goal: ?
Have: ?
————————————————————————————————————————————————————————————
p : even n
n : ?
当你满意的时候,你可以用你在里面写的任何东西(好吧,只要它有类型的东西)来替换洞C-c C-space.
如果您不关心实现(例如,您正在编写证明并且任何事情都可以),您也可以告诉Agda尝试猜测它C-c C-a.当你有很多琐碎的案例时,这非常有用.
然后是案件分裂.编写函数时,通常需要进行模式匹配以了解有关参数的更多信息.Agda允许您省去手动编写所有这些函数方程式的一些痛苦.
_+_ : (m n : ?) ? ?
m + n = { }0
我们写一个变量,我们想要在一个洞内分割一个案例:
_+_ : (m n : ?) ? ?
m + n = {m }0
按下神奇的C-c C-c瞧瞧:
_+_ : (m n : ?) ? ?
zero + n = { }0
suc m + n = { }1