Filtering...

extensionality

books/std/omaps/extensionality
other
(in-package "OMAP")
other
(include-book "std/util/define-sk" :dir :system)
other
(include-book "std/util/defrule" :dir :system)
other
(include-book "kestrel/utilities/polarity" :dir :system)
other
(local (include-book "std/basic/controlled-configuration" :dir :system))
other
(local (controlled-configuration :hooks nil))
other
(include-book "core")
other
(include-book "with-fixing-theorems")
other
(include-book "assoc")
other
(include-book "submap")
other
(define-sk ext-equal
  ((x mapp) (y mapp))
  :parents (omaps)
  :short "Extensional equality of @(see omaps)."
  :long (topstring (p "This definition is equivalent to omap equality."))
  (forall (key)
    (equal (assoc key x) (assoc key y)))
  :skolem-name ext-equal-witness)
other
(defrule ext-equal-when-mequiv-of-arg1-congruence
  (implies (mequiv x0 x1)
    (equal (ext-equal x0 y)
      (ext-equal x1 y)))
  :rule-classes :congruence :use (lemma (:instance lemma
      (x0 x1)
      (x1 x0)))
  :prep-lemmas ((defruled lemma
     (implies (and (mequiv x0 x1)
         (ext-equal x0 y))
       (ext-equal x1 y))
     :expand (ext-equal x1 y)
     :enable ext-equal-necc)))
other
(defrule ext-equal-when-mequiv-of-arg2-congruence
  (implies (mequiv y0 y1)
    (equal (ext-equal x y0)
      (ext-equal x y1)))
  :rule-classes :congruence :use (lemma (:instance lemma
      (y0 y1)
      (y1 y0)))
  :prep-lemmas ((defruled lemma
     (implies (and (mequiv y0 y1)
         (ext-equal x y0))
       (ext-equal x y1))
     :expand (ext-equal x y1)
     :enable ext-equal-necc)))
other
(defrule reflexivity-of-ext-equal
  (ext-equal x x)
  :enable ext-equal)
other
(defruled symmetry-of-ext-equal-weak
  (implies (ext-equal x y)
    (ext-equal y x))
  :expand (ext-equal y x)
  :enable ext-equal-necc)
other
(defrule symmetry-of-ext-equal
  (equal (ext-equal y x)
    (ext-equal x y))
  :use (symmetry-of-ext-equal-weak (:instance symmetry-of-ext-equal-weak
      (x y)
      (y x))))
other
(defruledl submap-when-ext-equal
  (implies (ext-equal x y)
    (submap x y))
  :enable (submap-to-submap-sk submap-sk
    ext-equal-necc))
other
(defruled ext-equal-becomes-equal
  (equal (ext-equal x y)
    (equal (mfix x) (mfix y)))
  :use lemma
  :prep-lemmas ((defruled lemma
     (implies (ext-equal x y)
       (equal (mfix x) (mfix y)))
     :enable (double-containment submap-when-ext-equal))))
other
(defruled equal-becomes-ext-equal-when-mapp
  (implies (and (mapp x) (mapp y))
    (equal (equal x y)
      (ext-equal x y)))
  :enable ext-equal-becomes-equal)
other
(defrule transitivity-of-ext-equal
  (implies (and (ext-equal x y)
      (ext-equal y z))
    (ext-equal x z))
  :enable ext-equal-becomes-equal)
other
(defequiv ext-equal)
other
(defsection extensionality
  :parents (omaps)
  :short "Prove omap equality by extensionality."
  :long (topstring (p "This rule rewrites an equality of omaps into an equality of
     @(tsee assoc) on an arbitrary element. The right-hand side is the
     expansion of @('(ext-equal x y)')."))
  (defruled extensionality
    (implies (and (mapp x) (mapp y))
      (equal (equal x y)
        (let ((arbitrary-key (ext-equal-witness x y)))
          (equal (assoc arbitrary-key x)
            (assoc arbitrary-key y)))))
    :rule-classes ((:rewrite :backchain-limit-lst (1 1)))
    :enable ext-equal
    :use equal-becomes-ext-equal-when-mapp))