; ----- micro verifieur de preuves par induction
;       de proprietes de programmes lisp (TRES pur)
;                                        d'apres pg

(lib evalsym.vlisp)

(df theo (l)
  (prove l 0))

; ex: (theo (p m n) = (p n m))

(de prove (th n ;; thh)         ; th = (* = **)
  (pstar (nconc [n 'prove] th))
  (cond
    ((eq (setq thh (reduce th)) t))
    ((equal th thh) (command))
    (t (prove thh (1+ n))))
  (pstar [n 'proved]))

(de pstar (l)
  (prin1 '**)
  (apply 'print l))

(de command (;; com pat remp nboc)
  (print "command ?")
  (setq com (read))
  (selectq (car com)
    (induct (cond ((eq (cadr com) 'list)
                   (listinduct (caddr com) th))
                  ((eq (cadr com) 'num)
                   (numinduct (caddr com) th))
                  (t (print "wrong type")
                     (command))))
    (indhyp (setq nboc (cadr com))
            (if (eq (caddr com) '->)
                (setq pat (car ih) remp (caddr ih))
                (setq pat (caddr ih) remp (car ih)))
            (prove (useindhyp th) (1+ n)))
    (gen    (prove (let ((th th) (lsub (cdr com)))
                     (if lsub
                         (self (subst (nextl lsub) (nextl lsub) th)
                               lsub)
                         th))
                    (1+ n)))
    (look (print (eval (cadr com))) (command))
    (t (print "unknown command")(command))))

(de reduce (thh ;; x y)
  (setq x (symeval (car thh) nil)
        y (symeval (caddr thh) nil))
  (pstar ['reduit 'a  x '=  y])
  (or (equal x y) [x '= y]))

(de listinduct (var ih)         ; ih = hypothese d'induction
  (pstar ['base])
  (prove (subst nil var ih) (1+ n))
  (pstar ['step])
  (prove (subst ['cons (gensym) var] var ih) (1+ n)))

(de numinduct (var ih)
  (pstar ['base])
  (prove (subst 0 var ih) (1+ n))
  (pstar ['step])
  (prove (subst ['1+ var] var ih) (1+ n)))

(de useindhyp (th) (cond
  ((atom th) (if (neq th pat) th
                 (decr nboc)
                 (if (= nboc 0) remp th)))
  ((equal th pat) (decr nboc)
                  (if (= nboc 0) remp
                      [(useindhyp (nextl th)) . (useindhyp th)]))
  (t [(useindhyp (nextl th)) . (useindhyp th)])))