前言：又到了期末寄，开始匆忙整理下半学期学的agda，果然ddl就是第一生产力，这个交互式证明工具还是挺有意思的虽然有的时候很蠢
Agda是基于Haskell的，所以很多语法和Haskell几乎一致
没有快捷键不会用系列
待补充的地方加问号
C-c C-l : 加载，把问号转换成goal
C-c C-, : goal&context
C-c C-. : goal&context&type
C-c C-r : refine
C-c C-c spilt:
一些框架和理论基础
命题通常是由等式来表示和进行推导（等式理论）
变量和命题都是Set，即一个集合中的元素，Set有等级，表示包含关系
一些语法：大致与haskell相似
{}中的是隐含变量，不一定需要在定义或调用中给出，可由参数推出即可
类型需要声明{A : Set}或者{l} {A : Set l}
要使用变量需要声明类型：(x : A)来声明一个A类型的变量
最基本的等式：refl，反身性，表示等式左右两边全等，即形式可化为完全相同
若所证明的等式to-prove-p已经化为左右全等，则只需写 to-prove-p = refl
如果需要利用别的已知等式p来替换，需要使用rewrite p，表示在要证明的命题中把包含的所有等式p左边的内容换成右边的内容再进行推导
Natural和List的定义都是递归定义的，包括他们的运算
在证明时能直接用的东西只有定义，并且是严格按照定义来（逻辑还是很严谨的，甚至有些过分严谨了）
证明通常是把变量利用递归定义的方式分解为子问题，利用归纳解决
写一个命题需要考虑所有的情况，比如Natural定义中的zero和suc n
一个例子：证明加法结合律
+assoc : (x y z : ℕ) → x + (y + z) ≡ (x + y) + z
+assoc 0 y z = refl
+assoc (suc x) y z rewrite +assoc x y z = refl
也可利用等式理论书写，将左边的式子一步步化为右边的
比用rewrite麻烦，但是在复杂的证明中逻辑更清晰，最后的\qed也显得很爽
语法规则大概是用"≡⟨⟩"来衔接推导，"⟨⟩"里可以不写，表示由定义得到，也可以写这一步的依据
依据的格式大概如下
cong f (x ≡ y) 表示把式子中被f函数包裹的x替换成y
cong-app (∀ x -> f x ≡ g x) f x ≡ g x，表示f和g相同则把f x替换为g x
+-suc : (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc 0 n = refl
+-suc (suc m) n =
begin
suc m + suc n
≡⟨⟩
suc (m + suc n)
≡⟨ cong suc (+-suc m n) ⟩
suc (suc m + n)
∎
Internal Verification
大概就是把一些性质的证明包含在函数定义或类型定义里
基础内容就整理到这里，还有一些进阶的玩法就不赘述了（其实是没学）
但我们已经可以利用它来推导证明接下来的一些计算理论了
标签：Set,suc,定义,笔记,证明,refl,等式,整理,agda From： https://www.cnblogs.com/deaf/p/16994899.html