• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
        • 4v-sexpr-eval
        • 4v-sexpr-to-faig
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
        • 4v-sexpr-alist-extract
        • 4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
        • Sexpr-equivs
        • 3v-syntax-sexprp
        • Sexpr-rewriting
          • 4v-shannon-expansion
          • Onehot-rewriting
          • 4v-sexpr-restrict-with-rw
          • 4v-sexpr-compose-with-rw
          • Sexpr-rewrite
          • Sexpr-rewrite-default
          • Sexpr-rewriting-internals
            • Sexpr-unify
            • Sexpr-rewrite
            • Sexpr-rewrite-try-rules
            • Sexpr-rewrite-ground
            • 4v-sexpr-compose-nofal
            • Sexpr-rewrite-sigma
            • Sexpr-rewrite-fncall
          • *sexpr-rewrites*
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Sexpr-rewriting-internals

Sexpr-unify

Unifies an S-expression with a pattern and returns the resulting substitution as an alist binding variables to subterms.

Definitions and Theorems

Function: sexpr-unify

(defun sexpr-unify (pat term alist)
  (declare (xargs :guard t))
  (if (atom pat)
      (if pat (let ((look (hons-assoc-equal pat alist)))
                (if look (if (hqual term (cdr look))
                             (mv t alist)
                           (mv nil alist))
                  (mv t (cons (cons pat term) alist))))
        (mv (eq term nil) alist))
    (if (and (consp term)
             (equal (car pat) (car term)))
        (sexpr-unify-list (cdr pat)
                          (cdr term)
                          alist)
      (mv nil alist))))

Function: sexpr-unify-list

(defun sexpr-unify-list (pat term alist)
  (declare (xargs :guard t))
  (if (atom pat)
      (mv (and (equal pat nil) (equal term nil))
          alist)
    (if (consp term)
        (b* (((mv ok alist)
              (sexpr-unify (car pat)
                           (car term)
                           alist))
             ((unless ok) (mv nil alist)))
          (sexpr-unify-list (cdr pat)
                            (cdr term)
                            alist))
      (mv nil alist))))

Function: sexpr-unify-ind

(defun sexpr-unify-ind (pat term alist)
  (declare (xargs :guard t))
  (if (atom pat)
      (if pat (let ((look (hons-assoc-equal pat alist)))
                (if look (if (hqual term (cdr look))
                             (mv t alist)
                           (mv nil alist))
                  (mv t (cons (cons pat term) alist))))
        (mv (eq term nil) alist))
    (if (and (consp term)
             (equal (car pat) (car term)))
        (sexpr-unify-list-ind (cdr pat)
                              (cdr term)
                              alist)
      (mv nil alist))))

Function: sexpr-unify-list-ind

(defun sexpr-unify-list-ind (pat term alist)
  (declare (xargs :guard t))
  (if (atom pat)
      (mv (and (equal pat nil) (equal term nil))
          alist)
    (if (consp term)
        (b* (((mv & &)
              (sexpr-unify-ind (car pat)
                               (car term)
                               alist))
             ((mv & alist)
              (sexpr-unify (car pat)
                           (car term)
                           alist)))
          (sexpr-unify-list-ind (cdr pat)
                                (cdr term)
                                alist))
      (mv nil alist))))

Function: sexpr-unify-flag

(defun sexpr-unify-flag (flag pat term alist)
 (declare (xargs :non-executable t))
 (declare (ignorable pat term alist))
 (prog2$
    (throw-nonexec-error 'sexpr-unify-flag
                         (list flag pat term alist))
    (cond ((equal flag 'sexpr-unify)
           (if (consp pat)
               (if (consp term)
                   (if (equal (car pat) (car term))
                       (sexpr-unify-flag 'sexpr-unify-list
                                         (cdr pat)
                                         (cdr term)
                                         alist)
                     (cons 'nil (cons alist 'nil)))
                 (cons 'nil (cons alist 'nil)))
             (if pat ((lambda (look pat alist term)
                        (if look (if (hons-equal term (cdr look))
                                     (cons 't (cons alist 'nil))
                                   (cons 'nil (cons alist 'nil)))
                          (cons 't
                                (cons (cons (cons pat term) alist)
                                      'nil))))
                      (hons-assoc-equal pat alist)
                      pat alist term)
               (cons (equal term 'nil)
                     (cons alist 'nil)))))
          (t (if (consp pat)
                 (if (consp term)
                     ((lambda (mv alist term pat)
                        ((lambda (ignore-0 ignore-1 alist term pat)
                           ((lambda (mv term pat)
                              ((lambda (ignore-0 alist term pat)
                                 (sexpr-unify-flag 'sexpr-unify-list
                                                   (cdr pat)
                                                   (cdr term)
                                                   alist))
                               (hide (mv-nth '0 mv))
                               (mv-nth '1 mv)
                               term pat))
                            (sexpr-unify (car pat) (car term) alist)
                            term pat))
                         (hide (mv-nth '0 mv))
                         (hide (mv-nth '1 mv))
                         alist term pat))
                      (sexpr-unify-flag 'sexpr-unify
                                        (car pat)
                                        (car term)
                                        alist)
                      alist term pat)
                   (cons 'nil (cons alist 'nil)))
               (if (equal pat 'nil)
                   (cons (equal term 'nil)
                         (cons alist 'nil))
                 (cons 'nil (cons alist 'nil))))))))

Theorem: sexpr-unify-flag-equivalences

(defthm sexpr-unify-flag-equivalences
  (and (equal (sexpr-unify-flag 'sexpr-unify
                                pat term alist)
              (sexpr-unify-ind pat term alist))
       (equal (sexpr-unify-flag 'sexpr-unify-list
                                pat term alist)
              (sexpr-unify-list-ind pat term alist))))

Theorem: sexpr-unify-hons-assoc-equal-prev

(defthm sexpr-unify-hons-assoc-equal-prev
  (mv-let (ok alist1)
          (sexpr-unify pat term alist)
    (declare (ignore ok))
    (implies (hons-assoc-equal x alist)
             (equal (hons-assoc-equal x alist1)
                    (hons-assoc-equal x alist)))))

Theorem: sexpr-unify-list-hons-assoc-equal-prev

(defthm sexpr-unify-list-hons-assoc-equal-prev
  (mv-let (ok alist1)
          (sexpr-unify-list pat term alist)
    (declare (ignore ok))
    (implies (hons-assoc-equal x alist)
             (equal (hons-assoc-equal x alist1)
                    (hons-assoc-equal x alist)))))

Theorem: 4v-sexpr-vars-assoc-sexpr-unify

(defthm 4v-sexpr-vars-assoc-sexpr-unify
  (mv-let (ok alist)
          (sexpr-unify pat term alist)
    (implies (and ok (member-equal v (4v-sexpr-vars pat)))
             (hons-assoc-equal v alist))))

Theorem: 4v-sexpr-vars-list-assoc-sexpr-unify-list

(defthm 4v-sexpr-vars-list-assoc-sexpr-unify-list
  (mv-let (ok alist)
          (sexpr-unify-list pat term alist)
    (implies (and ok
                  (member-equal v (4v-sexpr-vars-list pat)))
             (hons-assoc-equal v alist))))

Theorem: sexpr-unify-4v-sexpr-compose-tail-vars

(defthm sexpr-unify-4v-sexpr-compose-tail-vars
  (mv-let (ok alist1)
          (sexpr-unify pat term alist)
    (declare (ignore ok))
    (implies (subsetp-equal (4v-sexpr-vars x)
                            (alist-keys alist))
             (equal (4v-sexpr-compose x alist1)
                    (4v-sexpr-compose x alist)))))

Theorem: sexpr-unify-4v-sexpr-compose-list-tail-vars

(defthm sexpr-unify-4v-sexpr-compose-list-tail-vars
  (mv-let (ok alist1)
          (sexpr-unify pat term alist)
    (declare (ignore ok))
    (implies (subsetp-equal (4v-sexpr-vars-list x)
                            (alist-keys alist))
             (equal (4v-sexpr-compose-list x alist1)
                    (4v-sexpr-compose-list x alist)))))

Theorem: sexpr-unify-list-4v-sexpr-compose-tail-vars

(defthm sexpr-unify-list-4v-sexpr-compose-tail-vars
  (mv-let (ok alist1)
          (sexpr-unify-list pat term alist)
    (declare (ignore ok))
    (implies (subsetp-equal (4v-sexpr-vars x)
                            (alist-keys alist))
             (equal (4v-sexpr-compose x alist1)
                    (4v-sexpr-compose x alist)))))

Theorem: sexpr-unify-list-4v-sexpr-compose-list-tail-vars

(defthm sexpr-unify-list-4v-sexpr-compose-list-tail-vars
  (mv-let (ok alist1)
          (sexpr-unify-list pat term alist)
    (declare (ignore ok))
    (implies (subsetp-equal (4v-sexpr-vars-list x)
                            (alist-keys alist))
             (equal (4v-sexpr-compose-list x alist1)
                    (4v-sexpr-compose-list x alist)))))

Theorem: sexpr-unify-vars-subset-of-keys

(defthm sexpr-unify-vars-subset-of-keys
  (mv-let (ok alist1)
          (sexpr-unify pat term alist)
    (implies ok
             (subsetp-equal (4v-sexpr-vars pat)
                            (alist-keys alist1)))))

Theorem: sexpr-unify-list-vars-subset-of-keys

(defthm sexpr-unify-list-vars-subset-of-keys
  (mv-let (ok alist1)
          (sexpr-unify-list pat term alist)
    (implies ok
             (subsetp-equal (4v-sexpr-vars-list pat)
                            (alist-keys alist1)))))

Theorem: sexpr-unify-4v-sexpr-compose

(defthm sexpr-unify-4v-sexpr-compose
  (mv-let (ok alist)
          (sexpr-unify pat term alist)
    (implies ok
             (equal (4v-sexpr-compose pat alist)
                    term))))

Theorem: sexpr-unify-list-4v-sexpr-compose-list

(defthm sexpr-unify-list-4v-sexpr-compose-list
  (mv-let (ok alist)
          (sexpr-unify-list pat term alist)
    (implies ok
             (equal (4v-sexpr-compose-list pat alist)
                    term))))

Theorem: sexpr-unify-alist-vars

(defthm sexpr-unify-alist-vars
 (implies
  (and (not (member-equal x (4v-sexpr-vars term)))
       (not (member-equal x
                          (4v-sexpr-vars-list (alist-vals alist)))))
  (not
   (member-equal
      x
      (4v-sexpr-vars-list
           (alist-vals (mv-nth 1 (sexpr-unify pat term alist))))))))

Theorem: sexpr-unify-list-alist-vars

(defthm sexpr-unify-list-alist-vars
 (implies
  (and (not (member-equal x (4v-sexpr-vars-list term)))
       (not (member-equal x
                          (4v-sexpr-vars-list (alist-vals alist)))))
  (not
   (member-equal
    x
    (4v-sexpr-vars-list
        (alist-vals (mv-nth 1
                            (sexpr-unify-list pat term alist))))))))

Function: max-acl2-count

(defun max-acl2-count (x)
  (declare (xargs :guard t))
  (if (atom x)
      0
    (max (acl2-count (car x))
         (max-acl2-count (cdr x)))))

Theorem: acl2-count-gte-max-acl2-count-of-args

(defthm acl2-count-gte-max-acl2-count-of-args
  (implies (consp term)
           (< (max-acl2-count (cdr term))
              (acl2-count term)))
  :rule-classes
  ((:linear :trigger-terms ((max-acl2-count (cdr term))))))

Theorem: sexpr-unify-alist-max-count-small-term

(defthm sexpr-unify-alist-max-count-small-term
 (implies
   (<= (acl2-count term)
       (max-acl2-count (alist-vals alist)))
   (equal (max-acl2-count
               (alist-vals (mv-nth 1 (sexpr-unify pat term alist))))
          (max-acl2-count (alist-vals alist)))))

Theorem: sexpr-unify-list-alist-max-count-small-term

(defthm sexpr-unify-list-alist-max-count-small-term
 (implies
  (<= (max-acl2-count term)
      (max-acl2-count (alist-vals alist)))
  (equal
     (max-acl2-count
          (alist-vals (mv-nth 1 (sexpr-unify-list pat term alist))))
     (max-acl2-count (alist-vals alist)))))

Theorem: sexpr-unify-alist-max-count-large-term

(defthm sexpr-unify-alist-max-count-large-term
 (implies
      (<= (max-acl2-count (alist-vals alist))
          (acl2-count term))
      (<= (max-acl2-count
               (alist-vals (mv-nth 1 (sexpr-unify pat term alist))))
          (acl2-count term)))
 :rule-classes (:rewrite :linear))

Theorem: sexpr-unify-list-alist-max-count-large-term

(defthm sexpr-unify-list-alist-max-count-large-term
 (implies
  (<= (max-acl2-count (alist-vals alist))
      (max-acl2-count term))
  (<=
     (max-acl2-count
          (alist-vals (mv-nth 1 (sexpr-unify-list pat term alist))))
     (max-acl2-count term)))
 :rule-classes (:rewrite :linear))

Theorem: sexpr-vars-alist-of-unify

(defthm sexpr-vars-alist-of-unify
  (subsetp-equal
       (4v-sexpr-vars-list
            (alist-vals (mv-nth 1 (sexpr-unify pat term alist))))
       (append (4v-sexpr-vars term)
               (4v-sexpr-vars-list (alist-vals alist)))))

Theorem: sexpr-vars-alist-of-unify-list

(defthm sexpr-vars-alist-of-unify-list
 (subsetp-equal
     (4v-sexpr-vars-list
          (alist-vals (mv-nth 1 (sexpr-unify-list pat term alist))))
     (append (4v-sexpr-vars-list term)
             (4v-sexpr-vars-list (alist-vals alist)))))

Theorem: alist-keys-of-sexpr-unify

(defthm alist-keys-of-sexpr-unify
  (mv-let (ok alist1)
          (sexpr-unify pat term alist)
    (implies ok
             (set-equiv (alist-keys alist1)
                        (append (4v-sexpr-vars pat)
                                (alist-keys alist))))))

Theorem: alist-keys-of-sexpr-unify-list

(defthm alist-keys-of-sexpr-unify-list
  (mv-let (ok alist1)
          (sexpr-unify-list pat term alist)
    (implies ok
             (set-equiv (alist-keys alist1)
                        (append (4v-sexpr-vars-list pat)
                                (alist-keys alist))))))