Equational reasoning in Racket

This post is an excerpt that will be included in my final Master’s thesis, but I decided it is interesting enough to post it on its own.

We will define a few of Peano’s axioms together with a procedure for substitution in equations so that we can prove some theorems using this system.

We start with some basic Peano definitions:

(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))))

Namely:

1. zero is a constant with the symbol z
2. succ is a procedure that takes a single argument x and returns a list where x is prepended with the symbol s . This is the successor, e.g. (succ zero) evaluates to '(s z)
3. add-1 is a procedure that takes a parameter a and returns an equation '(= (+ a zero) a . This is basically
4. add-2 is a procedure that takes two parameters a and b and returns an equation '(= (+ a (succ b)) (succ (+ a b))) . This is

We proceed by defining procedures to work upon equations:

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

In this case, we defined eq-refl to construct equations of the form , together with procedures for taking the left and the right side of an equation.

Next, we define the (very simple! (no support for free/bound vars)) algorithm for equational substitution.

(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))))))

A couple of more helper procedures:

(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))

Finally, a theorem is valid if both sides of an equation are equal.

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

An example proof:

(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)

This proof defines steps where in each step we transform the given theorem (what we want to prove) by using an inference rule. Finally, the last transformation step2 will be returned. In this case, (valid-theorem? (prove-theorem)) will return true.

The same proof in Coq, except that instead of using our own subst we use Coq’s machinery:

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.

We showed a minimal system for constructing proofs in a Lisp, in which equations can be manipulated. In practice, Coq is much more convenient for more complex proofs, but this was nevertheless an interesting exercise.