1. 首頁 > 生活百科 > >

Agda學習筆記1

生活百科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
  1. \(\_+\_ : ? → ? → ?\)
    zero + n = n
    suc m + n = suc (m + n)
  2. \(\_*\_ : ? → ? → ?\)
    zero * n = zero
    suc m * n = n + (m * n)
  3. \(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，即把

推薦閱讀