acl2 - acl2 等式推論、等式の証明

Question

私は次の関数が真であることを証明しようとしていますが、非常に明白に見えますが、それを理解するのに苦労しています!

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

= レンの定義

(+ 1 (len y))

= rev の出力コントラクト

(+ 1 (len (rev y)))