Smart unfolding support

@[extern lean_get_structural_rec_arg_pos]

opaque Lean.Meta.getStructuralRecArgPos? (declName : Lean.Name) : Lean.CoreM (Option Nat)

Forward declaration. It is defined in the module src/Lean/Elab/PreDefinition/Structural/Eqns.lean. It is possible to avoid this hack if we move Structural.EqnInfo and Structural.eqnInfoExt to this module.

def Lean.Meta.smartUnfoldingSuffix : String

Equations

• Lean.Meta.smartUnfoldingSuffix = "_sunfold"

@[inline]

def Lean.Meta.mkSmartUnfoldingNameFor (declName : Lean.Name) : Lean.Name

Equations

• Lean.Meta.mkSmartUnfoldingNameFor declName = declName.mkStr Lean.Meta.smartUnfoldingSuffix

def Lean.Meta.hasSmartUnfoldingDecl (env : Lean.Environment) (declName : Lean.Name) : Bool

Equations

• Lean.Meta.hasSmartUnfoldingDecl env declName = env.contains (Lean.Meta.mkSmartUnfoldingNameFor declName)

opaque Lean.Meta.smartUnfolding : Lean.Option Bool

def Lean.Meta.markSmartUnfoldingMatch (e : Lean.Expr) : Lean.Expr

Add auxiliary annotation to indicate the match-expression e must be reduced when performing smart unfolding.

Equations

• Lean.Meta.markSmartUnfoldingMatch e = Lean.mkAnnotation `sunfoldMatch e

def Lean.Meta.smartUnfoldingMatch? (e : Lean.Expr) : Option Lean.Expr

Equations

• Lean.Meta.smartUnfoldingMatch? e = Lean.annotation? `sunfoldMatch e

def Lean.Meta.markSmartUnfoldingMatchAlt (e : Lean.Expr) : Lean.Expr

Add auxiliary annotation to indicate expression e (a match alternative rhs) was successfully reduced by smart unfolding.

Equations

• Lean.Meta.markSmartUnfoldingMatchAlt e = Lean.mkAnnotation `sunfoldMatchAlt e

def Lean.Meta.smartUnfoldingMatchAlt? (e : Lean.Expr) : Option Lean.Expr

Equations

• Lean.Meta.smartUnfoldingMatchAlt? e = Lean.annotation? `sunfoldMatchAlt e

Helper methods

def Lean.Meta.isAuxDef (constName : Lean.Name) : Lean.MetaM Bool

Equations

• Lean.Meta.isAuxDef constName = do let env ← Lean.getEnv pure (Lean.isAuxRecursor env constName || Lean.isNoConfusion env constName)

Helper functions for reducing recursors

def Lean.Meta.mkProjFn (ctorVal : Lean.ConstructorVal) (us : List Lean.Level) (params : Array Lean.Expr) (i : Nat) (major : Lean.Expr) : Lean.CoreM Lean.Expr

Create the ith projection major. It tries to use the auto-generated projection functions if available. Otherwise falls back to Expr.proj.

Equations

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

Helper functions for reducing Quot.lift and Quot.ind

Helper function for extracting "stuck term"

partial def Lean.Meta.getStuckMVar? (e : Lean.Expr) : Lean.MetaM (Option Lean.MVarId)

Return some (Expr.mvar mvarId) if metavariable mvarId is blocking reduction.

Weak Head Normal Form auxiliary combinators

inductive Lean.Meta.ProjReductionKind : Type

Configuration for projection reduction. See whnfCore.

• no: Lean.Meta.ProjReductionKind

  Projections s.i are not reduced at whnfCore.

• yes: Lean.Meta.ProjReductionKind

  Projections s.i are reduced at whnfCore, and whnfCore is used at s during the process. Recall that whnfCore does not perform delta reduction (i.e., it will not unfold constant declarations).

• yesWithDelta: Lean.Meta.ProjReductionKind

  Projections s.i are reduced at whnfCore, and whnf is used at s during the process. Recall that whnfCore does not perform delta reduction (i.e., it will not unfold constant declarations), but whnf does.

• yesWithDeltaI: Lean.Meta.ProjReductionKind

  Projections s.i are reduced at whnfCore, and whnfAtMostI is used at s during the process. Recall that whnfAtMostI is like whnf but uses transparency at most instances. This option is stronger than yes, but weaker than yesWithDelta. We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations. When unifying e.g. (@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1, we only want to unify negation (and not all other field operations as well). Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986

instance Lean.Meta.instDecidableEqProjReductionKind : DecidableEq Lean.Meta.ProjReductionKind

Equations

• Lean.Meta.instDecidableEqProjReductionKind x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Lean.Meta.instInhabitedProjReductionKind : Inhabited Lean.Meta.ProjReductionKind

Equations

• Lean.Meta.instInhabitedProjReductionKind = { default := Lean.Meta.ProjReductionKind.no }

instance Lean.Meta.instReprProjReductionKind : Repr Lean.Meta.ProjReductionKind

Equations

• Lean.Meta.instReprProjReductionKind = { reprPrec := Lean.Meta.reprProjReductionKind✝ }

structure Lean.Meta.WhnfCoreConfig : Type

Configuration options for whnfEasyCases and whnfCore.

• iota : Bool

  If true, reduce recursor/matcher applications, e.g., Nat.rec true (fun _ _ => false) Nat.zero reduces to true

• beta : Bool

  If true, reduce terms such as (fun x => t[x]) a into t[a]

• proj : Lean.Meta.ProjReductionKind

  Control projection reduction at whnfCore.

• zeta : Bool

  Zeta reduction: let x := v; e[x] reduces to e[v]. We say a let-declaration let x := v; e is non dependent if it is equivalent to (fun x => e) v. Recall that

  fun x : BitVec 5 => let n := 5; fun y : BitVec n => x = y
  

  is type correct, but

  fun x : BitVec 5 => (fun n => fun y : BitVec n => x = y) 5
  

  is not.

• zetaDelta : Bool

  Zeta-delta reduction: given a local context containing entry x : t := e, free variable x reduces to e.

@[specialize #[]]

partial def Lean.Meta.whnfEasyCases (e : Lean.Expr) (k : Lean.Expr → Lean.MetaM Lean.Expr) (config : Lean.Meta.WhnfCoreConfig := { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }) : Lean.MetaM Lean.Expr

Auxiliary combinator for handling easy WHNF cases. It takes a function for handling the "hard" cases as an argument

inductive Lean.Meta.ReduceMatcherResult : Type

• reduced: Lean.Expr → Lean.Meta.ReduceMatcherResult
• stuck: Lean.Expr → Lean.Meta.ReduceMatcherResult
• notMatcher: Lean.Meta.ReduceMatcherResult
• partialApp: Lean.Meta.ReduceMatcherResult

The "match" compiler uses dependent if-then-else dite and other auxiliary declarations to compile match-expressions such as

match v with
| 'a' => 1
| 'b' => 2
| _   => 3

because it is more efficient than using casesOn recursors. The method reduceMatcher? fails if these auxiliary definitions cannot be unfolded in the current transparency setting. This is problematic because tactics such as simp use TransparencyMode.reducible, and most users assume that expressions such as

match 0 with
| 0 => 1
| 100 => 2
| _ => 3

should reduce in any transparency mode.

Thus, if the transparency mode is .reducible or .instances, we first eagerly unfold dite constants used in the auxiliary match-declaration, and then use a custom canUnfoldAtMatcher predicate for whnfMatcher.

Remark: we used to include dite (and ite) as auxiliary declarations to unfold at canUnfoldAtMatcher, but this is problematic because the dite/ite may occur in the discriminant. See issue #5388.

This solution is not very modular because modifications at the match compiler require changes here. We claim this is defensible because it is reducing the auxiliary declaration defined by the match compiler.

Remark: if the eager unfolding is problematic, we may cache the result. We may also consider not using dite in the match-compiler and use Decidable.casesOn, but it will require changes in how we generate equation lemmas.

Alternative solution: tactics that use TransparencyMode.reducible should rely on the equations we generated for match-expressions. This solution is also not perfect because the match-expression above will not reduce during type checking when we are not using TransparencyMode.default or TransparencyMode.all.

def Lean.Meta.canUnfoldAtMatcher (cfg : Lean.Meta.Config) (info : Lean.ConstantInfo) : Lean.CoreM Bool

Auxiliary predicate for whnfMatcher. See comment above.

Equations

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

def Lean.Meta.reduceMatcher? (e : Lean.Expr) : Lean.MetaM Lean.Meta.ReduceMatcherResult

Equations

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

def Lean.Meta.projectCore? (e : Lean.Expr) (i : Nat) : Lean.MetaM (Option Lean.Expr)

Equations

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

def Lean.Meta.project? (e : Lean.Expr) (i : Nat) : Lean.MetaM (Option Lean.Expr)

Equations

• Lean.Meta.project? e i = do let __do_lift ← Lean.Meta.whnf e Lean.Meta.projectCore? __do_lift i

def Lean.Meta.reduceProj? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Reduce kernel projection Expr.proj .. expression.

Equations

• Lean.Meta.reduceProj? (Lean.Expr.proj typeName i c) = Lean.Meta.project? c i
• Lean.Meta.reduceProj? e = pure none

def Lean.Meta.whnfCore (e : Lean.Expr) (config : Lean.Meta.WhnfCoreConfig := { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }) : Lean.MetaM Lean.Expr

Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction, expand let-expressions, expand assigned meta-variables.

Equations

• Lean.Meta.whnfCore e config = Lean.Meta.whnfCore.go config e

partial def Lean.Meta.whnfCore.go (config : Lean.Meta.WhnfCoreConfig := { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }) (e : Lean.Expr) : Lean.MetaM Lean.Expr

def Lean.Meta.smartUnfoldingReduce? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Recall that _sunfold auxiliary definitions contains the markers: markSmartUnfoldingMatch (*) and markSmartUnfoldingMatchAlt (**). For example, consider the following definition

def r (i j : Nat) : Nat :=
  i +
    match j with
    | Nat.zero => 1
    | Nat.succ j =>
      i + match j with
          | Nat.zero => 2
          | Nat.succ j => r i j

produces the following _sunfold auxiliary definition with the markers

def r._sunfold (i j : Nat) : Nat :=
  i +
    (*) match j with
    | Nat.zero => (**) 1
    | Nat.succ j =>
      i + (*) match j with
          | Nat.zero => (**) 2
          | Nat.succ j => (**) r i j

match expressions marked with markSmartUnfoldingMatch (*) must be reduced, otherwise the resulting term is not definitionally equal to the given expression. The recursion may be interrupted as soon as the annotation markSmartUnfoldingAlt (**) is reached.

For example, the term r i j.succ.succ reduces to the definitionally equal term i + i * r i j

Equations

• Lean.Meta.smartUnfoldingReduce? e = (Lean.Meta.smartUnfoldingReduce?.go e).run

partial def Lean.Meta.smartUnfoldingReduce?.go (e : Lean.Expr) : OptionT Lean.MetaM Lean.Expr

partial def Lean.Meta.smartUnfoldingReduce?.goMatch (e : Lean.Expr) : OptionT Lean.MetaM Lean.Expr

partial def Lean.Meta.unfoldProjInst? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Auxiliary method for unfolding a class projection.

partial def Lean.Meta.unfoldProjInstWhenInstances? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Auxiliary method for unfolding a class projection when transparency is set to TransparencyMode.instances. Recall that class instance projections are not marked with [reducible] because we want them to be in "reducible canonical form".

partial def Lean.Meta.unfoldDefinition? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Unfold definition using "smart unfolding" if possible.

def Lean.Meta.unfoldDefinition (e : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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

@[specialize #[]]

partial def Lean.Meta.whnfHeadPred (e : Lean.Expr) (pred : Lean.Expr → Lean.MetaM Bool) : Lean.MetaM Lean.Expr

def Lean.Meta.whnfUntil (e : Lean.Expr) (declName : Lean.Name) : Lean.MetaM (Option Lean.Expr)

Equations

• Lean.Meta.whnfUntil e declName = do let e ← Lean.Meta.whnfHeadPred e fun (e : Lean.Expr) => pure !e.isAppOf declName if e.isAppOf declName = true then pure (some e) else pure none

def Lean.Meta.reduceRecMatcher? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Try to reduce matcher/recursor/quot applications. We say they are all "morally" recursor applications.

Equations

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

unsafe def Lean.Meta.reduceBoolNativeUnsafe (constName : Lean.Name) : Lean.MetaM Bool

unsafe def Lean.Meta.reduceNatNativeUnsafe (constName : Lean.Name) : Lean.MetaM Nat

@[implemented_by Lean.Meta.reduceBoolNativeUnsafe]

opaque Lean.Meta.reduceBoolNative (constName : Lean.Name) : Lean.MetaM Bool

@[implemented_by Lean.Meta.reduceNatNativeUnsafe]

opaque Lean.Meta.reduceNatNative (constName : Lean.Name) : Lean.MetaM Nat

def Lean.Meta.reduceNative? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.reduceNative? e = pure none

@[inline]

def Lean.Meta.withNatValue {α : Type} (a : Lean.Expr) (k : Nat → Lean.MetaM (Option α)) : Lean.MetaM (Option α)

Equations

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

def Lean.Meta.reduceUnaryNatOp (f : Nat → Nat) (a : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

• Lean.Meta.reduceUnaryNatOp f a = Lean.Meta.withNatValue a fun (a : Nat) => pure (some (Lean.mkRawNatLit (f a)))

def Lean.Meta.reduceBinNatOp (f : Nat → Nat → Nat) (a b : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

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

def Lean.Meta.reducePow (a b : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

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

def Lean.Meta.reduceBinNatPred (f : Nat → Nat → Bool) (a b : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

• Lean.Meta.reduceBinNatPred f a b = Lean.Meta.withNatValue a fun (a : Nat) => Lean.Meta.withNatValue b fun (b : Nat) => pure (some (Lean.toExpr (f a b)))

def Lean.Meta.reduceNat? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

@[export lean_whnf]

partial def Lean.Meta.whnfImp (e : Lean.Expr) : Lean.MetaM Lean.Expr

def Lean.Meta.reduceProjOf? (e : Lean.Expr) (p : Lean.Name → Bool) : Lean.MetaM (Option Lean.Expr)

If e is a projection function that satisfies p, then reduce it

Equations

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