Racket中的等式推理探索

本文是即将被纳入我的硕士论文的一个章节，但考虑到其内容的独特性和趣味性，决定将其单独发表。

我们将定义几个皮亚诺公理，以及一个用于方程中替换的过程，以便能够使用这个系统来证明一些定理。

首先，我们从一些基本的皮亚诺定义开始：

```racket
(define zero 'z)
(define (succ x) (list 's x))
(define (add-1 a) (list '= (list '+ a zero) a))
(define (add-2 a b) (list '= (list '+ a (succ b)) (succ (list '+ a b))))
```

具体来说：

1. `zero` 是一个常量，符号为 `z`。
2. `succ` 是一个过程，接受单个参数 `x` 并返回一个列表，其中 `x` 前面加了符号 `s`。这代表后继数，例如 `(succ zero)` 评估结果为 `'(s z)`。
3. `add-1` 是一个过程，接受参数 `a` 并返回一个等式 `'(= (+ a zero) a)`。这基本上表示任何数加上零等于该数本身。
4. `add-2` 是一个过程，接受两个参数 `a` 和 `b` 并返回一个等式 `'(= (+ a (succ b)) (succ (+ a b)))`。这表示任何数加上另一个数的后继数等于这两个数之和的后继数。

接下来，我们定义一些用于处理等式的程序：

```racket
(define (eq-refl a) (list '= a a))
(define (eq-left a) (cadr a))
(define (eq-right a) (caddr a))
```

这里，我们定义了 `eq-refl` 来构造形式为 `a = a` 的等式，同时还定义了提取等式左右两边的程序。

然后，我们定义了一个（非常简单！不支持自由/绑定变量）等式替换算法：

```racket
(define (subst x y expr)
(cond ((null? expr) '())
((equal? x expr) y)
((not (pair? expr)) expr)
(else (cons (subst x y (car expr))
(subst x y (cdr expr))))))
```

另外，我们还需要一些辅助程序：

```racket
(define (rewrite-left eq1 eq2)
(subst (eq-left eq1)
(eq-right eq1)
eq2))

(define (rewrite-right eq1 eq2)
(subst (eq-right eq1)
(eq-left eq1)
eq2))
```

最后，一个定理是有效的，如果等式的两边相等：

```racket
(define (valid-theorem? theorem)
(and (equal? theorem (eq-refl (eq-left theorem)))
(equal? theorem (eq-refl (eq-right theorem)))))
```

一个示例证明如下：

```racket
(define (prove-theorem)
; a + S(0) = S(a)
(define theorem '(= (+ a (s z)) (s a)))
; S(a + 0) = S(a)
(define step1 (rewrite-left (add-2 'a zero) theorem))
; S(a) = S(a)
(define step2 (rewrite-left (add-1 'a) step1))
step2)
```

此证明定义了一系列步骤，在每一步中，我们都通过使用推理规则来转换给定的定理（即我们要证明的内容）。最终，最后一个转换 `step2` 将被返回。在这个例子中，`(valid-theorem? (prove-theorem))` 将返回真值。

同样的证明在Coq中的实现，除了使用我们自己的 `subst` 之外，还利用了Coq的内置机制：

```coq
Axiom add_1 : forall (a : nat), (a = a + 0).
Axiom add_2 : forall (a b : nat), (a + S b = S (a + b)).
Axiom eq_refl : forall (a : nat), a = a.

Theorem theorem (a b : nat) : a + S(0) = S(a).
Proof.
intros.
rewrite (add_2 a 0).
rewrite <- (add_1 a).
apply eq_refl.
Qed.
```

我们展示了一个最小化的Lisp系统，用于构建和操作等式的证明。虽然对于更复杂的证明，Coq更为方便，但这仍然是一个有趣的练习。