Agda学习笔记1 _生活百科

Agda学习笔记1
- 快捷键
  - refl
- Natural Number
  - 自然数集合
  - operations
  - rewrite
  - cong
  - 加法结合律
  - 加法交换律
  - 乘法分配律
  - 比较大小
  - 衍生的一些证明
  - begin-qed
- 作业题
  - 乘法交换律
  - 乘法结合律
  - 一些比较大小

Agda学习笔记1好久没写博客了，诈尸一波。
说句题外话，期中有点小爆炸，开始后悔选实验班了。要读信科的后辈诸君，我劝你选计概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 : 自动填充（一般用不上）

refl表示左右相等
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

rewrite大概是用于递归的一个东西，相当于把rewrite的东西带入原式
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 = reflrewrite加竖线就是从左到右替换
乘法分配律同上

*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，即把