Documentation

Lean.Meta.Canonicalizer

Applications have implicit arguments. Thus, two terms that may look identical when pretty-printed can be structurally different. For example, @id (Id Nat) x and @id Nat x are structurally different but are both pretty-printed as id x. Moreover, these two terms are definitionally equal since Id Nat reduces to Nat. This may create situations that are counterintuitive to our users. Furthermore, several tactics (e.g., omega) need to collect unique atoms in a goal. One simple approach is to maintain a list of atoms found so far, and whenever a new atom is discovered, perform a linear scan to test whether it is definitionally equal to a previously found one. However, this method is too costly, even if the definitional equality test were inexpensive.

This module aims to efficiently identify terms that are structurally different, definitionally equal, and structurally equal when we disregard implicit arguments like @id (Id Nat) x and @id Nat x. The procedure is straightforward. For each atom, we create a hash that ignores all implicit information. Thus the hash for terms are equal @id (Id Nat) x and @id Nat x. To preserve any pre-existing directed acyclic graph (DAG) structure and prevent exponential blowups while computing the hash code, we employ unsafe techniques, such as pointer equality. Additionally, we maintain a mapping from hash to lists of terms, where each list contains terms sharing the same hash but not definitionally equal. We posit that these lists will be small in practice.

Auxiliary structure for creating a pointer-equality.

Instances For

    State for the CanonM monad.

    Instances For
      Equations
      def Lean.Meta.Canonicalizer.CanonM.run' {α : Type} (x : Lean.Meta.CanonM α) (transparency : optParam Lean.Meta.TransparencyMode Lean.Meta.TransparencyMode.instances) (s : optParam Lean.Meta.Canonicalizer.State { cache := Lean.mkHashMapImp, keyToExprs := Lean.mkHashMap }) :

      The definitionally equality tests are performed using the given transparency mode. We claim TransparencyMode.instances is a good setting for most applications.

      Equations
      • x.run' transparency s = (x transparency).run' s
      Instances For
        Equations
        • x.run transparency s = (x transparency).run s
        Instances For

          "Canonicalize" the given expression.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For