1

我试图证明以下函数是正确的，并且很难弄清楚，即使它看起来很明显！

(implies (and (listp x)
              (listp y))
         (equal (app (rev x) (rev y))
                (rev (app x y))))

通过这样做，我只需要使用以下函数证明 (app (rev x) (rev y)) 等效于 (rev (app xy))))：

(defunc len (x)
  :input-contract t
  :output-contract (natp (len x))
  (if (atom x)
    0
    (+ 1 (len (rest x)))))

(defunc atom (x)
  :input-contract t
  :output-contract (booleanp (atom x))
  (not (consp a)))

(defunc not (a)
  :input-contract (booleanp a)
  :output-contract (booleanp (not a))
  (if a nil t))

(defunc listp (l)
  :input-contract t
  :output-contract (booleanp (listp l))
  (or (equal l ())
      (consp l)))

(defunc endp (a)
  :input-contract (listp a)
  :output-contract (booleanp (endp a))
  (not (consp a)))

(defunc twice (l)
  :input-contract (listp l)
  :output-contract (listp (twice l))
  (if (endp l)
    nil
    (cons (first l) (cons (first l) (twice (rest l))))))

(defunc app (a b)
  :input-contract (and (listp a) (listp b))
  :output-contract (listp (app a b))
  (if (endp a)
    b
    (cons (first a) (app (rest a) b))))

(defunc rev (x)
  :input-contract (listp x)
  :output-contract (and (listp (rev x)) (equal (len x) (len (rev x))))
  (if (endp x)
    nil
    (app (rev (rest x)) (list (first x)))))

这就是我做另一个的方式（希望是正确的）

(implies (listp y)
         (equal (len (rev (cons x y)))
                (+ 1 (len (rev y)))))

“反向附加东西”

(rev (app (rev y) (rex x))) = (app x y)

(len (rev (cons x y))

= 转速的定义

len (app (rev y) (list x))

= rev 的输出合约

(len (rev (app (rev y) (list x))))

= "反向追加事物"

(len (rev (cons x y))

= rev 的输出合约

(len (cons x y))

= len 的定义

(+ 1 (len y))

= rev 的输出合约

(+ 1 (len (rev y)))
4

0 回答 0