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

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

比较大小

_<_ : ℕ → ℕ → 

标签：suc,rewrite,笔记,学习,zero,assoc,refl,comm,Agda	

From： https://www.cnblogs.com/lcyfrog/p/16859343.html