目录
- Agda学习笔记1
- 快捷键
- refl
- Natural Number
- 自然数集合
- operations
- rewrite
- cong
- 加法结合律
- 加法交换律
- 乘法分配律
- 比较大小
- 衍生的一些证明
- begin-qed
- 作业题
- 乘法交换律
- 乘法结合律
- 一些比较大小
- 快捷键
说句题外话,期中有点小爆炸,开始后悔选实验班了 。要读信科的后辈诸君,我劝你选计概A普通班拿4.0 。
开学的时候老是想着多学点东西,现在:绩点绩点绩点
快捷键
- C-c C-l : 加载,把问号转换成goal
- C-c C-f/C-b : 在goal之间切换
- C-c C-, : goal&context
- C-c C-. : goal&context&type
- C-c C-r : refine 有时可以自动填充
- C-c C-c spilt:
- 直接回车:补上变量
- 输入变量:把这个变量解释成所有定义
- C-c C-a : 自动填充(一般用不上)
Natural Number自然数集合data \(?\) : Set where
zero : \(?\)
suc : \(? \rightarrow ?\)
即只能从这两条推出其他的性质
解释一个 ? 变量的时候就会展开成这两个元素
operations
- \(\_+\_ : ? → ? → ?\)
zero + n = n
suc m + n = suc (m + n)
- \(\_*\_ : ? → ? → ?\)
zero * n = zero
suc m * n = n + (m * n)
- \(pred : ? → ?\)
pred 0 = 0
pred (suc n) = n
congcong f : 把 f 添加到左右两边
例:
+0 : ? (y : ?) -> y ≡ y + zero+0 zero = refl+0 (suc y) = cong suc (+0 y)
加法结合律+assoc : ? (x y z : ?) → x + (y + z) ≡ (x + y) + z+assoc zero y z = refl+assoc (suc x) y z rewrite +assoc x y z = refl
就是运用suc对+的结合律加法交换律依旧是利用suc递归...
+suc : ? (x y : ?) → suc x + y ≡ x + suc y+suc zero y = refl+suc (suc x) y rewrite +suc x y = refl +comm : ? (x y : ?) → x + y ≡ y + x+comm zero y = +0 y+comm (suc x) y rewrite +comm x y = +suc y x
也可以用rewrite这样写:+comm : ? (x y : ?) → x + y ≡ y + x+comm zero y = +0 y+comm (suc x) y rewrite +comm x y | +suc y x = refl
rewrite加竖线就是从左到右替换乘法分配律同上
*distribr : ? (x y z : ?) → (x + y) * z ≡ x * z + y * z*distribr zero y z = refl*distribr (suc x) y z rewrite *distribr x y z | +assoc z (x * z) (y * z) = refl
比较大小_<_ : ? → ? →0 < 0 = ff0 < (suc y) = tt(suc x) < (suc y) = x < y(suc x) < 0 = ff_=?_ : ? → ? →0 =? 0 = ttsuc x =? suc y = x =? y_ =? _ = ff_≤_ : ? → ? →x ≤ y = (x < y) || x =? y_>_ : ? → ? →a > b = b < a_≥_ : ? → ? →a ≥ b = b ≤ a
注意相等是 _=?_
衍生的一些证明其实上面的定义不用记 , 反正也会忘
写作业和考试前看看就好了
<-0 : ? (x : ?) → x < 0 ≡ false<-0 0 = refl<-0 (suc y) = refl
-contra : false ≡ true → ?{?} {P : Set ?} → P-contra ()<-trans : ? {x y z : ?} → x < y ≡ true → y < z ≡ true → x < z ≡ true<-trans {x} {0} p1 p2 rewrite <-0 x = -contra p1<-trans {0} {suc y} {0} p1 ()<-trans {0} {suc y} {suc z} p1 p2 = refl<-trans {suc x} {suc y} {0} p1 ()<-trans {suc x} {suc y} {suc z} p1 p2 = <-trans {x} {y} {z} p1 p2
其中 () 代表荒谬匹配,即出现 false==true 时就可以直接写 (),也可以像第一条一样,用大括号加上(必要的)参数之后用定义的 -contra(有点搞不懂原理)=?-refl : ? (x : ?) → (x =? x) ≡ tt=?-refl 0 = refl=?-refl (suc x) = =?-refl x=?-from-≡ : ? {x y : ?} → x ≡ y → x =? y ≡ tt=?-from-≡ {x} refl = =?-refl x
也可以用 refl 替换一个等式begin-qed一种语法 , 如下:
+0 : ? (y : ?) -> y ≡ y + zero+0 zero = refl+0 (suc y) =beginsuc y≡? cong suc (+0 y) ?suc (y + zero)≡??suc y + zero?
<>里的是依据 , 某些根据定义的依据可以不用写(如zero+x=x)作业题乘法交换律惨淡的证明:
+assoc' : ? (x y z : ?) → (x + y) + z ≡ x + (y + z)+assoc' x y z rewrite +assoc x y z = refl*0 : ? (x : ?) → zero ≡ x * zero*0 zero = refl*0 (suc x) = *0 x*suc : (x y : ?) → x + x * y ≡ x * suc y*suc zero y = refl*suc (suc x) y rewrite +assoc x y (x * y) | +comm x y | +assoc' y x (x * y) | *suc x y = refl*-comm : (x y : ?) → x * y ≡ y * x*-comm zero zero = refl*-comm zero (suc y) = *-comm zero y*-comm (suc x) y rewrite *-comm x y = *suc y x
优化:使用 sym x == y -> y == x,即把
推荐阅读
- 萌新版 xss学习笔记
- 1 JAVA语言学习-面向对象
- MyBatis笔记03------XXXMapper.xml文件解析
- 一百二十 salesforce零基础学习快去迁移你的代码中的 Alert / Confirm 以及 Prompt吧
- 我的Spark学习笔记
- 7000-8000高性价比笔记本排行榜2022-7000-8000值得买的笔记本排行榜
- JVM学习笔记——垃圾回收篇
- 黑莓q5用安装微信的方法a 用黑莓自带的印象笔记手敲的 看不懂的宝宝们在私聊我吧
- JVM学习笔记——内存结构篇
- 【lwip】08-ARP协议一图笔记及源码实现