;;; -*- Mode: Lisp; Syntax: Common-Lisp; Package: snark-user -*-
;;; File: front-last-example.lisp
;;; The contents of this file are subject to the Mozilla Public License
;;; Version 1.1 (the "License"); you may not use this file except in
;;; compliance with the License. You may obtain a copy of the License at
;;; http://www.mozilla.org/MPL/
;;;
;;; Software distributed under the License is distributed on an "AS IS"
;;; basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See the
;;; License for the specific language governing rights and limitations
;;; under the License.
;;;
;;; The Original Code is SNARK.
;;; The Initial Developer of the Original Code is SRI International.
;;; Portions created by the Initial Developer are Copyright (C) 1981-2002.
;;; All Rights Reserved.
;;;
;;; Contributor(s): Mark E. Stickel .
(in-package :snark-user)
;;; Let L be a nonempty list.
;;; Synthesize a program to compute the FRONT and LAST
;;; of the list where LAST of a list is its last element
;;; and FRONT is the list of all elements except the last.
;;;
;;; The program specification is
;;; (EXISTS (Y Z) (= L (APPEND Y (CONS Z NIL))))
;;; i.e., find Y and Z such that L can be formed by
;;; appending Y (the FRONT of L) and a single element list
;;; containing Z (the LAST of L).
;;;
;;; The appropriate inductive axiom is given explicitly in the axiom
;;; named induction.
;;;
;;; Necessary properties of APPEND, CONS, HEAD, and TAIL are given
;;; in the axioms named append-nil, append-cons, and cons-definition.
;;;
;;; A proof of the query is found and the program
;;; defined by the values found for variables Y and Z
;;; in the specification.
;;;
;;; Resolution and paramodulation (for equality) are the inference
;;; rules used.
(defun front-last-example ()
;; Waldinger program synthesis example 1989-12-14
(initialize)
(use-resolution)
(use-paramodulation)
(use-literal-ordering-with-resolution 'literal-ordering-p)
(use-literal-ordering-with-paramodulation 'literal-ordering-p)
(use-conditional-answer-creation)
(declare-constant 'nil)
(declare-constant 'l)
(declare-function 'head 1)
(declare-function 'tail 1)
(declare-function 'cons 2)
(declare-function 'append 2)
(declare-function 'front 1)
(declare-function 'last 1)
(declare-ordering-greaterp 'l 'nil)
(declare-ordering-greaterp 'head 'l)
(declare-ordering-greaterp 'tail 'l)
(declare-ordering-greaterp 'cons 'head)
(declare-ordering-greaterp 'cons 'tail)
(declare-ordering-greaterp 'append 'cons)
;;(assert '(forall (x) (= x x)))
(assert '(/= l nil)
:name 'l-nonempty)
(assert '(implies (and (/= l nil) (/= (tail l) nil))
(= (tail l) (append (front (tail l)) (cons (last (tail l)) nil))))
:name 'induction)
(assert '(forall (u) (= (append nil u) u))
:name 'append-nil)
(assert '(forall (u v w) (= (append (cons u v) w) (cons u (append v w))))
:name 'append-cons)
(assert '(forall (x) (implied-by (= x (cons (head x) (tail x))) (/= x nil)))
:name 'cons-definition)
(prove '(= l (append ?y (cons ?z nil))) :answer '(values ?y ?z)))
;;; front-last-example.lisp EOF