Agda学习笔记1

技术分享 3年前 (2022-11-05) 0 999+

关注

Agda学习笔记1

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的东西带入原式

cong

cong 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 = ff 0 < (suc y) = tt (suc x) < (suc y) = x < y (suc x) < 0 = ff _=ℕ_ : ℕ → ℕ → 𝔹 0 =ℕ 0 = tt suc 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) =      begin         suc 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 ≡ false n≮n zero = refl n≮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

发表评论