Documentation

Lean.Meta.WHNF

Smart unfolding support #

@[extern lean_get_structural_rec_arg_pos]

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.

Equations
Instances For

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

    Equations
    Instances For

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

      Equations
      Instances For

        Helper methods #

        Equations
        Instances For

          Helper functions for reducing recursors #

          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.
          Instances For

            Helper functions for reducing Quot.lift and Quot.ind #

            Helper function for extracting "stuck term" #

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

            Weak Head Normal Form auxiliary combinators #

            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

            Instances For

              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]

              • 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.

              Instances For
                @[specialize #[]]

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

                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.

                Auxiliary predicate for whnfMatcher. See comment above.

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

                        Reduce kernel projection Expr.proj .. expression.

                        Equations
                        Instances For

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

                          Equations
                          Instances For

                            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
                            Instances For

                              Auxiliary method for unfolding a class projection.

                              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".

                              Unfold definition using "smart unfolding" if possible.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[specialize #[]]
                                Equations
                                Instances For

                                  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.
                                  Instances For
                                    Instances For
                                      Instances For
                                        @[implemented_by Lean.Meta.reduceBoolNativeUnsafe]
                                        @[implemented_by Lean.Meta.reduceNatNativeUnsafe]
                                        Equations
                                        Instances For
                                          @[inline]
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[export lean_whnf]

                                                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.
                                                Instances For