02c8c2f9e1
This PR implements first-class support for nondependent let expressions in the elaborator; recall that a let expression `let x : t := v; b` is called *nondependent* if `fun x : t => b` typechecks, and the notation for a nondependent let expression is `have x := v; b`. Previously we encoded `have` using the `letFun` function, but now we make use of the `nondep` flag in the `Expr.letE` constructor for the encoding. This has been given full support throughout the metaprogramming interface and the elaborator. Key changes to the metaprogramming interface: - Local context `ldecl`s with `nondep := true` are generally treated as `cdecl`s. This is because in the body of a `have` expression the variable is opaque. Functions like `LocalDecl.isLet` by default return `false` for nondependent `ldecl`s. In the rare case where it is needed, they take an additional optional `allowNondep : Bool` flag (defaults to `false`) if the variable is being processed in a context where the value is relevant. - Functions such as `mkLetFVars` by default generalize nondependent let variables and create lambda expressions for them. The `generalizeNondepLet` flag (default true) can be set to false if `have` expressions should be produced instead. **Breaking change:** Uses of `letLambdaTelescope`/`mkLetFVars` need to use `generalizeNondepLet := false`. See the next item. - There are now some mapping functions to make telescoping operations more convenient. See `mapLetTelescope` and `mapLambdaLetTelescope`. There is also `mapLetDecl` as a counterpart to `withLetDecl` for creating `let`/`have` expressions. - Important note about the `generalizeNondepLet` flag: it should only be used for variables in a local context that the metaprogram "owns". Since nondependent let variables are treated as constants in most cases, the `value` field might refer to variables that do not exist, if for example those variables were cleared or reverted. Using `mapLetDecl` is always fine. - The simplifier will cache its let dependence calculations in the nondep field of let expressions. - The `intro` tactic still produces *dependent* local variables. Given that the simplifier will transform lets into haves, it would be surprising if that would prevent `intro` from creating a local variable whose value cannot be used. Note that nondependence of lets is not checked by the kernel. To external checker authors: If the elaborator gets the nondep flag wrong, we consider this to be an elaborator error. Feel free to typecheck `letE n t v b true` as if it were `app (lam n t b default) v` and please report issues. This PR follows up from #8751, which made sure the nondep flag was preserved in the C++ interface.
65 lines
1.5 KiB
Text
65 lines
1.5 KiB
Text
import Lean.Elab.Command
|
|
|
|
/-!
|
|
# Tests for `have x := v; b` notation
|
|
-/
|
|
|
|
/-!
|
|
Checks that types can be inferred and that default instances work with `have`.
|
|
-/
|
|
#check
|
|
have f x := x * 2
|
|
have x := 1
|
|
have y := x + 1
|
|
f (y + x)
|
|
|
|
/-!
|
|
Checks that `simp` can do zeta reduction of `have`s
|
|
-/
|
|
example (a b : Nat) (h1 : a = 0) (h2 : b = 0) : (have x := a + 1; x + x) > b := by
|
|
simp (config := { zeta := false }) [h1]
|
|
trace_state
|
|
simp (config := { decide := true }) [h2]
|
|
|
|
/-!
|
|
Checks that the underlying encoding for `have` can be overapplied.
|
|
This still pretty prints with `have` notation.
|
|
-/
|
|
#check (show Nat → Nat from id) 1
|
|
|
|
/-!
|
|
Checks that zeta reduction still occurs even if the `have` is applied to an argument.
|
|
-/
|
|
example (a b : Nat) (h : a > b) : (show Nat → Nat from id) a > b := by
|
|
simp
|
|
trace_state
|
|
exact h
|
|
|
|
/-!
|
|
Checks that the type of a `have` can depend on the value.
|
|
-/
|
|
#check have n := 5
|
|
(⟨[], Nat.zero_le n⟩ : { as : List Bool // as.length ≤ n })
|
|
|
|
/-!
|
|
Check that `have` is reducible.
|
|
-/
|
|
#check (rfl : (have n := 5; n) = 5)
|
|
|
|
/-!
|
|
Exercise `isDefEqQuick` for `have`.
|
|
-/
|
|
#check (rfl : (have _n := 5; 2) = 2)
|
|
|
|
/-!
|
|
Check that `have` responds to WHNF's `zeta` option.
|
|
-/
|
|
|
|
open Lean Meta Elab Term in
|
|
elab "#whnfCore " z?:(&"noZeta")? t:term : command => Command.runTermElabM fun _ => do
|
|
let e ← withSynthesize <| Term.elabTerm t none
|
|
let e ← withConfig (fun c => { c with zeta := z?.isNone }) <| Meta.whnfCore e
|
|
logInfo m!"{e}"
|
|
|
|
#whnfCore have n := 5; n
|
|
#whnfCore noZeta have n := 5; n
|