Documentation

Lean.Meta.Sym.Simp.App

Simplifying Application Arguments and Congruence Lemma Application #

This module provides functions for building congruence proofs during simplification. Given a function application f a₁ ... aₙ where some arguments are rewritable, we recursively simplify those arguments (via simp) and construct a proof that the original expression equals the simplified one.

The key challenge is efficiency: we want to avoid repeatedly inferring types, or destroying sharing, The CongrInfo type (see SymM.lean) categorizes functions by their argument structure, allowing us to choose the most efficient proof strategy:

Design principle: Never infer the type of proofs. This avoids expensive type inference on proof terms, which can be arbitrarily complex, and often destroys sharing.

source
def Lean.Meta.Sym.Simp.mkCongr (e f a : Expr) (fr ar : Result) :
e = f.app a → SymM Result

Helper function for constructing a congruence proof using congrFun', congrArg, congr. For the dependent case, use mkCongrFun

Equations
Instances For
    source
    def Lean.Meta.Sym.Simp.simpOverApplied (e : Expr) (numArgs : Nat) (simpFn : Expr → SimpM Result) :
    SimpM Result

    Handles simplification of over-applied function terms.

    When a function has more arguments than expected by its CongrInfo, we need to handle the "extra" arguments separately. This function peels off numArgs trailing applications, simplifies the remaining function using simpFn, then rebuilds the term by simplifying and re-applying the trailing arguments.

    Over-application occurs when:

    • A function with fixedPrefix prefixSize suffixSize is applied to more than prefixSize + suffixSize arguments
    • A function with interlaced rewritable mask is applied to more than mask.size arguments
    • A function with a congruence theorem is applied to more than the theorem expects

    Example: If f has CongrInfo.fixedPrefix 2 3 (expects 5 arguments) but we see f a₁ a₂ a₃ a₄ a₅ b₁ b₂, then numArgs = 2 (the extra arguments) and we:

    1. Recursively simplify f a₁ a₂ a₃ a₄ a₅ using the fixed prefix strategy (via simpFn)
    2. Simplify each extra argument b₁ and b₂
    3. Rebuild the term using either mkCongr (for non-dependent arrows) or mkCongrFun (for dependent functions)

    Parameters:

    • e: The over-applied expression to simplify
    • numArgs: Number of excess arguments to peel off
    • simpFn: Strategy for simplifying the function after peeling (e.g., simpFixedPrefix, simpInterlaced, or simpUsingCongrThm)

    Note: This is a fallback path without specialized optimizations. The common case (correct number of arguments) is handled more efficiently by the specific strategies.

    Equations
    Instances For
      source
      def Lean.Meta.Sym.Simp.propagateOverApplied (e : Expr) (numArgs : Nat) (simpFn : Expr → SimpM Result) :
      SimpM Result

      Handles over-applied function expressions by simplifying only the base function and propagating changes through extra arguments WITHOUT simplifying them.

      Unlike simpOverApplied, this function does not simplify the extra arguments themselves. It only uses congruence (mkCongrFun) to propagate changes when the base function is simplified.

      Algorithm:

      1. Peel off numArgs extra arguments from e
      2. Apply simpFn to simplify the base function
      3. If the base changed, propagate the change through each extra argument using mkCongrFun
      4. Return .rfl if the base function was not simplified

      Parameters:

      • e: The over-applied expression
      • numArgs: Number of excess arguments to peel off
      • simpFn: Strategy for simplifying the base function after peeling

      Contrast with simpOverApplied:

      Equations
      Instances For
        source
        def Lean.Meta.Sym.Simp.simpFixedPrefix (e : Expr) (prefixSize suffixSize : Nat) :
        SimpM Result

        Simplifies arguments of a function application with a fixed prefix structure. Recursively simplifies the trailing suffixSize arguments, leaving the first prefixSize arguments unchanged.

        For a function with CongrInfo.fixedPrefix prefixSize suffixSize, the arguments are structured as:

        f a₁ ... aₚ b₁ ... bₛ
  └───────┘ └───────┘
   prefix    suffix (rewritable)

        The prefix arguments (types, instances) should not be rewritten directly. Only the suffix arguments are recursively simplified.

        Performance optimization: We avoid calling inferType on applied expressions like f a₁ ... aₚ b₁ or f a₁ ... aₚ b₁ ... bₛ, which would have poor cache hit rates. Instead, we infer the type of the function prefix f a₁ ... aₚ (e.g., @HAdd.hAdd Nat Nat Nat instAdd) which is probably shared across many applications, then traverse the forall telescope to extract argument and result types as needed.

        The helper go returns Result × Expr where the Expr is the function type at that position. However, the type is only meaningful (non-default) when Result is .step, since we only need types for constructing congruence proofs. This avoids unnecessary type inference when no rewriting occurs.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Meta.Sym.Simp.simpInterlaced (e : Expr) (rewritable : Array Bool) :
          SimpM Result

          Simplifies arguments of a function application with interlaced rewritable/fixed arguments. Uses rewritable[i] to determine whether argument i should be simplified. For rewritable arguments, calls simp and uses congrFun', congrArg, and congr; for fixed arguments, uses congrFun to propagate changes from earlier arguments.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Meta.Sym.Simp.simpAppArgs (e : Expr) :
            SimpM Result

            Main entry point for simplifying function application arguments. Dispatches to the appropriate strategy based on the function's CongrInfo.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Lean.Meta.Sym.Simp.simpAppArgRange (e : Expr) (start stop : Nat) :
              SimpM Result

              Simplifies arguments in a specified range [start, stop) of a function application.

              Given an expression f a₀ a₁ ... aₙ, this function simplifies only the arguments at positions start ≤ i < stop, leaving arguments outside this range unchanged. Changes are propagated using congruence lemmas.

              Use case: Useful for control-flow simplification where we want to simplify only discriminants of a match expression without touching the branches.

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