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.

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.

          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 if-then-else expressions 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 (e.g., ite) 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, we define a custom canUnfoldAtMatcher predicate for whnfMatcher.

              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.

              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.

              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.

                      The parameter deltaAtProj controls how to reduce projections s.i. If deltaAtProj == true, then delta reduction is used to reduce s (i.e., whnf is used), otherwise whnfCore.

                      If simpleReduceOnly, then iota and projection reduction are not performed. Note that the value of deltaAtProj is irrelevant if simpleReduceOnly = true.

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