diff options
Diffstat (limited to 'books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms')
15 files changed, 9649 insertions, 0 deletions
diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/anti-unification.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/anti-unification.lisp new file mode 100644 index 0000000..b5fd366 --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/anti-unification.lisp @@ -0,0 +1,801 @@ +;;; anti-unification.lisp +;;; Definition and correctness of an anti-unification algorithm +;;; A proof of the existence of a greatest lower bound (glb) of two +;;; terms (w.r.t. subsumption). +;;; Created 22-10-99. Last revision: 15-02-2001 +;;; ================================================================= + +#| To certify this book: + +(in-package "ACL2") + +(certify-book "anti-unification") + +|# + +(in-package "ACL2") +(include-book "subsumption") + +;;; ****************************************************** +;;; ANTI-UNIFICATION: DEFINITION AND PROPERTIES. +;;; EXISTENCE OF A GLB OF TWO TERMS W.R.T. SUBSUMPTION. +;;; ****************************************************** + +;;; In this book: +;;; - Definition of anti-unify, a function implementing an +;;; anti-unification algorithm. +;;; - Main properties of anti-unify, stablishing that (anti-unify t1 t2) +;;; is the most particular common generalization of t1 and t2, thus +;;; showing that the set of first order terms (in a given signature) +;;; is a lower semi-lattice w.r.t. subsumption. + +;;; ============================================================================ +;;; 1. Definition of anti-unify-aux +;;; ============================================================================ + +;;; As usual, we will define anti-unification for terms and for list of +;;; terms. This is done by the function anti-unify-aux. An extra +;;; argument phi is needed to take acount of associations of the form +;;; ((s1 . s2) . x), where s1 and s2 are terms s.t. only variables are a +;;; common generalization of them, and x is a variable. We need to store +;;; this associations, since for the same pair of terms the same +;;; variable has to be assigned during the proccess. + + + +;;; The argument phi can be seen as an "injection" from pair of terms to +;;; variables. This injection is built on demmand. That's the role of +;;; the following function. The function returns a multi-value of three: +;;; see the comments below to understand the role of the three +;;; values. Note also the use of assoc-equal. + +(defun anti-unify-injection (p phi) + (declare (xargs :guard (alistp-acl2-numberp phi))) + (let ((found (assoc-equal p phi))) + (if found + (mv (cdr found) phi t) + (let ((y (if (endp phi) 1 (+ 1 (cdar phi))))) + (mv y (cons (cons p y) phi) t))))) + +;;; The function anti-unify-aux + +(defun anti-unify-aux (flg t1 t2 phi) + (declare (xargs :guard (and (term-p-aux flg t1) + (term-p-aux flg t2) + (alistp-acl2-numberp phi)) + :verify-guards nil)) + (if flg + (cond ((or (variable-p t1) (variable-p t2)) + (anti-unify-injection (cons t1 t2) phi)) + ((eql (car t1) (car t2)) + (mv-let (anti-unify-args phi1 bool) + (anti-unify-aux nil (cdr t1) (cdr t2) phi) + (if bool + (mv (cons (car t1) anti-unify-args) phi1 t) + (anti-unify-injection (cons t1 t2) phi)))) + (t (anti-unify-injection (cons t1 t2) phi))) + (cond ((endp t1) (if (eql t1 t2) (mv t1 phi t) (mv nil nil nil))) + ((endp t2) (mv nil nil nil)) + (t (mv-let (anti-unify-cdr phi1 bool1) + (anti-unify-aux nil (cdr t1) (cdr t2) phi) + (if bool1 + (mv-let (anti-unify-car phi2 bool2) + (anti-unify-aux t (car t1) (car t2) phi1) + (if bool2 + (mv (cons anti-unify-car anti-unify-cdr) + phi2 + t) + (mv nil nil nil))) + (mv nil nil nil))))))) +;;; REMARKS: +;;; - Note that the function returns a multi-value with three values: +;;; the anti-unification term, the "injection" and a boolean value to +;;; indicate success or fail. +;;; - Although for terms there is always a glb for two terms (a variable +;;; in the "worst" case), the same is not true for lists of terms. Thus, +;;; we have to distinguish nil as fail for nil as a list of +;;; terms. That's the reason for the third value of the returned +;;; muti-value. + +;;; Guard verification + +(local + (defthm alistp-acl2-numberp-second-anti-unify-aux + (implies (alistp-acl2-numberp phi) + (alistp-acl2-numberp + (second (anti-unify-aux flg t1 t2 phi)))))) + + +(verify-guards anti-unify-aux) + + +;;; An interesting property: anti-unification always suceeds for +;;; terms. For lists of terms, the sucess or failure is independent from +;;; phi. This rule reduces the complexity of the proofs. + +(local + (defthm anti-unify-aux-bool-pair-args + (iff (third (anti-unify-aux flg t1 t2 phi)) + (if flg t (second (pair-args t1 t2)))))) + + + + +;;; OUR GOAL: To prove that the first value of the multi-value returned +;;; by (anti-unify-aux flg t1 t2 phi), when succes, it is a glb of t1 t2 +;;; (under some assumptions about phi). + + + + +;;; ============================================================================ +;;; 2. Definition and properties of pre-anti-unify-aux +;;; ============================================================================ + +;;; INTERESTING REMARK: In a first attempt, we tried to prove the main +;;; properties of anti-unify-aux reasoning about the function definition +;;; (as usual). But it turned out difficult to manage the "incremental +;;; construction of the injection". In particular, we were not able to +;;; proof that the anti-unification is subsumed by any other common +;;; generalization. Thus, we changed our strategy: we defined +;;; pre-anti-unify-aux. In this function we suppose that the injection +;;; phi is already built. Note that anti-unify-aux returns the same term +;;; as pre-anti-unify-aux, whenever the injection finally constructed by +;;; anti-unify-aux is given to pre-anti-unify-aux initially. In this +;;; way, we have an equivalent definition of anti-unification although +;;; less eficcient, because we would need to traverse the terms twice: +;;; one for computing the injection and one for computing the +;;; anti-unification. In contrast, anti-unify-aux does this computation +;;; at the same time. But the main point here is that pre-anti-unify-aux +;;; is much more suitable for reasoning. We first prove the main +;;; properties of pre-anti-unify-aux, then we prove the relation between +;;; pre-anti-unify-aux and anti-unify-aux, and finally we export the +;;; properties of pre-anti-unify-aux to anti-unify-aux. In few words: a +;;; good example of compositional reasoning. + + +;;; ---------------------------------------------------------------------------- +;;; 2.1 Definition of pre-anti-unify-aux +;;; ---------------------------------------------------------------------------- + + +(local + (defun pre-anti-unify-aux (flg t1 t2 phi) + (if flg + (cond ((or (variable-p t1) (variable-p t2)) + (mv (cdr (assoc (cons t1 t2) phi)) t)) + ((eql (car t1) (car t2)) + (mv-let (anti-unify-args bool) + (pre-anti-unify-aux nil (cdr t1) (cdr t2) phi) + (if bool + (mv (cons (car t1) anti-unify-args) t) + (mv (cdr (assoc (cons t1 t2) phi)) t)))) + (t (mv (cdr (assoc (cons t1 t2) phi)) t))) + (cond ((endp t1) (if (eql t1 t2) (mv t1 t) (mv nil nil))) + ((endp t2) (mv nil nil)) + (t (mv-let (anti-unify-cdr bool1) + (pre-anti-unify-aux nil (cdr t1) (cdr t2) phi) + (if bool1 + (mv-let (anti-unify-car bool2) + (pre-anti-unify-aux t (car t1) (car t2) phi) + (if bool2 + (mv (cons anti-unify-car anti-unify-cdr) + t) + (mv nil nil))) + (mv nil nil)))))))) + +;;; REMARK: Note the difference with anti-unify-aux: we assume the +;;; injection phi as a constant association list. + +;;; An analogue property to anti-unify-aux-bool-pair-args: +;;; pre-anti-unification always suceeds for terms. For list of terms, +;;; the sucess or failure is independent from phi. This rule reduces the +;;; complexity of the proofs. + +(local + (defthm pre-anti-unify-aux-bool-pair-args + (iff (second (pre-anti-unify-aux flg t1 t2 phi)) + (if flg t (second (pair-args t1 t2)))))) + + +;;; ---------------------------------------------------------------------------- +;;; 2.2 Main properties of pre-anti-unify-aux +;;; ---------------------------------------------------------------------------- + +;;; We will prove that under some assumptions on phi, +;;; (pre-anti-unify-aux flg t1 t2 phi) computes a glb of t1 and t2, +;;; whenever it exists. + +;;; ············································································ +;;; 2.2.1 Assumptions on phi +;;; ············································································ + +;;; The following function defines the properties we are going to +;;; assume about an injection phi: it has to be an association such that +;;; its co-domain is a list of variables without repetitions and its +;;; domain contains the domain of the association list computed by +;;; anti-unify-aux. We will show that this property is enough to +;;; compute properly the anti-unification of two terms. + +(local + (defun injection-p (phi flg t1 t2) + (and + (alistp phi) + (setp (co-domain phi)) + (list-of-variables-p (co-domain phi)) + (mv-let (term phi1 bool) + (anti-unify-aux flg t1 t2 nil) + (declare (ignore term bool)) + (subsetp (domain phi1) (domain phi)))))) + + + + + +;;; ············································································ +;;; 2.2.2 pre-anti-unify-aux computes a generalization of t1 and t2 +;;; ············································································ + +;;; We have to prove something like: +; (let* ((glb (pre-anti-unify-aux flg t1 t2 phi)) +; (sigma1 (subst-anti-unify-1 phi))) +; (implies (and (alistp phi) (injection-p phi flg t1 t2) (second glb)) +; (equal (apply-subst flg sigma1 (first glb)) t1))) +;;; Using completeness of subsumption, this will suffice to prove that +;;; (first (pre-anti-unify-aux flg t1 t2 phi)) subsumes t1. But +;;; previously, we have to define subst-anti-unify-1, the witness +;;; matching substitution for t1. An analogue result has to be proved for t2, +;;; and also we have to define subst-anti-unify-2, the witness +;;; matching substitution for t2. + +(local + (defun subst-anti-unify-1 (phi) + (if (endp phi) + nil + (cons + (let* ((p (car phi)) + (pair-of-terms (car p)) + (variable (cdr p)) + (s1 (car pair-of-terms))) + (cons variable s1)) + (subst-anti-unify-1 (cdr phi)))))) + +(local + (defun subst-anti-unify-2 (phi) + (if (endp phi) + nil + (cons + (let* ((p (car phi)) + (pair-of-terms (car p)) + (variable (cdr p)) + (s2 (cdr pair-of-terms))) + (cons variable s2)) + (subst-anti-unify-2 (cdr phi)))))) + + + +;;; We will show previously that (subst-anti-unify-1 phi) and +;;; (subst-anti-unify-2 phi) are, respectively, the first and second +;;; projections of the inverse of phi. The following encapsulate does +;;; it. + + +(local + (encapsulate + () + + (defthm list-of-variables-p-co-domain-main-property + (implies (and + (member p (domain phi)) + (list-of-variables-p (co-domain phi))) + (variable-p (cdr (assoc p phi))))) + + (local + (defthm subst-anti-unify-1-inverse + (implies (and (setp (co-domain phi)) + (member x (co-domain phi)) + (list-of-variables-p (co-domain phi))) + (equal (val x (subst-anti-unify-1 phi)) + (car (val x (inverse phi))))))) + + + (local + (defthm subst-anti-unify-2-inverse + (implies (and (setp (co-domain phi)) + (member x (co-domain phi)) + (list-of-variables-p (co-domain phi))) + (equal (val x (subst-anti-unify-2 phi)) + (cdr (val x (inverse phi))))))) + + (local + (defthm val-val-inverse-lemma + (implies (and + (member x (domain phi)) + (equal (val x phi) y)) + (member y (co-domain phi))))) + + (local + (defthm val-val-inverse + (implies (and (setp (co-domain phi)) + (member x (domain phi))) + (equal (val (val x phi) (inverse phi)) x)))) + + + (local + (defthm member-domain-co-domain + (implies (member x (domain phi)) + (member (val x phi) (co-domain phi))))) + + (defthm inverse-projection-1 + (implies (and (setp (co-domain phi)) + (alistp phi) + (list-of-variables-p (co-domain phi)) + (member (cons t1 t2) (domain phi))) + (equal (val (cdr (assoc (cons t1 t2) phi)) + (subst-anti-unify-1 phi)) + t1))) + + (defthm inverse-projection-2 + (implies (and (setp (co-domain phi)) + (alistp phi) + (list-of-variables-p (co-domain phi)) + (member (cons t1 t2) (domain phi))) + (equal (val (cdr (assoc (cons t1 t2) phi)) + (subst-anti-unify-2 phi)) + t2))))) + + +;;; The following encapsulate prove some ugly technical lemmas for +;;; delaing with case *1/8 of the theorems subsumes-anti-unify-aux-1 +;;; and subsumes-anti-unify-aux-2. Se puede mejorar. + +(local + (encapsulate + () + + (local + (defthm anti-unify-aux-injection-subsetp-1 + (implies (third (anti-unify-aux flg t1 t2 phi)) + (subsetp (domain phi) + (domain (second (anti-unify-aux flg t1 t2 phi))))))) + + (defthm alistp-anti-unify-aux-injection ;;; This rule will be used later + ;;; again + (implies (alistp phi) + (alistp (second (anti-unify-aux flg t1 t2 phi))))) + + (defthm anti-unify-aux-injection-subsetp-2 ;;; This rule will be used later + ;;; again + (implies (and (alistp phi2) (subsetp (domain phi1) (domain phi2))) + (subsetp (domain (second (anti-unify-aux flg t1 t2 phi1))) + (domain (second (anti-unify-aux flg t1 t2 + phi2)))))) + + + + (defthm subsumes-anti-unify-aux-lemma-1 + (implies + (not (subsetp (domain (second (anti-unify-aux flg t3 t4 phi0))) + (domain phi))) + (not (subsetp + (domain + (second + (anti-unify-aux t t1 t2 + (second (anti-unify-aux + flg t3 t4 phi0))))) + (domain phi)))) + :hints (("Goal" + :use + (:instance + subsetp-transitive + (l (domain (second (anti-unify-aux flg t3 t4 phi0)))) + (m (domain + (second + (anti-unify-aux t t1 t2 + (second (anti-unify-aux + flg t3 t4 phi0)))))) + (n (domain phi)))))) + + + + (defthm subsumes-anti-unify-aux-lemma-2 + (implies + (and + (alistp phi0) + (third (anti-unify-aux flg2 t3 t4 phi0)) + (not (subsetp (domain (second (anti-unify-aux flg1 t1 t2 phi0))) + (domain phi)))) + (not + (subsetp + (domain + (second (anti-unify-aux flg1 t1 t2 + (second (anti-unify-aux + flg2 t3 t4 phi0))))) + (domain phi)))) + :hints (("Goal" + :in-theory (disable subsetp-transitive) + :use + (:instance + subsetp-transitive + (l (domain (second (anti-unify-aux flg1 t1 t2 phi0)))) + (m (domain + (second (anti-unify-aux flg1 t1 t2 + (second + (anti-unify-aux + flg2 t3 t4 phi0)))))) + (n (domain phi)))))))) + + +(local (in-theory (disable assoc-val))) + +;;; And the intended theorems: + +(local + (defthm subsumes-anti-unify-aux-1 + (let* ((glb (pre-anti-unify-aux flg t1 t2 phi)) + (sigma (subst-anti-unify-1 phi))) + (implies (and + (injection-p phi flg t1 t2) + (second glb)) + (equal (apply-subst flg sigma (first glb)) t1))))) + +(local + (defthm subsumes-anti-unify-aux-2 + (let* ((glb (pre-anti-unify-aux flg t1 t2 phi)) + (sigma (subst-anti-unify-2 phi))) + (implies (and + (injection-p phi flg t1 t2) + (second glb)) + (equal (apply-subst flg sigma (first glb)) t2))))) + + +;;; ············································································ +;;; 2.2.3 pre-anti-unify-aux computes the least common generalization of +;;; t1 and t2 +;;; ············································································ + +;;; This means, using completeness, that we have to construct, given an +;;; lower bound of t1 and t2, term, a matching substitution for term and +;;; (first (anti-unify-aux flg t1 t2 phi)). We are going to construct our +;;; matching substitutions using sigma1 and sigma2 (and phi). + +;;; SO our problem REDUCES to: + +;;; - We have two substitutions sigma1 and sigma2, and a term. +;;; - We have to construct a substitution a-u-subst s.t. applied to term +;;; returns (first (anti-unify-aux flg t1 t2 phi)), where t1 is +;;; (instance term sigma1) and t2 is (instance term sigma2). The +;;; function anti-unify-substitutions does the construction. + +;;; ======== ANTI-UNIFY-SUBSTITUTIONS + + +(local + (defun anti-unify-substitutions (sigma1 sigma2 l phi) + (if (endp l) + nil + (cons + (cons (car l) + (mv-let (anti-unify bool) + (pre-anti-unify-aux + t (val (car l) sigma1) (val (car l) sigma2) phi) + (declare (ignore bool)) + anti-unify)) + (anti-unify-substitutions sigma1 sigma2 (cdr l) phi))))) + +;;; REMARK: We only need to know the value of anti-unify-substitutions +;;; in the variables of term. This is the reason to define it with its +;;; domain depending on a list l. + + +(local + (defthm anti-unify-instances-success + (second (pre-anti-unify-aux flg + (apply-subst flg sigma1 term) + (apply-subst flg sigma2 term) + phi)))) + + +;;; The main theorem of 2.2.3 +;;; +;;; REMARK: note the role of the list l in the proof. + +(local + (defthm + pre-anti-unify-aux-greatest-lower-bound-main-lemma + (let ((anti-unif-sigma (anti-unify-substitutions sigma1 sigma2 l phi)) + (anti-unif-term (first (pre-anti-unify-aux + flg + (apply-subst flg sigma1 term) + (apply-subst flg sigma2 term) + phi)))) + (implies (subsetp (variables flg term) l) + (equal (apply-subst flg anti-unif-sigma term) + anti-unif-term))))) + + + +;;; ---------------------------------------------------------------------------- +;;; 2.3 Closure property of pre-anti-unify-aux +;;; ---------------------------------------------------------------------------- + +(local + (encapsulate + () + + (local + (defthm alistp-acl2-numberp-eqlablep + (implies (and + flg + (alistp-acl2-numberp phi) + (assoc x phi)) + (term-s-p-aux flg (cdr (assoc x phi)))))) + + (local + (defthm pre-anti-unify-aux-equal-len + (implies (second (pre-anti-unify-aux nil l1 l2 phi)) + (equal (len (first (pre-anti-unify-aux nil l1 l2 phi))) + (len l1))))) + + + (defthm pre-anti-unify-aux-term-s-p-aux + (let* ((glb (pre-anti-unify-aux flg t1 t2 phi))) + (implies (and (injection-p phi flg t1 t2) + (alistp-acl2-numberp phi) + (second glb) + (term-s-p-aux flg t1) + (term-s-p-aux flg t2)) + (term-s-p-aux flg (first glb))))))) + + +;;; Needed for guard verification + +(local + (defthm pre-anti-unify-aux-term-p-aux + (let* ((glb (pre-anti-unify-aux flg t1 t2 phi))) + (implies (and (injection-p phi flg t1 t2) + (alistp-acl2-numberp phi) + (second glb) + (term-p-aux flg t1) + (term-p-aux flg t2)) + (term-p-aux flg (first glb)))) + :hints (("Goal" :use (:functional-instance + pre-anti-unify-aux-term-s-p-aux + (signat (lambda (x n) (eqlablep x))) + (term-s-p-aux term-p-aux)))))) + + + +;;; ============================================================================ +;;; 3 The bridge between anti-unify-aux and pre-anti-unify-aux +;;; ============================================================================ + + + +;;; ---------------------------------------------------------------------------- +;;; 3.1 Relation between anti-unify-aux and pre-anti-unify-aux +;;; ---------------------------------------------------------------------------- + + + +;;; First, the auxiliary concept of extension-assoc. Intuitively ph1 is +;;; "extension-assoc" of phi if phi1 can be expressed as (append phi2 +;;; phi), where the domain of phi2 is disjoint with the domain of ph1. + +(local + (defun extension-assoc (phi1 phi) + (cond ((equal phi1 phi) t) + ((endp phi1) nil) + (t (and (not (assoc (caar phi1) phi)) + (extension-assoc (cdr phi1) phi)))))) + + +(local + (encapsulate + () + +;;; Relation between extension-assoc and assoc + + (local + (defthm extension-assoc-main-property + (implies (and (extension-assoc phi1 phi) (assoc x phi)) + (and (assoc x phi1) + (equal (cdr (assoc x phi1)) (cdr (assoc x phi))))))) + +;;; Transitivity of extension-assoc + + (local + (defthm extension-assoc-transitive + (implies (and (extension-assoc phi2 phi1) (extension-assoc phi1 phi)) + (extension-assoc phi2 phi)))) + +;;; Note that in every step, anti-unify-aux obtains an injection that +;;; "extends-assoc" the injection given as input. + + (local + (defthm anti-unify-aux-extension + (implies (third (anti-unify-aux flg t1 t2 phi)) + (extension-assoc (second (anti-unify-aux flg t1 t2 phi)) phi)))) + +;;; The intended relation between pre-anti-unify-aux and anti-unify-aux + + (local + (defthm anti-unify-aux-pre-anti-unify-aux-main-lemma + (implies (extension-assoc phi1 (second (anti-unify-aux flg t1 t2 phi))) + (equal (first (anti-unify-aux flg t1 t2 phi)) + (first (pre-anti-unify-aux flg t1 t2 phi1)))) + :rule-classes nil)) + +;;; A rewrite rule + + (defthm anti-unify-aux-pre-anti-unify-aux + (equal (first (anti-unify-aux flg t1 t2 phi)) + (first (pre-anti-unify-aux + flg t1 t2 (second (anti-unify-aux flg t1 t2 + phi))))) + :hints (("Goal" :use + (:instance anti-unify-aux-pre-anti-unify-aux-main-lemma + (phi1 (second (anti-unify-aux flg t1 t2 phi))))))))) + + +;;; ---------------------------------------------------------------------------- +;;; 3.2 anti-unify-aux returns a suitable injection for pre-anti-unify-aux +;;; ---------------------------------------------------------------------------- + +;;; The theorem anti-unify-aux-pre-anti-unify-aux shows the relation +;;; between anti-unify-aux and pre-anti-unify-aux, giving an alternative +;;; definition of anti-unify-aux, in terms of pre-anti-unify-aux. We +;;; will be able to export the properties of pre-anti-unify-aux if we +;;; prove that (second (anti-unify-aux flg t1 t2 phi)) meets the +;;; property injection-p. + + +(local + (defun acl2-numberp-increasing-list (l) + (cond ((endp l) t) + ((endp (cdr l)) (acl2-numberp (first l))) + (t + (and + (acl2-numberp (first l)) + (> (first l) (second l)) + (acl2-numberp-increasing-list (cdr l))))))) + +(local + (encapsulate + () + (local + (defthm acl2-numberp-increasing-list-set-of-variables-co-domain + (implies (acl2-numberp-increasing-list L) + (and (setp l) (list-of-variables-p l))))) + + (local + (defthm anti-unify-aux-injection-setp-co-domain + (implies (acl2-numberp-increasing-list (co-domain phi0)) + (acl2-numberp-increasing-list + (co-domain + (second (anti-unify-aux flg t1 t2 phi0))))))) + + (defthm anti-unify-aux-injection-injection-p + (implies + (and (acl2-numberp-increasing-list (co-domain phi0)) + (alistp phi0)) + (injection-p + (second + (anti-unify-aux flg t1 t2 phi0)) flg t1 t2))))) + +;;; To apply the closure property we also need to prove that the second +;;; value of anti-unify-aux is a alistp-acl2-numberp + +(local + (defthm anti-unify-aux-injection-alistp-acl2-numberp + (implies (alistp-acl2-numberp phi0) + (alistp-acl2-numberp + (second + (anti-unify-aux flg t1 t2 phi0)))))) + +;;; The above properties are enough to prove the main theorems below. So +;;; we disable: +(local + (in-theory (disable anti-unify-aux + pre-anti-unify-aux + injection-p))) + + + +;;; ============================================================================ +;;; 4 anti-unify: definition and (non-local) main properties +;;; ============================================================================ + +;;; ========= ANTI-UNIFY + +(defun anti-unify (t1 t2) + (declare (xargs :guard (and (term-p t1) (term-p t2)))) + (mv-let (anti-unify phi bool) + (anti-unify-aux t t1 t2 nil) + (declare (ignore phi bool)) + anti-unify)) + +;;; REMARK: Note how the following properties are proved, in general: +;;; - (first of) anti-unify-aux is rewritten to (first of) +;;; pre-anti-unify-aux using the rule anti-unify-aux-pre-anti-unify-aux +;;; - The corresponding property of pre-anti-unify-aux is used, since +;;; (second (anti-unify-aux t t1 t2 nil)) has the property injection-p + + + +(defthm anti-unify-lower-bound + + (and (subs (anti-unify t1 t2) t1) + (subs (anti-unify t1 t2) t2)) + + + :hints (("Goal" :use + ((:instance + subs-completeness + (sigma (subst-anti-unify-1 + (second + (anti-unify-aux t t1 t2 nil)))) + (t1 (first (anti-unify-aux t t1 t2 nil))) + (t2 t1)) + (:instance + subs-completeness + (sigma (subst-anti-unify-2 + (second + (anti-unify-aux t t1 t2 nil)))) + (t1 (first (anti-unify-aux t t1 t2 nil)))))))) + + + + +(defthm anti-unify-greatest-lower-bound + + (implies (and (subs term t1) + (subs term t2)) + (subs term (anti-unify t1 t2))) + + :hints (("Goal" + :use + ((:instance + subs-completeness + (sigma (anti-unify-substitutions + (matching term t1) + (matching term t2) + (variables t term) + (second + (anti-unify-aux t t1 t2 nil)))) + (t1 term) + (t2 (anti-unify t1 t2))))))) + + +;;; Closure property: + +(defthm anti-unify-term-s-p + (implies (and (term-s-p t1) (term-s-p t2)) + (term-s-p (anti-unify t1 t2)))) + + +;;; Needed for guard verification: + +(defthm anti-unify-term-p + (implies (and (term-p t1) (term-p t2)) + (term-p (anti-unify t1 t2)))) + +;;; REMARK: We could have obtained this last theorem by functional +;;; instantiation of the +;;; previous theorem, but it is also a trivial consequence of +;;; pre-anti-unify-aux-term-p-aux + + +(in-theory (disable anti-unify (anti-unify))) + + + + + + + + + + + + diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/basic.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/basic.lisp new file mode 100644 index 0000000..25fd294 --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/basic.lisp @@ -0,0 +1,679 @@ +;;; basic.lisp +;;; Some stuff about lists, sets, sequences and association lists. +;;; Created: 6-8-99 Last revison: 05-12-2000 +;;; ============================================================================= + +#| To certify this book: + +(in-package "ACL2") + +(certify-book "basic") + +|# + + +(in-package "ACL2") + + +;;; ******************************************************************* +;;; BASIC PROPERTIES ABOUT LISTS, SETS, SEQUENCES AND ASSOCIATION LISTS +;;; ******************************************************************* + +;;; REMARK: This is book is not intended to be a complete tratement of +;;; such data structures, but and "ad hoc" collection of definition and +;;; properties, needed for further development of the theory of first +;;; order terms. + +;;; ============================================================================ +;;; 1. Lists +;;; ============================================================================ + + +;;; ======= APPEND + +(defthm append-associative + (equal (append (append x y) z) + (append x (append y z)))) + +(defthm member-append + (iff (member x (append a b)) + (or (member x a) (member x b)))) + + +(defthm append-nil + (implies (true-listp l) + (equal (append l nil) l))) + + +;;; ======= REVLIST + +(defun revlist (l) + (if (endp l) + nil + (append (revlist (cdr l)) (list (car l))))) + +(defthm revlist-true-listp + (true-listp (revlist l))) + +(local + (defthm revappend-revlist + (equal (revappend l m) (append (revlist l) m)))) + +(defthm reverse-revlist + (implies (true-listp l) + (equal (reverse l) (revlist l)))) + +;;; ====== DELETE-ONE + +(defun delete-one (x l) + (cond ((atom l) l) + ((equal x (car l)) (cdr l)) + (t (cons (car l) (delete-one x (cdr l)))))) + +(defthm delete-one-less-length + (implies (member x m) + (< (len (delete-one x m)) (len m)))) + +(defthm member-delete-one + (implies (and (member x m) (not (equal x y))) + (member x (delete-one y m)))) + +(defthm delete-one-conmute + (equal (delete-one x (delete-one y l)) + (delete-one y (delete-one x l)))) + +(defthm subsetp-delete-one + (implies (not (member x l)) + (not (member x (delete-one y l))))) + +;;; ======= ELIMINATE (like remove, but different guard, using equal) + +(defun eliminate (x l) + (declare (xargs :guard (true-listp l))) + (cond ((endp l) nil) + ((equal x (car l)) (eliminate x (cdr l))) + (t (cons (car l) (eliminate x (cdr l)))))) + + +(defthm eliminate-len + (implies (member x l) + (< (len (eliminate x l)) (len l))) + :rule-classes :linear) + +;;; ====== NATURAL-TRUE-LISTP +(defun positive-integer-true-listp (l) + (declare (xargs :guard t)) + (if (atom l) + (equal l nil) + (and (integerp (car l)) (> (car l) 0) + (positive-integer-true-listp (cdr l))))) + +;;; ====== REPLACE-LIST + +(defun replace-list (l n x) + (declare (xargs :guard + (and (true-listp l) (integerp n) (>= n 0)))) + (if (endp l) + nil + (if (zp n) + (cons x (cdr l)) + (cons (car l) (replace-list (cdr l) (- n 1) x))))) + + +(defthm nth-replace-list-same-position + (implies (and (integerp i) + (<= 0 i) + (< i (len l))) + (equal (nth i (replace-list l i x)) x))) + + +(defthm replace-list-same-length + (equal (len (replace-list l i x)) (len l))) + + +(defthm nth-replace-list-different-position + (implies (and (integerp i) (integerp k) + (<= 0 i) (<= 0 k) + (< i (len l)) (< k (len l)) + (not (equal i k))) + (equal (nth i (replace-list l k x)) (nth i l)))) + + + + +(defthm replace-list-different-position + (implies (and (integerp i) (integerp k) + (<= 0 i) (<= 0 k) + (< i (len l)) (< k (len l)) + (not (equal i k))) + (equal + (replace-list (replace-list l i x) k y) + (replace-list (replace-list l k y) i x)))) + + + +(defthm replace-list-same-position + (implies (and (integerp i) + (<= 0 i) + (< i (len term))) + (equal + (replace-list (replace-list term i x) i y) + (replace-list term i y)))) + + + + + +;;; ====== PAIR-ARGS + +(defun pair-args (l1 l2) + (declare (xargs :guard (and (true-listp l1) (true-listp l2)))) + (cond ((endp l1) (if (equal l1 l2) (mv nil t) (mv nil nil))) + ((endp l2) (mv nil nil)) + (t (mv-let (pair-rest bool) + (pair-args (cdr l1) (cdr l2)) + (if bool + (mv (cons (cons (car l1) (car l2)) + pair-rest) + t) + (mv nil nil)))))) + +;;; **** Guard verification +(defthm pair-args-true-listp + (true-listp (car (pair-args l1 l2)))) + + +;;; ======= MV-NTH + +;;; REMARK: I prefer to deal with first,second, third, etc... than with +;;; mv-nth. + +(defthm mv-nth-0-first + (equal (mv-nth 0 l) (first l))) + +(defthm mv-nth-1-second + (equal (mv-nth 1 l) (second l))) + +(defthm mv-nth-2-third + (equal (mv-nth 2 l) (third l))) + +(defthm mv-nth-3-fourth + (equal (mv-nth 3 l) (fourth l))) + +;;; and so on... + + +;;; ============================================================================ +;;; 2. Sets +;;; ============================================================================ + +;;; ====== SETP +;;; A true-list without repeated elements. + +(defun setp (l) + (if (atom l) + t + (and (not (member (car l) (cdr l))) + (setp (cdr l))))) + +(encapsulate + () + (local (defthm member-eliminate + (implies (member y (eliminate x l)) + (member y l)))) + + (defthm eliminate-preserves-setp + (implies (setp l) + (setp (eliminate x l))))) + + + + +;;; ====== SUBSETP + +(defun not-subsetp-witness (l1 l2) + (if (atom l1) + nil + (if (member (car l1) l2) + (not-subsetp-witness (cdr l1) l2) + (car l1)))) + +(defthm not-subsetp-witness-lemma + (equal (subsetp l1 l2) + (implies (member (not-subsetp-witness l1 l2) l1) + (member (not-subsetp-witness l1 l2) l2)))) + + +(in-theory (disable not-subsetp-witness-lemma)) + +(defthm subsetp-append-1 + (equal (subsetp (append x y) z) + (and (subsetp x z) (subsetp y z)))) + +(defthm subsetp-append-2 + (implies (subsetp c a) + (subsetp c (append b a)))) + +(defthm subsetp-append-3 + (implies (subsetp b c) + (subsetp b (append c a)))) + + +(defthm subsetp-cons + (implies (subsetp l m) + (subsetp l (cons x m)))) + +(defthm subsetp-reflexive + (subsetp l l)) + +(defthm delete-one-subsetp + (subsetp (delete-one x l) l)) + +(defun subset-induction (l m) + (if (or (atom l) (atom m) (not (member (car l) m))) + t + (subset-induction (cdr l) (eliminate (car l) m)))) + +(defthm + substp-preserved-when-deleting-a-non-member + (implies (and (subsetp z m) (not (member x z))) + (subsetp z (eliminate x m)))) + + +;;; ====== DISJOINTP + +;;; No common elements + +(defun disjointp (l1 l2) + (if (endp l1) + t + (and (not (member (car l1) l2)) + (disjointp (cdr l1) l2)))) + + +(defthm disjointp-cons + (equal (disjointp l (cons x m)) + (and (not (member x l)) + (disjointp l m)))) + +(defthm disjointp-append-1 + (equal (disjointp (append l m) n) + (and (disjointp l n) + (disjointp m n)))) + +(defthm disjointp-append-2 + (equal (disjointp m (append l n)) + (and (disjointp m l) + (disjointp m n)))) + +(defthm disjointp-conmutative + (equal (disjointp l1 l2) (disjointp l2 l1))) + +(defthm disjointp-nil + (disjointp x nil)) + + + +;;; ======= MAKE-SET +;;; Eliminate duplicates. + +(defun make-set (l) + (if (atom l) + nil + (if (member (car l) (cdr l)) + (make-set (cdr l)) + (cons (car l) (make-set (cdr l)))))) + +(defthm member-make-set + (iff (member x (make-set l)) (member x l))) + +(defthm setp-make-set + (setp (make-set x))) + +(defthm make-set-of-a-setp-is-the-same + (implies (setp l) + (equal (make-set l) (fix-true-list l)))) + +(defthm len-fix-true-list + (equal (len (fix-true-list l)) (len l))) + +(defthm make-set-lessp-length-if-not-setp + (implies (not (setp l)) + (< (len (make-set l)) + (len l))) + :rule-classes :linear) + + +(defthm length-make-set-leq + (>= (len l) + (len (make-set l))) + :rule-classes :linear) + +(defthm make-set-fix-true-list + (equal (fix-true-list (make-set l)) (make-set l))) + + +;;; ============ EQUAL-SET: CONGRUENCE AND REWRITE RULES + +(defun equal-set (x y) + (and (subsetp x y) (subsetp y x))) + + +(defthm subsetp-transitive + (implies (and (subsetp l m) + (subsetp m n)) + (subsetp l n))) + + +(defequiv equal-set) + + +(defcong equal-set iff (subsetp x y) 1) +(defcong equal-set iff (subsetp x y) 2) +(defcong equal-set equal (consp l) 1) + +(encapsulate + () + (local + (defthm subsetp-disjoint-1 + (implies (and (subsetp x x-equiv) + (disjointp x-equiv y)) + (disjointp x y)))) + + (defcong equal-set iff (disjointp x y) 1)) + +(encapsulate + () + (local + (defthm subsetp-disjoint-2 + (implies (and (subsetp y y-equiv) + (disjointp x y-equiv)) + (disjointp x y)))) + + (defcong equal-set iff (disjointp x y) 2)) + + +(encapsulate + () + (local (defthm equal-set-member-cong-lemma-1 + (implies (and (not (member x y)) + (subsetp y-equiv y)) + (not (member x y-equiv))))) + + (local (defthm equal-set-member-cong-lemma-2 + (implies (and (member x y) + (subsetp y y-equiv)) + (member x y-equiv)))) + (defcong equal-set iff (member x y) 2)) + + +(defthm equal-set-make-set + (equal-set (make-set l) l)) + +;;; REMARK: The following rule is needed in +;;; equal-size-and-not-inverse-subsumption-implies-not-renaming-almost +;;; I don't know why the previous rule is not used (monitoring is not +;;; possible, because it is a "simple"(?) rule). So I think I need the +;;; following rule, which is redundant (?) + + +(defthm subsetp-make-set-provisional + (iff (subsetp a (make-set b)) (subsetp a b))) + + + + +;;; ====== PERM: CONGRUENCE AND REWRITE RULES + + +(defun perm (lst1 lst2) + (cond ((atom lst1) (atom lst2)) + ((member (car lst1) lst2) + (perm (cdr lst1) (delete-one (car lst1) lst2))) + (t nil))) + + +(encapsulate + () + + (defthm perm-reflexive + (perm x x)) + + (local + (defthm perm-main-lemma + (implies (and (member x a) + (member x b) + (perm (delete-one x a) (delete-one x b))) + (perm a b)))) + + (local + (defthm perm-symmetric + (implies (perm x y) (perm y x)))) + + + (local + (defthm perm-transitive-reverse + (implies (and (perm a b) + (perm a c)) + (perm b c)) + :rule-classes nil)) + + (local + (defthm perm-transitive + (implies (and (perm a b) + (perm b c)) + (perm a c)) + :hints (("Goal" :use + ((:instance perm-symmetric + (x a) (y b)) + (:instance perm-transitive-reverse + (a b) (b a))))))) + (defequiv perm)) + + + +(local (defthm perm-implies-subsetp + (implies (perm x y) (subsetp x y)) + :hints (("Goal" :induct (perm x y))))) + + +(defrefinement perm equal-set) + +;;; Rewriting rules + +(defthm perm-fix-true-list + (perm (fix-true-list l) l)) + + +;;; ============================================================================ +;;; 3. Sequences +;;; ============================================================================ + +;;; Sequences of natural numbers will be used to represent positions of +;;; terms. + +;;; ===== PREFIX + +(defun prefix (p1 p2) + (cond ((endp p1) t) + ((endp p2) nil) + ((equal (car p1) (car p2)) + (prefix (cdr p1) (cdr p2))) + (t nil))) + +;;; ===== DIFFERENCE-POS + +(defun difference-pos (p q) + (if (atom p) + q + (difference-pos (cdr p) (cdr q)))) + + +(defthm difference-the-same + (implies (true-listp l) + (equal (difference-pos l l) nil))) + +(defthm difference-pos-common-prefix + (equal (difference-pos l (append l m)) + m)) + +(defthm difference-pos-common-prefix-append + (equal (difference-pos (append l m) (append l n)) + (difference-pos m n))) + + +;;; ===== DISJOINT-POSITIONS + +(defun disjoint-positions (p1 p2) + (cond + ((or (endp p1) (endp p2)) nil) + ((equal (car p1) (car p2)) + (disjoint-positions (cdr p1) (cdr p2))) + (t t))) + + + +;;; ============================================================================ +;;; 4. Association lists +;;; ============================================================================ + + +;;; REMARK: Association lists represent finite domain functions in the +;;; following way: +;;; - Every atom object represents the identity function. +;;; - If an atom object is member of an association list will be +;;; considered as (nil . nil). +;;; - If several pairs (x . t1), (x . t2),... are member of an +;;; association list only the first one is considered. +;;; As a consecuence of this representation, different objects represent +;;; the same finite domain function. Thus, we cannot use equal as a +;;; predicate to talk about equality of finite domain functions. + +;;; REMARK: We do not use the book alist-theory.list +;;; provided by the distribution because we need our own version of +;;; assoc (see the function val). We want the association list to behave +;;; like identity outside its domain. + +;;; ======= VAL +;;; (i.e., sigma(x)) + +(defun val (x sigma) + (declare (xargs :guard (if (eqlablep x) + (alistp sigma) + (eqlable-alistp sigma)))) + (if (endp sigma) + x + (if (eql x (caar sigma)) (cdar sigma) (val x (cdr sigma))))) + +#|| +; [Removed by Matt K. to handle changes to member, assoc, etc. after ACL2 4.2.] + +;;; REMARK: For execution, I will use assoc when the variable is in the +;;; domain. Sometimes, I have to use assoc-equal (see renamings.lisp). +;;; The following rule rewrites assoc-equal to assoc. In this way, we +;;; can build one set of rules about assoc. WARNING: this is different +;;; rewriting strategy than the one given in the book alist-defthms.lisp +;;; in the ACL2 distribution. + +(defthm assoc-equal-assoc-equal + (equal (assoc-equal x a) (assoc x a))) +||# + + +;;; This relation between val and assoc is expressed +;;; here. For reasonig, I prefer to use val (that's the explanation for +;;; the orientation of the following rule): +(defthm assoc-val + (implies (assoc x l) + (equal (cdr (assoc x l)) (val x l)))) + +;;; ====== RESTRICTION +;;; The list of pairs (x. sigma(x)), for all x in l. + +(defun restriction (sigma l) + (if (atom l) + l + (cons (cons (car l) (val (car l) sigma)) + (restriction sigma (cdr l))))) + +;;; ====== DOMAIN +;;; domain of association lists (the list of first components of sigma). +;;; Note: as we said above, the atom elements of sigma are considered +;;; as (nil . nil). This remark also applies to the following definitions. + +(defun domain (sigma) + (declare (xargs :guard (alistp sigma))) + (if (endp sigma) + nil + (cons (caar sigma) (domain (cdr sigma))))) + + +(defthm domain-restriction + (equal (domain (restriction sigma l)) (fix-true-list l))) + + +(defthm domain-append + (equal (domain (append l1 l2)) + (append (domain l1) (domain l2)))) + +(defthm consp-domain + (equal (consp (domain sigma)) + (consp sigma))) + + +(defthm assoc-member-domain + (implies (alistp sigma) + (iff (member x (domain sigma)) + (assoc x sigma)))) + + +;;; ====== CO-DOMAIN +;;; co-domain of association lists (the list of first components of sigma). + +(defun co-domain (sigma) + (if (atom sigma) + nil + (cons (cdar sigma) (co-domain (cdr sigma))))) + + + +;;; ====== INVERSE +;;; The association list obtained reversing the pairs. + +(defun inverse (sigma) + (if (atom sigma) + nil + (cons (cons (cdar sigma) (caar sigma)) + (inverse (cdr sigma))))) + + +(defthm domain-of-inverse-is-co-domain + (equal (domain (inverse sigma)) (co-domain sigma))) + +(defthm co-domain-of-inverse-is-domain + (equal (co-domain (inverse sigma)) (domain sigma))) + +(defthm same-length-co-domain-and-domain + (equal (len (domain sigma)) + (len (co-domain sigma)))) + +(in-theory (disable same-length-co-domain-and-domain)) + + + +;;; ====== ALISTP (for guard verification) + +(defthm assoc-consp-or-nil + (implies (alistp a) + (or (consp (assoc x a)) + (equal (assoc x a) nil))) + :rule-classes :type-prescription) + + +(defun alistp-acl2-numberp (l) + (declare (xargs :guard t)) + (if (atom l) + (equal l nil) + (and (consp (car l)) (acl2-numberp (cdar l)) + (alistp-acl2-numberp (cdr l))))) + diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/lattice-of-terms.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/lattice-of-terms.lisp new file mode 100644 index 0000000..e8b1379 --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/lattice-of-terms.lisp @@ -0,0 +1,397 @@ +;;; lattice-of-terms.lisp +;;; A compilation of previous results to prove that we can define a +;;; complete well-founded lattice in the set of objects of the ACL2 logic. +;;; The lattice is defined w.r.t. the subsumption relation. +;;; Creation: 26-10-99. Last revision: 11-12-2000 +;;; ================================================================= + +#| To certify this book: + +(in-package "ACL2") + +(certify-book "lattice-of-terms") + +|# + +(in-package "ACL2") + + +(include-book "subsumption-well-founded") + +(include-book "mg-instance") + +(include-book "anti-unification") + +;;; ********************************************************* +;;; THE COMPLETE LATTICE OF FIRST-ORDER TERMS WITH RESPECT TO +;;; SUBSUMPTION +;;; ********************************************************* + +;;; We compile the results of this library about first-order terms, to +;;; prove that we can define a complete well-founded lattice +;;; w.r.t. subsumption in the set of objects of the ACL2 logic. We also +;;; prove that the set of terms of a given signature is a sublattice. + + +;;; ============================================================================ +;;; 1. Introducing one distinguished top term and substitution. +;;; ============================================================================ + + +;;; ------ +;;; Macros +;;; ------ + +;;; We will distinguish one term, called the top term: + +(defmacro the-top-term () + ''the-top-term) + +(defmacro is-the-top-term (term) + `(equal ,term (the-top-term))) + +;;; We will distinguish one substitution, called the top substitution: + +(defmacro the-top-substitution () + ''the-top-substitution) + +(defmacro is-the-top-substitution (subst) + `(equal ,subst (the-top-substitution))) + +;;; Some previous technical definitions: + + +(defun fix-substitution (sigma) + (declare (xargs :guard t)) + (if (atom sigma) nil sigma)) + +;;; REMARK: This will force to every empty substitution returned +;;; by subs to be distinct from the-top-substitution. + +(defun fix-term (term) + (declare (xargs :guard t)) + (if (variable-p term) 0 term)) + +;;; REMARK: This forces to every term returned by anti-unification and +;;; mg-instance to be distinct from the-top-term. + +;;; A few technical lemmas: + + +(local + (defthm the-top-term-anti-unify-variable-p + (implies (and (variable-p (anti-unify t1 t2)) + (subs term t1) (subs term t2)) + (variable-p term)) + :hints (("Goal" :use + ((:instance minimum-subsumption-implies-variable + (x (anti-unify t1 t2)))))))) + +; (local (in-theory (disable the-top-term-anti-unify-variable-p))) + +(local + (defthm the-top-term-mg-instance-variable-p-1 + (implies (and (mg-instance term t2) + (variable-p (mg-instance term t2))) + (variable-p term)) + :hints (("Goal" :use + ((:instance minimum-subsumption-implies-variable + (x (mg-instance term t2)))))))) + +(local + (defthm the-top-term-mg-instance-variable-p-2 + (implies (and (mg-instance t1 term) + (variable-p (mg-instance t1 term))) + (variable-p term)) + :hints (("Goal" :use + ((:instance minimum-subsumption-implies-variable + (x (mg-instance t1 term)))))))) + + +(local (in-theory (enable variable-minimum-subsumption))) + +(local + (defthm substitution-p-alistp-forward-chaining + (implies (substitution-p sigma) + (alistp sigma)) + :rule-classes :forward-chaining)) + + + +;;; In the following, we will state (and mechanichally prove) the +;;; properties of a well founded lattice: the set of terms w.r.t +;;; subsumption. + + +;;; ============================================================================ +;;; 2. Terms and substitutions +;;; ============================================================================ + + +;;; Every object can be seen as a term (see terms.lisp for details). But +;;; we can define (extended) terms of a given signature: + +(defun ext-term-s-p (term) + (or (term-s-p term) (is-the-top-term term))) + +;;; For guard verification purpouses, we can define well-formed +;;; (extended) terms: + +(defun ext-term-p (term) + (declare (xargs :guard t)) + (or (term-p term) (is-the-top-term term))) + + +;;; Every object can be seen as a substitution (see terms.lisp). But we +;;; can define (extended) substitutions of a given signature: + + +(defun ext-substitution-s-p (sigma) + (or (substitution-s-p sigma) (is-the-top-substitution sigma))) + + + +;;; For guard verification purpouses, we can define wel-formed +;;; (extended) substitutions: + +(defun ext-substitution-p (sigma) + (declare (xargs :guard t)) + (or (substitution-p sigma) (is-the-top-substitution sigma))) + + +;;; Applying substitutions to terms +;;; (see terms.lisp) + +(defun app<= (sigma term) + (declare (xargs :guard (and (ext-substitution-p sigma) + (ext-term-p term)))) + (if (or (is-the-top-substitution sigma) + (is-the-top-term term)) + (the-top-term) + (instance term sigma))) + + + +;;; ============================================================================ +;;; 3. Subsumption relation between terms. +;;; ============================================================================ + +;;; (see subsumption-one-definition-and-properties.lisp for details) + +(defun s<= (t1 t2) + (declare (xargs :guard (and (ext-term-p t1) + (ext-term-p t2)))) + (cond ((is-the-top-term t2) t) + ((is-the-top-term t1) nil) + (t (subs t1 t2)))) + +(defun match<= (t1 t2) + (declare (xargs :guard (and (ext-term-p t1) + (ext-term-p t2)))) + (cond ((is-the-top-term t2) + (the-top-substitution)) + ((is-the-top-term t1) + nil) + (t (fix-substitution (matching t1 t2))))) + + +;;; Closure properties: + +(defthm match<=-ext-substitution-s-p + (implies (and (ext-term-s-p t1) (ext-term-s-p t2)) + (ext-substitution-s-p (match<= t1 t2)))) + + +(defthm app<=-substitution-s-p + (implies (and (ext-term-s-p term) + (ext-substitution-s-p sigma)) + (ext-term-s-p (app<= sigma term)))) + + +;;; Relation between app<= and subsumption +;;; (see subsumption-one-definition-and-properties.lisp for details) + +;;; If exists sigma such that t2 = (app<= sigma term), then term subsumes +;;; t2: + +(defthm app<=-s<=-relationship-1 + + (implies (equal t2 (app<= sigma t1)) + (s<= t1 t2))) + + +;;; If t1 susbsumes t2, then exists a substitution s.t. applied to t1 +;;; returns t2. That substitution is given by match<=. + +(defthm app<=-s<=-relationship-2 + + (implies (s<= t1 t2) + (equal (app<= (match<= t1 t2) t1) t2)) + + :hints (("Goal" :in-theory (enable apply-atom)))) + + + +;;; ============================================================================ +;;; 4. s<= is a quasi-ordering +;;; ============================================================================ + +;;; (see subsumption-one-definition-and-properties.lisp for details) + + +;;; Reflexivity + +(defthm s<=-reflexivity + + (s<= term term)) + + +;;; Transitivity + +(defthm s<=-transitivity + + (implies (and (s<= t1 t2) (s<= t2 t3)) + (s<= t1 t3)) + + :hints (("Goal" :in-theory (enable subsumption-transitive)))) + + + +;;; ============================================================================ +;;; 5. s<= is well-founded +;;; ============================================================================ + + +;;; (see subsumption-well-founded.lisp for details) + + +;;; The strict part of s<= + +(defun s< (t1 t2) + (and (s<= t1 t2) (not (s<= t2 t1)))) + + + +;;; A measure on terms. + +(defun measure-s< (term) + (if (is-the-top-term term) + (make-ord (omega) 1 0) ;;; This is omega^{omega} + (subsumption-measure term))) + +;;; The measure is an ordinal. + +(defthm measure-s<-ordinalp + + (o-p (measure-s< term))) + + +;;; Strictly decreasing in s<= implies strictly decreasing in measure. + +(in-theory (disable (:executable-counterpart make-ord))) +(in-theory (disable (:executable-counterpart measure-s<))) + +(defthm s<-well-founded + + (implies (s< t1 t2) + (o< (measure-s< t1) (measure-s< t2)))) + +;;; REMARK: + +;;; The above two lemmas implies in our meta-logic that there no +;;; infinite decreasing (w.r.t. s<) chain of terms. Thus, subsumption +;;; between first order terms is a well founded relation. + + +;;; ============================================================================ +;;; 6. Greatest lower bound of two terms (w.r.t. s<=) +;;; ============================================================================ + +;;; (see anti-unification.lisp for details) + +(defun glb-s<= (t1 t2) + (declare (xargs :guard (and (ext-term-p t1) (ext-term-p t2)))) + (cond ((is-the-top-term t1) t2) + ((is-the-top-term t2) t1) + (t (fix-term (anti-unify t1 t2))))) + + +;;; glb-s<= is a lower bound of t1 and t2. + +(defthm glb-s<=-lower-bound-1 + + (s<= (glb-s<= t1 t2) t1)) + + +(defthm glb-s<=-lower-bound-2 + + (s<= (glb-s<= t1 t2) t2)) + + +;;; glb-s<= is greater (or equivalent) than any lower-bound. + + +(defthm glb-s<=-is-greater-than-any-lower-bound + + (implies (and (s<= term t1) + (s<= term t2)) + (s<= term (glb-s<= t1 t2)))) + + +;;; glb-s<= of two terms of a given signature is a term of that +;;; signature: + +(defthm glb-s<=-closure-property + (implies (and (ext-term-s-p t1) (ext-term-s-p t2)) + (ext-term-s-p (glb-s<= t1 t2)))) + +;;; ============================================================================ +;;; 7. Least upper bound of two terms (w.r.t. s<=) +;;; ============================================================================ +;;; (see mg-instance.lisp for details) + + +(defun lub-s<= (t1 t2) + (declare (xargs :guard (and (ext-term-p t1) (ext-term-p t2)))) + (cond ((or (is-the-top-term t1) + (is-the-top-term t2)) + (the-top-term)) + ((mg-instance t1 t2) (fix-term (mg-instance t1 t2))) + (t (the-top-term)))) + +;;; lub-s<= is an upper bound of t1 y t2 + +(defthm lub-s<=-upper-bound-1 + + (s<= t1 (lub-s<= t1 t2))) + + +(defthm lub-s<=-upper-bound-2 + + (s<= t2 (lub-s<= t1 t2))) + + +;;; lub-s<= es less (or equivalent) than any upper bound + +(defthm lub-s<=-less-than-any-upper-bound + + (implies (and (s<= t1 term) + (s<= t2 term)) + (s<= (lub-s<= t1 t2) term))) + + +;;; lub-s<= of two terms of a given signature is a term of that +;;; signature: + +(defthm lub-s<=-closure-property + (implies (and (ext-term-s-p t1) (ext-term-s-p t2)) + (ext-term-s-p (lub-s<= t1 t2)))) + + + +;;; CONCLUSION: + +;;; So the set of objects of ACL2 logic is well-founded lattice +;;; w.r.t. the s<= relation (in particular this implies tha it is a +;;; complete lattice). And the set of terms of a given signature is a +;;; sublattice. diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/matching.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/matching.lisp new file mode 100644 index 0000000..62e2c5b --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/matching.lisp @@ -0,0 +1,667 @@ +;;; matching.lisp +;;; Definition and correctness of a RULE BASED matching +;;; algorithm between systems of equations. +;;; This definition is a PATTERN for concrete matching +;;; algorithms. See subsumption.lisp for a concrete +;;; implementation. +;;; This is an alternative to a more classical formulation in +;;; matching.lisp +;;; Created: 9-10-99 Last revison: 05-01-2001 +;;; ============================================================================= + +#| To certify this book: + +(in-package "ACL2") + +(certify-book "matching") + +|# + + + +(in-package "ACL2") +(include-book "terms") + +;;; ******************************************************************** +;;; DEFINITION AND VERIFICATION OF A RULE-BASED SUBSUMPTION ALGORITHM WE +;;; USE THIS BOOK TO PROVIDE A "PATTERN" FOR DEFINING A CONCRETE AND +;;; EXECUTABLE SUBSUMPTION ALGORITHM. +;;; ******************************************************************** + + + +;;; ============================================================================ +;;; 1. The transformation rules +;;; ============================================================================ + + +;;; ---------------------------------------------------------------------------- +;;; 1.1 Definition. +;;; ---------------------------------------------------------------------------- + + +;;; First, we introduce some kind of non-determinism, by partially +;;; defining a selection function a-pair, assuming only the property that +;;; a-pair selects an element of every non-empty list: + +(encapsulate + + ((a-pair (lst) t)) + + (local (defun a-pair (lst) (car lst))) + + (defthm a-pair-selected + (implies (consp l) (member (a-pair l) l)))) + + +;;; The rules of transformation. This function is intended to act on a +;;; pair of systems, S-match. The first one, S, has the equations to be +;;; solved, and the second one has the bindings done for the moment. An +;;; equation is selected from S, and according to this equation, a rule +;;; of transformation is applied. + +(defun transform-subs-sel (S-match) + (let* ((S (car S-match)) (match (cdr S-match)) + (ecu (a-pair S)) + (t1 (car ecu)) (t2 (cdr ecu)) + (R (eliminate ecu S))) + (cond + ((variable-p t1) + (let ((bound (assoc t1 match))) + (if bound + (if (equal (cdr bound) t2) + (cons R match) ;;; *** DELETE + nil) ;;; *** FAIL-BIND + (cons R (cons (cons t1 t2) match))))) ;;; *** BIND + ((variable-p t2) nil) ;;; *** FAIL-VAR + ((equal (car t1) (car t2)) + (mv-let (pair-args bool) + (pair-args (cdr t1) (cdr t2)) + (if bool + (cons (append pair-args R) match) ;;; *** DECOMPOSE + nil))) ;;; *** CONFLICT-1 + (t nil)))) ;;; *** CONFLICT-2 + + + +;;; ---------------------------------------------------------------------------- +;;; 1.2 Main properties of transform-subs-sel +;;; ---------------------------------------------------------------------------- + + +;;; ············································································ +;;; 1.2.1 How we deal with selection. +;;; ············································································ + + +;;; Firs we prove that equal-set is a congruence w.r.t. the second +;;; argument of matcher: +(local + (encapsulate + () + + (local + (defthm member-matcher + (implies (and (matcher sigma S) + (member equ S)) + (equal (instance (car equ) sigma) (cdr equ))))) + + (local + (defthm subsetp-matcher + (implies (and (matcher sigma S) + (subsetp S1 S)) + (matcher sigma S1)))) + + + (defcong equal-set iff (matcher x y) 2))) + +;;; Then we define a rewrite rule w.r.t. the equivalence equal-set. This +;;; rule allows the prover to put the selected equation in front of the +;;; system, when we are talking of matchers: + +(local + (encapsulate + () + (local + (defthm equal-set-selection-and-eliminate-lemma + (implies (member x S) + (equal-set (cons x (eliminate x S)) S)))) + + (defthm equal-set-selection-and-eliminate + (implies (consp (car S-match)) + (equal-set (car S-match) + (cons (a-pair (car S-match)) + (eliminate (a-pair (car S-match)) + (car S-match)))))))) + +;;; REMARK: Note why we use (car S-match) (instead of S) in the above rule: +;;; we avoid non-termination. + + + +;;; ············································································ +;;; 1.2.2 transform-subs-sel preserves the set of matchers. +;;; ············································································ + + +(local + (defthm matcher-append + (equal (matcher sigma (append S1 S2)) + (and (matcher sigma S1) (matcher sigma S2))))) + + +(local + (encapsulate + () + + (local + (defun induction-pair-args (l1 l2) + (if (or (endp l1) (endp l2)) + t + (induction-pair-args (cdr l1) (cdr l2))))) + + (local + (defthm matcher-pair-args + (implies (second (pair-args l1 l2)) + (equal (matcher sigma (car (pair-args l1 l2))) + (equal (apply-subst nil sigma l1) l2))) + :hints (("Goal" :induct (induction-pair-args l1 l2))))) + + + + (local + (defthm matcher-sigma-value + (implies (and + (matcher sigma S) + (variable-p x) + (assoc x S)) + (equal (val x sigma) (cdr (assoc x S)))))) + + + (local + (defthm pair-args-apply-subst + (second (pair-args term (apply-subst nil sigma term))))) + + (local + (defthm matcher-topmost-function-symbol + (implies (and (not (variable-p t1)) + (not (equal (car t1) (car t2)))) + (not (equal (instance t1 sigma) t2))))) + + + (local + (defthm matcher-variable-non-variable + (implies (and (not (variable-p t1)) + (variable-p t2)) + (not (equal (instance t1 sigma) t2))))) + + + (local + (defthm matcher-not-pair-args + (implies (and (not (variable-p t1)) + (not (second (pair-args t1 t2)))) + (not (equal (instance t1 sigma) t2))))) + + (local + (defthm matcher-assoc + (implies (and + (variable-p x) + (assoc x S) + (not (equal (val x sigma) (cdr (assoc x S))))) + (not (matcher sigma S))))) + +;;; The three main theorems of this subsubsection +;;; ············································· + + (defthm transform-subs-sel-preserves-matchers-1 + (implies + (and (not (normal-form-syst S-match)) + (matcher sigma (union-systems S-match))) + (matcher sigma (union-systems (transform-subs-sel S-match))))) + + (defthm transform-subs-sel-preserves-matchers-2 + (implies + (and (not (normal-form-syst S-match)) + (transform-subs-sel S-match) + (matcher sigma (union-systems (transform-subs-sel S-match)))) + (matcher sigma (union-systems S-match)))) + + (defthm transform-subs-sel-fail + (implies + (and (not (normal-form-syst S-match)) + (not (transform-subs-sel S-match))) + (not (matcher sigma (union-systems S-match))))))) + + + + +;;; ············································································ +;;; 1.2.3 (system-substitution (cdr S-match)) is an invariant in the rules +;;; of transformation. +;;; ············································································ + + + +(local + (encapsulate + () + + (local + (defthm not-assoc-not-member-domain + (implies (and + (system-substitution S) + (not (assoc x S))) + (not (member x (domain S)))))) + + + (defthm transform-subs-sel-preserves-system-substitution + (implies + (and (not (normal-form-syst S-match)) + (system-substitution (cdr S-match))) + (system-substitution (cdr (transform-subs-sel S-match))))))) + + +;;; ············································································ +;;; 1.2.4 Main property of the property system-substitution +;;; ············································································ + + +(local + (encapsulate + () + + (local + (defthm matcher-extended + (implies (and (matcher sigma s) + (not (member x (domain s))) + (system-substitution s)) + (matcher (cons (cons x term) sigma) s)))) + + (defthm system-substitutions-main-property + (implies (system-substitution S) + (matcher S S))))) + + +;;; ---------------------------------------------------------------------------- +;;; 1.3 Termination properties of transform-subs-sel +;;; ---------------------------------------------------------------------------- + +;;; Let's see that the rules of transformation decreases the length of +;;; the first system of the pair of systems + +(encapsulate + () + + (local + (defthm length-system-positive-if-consp + (implies (consp S) + (< 0 (length-system S))) + :rule-classes :linear)) + + (local + (defthm length-system-append + (equal (length-system (append s1 s2)) + (+ (length-system s1) (length-system s2))))) + + (local + (defthm eliminate-not-member + (implies (not (member x S)) + (equal (length-system (eliminate x S)) + (length-system S))) + :rule-classes (:rewrite :linear))) + + (local + (defthm length-system-eliminate + (implies (member e S) + (< (length-system (eliminate e S)) + (length-system S))) + :rule-classes :linear)) + + (local + (defthm length-system-eliminate-leq + (<= (length-system (eliminate e S)) + (length-system S)) + :rule-classes :linear)) + + (local + (defthm length-system-selection-and-delete-one-lemma + (implies (member x S) + (equal (length-system (cons x (delete-one x S))) + (length-system S))) + :rule-classes nil)) + + (local + (defthm length-system-selection-and-delete-one + (implies (consp (car S-match)) + (equal (length-system (car S-match)) + (length-system + (cons (a-pair (car S-match)) + (delete-one (a-pair (car S-match)) + (car S-match)))))) + :hints (("Goal" :use + (:instance length-system-selection-and-delete-one-lemma + (S (car S-match)) + (x (a-pair (car S-match)))))))) + +;;; NOTE: This is a very similar technique to use +;;; equal-set-selection-and-eliminate. Note that the same is not true with +;;; eliminate. But the following lemma relates both. + + (local + (defthm length-system-eliminate-delete-one-x + (<= (length-system (eliminate x S)) (length-system (delete-one x S))) + :rule-classes :linear)) + + (local + (defthm length-size-pair-args + (implies (second (pair-args args1 args2)) + (equal (length-system (first (pair-args args1 args2))) + (+ (length-term nil args1) + (length-term nil args2)))))) + +;;; And the main result: +;;; ···················· + + (defthm transform-subs-sel-decreases-length-of-first-system + (implies (not (normal-form-syst S-match)) + (o< (length-system (car (transform-subs-sel s-match))) + (length-system (car s-match)))))) + +;;; REMARK: This is non-local because will be used to prove admission of +;;; concrete subsumption algorithms by functional instantiation + + +;;; ---------------------------------------------------------------------------- +;;; 1.4 Guard verification: system-p for the first system and +;;; substitution-p for the second system are preserved +;;; ---------------------------------------------------------------------------- + +(local + (encapsulate + () +;;; *** + (local + (defthm system-s-p-variable-s-p + (implies (and (system-s-p S) + (member equ S) + (variable-p (car equ))) + (variable-s-p (car equ))))) + + (local + (defthm termp-s-p-member-system-s-p + (implies (and (system-s-p S) + (member equ S)) + (term-s-p (cdr equ))))) + + +;;; Closure properties: + + (defthm transform-subs-sel-preserves-system-s-p + (implies + (and (not (normal-form-syst S-match)) + (system-s-p (first S-match))) + (system-s-p (first (transform-subs-sel S-match))))) + + + (defthm transform-subs-sel-sel-preserves-substitution-s-p + (implies + (and (not (normal-form-syst S-match)) + (system-s-p (first S-match)) + (substitution-s-p (cdr S-match))) + (substitution-s-p (cdr (transform-subs-sel S-match))))))) + +;;; ----------------- + + +;;; ******* We have just "extracted" all the required knowledge of +;;; ******* transform-subs-sel + +(in-theory (disable transform-subs-sel)) + +;;; Other necessary disable: + +(local (in-theory (disable union-systems))) ; we will enable later + + + + +;;; ============================================================================ +;;; 2. Applying transformation rules until a solution (or nil) is found +;;; ============================================================================ + + +;;; ---------------------------------------------------------------------------- +;;; 2.1 Definition of subs-system-sel +;;; ---------------------------------------------------------------------------- + +(defun subs-system-sel (S-match) + (declare (xargs :measure (length-system (car S-match)))) + (if (normal-form-syst S-match) + S-match + (subs-system-sel (transform-subs-sel S-match)))) + + + +;;; ---------------------------------------------------------------------------- +;;; 2.2 Main properties of subs-system-sel +;;; ---------------------------------------------------------------------------- + +;;; subs-system-sel inherits the properties of transform-subs-sel + +;;; Technical lemma: + +(local + (defthm if-matchable-transform-subs-sel-success + (implies (subs-system-sel (transform-subs-sel S-match)) + (transform-subs-sel S-match)))) + + +;;; Three lemmas to state that the set of matchers is preserved by +;;; subs-system-sel +;;; ·········································································· + +(local + (defthm subs-system-sel-preserves-matchers-1 + (implies (matcher sigma (union-systems S-match)) + (matcher sigma (union-systems (subs-system-sel S-match)))))) + + +(local + (defthm subs-system-sel-preserves-matchers-2 + (implies (and (subs-system-sel S-match) + (matcher sigma (union-systems (subs-system-sel S-match)))) + (matcher sigma (union-systems S-match))))) + + +(local + (defthm subs-system-sel-fail + (implies (and (not (subs-system-sel S-match)) + (consp S-match)) + (not (matcher sigma (union-systems S-match)))))) + + +;;; REMARK: we don't need (consp S-match), but the proofs are shorter. + + +(in-theory (enable union-systems)) + +;;; subs-system-sel preserves the property of being a system-substitution. +;;; ·································································· + +(local + (defthm subs-system-sel-preserves-system-substitution + (implies (system-substitution (cdr S-match)) + (system-substitution (cdr (subs-system-sel S-match)))))) + +;;; Guard verification: a substitution-s-p is returned +;;; ··················································· + +(local + (defthm + subs-system-sel-substitution-s-p + (let* ((S (first S-match)) (match (cdr S-match)) + (subs-system-sel (subs-system-sel S-match)) + (matcher (cdr subs-system-sel))) + (implies (and (system-s-p S) (substitution-s-p match)) + (substitution-s-p matcher))) + :hints (("Goal" :induct (subs-system-sel S-match))))) + + + +;;; ============================================================================ +;;; 3. A (non-deterministic) matching algorithm for systems of equations +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 3.1 Definition of match-sel +;;; ---------------------------------------------------------------------------- + +(defun match-sel (S) + (let ((subs-system-sel (subs-system-sel (cons S nil)))) + (if subs-system-sel (list (cdr subs-system-sel)) nil))) + +;;; REMARK: To distinguish unsolvability (nil) from the empty +;;; substitution, we "pack" the result in a list. + +;;; ---------------------------------------------------------------------------- +;;; 3.2 Main properties of match-sel +;;; ---------------------------------------------------------------------------- + +;;; Technical lemma: + +(local + (defthm + in-normal-forms-S-is-matchable-by-any-sigma + (matcher sigma (first (subs-system-sel S-sol))))) + + +;;; The following properties are inmediate consequence of those given in +;;; 2.2 for subs-system-sel + +(defthm match-sel-soundness + (implies (match-sel S) + (matcher (first (match-sel S)) S)) + :rule-classes nil + :hints + (("Goal" :use + (:instance subs-system-sel-preserves-matchers-2 + (S-match (cons S nil)) + (sigma (first (match-sel S))))))) + + +(defthm match-sel-completeness + (implies (matcher sigma S) + (match-sel S)) + :rule-classes nil + :hints + (("Goal" :use + (:instance subs-system-sel-fail (S-match (cons S nil)))))) + + +;;; Closure property: This theorem is needed for guard verification. + + +(defthm match-sel-substitution-s-p + (implies (system-s-p S) + (substitution-s-p (first (match-sel S)))) + :hints (("Goal" :use + (:instance + subs-system-sel-substitution-s-p + (S-match (cons S nil)))))) + + + +;;; We disable match-sel + +(local (in-theory (disable match-sel))) + +;;; ============================================================================ +;;; 4. A (non-deterministic) subsumption algorithm (matching of two terms) +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 4.1 Definition of matching-sel and subs-sel. +;;; ---------------------------------------------------------------------------- + + +(defun subs-sel (t1 t2) + (match-sel (list (cons t1 t2)))) + + + +(defun matching-sel (t1 t2) + (first (subs-sel t1 t2))) + +;;; REMARK: subs-sel checks the subsumption relation between to +;;; terms. If non-nil is a list containing a matching substitution as +;;; its firs element. + + +;;; ---------------------------------------------------------------------------- +;;; 4.2 Soundness and completeness of the subsumption algorithm +;;; ---------------------------------------------------------------------------- + +;;; Soundness +;;; ········· + + +(defthm subs-sel-soundness + (implies (subs-sel t1 t2) + (equal (instance t1 (matching-sel t1 t2)) t2)) + + :rule-classes nil + :hints (("Goal" :use + (:instance match-sel-soundness (S (list (cons t1 t2))))))) + + + +;;; Completeness +;;; ············ + + +(defthm subs-sel-completeness + (implies (equal (instance t1 sigma) t2) + (subs-sel t1 t2)) + :rule-classes nil + :hints (("Goal" :use + (:instance match-sel-completeness (S (list (cons t1 t2))))))) + + + +;;; Closure property: +;;; (the following theorem is needed for guard verification) +;;; ························································ + + +(defthm matching-sel-substitution-s-p + (implies (and (term-s-p t1) (term-s-p t2)) + (substitution-s-p (matching-sel t1 t2)))) + + +;;; SOME CONCLUSIONS: +;;; ================= + +;;; A comparison is made w.r.t. the more classical definition of a +;;; subsumption algorithm given in the book subsumption-definition-v0.lisp + +;;; ADVANTAGES of this rule-based approach: + +;;; 1) Several selection strategies could be implemented. A family of +;;; algorithms has been verified. +;;; 2) Less intermediate concepts are needed (extension, +;;; coincide,...). This proof seems easier (although I'm now more +;;; trained with the prover). +;;; 3) A common methodlogy with the verification of a rule-based +;;; unification algorithm is used. + + +;;; ADVANTAGES of the classical recursive definition: + +;;; 1) At the same time, the algorithm for terms and for lists of terms +;;; is verified (nevertheless, the rule-based algorithm can be adapted +;;; to deal with subsumption of lists of terms). + + + + + diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/mg-instance.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/mg-instance.lisp new file mode 100644 index 0000000..1c7f1c4 --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/mg-instance.lisp @@ -0,0 +1,372 @@ +;;; mg-instance.lisp +;;; Proof of the existence of a least upper bound - lub - (most general +;;; instance - mgi -) of two terms with respect to the subsumption +;;; relation. +;;; Creation: 24-10-99. Last revision: 11-12-2000 +;;; ================================================================= + +#| To certify this book: + +(in-package "ACL2") + +(certify-book "mg-instance") + +|# + +(in-package "ACL2") +(include-book "renamings") +(include-book "unification") + +;;; ********************************** +;;; MOST GENERAL INSTANCE OF TWO TERMS +;;; ********************************** + +;;; We prove here that, given two terms, there exists a most +;;; general instance (if they are unifiable). We will define such most +;;; general instance in the following way: +;;; "Given t1 and t2 we rename their variables in order to get their +;;; set of variables disjoint. Let t1' and t2' the respective renamed +;;; versions of t1 and t2. Let sigma = (mgu t1' t2') (if they are +;;; unifiable). Then sigma(t1') is a more general instantiation (a +;;; least upper bound w.r.t. subsumption) of t1 and t2. If t1' and t2' +;;; are not unifiable, there are no common instance of t1 and t2." + +;;; ============================================================================ +;;; 1. Most general instance +;;; ============================================================================ + +;;; Needed for guard verification +(local + (defthm substitution-p-alistp + (implies (substitution-p sigma) + (alistp sigma)))) + + +;;; ===== MG-INSTANCE-MV + +(defun mg-instance-mv (t1 t2) + (declare (xargs :guard (and (term-p t1) (term-p t2)))) + (let ((rename-t1 (number-rename t1 0 -1)) + (rename-t2 (number-rename t2 1 1))) + (mv-let (mgu unifiable) + (mgu-mv rename-t1 rename-t2) + (if unifiable + (mv (instance rename-t1 mgu) t) + (mv nil nil))))) + +;;; REMARK: We use multi-values to distinguish the variable term "nil" +;;; from nil. Although our concrete implementation of mgu-mv makes +;;; impossible to return the term "nil" as the first element of the +;;; result returned by mg-instance-mv (since we have numeric variables), +;;; we use multivalues because we are only using the fundamental +;;; properties given in unification.lisp + +;;; Closure property: + +(local + (defthm mg-instance-mv-term-s-p + (implies (and (term-s-p t1) (term-s-p t2)) + (term-s-p (first (mg-instance-mv t1 t2)))))) + +;;; Guard verification: + +(local + (defthm mg-instance-mv-term-p + (implies (and (term-p t1) (term-p t2)) + (term-p (first (mg-instance-mv t1 t2)))) + :hints (("Goal" :use (:functional-instance + mg-instance-mv-term-s-p + (signat (lambda (x n) (eqlablep x))) + (term-s-p-aux term-p-aux) + (substitution-s-p substitution-p)))))) + + +;;; ============================================================================ +;;; 2. Properties of mg-instance-mv for renamings +;;; ============================================================================ + +;;; GOAL. In this section we want to prove: + +;;; * If (second (mg-instance-mv t1 t2)), then: +;;; (1) and (2): (first (mg-instance-mv t1 t2)) is a common instance of +;;; (number-rename t1 1 1) and (number-rename t2 0 -1). +;;; (4): (first (mg-instance-mv t1 t2)) is a most general instance of +;;; (number-rename t1 1 1) and (number-rename t2 0 -1). + +;;; * If (not (second (mg-instance-mv t1 t2))): +;;; (3): There are no common instance of (number-rename t1 1 1) and +;;; (number-rename t2 0 -1). + + +;;; IMPORTANT REMARK: Since we are going to work with renamed terms, +;;; we disable renamed-implies-iff-subs-1 and renamed-implies-iff-subs-2 + +(local + (in-theory (disable renamed-implies-iff-subs-1 renamed-implies-iff-subs-2))) + +;;; And also the following rule: +(local (in-theory (disable subsumption-apply-subst))) + + +;;; ---------------------------------------------------------------------------- +;;; 2.1 (number-rename t1 0 -1) subsumes (first (mg-instance-mv t1 t2)) +;;; ---------------------------------------------------------------------------- + +(local + (defthm mg-instance-mv-subsumes-rename-1 + (implies (second (mg-instance-mv t1 t2)) + (subs (number-rename t1 0 -1) (first (mg-instance-mv t1 t2)))) + :hints (("Goal" + :use (:instance + subs-completeness + (t1 (number-rename t1 0 -1)) + (t2 (first (mg-instance-mv t1 t2))) + (sigma (mgu (number-rename t1 0 -1) + (number-rename t2 1 1)))))))) + + +;;; ---------------------------------------------------------------------------- +;;; 2.2 (number-rename t2 1 1) subsumes (first (mg-instance-mv t1 t2)) +;;; ---------------------------------------------------------------------------- + + +(local + (defthm mg-instance-mv-subsumes-rename-2 + (implies (second (mg-instance-mv t1 t2)) + (subs (number-rename t2 1 1) (first (mg-instance-mv t1 t2)))) + :hints (("Goal" :use + ((:instance + subs-completeness + (t1 (number-rename t2 1 1)) + (t2 (first (mg-instance-mv t1 t2))) + (sigma (mgu (number-rename t1 0 -1) + (number-rename t2 1 1))))))))) + + + +;;; ---------------------------------------------------------------------------- +;;; 2.3 Disjoint union of two substitution: definition and main property +;;; ---------------------------------------------------------------------------- + + +;;; ====== DISJOINT-UNION-SUBST +;;; Given two terms t1 and t2 and two substitutions sigma1 and sigma2 , +;;; we append the restriction of sigma1 and sigma2 to the variables of +;;; (number-rename t1 0 -1) and (number-rename t2 1 1) + +(local + (defun disjoint-union-subst (sigma1 sigma2 t1 t2) + (append (restriction sigma1 (variables t (number-rename t1 0 -1))) + (restriction sigma2 (variables t (number-rename t2 1 1)))))) + + +;;;; Main property of (disjoint-union-subst sigma1 sigma2 t1 t2): +;;; (disjoint-union-subst sigma1 sigma2 t1 t2) is an unifier of t1r and t2r. + +(local + (defthm disjoint-union-subst-unifier + (implies (equal (instance (number-rename t1 0 -1) sigma1) + (instance (number-rename t2 1 1) sigma2)) + (equal (instance (number-rename t2 1 1) + (disjoint-union-subst sigma1 sigma2 t1 t2)) + (instance (number-rename t1 0 -1) + (disjoint-union-subst sigma1 sigma2 t1 t2)))))) + + + + + +;;; REMARK: Strategy in the following to prove (3) and (4): + +;;; Let t1r = (number-rename t1 0 -1) and t2r = (number-rename t2 1 1): + +;;; If term is an upper bound of t1r and t2r, we have to prove that +;;; (first (mg-instance-mv t1 t2)) subsumes term (whenever +;;; (second (mg-instance-mv t1 t2)) + +;;; We will prove it +;;; - (first (mg-instance-mv t1 t2)) is (instance t1r unifier) and +;;; - term is (instance t1r sigma12 ) +;;; where sigma12 is the disjoint union of the two matching substitution +;;; for t1r and term and t2r and term, respectively. +;;; - sigma12 is an unifier of t1r and t2r, so unifier subsumes sigma12 +;;; using the lemma subs-sust-main-property (see +;;; subsumption-subst.lisp) + + + + +;;; ---------------------------------------------------------------------------- +;;; 2.4 (mg-instance-mv t1 t2) does not fail if there exists a common instance +;;; ---------------------------------------------------------------------------- + +;;; A lemma before disabling disjoint-union-subst: + +(local + (defthm + if-there-is-a-common-instance-of-renamings-then-unify + (implies (equal (instance (number-rename t1 0 -1) sigma1) + (instance (number-rename t2 1 1) sigma2)) + (unifiable (number-rename t1 0 -1) (number-rename t2 1 1))) + :hints (("Goal" :use + (:instance + mgu-completeness + (sigma (disjoint-union-subst sigma1 sigma2 t1 t2)) + (t1 (number-rename t1 0 -1)) + (t2 (number-rename t2 1 1))))))) + + + +;;; Main lemma for (3) +;;; The same as the previous lemma, but using subsumption. + +(local + (defthm + if-subsume-common-therm-mg-instance-mv + (implies (and (subs (number-rename t1 0 -1) term) + (subs (number-rename t2 1 1) term)) + (second (mg-instance-mv t1 t2))) + :hints (("Goal" :use + (:instance + if-there-is-a-common-instance-of-renamings-then-unify + (sigma1 (matching (number-rename t1 0 -1) term)) + (sigma2 (matching (number-rename t2 1 1) term))))))) + + +;;; We disable disjoint-union-subst +(local (in-theory (disable disjoint-union-subst))) + + + + +;;; ---------------------------------------------------------------------------- +;;; 2.5 mg-instance-mv is a most general instance of the renamed terms +;;; ---------------------------------------------------------------------------- + +;;; An important lemma: +;;; mgu of t1r and t2r subsumes disjoint union of matching substitutions + +(local + (defthm subsumption-sust-mgu-disjoint-union + (implies (equal (instance (number-rename t1 0 -1) sigma1) + (instance (number-rename t2 1 1) sigma2)) + (subs-subst (mgu (number-rename t1 0 -1) (number-rename t2 1 1)) + (disjoint-union-subst sigma1 sigma2 t1 t2))))) + + +;;; A bridge lemma: + +(local + (defthm mg-instance-mv-lub-rename-bridge-lemma + (implies (equal (instance (number-rename t1 0 -1) sigma1) + (instance (number-rename t2 1 1) sigma2)) + (subs (first (mg-instance-mv t1 t2)) + (instance (number-rename t1 0 -1) + (disjoint-union-subst sigma1 sigma2 t1 t2)))) + :rule-classes nil + :hints (("Goal" :in-theory (disable mgu-soundness))))) + +;;;; We disable mg-instance-mv +(in-theory (disable mg-instance-mv)) + + +;;; (4) +;;; mg-instance-mv is a most general instance of the renamed terms + +(local + (defthm mg-instance-mv-lub-rename + (implies (and (subs (number-rename t1 0 -1) term) + (subs (number-rename t2 1 1) term)) + (subs (first (mg-instance-mv t1 t2)) term)) + :hints (("Goal" :use + (:instance mg-instance-mv-lub-rename-bridge-lemma + (sigma1 (matching (number-rename t1 0 -1) term)) + (sigma2 (matching (number-rename t2 1 1) term))) + :in-theory (enable disjoint-union-subst))))) + + +;;; REMARK: The results (1), (2), (3) and (4) are enough to show that +;;; every pair of unifiable terms have a most general instance of their +;;; renamed versions. We can easily translate these properties to the +;;; original terms, using the fact that renamed versions are equivalent +;;; w.r.t. subsumption to the original term. For that purpose we enable +;;; again the congruence rules. + +(local + (in-theory + (enable renamed-implies-iff-subs-1 renamed-implies-iff-subs-2))) + + + +;;; ============================================================================ +;;; 3. mg-instance: definition and non-local properties. +;;; ============================================================================ + + + +(defun mg-instance (t1 t2) + (declare (xargs :guard (and (term-p t1) (term-p t2)))) + (mv-let (mg-instance bool) + (mg-instance-mv t1 t2) + (if bool + (number-rename mg-instance 1 1) + nil))) + + +;;; REMARK: We also rename the result given by mg-instance-mv. This is +;;; for two reassons: +;;; - Pretty printing +;;; - In this way, mg-instance returns nil ONLY WHEN mg-instance-mv +;;; fails. So we no longer need multivalues. + +(defthm mg-instance-subsumes-rename-1 + (implies (mg-instance t1 t2) + (subs t1 (mg-instance t1 t2))) + + :hints (("Goal" :use mg-instance-mv-subsumes-rename-1))) + + +(defthm mg-instance-subsumes-rename-2 + (implies (mg-instance t1 t2) + (subs t2 (mg-instance t1 t2))) + + :hints (("Goal" :use mg-instance-mv-subsumes-rename-2))) + + +(defthm + if-subsume-common-therm-mg-instance + (implies (and (subs t1 term) + (subs t2 term)) + (mg-instance t1 t2)) + + :hints + (("Goal" + :use if-subsume-common-therm-mg-instance-mv))) + +(defthm mg-instance-lub + (implies (and (subs t1 term) + (subs t2 term)) + (subs (mg-instance t1 t2) term)) + :hints (("Goal" :use (mg-instance-mv-lub-rename + if-subsume-common-therm-mg-instance-mv)))) + +;;; Closure property: +(defthm mg-instance-term-s-p + (implies (and (term-s-p t1) (term-s-p t2)) + (term-s-p (mg-instance t1 t2)))) + +;;; Needed for guard verification: +(defthm mg-instance-term-p + (implies (and (term-p t1) (term-p t2)) + (term-p (mg-instance t1 t2)))) +;;; REMARK: We could have obtained this by functional instantiation of the +;;; previous lemma, but it is also a trivial consequence of +;;; mg-instance-mv-term-p + +;;; Now we disable mg-instance. + +(in-theory (disable mg-instance (mg-instance))) + + + + diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/renamings.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/renamings.lisp new file mode 100644 index 0000000..7bf9152 --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/renamings.lisp @@ -0,0 +1,1016 @@ +;;; renamings.lisp +;;; Renamings variables of a term. Renamings substitutions. Properties. +;;; Created 24-10-99. Last modified: 15-02-2001 +;;; ============================================================================= + + +#| To certify this book: + +(in-package "ACL2") + +(certify-book "renamings") + +|# + +(in-package "ACL2") +(include-book "subsumption") + + +;;; ****************************************************** +;;; RENAMING SUBSTITUTIONS. THE "RENAMED" EQUIVALENCE. +;;; A PARTICULAR RENAMING: NUMBER-RENAME +;;; ****************************************************** + +;;; In this book: +;;; - The equivalence relation "renamed": one term t1 is a renamed version +;;; of t2 if (subs t1 t2) and (subs t2 t1). +;;; - Definition of the concept of renaming substitutions and the main +;;; property of renamings with respect to the renamed equivalence: t2 is +;;; a renamed version of t1 iff there exists a renaming s.t. its +;;; domain contains the variables of t1 and applied to t1 is equal to +;;; t2. +;;; - Definition and properties of a particular kind of renaming +;;; (number-renaming) and guard verification. This "number-renaming" +;;; will be defined for terms and for lists of terms. + + +;;; ============================================================================ +;;; 1. The "renamed" equivalence +;;; ============================================================================ + +;;; ====== RENAMED + +(defun renamed (t1 t2) + (if (subs t1 t2) + (if (subs t2 t1) t nil) + nil)) + +(defequiv renamed + :hints (("Goal" :in-theory + (enable subsumption-transitive)))) + +;;; And congruences: + +(defcong renamed iff (subs t1 t2) 1 + :hints (("Goal" :in-theory + (enable subsumption-transitive)))) + +(defcong renamed iff (subs t1 t2) 2 + :hints (("Goal" :in-theory + (enable subsumption-transitive)))) + + + +;;; ============================================================================ +;;; 2. Renaming variables: definition and properties. +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 2.1 Definition +;;; ---------------------------------------------------------------------------- + +;;; ======= VARIABLE-SUBSTITUTION + +(defun variable-substitution (sigma) + (if (atom sigma) + t + (and (variable-p (cdar sigma)) + (variable-substitution (cdr sigma))))) + +(local + (defthm variable-substitution-value-variable-p + (implies (and (variable-substitution sigma) + (variable-p term)) + (variable-p (val term sigma))))) + +;;; ======= RENAMING + +(defun renaming (sigma) + (and (variable-substitution sigma) + (setp (co-domain sigma)))) + + +;;; In the following, we will prove the main property of renamings: "t2 +;;; is a renamed version of t1 iff there exists a renaming sigma +;;; s.t. its domain is a set containing the variables of t1 and that +;;; applied to t1 is equal to t2" + + +;;; ---------------------------------------------------------------------------- +;;; 2.2 Renaming implies renamed +;;; ---------------------------------------------------------------------------- + + +;;; ············································································ +;;; 2.2.1 An important lemma +;;; ············································································ + +;;; We will show that the inverse substitution of a renaming is its +;;; inverse function, in some sense. + +(encapsulate + () + + (local + (defthm val-val-inverse-lemma + (implies (and + (member x (domain sigma)) + (equal (val x sigma) y)) + (member y (co-domain sigma))))) + +;;; If sigma is a substitution such that its co-domain is a set of +;;; variables, then sigma^{-1}(sigma(x)) = x, for all x in +;;; domain(sigma). Remeber that a renaming is a substitution such that +;;; its co-domain are sets of variables (no duplicated +;;; elements) + + (local + (defthm val-val-inverse-renaming + (implies (and (renaming sigma) + (member x (domain sigma))) + (equal (val (val x sigma) (inverse sigma)) x)))) + +;;; The main theorem: +;;; If the variables of t1 are in the domain of sigma, then +;;; sigma^{-1}(sigma(t1)) = t1, whenever sigma is a substitution with a +;;; set of variables as its co-domain. This theorema will be needed also +;;; in subsumption-well-founded.lisp + + (defthm renaming-inverse + (implies (and + (renaming sigma) + (subsetp (variables flg term) (domain sigma))) + (equal + (apply-subst flg (inverse sigma) (apply-subst flg sigma term)) + term)))) + + +;;; ············································································ +;;; 2.2.2 And the intended property +;;; ············································································ + + +(defthm renaming-implies-renamed + (implies (and + (renaming sigma) + (subsetp (variables t term) (domain sigma))) + (renamed (instance term sigma) term)) + :hints (("Goal" :use (:instance subs-completeness + (t1 (instance term sigma)) + (t2 term) + (sigma (inverse sigma)))))) + +;;; ---------------------------------------------------------------------------- +;;; 2.3 Renamed implies renaming +;;; ---------------------------------------------------------------------------- + +;;; We will show that when (subs t1 t2) and (subs t2 t1), then +;;; (normal-form-subst t (matching t1 t2) t1) is a renaming s.t. +;;; applied to t1 is equal to t2. + +;;; Note that the condition (subs term t2) and (subs t2 term) can be +;;; stated in terms of apply-subst: that is the same to say that +;;; there exists two substitutions sigma and delta such that: +;;; (equal (apply-subst flg delta (apply-subst flg sigma term)) +;;; term) + +;;; Let sigmar = (normal-form-subst flg sigma term). We have to prove +;;; the two following properties: +;;; * (variable-substitution sigmar) +;;; * (co-domain sigmar) is a setp. + + +;;; ············································································ +;;; 2.3.1 sigmar is a variable-substitution +;;; ············································································ + +(local + (encapsulate + () + + (local + (defthm renamed-implies-variable-val-lemma + (implies (and flg (variable-p (apply-subst flg delta (val term sigma)))) + (variable-p (val term sigma))) + :rule-classes nil)) + + + (local + (defthm renamed-implies-variable-val + (implies (and + (equal (apply-subst flg delta (apply-subst flg sigma term)) + term) + (member x (variables flg term))) + (variable-p (val x sigma))) + :hints (("Subgoal *1/1" + :use renamed-implies-variable-val-lemma)))) + + (local + (defthm renamed-implies-variable-substitution-main-lemma + (implies (and + (equal (apply-subst flg delta (apply-subst flg sigma term)) + term) + (subsetp l (variables flg term))) + (variable-substitution (restriction sigma l))) + :hints (("Goal" :induct (len l))))) + + (defthm renamed-implies-variable-substitution + (implies + (equal (apply-subst flg delta (apply-subst flg sigma term)) term) + (variable-substitution (normal-form-subst flg sigma term))) + :hints (("Goal" :use + (:instance renamed-implies-variable-substitution-main-lemma + (l (make-set (variables flg term))))))))) + +;;; ············································································ +;;; 2.3.2 An important lemma +;;; ············································································ + +;;; When (equal (apply-subst flg delta (apply-subst flg sigma term)) +;;; term) then two different variables of term cannot have the the value +;;; with respect to sigma + + +(local + (encapsulate + () + + (local + (defthm renamed-implies-injective-val-lemma + (implies (and + (equal (instance (val x sigma) delta) x) + (equal (instance (val y sigma) delta) y) + (not (equal x y))) + (not (equal (val x sigma) (val y sigma)))) + :rule-classes nil)) + + (local + (defthm identity-on-term-identity-val + (implies (and + (equal (apply-subst flg delta (apply-subst flg sigma term)) + term) + (member x (variables flg term))) + (equal (instance (val x sigma) delta) x)) + :rule-classes nil)) + + (defthm renamed-implies-injective-val + (implies (and + (equal (apply-subst flg delta (apply-subst flg sigma term)) + term) + (member x (variables flg term)) + (member y (variables flg term)) + (not (equal x y))) + (not (equal (val x sigma) (val y sigma)))) + :hints (("Goal" :use ((:instance renamed-implies-injective-val-lemma) + (:instance identity-on-term-identity-val) + (:instance identity-on-term-identity-val + (x y)))))))) + + +;;; ············································································ +;;; 2.3.2 co-domain of sigmar is a setp +;;; ············································································ + + + +(local + (encapsulate + + () + + (local + (defthm renamed-implies-setp-codomain-main-lemma + (implies (and + (equal (apply-subst flg delta (apply-subst flg sigma term)) + term) + (setp l) + (subsetp l (variables flg term))) + (setp (co-domain (restriction sigma l)))) + :hints (("Goal" :induct (setp l)) + ("Subgoal *1/2'4'" :induct (len l2))))) + + + (defthm renamed-implies-setp-codomain + (implies + (equal (apply-subst flg delta (apply-subst flg sigma term)) term) + (setp (co-domain (normal-form-subst flg sigma term)))) + :hints (("Goal" :use + (:instance renamed-implies-setp-codomain-main-lemma + (l (make-set (variables flg term))))))))) + +;;; ············································································ +;;; 2.3.3 sigmar is a renaming +;;; ············································································ + +(local + (defthm renamed-implies-renaming-main-lemma + (implies + (equal (apply-subst flg delta (apply-subst flg sigma term)) term) + (renaming (normal-form-subst flg sigma term))) + :rule-classes nil)) + + +(defthm renamed-implies-renaming + (let ((ren (normal-form-subst t (matching t1 t2) t1))) + (implies (renamed t1 t2) + (and (renaming ren) + (equal (instance t1 ren) t2)))) + :hints (("Goal" :use + (:instance renamed-implies-renaming-main-lemma + (term t1) (sigma (matching t1 t2)) + (delta (matching t2 t1)) + (flg t))))) + + +;;; ============================================================================ +;;; 3. Number renamings: a special kind of renaming. +;;; ============================================================================ + +;;; We will define number-renaming. We rename the term enumerating the +;;; variables, starting from a given number x and incrementing by y. + + +;;; ---------------------------------------------------------------------------- +;;; 3.1 Number renaming. +;;; ---------------------------------------------------------------------------- + + +;;; As we said before, this is a special kind of renaming. Every +;;; variable is substituted in a sound way for a number. This could be +;;; done very easiliy in two rounds. First compute the renaming +;;; substitution and then apply the renaming to obtain the renamed +;;; version of the term. Since this will be a procedure to apply very +;;; often, we implement here in a more eficcient way: the renaming and +;;; the renamed term are computed at the same time. + +;;; The definition: + +(defun number-rename-aux (flg term sigma x y) + (declare (xargs :guard (and (term-p-aux flg term) + (acl2-numberp x) + (acl2-numberp y) + (alistp-acl2-numberp sigma)) + :verify-guards nil)) + (if flg + (if (variable-p term) + (let ((find-term (assoc term sigma))) + (if find-term + (mv (cdr find-term) sigma) + (let ((z (if (endp sigma) x (+ y (cdar sigma))))) + (mv z (cons (cons term z) sigma))))) + (mv-let (renamed-args renaming-args) + (number-rename-aux nil (cdr term) sigma x y) + (mv (cons (car term) renamed-args) renaming-args))) + (if (endp term) + (mv term sigma) + (mv-let (renamed-car renaming-car) + (number-rename-aux t (car term) sigma x y) + (mv-let (renamed-cdr renaming-cdr) + (number-rename-aux nil (cdr term) renaming-car x y) + (mv (cons renamed-car renamed-cdr) + renaming-cdr)))))) +;;; REMARK : x is only needed when sigma is endp and no +;;; longer. It can be considered as a constant. + + + + +;;; Guard verification + +(local + (defthm alistp-acl2-numberp-alistp + (implies (alistp-acl2-numberp l) + (alistp l)) + :rule-classes :forward-chaining)) + +(local + (defthm alistp-acl2-numberp-second-number-rename-aux + (implies (and (alistp-acl2-numberp sigma) + (acl2-numberp x)) + (alistp-acl2-numberp + (second (number-rename-aux flg term sigma x y)))))) + + +(verify-guards number-rename-aux) + +;;; ---------------------------------------------------------------------------- +;;; 3.2 Number-rename-aux: closure properties +;;; ---------------------------------------------------------------------------- +;;; The results in this subsection are needed for further guard +;;; verification of functions using number-rename-aux and for the proof +;;; of closure properties of number-rename + + + +(local + (defthm number-rename-aux-substitution-s-p + (implies (and (acl2-numberp x) + (term-s-p-aux flg term) + (substitution-s-p sigma)) + (substitution-s-p + (second (number-rename-aux flg term sigma x y)))))) + +;;; Needed for closure property: + + +(local + (encapsulate + () + + (local + (defthm number-rename-aux-equal-len + (equal (len (first (number-rename-aux nil term sigma x y))) + (len term)))) + + (defthm number-rename-aux-term-s-p-aux + (implies (and (acl2-numberp x) + (term-s-p-aux flg term) + (alistp-acl2-numberp sigma)) + (term-s-p-aux + flg (first (number-rename-aux flg term sigma x y))))))) + + + + +;;; ---------------------------------------------------------------------------- +;;; 3.3 Number-rename-aux: main properties. +;;; ---------------------------------------------------------------------------- + +;;; ············································································ +;;; 3.3.1 Previous (local) lemmas about coincide. +;;; ············································································ + +;;; We will need these lemmas because we are going to talk about +;;; extensions (see the definition in terms.lisp, subsection 2.3) + +;;; ====== COINCIDE. See definition and properties in terms.lisp + +(local + (encapsulate + () + + (local + (defthm coincide-main-property + (implies (and (coincide sigma1 sigma2 l) + (member x l)) + (equal (equal (val x sigma1) (val x sigma2)) t)))) + +;;; REMARK: The form of the rule avoids non-termination +;;; This rule is also local in terms.lisp. We don't want terms.lisp to +;;; export everywhere. That's the reason why we repeat here the rule. + + + (defthm coincide-conmutative + (implies (coincide a b l) + (coincide b a l))) + + + (in-theory (disable coincide-conmutative)) + + (defthm coincide-cons + (implies (and + (not (member x l)) + (coincide sigma sigma1 l)) + (coincide (cons (cons x y) sigma) sigma1 l))) + + + (defthm coincide-subsetp-transitive + (implies (and (coincide sigma sigma1 l) + (coincide sigma1 sigma2 m) + (subsetp l m)) + (coincide sigma sigma2 l))) + + (in-theory (disable coincide-subsetp-transitive)))) + + +;;; ············································································ +;;; 3.3.2 Previous (local) lemmas about acl2-numberp-list-increment +;;; ············································································ + +;;; We will define and prove some local properties of the concept of +;;; being a list of numbers l such that each of its elements is obtained +;;; incrementing the previous one by a constant y. + +;;; ====== ACL2-NUMBERP-LIST-INCREMENT + +(local + (defun acl2-numberp-list-increment (l y) + (cond ((endp l) t) + ((endp (cdr l)) (acl2-numberp (first l))) + (t (and (acl2-numberp (first l)) + (= y (- (first l) (second l))) + (acl2-numberp-list-increment (cdr l) y)))))) + +(local + (encapsulate + () + + (local + (defthm acl2-numberp-list-increment-setp-1-lema + (implies (and (acl2-numberp-list-increment l y) + (consp l) + (> y 0) + (> x (first l))) + (not (member x l))))) + + (local + (defthm acl2-numberp-list-increment-setp-1 + (implies (and (acl2-numberp-list-increment l y) + (> y 0)) + (setp l)))) + + (local + (defthm acl2-numberp-list-increment-setp-2-lema + (implies (and (acl2-numberp-list-increment l y) + (consp l) + (< y 0) + (< x (first l))) + (not (member x l))))) + + (local + (defthm acl2-numberp-list-increment-setp-2 + (implies (and (acl2-numberp-list-increment l y) + (< y 0)) + (setp l)))) + + + (defthm acl2-numberp-list-increment-setp + (implies (and (acl2-numberp-list-increment l y) + (not (= y 0))) + (setp l)) + :hints (("Goal" :cases ((> y 0) (< y 0))))))) + + + +;;; ············································································ +;;; 3.3.3 number-rename-aux: properties of the variables of the returned term +;;; ············································································ + +;;; We will prove that (first (number-rename-aux flg term sigma x y) is a +;;; term having numeric variables, and: +;;; * if y>0, they are greater than x +;;; * if y<0, they are smaller than x + +;;; ===== ACL2-NUMBERP-LIST-SMALLER-THAN + +(defun acl2-numberp-list-smaller-than (l x) + (if (endp l) + t + (and (acl2-numberp (first l)) + (<= (first l) x) (acl2-numberp-list-smaller-than (cdr l) x)))) + +;;; ===== ACL2-NUMBERP-LIST-BIGGER-THAN + +(defun acl2-numberp-list-bigger-than (l x) + (if (endp l) + t + (and + (acl2-numberp (first l)) + (>= (first l) x) (acl2-numberp-list-bigger-than (cdr l) x)))) + + +(local + (encapsulate + () + + (local + (defthm acl2-numberp-list-bigger-than-append + (iff (acl2-numberp-list-bigger-than (append l1 l2) x) + (and (acl2-numberp-list-bigger-than l1 x) + (acl2-numberp-list-bigger-than l2 x))))) + + (defthm number-renamed-aux-variables->=-x + (implies (and (acl2-numberp-list-bigger-than (co-domain sigma) x) + (> y 0) + (acl2-numberp x)) + (and + (acl2-numberp-list-bigger-than + (variables + flg (first (number-rename-aux flg term sigma x y))) x) + (acl2-numberp-list-bigger-than + (co-domain + (second (number-rename-aux flg term sigma x y))) x)))) + + + (local + (defthm acl2-numberp-list-smaller-than-append + (iff (acl2-numberp-list-smaller-than (append l1 l2) x) + (and (acl2-numberp-list-smaller-than l1 x) + (acl2-numberp-list-smaller-than l2 x))))) + + (defthm number-renamed-aux-variables-<=-x + (implies (and (acl2-numberp-list-smaller-than (co-domain sigma) x) + (< y 0) + (acl2-numberp x)) + (and + (acl2-numberp-list-smaller-than + (variables + flg (first (number-rename-aux flg term sigma x y))) x) + (acl2-numberp-list-smaller-than + (co-domain + (second (number-rename-aux flg term sigma x y))) x)))))) + + +;;; ············································································ +;;; 3.3.4 number-rename-aux: Main property of the co-domain of the +;;; returned substitution. +;;; ············································································ + + +(local + (defthm number-rename-co-domain-acl2-numberp-list-increment + (implies (and (acl2-numberp-list-increment (co-domain sigma) y) + (acl2-numberp x) + (acl2-numberp y)) + (acl2-numberp-list-increment + (co-domain (second (number-rename-aux flg term sigma x y))) y)))) + +;;; ············································································ +;;; 3.3.5 number-rename-aux: the substitution returned is a renaming +;;; ············································································ + + +(local + (encapsulate + () + + (local + (defthm acl2-numberp-list-increment-implies-variable-substitution + (implies (acl2-numberp-list-increment (co-domain sigma) y) + (variable-substitution sigma)))) + + (local + (defthm acl2-numberp-list-increment-implies-renaming + (implies (and + (acl2-numberp-list-increment (co-domain sigma) y) + (acl2-numberp y) + (not (= y 0))) + (renaming sigma)))) + + + (defthm number-rename-renaming + (implies (and (acl2-numberp x) (acl2-numberp y) (not (= y 0))) + (renaming (second (number-rename-aux flg term nil x y)))) + :hints (("Goal" :use (:instance + acl2-numberp-list-increment-implies-renaming + (sigma + (second + (number-rename-aux flg term nil x y))))))))) + + + +;;; ············································································ +;;; 3.3.3 Subsumption properties of number-rename-aux +;;; ············································································ + + +;;; 3.3.3.1 +;;; The substituion returned by number-rename-aux, applied to the input +;;; term returns the returned term (i.e term subsumes the +;;; number-rename-aux term) +;;; ·········································································· + +;;; Two previos lemmas: + + +(local + (defthm number-rename-invariants + (let ((number-renaming-aux + (second (number-rename-aux flg t1 sigma x y)))) + (implies (alistp sigma) + (and + (alistp number-renaming-aux) + (subsetp (domain sigma) (domain number-renaming-aux)) + (extension number-renaming-aux sigma) + (subsetp (variables flg t1) (domain number-renaming-aux))))) + :hints (("Goal" + :in-theory (enable + subsetp-transitive + coincide-conmutative + coincide-subsetp-transitive))))) + +(local + (defthm number-rename-incremental + (implies (alistp sigma) + (equal (apply-subst + flg1 + (second (number-rename-aux + flg2 t2 + (second (number-rename-aux + flg1 t1 sigma x1 y1)) x2 y2)) + t1) + (apply-subst + flg1 + (second (number-rename-aux flg1 t1 sigma x1 y1)) + t1))) + :hints (("Goal" :use + (:instance coincide-in-term + (flg flg1) + (sigma2 + (second + (number-rename-aux + flg2 t2 + (second (number-rename-aux flg1 t1 sigma x1 y1)) + x2 y2))) + (term t1) + (sigma1 + (second (number-rename-aux flg1 t1 sigma x1 y1))) + (l + (domain + (second + (number-rename-aux flg1 t1 sigma x1 y1))))))))) + + +;;; And the main result: +(local + (defthm term-subsumes-number-renamed-aux-term + (implies (alistp sigma) + (equal + (apply-subst flg (second (number-rename-aux flg term sigma + x y)) + term) + (first (number-rename-aux flg term sigma x y)))))) + + + +;;; 3.3.3.2 +;;; The term returned by number-rename-aux subsumes the input term +;;; ··································································· + +(local + (encapsulate + () + (local + (defthm number-renamed-aux-term-subsumes-term-lemma + (implies (and (acl2-numberp x) (acl2-numberp y) (not (= y 0))) + (equal + (apply-subst + flg + (inverse (second (number-rename-aux flg term nil x y))) + (apply-subst flg (second (number-rename-aux flg term nil + x y)) + term)) + term)) + :hints (("Goal" + :in-theory (disable renaming + term-subsumes-number-renamed-aux-term))) + :rule-classes nil)) + + (defthm number-renamed-aux-term-subsumes-term + (implies (and (acl2-numberp x) (acl2-numberp y) (not (= y 0))) + (equal + (apply-subst + flg + (inverse (second (number-rename-aux flg term nil x y))) + (first (number-rename-aux flg term nil x y))) + term)) + :hints (("Goal" + :use (:instance number-renamed-aux-term-subsumes-term-lemma)))))) + + +;;; ---------------------------------------------------------------------------- +;;; 3.4 Number-rename: definition and main (non-local) properties +;;; ---------------------------------------------------------------------------- + +;;; Here we compile the results of section 3. + +(defun number-rename (term x y) + (declare (xargs :guard (and (term-p term) + (acl2-numberp x) + (acl2-numberp y)))) + (mv-let (renamed renaming) + (number-rename-aux t term nil x y) + (declare (ignore renaming)) + renamed)) + + +;;; The following lemma can be useful: number-rename never returns the +;;; term nil (instead, it could return the number x). So there are no +;;; confussion between nil as fail and nil as term. + +(defthm number-rename-not-nil + (implies (acl2-numberp x) + (number-rename term x y))) + +;;; Subsumption properties: + +(defthm term-subsumes-number-renamed-term + (subs term (number-rename term x y)) + + :hints (("Goal" :use + (:instance subs-completeness + (t1 term) + (t2 (number-rename term x y)) + (sigma + (second (number-rename-aux t term nil x y))))))) + +(defthm number-renamed-term-subsumes-term + (implies (and (acl2-numberp x) (acl2-numberp y) (not (= y 0))) + (subs (number-rename term x y) term)) + + :hints (("Goal" :use + (:instance subs-completeness + (t2 term) + (t1 (number-rename term x y)) + (sigma + (inverse + (second (number-rename-aux t term nil x y)))))))) + + +;;; Variables of (number-rename term x y) are: +;;; * if y>0, they are all bigger than x +;;; * if y<0, they are all smaller than x + +(defthm number-renamed-variables->=-x + (implies (and (acl2-numberp x) (> y 0)) + (acl2-numberp-list-bigger-than + (variables t (number-rename term x y)) + x))) + + +(defthm number-renamed-variables-<=-x + (implies (and (acl2-numberp x) (< y 0)) + (acl2-numberp-list-smaller-than + (variables t (number-rename term x y)) + x))) + +;;; An useful property for standardization apart: +(encapsulate + () + + (local + (defthm smaller-bigger-disjointp + (implies (and + (< x1 x2) + (acl2-numberp-list-smaller-than l1 x1) + (acl2-numberp-list-bigger-than l2 x2)) + (disjointp l1 l2)))) + + (defthm number-rename-standardization-apart + (implies (and (acl2-numberp x1) + (acl2-numberp x2) + (< x1 x2) + (< y1 0) + (< 0 y2)) + (disjointp (variables t (number-rename t1 x1 y1)) + (variables t (number-rename t2 x2 y2)))) + :hints (("Goal" :use + (:instance + smaller-bigger-disjointp + (l1 (variables t (number-rename t1 x1 y1))) + (l2 (variables t (number-rename t2 x2 y2)))))))) + + +;;; Closure property: + + +(defthm number-rename-term-s-p + (implies (and (acl2-numberp x) (term-s-p term)) + (term-s-p (number-rename term x y)))) + + +;;; Needed for guard verification: + +(defthm number-rename-term-p + (implies (and (acl2-numberp x) (term-p term)) + (term-p (number-rename term x y))) + :hints (("Goal" :use (:functional-instance + number-rename-term-s-p + (signat (lambda (x n) (eqlablep x))) + (term-s-p-aux term-p-aux))))) + +;;; We have extracted the main properties of number-rename, so we now +;;; disable its definition: +(in-theory (disable number-rename)) + + +;;; A rewriting congruence rule: + +(defthm number-renamed-term-renamed-term + (implies (and (acl2-numberp x) (acl2-numberp y) (not (= y 0))) + (renamed (number-rename term x y) term))) + + +;;; ---------------------------------------------------------------------------- +;;; 3.5 Number-rename-list: definition and main (non-local) properties +;;; ---------------------------------------------------------------------------- + +;;; Renaming lists of terms +;;; Although we are going just to repeat the above development, now for +;;; lists of terms, we think it is convinient to define separately +;;; number-rename from number-rename-list, although they are diferent +;;; particular cases of the same function: number-rename-aux. + +;;; Sometimes (see for example critical-pairs.lisp) we will need to +;;; rename several terms at the same time (for example, both terms of a +;;; rewriting rule). In such cases we want the same variable to be +;;; replaced for the same number, wherever that variable occurs in the +;;; list (even in diferent terms of the list). That's the reason why we +;;; define number-rename-list and its properties as non-local in this +;;; book. + +(defun number-rename-list (l x y) + (declare (xargs :guard (and (term-p-aux nil l) + (acl2-numberp x) + (acl2-numberp y)))) + (mv-let (renamed renaming) + (number-rename-aux nil l nil x y) + (declare (ignore renaming)) + renamed)) + + +;;; Subsumption properties: + +(defthm list-subsumes-number-renamed-list- + (subs-list l (number-rename-list l x y)) + + :hints (("Goal" :use + (:instance subs-list-completeness + (l1 l) + (l2 (number-rename-list l x y)) + (sigma + (second (number-rename-aux nil l nil x y))))))) + +(defthm number-renamed-list-subsumes-list + (implies (and (acl2-numberp x) (acl2-numberp y) (not (= y 0))) + (subs-list (number-rename-list l x y) l)) + + :hints (("Goal" :use + (:instance subs-list-completeness + (l2 l) + (l1 (number-rename-list l x y)) + (sigma + (inverse + (second (number-rename-aux nil l nil x y)))))))) + + +;;; Variables of (number-rename term x y) are: +;;; * if y>0, they are all bigger than x +;;; * if y<0, they are all smaller than x + +(defthm number-renamed-list-variables->=-x + (implies (and (acl2-numberp x) (> y 0)) + (acl2-numberp-list-bigger-than + (variables nil (number-rename-list term x y)) + x))) + + +(defthm number-renamed-list-variables-<=-x + (implies (and (acl2-numberp x) (< y 0)) + (acl2-numberp-list-smaller-than + (variables nil (number-rename-list term x y)) + x))) + +;;; An useful property for standardization apart: +(encapsulate + () + + (local + (defthm smaller-bigger-disjointp + (implies (and + (< x1 x2) + (acl2-numberp-list-smaller-than l1 x1) + (acl2-numberp-list-bigger-than l2 x2)) + (disjointp l1 l2)))) + + (defthm number-rename-list-standardization-apart + (implies (and (acl2-numberp x1) + (acl2-numberp x2) + (< x1 x2) + (< y1 0) + (< 0 y2)) + (disjointp (variables nil (number-rename-list l1 x1 y1)) + (variables nil (number-rename-list l2 x2 y2)))) + :hints (("Goal" :use + (:instance + smaller-bigger-disjointp + (l1 (variables nil (number-rename-list l1 x1 y1))) + (l2 (variables nil (number-rename-list l2 x2 y2)))))))) + + +;;; Closure property: + + +(defthm number-rename-list-term-s-p-aux-nil + (implies (and (acl2-numberp x) (term-s-p-aux nil l)) + (term-s-p-aux nil (number-rename-list l x y)))) + + +;;; Needed for guard verification: + +(defthm number-rename-list-term-p-aux-nil + (implies (and (acl2-numberp x) (term-p-aux nil l)) + (term-p-aux nil (number-rename-list l x y))) + :hints (("Goal" :use (:functional-instance + number-rename-list-term-s-p-aux-nil + (signat (lambda (x n) (eqlablep x))) + (term-s-p-aux term-p-aux))))) + +;;; We have extracted the main properties of number-rename-list, so we now +;;; disable its definition: +(in-theory (disable number-rename-list)) + + + + + diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-definition-v0.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-definition-v0.lisp new file mode 100644 index 0000000..56f8580 --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-definition-v0.lisp @@ -0,0 +1,264 @@ +;;; ================================================================= +;;; subsumption-definition-v0.lisp +;;; Definition and correctness of a subsumption +;;; algorithm between terms. Definition of the subsumption relation. +;;; Created 7-10-99. +;;; This is a translated version of an .events file for nqthm +;;; WARNING: Although this book is correct, there an improved version, +;;; based on rules of transformation, subsumption.lisp +;;; ================================================================= + +#| To certify this book: + +(in-package "ACL2") + +(certify-book "subsumption-definition-v0") + +|# + +(in-package "ACL2") +(include-book "terms") + +;;; ********************************** +;;; DEFINITION: SUBSUMPTION ALGORITHM +;;; ********************************** + +;;; NOTE: +;;; 1) Definition by mutual recursion on terms and list of terms. +;;; 2) sigma is a substitutions of computed bindings for the moment. + +(defun subsumption-alg (flg t1 t2 sigma) + (if flg + (if (variable-p t1) + (if (member t1 (domain sigma)) + (if (equal (val t1 sigma) t2) + sigma ; *11* + nil) ; *10* + (cons (cons t1 t2) sigma)) ; *9* + (if (variable-p t2) + nil ; *8* + (if (equal (car t1) (car t2)) + (subsumption-alg nil (cdr t1) (cdr t2) sigma) ; *7* + nil))) ; *6* + (if (atom t1) + (if (equal t1 t2) sigma nil) ; *5* y *4* + (if (atom t2) + nil ; *3* + (let ((subs-primeros (subsumption-alg t (car t1) (car t2) sigma))) + (if subs-primeros + (subsumption-alg nil ; *2* + (cdr t1) + (cdr t2) + subs-primeros) + nil)))))) ; *1* + +;;; DESCRIPTION: +;;; Input: t1 and t2 are terms or list of terms (depending on flg). +;;; sigma is a substitution (initial bindings) +;;; flg is a boolean value: +;;; - If flg is nil, t1 and t2 are list of terms +;;; - If flg is not nil, t1 and t2 are terms. +;;; Output: +;;; *11* If t1 and t2 are terms, t1 is a variable alrady bound in sigma, +;;; and its value in sigma is t2, returns sigma. +;;; *10* As in *1*, but the value of t1 in sigma iis not t2, returns nil +;;; *9* If t1 and t2 are terms, t1 is a variable not bound in sigma, +;;; return sigma adding the binding (t1 . t2) +;;; *8* If t1 is not a variable and t2 is a variable, returns nil. +;;; *7* If t1 and t2 are non-variable terms, with the same top function +;;; symbol, recursively call to subsumption-alg applied to the lists +;;; of the respective arguments. +;;; *6* If t1 and t2 are non-variable terms, with different top function +;;; symbol, return nil. +;;; *5* If t1 and t2 are lists of terms and t1 is an empty list, +;;; the same as t2, returns sigma. +;;; *4* If t1 and t2 are lists of terms and t1 is an empty list, +;;; different from t2, returns nil. +;;; *3* If t1 and t2 are lists of terms, t1 is not an empty list, +;;; and t2 is an empty list, returns nil. +;;; *2* If t1 and t2 are non-empty lists of terms and the the first +;;; elements of t1 subsumes the first element of t2, recursively +;;; call subsumption-alg with the list of the rest of respective +;;; arguments, with initial bindings the substitution obtained when +;;; applying the algorithm to the first arguments. +;;; *1* If t1 and t2 are non-empty lists of terms and the the first +;;; elements of t1 does not subsume the first element of t2, returns +;;; nil. + + +;;; ****************************** +;;; PREVIOUS LEMMAS ABOUT COINCIDE +;;; ****************************** +;;; ====== COINCIDE. See definition and properties in terms.lisp +(local +(defthm coincide-main-property + (implies (and (coincide sigma1 sigma2 l) + (member x l)) + (equal (equal (val x sigma1) (val x sigma2)) t)))) + +;;; The form of the rule avoids non-termination +;;; This rule is also local in terms.lisp. We don't want terms.lisp to +;;; export everywhere. That's the reason why we repeat here the rule. +(local +(defthm coincide-conmutative + (implies (coincide a b l) + (coincide b a l)))) + + +(local (in-theory (disable coincide-conmutative))) +(local +(defthm coincide-cons + (implies (and + (not (member x l)) + (coincide sigma sigma1 l)) + (coincide (cons (cons x y) sigma) sigma1 l)))) + +(local +(defthm coincide-subsetp-transitive + (implies (and (coincide sigma sigma1 l) + (coincide sigma1 sigma2 m) + (subsetp m l)) + (coincide sigma sigma2 m)))) + +(local +(in-theory (disable coincide-subsetp-transitive))) + + + +;;; ************************************************* +;;; LEMMAS FOR PROVING SOUNDNESS OF SUBSUMPTION-ALG +;;; ************************************************* + +;;; ======================== LEMA ================ +;;; If subsumption suceeds, the result extends sigma +;;; ================================================ + +(local (defthm soundness-main-lemma-1 + (let ((result-subsumption (subsumption-alg flg t1 t2 sigma))) + (implies result-subsumption + (and + (subsetp (domain sigma) (domain result-subsumption)) + (extension result-subsumption sigma) + (subsetp (variables flg t1) (domain result-subsumption))))) + :hints (("Goal" + :in-theory (enable + subsetp-transitive + coincide-conmutative + coincide-subsetp-transitive))))) + + + +(local (defthm soundness-main-lemma-2 + (implies (and (subsumption-alg flg1 t1 t2 sigma) + (subsumption-alg flg2 t3 t4 (subsumption-alg flg1 t1 t2 sigma))) + (equal (apply-subst + flg1 + (subsumption-alg flg2 t3 t4 (subsumption-alg flg1 t1 t2 + sigma)) + t1) + (apply-subst flg1 (subsumption-alg flg1 t1 t2 sigma) t1))) + :hints (("Goal" :use + (:instance coincide-in-term + (flg flg1) + (sigma2 (subsumption-alg flg2 t3 t4 + (subsumption-alg flg1 t1 t2 sigma))) + (term t1) + (sigma1 (subsumption-alg flg1 t1 t2 sigma)) + (l (domain (subsumption-alg flg1 t1 t2 sigma)))))))) + + + +;;; **************************** +;;; SOUNDNESS OF SUBSUMPTION-ALG +;;; **************************** + +;;; ============================== LEMMA ============================== +;;; If subsumption suceeds, the result is a matching susbtitution for t1 +;;; and t2 +;;; ===================================================================== + + +(local (defthm soudness-subsumption-alg + (implies (subsumption-alg flg t1 t2 sigma) + (equal (apply-subst flg (subsumption-alg flg t1 t2 sigma) t1) + t2)))) + + +;;; ****************************** +;;; COMPLETENESS OF SUBSUMPTION-ALG +;;; ****************************** + +;;; ============================ LEMMA =============================== +;;; If sigma1 is a matching substitution for t1 and t2, our subsumption +;;; algorithm succeeds and sigma1 is an extension of the substitution +;;; returned. +;;; =================================================================== + +(local (defthm completeness-subsumption-alg-general + (let ((result-subsumption (subsumption-alg flg t1 t2 sigma1))) + (implies (and (equal (apply-subst flg sigma t1) t2) + sigma1 + (extension sigma sigma1)) + (and result-subsumption + (extension sigma result-subsumption)))) + :rule-classes nil)) +;;; REMARKS: +;;; The free variables in the lemma make it useless as rewriting +;;; rule. + + +;;; ****************************************************************** +;;; DEFINITION: A SUBSUMPTION RELATION BETWEEN TERMS OR LISTS OF TERMS +;;; ****************************************************************** + + +(defun subs (t1 t2) + (subsumption-alg t t1 t2 0)) + + +;;; REMARK: In ACL2, nil and the empty list are the same thing. To +;;; distinguish fail from the empty list, we apply subsumption with an +;;; non-nil atom (0 in this case) and at teh end we fix the final tail. + +;;; ================= +;;; SOUNDNESS OF SUBS +;;; ================= + +(defthm soudness-subs + (implies (subs t1 t2) + (equal (instance t1 (subs t1 t2)) + t2)) + :rule-classes (:rewrite :elim)) + +;;; ============================ +;;; COMPLETENESS OF SUBS-WITNESS +;;; ============================ + +(defthm completeness-subs + (implies (equal (instance t1 sigma) t2) + (subs t1 t2)) + :rule-classes nil + :hints (("Goal" :use ((:instance + completeness-subsumption-alg-general + (flg t) + (sigma1 0)))))) + + +(in-theory (disable subsumption-alg)) +(in-theory (disable subs)) + + + + + + + + + + + + + + + + diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-subst.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-subst.lisp new file mode 100644 index 0000000..6eefb93 --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-subst.lisp @@ -0,0 +1,748 @@ +;;; subsumption-subst.lisp +;;; The subsumption relation between substitutions +;;; Created 13-10-99. Last revision: 09-01-2001 +;;; ================================================================= + + +#| To certify this book: + +(in-package "ACL2") + +(certify-book "subsumption-subst") + +|# + +(in-package "ACL2") +(include-book "subsumption") + + + + +;;; ******************************************************************* +;;; THE SUBSUMPTION RELATION BETWEEN SUBSTITUTIONS. +;;; DEFINITION AND PROPERTIES. +;;; ******************************************************************* + +;;; Our goal is to define the subsumption relation between +;;; substitutions. In the literature, this relation is defined in this +;;; way: +;;; sigma <= delta iff (exists gamma) gamma·sigma = delta +;;; where "·" stands for composition. + +;;; Note that equality between substitutions is functional equality (we cannot +;;; use equal), so we reformulate this property as: + +;;; (*) sigma <= delta iff (exists gamma) +;;; s.t. for all term +;;; gamma·sigma(term) = delta(term) + + +;;; Our goal in this book is to define the subsumption relation between +;;; substitutions as a function, subs-subst. We will define that +;;; function paying attention only to a restricted list of +;;; variables. Then will prove (*) in the ACL2 logic. As subsumption +;;; between terms (due to existential quantification) we have to give +;;; the substitution gamma in a constructive way, so our definition of +;;; the subsumption relation will be based on a algorithm that finds +;;; such substitution gamma, whenever it exists. + + +;;; That is to say, we are going to: + +;;; 1) Define the subsumption relation, (subs-subst sigma delta) as a +;;; function and the witness matching substitution, called +;;; (matching-subst-r sigma delta). Both functions will be based on a +;;; matching algorithm called subs-subst-mv. + +;;; 2) Prove that if (subs-subst sigma delta), then +;;; (matching-subst-r sigma delta) applied to sigma(term) is equal to +;;; delta(term), with the same matching substitution, for all +;;; term. The reverse implication is trivial. + + +;;; ============================================================================ +;;; 1. Definition of subs-subst +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 1.1. Some previous definitions and lemmas +;;; ---------------------------------------------------------------------------- + +;;; ===== TRUE-LIST-OF-VARIABLES +(local + (defun true-list-of-variables (l) + (if (atom l) + (equal l nil) + (and (variable-p (car l)) + (true-list-of-variables (cdr l)))))) + +(local + (defthm true-list-of-variables-append + (implies (and (true-list-of-variables l) + (true-list-of-variables m)) + (true-list-of-variables (append l m))))) + +(local + (defthm true-list-of-variables-variables + (true-list-of-variables (variables flg term)))) + + +;;; ===== TRUE-LIST-OF-EQLABLEP (needed for guard verification) +(local + (defun true-list-of-eqlablep (l) + (if (atom l) + (equal l nil) + (and (eqlablep (car l)) + (true-list-of-eqlablep (cdr l)))))) + +(local + (defthm true-list-of-eqlablep-append + (implies (and (true-list-of-eqlablep l) + (true-list-of-eqlablep m)) + (true-list-of-eqlablep (append l m))))) + +(local + (defthm true-list-of-eqlablep-variables + (implies (term-s-p-aux flg term) + (true-list-of-eqlablep (variables flg term))))) + + + +;;; ===== DOMAIN-VAR +;;; The variables of the domain (to remove anomalies). + +(defun domain-var (sigma) + (if (endp sigma) + nil + (if (variable-p (caar sigma)) + (cons (caar sigma) (domain-var (cdr sigma))) + (domain-var (cdr sigma))))) + + + +;;; Its main properties + +(local + (defthm domain-var-main-property + (iff (member x (domain-var sigma)) + (and (member x (domain sigma)) + (variable-p x))))) + +;;; Needed for guard verification +(local + (defthm true-list-of-variables-domain-var + (true-list-of-variables (domain-var sigma)))) + +(local + (defthm true-list-of-eqlablep-domain-var + (implies (substitution-s-p sigma) + (true-list-of-eqlablep (domain-var sigma))))) + + +(local (in-theory (disable domain-var))) + + + + +;;; ====== CO-DOMAIN-VAR +;;; The "values" of the variables in domain-var + + +(defun co-domain-var (sigma) + (if (endp sigma) + nil + (if (variable-p (caar sigma)) + (cons (cdar sigma) (co-domain-var (cdr sigma))) + (co-domain-var (cdr sigma))))) + +;;; Needed for guard verification +(local + (defthm term-s-p-aux-co-domain-var + (implies (substitution-s-p sigma) + (term-s-p-aux nil (co-domain-var sigma))))) + + + +;;; ====== IMPORTANT-VARIABLES +;;; For subsumption of substitutions, we only pay atention to these +;;; variables + +(defun important-variables (sigma delta) + (append (domain-var sigma) + (append (domain-var delta) + (variables nil (co-domain-var sigma))))) + + + +;;; ===== SYSTEM-SUBS-SUBST. +;;; A technical macro definition +;;; We will prove below that two substitutions are related by +;;; subsumption iff the following system of equations is matchable. + +(local + (defmacro system-subs-subst (sigma delta) + `(first + (pair-args + (apply-subst nil ,sigma (important-variables ,sigma ,delta)) + (apply-subst nil ,delta (important-variables ,sigma ,delta)))))) + + +;;; ---------------------------------------------------------------------------- +;;; 1.2. Definition of subs-subst +;;; ---------------------------------------------------------------------------- + + +;;;; NOTATION: +;;;; ^^^^^^^^^ +;;;; In the followin comments, V will be +;;;; (important-variables sigma delta)) + +;;; ===== SUBS-SUBST-MV +;;; Subsumption between substitutions. +;;; To decide wether sigma subsumes delta, then we take the list of +;;; variables of the domain of sigma, the domain of delta and the +;;; variables of the terms in the co-domain of sigma (i.e, the list V), and +;;; test if the list of terms sigma(V) subsumes the list of terms +;;; delta(V). + +(defun subs-subst-mv (sigma delta) + (let ((V (important-variables sigma delta))) + (mv-let (system bool) + (pair-args (apply-subst nil sigma V) + (apply-subst nil delta V)) + (declare (ignore bool)) + (match-mv system)))) + +;;; ====== SUBS-SUBST +;;; The subsumption relation between substitutions: + + +(defun subs-subst (sigma delta) + (mv-let (match bool) + (subs-subst-mv sigma delta) + (declare (ignore match)) + bool)) + + +;;; ===== MATCHING-SUBST +;;; An important auxiliary definition: when +;;; (subs-subst sigma delta) returns t, this is the substitution that +;;; applied to the list (apply-subst nil sigma V) returns +;;; (apply-subst nil delta V) + +(defun matching-subst (sigma delta) + (mv-let (match bool) + (subs-subst-mv sigma delta) + (declare (ignore bool)) + match)) + +;;; ====== MATCHING-SUBST-R +;;; Restriction of (subs-sust sigma delta) to V. + +(defun matching-subst-r (sigma delta) + (restriction (matching-subst sigma delta) + (important-variables sigma delta))) + + +;;; REMARKS: +;;; +;;; 1) The substitution subs-sust-r is the witness substitution to prove +;;; subsumption between sigma(term) and delta(term), for all terms, as +;;; we will prove. + +;;; 2) For our particular implementation of subsumption between terms, +;;; subs-sust and subs-sust-r are exactly the same (from a functional +;;; pont of view) (when subs-sust is not nil). But we have to define +;;; subs-sust-r to assure explicitly that outside V, the substitution is +;;; the identity, because this is not derived from the soundness and +;;; completeness theorems of and we forbid ourselves to use particular +;;; properties of a particular matching algorithms. + +;;; 3) Note that subst-sust-r probably has many repetitions in his +;;; domain, but this is not a problem for us. We will not use +;;; subs-sust-r to compute, only as a tool to deduce properties. + + +;;; ============================================================================ +;;; 2. Soundness theorem +;;; ============================================================================ + +;;; We want to prove: if (subs-sust sigma delta), then +;;; the substitutions +;;; delta +;;; and +;;; (composition (subs-subst-r sigma delta) sigma) +;;; are functionally equal. + +;;; ---------------------------------------------------------------------------- +;;; 3.1 The main lemma needed for the soundness theorem +;;; ---------------------------------------------------------------------------- + + +;;; The main goal here is to prove that: +;;; For all variable x, +;;; (val x (composition (subs-subst-r sigma delta) sigma)) = (val x delta) +;;; if (subs-sust sigma delta) +;;; WE DISTINGUISH THREE CASES. + +;;; ············································································ +;;; 3.1.1 Case 1: x is a variable outside V +;;; ············································································ + + + +(local + (defthm subs-subst-main-property-variable-x-not-in-V + (let ((V (important-variables sigma delta))) + (implies (and + (variable-p x) + (not (member x V)) + (subs-subst sigma delta)) + (equal (instance (val x sigma) (matching-subst-r sigma delta)) + (val x delta)))) + :hints (("Goal" :in-theory (enable x-not-in-domain-remains-the-same))))) + + +;;; ············································································ +;;; 3.1.2. Case 2: x is a variable of (domain-var sigma) +;;; ············································································ + + +;;; 3.1.2.1 A lemma for this case 2: +;;; subs-subst composed with sigma is equal to delta in V. +;;; ······················································ + +(local + (encapsulate + () + +;;; Two previous lemmas: + (local + (defthm pair-args-success + (second (pair-args (apply-subst nil sigma l) + (apply-subst nil delta l))))) + + (local + (defthm apply-nil-apply-t + (implies (and (equal (apply-subst nil sigma1 l) + (apply-subst nil sigma2 l)) + (member x l)) + (equal (instance x sigma1) + (instance x sigma2))) + :rule-classes nil)) + +;;; A technical lemma: + + (local + (defthm apply-subst-from-matchers-to-lists-of-terms + (implies (and + (second (pair-args l m)) + (matcher sigma (first (pair-args l m)))) + (equal (equal (apply-subst nil sigma l) m) t)) + :hints (("Goal" :induct (pair-args l m))))) + +;;; And the intended lemma: + + (defthm matching-subst-composed-sigma-coincide-with-delta-in-V + (let ((V (important-variables sigma delta))) + (implies (and + (variable-p x) + (member x V) + (subs-subst sigma delta)) + (equal (instance (val x sigma) (matching-subst sigma delta)) + (val x delta)))) + :hints (("Goal" :in-theory (disable important-variables) + :use (:instance apply-nil-apply-t + (l (important-variables sigma delta)) + (sigma1 (composition + (matching-subst sigma delta) sigma)) + (sigma2 delta))))))) + + + +;;; REMARKS: +;;; 1) If we not disable important-variables the proof is longer. +;;; 2) The condition (variable-p x) is not necessary, but the proof is +;;; shorter. + + +;;; The above lemma gives the fundamental property of subs-subst and +;;; matching-subst . We can forget its definition, so we disable their +;;; definitions: + +(local (in-theory (disable subs-subst matching-subst))) + +;;; 3.1.2.2 Another lemma for case 2: +;;; ······························· + +(local + (defthm variables-co-domain-var + (implies (member x (domain-var sigma)) + (subsetp (variables t (val x sigma)) + (variables nil (co-domain-var sigma)))))) + + +;;; 3.1.2.3 The main result for Case 2 +;;; ································ + +(local + (defthm + subs-subst-main-property-variable-x-in-domain-var-sigma + (implies (and + (variable-p x) + (member x (domain-var sigma)) + (subs-subst sigma delta)) + (equal (apply-subst t (matching-subst-r sigma delta) (val x sigma)) + (val x delta))))) + + +;;; ············································································ +;;; 3.1.3. Case 3: x in V but not in (domain-var sigma) +;;; ············································································ + + +;;; 3.1.3.1 A lemma for Case 3 +;;; In this case, matching and matching-subst-r take the same values. +;;; ································································· + +(local + (defthm + subsumption-subst-main-property-variable-in-V-not-in-domain-var-sigma-lemma + (let ((V (important-variables sigma delta))) + (implies (and + (variable-p x) + (not (member x (domain-var sigma))) + (member x V) + (subs-subst sigma delta)) + (equal (apply-subst t (matching-subst-r sigma delta) (val x sigma)) + (apply-subst t (matching-subst sigma delta) + (val x sigma))))) + :hints (("Goal" :in-theory (enable x-not-in-domain-remains-the-same))))) + + +;;; We disable important-variables and matching-subst-r since we do not +;;; need to "extract" more properties from the definitions. + +(local (in-theory (disable important-variables matching-subst-r))) + + +;;; 3.1.3.2 The main result for this case. +;;; This result is not strictly needed, bu we include in favour of +;;; clarity. + +(local + (defthm + subs-subst-main-property-variable-x-in-V-not-in-domain-var-sigma + (let ((V (important-variables sigma delta))) + (implies (and + (variable-p x) + (not (member x (domain-var sigma))) + (member x V) + (subs-subst sigma delta)) + (equal (apply-subst t (matching-subst-r sigma delta) (val x sigma)) + (val x delta)))))) + + + +;;; ---------------------------------------------------------------------------- +;;; 3.2 Statements of the soundness theorem +;;; ---------------------------------------------------------------------------- + +;;; Joining the three cases together, we prove +;;; functional equality between +;;; (composition (matching-subst-r sigma delta) sigma) and delta. + + +(local + (defthm + equal-composition-matching-subst-with-sigma-to-delta-variable + (implies (and (variable-p x) + (subs-subst sigma delta)) + (equal (val x (composition (matching-subst-r sigma delta) sigma)) + (val x delta))) + :hints + (("Goal" + :cases ((not (member x (important-variables sigma delta))) + (member x (domain-var sigma))))))) + + + + +;;; DIFFERENT VERSIONS OF THE SOUNDNESS THEOREM + + +;;; With terms and list of terms (not only with variables) +;;; ······················································ + +(local + (defthm + equal-composition-subs-subst-with-sigma-to-delta + (implies (subs-subst sigma delta) + (equal (apply-subst + flg + (composition (matching-subst-r sigma delta) sigma) + term) + (apply-subst flg delta term))) + :hints (("Goal" :in-theory (disable + composition-of-substitutions-apply))) + :rule-classes nil)) + +;;; We prefer this formulation to be called the soundness theorem of +;;; subs-subst + +(defthm + subs-subst-soundness + (implies (subs-subst sigma delta) + (equal + (instance term (composition (matching-subst-r sigma delta) + sigma)) + + (instance term delta))) + :rule-classes nil + :hints (("Goal" :use + (:instance + equal-composition-subs-subst-with-sigma-to-delta + (flg t))))) + + + + +;;; REMARK: we do not use the two above lemmas as a rewrite rule to avoid +;;; conflicts with composition-of-substitutions-appply. Instead, the +;;; following version will be used as a rewrite rule. + +;;; With terms but without using composition +;;; ········································ + +(defthm + subs-subst-implies-matching-subst-r-appplied-to-sigma-term-is-delta-term + (implies (subs-subst sigma delta) + (equal (apply-subst flg (matching-subst-r sigma delta) + (apply-subst flg sigma term)) + (apply-subst flg delta term))) + :hints + (("Goal" :use + (:instance equal-composition-subs-subst-with-sigma-to-delta)))) + + +;;; With respect to subsumption between terms +;;; ········································· + + +;;; Trivial consequence of completeness of subsumption and the previous +;;; lemma: + + +(defthm + subs-subst-main-property + (implies (subs-subst sigma delta) + (subs (instance term sigma) (instance term delta))) + :hints (("Goal" :use + ((:instance subs-completeness + (t1 (instance term sigma)) + (t2 (instance term delta)) + (sigma (matching-subst-r sigma delta))))))) + + + + +;;; ============================================================================ +;;; 3. Completeness theorem +;;; ============================================================================ + +(local (in-theory (enable subs-subst))) + + +;;; We want to prove the following: +;;; If sigma <= delta, then (subs-subst sigma delta). +;;; In fact, it will be more useful to prove + + +;;; The theorem is very easy to prove, but the problem is how we +;;; formulate the hypothesis sigma <= delta. We will assume the +;;; existence of two substitutions, called sigma-w and delta-w and the +;;; only property we will assume about them is that sigma-w <= +;;; delta-w. That is, exists another substitution gamma-w such that +;;; delta-w = gamma-w·sigma-w. + +;;; We will use encapsulate for that purpose. Let sigma-w, delta-w and +;;; gamma-w three susbtitutions such that delta-w is functionally equal +;;; to (composition gamma-w sigma-w) + +;;; HYPOTHESIS: + +(encapsulate + (((sigma-w) => *) + ((delta-w) => *) + ((gamma-w) => *)) + + (local (defun sigma-w () nil)) + (local (defun delta-w () nil)) + (local (defun gamma-w () nil)) + + (defthm sigma-w-delta-w-subsumption-hypothesis + (equal (instance term (composition (gamma-w) (sigma-w))) + (instance term (delta-w))) + :rule-classes nil)) + +;;; Now our goal is to prove (subs-subst (sigma-w) (delta-w)). + +;;; The assumption as a rewrite rule: +(local + (defthm sigma-w-delta-w-subsumption-hypothesis-rewrite-rule + (equal (instance (instance term (sigma-w)) (gamma-w)) + (instance term (delta-w))) + :hints (("Goal" :use sigma-w-delta-w-subsumption-hypothesis)))) + +;;; The main lemma +(defthm gamma-w-matcher + (matcher (gamma-w) + (first (pair-args (apply-subst nil (sigma-w) l) + (apply-subst nil (delta-w) l))))) + +;;; And the completeness theorem: + +(defthm subs-subst-completeness + (subs-subst (sigma-w) (delta-w)) + :rule-classes nil + :hints (("Goal" :use + (:instance match-mv-completeness + (sigma (gamma-w)) + (S (system-subs-subst (sigma-w) (delta-w))))))) + +;;; REMARK: Note that this result can be easily used by functional +;;; instantiation (see for example unification-definition.lisp). + + +;;; ============================================================================ +;;; 4. Closure properties of subs-subst +;;; ============================================================================ + +(local (in-theory (enable matching-subst matching-subst-r + important-variables))) + +;;; ============================================================================ +;;; 4.1 Closure properties for the soundness theorem +;;; ============================================================================ + + +;;; We are going to prove that, provided the two substitutions are in a +;;; given signature, the witness substitution used for the soundness +;;; proof above, is also in the given signature. + +(encapsulate + () + + (local + (defthm substitution-s-p--apply-subst-nil-term-s-p-aux + (implies (and (substitution-s-p sigma) + (true-list-of-eqlablep l)) + (term-s-p-aux nil (apply-subst nil sigma l))))) + + (local + (defthm pair-args-system-p + (implies (and (term-s-p-aux nil l) + (term-s-p-aux nil m)) + (system-s-p (first (pair-args l m)))))) + + (defthm matching-subst-substitution-s-p + (implies (and (substitution-s-p sigma) + (substitution-s-p delta)) + (substitution-s-p (matching-subst sigma delta)))) + + (local + (defthm restriction-substitution-s-p + (implies (and (substitution-s-p sigma) + (true-list-of-eqlablep l)) + (substitution-s-p (restriction sigma l))))) + + (defthm matching-subst-r-substitution-s-p + (implies (and (substitution-s-p sigma) + (substitution-s-p delta)) + (substitution-s-p (matching-subst-r sigma delta))))) + + + + + +;;; ---------------------------------------------------------------------------- +;;; 4.2 Closure property for the completeness theorem +;;; ---------------------------------------------------------------------------- + +;;; We can prove a slightly different version of the completeness +;;; theorem: the closure property of the completeness theorem +;;; + +;;; We want to prove the following: +;;; let us suppose that sigma and gamma are two substitutions IN A GIVEN +;;; SIGNATURE. Suppose that sigma <= delta, i.e., there exists a +;;; substitution gamma IN THE SAME SIGNATURE such that sigma(term) = +;;; gamma.sigma(term), FOR ALL TERM IN THE SIGNATURE. +;;; Then (subs-subst sigma delta). + +;;; Let us formulate the hypothesis using encapsulate: + + +(encapsulate + (((sigma-w-s) => *) + ((delta-w-s) => *) + ((gamma-w-s) => *)) + + (local (defun sigma-w-s () nil)) + (local (defun delta-w-s () nil)) + (local (defun gamma-w-s () nil)) + + (defthm sigma-w-s-substitution-s-p (substitution-s-p (sigma-w-s))) + (defthm delta-w-s-substitution-s-p (substitution-s-p (delta-w-s))) + (defthm gamma-w-s-substitution-s-p (substitution-s-p (gamma-w-s))) + + (defthm sigma-w-s-delta-w-s-subsumption-hypothesis + (implies (term-s-p term) + (equal (instance term (composition (gamma-w-s) (sigma-w-s))) + (instance term (delta-w-s)))) + :rule-classes nil)) + +;;; Now our goal is to prove (subs-subst (sigma-w-s) (delta-w-s)). + + +;;; The assumption as a rewrite rule: +(local + (defthm sigma-w-s-delta-w-s-subsumption-hypothesis-rewrite-rule + (implies (variable-s-p x) + (equal (instance (val x (sigma-w-s)) (gamma-w-s)) + (val x (delta-w-s)))) + :hints (("Goal" + :use (:instance + sigma-w-s-delta-w-s-subsumption-hypothesis + (term x)))))) + +;;; The main lemma +(local + (defthm gamma-w-s-matcher + (implies (true-list-of-eqlablep l) + (matcher (gamma-w-s) + (first (pair-args (apply-subst nil (sigma-w-s) l) + (apply-subst nil (delta-w-s) + l))))))) +;;; And the closure property for the completeness theorem + +(defthm subs-subst-completeness-closure + (subs-subst (sigma-w-s) (delta-w-s)) + :rule-classes nil + :hints (("Goal" :use + (:instance match-mv-completeness + (sigma (gamma-w-s)) + (S (system-subs-subst (sigma-w-s) (delta-w-s))))))) + +;;; REMARK: Note that this result can be easily used by functional +;;; instantiation. + +;;; We disable the defintions of subs-subst (the subsumption relation) +;;; and matching-subst-r (the witness substitution) + +(in-theory (disable subs-subst matching-subst-r)) + + + + + diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-well-founded.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-well-founded.lisp new file mode 100644 index 0000000..bd3e6e6 --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-well-founded.lisp @@ -0,0 +1,491 @@ +;;; subsumption-well-founded.lisp +;;; Well-foundedness of the subsumption relation +;;; Created: 8-10-99 Last revison: 09-12-2000 +;;; ============================================================================= + +#| To certify this book: + +(in-package "ACL2") + +(certify-book "subsumption-well-founded") + +|# + +(in-package "ACL2") +(local (include-book "renamings")) +(include-book "subsumption") +(include-book "../../../../ordinals/ordinals-without-arithmetic") + +;;; ******************************************************* +;;; A PROOF OF WELL-FOUNDEDNESS OF THE SUBSUMPTION RELATION +;;; ******************************************************* + +;;; We will prove that the following ordinal measure: +;;; (defun subsumption-measure (term) +;;; (cons (1+ (size t term)) +;;; (- (len (variables t term)) +;;; (len (make-set (variables t term)))))) +;;; is order-preserving with respect the stric subsumption relation. + +;;; That is to say: +;;; - If (subs t1 t2), then (size t t1) is less or equal than (size t +;;; t2). +;;; - If, in addition, (not (subs t2 t1)) and (size t t1) = (size t t2), +;;; then the number of distinct variables of t1 is greater than the +;;; number of distinct variables of t2, and both of them are at most the +;;; number of variable positions of t1 (or t2). + +;;; Note that the properties described below only use the soundness and +;;; completeness properties of the subsumption algorithm given in +;;; subsumption-one-definition-and-properties.lisp: The +;;; definition and executable-counterpart of subs, matching and subs-mv +;;; are disabled. + + +;;; ============================================================================ +;;; 1. Preliminaries +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 1.1 val-mapcar and properties +;;; ---------------------------------------------------------------------------- + +;;; ===== VAL-MAPCAR +;;; The list of values returned by delta for the elements of the list l + +(local + (defun val-mapcar (delta l) + (if (atom l) + nil + (cons (val (car l) delta) (val-mapcar delta (cdr l)))))) + +;;; Properties: + +(local + (defthm val-map-car-append + (equal (val-mapcar delta (append l m)) + (append (val-mapcar delta l) (val-mapcar delta m))))) + +(local + (defthm val-mapcar-elimination-1 + (implies (not (member x l)) + (equal (val-mapcar (cons (cons x y) delta) l) + (val-mapcar delta l))))) + + +(local + (defthm val-mapcar-elimination-2 + (implies (and (atom x) + (not (member nil l))) + (equal (val-mapcar (cons x delta) l) + (val-mapcar delta l))))) + + +(local + (defthm val-mapcar-main-lemma + (implies (member x l) + (member (val x delta) (val-mapcar delta l))))) + +(local + (encapsulate + () + (local + (defthm val-mapcar-only-one-make-set-is-needed-lemma-1 + (implies (member x (val-mapcar delta (make-set m))) + (member x (val-mapcar delta m))))) + + (local + (defthm val-mapcar-only-one-make-set-is-needed-lemma-2 + (implies (member x (val-mapcar delta m )) + (member x (val-mapcar delta (make-set m)))))) + + + (defthm val-mapcar-only-one-make-set-is-needed + (equal (make-set (val-mapcar delta (make-set l))) + (make-set (val-mapcar delta l)))))) + +(local + (defthm length-val-mapcar + (equal (len (val-mapcar delta l)) (len l)))) + + +;;; ---------------------------------------------------------------------------- +;;; 1.2 variable-substitution: definition and properties +;;; ---------------------------------------------------------------------------- + +;;; A substitution is a variable substitution if every element in its +;;; co-domain is a variable. + + +;;; Properties: + +(local + (defthm variable-substitution-make-set-append + (implies (and (variable-substitution (restriction delta (make-set l))) + (variable-substitution (restriction delta (make-set m)))) + (variable-substitution + (restriction delta (make-set (append l m))))))) + + + +(local + (defthm variable-substitution-value-variable-p + (implies (and (variable-substitution delta) + (variable-p term)) + (variable-p (val term delta))))) + + +;;; value of variable substitutions are variables: + +(local + (defthm variable-p-value + (implies (and (variable-substitution delta) + (member x (domain delta))) + (variable-p (val x delta))))) + + +;;; If delta is a variable substitution, the the variables of delta(t1) +;;; are obtained mapping the variables of t1 by the val of delta. + + + +(local + (defthm variables-apply-subst-variable-substitution + (implies (variable-substitution delta) + (equal + (val-mapcar delta (variables flg term)) + (variables flg (apply-subst flg delta term)))))) + + +;;; An additional lemma: +(local + (defthm val-domain-in-co-domain + (implies (member x (domain delta)) + (member (val x delta) (co-domain delta))))) + + + + +;;; ============================================================================ +;;; 2. The main part of the proof. +;;; ============================================================================ + + +;;; size(t1) <= size(sigma(t1)) + +(local + (defthm size-instance-geq + (>= (size flg (apply-subst flg sigma t1)) + (size flg t1)) + :rule-classes :linear)) + + +;;; If t1 and sigma(t1) have the same size, sigma restricted to the set +;;; of variables of t1 is a variable substitution. That's the reason why +;;; we need the properties of subsection 1.2 + + +(local + (defthm size-equal-variable-substitution + (implies (equal (size flg t1) (size flg (apply-subst flg sigma t1))) + (variable-substitution + (normal-form-subst flg sigma t1))))) + + +;;; If t1 and sigma(t1) have equal size, and the inverse substitution of +;;; the restriction of sigma to the variables of t1 applied to sigma(t1) +;;; is different from t1, then such substitution (which is a variable +;;; substitution, by the above lemma), IS NOT injective (i.e., its +;;; co-domain is not a set). +;;; Note that the hypothesis of the lemma are met as a particular case +;;; of (subs t1 t2), (not (subs t2 t1)), and (size t t1) = (size t t2). + +(local + (encapsulate + () + +;;; This is almost the intended lemma, but for the restriction of sigma +;;; to the set of variables of t1, instead of sigma. + (local + (defthm + equal-size-and-not-inverse-subsumption-implies-not-renaming-almost + (let ((sigmar (normal-form-subst flg sigma t1))) + (implies + (and + (not (equal (apply-subst flg (inverse sigmar) + (apply-subst flg sigmar t1)) t1)) + (equal (size flg t1) (size flg (apply-subst flg sigma t1)))) + (not (setp (co-domain sigmar))))) + :hints (("Goal" :in-theory (disable subsetp-restriction))))) +;;; REMARK: Intentar que esta se hage so'lo aplicando la reglka de +;;; renamings.lisp + +;;; The intended lemma: + (defthm + equal-size-and-not-inverse-subsumption-implies-not-renaming + (let ((sigmar (normal-form-subst flg sigma t1))) + (implies + (and + (not (equal (apply-subst flg (inverse sigmar) + (apply-subst flg sigma t1)) + t1)) + (equal (size flg t1) (size flg (apply-subst flg sigma t1)))) + (not (setp (co-domain sigmar)))))))) + + + +;;; If a substitution is not injective (i.e., its co-domain is not a +;;; set), then the length of the set of elements of the co-domain is +;;; less than the length of the domain. + +(local + (defthm not-injective-implies-co-domain-lessp-than-domain + (implies (not (setp (co-domain delta))) + (< (len (make-set (co-domain delta))) + (len (domain delta)))) + :rule-classes :linear + :hints (("Goal" :in-theory (enable same-length-co-domain-and-domain))))) + + + + + +;;; Relation between domain and co-domain. That is the reason why we +;;; need the properties of 1.2. + + + +(local + (defthm co-domain-val-mapcar + (implies (setp (domain delta)) + (equal (co-domain delta) + (val-mapcar delta (domain delta)))))) + +;;; NOTE: this is not true if the domain is not a set + + + +;;; ------------------------------------------------------------------------- +;;; REMARK: +;;; The above lemmas implies the following two results: + +;;; Let sigmar = (restriction sigma (make-set (variables flg t1))), then +;;; +;;; I) IF sigmar is a variable-substitution THEN +;;; (make-set (co-domain sigmar)) +;;; = +;;; (make-set (variables flg (apply-subst flg sigma t1))), +;;; + +;;; WITH THE FOLLOWING PROOF SKETCH: + +;;; (make-set (co-domain (restriction sigma +;;; (make-set (variables flg t1)))))) +;;; +;;; = (** USING co-domain-val-mapcar and (setp (domain sigmar)) **) +;;; +;;; (make-set (val-mapcar sigma (domain (restriction sigma +;;; (make-set (variables flg t1)))))) +;;; +;;; = (** USING domain-restriction **) +;;; +;;; (make-set (val-mapcar sigma (make-set (variables flg t1)))) +;;; +;;; = (** USING val-mapcar-only-one-make-set-is-needed **) +;;; +;;; (make-set (val-mapcar sigma (variables flg t1))) +;;; +;;; = (** USING variables-apply-substing-variable-substitution, because sigmar +;;; is a variable-substitution **) +;;; +;;; (make-set (variables flg (apply-subst flg sigma t1))) + + + +;;; +;;; II) ALSO, +;;; (domain sigmar) = (make-set (variables flg t1)), +;;; (** USING domain-restriction **) +;;; + + +;;; These are the following theorem. WE DON'T USE them, its only for +;;; presentation of the result (there are some problems with the +;;; orientation of the rule). +(local + (defthm n-variables-decreases-lemma-2 + (let ((sigmar (normal-form-subst flg sigma t1))) + (implies + (equal (size flg t1) (size flg (apply-subst flg sigma t1))) + (equal (make-set (co-domain sigmar)) + (make-set (variables flg (apply-subst flg sigma t1)))))) + :rule-classes nil)) + +(local + (defthm n-variables-decreases-lemma-1 + (let ((sigmar (normal-form-subst flg sigma t1))) + (equal (domain sigmar) (make-set (variables flg t1)))) + :rule-classes nil)) + + +;;; ------------------------------------------------------------------------- + +(local + (encapsulate + () + + +;;; The following lemma is a bridge between domain and co-domains and +;;; the set of variables, using the above proof sketch. + + (local + (defthm n-variables-decreases-bridge-lemma + (let ((sigmar (normal-form-subst flg sigma t1))) + (implies + (and + (equal (size flg t1) (size flg (apply-subst flg sigma t1))) + (< (len (make-set (co-domain sigmar))) + (len (domain sigmar)))) + (< (len (make-set (variables flg (apply-subst flg sigma t1)))) + (len (make-set (variables flg t1)))))) + :rule-classes :linear)) + +;;; If size(t1) = size(sigma(t1)) and t1 is not an instance of sigma(t1) +;;; then the number of variables of t1 is greater tha the number of +;;; variables of sigma(t1) + + (defthm n-variables-decreases + (let ((sigmar (normal-form-subst flg sigma t1))) + (implies + (and + (equal (size flg t1) (size flg (apply-subst flg sigma t1))) + (not (equal (apply-subst flg + (inverse sigmar) + (apply-subst flg sigma t1)) + t1))) + + (< (len (make-set (variables flg (apply-subst flg sigma t1)))) + (len (make-set (variables flg t1)))))) + :rule-classes :linear + :hints (("Goal" :in-theory (disable domain-restriction)))))) + + + +(local + (encapsulate + () + +;;; If delta is a variable substitution, then the length of the list of +;;; variables of t1 and the list of variables of delta(t1) is the same. +;;; Note that this common length is the number of variable positions of +;;; t1. + + (local + (defthm n-variables-bounded-substitution-variable-almost + (implies (variable-substitution delta) + (equal (len (variables flg (apply-subst flg delta term))) + (len (variables flg term)))) + :hints (("Goal" + :use (:instance variables-apply-subst-variable-substitution) + :in-theory + (disable variables-apply-subst-variable-substitution))))) + + +;;; The following lemma gives a bound for the number of distinct +;;; variables of the terms of a chain t1 <= t2 <= t3 <= ..., all having +;;; the same size. This bound is the number of variables positions of t1. + + (defthm n-variables-bounded-substitution-variable + (implies (variable-substitution + (normal-form-subst flg sigma t1)) + (equal (len (variables flg (apply-subst flg sigma t1))) + (len (variables flg t1)))) + :hints (("Goal" + :use + ((:instance + n-variables-bounded-substitution-variable-almost + (term t1) + (delta (restriction sigma + (make-set (variables flg t1))))))))))) + + + +;;; A technical lemma + + +(local + (defthm completeness-in-reverse-order + (implies (not (subs t1 t2)) + (not (equal (instance t1 delta) t2))) + :hints (("Goal" :use (:instance subs-completeness))))) + + +;;; ============================================================================ +;;; 3. The well-foundedness theorem +;;; ============================================================================ + +;;; ===== SUBSUMPTION-MEASURE +;;; An ordinal measure to prove well-foundedness of subsumption. +;;; The lexicographic combination of the size of the term and the +;;; difference between the number of variable positions and the number +;;; of distinct variables. + + +(defun subsumption-measure (term) + (make-ord (1+ (size t term)) + 1 + (- (len (variables t term)) + (len (make-set (variables t term)))))) + + +;;; Lemma: well-foundedness, instance version + +(local + (defthm subsumption-well-founded-instance-version + (implies (not (subs (instance t1 sigma) t1)) + (o< (subsumption-measure t1) + (subsumption-measure (instance t1 sigma)))) + :rule-classes nil)) + + +;;; Lemma: subsumption-measure, o-p + +(local + (defthm subsumption-measure-o-p + (o-p (subsumption-measure term)))) + +;;; An upper bound for subsumption-measure (omega^{omega}) + + +(defthm subsumption-measure-upper-bounded + (o< (subsumption-measure term) (make-ord (omega) 1 0))) + +;;; REMARK: This lemma is not needed here, but will be useful in +;;; lattice-of-terms.lisp where an additional top term is added. + + +(in-theory (disable subsumption-measure)) + + +;;; ======== STRICT-SUBS +;;; The strict subsumption relation + +(defun strict-subs (t1 t2) + (and (subs t1 t2) (not (subs t2 t1)))) + + +;;; =============================== +;;; The well-foundedness theorem +;;; =============================== + + +(defthm subsumption-well-founded + (and (o-p (subsumption-measure t1)) + (implies (strict-subs t1 t2) + (o< (subsumption-measure t1) + + (subsumption-measure t2)))) + :rule-classes (:rewrite :well-founded-relation) + :hints (("Goal" :use + (:instance subsumption-well-founded-instance-version + (sigma (matching t1 t2)))))) diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption.lisp new file mode 100644 index 0000000..4a36b0f --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption.lisp @@ -0,0 +1,567 @@ +;;; subsumption.lisp Definition of a particular RULE-BASED matching +;;; algorithm between terms. We use functional instantion of the +;;; pattern given in matching.lisp Using this algorithm, we define the +;;; subsumption relation between terms and lists of terms in a +;;; constructive way, and we prove that subsumption is a preorder. +;;; Created: 11-10-99 Last revison: 07-12-2000 +;;; ============================================================================= + +#| To certify this book: + +(in-package "ACL2") + +(certify-book "subsumption") + +|# + +(in-package "ACL2") +(local (include-book "matching")) +(include-book "terms") +(include-book "../../../../ordinals/e0-ordinal") +(set-well-founded-relation e0-ord-<) + +;;; ************************************************* +;;; A PARTICULAR AND EXECUTABLE SUBSUMPTION ALGORITHM +;;; ************************************************* + +;;; Here we show how we can obtain a correct subsumption algorithm from +;;; the "pattern" verified in subsumption-definition.lisp: +;;; - We define a particular selection function. +;;; - We introduce multi-values to deal with the pair of systems +;;; S-match. +;;; - Some other minor improvements concerning efficency are done. +;;; - Guards are verified, allowing execution in raw Common Lisp. + +;;; ============================================================================ +;;; 1. The subsumption algorithm between terms +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 1.1 A particular version of transform-subs +;;; ---------------------------------------------------------------------------- + +;;; Selection function. If we detect an inmediate fail, we select it. + +(defun sel-match (S) + (declare (xargs :guard (and (consp S) (system-p S)))) + (if (endp (cdr S)) + (car S) + (let* ((equ (car S)) + (t1 (car equ)) + (t2 (cdr equ))) + (cond ((variable-p t1) + (sel-match (cdr S))) + ((variable-p t2) equ) + ((eql (car t1) (car t2)) + (sel-match (cdr S))) + (t equ))))) + +;;; Main property, needed to instantiate from +;;; subsumption-definition.lisp: +(local + (defthm sel-match-select-a-pair + (implies (consp S) + (member (sel-match S) S)))) + + +;;; The following lemmas help the guard verification of +;;; transform-subs (although they are not strictly needed) + +(local + (defthm sel-match-consp + (implies (and (consp S) + (alistp S)) + (consp (sel-match S))) + :rule-classes :type-prescription)) + + +(encapsulate + () + (local + (defthm transform-subs-guard-verification-stuff-1 + (implies (and (system-p S) + (member equ S)) + (and + (implies (variable-p (car equ)) (eqlablep (car equ))) + (implies (variable-p (cdr equ)) (eqlablep (cdr equ))))))) + + + (local + (defthm transform-subs-guard-verification-stuff-2 + (implies (and (system-p S) + (member equ S)) + (and + (eqlablep (cadr equ)) + (true-listp (cdar equ)) + (true-listp (cddr equ)) + (iff (variable-p (car equ)) (eqlablep (car equ))) + (iff (variable-p (cdr equ)) (eqlablep (cdr equ))))))) + +;;; The rules of transformation: + + (defun transform-subs (S match) + (declare (xargs :guard (and (consp S) (system-p S) + (alistp match)))) + (let* ((ecu (sel-match S)) + (t1 (car ecu)) (t2 (cdr ecu)) + (R (eliminate ecu S))) + (cond + ((variable-p t1) + (let ((bound (assoc t1 match))) + (if bound + (if (equal (cdr bound) t2) + (mv R match t) + (mv nil nil nil)) + (mv R (cons (cons t1 t2) match) t)))) + ((variable-p t2) (mv nil nil nil)) + ((eql (car t1) (car t2)) + (mv-let (empareja bool) + (pair-args (cdr t1) (cdr t2)) + (if bool + (mv (append empareja R) match t) + (mv nil nil nil)))) + (t (mv nil nil nil)))))) + + +;;; REMARK: transform-subs will not be the counterpart of +;;; transform-subs in our functional instantiation. Instead we have to +;;; define a function acting on pair of systems: + +(local + (defun transform-subs-bridge (S-match) + (mv-let (S1 match1 bool1) + (transform-subs (car S-match) (cdr S-match)) + (if bool1 (cons S1 match1) nil)))) + +;;; ---------------------------------------------------------------------------- +;;; 1.2 A particular version of a matching algorithm for systems of equations +;;; ---------------------------------------------------------------------------- + + +;;; Termination properties of transform-subs. + +(local + (defthm transform-subs-decreases-length-of-first-system + (implies (consp S) + (e0-ord-< (length-system (first (transform-subs S match))) + (length-system S))) + :hints (("Goal" :use ((:functional-instance + (:instance + transform-subs-sel-decreases-length-of-first-system + (S-match (cons S match))) + (transform-subs-sel transform-subs-bridge) + (a-pair sel-match))))))) + +;;; A particular version of subs-system + +(defun subs-system (S match bool) + (declare (xargs + :guard (and (system-p S) (alistp match)) + :measure (length-system S) + :hints (("Goal" :in-theory (disable transform-subs))))) + (if (or (not bool) (not (consp S))) + (mv S match bool) + (mv-let (S1 match1 bool1) + (transform-subs S match) + (subs-system S1 match1 bool1)))) + +;;; Matching algorithm for systems of equations: + +(defun match-mv (S) + (declare (xargs :guard (system-p S))) + (mv-let (S1 sol1 bool1) + (subs-system S nil t) + (declare (ignore S1)) + (mv sol1 bool1))) + +;;; REMARK: Again, subs-system and match-mv will not be the counterpart +;;; of subs-system-sel, match-sel in our functional instantiation, +;;; because of signature mismatch. Instead we have to +;;; define functions acting on pair of systems: + +(local + (defun subs-system-bridge (S-match) + (if (normal-form-syst S-match) + S-match + (mv-let (S1 match1 bool1) + (subs-system (car S-match) (cdr S-match) t) + (if bool1 (cons S1 match1) nil))))) + + + +(local + (defun match-mv-bridge (S) + (let ((subs-system-bridge (subs-system-bridge (cons S nil)))) + (if subs-system-bridge (list (cdr subs-system-bridge)) nil)))) + + + +;;; ---------------------------------------------------------------------------- +;;; 1.3 Main properties of the matching algorithm for systems of equations +;;; ---------------------------------------------------------------------------- + +;;; Some technical lemmas + +(local + (defthm booleanp-third-subs-system + (implies (booleanp bool) + (booleanp (third (subs-system S match bool)))) + :rule-classes :type-prescription)) + +(local + (defthm nil-third-implies-nil-second-subs-system + (implies (not (third (subs-system s match t))) + (not (second (subs-system s match t)))))) + +;;; And the main properties of match-mv + +(defthm match-mv-soundness + (implies (second (match-mv S)) + (matcher (first (match-mv S)) S)) + :hints (("Goal" :use ((:functional-instance + match-sel-soundness + (match-sel match-mv-bridge) + (subs-system-sel subs-system-bridge) + (transform-subs-sel transform-subs-bridge) + (a-pair sel-match)))))) + + +(defthm match-mv-completeness + (implies (matcher sigma S) + (second (match-mv S))) + :hints (("Goal" :use ((:functional-instance + match-sel-completeness + (match-sel match-mv-bridge) + (subs-system-sel subs-system-bridge) + (transform-subs-sel transform-subs-bridge) + (a-pair sel-match)))))) + + +(defthm match-mv-substitution-s-p + (implies (system-s-p S) + (substitution-s-p (first (match-mv S)))) + :hints (("Goal" :use ((:functional-instance + match-sel-substitution-s-p + (match-sel match-mv-bridge) + (subs-system-sel subs-system-bridge) + (transform-subs-sel transform-subs-bridge) + (a-pair sel-match)))))) + + +;;; ---------------------------------------------------------------------------- +;;; 1.4 A particular and executable version of subsumption of two terms. +;;; ---------------------------------------------------------------------------- + +;;; The subsumption algorithm + +(defun subs-mv (t1 t2) + (declare (xargs :guard (and (term-p t1) (term-p t2)))) + (match-mv (list (cons t1 t2)))) + +;;; The subsumption relation + +(defun subs (t1 t2) + (declare (xargs :guard (and (term-p t1) (term-p t2)))) + (mv-let (matching subs) + (subs-mv t1 t2) + (declare (ignore matching)) + subs)) + +;;; The witness substitution for matching (when (subs t1 t2)) + +(defun matching (t1 t2) + (declare (xargs :guard (and (term-p t1) (term-p t2)))) + (mv-let (matching subs) + (subs-mv t1 t2) + (declare (ignore subs)) + matching)) + + +;;; REMARK: +;;; subs-mv will be used to compute the subsumption relation and +;;; matching substitutions at the same time. The functions subs and +;;; matching are defined to be used in the statements of theorems. + + +;;; ---------------------------------------------------------------------------- +;;; 1.5 Fundamental properties of subs, matching and subs-mv +;;; ---------------------------------------------------------------------------- +;;; Most of these properties are obtained by functional instantiation. + +;;; Soundness +;;; ········· + +(defthm subs-soundness + (implies (subs t1 t2) + (equal (instance t1 (matching t1 t2)) t2)) + :rule-classes (:rewrite :elim) + :hints (("Goal" :use + (:instance match-mv-soundness (S (list (cons t1 t2))))))) + + +;;; Completeness +;;; ············· + +(defthm subs-completeness + (implies (equal (instance t1 sigma) t2) + (subs t1 t2)) + :rule-classes nil + :hints (("Goal" :use + (:instance match-mv-completeness (S (list (cons t1 t2))))))) + +;;; Substitution-s-p (closure property) +;;; ··································· + + +(defthm matching-substitution-s-p + (implies (and (term-s-p t1) (term-s-p t2)) + (substitution-s-p (matching t1 t2))) + :hints (("Goal" :use + (:instance match-mv-substitution-s-p (S (list (cons t1 t2))))))) + +;;; Substitution-p (needed for guard verification) +;;; ·············································· + + +(defthm matching-substitution-p + (implies (and (term-p t1) (term-p t2)) + (substitution-p (matching t1 t2))) + :hints (("Goal" :use (:functional-instance + matching-substitution-s-p + (signat (lambda (x n) (eqlablep x))) + (term-s-p-aux term-p-aux) + (substitution-s-p substitution-p))))) + +;;; Later, We will disable match-mv, subs-mv, matching and subs and +;;; their executable counter-parts, to be sure that ONLY the above two +;;; properties are used in the sequel. But before doing this, we state +;;; the relations between subs-mv and subs and matching. Note that, from +;;; now on, we will not assume any relations between match-mv and +;;; subs-mv + +(defthm subs-mv-subs + (equal (second (subs-mv t1 t2)) (subs t1 t2))) + +(defthm subs-mv-matching + (equal (first (subs-mv t1 t2)) (matching t1 t2))) + + + +;;; ============================================================================ +;;; 2. The subsumption algorithm between lists of terms +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 2.1 Subsumption between lists of terms +;;; ---------------------------------------------------------------------------- + +;;; Sometimes it will be useful to talk abou subsumption between lists +;;; of terms (see, for example, kb/critical-pairs.lisp). We define here +;;; such concept and its main properties, in a similar way to subs. + +;;; The subsumption algorithm (between lists of terms) + +(defun subs-list-mv (l1 l2) + (declare (xargs :guard (and (term-p-aux nil l1) + (term-p-aux nil l2)))) + (mv-let (pair-lists bool) + (pair-args l1 l2) + (if bool (match-mv pair-lists) (mv nil nil)))) + + + +;;; The subsumption relation between lists of terms + +(defun subs-list (l1 l2) + (declare (xargs :guard (and (term-p-aux nil l1) + (term-p-aux nil l2)))) + (mv-let (matching subs-list) + (subs-list-mv l1 l2) + (declare (ignore matching)) + subs-list)) + +;;; The witness substitution for matching lists of terms (when +;;; (subs-list l1 l2)) + +(defun matching-list (l1 l2) + (declare (xargs :guard + (and (term-p-aux nil l1) + (term-p-aux nil l2)))) + (mv-let (matching subs-list) + (subs-list-mv l1 l2) + (declare (ignore subs-list)) + matching)) + + +;;; ---------------------------------------------------------------------------- +;;; 2.2 Main properties of subsumption between lists of terms +;;; ---------------------------------------------------------------------------- + +;;; Two previous lemmas relating matcher with instances: + +(local + (defthm matcher-apply-subst-nil + (implies (second (pair-args l1 l2)) + (iff (matcher sigma (first (pair-args l1 l2))) + (equal (apply-subst nil sigma l1) l2))))) + + +(local + (defthm apply-subst-nil-pair-args + (second (pair-args l1 (apply-subst nil sigma l1))))) + +;;; Soundness +;;; ········· + + +(defthm subs-list-soundness + (implies (subs-list l1 l2) + (equal (apply-subst nil (matching-list l1 l2) l1) l2)) + :rule-classes (:rewrite :elim) + :hints (("Goal" :use + (:instance match-mv-soundness (S (first (pair-args l1 l2))))))) + + +;;; Completeness +;;; ············· + +(defthm subs-list-completeness + (implies (equal (apply-subst nil sigma l1) l2) + (subs-list l1 l2)) + :rule-classes nil + :hints (("Goal" :use + (:instance match-mv-completeness (S (first (pair-args l1 l2))))))) + +;;; Substitution-s-p (closure property) +;;; ··································· + + +(defthm matching-list-substitution-s-p + (implies (and (term-s-p-aux nil l1) (term-s-p-aux nil l2)) + (substitution-s-p (matching-list l1 l2))) + :hints (("Goal" :use + (:instance match-mv-substitution-s-p + (S (first (pair-args l1 l2))))))) + + + +;;; Substitution-p (needed for guard verification) +;;; ·············································· + + +(defthm matching-list-substitution-p + (implies (and (term-p-aux nil l1) + (term-p-aux nil l2)) + (substitution-p (matching-list l1 l2))) + :hints (("Goal" :use (:functional-instance + matching-list-substitution-s-p + (signat (lambda (x n) (eqlablep x))) + (term-s-p-aux term-p-aux) + (substitution-s-p substitution-p))))) + + +;;; As with subs, we will disable the definitions related to subs-list to be +;;; sure that ONLY the above two properties are used in the sequel. But +;;; before doing this, we state the relations between subs-list-mv and subs-list +;;; and matching-list. + +(defthm subs-list-mv-subs-list + (equal (second (subs-list-mv t1 t2)) (subs-list t1 t2))) + +(defthm subs-list-mv-matching-list + (equal (first (subs-list-mv t1 t2)) (matching-list t1 t2))) + + +(in-theory + (disable + subs-list-mv (subs-list-mv) subs-list (subs-list) matching-list + (matching-list))) + + + +;;; ============================================================================ +;;; 3. Properties of the subsumption relation +;;; ============================================================================ + + +(in-theory + (disable + match-mv (match-mv) subs-mv (subs-mv) subs (subs) matching (matching))) + + +;;; REMARK: Note that the properties described below only use the +;;; soundness and completeness properties of the subsumption +;;; algorithm (the definition and executable-counterpart of subs +;;; are disabled) + + +;;; ---------------------------------------------------------------------------- +;;; 3.1 Subsumption is a quasi-order +;;; ---------------------------------------------------------------------------- + +;;;; Subsumption reflexive +;;;; ····················· + +(defthm subsumption-reflexive + (subs t1 t1) + :hints (("Goal" :use (:instance + subs-completeness + (sigma nil) (t2 t1))))) + + +;;;; Subsumption transitive +;;;; ······················ + + +(defthm subsumption-transitive + (implies (and (subs t1 t2) (subs t2 t3)) + (subs t1 t3)) + :hints (("Goal" :use ((:instance + subs-completeness + (sigma (composition + (matching t2 t3) + (matching t1 t2))) + (t2 t3)))))) + +(in-theory (disable subsumption-transitive )) + +;;; ---------------------------------------------------------------------------- +;;; 3.2 Several properties of subsumption +;;; ---------------------------------------------------------------------------- + +;;; An useful rule: +;;; ··············· + +(defthm subsumption-apply-subst + (subs term (instance term sigma)) + :hints (("Goal" :use (:instance subs-completeness + (t1 term) (t2 (instance term sigma)))))) + +;;; Variables are minimum elements in this quasi-order +;;; ·················································· + +(defthm variable-minimum-subsumption + (implies (variable-p x) + (subs x term)) + :hints (("Goal" :use ((:instance subs-completeness + (sigma (list (cons x term))) + (t1 x) + (t2 term)))))) + +(in-theory (disable variable-minimum-subsumption)) + +(defthm minimum-subsumption-implies-variable + (implies (and (variable-p x) (subs term x)) + (variable-p term)) + :hints (("Goal" :use (:instance + apply-returns-variable-implies-variable + (flg t) (sigma (matching term x))))) + :rule-classes nil) + + + + + + + + diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/terms.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/terms.lisp new file mode 100644 index 0000000..95af93c --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/terms.lisp @@ -0,0 +1,1535 @@ +;;; terms.lisp +;;; Properties about terms, substitutions, and system of equations. +;;; Created: 7-10-99 Last revison: 15-02-2001 +;;; ============================================================================= + +#| To certify this book: + +(in-package "ACL2") + +(certify-book "terms") + +|# + + +(in-package "ACL2") +(include-book "basic") + +;;; ******************************************************************* +;;; BASIC PROPERTIES ABOUT FIRST-ORDER TERMS, SUBSTITUTIONS AND SYSTEM +;;; OF EQUATIONS. +;;; ******************************************************************* + + +;;; ============================================================================ +;;; 1. Terms +;;; ============================================================================ + + + +;;; ---------------------------------------------------------------------------- +;;; 1.1 Representation of terms +;;; ---------------------------------------------------------------------------- + +;;; We will represent first-order terms in prefix notation, using +;;; lists. For example, the term f(x h(a) g(x y b)), where x, y are +;;; variables and a, b are constants is represented as +;;; (f x (h (a) (g x y (b)). +;;; Note that constants are considered as 0-ary functions. + + +;;; The following functions define the set of well-formed terms (and +;;; list of terms) in a given signature We will prove later that our +;;; main functions acting on terms are closed in the set of terms of a +;;; given signature (the closure theorems). + +;;; A signature is defined to be a function of two arguments. The +;;; intended meaning is that receiving as input a symbol function and a +;;; natural number, we return t if the arity of the symbol is n, and nil +;;; otherwise. This will allows to represent infinite signatures and +;;; variadic symbol functions. + +;;; A general signature: + +(defstub signat (* *) => *) + + +;;; EXAMPLE: +;;; This is for example, the signature of group theory +; (defun signat (symb n) +; (let* ((sig '((* 2) (i 1) (e 0))) +; (found (assoc symb sig)) +; (arity (cdr found))) +; (and found (member n arity)))) + + +;;; The variables of terms in a given signature, will be restricted to +;;; eqlablep ACL2 objects. This is due to two reasons: +;;; - First we restrict the kind objects that can be considered as +;;; variables in a given language, to discard "strange" cases. + +;;; - Second, in this way well-formed terms (as defined by term-p below) +;;; can be seen as terms in a particular signature. This will allow to +;;; export the closure theorems to guard theorems, as we will see. + +;;; Thus we define variable-s-p as eqlablep, a predicate for recognizing +;;; variables of terms in a given signature. + +(defmacro variable-s-p (x) `(eqlablep ,x)) + +;;; ====== TERM-S-P, TERM-S-P-AUX + + +;;; term-s-p-aux define terms and lists of terms in a given +;;; signature. We define at the same time terms and lists of terms, +;;; using a standard trick for mutual recursion. (term-s-p-aux flg x) is +;;; t if flg=nil and x is a list of terms in a signature or flg /= nil +;;; and x is a term in a signature. Nil otherwise. + +(defun term-s-p-aux (flg x) + (if flg + (if (atom x) + (variable-s-p x) + (if (signat (car x) (len (cdr x))) + (term-s-p-aux nil (cdr x)) + nil)) + (if (atom x) + (equal x nil) + (and (term-s-p-aux t (car x)) + (term-s-p-aux nil (cdr x)))))) + +(defmacro term-s-p (x) + `(term-s-p-aux t ,x)) + + +;;; ====== TERM-P, TERM-P-AUX + + +;;; For guard verification purposes, we will define a function term-p +;;; defining "proper" representation of first-order terms, i.e., the +;;; kind of Common Lisp objects that our functions are expected to +;;; receive as input when executed. As for terms in a signature, this is +;;; done for terms and for lists of terms. Note that we require that +;;; variables and function symbols have to be eqlablep objects. This +;;; will allow us to use eql instead of equal in executable functions, +;;; making them more efficient. + + +(defun term-p-aux (flg x) + (declare (xargs :guard t)) + (if flg + (if (atom x) + (eqlablep x) + (and (eqlablep (car x)) + (term-p-aux nil (cdr x)))) + (if (atom x) + (equal x nil) + (and (term-p-aux t (car x)) + (term-p-aux nil (cdr x)))))) + +(defmacro term-p (x) + (declare (xargs :guard t)) + `(term-p-aux t ,x)) + + + + +;;; VERY IMPORTANT REMARK: NON-PROPER TERMS +;;; *************************************** + +;;; Having defined the above functions, nevertheless, since ACL2 is a +;;; logic of total functions, our functions acting on terms are defined +;;; for every object, even for those not representing "proper" terms, as +;;; defined by term-s-p and term-p. Our definitions will deal +;;; with the "non-proper" case in such a way that our theorems do not +;;; need hypothesis of the form "(term-p term)" or "(term-s-p term)" +;;; (except those concerning guard verification or closure properties, +;;; as we will see later). + +;;; Thus, we can see any ACL2 object as a representation of a term, in +;;; the following way: + +;;; - Variables are atomic objects. +;;; - Every consp object can be seen as the term with the top function +;;; symbol in its car. The cdr is the list of its arguments. + + +;;; ====== VARIABLE-P +;;; x is a variable (in a wide sense) +;;; Similar to variable-s-p, we define variable-p, recognizing those +;;; ACL2 objects that can be considered as variables with this wide +;;; point of view. + +(defun variable-p (x) + (declare (xargs :guard t)) + (atom x)) + +;;; REMARKS: +;;; -------- + +;;; - Note that this function variable-p is not strictly needed (we +;;; could use atom), but it improves readability of the proofs +;;; developed by the prover. +;;; - This could be optimized if we used a macro definition instead of +;;; defun. But we prefer to disable variable-p after proving its main +;;; properties, for the sake of readability of theorems and proofs +;;; (maybe we will modify it later). +;;; - Note that variable-s-p implies variable-p. The reverse implication +;;; is not true. + + +;;; Before disabling variable-p, we prove its main property: + +(defthm non-variables-are-consp + (equal (variable-p x) + (not (consp x))) + :rule-classes :compound-recognizer) + +(in-theory (disable variable-p)) + + +;;; IMPORTANT REMARK: from the discussions above, note that we are +;;; guided by the following principle: + +;;; - To reason, it is better not to restrict the kind of objects we are +;;; deling with, since the theorems are more general, and often easier +;;; to prove (in addition, we will prove the corresponding closure +;;; theorems). +;;; - For execution (i.e., for guard verification), it is better to restrict +;;; if we can improve eficiency. For example, restricting variables and +;;; function symbols to be eqlablep objects allows us to replace eql by +;;; equal (when comparing variables or function symbols). + +;;; ---------------------------------------------------------------------------- +;;; 1.2 Some functions on terms. +;;; ---------------------------------------------------------------------------- + +;;; REMARK: Note that the following functions are defined for terms and +;;; for list of terms, using mutual recursion. If the flag flg is not nil, +;;; then we refer to terms and if flg is nil, we refer to lists of terms. + +;;; ====== VARIABLES +;;; The list of variables of a term + + +(defun variables (flg term) + (declare (xargs :guard (term-p-aux flg term) + :verify-guards nil)) + (if flg + (if (variable-p term) + (list term) + (variables nil (cdr term))) + (if (endp term) + nil + (append (variables t (car term)) + (variables nil (cdr term)))))) + +;;; Needed for guard verification: +(defthm variables-true-listp + (true-listp (variables flg term))) + +(verify-guards variables) + + +;;; ======= LIST-OF-VARIABLES-P +(defun list-of-variables-p (l) + (if (endp l) + t + (and (variable-p (car l)) + (list-of-variables-p (cdr l))))) + + +(defthm variables-is-a-list-of-variables + (list-of-variables-p (variables flg term))) + + +(encapsulate + () + + (local + (defthm list-of-variables-p-subsetp + (implies (and (list-of-variables-p l) + (subsetp m l)) + (list-of-variables-p m)))) + + (defcong equal-set iff (list-of-variables-p l) 1)) + + +;;; ======= MAKE-VAR and related macros + + +(defmacro make-var (t1 t2) `(list 'var ,t1 ,t2)) + +(defmacro compound-var (x) `(equal (car ,x) 'var)) + +(defmacro first-of-var (x) `(second ,x)) + +(defmacro second-of-var (x) `(third ,x)) + + +;;; ======= VARIABLES-SET +;;; The set of variables of a term. + +(defmacro variables-set (flg term) + `(make-set (variables ,flg ,term))) + + + +;;; ======= N-VARIABLES +;;; Number of distinct variables + +(defmacro n-variables (flg term) + `(len (variables-set ,flg ,term))) + +;;; ======= SIZE +;;; Number of function symbols of a term + +(defun size (flg term) + (if flg + (if (variable-p term) + 0 + (+ 1 (size nil (cdr term)))) + (if (endp term) + 0 + (+ (size t (car term)) + (size nil (cdr term)))))) + + +;;; ======= LENGTH +;;; Number of symbols of a term (including variables) + +(defun length-term (flg term) + (if flg + (if (variable-p term) + 1 + (1+ (length-term nil (cdr term)))) + (if (endp term) + 0 + (+ (length-term t (car term)) + (length-term nil (cdr term)))))) + +(defthm length-term-positive + (< 0 (length-term t term)) + :rule-classes :linear) + +;;; ========== SUBTERM + +(defun subterm (flg t1 t2) + (if flg + (if (equal t1 t2) + t + (if (variable-p t2) + nil + (subterm nil t1 (cdr t2)))) + (if (endp t2) + nil + (or (subterm t t1 (car t2)) + (subterm nil t1 (cdr t2)))))) + + + + + +;;; ============================================================================ +;;; 2. Substitutions. +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 2.1 Representation of substitutions. +;;; ---------------------------------------------------------------------------- + + +;;; We represent substitutions as lists of pairs of the form +;;; (variable . term). As with terms, we can view every object as a +;;; substitution. See section 4 of basic.lisp. +;;; Anyway, we define substitution-p for guard verification purposes, +;;; and substitution-s-p to define substitutions in a given signature. + + +;;; ====== SUBSTITUTION-P + +(defun substitution-p (l) + (declare (xargs :guard t)) + (if (atom l) + (equal l nil) + (and (consp (car l)) + (eqlablep (caar l)) + (term-p (cdar l)) + (substitution-p (cdr l))))) + +;;; ====== SUBSTITUTION-S-P + +(defun substitution-s-p (l) + (if (atom l) + (equal l nil) + (and (consp (car l)) + (variable-s-p (caar l)) + (term-s-p (cdar l)) + (substitution-s-p (cdr l))))) + + +;;; ---------------------------------------------------------------------------- +;;; 2.2 Applying substitutions to terms (and lists of terms) +;;; ---------------------------------------------------------------------------- + +;;; ==== APPLY-SUBST + +(defun apply-subst (flg sigma term) + (declare (xargs :guard (and (alistp sigma) + (term-p-aux flg term)))) + (if flg + (if (variable-p term) + (val term sigma) + (cons (car term) + (apply-subst nil sigma (cdr term)))) + (if (endp term) + term + (cons (apply-subst t sigma (car term)) + (apply-subst nil sigma (cdr term)))))) + +;;; REMARK: the substitution does not change the final tail of the lists +;;; (this is essential for having the same properties for proper and +;;; non-proper terms) + +(defmacro instance (term sigma) + `(apply-subst t ,sigma ,term)) + +;;; Some useful lemmas: + +(defthm apply-consp-is-consp-list-of-terms + (equal (consp (apply-subst nil sigma l)) + (consp l))) + +(defthm apply-returns-variable-implies-variable + (implies (and flg (not (variable-p term))) + (not (variable-p (apply-subst flg sigma term))))) + + +(defthm equal-len-apply-subst-nil + (equal (len (apply-subst nil sigma term)) + (len term))) + + +(defthm apply-atom + (implies (atom sigma) + (equal (apply-subst flg sigma term) term))) + +(defthm one-identity-substitution + (equal (apply-subst flg nil term) term)) + + +(in-theory (disable apply-atom)) + + + + +;;; The following lemmas proves closure properties w.r.t a given +;;; signature and they are needed for guard verification. + +(defthm val-substitution-s-p-term-s-p + (implies (and (substitution-s-p sigma) + (variable-s-p x)) + (term-s-p (val x sigma)))) + +(defthm apply-subst-term-s-p-aux + (implies (and (term-s-p-aux flg term) + (substitution-s-p sigma)) + (term-s-p-aux flg (apply-subst flg sigma term)))) + +(defthm apply-subst-term-p-aux + (implies (and (term-p-aux flg term) + (substitution-p sigma)) + (term-p-aux flg (apply-subst flg sigma term))) + :hints (("Goal" :use (:functional-instance + apply-subst-term-s-p-aux + (signat (lambda (x n) (eqlablep x))) + (term-s-p-aux term-p-aux) + (substitution-s-p substitution-p))))) + +;;; IMPORTANT REMARK: It can be proved without the hint. But this a good +;;; example of how the concept of well-formed term is a particular case +;;; of the general concept of term in a given signature. We will use +;;; this technique very often. + + +;;; ==== SUBSTITUTE-VAR +;;; Replace every occurrence of a given variable x by a given term t1. + +(defun substitute-var (x t1 flg term) + (declare (xargs :guard (term-p-aux flg term))) + (if flg + (if (variable-p term) + (if (eql x term) + t1 + term) + (cons (car term) + (substitute-var x t1 nil (cdr term)))) + (if (endp term) + term + (cons (substitute-var x t1 t (car term)) + (substitute-var x t1 nil (cdr term)))))) + + + +;;; ---------------------------------------------------------------------------- +;;; 2.3 Functional aspects of substitutions. +;;; ---------------------------------------------------------------------------- + + +;;; ====== COMPOSITION +;;; Composition of two substitutions + +(defun composition (sigma1 sigma2) + (declare (xargs :guard (and (alistp sigma1) + (substitution-p sigma2)))) + (if (endp sigma2) + sigma1 + (cons (cons (caar sigma2) (apply-subst t sigma1 (cdar sigma2))) + (composition sigma1 (cdr sigma2))))) + +;;; Lemmas: + +(defthm value-composition + (implies (variable-p x) + (equal (val x (composition sigma1 sigma2)) + (apply-subst t sigma1 (val x sigma2))))) + + +(defthm composition-of-substitutions-apply + (equal (apply-subst flg (composition sigma1 sigma2) term) + (apply-subst flg sigma1 (apply-subst flg sigma2 term)))) + +;;; Closure property + +(defthm composition-substitution-s-p + (implies (and (substitution-s-p sigma1) + (substitution-s-p sigma2)) + (substitution-s-p (composition sigma1 sigma2)))) + +;;; ========= RESTRICTION (see basic.lisp) + +(defthm subsetp-restriction + (implies (subsetp (variables flg term) l) + (equal (apply-subst flg (restriction sigma l) term) + (apply-subst flg sigma term)))) + +;;; ========= DOMAIN (see basic.lisp) + +(defthm x-not-in-domain-remains-the-same + (implies (not (member x (domain sigma))) + (equal (val x sigma) x))) + +(in-theory (disable x-not-in-domain-remains-the-same)) + + +(defthm substitution-does-not-change-term + (implies (disjointp (domain sigma) (variables flg term)) + (equal (apply-subst flg sigma term) term)) + :hints (("Goal" + :in-theory (enable x-not-in-domain-remains-the-same)))) + + +(in-theory (disable substitution-does-not-change-term)) + +;;; ========= UNION OF SUBSTITUTIONS + +;;; Lemmas about union of substitutions of disjoint domains +;;; They will be used in mg-instance.lisp and in +;;; critical-pairs.lisp + +(defthm only-the-first-bind-is-important-append + (implies (subsetp (variables flg term) (domain sigma1)) + (equal (apply-subst flg (append sigma1 sigma2) term) + (apply-subst flg sigma1 term)))) + +(local + (defthm domains-disjointp-do-not-interfere-lemma + (implies (and (disjointp (domain sigma1) + (domain sigma2)) + (member term (domain sigma2))) + (equal (val term (append sigma1 sigma2)) + (val term sigma2))))) + +(defthm domains-disjointp-do-not-interfere + (implies (and (disjointp (domain sigma1) (domain sigma2)) + (subsetp (variables flg term) (domain sigma2))) + (equal (apply-subst flg (append sigma1 sigma2) term) + (apply-subst flg sigma2 term)))) + + +;;; ====== COINCIDE + +;;; This will be our predicate for testing the equality +;;; of substitutions. sigma1 and sigma2 coincide in l if their +;;; restriction to l are equal. + +(defun coincide (sigma1 sigma2 l) + (if (atom l) + T + (and (equal (val (car l) sigma1) + (val (car l) sigma2)) + (coincide sigma1 sigma2 (cdr l))))) + + +;;; Properties of coincide + + +(encapsulate + () + (local + (defthm coincide-main-property + (implies (and (coincide sigma1 sigma2 l) + (member x l)) + (equal (equal (val x sigma1) (val x sigma2)) t)))) +;;; Note: this form of the rule avoids cycles. + + + (defthm coincide-in-term + (implies (and + (subsetp (variables flg term) l) + (coincide sigma1 sigma2 l)) + (equal (apply-subst flg sigma1 term) + (apply-subst flg sigma2 term))) + :rule-classes nil)) + +(defthm coincide-reflexive + (coincide sigma sigma l)) + +(defthm coincide-append + (equal (coincide sigma sigma1 (append l m)) + (and (coincide sigma sigma1 l) + (coincide sigma sigma1 m)))) + + +;;; ======== EXTENSION + +;;; sigma1 "extends" sigma + +(defmacro extension (sigma1 sigma) + `(coincide ,sigma ,sigma1 (domain ,sigma))) + +;;; ======== NORMAL-FORM-SUBST + +;;; Given a term (or a list of terms), there are an infinite number of +;;; substitutions acting in the same way on the term. Sometimes, it will +;;; be useful to take a representative of all those functions. + +(defmacro normal-form-subst (flg sigma term) + `(restriction ,sigma (make-set (variables ,flg ,term)))) + +(defthm equal-normal-form-subst-wrt-term + (equal (apply-subst flg (normal-form-subst flg sigma term) term) + (apply-subst flg sigma term)) + :rule-classes nil) + + +;;; ============================================================================ +;;; 3. Systems of equations. +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 3.1 Representation +;;; ---------------------------------------------------------------------------- + + +;;; Every object ecu can be seen as an equation, +;;; being its left side (car ecu) and its right side (cdr ecu). + +;;; ========== LHS and RHS +;;; The left-hand side and right-hand side of +;;; an equation or rule: + +(defmacro lhs (equ) + `(car ,equ)) + +(defmacro rhs (equ) + `(cdr ,equ)) + + + +;;; Note that atomic objects are equivalent to '(nil . nil). Every +;;; object can be interpreted as a system of equations: a list of +;;; equations. Note that atomic objects are empty systems. It is +;;; interesting to note that we use the same representation for systems +;;; and for substitutions. +;;; Nevertheless, we define system-p for guard verification: + +;;; ========= SYSTEM-P + +(defun system-p (S) + (declare (xargs :guard t)) + (if (atom S) + (equal S nil) + (and (consp (car S)) + (term-p (caar S)) (term-p (cdar S)) + (system-p (cdr S))))) + +;;; And we define the concept of system of terms in a given signature + +;;; ========= SYSTEM-P + +(defun system-s-p (S) + (if (atom S) + (equal S nil) + (and (consp (car S)) + (term-s-p (caar S)) (term-s-p (cdar S)) + (system-s-p (cdr S))))) + + +;;; The following lemmas are needed for guard verification: + +;;; REMARK: Note that the following lemmas state a result for terms and +;;; substitutions in given signature and there are also the same results +;;; for well-formed terms and substitutitions. Since well-formed terms +;;; are a particular case of terms of a signature (the signature that +;;; returns t for every eqlablep object and natural number), we could +;;; have proved the results for well-formed terms by functional +;;; instantiation of the corresponding results for signatures. But the +;;; results are so simple that they are proved anyway in a very easily +;;; without functional instantiation. + +(defthm system-p-implies-alistp + (implies (system-p S) (alistp S)) + :rule-classes :forward-chaining) + +(defthm system-p-append + (implies (and (system-p S1) (system-p S2)) + (system-p (append S1 S2)))) + +(defthm system-s-p-append + (implies (and (system-s-p S1) (system-s-p S2)) + (system-s-p (append S1 S2)))) + + +(defthm system-p-eliminate + (implies (system-p S) + (system-p (eliminate equ S)))) + +(defthm system-s-p-eliminate + (implies (system-s-p S) + (system-s-p (eliminate equ S)))) + +(defthm system-p-pair-args + (implies + (and (term-p-aux nil t1) + (term-p-aux nil t2)) + (system-p (first (pair-args t1 t2))))) + +(defthm system-s-p-pair-args + (implies + (and (term-s-p-aux nil t1) + (term-s-p-aux nil t2)) + (system-s-p (first (pair-args t1 t2))))) + + +(defthm system-p-term-p-aux-arguments + (implies (and (system-p S) + (member ecu S) + (not (variable-p (car ecu))) + (not (variable-p (cdr ecu)))) + (and (term-p-aux nil (cdar ecu)) + (term-p-aux nil (cddr ecu))))) + +(defthm system-s-p-term-p-aux-arguments + (implies (and (system-s-p S) + (member ecu S) + (not (variable-p (car ecu))) + (not (variable-p (cdr ecu)))) + (and (term-s-p-aux nil (cdar ecu)) + (term-s-p-aux nil (cddr ecu))))) + + +;;; ---------------------------------------------------------------------------- +;;; 3.2 Some related function definitions. +;;; ---------------------------------------------------------------------------- + + +;;; ===== DOMAIN and CO-DOMAIN +;;; already defined (see basic.lisp, section 4) + +;;; ===== SYSTEM-VAR +;;; Variables of the system: + +(defun system-var (S) + (if (endp S) + nil + (append (variables t (caar S)) + (append (variables t (cdar S)) + (system-var (cdr S)))))) + + +;;; ===== APPLY-SIST: +;;; Apply sigma to every term in system S. + +(defun apply-syst (sigma S) + (if (endp S) + nil + (cons (cons (apply-subst t sigma (caar S)) + (apply-subst t sigma (cdar S))) + (apply-syst sigma (cdr S))))) + +;;; REMARK: After applying apply-syst, every element of the system is +;;; listp. + + +;;; ====== APPLY-RANGE: +;;; Apply sigma only to the right-hand sides of equations in system S. + +(defun apply-range (sigma S) + (if (endp S) + nil + (cons (cons (caar S) (apply-subst t sigma (cdar S))) + (apply-range sigma (cdr S))))) + + +;;; ===== SUBSTITUTE-SYST: +;;; Apply sigma= '((x . t1)) to every term in system S. + +(defun substitute-syst (x t1 S) + (declare (xargs :guard (system-p S))) + (if (endp S) + nil + (cons (cons (substitute-var x t1 t (caar S)) + (substitute-var x t1 t (cdar S))) + (substitute-syst x t1 (cdr S))))) + + +;;; ===== SUBSTITUTE-RANGE: +;;; Apply sigma = '((x . t1)) to every term in system S. + +(defun substitute-range (x t1 S) + (declare (xargs :guard (system-p S))) + (if (endp S) + nil + (cons (cons (caar S) + (substitute-var x t1 t (cdar S))) + (substitute-range x t1 (cdr S))))) + + + +;;; ======= UNION-SYSTEMS + +(defun union-systems (S-T) (append (car S-T) (cdr S-T))) + + +;;; ======= NORMAL-FORM-SYST +;;; Pair of system in normal form + +(defun normal-form-syst (S-sol) + (declare (xargs :guard t)) + (not (and (consp S-sol) (consp (car S-sol))))) + + + +;;; ======= LENGTH-SYSTEM + +(defun length-system (S) + (if (endp S) + 0 + (+ (length-term t (caar S)) (length-term t (cdar S)) + (length-system (cdr S))))) + + + +;;; ======= MATCHER +;;; Matcher of a system of equations + +(defun matcher (sigma S) + (if (endp S) + t + (and (equal (apply-subst t sigma (caar S)) + (cdar S)) + (matcher sigma (cdr S))))) + + +;;; ====== SYSTEM-SUBSTITUTION +;;; The kind of substitutions that are matchers of themselves. + +(defun system-substitution (S) + (if (endp S) + t + (and + (consp (car S)) + (variable-p (caar S)) + (not (member (caar S) (domain (cdr S)))) + (system-substitution (cdr S))))) + + + +;;; ===== N-SYSTEM-VAR + +(defun n-system-var (S) + (len (make-set (system-var S)))) + + +;;; ====== SIZE-SYSTEM + + +(defun size-system (S) + (if (endp S) + 0 + (+ (size t (caar s)) + (size t (cdar s)) + (size-system (cdr s))))) + + +;;; ====== N-VARIABLES-RIGHT-HAND-SIDE + + + +(defun n-variables-right-hand-side (S) + (cond ((endp S) 0) + ((variable-p (cdar S)) (1+ (n-variables-right-hand-side (cdr S)))) + (t (n-variables-right-hand-side (cdr S))))) + + + + +;;; ======= UNIFICATION-MEASURE + +(defun unification-measure (S-sol) + (cons (cons (1+ (n-system-var (first S-sol))) + (size-system (first S-sol))) + (n-variables-right-hand-side (first S-sol)))) + + +;;; ---------------------------------------------------------------------------- +;;; 3.3 Solutions of systems. Idempotent substitutions. +;;; ---------------------------------------------------------------------------- + + + +;;; ==== SOLUTION +;;; Solution of system of equations. +;;; A substitution is a solution of a system if its a solution of every +;;; member of the system. A substitution sigma is a solution of an +;;; equation ecu if sigma(car(ecu)) = sigma (cdr (ecu)). Two systems are +;;; equivalent if they have the same set of solutions. + + +(defun solution (sigma S) + (if (endp S) + t + (and (equal (apply-subst t sigma (caar S)) + (apply-subst t sigma (cdar S))) + (solution sigma (cdr S))))) + + +;;; ===== IDEMPOTENT SYSTEMS/SUBSTITUTIONS + +;;; Some substitutions are solution +;;; of themselves. We then call that substitution idempotent. +;;; Its domain is a set of variables and the variables of its +;;; co-domain are disjoint with its domain. + +(defun idempotent (S) + (and (system-substitution S) + (disjointp (variables nil (co-domain S)) (domain S)))) + +;;; REMARK: In the literature, idempotent substitutions are defined as +;;; substitutions sigma such that sigma·sigma = sigma. But this +;;; definition involves functional equality. We will see that the above +;;; definition implies this property (see main-property-mgs in the book +;;; unification-definition.lisp) Nevertheless, the definition does not +;;; characterize the property. For example, the substitution represented +;;; by ((x . y) (x . z)) verify that property but is not idempotent in +;;; our sense. Fortunately, it can be proved that there exists a +;;; functionally equivalent idempotent (in our sense) substitution, ((x +;;; . y)) in this case. + +;;; ············································································ +;;; 3.3.1 The main property of idempotent substitutions. +;;; ············································································ + +;;; .... PROOF PLAN: + +; We want to prove idempotence-main-lemma (see below) +; idempotence-main-lemma fails in: + +; (IMPLIES (AND (SOLUTION S X) +; (SYSTEM-SUBSTITUTION S) +; (DISJOINT (VARIABLES F (CO-DOMAIN S)) (DOMAIN S)) +; (SETP (DOMAIN S)) +; (MEMBER (CONS V W) S) +; (SUBSETP X S)) +; (EQUAL (APPLY T S V) +; (APPLY T S W))). + + +; Strategy to prove this: + +; 1) (apply-subst t sigma v) is (val v sigma) if sigma is +; system-substitution and (v . w) is in sigma +; 2) (val v sigma) is w si (v . w) is in s and (domain s) is setp +; 3) (apply-subst t sigma w) is w if (domain s) is disjoint with +; variables of w (this has been proved before, in terms.lisp) +; 4) if (disjointp (variables nil (co-domain s)) l), and (v . w) is a +; member of s, the variables of w is disjoint with l. +;;; We compile these properties in the following encapsulate: + + +(local + (encapsulate + () + (local + (defthm system-substitution-properties + (implies (and (system-substitution sigma) + (member (cons v w) sigma)) + (and (variable-p v) (equal (val v sigma) w))))) + + (local + (defthm co-domain-disjoint-lemma + (implies (and (disjointp (variables nil (co-domain s)) l) + (member (cons v w) s)) + (disjointp (variables t w) l)) + :rule-classes nil + :hints (("Goal" :induct (len s))))) + + (local + (defthm co-domain-disjoint + (implies (and (disjointp (variables nil (co-domain s)) (domain s)) + (member (cons v w) s)) + (equal (apply-subst t s w) w)) + :hints (("Goal" :use + (:instance co-domain-disjoint-lemma + (l (domain s))) + :in-theory (enable substitution-does-not-change-term ))))) + + (defthm idempotence-main-lemma + (implies (and (idempotent S) + (subsetp sol S)) + (solution S sol))))) + +;;; And the main property of idempotent substitutions. + +(defthm idempotence + (implies (idempotent S) + (solution S S))) + + +;;; ============================================================================ +;;; 4. The tree structure of a term +;;; ============================================================================ + + +;;; ---------------------------------------------------------------------------- +;;; 4.1 Positions, occurrences and replacements. +;;; ---------------------------------------------------------------------------- + +;;; ============ POSITIONS OF A TERM + +(defun position-p (pos term) + (declare (xargs :guard (term-p term) + :verify-guards nil)) + (cond ((atom pos) (equal pos nil)) + ((variable-p term) nil) + (t + (and (integerp (car pos)) (< 0 (car pos)) + (<= (car pos) (len (cdr term))) + (position-p (cdr pos) + (nth (- (car pos) 1) (cdr term))))))) + + + +;;; ====== OCURRENCE IN A TERM AT A POSITION + +(defun occurrence (term pos) + (declare (xargs :guard + (and (term-p term) + (position-p pos term)) + :verify-guards nil)) + (if (endp pos) + term + (occurrence (nth (- (car pos) 1) (cdr term)) + (cdr pos)))) + + +;;; ====== REPLACING A OCCURRENCE IN A TERM FOR OTHER TERM + +(defun replace-term (term1 pos term2) + (declare (xargs :guard + (and (term-p term1) + (position-p pos term1)) + :verify-guards nil)) + (if (endp pos) + term2 + (cons (car term1) + (replace-list (cdr term1) + (- (car pos) 1) + (replace-term (nth (- (car pos) 1) (cdr term1)) + (cdr pos) + term2))))) + +;;; Guard verification + +(encapsulate + () + + (local + (defthm term-p-aux-true-listp + (implies (and (term-p-aux flg term) + (implies flg (not (variable-p term)))) + (true-listp term)))) + + (local + (defthm term-p-aux-true-listp + (implies (and (term-p-aux flg term) + (implies flg (not (variable-p term)))) + (true-listp term)))) + + + (local + (defthm term-p-aux-nth + (implies (term-p-aux nil term) + (term-p-aux t (nth i term))))) + + (verify-guards position-p) + (verify-guards occurrence) + (verify-guards replace-term)) + +;;; ---------------------------------------------------------------------------- +;;; 4.2 Some results concerning the tree structure of a term +;;; ---------------------------------------------------------------------------- + +;;; ············································································ +;;; 4.2.1 Concatenation of positions +;;; ············································································ + +(defthm position-p-append + (implies (position-p p1 term) + (iff (position-p (append p1 p2) term) + (position-p p2 (occurrence term p1))))) + + +(defthm occurrence-append + (implies (and (position-p p1 term) + (position-p p2 (occurrence term p1))) + (equal (occurrence term (append p1 p2)) + (occurrence (occurrence term p1) p2)))) + + +(defthm replace-term-append + (implies (position-p (append pos1 q) term) + (equal (replace-term term (append pos1 q) x) + (replace-term term pos1 + (replace-term (occurrence term pos1) + q x))))) + + +;;; ············································································ +;;; 4.2.2 Substitutions and positions +;;; ············································································ + +(defthm nth-apply-subst + (implies (and (integerp i) + (<= 0 i) + (< i (len l))) + (equal (nth i (apply-subst nil sigma l)) + (apply-subst t sigma (nth i l))))) + + +(defthm position-p-instance + (implies (position-p pos term) + (position-p pos (instance term sigma)))) + +(defthm occurrence-instance + (implies (position-p pos term) + (equal + (occurrence (instance term sigma) pos) + (instance (occurrence term pos) sigma)))) + +(local + (defthm replace-list-instance + (equal + (apply-subst nil sigma (replace-list l i x)) + (replace-list (apply-subst nil sigma l) i (apply-subst t sigma x))))) + + +(defthm replace-term-instance + (implies (position-p pos term) + (equal + (replace-term (instance term sigma) pos + (instance t1 sigma)) + (instance (replace-term term pos t1) sigma)))) + + +;;; ············································································ +;;; 4.2.3 Prefix positions +;;; ············································································ + +(local + (defthm equal-len-replace-list + (equal (len (replace-list l i x)) + (len l)))) + +(defthm position-p-prefix + (implies (position-p pos1 term1) + (iff (position-p (append pos1 pos2) + (replace-term term1 pos1 term2)) + (position-p pos2 term2)))) + +(defthm occurrence-prefix + (implies (and (position-p pos1 term1) + (position-p pos2 term2)) + (equal (occurrence + (replace-term term1 pos1 term2) + (append pos1 pos2)) + (occurrence term2 pos2)))) + +(defthm replace-term-prefix + (implies (and (position-p pos1 term1) + (position-p pos2 term2)) + (equal (replace-term + (replace-term + term1 pos1 term2) + (append pos1 pos2) + term3) + (replace-term + term1 pos1 + (replace-term term2 pos2 term3))))) + + + +;;; ············································································ +;;; 4.2.4 Disjoint positions +;;; ············································································ + +(local + (defun induct-position-p-disjoint (pos1 pos2 term) + (cond ((variable-p term) t) + ((and (consp pos1) (consp pos2)) + (if (equal (car pos1) (car pos2)) + (induct-position-p-disjoint + (cdr pos1) + (cdr pos2) + (nth (- (car pos1) 1) (cdr term))) + t)) + (t t)))) + +(local + (defthm equality-of-predecesor + (implies (and (integerp i) (integerp j)) + (iff (equal (+ -1 i) (+ -1 j)) + (equal i j))))) ;;; I don't like this rule. + +(defthm position-p-disjoint-positions + (implies (and (position-p pos1 term) + (position-p pos2 term) + (disjoint-positions pos1 pos2)) + (position-p pos1 (replace-term term pos2 x))) + :hints (("Goal" + :induct (induct-position-p-disjoint pos1 pos2 term) + :expand ((:free (term i pos x) + (replace-term term (cons i pos) x)) + (:free (i pos fn args) + (position-p (cons i pos) + (cons fn args))))))) + +(defthm occurrence-disjoint-positions + (implies (and (position-p pos1 term) + (position-p pos2 term) + (disjoint-positions pos1 pos2)) + (equal (occurrence (replace-term term pos1 x) pos2) + (occurrence term pos2))) + :hints (("Goal" + :induct (induct-position-p-disjoint + pos1 pos2 term) + :expand ((:free (term i pos x) + (replace-term term (cons i pos) x)) + (:free (i pos fn args) + (occurrence (cons fn args) + (cons i pos))))))) + + +(defthm replace-term-disjoint-positions + (implies (and + (position-p pos1 term) + (position-p pos2 term) + (disjoint-positions pos1 pos2)) + (equal (replace-term (replace-term term pos1 x) pos2 y) + (replace-term (replace-term term pos2 y) pos1 x))) + :hints (("Goal" :induct (induct-position-p-disjoint pos1 pos2 term) + :expand ((:free (term i pos x) + (replace-term term (cons i pos) x)) + (:free (i pos fn args) + (position-p (cons i pos) (cons fn args))))))) + + +;;; ············································································ +;;; 4.2.5 Disabling the theory +;;; ············································································ + +(defconst *tree-structure-of-terms* + '(position-p-append occurrence-append replace-term-append + position-p-instance occurrence-instance replace-term-instance + position-p-prefix occurrence-prefix replace-term-prefix + position-p-disjoint-positions occurrence-disjoint-positions + replace-term-disjoint-positions)) + +(in-theory + (set-difference-theories (current-theory :here) *tree-structure-of-terms*)) + +;;; ---------------------------------------------------------------------------- +;;; 4.3 Recursive versions of position-p, occurrence and replace-term +;;; ---------------------------------------------------------------------------- + +;;; The definition of position-p, occurrence and replace-term is done +;;; following the classical definition in the literature. Sometimes, +;;; this kind of definition does not provide a good induction scheme +;;; when proving properties relating this functions with other functions +;;; defined in a mutually recursive way, for terms and for lists of +;;; terms. For that reason we will give and alternative definition of +;;; position-p, occurrence and replace-term, in a mutually recursive +;;; style, and we prove that both definitions are equivalente for +;;; terms. + +;;; POSITION-P-REC + +(defun position-p-rec (flg pos term) + (declare (xargs :guard t)) + (if flg + (cond ((atom pos) (equal pos nil)) + ((variable-p term) nil) + (t (position-p-rec nil pos (cdr term)))) + (cond ((or (atom term) (atom pos)) nil) + ((eql 1 (car pos)) + (position-p-rec t (cdr pos) (car term))) + ((and (integerp (car pos)) (<= 2 (car pos))) + (position-p-rec nil (cons (- (car pos ) 1) (cdr pos)) (cdr + term))) + (t nil)))) + +;;; The two definitions are the same, as stated in the following +;;; rewrite rule + +(encapsulate + () + (defthm equal-position-p-position-p-rec-lemma + (if flg + (equal (position-p-rec flg pos term) + (position-p pos term)) + (equal (position-p-rec flg pos term) + (and (consp pos) (consp term) + (integerp (car pos)) (<= 1 (car pos)) + (<= (car pos) (len term)) + (position-p (cdr pos) (nth (- (car pos) 1) term))))) + :rule-classes nil) + + (defthm equal-position-p-position-p-rec + (equal (position-p pos term) + (position-p-rec t pos term)) + :hints (("Goal" :use (:instance + equal-position-p-position-p-rec-lemma + (flg t)))))) + + + + +;;; OCCURRENCE-REC + +(defun occurrence-rec (flg term pos) + (if flg + (cond ((endp pos) term) + ((variable-p term) nil) + (t (occurrence-rec nil (cdr term) pos))) + (cond ((or (endp term) (endp pos)) nil) + ((equal (car pos) 1) + (occurrence-rec t (car term) (cdr pos))) + ((and (integerp (car pos)) (<= 2 (car pos))) + (occurrence-rec nil (cdr term) (cons (- (car pos ) 1) (cdr pos)))) + (t nil)))) + +;;; The two definitions are the same, as stated in the following +;;; rewrite rule + +(encapsulate + () + (local + (defthm equal-occurrence-occurrence-rec-lemma + (implies (position-p-rec flg pos term) + (if flg + (equal (occurrence-rec flg term pos) + (occurrence term pos)) + (equal (occurrence-rec flg term pos) + (occurrence (nth (- (car pos) 1) term) (cdr pos))))) + :rule-classes nil)) + + + (defthm equal-occurrence-occurrence-rec + (implies (position-p-rec t pos term) + (equal (occurrence term pos) + (occurrence-rec t term pos))) + :hints (("Goal" :use (:instance + equal-occurrence-occurrence-rec-lemma (flg t)))))) + + + + + +;;; REPLACE-TERM-REC + +(defun replace-term-rec (flg term1 pos term2) + (if flg + (cond ((endp pos) term2) + ((variable-p term1) nil) + (t (cons (car term1) + (replace-term-rec nil (cdr term1) pos term2)))) + (cond ((or (endp term1) (endp pos)) nil) + ((equal (car pos) 1) + (cons (replace-term-rec t (car term1) (cdr pos) term2) + (cdr term1))) + ((and (integerp (car pos)) (<= 2 (car pos))) + (cons (car term1) + (replace-term-rec nil (cdr term1) + (cons (- (car pos ) 1) (cdr pos)) term2))) + (t nil)))) + + +(encapsulate + () + (local + (defthm equal-replace-term-replace-term-rec-lemma + (implies (position-p-rec flg pos term1) + (if flg + (equal (replace-term-rec flg term1 pos term2) + (replace-term term1 pos term2)) + (equal (replace-term-rec flg term1 pos term2) + (replace-list + term1 + (- (car pos) 1) + (replace-term (nth (- (car pos) 1) term1) + (cdr pos) term2))))) + :rule-classes nil)) + + + (defthm equal-replace-term-replace-term-rec + (implies (position-p-rec t pos term1) + (equal (replace-term term1 pos term2) + (replace-term-rec t term1 pos term2))) + :hints (("Goal" :use (:instance + equal-replace-term-replace-term-rec-lemma + (flg t)))))) + + + + +;;; ---------------------------------------------------------------------------- +;;; 4.2 Related closure theorems +;;; ---------------------------------------------------------------------------- + +;;; The following is a good example of how these "-aux" versions can +;;; help to prove properties. Recall that term-s-p and term-p are +;;; defined by mutual recursion (functions term-s-p-aux and +;;; term-p-aux). If we want to prove that occurrence and replace-term +;;; are closed in the set of terms of a given signature, then it is much +;;; easier to prove first the analogous theorems for occurrence-rec, and +;;; replace-term-rec (i.e. the theorem for terms and for lists of terms +;;; at the same time), and then to export those properties to the +;;; original definitions of position-p, occurrence and replace-term. + +;;; The "-aux" versions +(defthm occurrence-term-s-p-aux + (implies (and (term-s-p-aux flg term) + (position-p-rec flg pos term)) + (term-s-p (occurrence-rec flg term pos)))) + +(encapsulate + () + + (local + (defthm replace-term-rec-equal-len + (implies (position-p-rec nil pos term) + (equal (len (replace-term-rec nil term pos t1)) + (len term))))) + + (defthm replace-term-rec-term-s-p-aux + (implies (and (term-s-p-aux flg term) + (position-p-rec flg pos term) + (term-s-p t1)) + (term-s-p-aux flg (replace-term-rec flg term pos t1))))) + + + +;;; The intended theorems are now an easy consequence of the +;;; equivalence lemmas between the original definitions and its "-aux" +;;; versions + +(defthm occurrence-term-s-p + (implies (and (term-s-p term) + (position-p pos term)) + (term-s-p (occurrence term pos)))) + +(defthm replace-term-term-s-p + (implies (and (term-s-p term) + (position-p pos term) + (term-s-p t1)) + (term-s-p (replace-term term pos t1)))) + + +;;; Theorems needed for guard verification: + + +(defthm occurrence-term-p + (implies (and (term-p term) + (position-p pos term)) + (term-p (occurrence term pos))) + :hints (("Goal" :use (:functional-instance + occurrence-term-s-p + (signat (lambda (x n) (eqlablep x))) + (term-s-p-aux term-p-aux))))) + + + +(defthm replace-term-term-p + (implies (and (term-p term) + (position-p pos term) + (term-p t1)) + (term-p (replace-term term pos t1))) + :hints (("Goal" :use (:functional-instance + replace-term-term-s-p + (signat (lambda (x n) (eqlablep x))) + (term-s-p-aux term-p-aux))))) + + +;;; ---------------------------------------------------------------------------- +;;; 4.3 Another useful rules +;;; ---------------------------------------------------------------------------- + +;;; Here we list some additional rules which more easily proved using +;;; the "-aux" versions of position-p, occurrence and replace-term. + +(local + (defthm occurrence-position-p-rec-relation + (implies (position-p-rec flg pos term) + (iff (equal t1 (occurrence-rec flg term pos)) + (equal (replace-term-rec flg term pos t1) + term))))) + +(defthm occurrence-position-relation + (implies (position-p pos term) + (iff (equal t1 (occurrence term pos)) + (equal (replace-term term pos t1) + term)))) + +;;; REMARK: very useful rule!!! (take care with it) +(in-theory (disable occurrence-position-relation)) + + +;;; Now we disable the theorems of equivalence between the "-aux" +;;; versions and the original functions. We will enable locally when +;;; needed: + + + +(defconst *position-rec-versions* + '(equal-position-p-position-p-rec + equal-occurrence-occurrence-rec + equal-replace-term-replace-term-rec)) + +(in-theory + (set-difference-theories (current-theory :here) *position-rec-versions*)) + + + + + diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification-pattern.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification-pattern.lisp new file mode 100644 index 0000000..f0b3525 --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification-pattern.lisp @@ -0,0 +1,1597 @@ +;;; unification-pattern.lisp +;;; Definition and correctness of a rule-based unification algorithm +;;; with undefined selection function. This is a "pattern" for concrete +;;; unification algorithms. See unification.lisp +;;; Created 14-10-99. Last revision: 10-12-2000 +;;; ================================================================= + +#| To certify this book: + +(in-package "ACL2") + +(certify-book "unification-pattern") + +|# + +(in-package "ACL2") +(include-book "subsumption-subst") +(include-book "../../../../ordinals/e0-ordinal") +(set-well-founded-relation e0-ord-<) + +;;; ******************************************************************** +;;; DEFINITION AND VERIFICATION OF A RULE-BASED UNIFICATION ALGORITHM +;;; WE USE THIS BOOK TO PROVIDE A "PATTERN" FOR DEFINING A CONCRETE AND +;;; EXECUTABLE UNIFICATION ALGORITHM. +;;; ******************************************************************** + +;;; ============================================================================ +;;; 1. The transformation rules +;;; ============================================================================ + + +;;; ---------------------------------------------------------------------------- +;;; 1.1 Definition. +;;; ---------------------------------------------------------------------------- + + +;;; To formalize some kind of non-determinism, we partially define a +;;; selection function sel, assuming only the property that sel selects +;;; an element of every non-empty list. This function will be used to +;;; select an equation from the set unsolved equations. + + +(encapsulate + + ((sel (lst) t)) + + (local (defun sel (lst) (car lst))) + + (defthm sel-selects + (implies (consp l) (member (sel l) l)))) + +;;; The rules of transformation. This function is intended to act on a +;;; pair of systems, S-sol. The first one, S, has the equations to be +;;; solved, and the second one has the bindings done for the moment. An +;;; equation is selected from S, and according to this equation, a rule +;;; of transformation is applied. Note that for every particular +;;; instance of sel, we have a concrete unification algorithm. + +;;; We define here a function that applies one step of +;;; transformation. The rules of transformation are essentially the ones +;;; given by Martelli and Montanari. + +;;; There are seven rules of transformations, every rule named as in the +;;; comments. Note that the selected equation determines the rule to +;;; apply. If unsolvability is detected, nil is returned. + + +(defun transform-mm-sel (S-sol) + (let* ((S (first S-sol)) (sol (rest S-sol)) + (ecu (sel S)) + (t1 (car ecu)) (t2 (cdr ecu)) (R (eliminate ecu S))) + (cond ((equal t1 t2) (cons R sol)) ;;; *DELETE* + ((variable-p t1) + (if (member t1 (variables t t2)) + nil ;;; *CHECK* + (cons ;;; *ELIMINATE* + (apply-syst (list ecu) R) + (cons ecu (apply-range (list ecu) sol))))) + ((variable-p t2) + (cons (cons (cons t2 t1) R) sol)) ;;; *ORIENT* + ((not (equal (car t1) (car t2))) nil) ;;; *CONFLICT* + (t (mv-let (pair-args bool) + (pair-args (cdr t1) (cdr t2)) + (if bool + (cons (append pair-args R) sol) ;;; *DESCOMPOSE* + nil)))))) ;;; *NOT-PAIR* + + +;;; PROOF PLAN: + +;;; Prove that applying transformations repeatedly, beginning with (cons +;;; S nil), and stopping when the first system is empty (or +;;; unsolvability is detected), we obtain: +;;; 1) If S is solvable, a most general solution. +;;; 2) nil otherwise. + +;;; Iterative application of transform-mm will be defined by: +;(defun solve-system-sel (S-sol) +; (if (normal-form-syst S-sol) +; S-sol +; (solve-system-sel (transform-mm-sel S-sol)))) + + +;;; We will follow the satandard proof given in the literature. +;;; We have to prove that: +;;; - Transformations preserves the set of solutions. +;;; - Idempotence of the second system is preserved. +;;; - Every idempotent substitution is a most general solution of itself. +;;; - A normal form is always reached (giving a suitable ordinal +;;; measure for the admission of solve-system-sel) + +;;; For guard verification purposes, we will also prove that the +;;; properties system-p and substitution-p are preserved for the first +;;; and second system, respectively. + + +;;; ---------------------------------------------------------------------------- +;;; 1.2 How we deal with selection (first part) +;;; ---------------------------------------------------------------------------- + +;;; Since S and (cons x (eliminate x S)) are equal-set, and some of our +;;; predicates are congruences (in some of their arguments) w.r.t. the +;;; equal-set equivalence relation, let's take advantage of this. + +;;; The rewriting rule + +(local + (encapsulate + () + (local (defthm select-eliminate-and-cons-equal-set + (implies (member ecu S) + (and (subsetp S (cons ecu (eliminate ecu S))) + (subsetp (cons ecu (eliminate ecu S)) S))) + :hints (("Goal" :induct (eliminate ecu S))) + :rule-classes nil)) + + (defthm select-eliminate-and-cons-equal-set-instance + (let* ((S (first S-sol)) (ecu (sel S))) + (implies (and (consp S-sol) (consp S)) + (equal-set S (cons ecu (eliminate ecu S))))) + :hints (("Goal" :use + ((:instance select-eliminate-and-cons-equal-set + (S (first S-sol)) + (ecu (sel (first S-sol)))))))))) + +;;; REMARK: This is only a trick: if select-eliminate-and-cons-equal-set is +;;; used as a rewrite rule, it lead us to non-terminating rewritings. We +;;; will only use the rule when the system S is (car S-sol), so we only +;;; need the above (terminating) rewriting rule + + + +;;; The congruence respect solution +(local + (encapsulate + () + (local (defthm member-solution + (implies (and + (member ecu S) + (solution sigma S)) + (equal (instance (car ecu) sigma) + (instance (cdr ecu) sigma))))) + (local (defthm subsetp-solution + (implies (and (subsetp s1 s2) + (solution sigma s2)) + (solution sigma s1)))) + + (defcong equal-set iff (solution sigma s) 2))) + + +;;; The congruence with respect to system-var + +(local + (encapsulate + () + (local (defthm subsetp-variables-lemma-1 + (implies (member ecu s2) + (subsetp (variables t (car ecu)) + (system-var s2))))) + + (local (defthm subsetp-variables-lemma-2 + (implies (member ecu s2) + (subsetp (variables t (cdr ecu)) + (system-var s2))))) + + (local (defthm subsetp-system-var + (implies (subsetp S1 S2) + (subsetp (system-var S1) (system-var S2))))) + + (defcong equal-set equal-set (system-var s) 1))) + + +;;; ============================================================================ +;;; 2. Main properties of transform-mm-sel +;;; ============================================================================ + +;;; This is the main section of this book. We are going to prove some +;;; properties of transform-mm. Since transform-mm implements a set of +;;; transformation rules, we will need a set of lemmas for each property +;;; we want to prove and each rule of the transformation system. In the +;;; sequel, the name of the transformation rule will precede the +;;; corresponding set of lemmas. + + +;;; ---------------------------------------------------------------------------- +;;; 2.1 transform-mm-sel preserves the set of solutions of S-sol +;;; ---------------------------------------------------------------------------- + + +;;; One previous lemma: + +(local + (defthm solution-append + (equal (solution sigma (append S1 S2)) + (and (solution sigma S1) (solution sigma S2))))) + + +;;; Equivalence for each rule (some rules do not need auxiliary lemmas) +;;; ··································································· + + +;;; ···················· +;;; 2.1.1 rule DECOMPOSE +;;; ···················· +(local + (defun induction-transform-sel-decompose-rule (l1 l2) + (if (or (atom l1) (atom l2)) + t + (induction-transform-sel-decompose-rule (cdr l1) (cdr l2))))) + +(local + (defthm transform-sel-rule-decompose + (implies (second (pair-args l1 l2)) + (equal (solution sigma (first (pair-args l1 l2))) + (equal (apply-subst nil sigma l1) + (apply-subst nil sigma l2)))) + :hints (("Goal" :induct + (induction-transform-sel-decompose-rule l1 l2))))) + +;;; REMARK: The induction hint makes the proof shorter. + + + +;;; ····················· +;;; 2.1.2 rule ELIMINATE +;;; ····················· + +;;; If sigma is a solution of sol, and x is a variable, then +;;; sigma(sol(x)) = sol(x). + +(local + (encapsulate + () + (local + (defthm main-property-eliminate-lemma + (implies (and (solution sigma sol) (variable-p x) flg) + (equal + (apply-subst flg sigma (val x sol)) + (val x sigma))))) + +;;; If sigma is a solution of S, sigma = sigma · S + + (defthm substitutions-solution-system + (implies (solution sigma S) + (equal + (apply-subst flg sigma (apply-subst flg S term)) + (apply-subst flg sigma term)))))) + +;;; IMPORTANT REMARK: The above rule is key to prove the generality of +;;; the solution obatained. + +;;; Two corolaries: + +(local + (defthm main-property-eliminate + (implies (solution sigma sol) + (equal + (solution sigma (apply-syst sol S)) + (solution sigma S))))) + + +(local + (defthm main-property-eliminate-corolary + (implies (solution sigma sol) + (equal + (solution sigma (apply-range sol s)) + (solution sigma s))))) + + +;;; ················ +;;; 2.1.3 rule CHECK +;;; ················ + +;;; GOAL: +;;; Prove that x = term, when x is not in term and is not term, has no +;;; solution. + +;;; PROOF PLAN: +;;; We will see sigma(x) /= sigma (term), for every sigma. +;;; We need: +;;; * term is of the form (f t1...tn), and x is in some t_i. +;;; * sigma(x) is subterm of sigma(t_i) +;;; * sigma(t_i) is a son of sigma(term) +;;; * Every subterm has size less or equal than the term. +;;; * Every son has less size than the term. +;;; * so size(sigma(x)) < size (sigma(term)) (they are not equal). + +(local + (encapsulate + () + + (local + (defthm if-x-in-term-sigma-x-subterm-of-sigma-term + (implies (and (variable-p x) + (member x (variables flg term))) + (subterm flg (val x sigma) (apply-subst flg sigma term))))) + + (local + (defthm + if-x-is-not-term-and-is-in-term-then-is-in-some-argument + (implies (and (member x (variables t term)) + (not (equal x term))) + (member x (variables nil (cdr term)))))) + + (local + (defthm size-subterm + (implies (subterm flg t1 t2) + (>= (size flg t2) (size t t1))) + :rule-classes nil)) + + (local + (defthm + size-of-sigma-x-leq-than-the-size-of-sigma-of-arguments + (implies (and + (variable-p x) + (member x (variables t term)) + (not (equal x term))) + (>= (size nil (apply-subst nil sigma (cdr term))) + (size t (val x sigma)))) + :rule-classes nil + :hints (("Goal" :use + ((:instance size-subterm (flg nil) + (t1 (val x sigma)) + (t2 (apply-subst nil sigma (cdr term))))))))) + +;;; ===== Corolary: +;;; sigma(x) does not have the same size than sigma(term). + (defthm + transform-sel-check-rule-not-equal-size + (implies (and + (variable-p x) + (member x (variables t term)) + (not (equal x term))) + (not (equal (size t (val x sigma)) + (size t (apply-subst t sigma term))))) + :rule-classes nil + :hints (("Goal" + :use (:instance + size-of-sigma-x-leq-than-the-size-of-sigma-of-arguments)))))) + +;;; REMARK: It can be proved that is <, but it is not necessary + + +;;; And finally: +;;; x = term, if x is a variable in term and term is not variable, has +;;; no solution. + +(local + (defthm transform-sel-check-rule + (implies (and + (variable-p x) + (member x (variables t term)) + (not (equal x term))) + (not (equal (val x sigma) + (apply-subst t sigma term)))) + :hints (("Goal" + :use ((:instance + transform-sel-check-rule-not-equal-size)))))) + +;;; ··················· +;;; 2.1.4 rule CONFLICT +;;; ··················· + +;;; The equation (f t1 ... tn) = (g s1 ... sm), with f/=g has no +;;; solution: + +(local + (defthm transform-mm-sel-conflict-rule + (implies (and (not (variable-p t1)) + (not (variable-p t2)) + (not (equal (car t1) (car t2)))) + (not (equal (apply-subst t sigma t1) + (apply-subst t sigma t2)))))) + +;;; ···················· +;;; 2.1.5 rule NOT-PAIR +;;; ···················· + +;;; If sigma(t1...tn . a) = sigma(s1...sm . b), then n=m and a=b: +;;; ======= Corolary: The equation (f t1 ... tn . a) = (g s1 ... sm . b) +;;; has no solution when n/=m o' a/=b. + +(local + (encapsulate + () + (local + (defthm transform-sel-not-pair-rule-lemma + (implies (equal (apply-subst nil sigma l) + (apply-subst nil sigma m)) + (second (pair-args l m))))) + + (defthm transform-sel-not-pair-rule + (implies (and (not (variable-p t1)) + (not (variable-p t2)) + (not (second (pair-args (cdr t1) (cdr t2))))) + (not (equal (apply-subst t sigma t1) + (apply-subst t sigma t2))))))) + + +;;; ·················· +;;; 2.1.6 And finally: +;;; ·················· + +;;; Three lemmas to state that transform-mm-sel preserves the set of +;;; solutions: + + +(local + (defthm transform-mm-sel-equivalent-1 + (implies (and + (consp S-sol) + (consp (first S-sol)) + (solution sigma (union-systems S-sol))) + (solution sigma (union-systems (transform-mm-sel S-sol)))))) + + + +(local + (defthm transform-mm-sel-equivalent-2 + (implies (and + (consp S-sol) + (consp (first S-sol)) + (transform-mm-sel S-sol) + (solution sigma (union-systems (transform-mm-sel S-sol)))) + (solution sigma (union-systems S-sol))))) + + + +(local + (defthm transform-sel-unsolvable + (implies (and (not (transform-mm-sel S-sol)) + (consp S-sol) + (consp (first S-sol))) + (not (solution sigma (union-systems S-sol)))))) + + +;;; REMARK: although redundant, (consp S-sol) makes proofs shorter. + + +;;; ---------------------------------------------------------------------------- +;;; 2.2 transform-mm-sel preserves idempotence of the second system. +;;; ---------------------------------------------------------------------------- + +;;; Our goal: +; (defthm transform-mm-sel-preserves-idempotency +; (let ((transformed (transform-mm-sel (cons S sol)))) +; (let ((St (first transformed)) (solt (cdr transformed))) +; (implies (and +; (consp S) +; transformed +; (idempotent sol) +; (disjointp (system-var S) (domain sol))) +; (and (idempotent solt) +; (disjointp (system-var St) (domain +; solt))))))) +;;; INTERESTING REMARK: Note that we are proving that there are a number +;;; of INVARIANTS in any sequence of transformations: +;;; - Set of solutions. +;;; - Idempotence of the second system. +;;; - Every variable in the domain of the second system does not appear +;;; elsewher in the pair of system. +;;; This last two properties needs to be proved together. Note that +;;; idempotence needs two prove two properties: that we have a +;;; system-substitution and that the variables of the co-domain are not +;;; in the domain. See the definition of idempotence in terms.lisp + + +;;; A technical lemma: + +(local + (defthm system-var-append + (equal (system-var (append x y)) + (append (system-var x) (system-var y))))) + + +;;; As we said before, in the following, we have to prove this result +;;; for every transformation rule. Only two rules, DECOMPOSE and +;;; ELIMINATE needs help form the user + + +;;; ···················· +;;; 2.2.1 rule DECOMPOSE +;;; ···················· + +;;; Properties to prove that, for the rule decompose, the variables of +;;; the system S are disjoint from the domain of sol. + +(local + (encapsulate + () + (defthm pair-args-system-var-lemma-1 ;;it will be used later + (subsetp (system-var (first (pair-args l1 l2))) + (append (variables nil l1) (variables nil l2)))) + + (local (defthm pair-args-system-var-lemma-2 + (implies (second (pair-args l1 l2)) + (subsetp (append (variables nil l1) + (variables nil l2)) + (system-var (first (pair-args l1 l2))))) + :hints (("Goal" :induct + (induction-transform-sel-decompose-rule l1 l2) + :in-theory + (disable select-eliminate-and-cons-equal-set-instance))))) + + (defthm pair-args-system-var + (implies (second (pair-args l1 l2)) + (equal-set (system-var (first (pair-args l1 l2))) + (append (variables nil l1) + (variables nil l2))))))) + + +;;; ···················· +;;; 2.2.2 rule ELIMINATE +;;; ···················· + +;;; Properties to prove that, for the rule eliminate, the variables of +;;; the system S and the co-domain of sol are disjoint from the domain +;;; of sol. + + +(local + (defthm apply-range-preserves-domain + (equal (domain (apply-range sigma S)) (domain S)))) + +(local + (defthm co-domain-de-apply-range + (equal (co-domain (apply-range sigma s)) + (apply-subst nil sigma (co-domain s))))) + + +(local + (defthm apply-range-preserves-system-substitution + (implies (system-substitution S) + (system-substitution (apply-range sigma S))))) + + +(local + (defthm eliminate-variables-in-co-domain + (implies (not (member (car ecu) (variables t (cdr ecu)))) + (not (member (car ecu) + (variables flg (apply-subst flg (list ecu) s))))))) + +(local + (defthm variables-apply-subsetp-lemma + (implies (and (not (member x (variables flg term))) + (not (member x (variables nil (co-domain sigma))))) + (not (member x (variables flg (apply-subst flg sigma term))))))) + + +(local + (defthm variables-apply-subsetp + (subsetp (variables flg (apply-subst flg sigma term)) + (append (variables flg term) (variables nil (co-domain sigma)))) + :hints (("Goal" :in-theory (enable not-subsetp-witness-lemma))))) + +(local + (defthm subsetp-disjoint + (implies (and (subsetp a b) + (disjointp m b)) + (disjointp m a)) + :rule-classes nil)) + +(local + (defthm + domain-disjoint-co-domain-eliminate-bridge-lemma + (implies (disjointp m + (append (variables flg term) + (variables nil (co-domain sigma)))) + (disjointp m (variables flg (apply-subst flg sigma term)))) + :hints (("Goal" :use + ((:instance + subsetp-disjoint + (b (append (variables flg term) (variables nil (co-domain sigma)))) + (a (variables flg (apply-subst flg sigma term))))))))) + + +(local + (defthm eliminate-eliminate-variables + (implies (not (member (car ecu) (variables t (cdr ecu)))) + (not (member (car ecu) (system-var + (apply-syst (list ecu) s))))) + :hints (("Goal" :induct (len s))))) + + +(local + (defthm eliminate-eliminate-variables-2 + (implies (and (not (member x (variables nil (co-domain sigma)))) + (not (member x (system-var s)))) + (not (member x (system-var + (apply-syst sigma s))))))) + + +(local + (defthm subsetp-system-var-co-domain + (subsetp (system-var (apply-syst sigma s)) + (append (variables nil (co-domain sigma)) + (system-var s))) + :hints (("Goal" :in-theory + (enable not-subsetp-witness-lemma))))) + + +(local + (defthm + domain-disjoint-system-eliminate-bridge-lemma + (implies (disjointp m + (append (variables nil (co-domain sigma)) + (system-var S))) + (disjointp m + (system-var (apply-syst sigma S)))) + :hints (("Goal" + :use ((:instance + subsetp-disjoint + (b (append (variables nil (co-domain sigma)) (system-var S))) + (a (system-var (apply-syst sigma S))))))))) + + +;;; ···················· +;;; 2.2.3 And finally +;;; ···················· + +(local + (defthm transform-mm-sel-preserves-idempotency + (let* ((S (first S-sol)) (sol (rest S-sol)) + (transformado (transform-mm-sel S-sol)) + (St (first transformado)) (solt (cdr transformado))) + (implies (and + (consp S-sol) + (consp S) + transformado + (idempotent sol) + (disjointp (system-var S) (domain sol))) + (and (idempotent solt) + (disjointp (system-var St) (domain solt))))))) + +;;; We extracted all we wanted about idempotent. So we disable it. +(local (in-theory (disable idempotent))) + + +;;; ---------------------------------------------------------------------------- +;;; 2.3 transform-mm-sel preserves system-p and substitution-p +;;; ---------------------------------------------------------------------------- + +;;; This section is needed for guard verification. + +;;; ············································································ +;;; 2.3.1 preservation of the system-p property +;;; ············································································ + +(local + (encapsulate + () + +;;; Some previous lemmas for the result + + + (local + (defthm system-s-p-apply-syst + (implies (and (system-s-p S) + (substitution-s-p sigma)) + (system-s-p (apply-syst sigma S))))) + + (local + (defthm system-s-p-variable-s-p-cdr + (implies (and (system-s-p S) + (member equ S) + (variable-p (cdr equ))) + (eqlablep (cdr equ))))) + + + (local + (defthm substitution-s-p-member-system-s-p + (implies (and (system-s-p S) ;;; the order between the hypothesis is + ;;; important (free variables) + (member equ S) + (variable-p (car equ))) + (substitution-s-p (list equ))))) + + (local + (defthm term-s-p-member-system-s-p + (implies (and (system-s-p S) ;;; the order between the hypothesis is + ;;; important (free variables) + (member equ S)) + (term-s-p (car equ))))) + + + (local + (defthm system-s-p-term-p-bridge-lemma + (implies (and (system-s-p S) + (member ecu S) + (not (variable-p (car ecu))) + (not (variable-p (cdr ecu)))) + (and (term-s-p-aux nil (cdar ecu)) + (term-s-p-aux nil (cddr ecu)))))) + +;;; And the main result: + + (defthm transform-mm-sel-preserves-system-s-p + (implies (and + (consp S-sol) + (consp (first S-sol)) + (system-s-p (first S-sol))) + (system-s-p (first (transform-mm-sel S-sol)))) + :hints (("Goal" :in-theory (disable substitution-s-p)))))) + + +;;; ············································································ +;;; 2.3.2 preservation of the system-p property +;;; ············································································ + +(local + (encapsulate + () + +;;; Previous lemmas: + (local + (defthm system-s-p-eqlablep-car + (implies (and (system-s-p S) + (member equ S) + (variable-p (car equ))) + (eqlablep (car equ))))) + + + (local + (defthm substitution-s-p-apply-range + (implies (and (substitution-s-p sol) + (substitution-s-p sigma)) + (substitution-s-p (apply-range sigma sol))))) + + + (local + (defthm termp-s-p-member-system-s-p + (implies (and (system-s-p S) + (member equ S)) + (and + (term-s-p (cdr equ)))))) + +;;; And the main result: + + (defthm transform-mm-sel-preserves-substitution-s-p + (implies (and + (consp S-sol) + (consp (first S-sol)) + (system-s-p (first S-sol)) + (substitution-s-p (cdr S-sol))) + (substitution-s-p (cdr (transform-mm-sel S-sol))))))) + + + +;;; ---------------------------------------------------------------------------- +;;; 2.4 Termination properties of transform-mm-sel +;;; ---------------------------------------------------------------------------- + + +;;; Recall, we want define: +;(defun solve-system-sel (S-sol) +; (if (normal-form-syst S-sol) +; S-sol +; (solve-system-sel (transform-mm-sel S-sol)))) + + +;;; Proof plan for the admission of solve-system-sel: + +;;; We will define a measure unification-measure +;;; We will prove that unification-measure to prove that +;;; (unification-measure (transform-mm-sel S-sol)) is e0-ord-< than +;;; (unification-measure S-sol) + +;;; Unification-measure is a lexicographical +;;; combination of these three quantities (let S the first of S-sol): +;;; - Number of distinct variables of S. +;;; - Number of function symbols of S. +;;; - Number of equations of S with a variable as its righ-hand side. + +;;; See the definition of unification-measure in terms.lisp + + +;;; In this section, we will provide a number of lemmas needed to prove +;;; the following: + +;(defthm unification-measure-decreases +; (implies (not (normal-form-syst S-sol)) +; (e0-ord-< (unification-measure (transform-mm-sel S-sol)) +; (unification-measure S-sol)))) + +;;; Due to the definition of e0-ord-<, this lemma means the +;;; following. Let S be (car S-sol). +;;; 1) The number of distinct variables of S does not increase after one +;;; step of transformation. +;;; 2) If the number of distinct variables of the transformed system +;;; does not change, then size-system does not increase after one step of +;;; transformation. +;;; 3) If the above two quantities do not change, then +;;; n-variables-right-hand-side strictly decreases. + + + +;;; ············································································ +;;; 2.4.1 transform-mm-sel does not add new variables +;;; ············································································ + +;;; Goal: +;;; We will prove that the variables of S are a subset of +;;; the variables of the transformed, for every rule. + +;;; Some lemmas about eliminate +;;; ··························· + +(local + (defthm subsetp-variables-delete + (subsetp (system-var (eliminate ecu S)) + (system-var S)))) + +(local + (defthm subsetp-variables-eliminate-lemma + (implies (member ecu S) + (subsetp (append (system-var (list ecu)) + (system-var (eliminate ecu S))) + (system-var S))) + :rule-classes nil)) + + +(local + (defthm subsetp-variables-eliminate + (implies + (and (member ecu s) + (variable-p (car ecu))) + (subsetp (system-var + (apply-syst (list ecu) (eliminate ecu s))) + (system-var s))) + :hints (("Goal" + :in-theory (disable subsetp-system-var-co-domain) + :use ((:instance subsetp-variables-eliminate-lemma) + (:instance subsetp-system-var-co-domain + (sigma (list ecu)) + (S (eliminate ecu S)))))))) + +;;; Lemmas dealing with length, setps and subsetps +;;; ·············································· + +(local + (defthm len-subsetp-setp + (implies (and (setp l) (setp m) (subsetp l m)) + (<= (len l) (len m))) + :hints (("Goal" :induct (subset-induction l m))))) + +(local + (defthm subsetp-make-set + (implies (subsetp l m) + (subsetp (make-set l) (make-set m))))) + + +(local + (encapsulate + () + +;;; Main lemma (in terms of subsetp) +;;; ································ + + (local + (defthm transform-sel-does-not-add-new-variables + (let* ((S (first S-sol)) + (transformed (transform-mm-sel S-sol)) + (St (first transformed))) + (implies (and (consp S) (consp S-sol)) + (subsetp (system-var St) + (system-var S)))) + :hints (("Subgoal 5" + :use (:instance subsetp-variables-eliminate + (ecu (sel (car S-sol))) + (S (car S-sol))))))) + +;;; The main lemma (the previous lemma in terms of n-system-var) +;;; ···························································· + + (defthm + transform-does-not-increases-n-variables + (implies (not (normal-form-syst S-sol)) + (>= (n-system-var (first S-sol)) + (n-system-var (first (transform-mm-sel S-sol))))) + :rule-classes :linear + :hints (("Goal" :in-theory + (disable system-var transform-mm-sel)))))) + + +;;; ············································································ +;;; 2.4.2 The rule eliminate eliminates one variable from S +;;; ············································································ + +;;; This subsection is needed to show that when n-system-var does not +;;; change after one step of transformation, then the rule ELIMNATE has +;;; not been applied. + +;;; PROOF PLAN: +;;; The idea is to use length-subsetp-setp-strict (see below), where x +;;; is (car ecu)): + +(local + (encapsulate + () + + (local + (defthm positive-length-member + (implies (member x l) + (< 0 (len l))) + :rule-classes (:rewrite :linear))) + + (local + (defthm member-eliminate + (implies (and (member x l) + (not (equal x y))) + (member x (eliminate y l))))) + + (defthm len-subsetp-setp-strict + (implies (and + (setp l) + (setp m) + (subsetp l m) + (member x m) + (not (member x l))) + (< (len l) (len m))) + :hints (("Goal" :induct (subset-induction l m))) + :rule-classes nil))) + + +;;; A technical lemma: + +(local + (defthm subsetp-variables-orient-2 + (implies (and (member ecu S) (variable-p (car ecu))) + (member (car ecu) (system-var S))))) + +;;; REMARK: The previous lemma is trivial, but is needed because we +;;; disable system-var in the following lemma. + +;;; And the main lemma: + +(local + (defthm eliminate-variables-strict + (implies + (and + (member ecu S) + (variable-p (car ecu)) + (not (member (car ecu) (variables t (cdr ecu))))) + (> (n-system-var S) + (n-system-var (apply-syst (list ecu) + (eliminate ecu S))))) + :rule-classes :linear + :hints (("Goal" :use + ((:instance len-subsetp-setp-strict + (l (make-set + (system-var (apply-syst (list ecu) + (eliminate ecu S))))) + (m (make-set (system-var S))) + (x (car ecu)))) + :in-theory (disable system-var))))) + +;;; REMARK: In this lemma, the (first S-sol) version is more +;;; complicated. + + +;;; ············································································ +;;; 2.4.3 How we deal with selection (second part). +;;; ············································································ + +;;; equal-set is not a congruence w.r.t. size-system and +;;; n-variables-right-hand-side. See observaciones.txt to understand why +;;; a congruence based approach does not work We define the following +;;; rewrite rules to rewrite (size-system (first S-sol)) y +;;; (n-variables-right-hand-side S-sol) + +(local + (defthm size-system-cons-select-and-delete-one-lemma + (implies (member ecu S) + (equal (size-system S) + (size-system (cons ecu (delete-one ecu S))))) + :rule-classes nil)) + +(local + (defthm size-system-cons-select-and-delete-one + (implies (consp (first S-sol)) + (equal (size-system (first S-sol)) + (size-system (cons (sel (first S-sol)) + (delete-one (sel (first S-sol)) + (first S-sol)))))) + :hints (("Goal" + :use ((:instance size-system-cons-select-and-delete-one-lemma + (S (first S-sol)) + (ecu (sel (first S-sol))))))))) + + + +(local + (defthm n-variables-rhs-cons-select-and-delete-one-lemma + (implies (member ecu S) + (equal (n-variables-right-hand-side S) + (if (variable-p (cdr ecu)) + (1+ (n-variables-right-hand-side + (delete-one ecu S))) + (n-variables-right-hand-side (delete-one ecu S))))) + :rule-classes nil)) + +(local + (defthm n-variables-rhs-cons-select-and-delete-one + (let ((S (first S-sol)) (ecu (sel (first S-sol)))) + (implies (consp S) + (equal (n-variables-right-hand-side S) + (if (variable-p (cdr ecu)) + (1+ (n-variables-right-hand-side + (delete-one ecu S))) + (n-variables-right-hand-side (delete-one ecu + S)))))) + :hints (("Goal" :use + (:instance + n-variables-rhs-cons-select-and-delete-one-lemma + (ecu (sel (first S-sol))) + (S (first S-sol))))))) + + +;;; Note that our transformation select and ELIMINATE (which removes all +;;; occurrences, not only the first on, as delete-one does): The +;;; following linear arithmetic rules relates eliminate and delete-one: + +(local + (defthm size-system-eliminate-delete-one-lemma + (<= (size-system (delete-one x S)) + (size-system S)) + :rule-classes :linear)) + + +(local + (defthm size-system-eliminate-delete-one + (>= (size-system (delete-one x S)) + (size-system (eliminate x S))) + :rule-classes :linear)) + + +(local + (defthm n-variables-right-hand-side-eliminate-delete-one-lemma + (<= (n-variables-right-hand-side (delete-one x S)) + (n-variables-right-hand-side S)) + :rule-classes :linear)) + + +(local + (defthm n-variables-right-hand-side-eliminate-delete-one + (>= (n-variables-right-hand-side (delete-one x S)) + (n-variables-right-hand-side (eliminate x S))) + :rule-classes :linear)) + + + +;;; ············································································ +;;; 2.4.4 Size-system does not increase (when n-variables remains the same) +;;; ············································································ + +;;; Technical lemma: + +(local + (defthm size-system-append + (equal (size-system (append x y)) + (+ (size-system x) (size-system y))))) + + +;;; Needed for the DECOMPOSE rule: + +(local + (defthm size-systems-decompose-lemma + (implies (second (pair-args l1 l2)) + (equal (size-system (first (pair-args l1 l2))) + (+ (size nil l1) (size nil l2)))))) + + +;;; And the main lemma: + +(local + (defthm + si-permanece-system-var-al-transformar-decrece-size-system + (implies (and + (not (normal-form-syst S-sol)) + (equal (n-system-var (first S-sol)) + (n-system-var (first (transform-mm-sel S-sol))))) + (>= (size-system (first S-sol)) + (size-system (first (transform-mm-sel S-sol))))) + :rule-classes :linear + :hints (("Goal" :in-theory + (disable n-system-var))))) + +(local (in-theory (disable size-system-cons-select-and-delete-one))) + + + +;;; ············································································ +;;; 2.4.5 n-variables-right-hand-side does not increase (when the two above +;;; quantities remain the same) +;;; ············································································ + +;;; Lemmas: + +(local + (encapsulate + () + (local + (defthm size-system-equation-lemma + (implies (member ecu S) + (equal (size-system S) + (+ (size t (car ecu)) + (size t (cdr ecu)) + (size-system (delete-one ecu S))))) + :rule-classes nil)) + + (defthm size-system-equation + (let ((S (first S-sol)) (ecu (sel (first S-sol)))) + (implies (consp S) + (equal (size-system S) + (+ (size t (car ecu)) + (size t (cdr ecu)) + (size-system (delete-one ecu S)))))) + :hints (("Goal" :use + (:instance + size-system-equation-lemma + (S (first S-sol)) + (ecu (sel (first S-sol))))))))) + +;;; REMARK: the form of this rule to avoid non-termination. + + +(local + (defthm size-t->-0 + (implies (not (variable-p term)) (< 0 (size t term))) + :rule-classes :linear)) + +(local + (defthm n-variables-right-hand-side-orient + (implies + (and + (member ecu S) + (variable-p (cdr ecu)) + (not (variable-p (car ecu)))) + (< (n-variables-right-hand-side (eliminate ecu S)) + (n-variables-right-hand-side S))))) + + +(local + (defthm n-variables-right-hand-side-check-lemma + (implies (and (member ecu S) (variable-p (car ecu))) + (consp (system-var S))) + :rule-classes nil)) + +(local + (defthm n-variables-right-hand-side-check + (implies (and (consp S) (variable-p (car (sel S)))) + (consp (system-var S))) + :hints (("Goal" + :use ((:instance + n-variables-right-hand-side-check-lemma + (ecu (sel S)))))))) + + +;;; And the main lemma: + +(local + (defthm + if-n-variables-and-size-are-equal-transform-mm-sel-decrease-n-variables-r-h-s + (implies (and + (not (normal-form-syst S-sol)) + (equal (n-system-var (first S-sol)) + (n-system-var (first (transform-mm-sel S-sol)))) + (equal (size-system (first S-sol)) + (size-system (first (transform-mm-sel S-sol))))) + (< (n-variables-right-hand-side + (first (transform-mm-sel S-sol))) + (n-variables-right-hand-side (first S-sol)))) + :otf-flg t + :rule-classes :linear + :hints (("Goal" :in-theory + (disable n-system-var size-system))))) + + +(local (in-theory (disable n-variables-rhs-cons-select-and-delete-one))) + +;;; ············································································ +;;; 2.4.6 Compiling the previous results: the main termination property +;;; ············································································ + +;;; We disable some definition and lemmas + + +(local (in-theory (disable n-system-var + size-system + n-variables-right-hand-side))) +(local (in-theory + (disable size-system-equation))) + +;;; We disable transform-mm-sel +;;; This will allow previous lemmas about transform-sel be used. + +(in-theory (disable transform-mm-sel)) + + +;;; AND THE MAIN TERMINATION THEOREMS +;;; ································· + +(defthm ordinalp-unification-measure + (e0-ordinalp (unification-measure S-sol))) + + +(defthm unification-measure-decreases + (implies (not (normal-form-syst S-sol)) + (e0-ord-< (unification-measure (transform-mm-sel S-sol)) + (unification-measure S-sol)))) + +;;; We disable unification-measure (we already know all we needed) + +(local (in-theory (disable unification-measure))) + + + + + + +;;; ============================================================================ +;;; 3. solve-system-sel: applying transform-sel until a normal form is reached +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 3.1 Definition. +;;; ---------------------------------------------------------------------------- + + +;;; IMPORTANT REMARK: +;;; The following functions are partially defined because the selection +;;; function sel is partially defined. Concrete instantiations of this +;;; algorithm can be defined and their properties can be easily obtained +;;; by functional instantiations. See unification-one-definition.lisp +;;; for a concrete unification algorithm + +;;; ======= SOLVE-SYSTEM-SEL + +(defun solve-system-sel (S-sol) + (declare (xargs :measure (unification-measure S-sol))) + (if (normal-form-syst S-sol) + S-sol + (solve-system-sel (transform-mm-sel S-sol)))) + +;;; ---------------------------------------------------------------------------- +;;; 3.2 Properties of solve-system-sel +;;; ---------------------------------------------------------------------------- + + +;;; ·········································· +;;; 3.2.1 solve-system-sel preserves solutions +;;; ·········································· + +;;; A technical lemma + +(local + (defthm if-solvable-transform-sel-success + (implies (solve-system-sel (transform-mm-sel S-sol)) + (transform-mm-sel S-sol)))) + + +;;; This is for the three following lemmas: +(local (in-theory (disable union-systems))) + +;;; The main three lemmas to state that the set of solutions is preserved +;;; by sove-sel. + +(local + (defthm + solve-system-sel-equivalent-1 + (implies (and (solution sigma (union-systems S-sol)) + (consp S-sol)) + (solution sigma (union-systems (solve-system-sel S-sol)))) + :rule-classes nil)) + +(local + (defthm solve-system-sel-equivalent-2 + (implies (and (solve-system-sel S-sol) + (solution sigma (union-systems (solve-system-sel S-sol))) + (consp S-sol)) + (solution sigma (union-systems S-sol))) + :rule-classes nil)) + +(local + (defthm solve-system-sel-unsolvable + (implies (and (not (solve-system-sel S-sol)) + (consp S-sol)) + (not (solution sigma (union-systems S-sol)))) + :rule-classes nil)) + +;;; REMARK: we don't need (consp S-sol), but the proof is shorter. + +(local (in-theory (enable union-systems))) + + +;;; ············································· +;;; 3.2.2 solve-system-sel preserves idempotence +;;; ············································· + + +(local (in-theory (disable disjointp-conmutative))) + + +(local + (defthm + solve-system-sel-preserves-idempotency + (let* ((S (first S-sol)) (sol (cdr S-sol)) + (solve-system-sel (solve-system-sel S-sol)) + (solucion (cdr solve-system-sel))) + (implies (and + (consp S-sol) + solve-system-sel + (idempotent sol) + (disjointp (system-var S) (domain sol))) + (idempotent solucion))) + :hints (("Goal" :induct (solve-system-sel S-sol))))) + + +;;; ···························································· +;;; 3.2.3 solve-system-sel preserves system-p and substitution-p +;;; ···························································· + +;;; Closure property + +(local + (defthm + solve-system-sel-substitution-s-p + (let* ((S (first S-sol)) (sol (cdr S-sol)) + (solve-system-sel (solve-system-sel S-sol)) + (solucion (cdr solve-system-sel))) + (implies (and + (consp S-sol) + solve-system-sel + (system-s-p S) (substitution-s-p sol)) + (substitution-s-p solucion))) + :hints (("Goal" :induct (solve-system-sel S-sol))))) + + + +;;; ============================================================================ +;;; 4. mgs-sel: An algorithm for finding the most general solution of S +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 4.1 Definition. +;;; ---------------------------------------------------------------------------- + +;;; We simply call solve-system-sel with the input (cons S nil) + +;;; ========= MGS-SEL + +(defun mgs-sel (S) + (let ((solve-system-sel (solve-system-sel (cons S nil)))) + (if solve-system-sel (list (cdr solve-system-sel)) nil))) + +;;; REMARK: In order to distinguish the empty substitution nil, from nil +;;; as fail, "pack" the result in a list. + +;;; ---------------------------------------------------------------------------- +;;; 4.2 Main properties of mgs-sel +;;; ---------------------------------------------------------------------------- + +;;; ······························································ +;;; THEOREM 4.2.1. If S is solvable, then (mgs-sel S) succeeds. +;;; ······························································ + +(defthm mgs-sel-completeness + (implies (solution sigma S) + (mgs-sel S)) + :rule-classes nil + :hints + (("Goal" :use + ((:instance solve-system-sel-unsolvable (S-sol (cons S nil))))))) + +;;; ======= One technical lemmas: + +(local + (defthm + in-normal-forms-S-is-solvable-by-any-sigma + (solution sigma (first (solve-system-sel S-sol))))) + + +;;; ······································································· +;;; THEOREM 4.2.2: If (mgs-sel S) succeeds, then the system is solvable +;;; (and a solution is (first (mgs-sel S)) +;;; ······································································· + +(local + (defthm mgs-sel-soundness + (implies (mgs-sel S) + (solution (first (mgs-sel S)) S)) + :rule-classes nil + :hints (("Goal" :use + ((:instance solve-system-sel-equivalent-2 + (S-sol (cons S nil)) + (sigma (first (mgs-sel S))))))))) + +;;; ···················································· +;;; THEOREM 4.2.3: (first (mgs-sel S)) is idempotent. +;;; ····················································· + + +(local + (defthm mgs-sel-idempotent + (idempotent (first (mgs-sel S))))) + + +;;; REMARK: This is true even if (mgs-sel S) fails + + +;;; ··························································· +;;; THEOREM 4.2.4: The substitution returned by mgs-sel is +;;; substitution-p, whenever its input system is system-p +;;; ···························································· + +;;; This theorem is needed for guard verification. + + +(local + (defthm substituion-s-p-mgs-sel + (implies (system-s-p S) + (substitution-s-p (first (mgs-sel S)))) + :hints (("Goal" :use + (:instance + solve-system-sel-substitution-s-p + (S-sol (cons S nil))))))) + + + + + +;;; ·································································· +;;; THEOREM 4.2.5: If sigma is a solution of S, (first (mgs-sel S)) +;;; subsumes sigma. (thus, (first (mgs-sel S)) is a mgs of S) +;;; ··································································· + +;;; Lemma: If sigma is a solution of S, then for all term, (first +;;; (mgs-sel S))(term) subsumes sigma(term), with the matching +;;; substitution, sigma, for all terms. + + +(local + (defthm mgs-sel-most-general-solution-main-lemma + (implies (solution sigma S) + (equal (instance (instance term (first (mgs-sel S))) + sigma) + (instance term sigma))) + :hints (("Goal" :use + (:instance + solve-system-sel-equivalent-1 (S-sol (cons S nil))))))) + +;;; We disable mgs-sel + +(in-theory (disable mgs-sel)) + +(local + (defthm mgs-sel-most-general-solution + (implies (solution sigma S) + (subs-subst (first (mgs-sel S)) sigma)) + :hints (("Goal" + :use + ((:functional-instance + subs-subst-completeness + (sigma-w (lambda () + (if (solution sigma S) (first (mgs-sel S)) nil))) + (gamma-w (lambda () + (if (solution sigma S) sigma nil))) + (delta-w (lambda () + (if (solution sigma S) sigma nil))))))))) + + +;;; REMARK: note the interesting use of functional instantiation here, +;;; where the functional substitutions assigns to sigma-w, gamma-w and +;;; delta-w, lambda expressions with free variables in their +;;; bodies. This trick is used several times in the ACL2 books. + + +;;; ============================================================================ +;;; 5. mgu-sel: Unification of two terms +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 5.1 Definitions. +;;; ---------------------------------------------------------------------------- + +;;; ======= UNIFIABLE-SEL +;;; This is only a particular case of solve-sel. We solve the sistem +;;; (list (cons t1 t2)) + +(defun unifiable-sel (t1 t2) + (mgs-sel (list (cons t1 t2)))) + +;;; We can also define the property the computed unifier: +(defun mgu-sel (t1 t2) + (first (unifiable-sel t1 t2))) + +;;; ---------------------------------------------------------------------------- +;;; 5.2 Main properties mgu-sel and unifiable-sel. +;;; ---------------------------------------------------------------------------- + +;;; Inmediate consequences of the properties of mgs-sel: note that two +;;; terms t1 and t2 are unifiable iff the system (list (cons t1 t2)) is +;;; solvable (and an unifier of t1 and t2 is a solution of (list (cons +;;; t1 t2))) + + +;;; ······································································ +;;; THEOREM 5.2.1: If t1 and t2 are unifiable, then (unifiable-sel t1 t2). +;;; ······································································ + +(defthm unifiable-sel-completeness + (implies (equal (instance t1 sigma) + (instance t2 sigma)) + (unifiable-sel t1 t2)) + :rule-classes nil + :hints (("Goal" :use + (:instance mgs-sel-completeness + (S (list (cons t1 t2))))))) + + +;;; ········································································ +;;; THEOREM 5.2.2: If (unifiable-sel t1 t2), t1 and t2 are unifiable +;;; (and (mgu-sel t1 t2) is an unifier). +;;; ········································································ + + +(defthm unifiable-sel-soundness + (implies (unifiable-sel t1 t2) + (equal (instance t1 (mgu-sel t1 t2)) + (instance t2 (mgu-sel t1 t2)))) + :hints (("Goal" :use + ((:instance mgs-sel-soundness + (S (list (cons t1 t2)))))))) + + +;;; ········································································ +;;; THEOREM 5.2.3: (mgu-sel t1 t2) is idempotent. +;;; ········································································ + +(defthm mgu-sel-idempotent + (idempotent (mgu-sel t1 t2))) + +;;; ········································································ +;;; THEOREM 5.2.4: If t1 and t2 are terms of a given signature, then mgu-sel +;;; returns a substitution of that signature +;;; ········································································ + + + +(defthm mgu-sel-substitution-s-p + (implies (and (term-s-p t1) (term-s-p t2)) + (substitution-s-p (mgu-sel t1 t2)))) + + + +;;; ········································································ +;;; THEOREM 5.2.5: If sigma is an unifier of t1 and t2, then (mgu-sel t1 t2) +;;; subsumes sigma (thus, (mgu-sel t1 t2) is a mgu of t1 and t2). +;;; ········································································ + +(defthm mgu-sel-most-general-unifier + (implies (equal (instance t1 sigma) + (instance t2 sigma)) + (subs-subst (mgu-sel t1 t2) sigma))) + + +;;; We disable mgu-sel + +(in-theory (disable mgu-sel)) + + + + + + + + diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification.lisp new file mode 100644 index 0000000..aa724aa --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification.lisp @@ -0,0 +1,515 @@ +;;; unification.lisp +;;; Definition of a particular rule-based unification algorithm. +;;; This is an executable instance of the general pattern verified in +;;; unification-pattern.lisp +;;; Created 17-10-99. Last revision: 10-12-2000 +;;; ================================================================= + +#| To certify this book: + +(in-package "ACL2") + +(certify-book "unification") + +|# + + + + + +(in-package "ACL2") +(include-book "subsumption-subst") +(local (include-book "unification-pattern")) +(set-well-founded-relation e0-ord-<) + + +;;; ************************************************* +;;; A CONCRETE AND EXECUTABLE UNIFICATION ALGORITHM +;;; ************************************************* + +;;; Here we show how we can obtain a correct and executable unification +;;; algorithm from the "pattern" verified in unification-definition.lisp: +;;; - We define a particular selection function. +;;; - We introduce multi-values to deal with the pair of systems +;;; S-sol and with the returned values, to improve efficiency. +;;; - Some other improvements concerning efficency are done. +;;; - Guards are verified, allowing execution in Common Lisp. + +;;; ============================================================================ +;;; 1. The unification algorithm +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 1.1 A particular version of transform-mm-sel +;;; ---------------------------------------------------------------------------- + +;;; ············································································ +;;; 1.1.1 A particular "selection" function. If we detect an inmediate fail, +;;; we select it. +;;; ············································································ + +(defun sel-unif (S) + (declare (xargs :guard (and (consp S) (system-p S)))) + (if (endp (cdr S)) + (car S) + (let* ((equ (car S)) + (t1 (car equ)) + (t2 (cdr equ))) + (cond ((or (variable-p t1) (variable-p t2)) + (sel-unif (cdr S))) + ((eql (car t1) (car t2)) + (sel-unif (cdr S))) + (t equ))))) + +;;; Main property, needed to instantiate from unification-definition.lisp: +(local + (defthm sel-unif-select-a-pair + (implies (consp S) + (member (sel-unif S) S)))) + + + +;;; ············································································ +;;; 1.1.2 Some lemmas needed for guard verification: +;;; ············································································ + +(encapsulate + () + + (local + (defthm sel-unif-consp + (implies (and (alistp S) + (consp S) + (system-p S)) + (consp (sel-unif S))) + :rule-classes :type-prescription)) + + (defthm termp-p-sel-unif-system-p + (implies (and (consp S) + (system-p S)) + (and + (term-p (car (sel-unif S))) + (term-p (cdr (sel-unif S)))))) + + (local + (defthm term-p-true-listp-arguments + (implies (and (term-p term) (not (variable-p term))) + (true-listp (cdr term))))) + + (local + (defthm system-p-eqlable-function-symbols + (implies (and (system-p S) + (member equ S)) + (eqlablep (cadr equ))))) + + (defthm system-p-eqlablep-car + (implies (and (system-p S) + (consp S) + (variable-p (car (sel-unif S)))) + (eqlablep (car (sel-unif S))))) + +;;; ············································································ +;;; 1.1.3 The function transform-mm +;;; ············································································ + + + (defun transform-mm (S sol) + (declare (xargs :guard (and (system-p S) + (system-p sol) + (consp S)))) + (let* ((ecu (sel-unif S)) + (t1 (car ecu)) (t2 (cdr ecu)) + (R (eliminate ecu S))) + (cond ((equal t1 t2) (mv R sol t)) ;;; *DELETE* + ((variable-p t1) + (if (member t1 (variables t t2)) + (mv nil nil nil) ;;; *CHECK* + (mv ;;; *ELIMINATE* + (substitute-syst t1 t2 R) + (cons ecu + (substitute-range t1 t2 sol)) + t))) + ((variable-p t2) + (mv (cons (cons t2 t1) R) sol t)) ;;; *ORIENT* + ((not (eql (car t1) (car t2))) + (mv nil nil nil)) ;;; *CONFLICT* + (t (mv-let (pairs bool) + (pair-args (cdr t1) (cdr t2)) + (if bool + (mv (append pairs R) sol t) ;;; *DESCOMPOSE* + (mv nil nil nil)))))))) ;;; *NOT-PAIR* + + + +;;; ---------------------------------------------------------------------------- +;;; 1.2 Some lemmas needed for functional instantiation (first part) +;;; ---------------------------------------------------------------------------- + +;;; Here we define some lemmas to show that the efficiency improvements +;;; done in transform-mm does not affect the logic: + +(local + (defthm substitute-var-apply-subst + (equal (apply-subst flg (list equ) term) + (substitute-var (car equ) (cdr equ) flg term)))) + + +(local + (defthm substitute-syst-apply-syst + (equal (apply-syst (list equ) S) + (substitute-syst (car equ) (cdr equ) S)))) + +(local + (defthm substitute-range-apply-range + (equal (apply-range (list equ) S) + (substitute-range (car equ) (cdr equ) S)))) + + +;;; transform-mm-sel of unification-definition.lisp cannot be +;;; instantiated by transform-mm, since they different signatures, due +;;; to the use of multi values in transform-mm. Instead, we will +;;; instantiate transform-mm-sel for the following function: + +(local + (defun transform-mm-bridge (S-sol) + (mv-let (S1 sol1 bool1) + (transform-mm (car S-sol) (cdr S-sol)) + (if bool1 (cons S1 sol1) nil)))) + + +;;; ---------------------------------------------------------------------------- +;;; 1.3 Termination properties of transform-mm +;;; ---------------------------------------------------------------------------- + +;;; The theorem to justify the definition. This lemma is easily obtained +;;; by functional instantiation: + +(local + (encapsulate + () +;;; A technical lemma, to make the proof shorter: + (local + (defthm um-technical + (equal (unification-measure '(nil)) + (unification-measure nil)))) + + (defthm unification-measure-decreases-instance + (let ((transform-mm (transform-mm S sol))) + (implies (consp S) + (e0-ord-< + (unification-measure (cons (first transform-mm) + (second transform-mm))) + (unification-measure (cons S sol))))) + :hints (("Goal" :use (:functional-instance + (:instance unification-measure-decreases + (S-sol (cons S sol))) + (transform-mm-sel transform-mm-bridge) + (sel sel-unif))) + ("Subgoal 3" :in-theory (disable unification-measure + (unification-measure))))))) + + + +(local (in-theory (disable unification-measure))) + + + +;;; ---------------------------------------------------------------------------- +;;; 1.4 Guard verification +;;; ---------------------------------------------------------------------------- + +;;; Some lemmas needed for guard verification of mgu-mv + +(local + (defthm system-p-substitute-var + (implies (and (term-p t1) + (term-p-aux flg term)) + (term-p-aux flg (substitute-var x t1 flg term))))) + +(local + (defthm system-p-substitute-syst + (implies (and (system-p S) + (term-p term)) + (system-p (substitute-syst x term S))))) + +(local + (defthm system-p-substitute-range + (implies (and (system-p S) + (term-p term)) + (system-p (substitute-range x term S))))) + + +;;; ---------------------------------------------------------------------------- +;;; 1.5 The unification algorithm +;;; ---------------------------------------------------------------------------- + +;;; Appling transform-mm until a normal form is found: + +(defun solve-system (S sol bool) + (declare + (xargs + :guard (and (system-p S) + (system-p sol)) + :measure (unification-measure (cons S sol)) + :hints + (("Goal" :in-theory (disable transform-mm))))) + (if (or (not bool) (not (consp S))) + (mv S sol bool) + (mv-let (S1 sol1 bool1) + (transform-mm S sol) + (solve-system S1 sol1 bool1)))) + + + +;;; Most general solutions of systems of equations + +(defun mgs-mv (S) + (declare (xargs :guard (system-p S))) + (mv-let (S1 sol1 bool1) + (solve-system S nil t) + (declare (ignore S1)) + (mv sol1 bool1))) + +;;; The unification algorithm + +(defun mgu-mv (t1 t2) + (declare (xargs :guard (and (term-p t1) (term-p t2)))) + (mgs-mv (list (cons t1 t2)))) + + + +;;; We also define as functions the property of being unifiable and the +;;; umg substitution: +(defun unifiable (t1 t2) + (declare (xargs :guard (and (term-p t1) (term-p t2)))) + (mv-let (mgu unifiable) + (mgu-mv t1 t2) + (declare (ignore mgu)) + unifiable)) + +(defun mgu (t1 t2) + (declare (xargs :guard (and (term-p t1) (term-p t2)))) + (mv-let (mgu unifiable) + (mgu-mv t1 t2) + (declare (ignore unifiable)) + mgu)) + + +;;; REMARK: mgu-mv will be used to compute unifiability and most general +;;; unifier at the same time. The functions unifiable and mgu are +;;; defined to be used in the statements of theorems. + +;;; ============================================================================ +;;; 2. Fundamental properties of mgu-mv, unifiable and mgu +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 2.1 Some lemmas needed for the functional instantiation (second part) +;;; ---------------------------------------------------------------------------- + +(local + (defthm booleanp-third-solve-system + (implies (booleanp bool) + (booleanp (third (solve-system S sol bool)))) + :rule-classes :type-prescription)) + +(local + (defthm nil-third-implies-nil-second-solve-system + (implies (not (third (solve-system S sol t))) + (not (second (solve-system S sol t)))))) + + +;;; solve-system-sel of unification-pattern.lisp cannot be +;;; instantiated by solve-system, since they different signatures, due +;;; to the use of multi values in transform-mm. Instead, we will +;;; instantiate solve-system-sel for the following function: + +(local + (defun solve-system-bridge (S-sol) + (if (not (consp S-sol)) + S-sol + (mv-let (S1 sol1 bool1) + (solve-system (car S-sol) (cdr S-sol) t) + (if bool1 (cons S1 sol1) nil))))) + +;;; The same happens with mgs-sel and mgu-sel + +(local + (defun mgs-mv-bridge (S) + (let ((solve-system-bridge (solve-system-bridge (cons S nil)))) + (if solve-system-bridge (list (cdr solve-system-bridge)) nil)))) + +(local + (defun unifiable-bridge (t1 t2) + (mgs-mv-bridge (list (cons t1 t2))))) + +(local + (defun mgu-bridge (t1 t2) + (first (unifiable-bridge t1 t2)))) + + +;;; ---------------------------------------------------------------------------- +;;; 2.2 The properties +;;; ---------------------------------------------------------------------------- +;;; Most of these properties are obtained by functional instantiation. + +;;; Completeness +;;; ············ + +(defthm mgu-completeness + (implies (equal (instance t1 sigma) + (instance t2 sigma)) + (unifiable t1 t2)) + :rule-classes nil + :otf-flg t + :hints + (("Goal" + :use + ((:functional-instance + unifiable-sel-completeness + (sel sel-unif) + (transform-mm-sel transform-mm-bridge) + (solve-system-sel solve-system-bridge) + (mgs-sel mgs-mv-bridge) + (unifiable-sel unifiable-bridge)))))) + +;;; The hint is not necessary, but makes the proof shorter. + +;;; Soundness +;;; ········· + + +(defthm mgu-soundness + (implies (unifiable t1 t2) + (equal (instance t1 (mgu t1 t2)) + (instance t2 (mgu t1 t2)))) + :hints + (("Goal" + :use + ((:functional-instance + unifiable-sel-soundness + (sel sel-unif) + (transform-mm-sel transform-mm-bridge) + (solve-system-sel solve-system-bridge) + (mgs-sel mgs-mv-bridge) + (unifiable-sel unifiable-bridge) + (mgu-sel mgu-bridge)))))) + + +;;; Idempotence +;;; ··········· + +(defthm mgu-idempotent + (idempotent (mgu t1 t2)) + :hints + (("Goal" + :use + ((:functional-instance + mgu-sel-idempotent + (sel sel-unif) + (transform-mm-sel transform-mm-bridge) + (solve-system-sel solve-system-bridge) + (mgs-sel mgs-mv-bridge) + (unifiable-sel unifiable-bridge) + (mgu-sel mgu-bridge)))))) + + + +;;; Generality of the unifier +;;; ························· + +(defthm mgu-most-general-unifier + (implies (equal (instance t1 sigma) + (instance t2 sigma)) + (subs-subst (mgu t1 t2) sigma)) + :hints + (("Goal" + :use + ((:functional-instance + mgu-sel-most-general-unifier + (sel sel-unif) + (transform-mm-sel transform-mm-bridge) + (solve-system-sel solve-system-bridge) + (mgs-sel mgs-mv-bridge) + (unifiable-sel unifiable-bridge) + (mgu-sel mgu-bridge)))))) + + + +;;; Substitution-s-p (closure property of mgu) +;;; ·············································· + + +(defthm mgu-substitution-s-p + (implies (and (term-s-p t1) (term-s-p t2)) + (substitution-s-p (mgu t1 t2))) + :hints + (("Goal" + :use + ((:functional-instance + mgu-sel-substitution-s-p + (sel sel-unif) + (transform-mm-sel transform-mm-bridge) + (solve-system-sel solve-system-bridge) + (mgs-sel mgs-mv-bridge) + (unifiable-sel unifiable-bridge) + (mgu-sel mgu-bridge)))))) + + + +;;; Substitution-p (needed for guard verification) +;;; ·············································· + + +(defthm mgu-substitution-p + (implies (and (term-p t1) (term-p t2)) + (substitution-p (mgu t1 t2))) + :hints (("Goal" :use (:functional-instance + mgu-substitution-s-p + (signat (lambda (x n) (eqlablep x))) + (term-s-p-aux term-p-aux) + (substitution-s-p substitution-p))))) + + + +;;; We disable mgu-mv, unifiable and mgu and their executable +;;; counter-parts, to be sure that ONLY the above two properties are +;;; used in the sequel. But before doind this, we state the relations +;;; between mgu-mv and unifiable and mgu. + +(defthm mgu-mv-unifiable + (equal (second (mgu-mv t1 t2)) (unifiable t1 t2))) + +(defthm mgu-mv-mgu + (equal (first (mgu-mv t1 t2)) (mgu t1 t2))) + + +(in-theory (disable mgu-mv (mgu-mv) mgu (mgu) unifiable (unifiable))) + + +;;; ============================================================================ +;;; 3. Some examples +;;; ============================================================================ + +;;; ACL2 !>(mgu '(h u) '(h (b))) +;;; ((U B)) +;;; ACL2 !>(mgu 1 1) +;;; NIL +;;; ACL2 !>(mgu '(f (g x y) (g y x)) '(f u u)) +;;; ((X . Y) (U G Y Y)) +;;; ACL2 !>(unifiable '(f (g x y) (g y x)) '(f x x)) +;;; NIL +;;; ACL2 !>(mgu '(f (h z) (h (h z))) '(f u (h (h (g v v))))) +;;; ((Z G V V) (U H (G V V))) +;;; ACL2 !>(mgu '(f x (g (a) y)) '(f x (g y x))) +;;; ((X A) (Y A)) +;;; ACL2 !>(mgu '(f x (g a y)) '(f x (g y x))) +;;; ((A . X) (Y . X)) +;;; ACL2 !>(mgu '(f x (g (a) y)) '(f x (g y x))) +;;; ((X A) (Y A)) +;;; ACL2 !>(mgu '(f x (g a y)) '(f x (g y x))) +;;; ((A . X) (Y . X)) + + + + diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/terms.pdf.gz b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/terms.pdf.gz Binary files differnew file mode 100644 index 0000000..5eae51d --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/terms.pdf.gz diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/terms.ps.gz b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/terms.ps.gz Binary files differnew file mode 100644 index 0000000..455fe22 --- /dev/null +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/terms.ps.gz |