也可以用 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，即把+assoc' y x (x * y) 换成 sym ( +assoc y x (x * y) )
乘法结合律精简的证明：
*-assoc : (x y z : ?) → (x * y) * z ≡ x * (y * z)*-assoc zero y z = refl*-assoc (suc x) y z rewrite *distribr y (x * y) z | *-assoc x y z = refl一些比较大小n≮n : (n : ?) → n < n ≡ falsen≮n zero = refln≮n (suc x) = n≮n x-- problem 2.2<-antisym : (x y : ?) → x < y ≡ true → y < x ≡ false<-antisym zero (suc y) p1 = refl<-antisym (suc x) (suc y) = <-antisym x y -- problem 2.3<-trichotomy : (x y : ?) → x < y ∨ x =? y ∨ y < x ≡ true<-trichotomy zero zero = refl<-trichotomy zero (suc y) = refl<-trichotomy (suc x) zero = refl<-trichotomy (suc x) (suc y) = <-trichotomy x y【Agda学习笔记1】
经验总结扩展阅读
- 萌新版 xss学习笔记
- 1 JAVA语言学习-面向对象
- MyBatis笔记03------XXXMapper.xml文件解析
- 一百二十 salesforce零基础学习快去迁移你的代码中的 Alert / Confirm 以及 Prompt吧
- 我的Spark学习笔记
- 7000-8000高性价比笔记本排行榜2022-7000-8000值得买的笔记本排行榜
- JVM学习笔记——垃圾回收篇
- 黑莓q5用安装微信的方法a 用黑莓自带的印象笔记手敲的 看不懂的宝宝们在私聊我吧
- 未来两个月小宇宙爆发逆袭黑马 学习运超好的4大星座
- JVM学习笔记——内存结构篇