在 Agda 中定义演绎系统并进行定理证明

Posted on Edited on In

Abstract. 最不想学 FP 的一集《三句话让我写了一晚上形式化验证》。

本文讲如何在 Agda 中定义《数理逻辑与集合论 (1) 命题逻辑》中提到的演绎系统，并形式化验证了文中的几个定理。

好像现在我们的姿势还不太正确，我们确实找到了一种方法来验证一个证明对不对，但是对自己证明定理没有一点帮助（甚至有负贡献）。

初始符号 形成规则 补充定义

这三部分内容可以用 data constructor 来完成。我们这里以 var ℕ 作为变量，然后定义两个构造器 ¬_ 和 _∨_。对于补充定义，可以直接写函数。

1
2
3
4
5
6
7
8
9
10
data Expr : Set where
  var_ : ℕ → Expr
  ¬_ : Expr → Expr 
  _∨_ : Expr → Expr → Expr 

_-→_ : Expr → Expr → Expr
A -→ B = (¬ A) ∨ B

_∧_ : Expr → Expr → Expr
A ∧ B = ¬ ((¬ A) ∨ (¬ B))

公理 变形规则

定义一个 data constructor ⊢_ : Expr → Set，然后里面的内容就是公理和变形规则。代入规则的实现依赖于显参，分离规则和公理是 constructor，置换规则直接由 normalization 完成。

1
2
3
4
5
6
data ⊢_ : Expr → Set where
  A1 : ∀ A     → ⊢ ((A ∨ A) -→ A)
  A2 : ∀ A B   → ⊢ (A -→ (A ∨ B))
  A3 : ∀ A B   → ⊢ ((A ∨ B) -→ (B ∨ A))
  A4 : ∀ A B C → ⊢ ((B -→ C) -→ ((A ∨ B) -→ (A ∨ C)))
  MP : ∀ {A B} → ⊢ A → ⊢ (A -→ B) → ⊢ B

诸定理的形式化验证

这里验证了三段论，自反律，排中律和结合律。

首先一开始我们并没有对格式做过多的思考，只是直接一行流。

1
2
3
4
5
6
7
8
9
10
11
Syl : ∀ (A B C : Expr) → ⊢ ((B -→ C) -→ ((A -→ B) -→ (A -→ C)))
Syl A B C = A4 (¬ A) B C

Refl : ∀ (A : Expr) → ⊢ (A -→ A)
Refl A = MP (A2 A A) (MP (A1 A) ((Syl A (A ∨ A) A)))

EM : ∀ (A : Expr) → ⊢ (A ∨ (¬ A))
EM A = MP (Refl A) (A3 (¬ A) A)

Assoc : ∀ (A B C : Expr) → ⊢ ((A ∨ (B ∨ C)) -→ ((A ∨ B) ∨ C))
Assoc A B C = MP (MP (MP (MP (MP (A3 B C) (MP (MP (MP (MP (A2 B A) (MP (A3 B A) (Syl B (B ∨ A) (A ∨ B)))) (A4 C B (A ∨ B))) (MP (A3 (C) (A ∨ B)) (Syl (C ∨ B) (C ∨ (A ∨ B)) ((A ∨ B) ∨ C)))) (Syl (B ∨ C) (C ∨ B) ((A ∨ B) ∨ C)))) (A4 A (B ∨ C) ((A ∨ B) ∨ C))) (MP (A3 A ((A ∨ B) ∨ C)) (Syl (A ∨ (B ∨ C)) (A ∨ ((A ∨ B) ∨ C)) (((A ∨ B) ∨ C) ∨ A)))) (MP (MP (MP (A2 A B) (MP (A2 (A ∨ B) C) (Syl A (A ∨ B) ((A ∨ B) ∨ C)))) (A4 ((A ∨ B) ∨ C) A ((A ∨ B) ∨ C))) (Syl (A ∨ (B ∨ C)) (((A ∨ B) ∨ C) ∨ A) (((A ∨ B) ∨ C) ∨ ((A ∨ B) ∨ C))))) (MP (A1 ((A ∨ B) ∨ C)) (Syl (A ∨ (B ∨ C)) (((A ∨ B) ∨ C) ∨ ((A ∨ B) ∨ C)) ((A ∨ B) ∨ C)))

可以看到结合律的证明非常阴间。但实际上我自己写起来感觉还是比较顺利，有一套操作流程，可以比较流畅地完成验证的工作：

  • 开一个 Hole，观察要证明的式子，定位到对应的定理。
  • 观察后面的提示文字，如果是 $\text{A}x, \text{Syl}$ 等，直接写 Ax (X1) (X2) ...。如果是分离，写 MP ? (对应的定理)；如果是分离两次，写 MP ? (MP ? (对应的定理))，然后一个一个填。

这样我们得到了一坨没人看得懂的奥力给。

后来经过思考，我们有另一种方法，加长了代码长度，但是基本上符合人类的证明习惯（甚至证明格式），可读性极强。作为例子我们只证明前两个例子。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
Syl : ∀ (A B C : Expr) → ⊢ ((B -→ C) -→ ((A -→ B) -→ (A -→ C)))
Syl A B C = T1 A B C where
    T1 : ∀ (A B C : Expr) → ⊢ ((B -→ C) -→ ((A -→ B) -→ (A -→ C)))
    T1 A B C = A4 (¬ A) B C

Refl : ∀ (A : Expr) → ⊢ (A -→ A)
Refl A = T5 A where
    T1 : ∀ (A : Expr) → ⊢ (A -→ (A ∨ A))
    T1 A = A2 A A

    T2 : ∀ (A : Expr) → ⊢ ((A ∨ A) -→ A)
    T2 A = A1 A

    T3 : ∀ (A : Expr) → ⊢ (((A ∨ A) -→ A) -→ ((A -→ (A ∨ A)) -→ (A -→ A)))
    T3 A = Syl A (A ∨ A) A

    T4 : ∀ (A : Expr) → ⊢ ((A -→ (A ∨ A)) -→ (A -→ A))
    T4 A = MP (T2 A) (T3 A)

    T5 : ∀ (A : Expr) → ⊢ ((A -→ A))
    T5 A = MP (T1 A) (T4 A)

待续内容

可能会研究自然演绎系统的写法。这里难点是集合 $\Gamma$ 的写法。

可能会研究语义相关的内容，证明完备性等。

可能会给奥里给写一个 Parser。