defmapping-doc

(in-package "ACL2")

(defxdoc defmapping
  :parents (std/util)
  :short "Establish a mapping between two domains."
  :long (topstring (evmac-section-intro (p "A mapping between two domains (i.e. predicates) @($A$) and @($B$)
      consists of two conversions (i.e. functions) @($\alpha$) and @($\beta$).
      The domains and conversions are illustrated in these "
        *defmapping-design-notes*
        ", which use this "
        *notation-design-notes*
        ". Each of the conversions may be
      injective, surjective, both (i.e. bijective), or neither.")
      (p "This macro attempts to verify that
      two specified conversions are mappings between two specified domains
      i.e. that they map values in one domain to values in the other domain.
      Optionally, the macro also attempts to verify
      additional properties of the conversions
      that imply injectivity and/or surjectivity.
      The verification amounts to
      proving the applicability conditions below as theorems,
      from which additional theorems are automatically proved.")
      (p "The domains, conversions, and theorems
      are recorded in the ACL2 @(see world),
      under a specified name that can be referenced from other tools
      (e.g. "
        (seetopic "apt::apt" "APT")
        " transformations).")
      (p "The domains may have multiple arguments,
      and the conversions may have multiple arguments and results.
      In this case, the domains are subsets of
      cartesian products of the ACL2 universe of values,
      and the conversions map tuples to tuples,
      as shown in the `Generalization to Tuples' page of the "
        *defmapping-design-notes*
        "."))
    (evmac-section-form (codeblock "(defmapping name"
        "            doma"
        "            domb"
        "            alpha"
        "            beta"
        "            :beta-of-alpha-thm ..."
        "            :alpha-of-beta-thm ..."
        "            :guard-thms ..."
        "            :unconditional ..."
        "            :thm-names ..."
        "            :thm-enable ..."
        "            :hints ..."
        "            :print ..."
        "            :show-only ..."
        "  )"))
    (evmac-section-inputs (desc "@('name')"
        (p "Name under which the domains, conversions, and theorems
       are recorded in the world.")
        (p "It must be a symbol that is not a keyword."))
      (desc (list "@('doma')" "@('domb')" "@('alpha')" "@('beta')")
        (p "Denote
       the domain @($A$),
       the domain @($B$),
       the conversion @($\alpha$) from @($A$) to @($B$), and
       the conversion @($\beta$) from @($B$) to @($A$).")
        (evmac-desc-function/lambda/macro :subject "Each"
          :stobjs t
          :guard "the @(':guard-thms') input is @('t')")
        (p "Let @('n') be the arity of @('doma'),
       and @('m') be the arity of @('domb').
       Then:
       @('alpha') must take @('n') arguments and return @('m') results;
       @('beta') must take @('m') arguments and return @('n') results;
       @('doma') and @('domb') must return one result."))
      (desc "@(':beta-of-alpha-thm') — default @('nil')"
        (p "Determines whether
       the @(':beta-of-alpha') applicability condition is generated or not,
       which in turn determines whether certain theorems are generated or not.")
        (p "It must be one of the following:")
        (ul (li "@('t'), to generate them.")
          (li "@('nil'), to not generate them.")))
      (desc "@(':alpha-of-beta-thm') — default @('nil')"
        (p "Determines whether
       the @(':alpha-of-beta') applicability condition is generated or not,
       which in turn determines whether certain theorems are generated or not.")
        (p "It must be one of the following:")
        (ul (li "@('t'), to generate them.")
          (li "@('nil'), to not generate them.")))
      (desc "@(':guard-thms') — default @('t')"
        (p "Determines whether the @('...-guard') applicability conditions
       are present or not, and generated as theorems.")
        (p "It must be one of the following:")
        (ul (li "@('t'), to check and generate them.")
          (li "@('nil'), to not check and generate them.")))
      (desc "@(':unconditional') — default @('nil')"
        (p "Determines whether some of the applicability conditions
       and generated theorems are unconditional, i.e. without hypotheses
       (see the `Variant: Unconditional Theorems' page of the "
          *defmapping-design-notes*
          ", and the `Applicability Conditions' and `Generated Events' sections
       below).")
        (p "It must be one of the following:")
        (ul (li "@('t'), for unconditional (i.e. stronger) theorems.")
          (li "@('nil'), for conditional (i.e. normal) theorems."))
        (p "It may be @('t') only if
       @(':beta-of-alpha-thm') is @('t') or
       @(':alpha-of-beta-thm') is @('t')."))
      (desc "@(':thm-names') — default @('nil')"
        (p "Non-default names for the generated theorems.")
        (p "It must be a "
          (seetopic "acl2::keyword-value-listp"
            "keyword-value list")
          " @('(thm1 name1 ... thmp namep)'),
       where each @('thmk') is a keyword
       that identifies one of the generated theorems below,
       and each @('namek') is a valid fresh theorem name."))
      (desc "@(':thm-enable') — default @('nil')"
        (p "Determines which of the generated theorems must be enabled.")
        (p "It must be one of the following:")
        (ul (li "@('nil'), to enable none of them.")
          (li "@(':all'), to enable all of them.")
          (li "@(':all-nonguard'), to enable all of them
        except for the @('...-guard') theorems.")
          (li "A non-empty list @('(thm1 ... thmp)'),
        where each @('thmk') is a keyword
        that identifies one of the generated theorems below,
        to enable the theorems identified by the keywords.
        Only keywords for theorems that are generated
        (based on the @(':beta-of-alpha-thm'), @(':alpha-of-beta-thm'), and
        @(':guard-thms') inputs)
        may be in this list."))
        (p "As explained under `"
          *evmac-section-generated-title*
          "',
       the theorems are generated as rewrite rules,
       if they are valid rewrite rules.
       The enablement specified by @(':thm-enable') applies
       only to those theorems that are rewrite rules;
       it is ignored for theorems that are not rewrite rules.")
        (p "Note that the first and last of the four options above
       could be described as a single one,
       namely as a possibly empty list of theorem keywords,
       where the empty list @('nil') enables no theorem.
       The @(':all') option is provided for completeness,
       but the @(':all-nonguard') may be more useful:
       in general, the @('...-guard') theorems
       do not look like useful rewrite rules,
       while the other theorems generally do.")
        (p "If @(':guard-thms') is @('nil'),
       then the @(':all') and @(':all-nonguard') options are equivalent."))
      (evmac-input-hints)
      (evmac-input-print defmapping)
      (evmac-input-show-only defmapping))
    (evmac-section-appconds defmapping
      (evmac-appcond ":alpha-image"
        (&& (p "The conversion @($\alpha$) maps
        the domain @($A$) to the domain @($B$):")
          (codeblock ";; when m = 1:"
            "(implies (doma a1 ... an)"
            "         (domb (alpha a1 ... an)))"
            ""
            ";; when m > 1:"
            "(implies (doma a1 ... an)"
            "         (mv-let (b1 ... bm) (alpha a1 ... an)"
            "           (domb b1 ... bm)))"))
        :design-notes *defmapping-design-notes*
        :design-notes-appcond "@($\alpha{}A$)")
      (evmac-appcond ":beta-image"
        (&& (p "The conversion @($\beta$) maps
        the domain @($B$) to the domain @($A$):")
          (codeblock ";; when n = 1:"
            "(implies (domb b1 ... bm)"
            "         (doma (beta b1 ... bm)))"
            ""
            ";; when n > 1:"
            "(implies (domb b1 ... bm)"
            "         (mv-let (a1 ... an) (beta b1 ... bm)"
            "           (doma a1 ... an)))"))
        :design-notes *defmapping-design-notes*
        :design-notes-appcond "@($\beta{}B$)")
      (evmac-appcond ":beta-of-alpha"
        (&& (p "The conversion @($\beta$) is left inverse of @($\alpha$), i.e.
        the conversion @($\alpha$) is right inverse of @($\beta$):")
          (codeblock ";; when m = n = 1 and :unconditional is nil:"
            "(implies (doma a)"
            "         (equal (beta (alpha a))"
            "                a))"
            ""
            ";; when m = n = 1 and :unconditional is t:"
            "(equal (beta (alpha a))"
            "       a)"
            ""
            ";; when m = 1 and n > 1 and :unconditional is nil:"
            "(implies (doma a1 ... an)"
            "         (mv-let (aa1 ... aan) (beta (alpha a1 ... an))"
            "           (and (equal aa1 a1)"
            "                ..."
            "                (equal aan an))))"
            ""
            ";; when m = 1 and n > 1 and :unconditional is t:"
            "(mv-let (aa1 ... aan) (beta (alpha a1 ... an))"
            "  (and (equal aa1 a1)"
            "       ..."
            "       (equal aan an)))"
            ""
            ";; when m > 1 and n = 1 and :unconditional is nil:"
            "(implies (doma a)"
            "         (mv-let (b1 ... bm) (alpha a)"
            "           (equal (beta b1 ... bm)"
            "                  a)))"
            ""
            ";; when m > 1 and n = 1 and :unconditional is t:"
            "(mv-let (b1 ... bm) (alpha a)"
            "  (equal (beta b1 ... bm)"
            "         a))"
            ""
            ";; when m > 1 and n > 1 and :unconditional is nil:"
            "(implies (doma a1 ... an)"
            "         (mv-let (b1 ... bm) (alpha a1 ... an)"
            "           (mv-let (aa1 ... aan) (beta b1 ... bm)"
            "             (and (equal aa1 a1)"
            "                  ..."
            "                  (equal aan an)))))"
            ""
            ";; when m > 1 and n > 1 and :unconditional is t:"
            "(mv-let (b1 ... bm) (alpha a1 ... an)"
            "  (mv-let (aa1 ... aan) (beta b1 ... bm)"
            "    (and (equal aa1 a1)"
            "         ..."
            "         (equal aan an))))"))
        :design-notes *defmapping-design-notes*
        :design-notes-appcond "@($\beta{}\alpha$) or @($\beta{}\alpha'$)"
        :presence "@(':beta-of-alpha-thm') is @('t')")
      (evmac-appcond ":alpha-of-beta"
        (&& (p "The conversion @($\alpha$) is left inverse of @($\beta$), i.e.
        the conversion @($\beta$) is right inverse of @($\alpha$):")
          (codeblock ";; when n = m = 1 and :unconditional is nil:"
            "(implies (domb b)"
            "         (equal (alpha (beta b))"
            "                b))"
            ""
            ";; when n = m = 1 and :unconditional is t:"
            "(equal (alpha (beta b))"
            "       b)"
            ""
            ";; when n = 1 and m > 1 and :unconditional is nil:"
            "(implies (domb b1 ... bm)"
            "         (mv-let (bb1 ... bbm) (alpha (beta b1 ... bm))"
            "           (and (equal bb1 b1)"
            "                ..."
            "                (equal bbm bm))))"
            ""
            ";; when n = 1 and m > 1 and :unconditional is t:"
            "(mv-let (bb1 ... bbm) (alpha (beta b1 ... bm))"
            "  (and (equal bb1 b1)"
            "       ..."
            "       (equal bbm bm)))"
            ""
            ";; when n > 1 and m = 1 and :unconditional is nil:"
            "(implies (domb b)"
            "         (mv-let (a1 ... an) (beta b)"
            "           (equal (alpha a1 ... an)"
            "                  b)))"
            ""
            ";; when n > 1 and m = 1 and :unconditional is t:"
            "(mv-let (a1 ... an) (beta b)"
            "  (equal (alpha a1 ... an)"
            "         b))"
            ""
            ";; when n > 1 and m > 1 and :unconditional is nil:"
            "(implies (domb b1 ... bm)"
            "         (mv-let (a1 ... an) (beta b1 ... bm)"
            "           (mv-let (bb1 ... bbm) (alpha a1 ... an)"
            "             (and (equal bb1 b1)"
            "                  ..."
            "                  (equal bbm bm)))))"
            ""
            ";; when n > 1 and m > 1 and :unconditional is t:"
            "(mv-let (a1 ... an) (beta b1 ... bm)"
            "  (mv-let (bb1 ... bbm) (alpha a1 ... an)"
            "    (and (equal bb1 b1)"
            "         ..."
            "         (equal bbm bm))))"))
        :design-notes *defmapping-design-notes*
        :design-notes-appcond "@($\alpha{}\beta$) or @($\alpha{}\beta'$)"
        :presence "@(':alpha-of-beta-thm') is @('t')")
      (p "The @(':beta-of-alpha') applicability condition (when present)
      implies the injectivity of @($\alpha$).
      See the @($\alpha{}i$) and @($\alpha{}i'$) theorems in the "
        *defmapping-design-notes*
        ", and the generated theorem @(':alpha-injective') below.")
      (p "The @(':alpha-of-beta') applicability condition (when present)
      implies the injectivity of @($\beta$).
      See the @($\beta{}i$) and @($\beta{}i'$) theorems in the "
        *defmapping-design-notes*
        ", and the generated theorem @(':beta-injective') below.")
      (p "The @(':alpha-image') applicability condition (always present)
      and the @(':alpha-of-beta') applicability condition (when present)
      imply the surjectivity of @($\alpha$).
      See the @($\alpha{}s$) and @($\alpha{}s'$) theorems in the "
        *defmapping-design-notes*
        ".")
      (p "The @(':beta-image') applicability condition (always present)
      and the @(':beta-of-alpha') applicability condition (when present)
      imply the surjectivity of @($\beta$).
      See the @($\beta{}s$) and @($\beta{}s'$) theorems in the "
        *defmapping-design-notes*
        ".")
      (evmac-appcond ":doma-guard"
        (&& (p "The domain @($A$) is well-defined everywhere:")
          (codeblock "doma-guard<a1,...,an>")
          (p "where @('doma-guard<a1,...,an>') is:
        the guard term of @('doma'),
        if @('doma') is a function;
        the guard obligation of the body of @('doma'),
        if @('doma') is a lambda expression."))
        :design-notes *defmapping-design-notes*
        :design-notes-appcond "@($G{}A$)"
        :presence "@(':guard-thms') is @('t')")
      (evmac-appcond ":domb-guard"
        (&& (p "The domain @($B$) is well-defined everywhere:")
          (codeblock "domb-guard<b1,...,bm>")
          (p "where @('domb-guard<b1,...,bm>') is:
        the guard term of @('domb'),
        if @('domb') is a function;
        the guard obligation of the body of @('domb'),
        if @('domb') is a lambda expression."))
        :design-notes *defmapping-design-notes*
        :design-notes-appcond "@($G{}B$)"
        :presence "@(':guard-thms') is @('t')")
      (evmac-appcond ":alpha-guard"
        (&& (p "The conversion @($\alpha$) is well-defined
        at least over the domain @($A$):")
          (codeblock "(implies (doma a1 ... an)"
            "         alpha-guard<a1,...,an>)")
          (p "where @('alpha-guard<a1,...,an>') is:
        the guard term of @('alpha'),
        if @('alpha') is a function;
        the guard obligation of the body of @('alpha'),
        if @('alpha') is a lambda expression."))
        :design-notes *defmapping-design-notes*
        :design-notes-appcond "@($G{}\alpha$)"
        :presence "@(':guard-thms') is @('t')")
      (evmac-appcond ":beta-guard"
        (&& (p "The conversion @($\beta$) is well-defined
        at least over the domain @($B$):")
          (codeblock "(implies (domb b1 ... bm)"
            "         beta-guard<b1,...,bm>)")
          (p "where @('beta-guard<b1,...,bm>') is:
        the guard term of @('beta'),
        if @('beta') is a function;
        the guard obligation of the body of @('beta'),
        if @('beta') is a lambda expression."))
        :design-notes *defmapping-design-notes*
        :design-notes-appcond "@($G{}\beta$)"
        :presence "@(':guard-thms') is @('t')"))
    (evmac-section-generated (p "Unless overridden via the @(':thm-names') input,
      the name of each generated theorem consists of
      the input @('name') of @('defmapping'),
      followed by @('.'),
      followed by the identifying keyword (without @(':')) below.")
      (p "The theorems are generated as rewrite rules
      if they are valid rewrite rules;
      otherwise, they are generated with no rule classes.
      The macros @(tsee defthmr) and @('defthmdr')
      are used to generate the theorems.")
      (desc (list "@(':alpha-image')"
          "@(':beta-image')"
          "@(':beta-of-alpha')"
          "@(':alpha-of-beta')"
          "@(':doma-guard')"
          "@(':domb-guard')"
          "@(':alpha-guard')"
          "@(':beta-guard')")
        (p "A theorem for each applicability condition.
       The @(':beta-of-alpha') theorem is generated if and only if
       the @(':beta-of-alpha-thm') input is @('t').
       The @(':alpha-of-beta') theorem is generated if and only if
       the @(':alpha-of-beta-thm') input is @('t').
       The @('...-guard') theorems are generated if and only if
       the @(':guard-thms') input is @('t')."))
      (desc "@(':alpha-injective')"
        (p "The conversion @($\alpha$) is injective:")
        (codeblock ";; when :unconditional is nil:"
          "(defthmr name.alpha-injective"
          "  (implies (and (doma a1 ... an)"
          "                (doma aa1 ... aan))"
          "           (equal (equal (alpha a1 ... an)"
          "                         (alpha aa1 ... aan))"
          "                  (and (equal a1 aa1)"
          "                       ..."
          "                       (equal an aan)))))"
          ""
          ";; when :unconditional is t:"
          "(defthmr name.alpha-injective"
          "  (equal (equal (alpha a1 ... an)"
          "                (alpha aa1 ... aan))"
          "         (and (equal a1 aa1)"
          "              ..."
          "              (equal an aan))))")
        (p "This corresponds to @($\alpha{}i$) or @($\alpha{}i'$) in the "
          *defmapping-design-notes*
          ".")
        (p "This theorem is automatically proved
       from the applicability conditions.")
        (p "This theorem is generated if and only if
       the @(':beta-of-alpha-thm') input is @('t')."))
      (desc "@(':beta-injective')"
        (p "The conversion @($\beta$)
       is injective over the domain @($B$):")
        (codeblock ";; when :unconditional is nil:"
          "(defthmr name.beta-injective"
          "  (implies (and (domb b1 ... bm)"
          "                (domb bb1 ... bbm))"
          "           (equal (equal (beta b1 ... bm)"
          "                         (beta bb1 ... bbm))"
          "                  (and (equal b1 bn1)"
          "                       ..."
          "                       (equal bm bbm)))))"
          ""
          ";; when :unconditional is t:"
          "(defthmr name.beta-injective"
          "  (equal (equal (beta b1 ... bm)"
          "                (beta bb1 ... bbm))"
          "         (and (equal b1 bn1)"
          "              ..."
          "              (equal bm bbm))))")
        (p "This corresponds to @($\beta{}i$) or @($\beta{}i'$) in the "
          *defmapping-design-notes*
          ".")
        (p "This theorem is automatically proved
       from the applicability conditions.")
        (p "This theorem is generated if and only if
       the @(':alpha-of-beta-thm') input is @('t').")))
    (evmac-section-redundancy defmapping)))