from Programming Language Theory and its Implementation

prover.clj

(ns
    ^{:doc
      "Simple Theorem Prover 'Programming Language Theory and its Implementation' Michael J.C. Gordon"
      :author "Kenichi Kobayashi"}
  prover
  (:use [clojure.test])
  (:require [clojure.walk :as cw]))

(def constant #{'+ '- '< '<= '> '>= '* '= 'T 'F 'DIV 'not 'and 'or 'implies})

(defmacro third [x] `(first (rest (rest ~x))))

(defmacro variable? [x] `(not (or (nil? ~x) (number? ~x) (contains? constant ~x))))

(defn elem? [exp] (or (not (coll? exp)) (= exp '())))

(defn ^{:arglists '([pattern expression map-of-substitutions])}
  matchfn [pat exp sub]
  (if (elem? pat)
    (if (and (not=  pat '()) (variable? pat)) 
      (if (contains? sub pat)
	(if (= (sub pat) exp)
	  sub
	  (throw (Exception.)))
	(assoc-in sub (list pat) exp))
      (if (= pat exp) sub (throw (Exception.))))
    (recur
     (rest pat)
     (rest exp)
     (matchfn (first pat) (first exp) sub))))

(defn match [pat exp]
  (try (matchfn pat exp nil) (catch Exception e 'fail)) )

(def ^{:doc "trueの時にはrewrite1は等式の変換結果を表示する"}
  *rewrite-flag* true)

(defn ^{:doc "等式の左辺と式を比較して同一の項の対応を取得し、変換した右辺を返す"
	:arglists '([equation expression])}
  rewrite1 [eqn exp]
  (let [l (first eqn)
	r (third eqn)]
    (let [sub (match l exp)]
      (if (= sub 'fail)
	exp
	(do
	  (if *rewrite-flag*
	    (println (cw/prewalk-replace sub eqn)))
	  (cw/prewalk-replace sub r))))))

(defn ^{:doc "複数の等式を受取り、変換した式を返す"}
  rewrite [eqns exp]
  (reduce #(rewrite1 %2 %1) exp eqns))

(defmacro
  ^{:doc "test if expression is the form of implies" }
  imp? [exp]
  `(and (coll? ~exp)
	(= (count ~exp) 3)
	(= (second ~exp) ~''implies)))

(defmacro mk-imp [p q]
  `(list ~p ~''implies ~q))

(defmacro antecedant [exp] `(first ~exp))

(defmacro consequent [exp] `(third ~exp))

(defn ^{:doc "recursively substitute expression with implies rule" }
  imp-subst-simp [exp]
  (if (imp? exp)
    (let [a (antecedant exp)
	  c (consequent exp)]
      (mk-imp a (cw/prewalk-replace {a 'T} c)))
    exp))

(defmacro
  ^{:doc "test if expression is the form of equation" }
  eqn? [exp]
  `(and (coll? ~exp)
	(= (count ~exp) 3)
	(= (second ~exp) ~''=)))

(defn imp-and-simp [exp]
  (if (and (imp? exp) (eqn? (antecedant exp)))
    (let [a (antecedant exp)
	  c (consequent exp)]
      (mk-imp a (cw/prewalk-replace {(first a) (third a)} c)))
    exp))

(defn imp-simp [exp]
  (imp-and-simp (imp-subst-simp exp)))

(deftest test-variable?
  (is (= false (variable? 1)))
  (is (= false (variable? 'and)))
  (is (= false (variable? nil)))
  (is (= true (variable? 'x))))

(deftest test-matchfn
  (is (= '{z 3, x 1} (matchfn '(x 2 z) '(1 2 3) nil)))
  (is (= '{z 3, x 1} (matchfn '(x 2 z) '(1 2 3) '{x 1})))
  (is (= '{y 1, x 3, z 3} (matchfn '((x + y) * (z * y)) '((3 + 1) * (3 * 1)) '{z 3})))
  (is (= '{y 1, x x, z x} (matchfn '((x + y) * (z * y)) '((x + 1) * (x * 1)) '{z x}))))

(deftest test-match
  (is (= '{y 2, x 1} (match '(x + y) '(1 + 2))))
  (is (= 'fail (match '(x + x) '(1 + 2))))
  (is (= 'fail (match '(x * y) '(1 + 2)))))

(deftest test-rewrite1
  (is (= '(1 * 2) (rewrite1 '((x + 0) = x) '((1 * 2) + 0))))
  (is (= '((1 * 2) * 0) (rewrite1 '((x + 0) = x) '((1 * 2) * 0)))))

(deftest test-rewrite
  (is (= 'X (rewrite '(((x + 0) = x) ((x * 1) = x)) '((X * 1) + 0)))))

(deftest test-mk-imp
  (is (= '(x implies y) (mk-imp 'x 'y))))

(deftest test-antecedant
  (is (= 'x (antecedant '(x implies y)))))

(deftest test-consequent
  (is (= 'y (consequent '(x implies y)))))

(deftest test-imp?
  (is (= false (imp? nil)))
  (is (= false (imp? '())))
  (is (= false (imp? '(x imp y))))
  (is (= true (imp? '(x implies y))))
  (is (= false (imp? '(x implies)))))

(deftest test-imp-subst-simp
  (is (= '(P implies T) (imp-subst-simp (mk-imp 'P 'P))))
  (is (= '(P implies (T and Q)) (imp-subst-simp (mk-imp 'P '(P and Q))))))

(defn repeat-apply [f exp]
  (let [exp1 (f exp)]
    (if (= exp exp1)
      exp
      (recur f exp1))))

(defn depth-imp-simp [exp]
  (cw/postwalk
   (fn [x] (imp-simp x))
   exp))

(deftest test-depth-imp-simp
  (is (= '((x = 1) implies ((y = 1) implies (1 = z)))
	 (depth-imp-simp '((x = 1) implies ((y = x) implies (y = z)))))))

(defn top-depth-rewrite [eqns exp]
  (cw/prewalk
   (fn [x] (rewrite eqns x))
   exp))

(defn depth-rewrite [eqns exp]
  (cw/postwalk
   (fn [x] (rewrite eqns x))
   exp))

(deftest test-top-depth-rewrite
  (is (= '(1 < 2)
	 (top-depth-rewrite
	  '(((not (x >= y)) = (x < y)) ((x >= y) = ((x = y) or (x > y))))
	  '(not (1 >= 2))))))

(defn prove [eqns exp]
  (repeat-apply
   (fn [x] (top-depth-rewrite eqns (depth-imp-simp x)))
   exp))

(def logic
  '(
    ((T implies X) = X)
    ((F implies X) = T)
    ((X implies T) = T)
    ((X implies X) = T)
    ((T and X) = X)
    ((X and T) = X)
    ((F and X) = F)
    ((X and F) = F)
    ((X = X) = T)
    (((X and Y) implies Z) = (X implies (Y implies Z)))))

(def arithmetic
  '(
    ((X + 0) = X)
    ((0 + X) = X)
    ((X * 0) = 0)
    ((0 * X) = 0)
    ((X * 1) = X)
    ((1 * X) = X)
    ((not (X <= Y)) = (Y < X))
    ((not (X >= Y)) = (Y > X))
    ((not (X < Y)) = (X >= Y))
    (((- X) >= (- Y)) = (X <= Y))
    (((- X) >= Y) = (X <= (- Y)))
    ((- 0) = 0)
    (((X < Y) implies (X <= Y)) = T)
    ((X - X) = 0)
    (((X + Y) - Z) = (X + (Y - Z)))
    (((X - Y) * Z) = ((X * Z) - (Y * Z)))
    ((X * (Y + Z)) = ((X * Y) + (X * Z)))
    (((X + Y) * Z) = ((X * Z) + (Y * Z)))
    (((X >= Y) implies ((X < Y) implies Z)) = T)
    (((X <= Y) implies ((Y < X) implies Z)) = T)
    ((0 DIV X) = 0)
    (((X DIV Y) + Z) = ((X + (Y * Z)) DIV Y))
    (((X - Y) + Z) = (X + (Z - Y)))
    ((2 * X) = (X + X))
    ))

(def facts (concat logic arithmetic))

(deftest test-prove
  (is (= 'T
	 (prove facts
		'(((X = (((N - 1) * N) DIV 2)) and ((1 <= N) and (N <= M)))
		  implies
		  ((X + N) = ((((N + 1) - 1) * (N + 1)) DIV 2)))))))