#|
Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Computational Logic, Inc. PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT
IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL Computational Logic, Inc. BE LIABLE TO YOU FOR ANY DAMAGES,
ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#

Event: Start with the initial nqthm theory.

;  This file contains examples that illustrate the use
;  of the new events CONSTRAIN and FUNCTIONALLY-INSTANTIATE.
;  Example 1.  Here we simply introduce three new function symbols of
;  1 argument with no constraints on them.

Conservative Axiom: p-q-r-intro t

Simultaneously, we introduce the new function symbols p, q, and r.

;  Example 2.  Here we introduce the function h, which has the strange
;  property we call ``commutativity2'' and show that one can ``map''
;  with such a function in a primitive recursive way (using pr-h) or
;  by using an accumulator (using pr-ac); but either way one gets the
;  same result.  We then can FUNCTIONALLY-INSTANTIATE this result

;  using times instead of h.

Conservative Axiom: intro-h h (x, h (y, z)) = h (y, h (x, z))

Simultaneously, we introduce the new function symbol h.

Definition: pr-h (l, z) = if l ≃ nil then z

else h (car (l), pr-h (cdr (l), z)) endif

Definition: ac-h (l, z) = if l ≃ nil then z

else ac-h (cdr (l), h (car (l), z)) endif

Theorem: pr-is-ac ac-h (l, z) = pr-h (l, z)

Definition: pr-times (l, z) = if l ≃ nil then z

else car (l) ∗ pr-times (cdr (l), z) endif

Definition: ac-times (l, z) = if l ≃ nil then z

else ac-times (cdr (l), car (l) ∗ z) endif

Theorem: pr-times-is-ac-times ac-times (l, z) = pr-times (l, z)

;  Example 3.  This example is somewhat similar to the last one in
;  spirit.  This time we constrain the function lt to have one of the
;  properties of a simple order, define a sort on top of it, prove the
;  sort correct, and then instantiate the result with lessp for lt.

Conservative Axiom: lt-intro lt (z, v) → (¬ lt (v, z))

Simultaneously, we introduce the new function symbol lt.

Definition: ordered-lt (l) = if listp (l)

then if listp (cdr (l))

then if lt (cadr (l), car (l)) then f

else ordered-lt (cdr (l)) endif else t endif

else t endif

Definition: addtolist-lt (x, l) = if listp (l)

then if lt (x, car (l)) then cons (x, l)

else cons (car (l), addtolist-lt (x, cdr (l))) endif else list (x) endif

Definition: sort-lt (l) = if listp (l) then addtolist-lt (car (l), sort-lt (cdr (l)))

else nil endif

Theorem: ordered-sort-lt ordered-lt (sort-lt (l))

Definition: ordered-lessp (l) = if listp (l)

then if listp (cdr (l))

then if cadr (l) < car (l) then f

else ordered-lessp (cdr (l)) endif else t endif

else t endif

Definition: addtolist-lessp (x, l) = if listp (l)

then if x < car (l) then cons (x, l)

else cons (car (l), addtolist-lessp (x, cdr (l))) endif else list (x) endif

Definition: sort-lessp (l) = if listp (l) then addtolist-lessp (car (l), sort-lessp (cdr (l)))

else nil endif Theorem: ordered-sort-lessp ordered-lessp (sort-lessp (l))

;  Example 4.  We here define the familiar map function, show that it
;  distributes over append, and instantiate the result with a LAMBDA
;  that has a free variable.

Conservative Axiom: fn-intro t

Simultaneously, we introduce the new function symbol fn.

Definition: map-fn (x) = if x ≃ nil then nil

else cons (fn (car (x)), map-fn (cdr (x))) endif

Theorem: map-distributes-over-append map-fn (append (u, v)) = append (map-fn (u), map-fn (v))

Definition: map-plus-y (x, y) = if x ≃ nil then nil

else cons (car (x) + y, map-plus-y (cdr (x), y)) endif

Theorem: map-plus-y-distributes-over-append map-plus-y (append (u, v), z) = append (map-plus-y (u, z), map-plus-y (v, z))

;  Example 5.  Here we follow the lead of Goodstein in his book
;  Primitive Recursive Arithmetic and of McCarthy with his recursion
;  induction.  We show, using FUNCTIONALLY-INSTANTIATE, that the
;  associativity of append can be proved without explicit appeal to
;  induction.  Of course there are inductions hidden all over the
;  place, e.g. in the type-set analysis for true-rec and in the proof
;  of the metatheorem that justifies FUNCTIONALLY-INSTANTIATE.  Still,
;  this is a startling development to those who regard the
;  associativity of append as the first theorem requiring an inductive
;  proof.

Definition: true-rec (x) = if x ≃ nil then t

else true-rec (cdr (x)) endif Theorem: true-rec-is-true true-rec (x)

Definition: app (x, y) = if x ≃ nil then y

else cons (car (x), app (cdr (x), y)) endif

Theorem: assoc-of-app app (app (x, y), z) = app (x, app (y, z))

;  Example 6.  We illustrate that one can prove theorems using
;  CONSTRAIN and FUNCTIONALLY-INSTANTIATE that resemble proofs in
;  first-order predicate calculus with quantifiers.

Conservative Axiom: all-x-p-x-intro all-x-p-x → p (x)

Simultaneously, we introduce the new function symbol all-x-p-x.

Conservative Axiom: all-x-not-p-x-into all-x-not-p-x → (¬ p (x))

Simultaneously, we introduce the new function symbol all-x-not-p-x.

Theorem: all-x-not-p-x-into-converse p (x) → (¬ all-x-not-p-x)

Definition: some-x-p-x = (¬ all-x-not-p-x)

Theorem: all-implies-some all-x-p-x → some-x-p-x

;  Example 7.  We illustrate a CONSTRAIN that expresses that a
;  function is ``fair'' in the sense that it is infinitely often true
;  and false.

Definition: even (x) = if x ≃ 0 then t

elseif x = 1 then false else ¬ even (x − 1) endif Conservative Axiom: fair-intro fair (fair-true-witness (n)) ∧ (¬ fair (fair-false-witness (n))) ∧ (fair-true-witness (n) ≮ n) ∧ (fair-false-witness (n) ≮ n)

Simultaneously, we introduce the new function symbols fair, fair-true-witness, and fair-false-witness.

;  Example 8.  We illustrate the idea of ``stubbing'' functions.  We
;  define interp to call an undefined, but constrained, function num.
;  Later we prove a result about instantiation of interp by
;  FUNCTIONALLY-INSTANTIATE.

Conservative Axiom: num-intro num (x) ∈ N

Simultaneously, we introduce the new function symbol num.

Definition: interp (x) = if x ≄ 0 then x ∗ x

else num (x) endif

Theorem: interp-is-numeric interp (x) ∈ N

Definition: interp2 (x) = if x ≄ 0 then x ∗ x

else x + x endif

Theorem: interp2-is-numeric interp2 (x) ∈ N

;  Example 9.  We here illustrate the fact that add-axioms
;  are correctly tracked.

Definition: p-alias (x) = p (x)

Axiom: even-p-alias even (p-alias (x))

Theorem: even-p even (p (x))

#|
;  Because this step fails, we comment it out.  The failure
;  stems from our having provided a substitution for the
;  apparently irrelevant function q-alias.  However, providing
;  an analogue to q-alias explose the real problem, the necessity
;  of anopther add-axiom.  The key point is that p-alias
;  is not irrelevant when trying to FUNCTIONALLY-INSTANTIATE
;  even-p because p is ancestral in even-p-alias.
(functionally-instantiate even-q nil
  (even (q x))
  even-p
  ((p q)))
|#
;  Example 10.  It is necessary for soundness that we check that
;  the variables in the constraints do not intersect the free variables
;  in the FUNCTIONALLY-INSTANTIATE substitutions.  Otherwise,
;  the following sequence would lead to unsoundness.

Conservative Axiom: pp-intro (y = 0) → (pp = y)

Simultaneously, we introduce the new function symbol pp.

Theorem: pp-is-0 0 = pp

#|
;  Because this last step fails, we comment it out.  Note that if we
;  did not catch this, relieving the constraint would amount to
;  checking merely that (implies (equal y 0) (equal y y)).
(functionally-instantiate anything-is-0 (rewrite)
  (equal 0 y)
  pp-is-0
  ((pp (lambda () y))))
|#
;  Example 11.  Some from ``higher logic.''

Conservative Axiom: fn-commutative fn2 (x, y) = fn2 (y, x)

Simultaneously, we introduce the new function symbol fn2 .

Definition: foldr-fn (lst, r) = if listp (lst) then fn2 (car (lst), foldr-fn (cdr (lst), r))

else r endif

Definition: foldl-fn (lst, r) = if listp (lst) then foldl-fn (cdr (lst), fn2 (r, car (lst)))

else r endif

Definition: reverse (x) = if listp (x) then append (reverse (cdr (x)), list (car (x)))

else nil endif

Theorem: foldl-is-foldr foldr-fn (lst, r) = foldl-fn (reverse (lst), r)

Theorem: times-add1 (x ∗ (1 + y)) = (x + (x ∗ y))

Theorem: times-comm (x ∗ y) = (y ∗ x)

Definition: foldr-times (lst, r) = if listp (lst) then car (lst) ∗ foldr-times (cdr (lst), r)

else r endif

Definition: foldl-times (lst, r) = if listp (lst) then foldl-times (cdr (lst), r ∗ car (lst))

else r endif

Theorem: foldl-times-is-foldr-times foldr-times (lst, r) = foldl-times (reverse (lst), r)

Index

ac-h, 2 ac-times, 2 addtolist-lessp, 3 addtolist-lt, 3 all-implies-some, 5 all-x-not-p-x, 5 all-x-not-p-x-into, 5 all-x-not-p-x-into-converse, 5 all-x-p-x, 5 all-x-p-x-intro, 5 app, 5 assoc-of-app, 5

even, 5, 6 even-p, 6 even-p-alias, 6

fair, 6 fair-false-witness, 6 fair-intro, 6 fair-true-witness, 6 fn, 4 fn-commutative, 8 fn-intro, 4 fn2, 8 foldl-fn, 8 foldl-is-foldr, 8 foldl-times, 8 foldl-times-is-foldr-times, 8 foldr-fn, 8 foldr-times, 8

h, 2

interp, 6 interp-is-numeric, 6 interp2, 6 interp2-is-numeric, 6 intro-h, 2

lt, 2, 3 lt-intro, 2 map-distributes-over-append, 4 map-fn, 4 map-plus-y, 4 map-plus-y-distributes-over-appe

nd, 4

num, 6

num-intro, 6

ordered-lessp, 3, 4

ordered-lt, 3

ordered-sort-lessp, 4 ordered-sort-lt, 3

p, 5, 6 p-alias, 6 p-q-r-intro, 1 pp, 7 pp-intro, 7 pp-is-0, 7 pr-h, 2 pr-is-ac, 2 pr-times, 2 pr-times-is-ac-times, 2

reverse, 8

some-x-p-x, 5 sort-lessp, 3, 4 sort-lt, 3

times-add1, 8 times-comm, 8 true-rec, 4, 5 true-rec-is-true, 5