Compare commits

..

1 Commits

Author SHA1 Message Date
Sofia Rodrigues
6313f22b1e feat: future 2026-01-09 20:01:19 -03:00
1852 changed files with 2458 additions and 7629 deletions

View File

@@ -45,7 +45,3 @@ feat: add optional binder limit to `mkPatternFromTheorem`
This PR adds a `num?` parameter to `mkPatternFromTheorem` to control how many
leading quantifiers are stripped when creating a pattern.
```
## CI Log Retrieval
When CI jobs fail, investigate immediately - don't wait for other jobs to complete. Individual job logs are often available even while other jobs are still running. Try `gh run view <run-id> --log` or `gh run view <run-id> --log-failed`, or use `gh run view <run-id> --job=<job-id>` to target the specific failed job. Sleeping is fine when asked to monitor CI and no failures exist yet, but once any job fails, investigate that failure immediately.

View File

@@ -267,17 +267,14 @@ jobs:
"test": true,
// turn off custom allocator & symbolic functions to make LSAN do its magic
"CMAKE_PRESET": "sanitize",
// * `StackOverflow*` correctly triggers ubsan.
// * `reverse-ffi` fails to link in sanitizers.
// * `interactive` and `async_select_channel` fail nondeterministically, would need
// to be investigated..
// * 9366 is too close to timeout.
// * `bv_` sometimes times out calling into cadical even though we should be using
// the standard compile flags for it.
// * `grind_guide` always times out.
// * `pkg/|lake/` tests sometimes time out (likely even hang), related to Lake CI
// failures?
"CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366|run/bv_|grind_guide|pkg/|lake/'"
// `StackOverflow*` correctly triggers ubsan.
// `reverse-ffi` fails to link in sanitizers.
// `interactive` and `async_select_channel` fail nondeterministically, would need to
// be investigated..
// 9366 is too close to timeout.
// `bv_` sometimes times out calling into cadical even though we should be using the
// standard compile flags for it.
"CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366|run/bv_'"
},
{
"name": "macOS",

View File

@@ -5,13 +5,12 @@ Authors: Mario Carneiro, Sebastian Ullrich
-/
module
prelude
public import Init.Prelude
public import Init.System.IO
public import Lean.Util.Path
import Lean.Environment
import Lean.ExtraModUses
import Lake.CLI.Main
import Lean.Parser.Module
import Lake.Load.Workspace
/-! # Shake: A Lean import minimizer
@@ -21,12 +20,84 @@ ensuring that every import is used to contribute some constant or other elaborat
recorded by `recordExtraModUse` and friends.
-/
/-- help string for the command line interface -/
def help : String := "Lean project tree shaking tool
Usage: lake exe shake [OPTIONS] <MODULE>..
Arguments:
<MODULE>
A module path like `Mathlib`. All files transitively reachable from the
provided module(s) will be checked.
Options:
--force
Skips the `lake build --no-build` sanity check
--keep-implied
Preserves existing imports that are implied by other imports and thus not technically needed
anymore
--keep-prefix
If an import `X` would be replaced in favor of a more specific import `X.Y...` it implies,
preserves the original import instead. More generally, prefers inserting `import X` even if it
was not part of the original imports as long as it was in the original transitive import closure
of the current module.
--keep-public
Preserves all `public` imports to avoid breaking changes for external downstream modules
--add-public
Adds new imports as `public` if they have been in the original public closure of that module.
In other words, public imports will not be removed from a module unless they are unused even
in the private scope, and those that are removed will be re-added as `public` in downstream
modules even if only needed in the private scope there. Unlike `--keep-public`, this may
introduce breaking changes but will still limit the number of inserted imports.
--explain
Gives constants explaining why each module is needed
--fix
Apply the suggested fixes directly. Make sure you have a clean checkout
before running this, so you can review the changes.
--gh-style
Outputs messages that can be parsed by `gh-problem-matcher-wrap`
Annotations:
The following annotations can be added to Lean files in order to configure the behavior of
`shake`. Only the substring `shake: ` directly followed by a directive is checked for, so multiple
directives can be mixed in one line such as `-- shake: keep-downstream, shake: keep-all`, and they
can be surrounded by arbitrary comments such as `-- shake: keep (metaprogram output dependency)`.
* `module -- shake: keep-downstream`:
Preserves this module in all (current) downstream modules, adding new imports of it if needed.
* `module -- shake: keep-all`:
Preserves all existing imports in this module as is. New imports now needed because of upstream
changes may still be added.
* `import X -- shake: keep`:
Preserves this specific import in the current module. The most common use case is to preserve a
public import that will be needed in downstream modules to make sense of the output of a
metaprogram defined in this module. For example, if a tactic is defined that may synthesize a
reference to a theorem when run, there is no way for `shake` to detect this by itself and the
module of that theorem should be publicly imported and annotated with `keep` in the tactic's
module.
```
public import X -- shake: keep (metaprogram output dependency)
...
elab \"my_tactic\" : tactic => do
... mkConst ``f -- `f`, defined in `X`, may appear in the output of this tactic
```
"
open Lean
namespace Lake.Shake
/-- The parsed CLI arguments for shake. -/
public structure Args where
/-- The parsed CLI arguments. See `help` for more information -/
structure Args where
help : Bool := false
keepImplied : Bool := false
keepPrefix : Bool := false
keepPublic : Bool := false
@@ -65,7 +136,7 @@ instance : Union Bitset where
instance : XorOp Bitset where
xor a b := { toNat := a.toNat ^^^ b.toNat }
def has (s : Bitset) (i : Nat) : Bool := s.toNat.testBit i
def has (s : Bitset) (i : Nat) : Bool := s {i}
end Bitset
@@ -166,19 +237,8 @@ structure State where
/-- Edits to be applied to the module imports. -/
edits : Edits := {}
-- Memoizations
reservedNames : Std.HashSet Name := Id.run do
let mut m := {}
for (c, _) in env.constants do
if isReservedName env c then
m := m.insert c
return m
indirectModUses : Std.HashMap Name (Array ModuleIdx) :=
indirectModUseExt.getState env
modNames : Array Name :=
env.header.moduleNames
def State.mods (s : State) := s.env.header.moduleData
def State.modNames (s : State) := s.env.header.moduleNames
/--
Given module `j`'s transitive dependencies, computes the union of `transImps` and the transitive
@@ -233,9 +293,9 @@ def isDeclMeta' (env : Environment) (declName : Name) : Bool :=
Given an `Expr` reference, returns the declaration name that should be considered the reference, if
any.
-/
def getDepConstName? (s : State) (ref : Name) : Option Name := do
def getDepConstName? (env : Environment) (ref : Name) : Option Name := do
-- Ignore references to reserved names, they can be re-generated in-place
guard <| !s.reservedNames.contains ref
guard <| !isReservedName env ref
-- `_simp_...` constants are similar, use base decl instead
return if ref.isStr && ref.getString!.startsWith "_simp_" then
ref.getPrefix
@@ -268,12 +328,12 @@ where
let env := s.env
Lean.Expr.foldConsts e deps fun c deps => Id.run do
let mut deps := deps
if let some c := getDepConstName? s c then
if let some c := getDepConstName? env c then
if let some j := env.getModuleIdxFor? c then
let k := { k with isMeta := k.isMeta && !isDeclMeta' env c }
if j != i then
deps := deps.union k {j}
for indMod in s.indirectModUses[c]?.getD #[] do
for indMod in (indirectModUseExt.getState env)[c]?.getD #[] do
if s.transDeps[i]!.has k indMod then
deps := deps.union k {indMod}
return deps
@@ -309,11 +369,11 @@ where
let env := s.env
Lean.Expr.foldConsts e deps fun c deps => Id.run do
let mut deps := deps
if let some c := getDepConstName? s c then
if let some c := getDepConstName? env c then
if let some j := env.getModuleIdxFor? c then
let k := { k with isMeta := k.isMeta && !isDeclMeta' env c }
deps := addExplanation j k name c deps
for indMod in s.indirectModUses[c]?.getD #[] do
for indMod in (indirectModUseExt.getState env)[c]?.getD #[] do
if s.transDeps[i]!.has k indMod then
deps := addExplanation indMod k name (`_indirect ++ c) deps
return deps
@@ -580,7 +640,7 @@ def visitModule (pkg : Name) (srcSearchPath : SearchPath)
if toRemove.any fun imp => imp == decodeImport stx then
let pos := inputCtx.fileMap.toPosition stx.raw.getPos?.get!
println! "{path}:{pos.line}:{pos.column+1}: warning: unused import \
(use `lake shake --fix` to fix this, or `lake shake --update` to ignore)"
(use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)"
if !toAdd.isEmpty then
-- we put the insert message on the beginning of the last import line
let pos := inputCtx.fileMap.toPosition endHeader.offset
@@ -625,31 +685,76 @@ def visitModule (pkg : Name) (srcSearchPath : SearchPath)
run j
for i in toAdd do run i
/-- Convert a list of module names to a bitset of module indexes -/
def toBitset (s : State) (ns : List Name) : Bitset :=
ns.foldl (init := ) fun c name =>
match s.env.getModuleIdxFor? name with
| some i => c {i}
| none => c
local instance : Ord Import where
compare :=
let _ := @lexOrd
compareOn fun imp => (!imp.isExported, imp.module.toString)
/--
Run the shake analysis with the given arguments.
/-- The main entry point. See `help` for more information on arguments. -/
public def main (args : List String) : IO UInt32 := do
initSearchPath ( findSysroot)
-- Parse the arguments
let rec parseArgs (args : Args) : List String Args
| [] => args
| "--help" :: rest => parseArgs { args with help := true } rest
| "--keep-implied" :: rest => parseArgs { args with keepImplied := true } rest
| "--keep-prefix" :: rest => parseArgs { args with keepPrefix := true } rest
| "--keep-public" :: rest => parseArgs { args with keepPublic := true } rest
| "--add-public" :: rest => parseArgs { args with addPublic := true } rest
| "--force" :: rest => parseArgs { args with force := true } rest
| "--fix" :: rest => parseArgs { args with fix := true } rest
| "--explain" :: rest => parseArgs { args with explain := true } rest
| "--trace" :: rest => parseArgs { args with trace := true } rest
| "--gh-style" :: rest => parseArgs { args with githubStyle := true } rest
| "--" :: rest => { args with mods := args.mods ++ rest.map (·.toName) }
| other :: rest => parseArgs { args with mods := args.mods.push other.toName } rest
let args := parseArgs {} args
Assumes Lean's search path has already been properly configured.
-/
public def run (args : Args) (h : 0 < args.mods.size)
(srcSearchPath : SearchPath := {}) : IO UInt32 := do
-- Bail if `--help` is passed
if args.help then
IO.println help
IO.Process.exit 0
if !args.force then
if ( IO.Process.output { cmd := "lake", args := #["build", "--no-build"] }).exitCode != 0 then
IO.println "There are out of date oleans. Run `lake build` or `lake exe cache get` first"
IO.Process.exit 1
-- Determine default module(s) to run shake on
let defaultTargetModules : Array Name try
let (elanInstall?, leanInstall?, lakeInstall?) Lake.findInstall?
let config Lake.MonadError.runEIO <| Lake.mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
let some workspace Lake.loadWorkspace config |>.toBaseIO
| throw <| IO.userError "failed to load Lake workspace"
let defaultTargetModules := workspace.root.defaultTargets.flatMap fun target =>
if let some lib := workspace.root.findLeanLib? target then
lib.roots
else if let some exe := workspace.root.findLeanExe? target then
#[exe.config.root]
else
#[]
pure defaultTargetModules
catch _ =>
pure #[]
let srcSearchPath getSrcSearchPath
-- the list of root modules
let mods := args.mods
let mods := if args.mods.isEmpty then defaultTargetModules else args.mods
-- Only submodules of `pkg` will be edited or have info reported on them
let pkg := mods[0].getRoot
let pkg := mods[0]!.components.head!
-- Load all the modules
let imps := mods.map ({ module := · })
let (_, s) importModulesCore imps (isExported := true) |>.run
let s := s.markAllExported
let mut env finalizeImport s (isModule := true) imps {} (leakEnv := true) (loadExts := false)
if env.header.moduleData.any (!·.isModule) then
throw <| .userError "`lake shake` only works with `module`s currently"
let mut env finalizeImport s (isModule := true) imps {} (leakEnv := false) (loadExts := false)
-- the one env ext we want to initialize
let is := indirectModUseExt.toEnvExtension.getState env
let newState indirectModUseExt.addImportedFn is.importedEntries { env := env, opts := {} }

View File

@@ -3,3 +3,9 @@ name = "scripts"
[[lean_exe]]
name = "modulize"
root = "Modulize"
[[lean_exe]]
name = "shake"
root = "Shake"
# needed by `Lake.loadWorkspace`
supportInterpreter = true

View File

@@ -40,10 +40,6 @@ find_program(LLD_PATH lld)
if(LLD_PATH)
string(APPEND LEAN_EXTRA_LINKER_FLAGS_DEFAULT " -fuse-ld=lld")
endif()
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
# Create space in install names so they can be patched later in Nix.
string(APPEND LEAN_EXTRA_LINKER_FLAGS_DEFAULT " -headerpad_max_install_names")
endif()
set(LEAN_EXTRA_LINKER_FLAGS ${LEAN_EXTRA_LINKER_FLAGS_DEFAULT} CACHE STRING "Additional flags used by the linker")
set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler. Unlike `CMAKE_CXX_FLAGS`, these will not be used to build e.g. cadical.")
@@ -456,14 +452,11 @@ if(LLVM AND ${STAGE} GREATER 0)
message(VERBOSE "leanshared linker flags: '${LEANSHARED_LINKER_FLAGS}' | lean extra cxx flags '${CMAKE_CXX_FLAGS}'")
endif()
# We always strip away unused declarations to reduce binary sizes as the time cost is small and the
# potential benefit can be huge, especially when stripping `meta import`s.
# get rid of unused parts of C++ stdlib
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
string(APPEND LEANC_EXTRA_CC_FLAGS " -fdata-sections -ffunction-sections")
string(APPEND LEAN_EXTRA_LINKER_FLAGS " -Wl,-dead_strip")
string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-dead_strip")
elseif(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
string(APPEND LEANC_EXTRA_CC_FLAGS " -fdata-sections -ffunction-sections")
string(APPEND LEAN_EXTRA_LINKER_FLAGS " -Wl,--gc-sections")
string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,--gc-sections")
endif()
if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
@@ -638,9 +631,6 @@ if(${STAGE} GREATER 1)
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/libleanrt.a" "${CMAKE_BINARY_DIR}/lib/lean/libleanrt.a"
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/libleancpp.a" "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a"
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/temp/libleancpp_1.a" "${CMAKE_BINARY_DIR}/lib/temp/libleancpp_1.a")
add_dependencies(leanrt_initial-exec copy-leancpp)
add_dependencies(leanrt copy-leancpp)
add_dependencies(leancpp_1 copy-leancpp)
add_dependencies(leancpp copy-leancpp)
if(LLVM)
add_custom_target(copy-lean-h-bc

View File

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Init.Prelude
public import Init.Notation
@@ -37,7 +38,6 @@ public import Init.Omega
public import Init.MacroTrace
public import Init.Grind
public import Init.GrindInstances
public import Init.Sym
public import Init.While
public import Init.Syntax
public import Init.Internal

View File

@@ -13,10 +13,6 @@ public import Init.SizeOf
public section
set_option linter.missingDocs true -- keep it documented
-- BEq instance for Option defined here so it's available early in the import chain
-- (before Init.Grind.Config and Init.MetaTypes which need BEq (Option Nat))
deriving instance BEq for Option
@[expose] section
universe u v w
@@ -1565,10 +1561,6 @@ instance {p q : Prop} [d : Decidable (p ↔ q)] : Decidable (p = q) :=
| isTrue h => isTrue (propext h)
| isFalse h => isFalse fun heq => h (heq Iff.rfl)
/-- Helper theorem for proving injectivity theorems -/
theorem Lean.injEq_helper {P Q R : Prop} :
(P Q R) (P Q R) := by intro h h₁,h₂; exact h h₁ h₂
gen_injective_theorems% Array
gen_injective_theorems% BitVec
gen_injective_theorems% ByteArray

View File

@@ -159,17 +159,4 @@ theorem setWidth_neg_of_le {x : BitVec v} (h : w ≤ v) : BitVec.setWidth w (-x)
omega
omega
@[induction_eliminator, elab_as_elim]
theorem cons_induction {motive : (w : Nat) BitVec w Prop} (nil : motive 0 .nil)
(cons : {w : Nat} (b : Bool) (bv : BitVec w), motive w bv motive (w + 1) (.cons b bv)) :
{w : Nat} (x : BitVec w), motive w x := by
intros w x
induction w
case zero =>
simp only [BitVec.eq_nil x, nil]
case succ wl ih =>
rw [ cons_msb_setWidth x]
apply cons
apply ih
end BitVec

View File

@@ -3362,26 +3362,6 @@ theorem extractLsb'_concat {x : BitVec (w + 1)} {y : Bool} :
· simp
· simp [show i - 1 < t by omega]
theorem concat_extractLsb'_getLsb {x : BitVec (w + 1)} :
BitVec.concat (x.extractLsb' 1 w) (x.getLsb 0) = x := by
ext i hw
by_cases h : i = 0
· simp [h]
· simp [h, hw, show (1 + (i - 1)) = i by omega, getElem_concat]
@[elab_as_elim]
theorem concat_induction {motive : (w : Nat) BitVec w Prop} (nil : motive 0 .nil)
(concat : {w : Nat} (bv : BitVec w) (b : Bool), motive w bv motive (w + 1) (bv.concat b)) :
{w : Nat} (x : BitVec w), motive w x := by
intros w x
induction w
case zero =>
simp only [BitVec.eq_nil x, nil]
case succ wl ih =>
rw [ concat_extractLsb'_getLsb (x := x)]
apply concat
apply ih
/-! ### shiftConcat -/
@[grind =]
@@ -6403,6 +6383,73 @@ theorem cpopNatRec_add {x : BitVec w} {acc n : Nat} :
x.cpopNatRec n (acc + acc') = x.cpopNatRec n acc + acc' := by
rw [cpopNatRec_eq (acc := acc + acc'), cpopNatRec_eq (acc := acc), Nat.add_assoc]
theorem cpopNatRec_le {x : BitVec w} (n : Nat) :
x.cpopNatRec n acc acc + n := by
induction n generalizing acc
· case zero =>
simp
· case succ n ihn =>
have : (x.getLsbD n).toNat 1 := by cases x.getLsbD n <;> simp
specialize ihn (acc := acc + (x.getLsbD n).toNat)
simp
omega
@[simp]
theorem cpopNatRec_of_le {x : BitVec w} (k n : Nat) (hn : w n) :
x.cpopNatRec (n + k) acc = x.cpopNatRec n acc := by
induction k
· case zero =>
simp
· case succ k ihk =>
simp [show n + (k + 1) = (n + k) + 1 by omega, ihk, show w n + k by omega]
theorem cpopNatRec_zero_le (x : BitVec w) (n : Nat) :
x.cpopNatRec n 0 w := by
induction n
· case zero =>
simp
· case succ n ihn =>
by_cases hle : n w
· by_cases hx : x.getLsbD n
· have := cpopNatRec_le (x := x) (acc := 1) (by omega)
have := lt_of_getLsbD hx
simp [hx]
omega
· have := cpopNatRec_le (x := x) (acc := 0) (by omega)
simp [hx]
omega
· simp [show w n by omega]
omega
@[simp]
theorem cpopNatRec_allOnes (h : n w) :
(allOnes w).cpopNatRec n acc = acc + n := by
induction n
· case zero =>
simp
· case succ n ihn =>
specialize ihn (by omega)
simp [show n < w by omega, ihn,
cpopNatRec_add (acc := acc) (acc' := 1)]
omega
@[simp]
theorem cpop_allOnes :
(allOnes w).cpop = BitVec.ofNat w w := by
simp [cpop, cpopNatRec_allOnes]
@[simp]
theorem cpop_zero :
(0#w).cpop = 0#w := by
simp [cpop]
theorem toNat_cpop_le (x : BitVec w) :
x.cpop.toNat w := by
have hlt := Nat.lt_two_pow_self (n := w)
have hle := cpopNatRec_zero_le (x := x) (n := w)
simp only [cpop, toNat_ofNat, ge_iff_le]
rw [Nat.mod_eq_of_lt (by omega)]
exact hle
@[simp]
theorem cpopNatRec_cons_of_le {x : BitVec w} {b : Bool} (hn : n w) :
@@ -6428,68 +6475,6 @@ theorem cpopNatRec_cons_of_lt {x : BitVec w} {b : Bool} (hn : w < n) :
· simp [show w = n by omega, getElem_cons,
cpopNatRec_add (acc := acc) (acc' := b.toNat), Nat.add_comm]
theorem cpopNatRec_le {x : BitVec w} (n : Nat) :
x.cpopNatRec n acc acc + n := by
induction n generalizing acc
· case zero =>
simp
· case succ n ihn =>
have : (x.getLsbD n).toNat 1 := by cases x.getLsbD n <;> simp
specialize ihn (acc := acc + (x.getLsbD n).toNat)
simp
omega
@[simp]
theorem cpopNatRec_of_le {x : BitVec w} (k n : Nat) (hn : w n) :
x.cpopNatRec (n + k) acc = x.cpopNatRec n acc := by
induction k
· case zero =>
simp
· case succ k ihk =>
simp [show n + (k + 1) = (n + k) + 1 by omega, ihk, show w n + k by omega]
@[simp]
theorem cpopNatRec_allOnes (h : n w) :
(allOnes w).cpopNatRec n acc = acc + n := by
induction n
· case zero =>
simp
· case succ n ihn =>
specialize ihn (by omega)
simp [show n < w by omega, ihn,
cpopNatRec_add (acc := acc) (acc' := 1)]
omega
@[simp]
theorem cpop_allOnes :
(allOnes w).cpop = BitVec.ofNat w w := by
simp [cpop, cpopNatRec_allOnes]
@[simp]
theorem cpop_zero :
(0#w).cpop = 0#w := by
simp [cpop]
theorem cpopNatRec_zero_le (x : BitVec w) (n : Nat) :
x.cpopNatRec n 0 w := by
induction x
· case nil => simp
· case cons w b bv ih =>
by_cases hle : n w
· have := cpopNatRec_cons_of_le (b := b) (x := bv) (n := n) (acc := 0) hle
omega
· rw [cpopNatRec_cons_of_lt (by omega)]
have : b.toNat 1 := by cases b <;> simp
omega
theorem toNat_cpop_le (x : BitVec w) :
x.cpop.toNat w := by
have hlt := Nat.lt_two_pow_self (n := w)
have hle := cpopNatRec_zero_le (x := x) (n := w)
simp only [cpop, toNat_ofNat, ge_iff_le]
rw [Nat.mod_eq_of_lt (by omega)]
exact hle
theorem cpopNatRec_concat_of_lt {x : BitVec w} {b : Bool} (hn : 0 < n) :
(concat x b).cpopNatRec n acc = b.toNat + x.cpopNatRec (n - 1) acc := by
induction n generalizing acc
@@ -6587,12 +6572,12 @@ theorem cpop_cast (x : BitVec w) (h : w = v) :
@[simp]
theorem toNat_cpop_append {x : BitVec w} {y : BitVec u} :
(x ++ y).cpop.toNat = x.cpop.toNat + y.cpop.toNat := by
induction x generalizing y
· case nil =>
simp
· case cons w b bv ih =>
simp [cons_append, ih]
omega
induction w generalizing u
· case zero =>
simp [cpop]
· case succ w ihw =>
rw [ cons_msb_setWidth x, toNat_cpop_cons, cons_append, cpop_cast, toNat_cast,
toNat_cpop_cons, ihw, Nat.add_assoc]
theorem cpop_append {x : BitVec w} {y : BitVec u} :
(x ++ y).cpop = x.cpop.setWidth (w + u) + y.cpop.setWidth (w + u) := by
@@ -6603,14 +6588,4 @@ theorem cpop_append {x : BitVec w} {y : BitVec u} :
simp only [toNat_cpop_append, toNat_add, toNat_setWidth, Nat.add_mod_mod, Nat.mod_add_mod]
rw [Nat.mod_eq_of_lt (by omega)]
theorem toNat_cpop_not {x : BitVec w} :
(~~~x).cpop.toNat = w - x.cpop.toNat := by
induction x
· case nil =>
simp
· case cons b x ih =>
have := toNat_cpop_le x
cases b
<;> (simp [ih]; omega)
end BitVec

View File

@@ -148,7 +148,6 @@ theorem Subarray.copy_eq_toArray {s : Subarray α} :
s.copy = s.toArray :=
(rfl)
@[grind =]
theorem Subarray.sliceToArray_eq_toArray {s : Subarray α} :
Slice.toArray s = s.toArray :=
(rfl)

View File

@@ -119,13 +119,6 @@ public theorem forIn_toList {α : Type u} {s : Subarray α}
ForIn.forIn s.toList init f = ForIn.forIn s init f :=
Slice.forIn_toList
@[grind =]
public theorem forIn_eq_forIn_toList {α : Type u} {s : Subarray α}
{m : Type v Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ}
{f : α γ m (ForInStep γ)} :
ForIn.forIn s init f = ForIn.forIn s.toList init f :=
forIn_toList.symm
@[simp]
public theorem forIn_toArray {α : Type u} {s : Subarray α}
{m : Type v Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ}
@@ -174,22 +167,22 @@ public theorem Array.toSubarray_eq_min {xs : Array α} {lo hi : Nat} :
simp only [Array.toSubarray]
split <;> split <;> simp [Nat.min_eq_right (Nat.le_of_not_ge _), *]
@[simp, grind =]
@[simp]
public theorem Array.array_toSubarray {xs : Array α} {lo hi : Nat} :
(xs.toSubarray lo hi).array = xs := by
simp [toSubarray_eq_min, Subarray.array]
@[simp, grind =]
@[simp]
public theorem Array.start_toSubarray {xs : Array α} {lo hi : Nat} :
(xs.toSubarray lo hi).start = min lo (min hi xs.size) := by
simp [toSubarray_eq_min, Subarray.start]
@[simp, grind =]
@[simp]
public theorem Array.stop_toSubarray {xs : Array α} {lo hi : Nat} :
(xs.toSubarray lo hi).stop = min hi xs.size := by
simp [toSubarray_eq_min, Subarray.stop]
public theorem Subarray.toList_eq {xs : Subarray α} :
theorem Subarray.toList_eq {xs : Subarray α} :
xs.toList = (xs.array.extract xs.start xs.stop).toList := by
let aslice := xs
obtain array, start, stop, h₁, h₂ := xs
@@ -206,46 +199,45 @@ public theorem Subarray.toList_eq {xs : Subarray α} :
simp [Subarray.array, Subarray.start, Subarray.stop]
simp [this, ListSlice.toList_eq, lslice]
@[grind =]
public theorem Subarray.size_eq {xs : Subarray α} :
xs.size = xs.stop - xs.start := by
simp [Subarray.size]
@[simp, grind =]
@[simp]
public theorem Subarray.toArray_toList {xs : Subarray α} :
xs.toList.toArray = xs.toArray := by
simp [Std.Slice.toList, Subarray.toArray, Std.Slice.toArray]
@[simp, grind =]
@[simp]
public theorem Subarray.toList_toArray {xs : Subarray α} :
xs.toArray.toList = xs.toList := by
simp [Std.Slice.toList, Subarray.toArray, Std.Slice.toArray]
@[simp, grind =]
@[simp]
public theorem Subarray.length_toList {xs : Subarray α} :
xs.toList.length = xs.size := by
have : xs.start xs.stop := xs.internalRepresentation.start_le_stop
have : xs.stop xs.array.size := xs.internalRepresentation.stop_le_array_size
simp [Subarray.toList_eq, Subarray.size]; omega
@[simp, grind =]
@[simp]
public theorem Subarray.size_toArray {xs : Subarray α} :
xs.toArray.size = xs.size := by
simp [ Subarray.toArray_toList, Subarray.size, Slice.size, SliceSize.size, start, stop]
namespace Array
@[simp, grind =]
@[simp]
public theorem array_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo...hi].array = xs := by
simp [Std.Rco.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
@[simp, grind =]
@[simp]
public theorem start_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo...hi].start = min lo (min hi xs.size) := by
simp [Std.Rco.Sliceable.mkSlice]
@[simp, grind =]
@[simp]
public theorem stop_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo...hi].stop = min hi xs.size := by
simp [Std.Rco.Sliceable.mkSlice]
@@ -254,14 +246,14 @@ public theorem mkSlice_rco_eq_mkSlice_rco_min {xs : Array α} {lo hi : Nat} :
xs[lo...hi] = xs[(min lo (min hi xs.size))...(min hi xs.size)] := by
simp [Std.Rco.Sliceable.mkSlice, Array.toSubarray_eq_min]
@[simp, grind =]
@[simp]
public theorem toList_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
rw [List.take_eq_take_min, List.drop_eq_drop_min]
simp [Std.Rco.Sliceable.mkSlice, Subarray.toList_eq, List.take_drop,
Nat.add_sub_of_le (Nat.min_le_right _ _)]
@[simp, grind =]
@[simp]
public theorem toArray_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo...hi].toArray = xs.extract lo hi := by
simp only [ Subarray.toArray_toList, toList_mkSlice_rco]
@@ -274,12 +266,12 @@ public theorem toArray_mkSlice_rco {xs : Array α} {lo hi : Nat} :
· simp; omega
· simp; omega
@[simp, grind =]
@[simp]
public theorem size_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo...hi].size = min hi xs.size - lo := by
simp [ Subarray.length_toList]
@[simp, grind =]
@[simp]
public theorem mkSlice_rcc_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo...=hi] = xs[lo...(hi + 1)] := by
simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -288,7 +280,7 @@ public theorem mkSlice_rcc_eq_mkSlice_rco_min {xs : Array α} {lo hi : Nat} :
xs[lo...=hi] = xs[(min lo (min (hi + 1) xs.size))...(min (hi + 1) xs.size)] := by
simp [mkSlice_rco_eq_mkSlice_rco_min]
@[simp, grind =]
@[simp]
public theorem array_mkSlice_rcc {xs : Array α} {lo hi : Nat} :
xs[lo...=hi].array = xs := by
simp [Std.Rcc.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
@@ -333,7 +325,7 @@ public theorem stop_mkSlice_rci {xs : Array α} {lo : Nat} :
xs[lo...*].stop = xs.size := by
simp [Std.Rci.Sliceable.mkSlice, Std.Rci.HasRcoIntersection.intersection]
@[simp, grind =]
@[simp]
public theorem mkSlice_rci_eq_mkSlice_rco {xs : Array α} {lo : Nat} :
xs[lo...*] = xs[lo...xs.size] := by
simp [Std.Rci.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice, Std.Rci.HasRcoIntersection.intersection]
@@ -352,7 +344,7 @@ public theorem toArray_mkSlice_rci {xs : Array α} {lo : Nat} :
xs[lo...*].toArray = xs.extract lo := by
simp
@[simp, grind =]
@[simp]
public theorem size_mkSlice_rci {xs : Array α} {lo : Nat} :
xs[lo...*].size = xs.size - lo := by
simp [ Subarray.length_toList]
@@ -372,7 +364,7 @@ public theorem stop_mkSlice_roo {xs : Array α} {lo hi : Nat} :
xs[lo<...hi].stop = min hi xs.size := by
simp [Std.Roo.Sliceable.mkSlice]
@[simp, grind =]
@[simp]
public theorem mkSlice_roo_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo<...hi] = xs[(lo + 1)...hi] := by
simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -416,11 +408,6 @@ public theorem mkSlice_roc_eq_mkSlice_roo {xs : Array α} {lo hi : Nat} :
xs[lo<...=hi] = xs[lo<...(hi + 1)] := by
simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice]
@[grind =]
public theorem mkSlice_roc_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} :
xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
simp
public theorem mkSlice_roc_eq_mkSlice_roo_min {xs : Array α} {lo hi : Nat} :
xs[lo<...=hi] = xs[(min (lo + 1) (min (hi + 1) xs.size))...(min (hi + 1) xs.size)] := by
simp [mkSlice_rco_eq_mkSlice_rco_min]
@@ -465,11 +452,6 @@ public theorem mkSlice_roi_eq_mkSlice_roo {xs : Array α} {lo : Nat} :
xs[lo<...*] = xs[lo<...xs.size] := by
simp [mkSlice_rci_eq_mkSlice_rco]
@[grind =]
public theorem mkSlice_roi_eq_mkSlice_rco {xs : Array α} {lo : Nat} :
xs[lo<...*] = xs[(lo + 1)...xs.size] := by
simp [mkSlice_rci_eq_mkSlice_rco]
public theorem mkSlice_roi_eq_mkSlice_roo_min {xs : Array α} {lo : Nat} :
xs[lo<...*] = xs[(min (lo + 1) xs.size)...xs.size] := by
simp [mkSlice_rco_eq_mkSlice_rco_min]
@@ -494,7 +476,7 @@ public theorem array_mkSlice_rio {xs : Array α} {hi : Nat} :
xs[*...hi].array = xs := by
simp [Std.Rio.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
@[simp, grind =]
@[simp]
public theorem start_mkSlice_rio {xs : Array α} {hi : Nat} :
xs[*...hi].start = 0 := by
simp [Std.Rio.Sliceable.mkSlice]
@@ -504,7 +486,7 @@ public theorem stop_mkSlice_rio {xs : Array α} {hi : Nat} :
xs[*...hi].stop = min hi xs.size := by
simp [Std.Rio.Sliceable.mkSlice]
@[simp, grind =]
@[simp]
public theorem mkSlice_rio_eq_mkSlice_rco {xs : Array α} {hi : Nat} :
xs[*...hi] = xs[0...hi] := by
simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -533,7 +515,7 @@ public theorem array_mkSlice_ric {xs : Array α} {hi : Nat} :
xs[*...=hi].array = xs := by
simp [Std.Ric.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
@[simp, grind =]
@[simp]
public theorem start_mkSlice_ric {xs : Array α} {hi : Nat} :
xs[*...=hi].start = 0 := by
simp [Std.Ric.Sliceable.mkSlice]
@@ -548,11 +530,6 @@ public theorem mkSlice_ric_eq_mkSlice_rio {xs : Array α} {hi : Nat} :
xs[*...=hi] = xs[*...(hi + 1)] := by
simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice]
@[grind =]
public theorem mkSlice_ric_eq_mkSlice_rco {xs : Array α} {hi : Nat} :
xs[*...=hi] = xs[0...(hi + 1)] := by
simp
public theorem mkSlice_ric_eq_mkSlice_rio_min {xs : Array α} {hi : Nat} :
xs[*...=hi] = xs[*...(min (hi + 1) xs.size)] := by
simp [mkSlice_rco_eq_mkSlice_rco_min]
@@ -582,16 +559,11 @@ public theorem mkSlice_rii_eq_mkSlice_rio {xs : Array α} :
xs[*...*] = xs[*...xs.size] := by
simp [mkSlice_rci_eq_mkSlice_rco]
@[grind =]
public theorem mkSlice_rii_eq_mkSlice_rco {xs : Array α} :
xs[*...*] = xs[0...xs.size] := by
simp
public theorem mkSlice_rii_eq_mkSlice_rio_min {xs : Array α} :
xs[*...*] = xs[*...xs.size] := by
simp [mkSlice_rco_eq_mkSlice_rco_min]
@[simp, grind =]
@[simp]
public theorem toList_mkSlice_rii {xs : Array α} :
xs[*...*].toList = xs.toList := by
rw [mkSlice_rii_eq_mkSlice_rci, toList_mkSlice_rci, List.drop_zero]
@@ -601,7 +573,7 @@ public theorem toArray_mkSlice_rii {xs : Array α} :
xs[*...*].toArray = xs := by
simp
@[simp, grind =]
@[simp]
public theorem size_mkSlice_rii {xs : Array α} :
xs[*...*].size = xs.size := by
simp [ Subarray.length_toList]
@@ -611,12 +583,12 @@ public theorem array_mkSlice_rii {xs : Array α} :
xs[*...*].array = xs := by
simp
@[simp, grind =]
@[simp]
public theorem start_mkSlice_rii {xs : Array α} :
xs[*...*].start = 0 := by
simp
@[simp, grind =]
@[simp]
public theorem stop_mkSlice_rii {xs : Array α} :
xs[*...*].stop = xs.size := by
simp [Std.Rii.Sliceable.mkSlice]
@@ -627,7 +599,7 @@ section SubarraySlices
namespace Subarray
@[simp, grind =]
@[simp]
public theorem toList_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
simp only [Std.Rco.Sliceable.mkSlice, Std.Rco.HasRcoIntersection.intersection, toList_eq,
@@ -636,12 +608,12 @@ public theorem toList_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
rw [Nat.add_sub_cancel' (by omega)]
simp [Subarray.size, Array.length_toList, List.take_eq_take_min, Nat.add_comm xs.start]
@[simp, grind =]
@[simp]
public theorem toArray_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
xs[lo...hi].toArray = xs.toArray.extract lo hi := by
simp [ Subarray.toArray_toList, List.drop_take]
@[simp, grind =]
@[simp]
public theorem mkSlice_rcc_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
xs[lo...=hi] = xs[lo...(hi + 1)] := by
simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
@@ -657,7 +629,7 @@ public theorem toArray_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
xs[lo...=hi].toArray = xs.toArray.extract lo (hi + 1) := by
simp
@[simp, grind =]
@[simp]
public theorem mkSlice_rci_eq_mkSlice_rco {xs : Subarray α} {lo : Nat} :
xs[lo...*] = xs[lo...xs.size] := by
simp [Std.Rci.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
@@ -679,17 +651,12 @@ public theorem mkSlice_roc_eq_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice,
Std.Roc.HasRcoIntersection.intersection, Std.Roo.HasRcoIntersection.intersection]
@[simp, grind =]
@[simp]
public theorem mkSlice_roo_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
xs[lo<...hi] = xs[(lo + 1)...hi] := by
simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
Std.Roo.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
@[grind =]
public theorem mkSlice_roc_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
simp
@[simp]
public theorem toList_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
xs[lo<...hi].toList = (xs.toList.take hi).drop (lo + 1) := by
@@ -703,7 +670,8 @@ public theorem toArray_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
@[simp]
public theorem mkSlice_roc_eq_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
xs[lo<...=hi] = xs[(lo + 1)...=hi] := by
simp
simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
Std.Roc.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
@[simp]
public theorem toList_mkSlice_roc {xs : Subarray α} {lo hi : Nat} :
@@ -721,11 +689,6 @@ public theorem mkSlice_roi_eq_mkSlice_rci {xs : Subarray α} {lo : Nat} :
simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice,
Std.Roi.HasRcoIntersection.intersection, Std.Rci.HasRcoIntersection.intersection]
@[grind =]
public theorem mkSlice_roi_eq_mkSlice_rco {xs : Subarray α} {lo : Nat} :
xs[lo<...*] = xs[(lo + 1)...xs.size] := by
simp
@[simp]
public theorem toList_mkSlice_roi {xs : Subarray α} {lo : Nat} :
xs[lo<...*].toList = xs.toList.drop (lo + 1) := by
@@ -742,17 +705,12 @@ public theorem mkSlice_ric_eq_mkSlice_rio {xs : Subarray α} {hi : Nat} :
simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice,
Std.Ric.HasRcoIntersection.intersection, Std.Rio.HasRcoIntersection.intersection]
@[simp, grind =]
@[simp]
public theorem mkSlice_rio_eq_mkSlice_rco {xs : Subarray α} {hi : Nat} :
xs[*...hi] = xs[0...hi] := by
simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
Std.Rio.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
@[grind =]
public theorem mkSlice_ric_eq_mkSlice_rco {xs : Subarray α} {hi : Nat} :
xs[*...=hi] = xs[0...(hi + 1)] := by
simp
@[simp]
public theorem toList_mkSlice_rio {xs : Subarray α} {hi : Nat} :
xs[*...hi].toList = xs.toList.take hi := by
@@ -779,7 +737,7 @@ public theorem toArray_mkSlice_ric {xs : Subarray α} {hi : Nat} :
xs[*...=hi].toArray = xs.toArray.extract 0 (hi + 1) := by
simp
@[simp, grind =]
@[simp]
public theorem mkSlice_rii {xs : Subarray α} :
xs[*...*] = xs := by
simp [Std.Rii.Sliceable.mkSlice]

View File

@@ -47,28 +47,21 @@ public theorem toList_eq {xs : ListSlice α} :
simp only [Std.Slice.toList, toList_internalIter]
rfl
@[simp, grind =]
public theorem toArray_toList {xs : ListSlice α} :
xs.toList.toArray = xs.toArray := by
simp [Std.Slice.toArray, Std.Slice.toList]
@[simp, grind =]
public theorem toList_toArray {xs : ListSlice α} :
xs.toArray.toList = xs.toList := by
simp [Std.Slice.toArray, Std.Slice.toList]
@[simp, grind =]
@[simp]
public theorem length_toList {xs : ListSlice α} :
xs.toList.length = xs.size := by
simp [ListSlice.toList_eq, Std.Slice.size, Std.Slice.SliceSize.size, Iter.length_toList_eq_count,
toList_internalIter]; rfl
@[grind =]
public theorem size_eq_length_toList {xs : ListSlice α} :
xs.size = xs.toList.length :=
length_toList.symm
@[simp, grind =]
@[simp]
public theorem size_toArray {xs : ListSlice α} :
xs.toArray.size = xs.size := by
simp [ ListSlice.toArray_toList]
@@ -77,7 +70,7 @@ end ListSlice
namespace List
@[simp, grind =]
@[simp]
public theorem toList_mkSlice_rco {xs : List α} {lo hi : Nat} :
xs[lo...hi].toList = (xs.take hi).drop lo := by
rw [List.take_eq_take_min, List.drop_eq_drop_min]
@@ -88,17 +81,17 @@ public theorem toList_mkSlice_rco {xs : List α} {lo hi : Nat} :
· have : min hi xs.length lo := by omega
simp [h, Nat.min_eq_right this]
@[simp, grind =]
@[simp]
public theorem toArray_mkSlice_rco {xs : List α} {lo hi : Nat} :
xs[lo...hi].toArray = ((xs.take hi).drop lo).toArray := by
simp [ ListSlice.toArray_toList]
@[simp, grind =]
@[simp]
public theorem size_mkSlice_rco {xs : List α} {lo hi : Nat} :
xs[lo...hi].size = min hi xs.length - lo := by
simp [ ListSlice.length_toList]
@[simp, grind =]
@[simp]
public theorem mkSlice_rcc_eq_mkSlice_rco {xs : List α} {lo hi : Nat} :
xs[lo...=hi] = xs[lo...(hi + 1)] := by
simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -129,22 +122,12 @@ public theorem toArray_mkSlice_rci {xs : List α} {lo : Nat} :
xs[lo...*].toArray = (xs.drop lo).toArray := by
simp [ ListSlice.toArray_toList]
@[grind =]
public theorem toList_mkSlice_rci_eq_toList_mkSlice_rco {xs : List α} {lo : Nat} :
xs[lo...*].toList = xs[lo...xs.length].toList := by
simp
@[grind =]
public theorem toArray_mkSlice_rci_eq_toArray_mkSlice_rco {xs : List α} {lo : Nat} :
xs[lo...*].toArray = xs[lo...xs.length].toArray := by
simp
@[simp]
public theorem size_mkSlice_rci {xs : List α} {lo : Nat} :
xs[lo...*].size = xs.length - lo := by
simp [ ListSlice.length_toList]
@[simp, grind =]
@[simp]
public theorem mkSlice_roo_eq_mkSlice_rco {xs : List α} {lo hi : Nat} :
xs[lo<...hi] = xs[(lo + 1)...hi] := by
simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -169,11 +152,6 @@ public theorem mkSlice_roc_eq_mkSlice_roo {xs : List α} {lo hi : Nat} :
xs[lo<...=hi] = xs[lo<...(hi + 1)] := by
simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice]
@[simp, grind =]
public theorem mkSlice_roc_eq_mkSlice_rco {xs : List α} {lo hi : Nat} :
xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
simp
@[simp]
public theorem toList_mkSlice_roc {xs : List α} {lo hi : Nat} :
xs[lo<...=hi].toList = (xs.take (hi + 1)).drop (lo + 1) := by
@@ -189,27 +167,11 @@ public theorem size_mkSlice_roc {xs : List α} {lo hi : Nat} :
xs[lo<...=hi].size = min (hi + 1) xs.length - (lo + 1) := by
simp [ ListSlice.length_toList]
@[simp, grind =]
@[simp]
public theorem mkSlice_roi_eq_mkSlice_rci {xs : List α} {lo : Nat} :
xs[lo<...*] = xs[(lo + 1)...*] := by
simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice]
public theorem toList_mkSlice_roi_eq_toList_mkSlice_roo {xs : List α} {lo : Nat} :
xs[lo<...*].toList = xs[lo<...xs.length].toList := by
simp
public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_roo {xs : List α} {lo : Nat} :
xs[lo<...*].toArray = xs[lo<...xs.length].toArray := by
simp
public theorem toList_mkSlice_roi_eq_toList_mkSlice_rco {xs : List α} {lo : Nat} :
xs[lo<...*].toList = xs[(lo + 1)...xs.length].toList := by
simp
public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_rco {xs : List α} {lo : Nat} :
xs[lo<...*].toArray = xs[(lo + 1)...xs.length].toArray := by
simp
@[simp]
public theorem toList_mkSlice_roi {xs : List α} {lo : Nat} :
xs[lo<...*].toList = xs.drop (lo + 1) := by
@@ -225,7 +187,7 @@ public theorem size_mkSlice_roi {xs : List α} {lo : Nat} :
xs[lo<...*].size = xs.length - (lo + 1) := by
simp [ ListSlice.length_toList]
@[simp, grind =]
@[simp]
public theorem mkSlice_rio_eq_mkSlice_rco {xs : List α} {hi : Nat} :
xs[*...hi] = xs[0...hi] := by
simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -250,11 +212,6 @@ public theorem mkSlice_ric_eq_mkSlice_rio {xs : List α} {hi : Nat} :
xs[*...=hi] = xs[*...(hi + 1)] := by
simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice]
@[grind =]
public theorem mkSlice_ric_eq_mkSlice_rco {xs : List α} {hi : Nat} :
xs[*...=hi] = xs[0...(hi + 1)] := by
simp
@[simp]
public theorem toList_mkSlice_ric {xs : List α} {hi : Nat} :
xs[*...=hi].toList = xs.take (hi + 1) := by
@@ -270,19 +227,11 @@ public theorem size_mkSlice_ric {xs : List α} {hi : Nat} :
xs[*...=hi].size = min (hi + 1) xs.length := by
simp [ ListSlice.length_toList]
@[simp, grind =]
@[simp]
public theorem mkSlice_rii_eq_mkSlice_rci {xs : List α} :
xs[*...*] = xs[0...*] := by
simp [Std.Rii.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice]
public theorem toList_mkSlice_rii_eq_toList_mkSlice_rco {xs : List α} :
xs[*...*].toList = xs[0...xs.length].toList := by
simp
public theorem toArray_mkSlice_rii_eq_toArray_mkSlice_rco {xs : List α} :
xs[*...*].toArray = xs[0...xs.length].toArray := by
simp
@[simp]
public theorem toList_mkSlice_rii {xs : List α} :
xs[*...*].toList = xs := by
@@ -304,7 +253,7 @@ section ListSubslices
namespace ListSlice
@[simp, grind =]
@[simp]
public theorem toList_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
simp only [instSliceableListSliceNat_1, List.toList_mkSlice_rco, ListSlice.toList_eq (xs := xs)]
@@ -313,12 +262,12 @@ public theorem toList_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
· simp
· simp [List.take_take, Nat.min_comm]
@[simp, grind =]
@[simp]
public theorem toArray_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
xs[lo...hi].toArray = xs.toArray.extract lo hi := by
simp [ toArray_toList, List.drop_take]
@[simp, grind =]
@[simp]
public theorem mkSlice_rcc_eq_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
xs[lo...=hi] = xs[lo...(hi + 1)] := by
simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -346,19 +295,9 @@ public theorem toArray_mkSlice_rci {xs : ListSlice α} {lo : Nat} :
xs[lo...*].toArray = xs.toArray.extract lo := by
simp only [ toArray_toList, toList_mkSlice_rci]
rw (occs := [1]) [ List.take_length (l := List.drop lo xs.toList)]
simp [- toArray_toList]
@[grind =]
public theorem toList_mkSlice_rci_eq_toList_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
xs[lo...*].toList = xs[lo...xs.size].toList := by
simp [ length_toList, - Slice.length_toList_eq_size]
@[grind =]
public theorem toArray_mkSlice_rci_eq_toArray_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
xs[lo...*].toArray = xs[lo...xs.size].toArray := by
simp
@[simp, grind =]
@[simp]
public theorem mkSlice_roo_eq_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
xs[lo<...hi] = xs[(lo + 1)...hi] := by
simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -383,11 +322,6 @@ public theorem mkSlice_roc_eq_mkSlice_rcc {xs : ListSlice α} {lo hi : Nat} :
xs[lo<...=hi] = xs[(lo + 1)...=hi] := by
simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@[simp, grind =]
public theorem mkSlice_roc_eq_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@[simp]
public theorem toList_mkSlice_roc {xs : ListSlice α} {lo hi : Nat} :
xs[lo<...=hi].toList = (xs.toList.take (hi + 1)).drop (lo + 1) := by
@@ -398,28 +332,11 @@ public theorem toArray_mkSlice_roc {xs : ListSlice α} {lo hi : Nat} :
xs[lo<...=hi].toArray = xs.toArray.extract (lo + 1) (hi + 1) := by
simp [ toArray_toList, List.drop_take]
@[simp, grind =]
@[simp]
public theorem mkSlice_roi_eq_mkSlice_rci {xs : ListSlice α} {lo : Nat} :
xs[lo<...*] = xs[(lo + 1)...*] := by
simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice]
public theorem toList_mkSlice_roi_eq_toList_mkSlice_roo {xs : ListSlice α} {lo : Nat} :
xs[lo<...*].toList = xs[lo<...xs.size].toList := by
simp [ length_toList, - Slice.length_toList_eq_size]
public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_roo {xs : ListSlice α} {lo : Nat} :
xs[lo<...*].toArray = xs[lo<...xs.size].toArray := by
simp only [mkSlice_roi_eq_mkSlice_rci, toArray_mkSlice_rci, size_toArray_eq_size,
mkSlice_roo_eq_mkSlice_rco, toArray_mkSlice_rco]
public theorem toList_mkSlice_roi_eq_toList_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
xs[lo<...*].toList = xs[(lo + 1)...xs.size].toList := by
simp [ length_toList, - Slice.length_toList_eq_size]
public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
xs[lo<...*].toArray = xs[(lo + 1)...xs.size].toArray := by
simp
@[simp]
public theorem toList_mkSlice_roi {xs : ListSlice α} {lo : Nat} :
xs[lo<...*].toList = xs.toList.drop (lo + 1) := by
@@ -430,9 +347,9 @@ public theorem toArray_mkSlice_roi {xs : ListSlice α} {lo : Nat} :
xs[lo<...*].toArray = xs.toArray.extract (lo + 1) := by
simp only [ toArray_toList, toList_mkSlice_roi]
rw (occs := [1]) [ List.take_length (l := List.drop (lo + 1) xs.toList)]
simp [- toArray_toList]
simp
@[simp, grind =]
@[simp]
public theorem mkSlice_rio_eq_mkSlice_rco {xs : ListSlice α} {hi : Nat} :
xs[*...hi] = xs[0...hi] := by
simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -457,11 +374,6 @@ public theorem mkSlice_ric_eq_mkSlice_rcc {xs : ListSlice α} {hi : Nat} :
xs[*...=hi] = xs[0...=hi] := by
simp [Std.Ric.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@[grind =]
public theorem mkSlice_ric_eq_mkSlice_rco {xs : ListSlice α} {hi : Nat} :
xs[*...=hi] = xs[0...(hi + 1)] := by
simp [Std.Ric.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@[simp]
public theorem toList_mkSlice_ric {xs : ListSlice α} {hi : Nat} :
xs[*...=hi].toList = xs.toList.take (hi + 1) := by
@@ -472,7 +384,7 @@ public theorem toArray_mkSlice_ric {xs : ListSlice α} {hi : Nat} :
xs[*...=hi].toArray = xs.toArray.extract 0 (hi + 1) := by
simp [ toArray_toList]
@[simp, grind =]
@[simp]
public theorem mkSlice_rii {xs : ListSlice α} :
xs[*...*] = xs := by
simp [Std.Rii.Sliceable.mkSlice]

View File

@@ -123,6 +123,18 @@ opaque getUTF8Byte (s : @& String) (n : Nat) (h : n < s.utf8ByteSize) : UInt8
end String.Internal
/--
Creates a string that contains the characters in a list, in order.
Examples:
* `['L', '∃', '∀', 'N'].asString = "L∃∀N"`
* `[].asString = ""`
* `['a', 'a', 'a'].asString = "aaa"`
-/
@[extern "lean_string_mk", expose]
def String.ofList (data : List Char) : String :=
List.utf8Encode data,.intro data rfl
@[extern "lean_string_mk", expose, deprecated String.ofList (since := "2025-10-30")]
def String.mk (data : List Char) : String :=
List.utf8Encode data,.intro data rfl

View File

@@ -4,9 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Init.Classical
public section
namespace Lean.Grind
/-- A helper gadget for annotating nested proofs in goals. -/

View File

@@ -143,7 +143,6 @@ end DSimp
namespace Simp
@[inline]
def defaultMaxSteps := 100000
/--

View File

@@ -3192,7 +3192,7 @@ Constructs a new empty array with initial capacity `0`.
Use `Array.emptyWithCapacity` to create an array with a greater initial capacity.
-/
@[expose, inline]
@[expose]
def Array.empty {α : Type u} : Array α := emptyWithCapacity 0
/--
@@ -3481,18 +3481,6 @@ structure String where ofByteArray ::
attribute [extern "lean_string_to_utf8"] String.toByteArray
attribute [extern "lean_string_from_utf8_unchecked"] String.ofByteArray
/--
Creates a string that contains the characters in a list, in order.
Examples:
* `String.ofList ['L', '∃', '∀', 'N'] = "L∃∀N"`
* `String.ofList [] = ""`
* `String.ofList ['a', 'a', 'a'] = "aaa"`
-/
@[extern "lean_string_mk"]
def String.ofList (data : List Char) : String :=
List.utf8Encode data, .intro data rfl
/--
Decides whether two strings are equal. Normally used via the `DecidableEq String` instance and the
`=` operator.

View File

@@ -1,8 +0,0 @@
/-
Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Init.Sym.Lemmas

View File

@@ -1,140 +0,0 @@
/-
Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Init.Data.Nat.Basic
public import Init.Data.Rat.Basic
public import Init.Data.Int.Basic
public import Init.Data.UInt.Basic
public import Init.Data.SInt.Basic
public section
namespace Lean.Sym
theorem ne_self (a : α) : (a a) = False := by simp
theorem not_true_eq : (¬ True) = False := by simp
theorem not_false_eq : (¬ False) = True := by simp
theorem ite_cond_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α)
(c' : Prop) {inst' : Decidable c'} (h : c = c') : @ite α c inst a b = @ite α c' inst' a b := by
simp [*]
theorem dite_cond_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a : c α) (b : ¬ c α)
(c' : Prop) {inst' : Decidable c'} (h : c = c')
: @dite α c inst a b = @dite α c' inst' (fun h' => a (h.mpr_prop h')) (fun h' => b (h.mpr_not h')) := by
simp [*]
theorem cond_cond_eq_true {α : Sort u} (c : Bool) (a b : α) (h : c = true) : cond c a b = a := by
simp [*]
theorem cond_cond_eq_false {α : Sort u} (c : Bool) (a b : α) (h : c = false) : cond c a b = b := by
simp [*]
theorem cond_cond_congr {α : Sort u} (c : Bool) (a b : α) (c' : Bool) (h : c = c') : cond c a b = cond c' a b := by
simp [*]
theorem Nat.lt_eq_true (a b : Nat) (h : decide (a < b) = true) : (a < b) = True := by simp_all
theorem Int.lt_eq_true (a b : Int) (h : decide (a < b) = true) : (a < b) = True := by simp_all
theorem Rat.lt_eq_true (a b : Rat) (h : decide (a < b) = true) : (a < b) = True := by simp_all
theorem Int8.lt_eq_true (a b : Int8) (h : decide (a < b) = true) : (a < b) = True := by simp_all
theorem Int16.lt_eq_true (a b : Int16) (h : decide (a < b) = true) : (a < b) = True := by simp_all
theorem Int32.lt_eq_true (a b : Int32) (h : decide (a < b) = true) : (a < b) = True := by simp_all
theorem Int64.lt_eq_true (a b : Int64) (h : decide (a < b) = true) : (a < b) = True := by simp_all
theorem UInt8.lt_eq_true (a b : UInt8) (h : decide (a < b) = true) : (a < b) = True := by simp_all
theorem UInt16.lt_eq_true (a b : UInt16) (h : decide (a < b) = true) : (a < b) = True := by simp_all
theorem UInt32.lt_eq_true (a b : UInt32) (h : decide (a < b) = true) : (a < b) = True := by simp_all
theorem UInt64.lt_eq_true (a b : UInt64) (h : decide (a < b) = true) : (a < b) = True := by simp_all
theorem Fin.lt_eq_true (a b : Fin n) (h : decide (a < b) = true) : (a < b) = True := by simp_all
theorem BitVec.lt_eq_true (a b : BitVec n) (h : decide (a < b) = true) : (a < b) = True := by simp_all
theorem String.lt_eq_true (a b : String) (h : decide (a < b) = true) : (a < b) = True := by simp_all
theorem Char.lt_eq_true (a b : Char) (h : decide (a < b) = true) : (a < b) = True := by simp_all
theorem Nat.lt_eq_false (a b : Nat) (h : decide (a < b) = false) : (a < b) = False := by simp_all
theorem Int.lt_eq_false (a b : Int) (h : decide (a < b) = false) : (a < b) = False := by simp_all
theorem Rat.lt_eq_false (a b : Rat) (h : decide (a < b) = false) : (a < b) = False := by simp_all
theorem Int8.lt_eq_false (a b : Int8) (h : decide (a < b) = false) : (a < b) = False := by simp_all
theorem Int16.lt_eq_false (a b : Int16) (h : decide (a < b) = false) : (a < b) = False := by simp_all
theorem Int32.lt_eq_false (a b : Int32) (h : decide (a < b) = false) : (a < b) = False := by simp_all
theorem Int64.lt_eq_false (a b : Int64) (h : decide (a < b) = false) : (a < b) = False := by simp_all
theorem UInt8.lt_eq_false (a b : UInt8) (h : decide (a < b) = false) : (a < b) = False := by simp_all
theorem UInt16.lt_eq_false (a b : UInt16) (h : decide (a < b) = false) : (a < b) = False := by simp_all
theorem UInt32.lt_eq_false (a b : UInt32) (h : decide (a < b) = false) : (a < b) = False := by simp_all
theorem UInt64.lt_eq_false (a b : UInt64) (h : decide (a < b) = false) : (a < b) = False := by simp_all
theorem Fin.lt_eq_false (a b : Fin n) (h : decide (a < b) = false) : (a < b) = False := by simp_all
theorem BitVec.lt_eq_false (a b : BitVec n) (h : decide (a < b) = false) : (a < b) = False := by simp_all
theorem String.lt_eq_false (a b : String) (h : decide (a < b) = false) : (a < b) = False := by simp_all
theorem Char.lt_eq_false (a b : Char) (h : decide (a < b) = false) : (a < b) = False := by simp_all
theorem Nat.le_eq_true (a b : Nat) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem Int.le_eq_true (a b : Int) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem Rat.le_eq_true (a b : Rat) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem Int8.le_eq_true (a b : Int8) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem Int16.le_eq_true (a b : Int16) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem Int32.le_eq_true (a b : Int32) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem Int64.le_eq_true (a b : Int64) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem UInt8.le_eq_true (a b : UInt8) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem UInt16.le_eq_true (a b : UInt16) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem UInt32.le_eq_true (a b : UInt32) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem UInt64.le_eq_true (a b : UInt64) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem Fin.le_eq_true (a b : Fin n) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem BitVec.le_eq_true (a b : BitVec n) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem String.le_eq_true (a b : String) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem Char.le_eq_true (a b : Char) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem Nat.le_eq_false (a b : Nat) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem Int.le_eq_false (a b : Int) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem Rat.le_eq_false (a b : Rat) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem Int8.le_eq_false (a b : Int8) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem Int16.le_eq_false (a b : Int16) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem Int32.le_eq_false (a b : Int32) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem Int64.le_eq_false (a b : Int64) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem UInt8.le_eq_false (a b : UInt8) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem UInt16.le_eq_false (a b : UInt16) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem UInt32.le_eq_false (a b : UInt32) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem UInt64.le_eq_false (a b : UInt64) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem Fin.le_eq_false (a b : Fin n) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem BitVec.le_eq_false (a b : BitVec n) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem String.le_eq_false (a b : String) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem Char.le_eq_false (a b : Char) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem Nat.eq_eq_true (a b : Nat) (h : decide (a = b) = true) : (a = b) = True := by simp_all
theorem Int.eq_eq_true (a b : Int) (h : decide (a = b) = true) : (a = b) = True := by simp_all
theorem Rat.eq_eq_true (a b : Rat) (h : decide (a = b) = true) : (a = b) = True := by simp_all
theorem Int8.eq_eq_true (a b : Int8) (h : decide (a = b) = true) : (a = b) = True := by simp_all
theorem Int16.eq_eq_true (a b : Int16) (h : decide (a = b) = true) : (a = b) = True := by simp_all
theorem Int32.eq_eq_true (a b : Int32) (h : decide (a = b) = true) : (a = b) = True := by simp_all
theorem Int64.eq_eq_true (a b : Int64) (h : decide (a = b) = true) : (a = b) = True := by simp_all
theorem UInt8.eq_eq_true (a b : UInt8) (h : decide (a = b) = true) : (a = b) = True := by simp_all
theorem UInt16.eq_eq_true (a b : UInt16) (h : decide (a = b) = true) : (a = b) = True := by simp_all
theorem UInt32.eq_eq_true (a b : UInt32) (h : decide (a = b) = true) : (a = b) = True := by simp_all
theorem UInt64.eq_eq_true (a b : UInt64) (h : decide (a = b) = true) : (a = b) = True := by simp_all
theorem Fin.eq_eq_true (a b : Fin n) (h : decide (a = b) = true) : (a = b) = True := by simp_all
theorem BitVec.eq_eq_true (a b : BitVec n) (h : decide (a = b) = true) : (a = b) = True := by simp_all
theorem String.eq_eq_true (a b : String) (h : decide (a = b) = true) : (a = b) = True := by simp_all
theorem Char.eq_eq_true (a b : Char) (h : decide (a = b) = true) : (a = b) = True := by simp_all
theorem Nat.eq_eq_false (a b : Nat) (h : decide (a = b) = false) : (a = b) = False := by simp_all
theorem Int.eq_eq_false (a b : Int) (h : decide (a = b) = false) : (a = b) = False := by simp_all
theorem Rat.eq_eq_false (a b : Rat) (h : decide (a = b) = false) : (a = b) = False := by simp_all
theorem Int8.eq_eq_false (a b : Int8) (h : decide (a = b) = false) : (a = b) = False := by simp_all
theorem Int16.eq_eq_false (a b : Int16) (h : decide (a = b) = false) : (a = b) = False := by simp_all
theorem Int32.eq_eq_false (a b : Int32) (h : decide (a = b) = false) : (a = b) = False := by simp_all
theorem Int64.eq_eq_false (a b : Int64) (h : decide (a = b) = false) : (a = b) = False := by simp_all
theorem UInt8.eq_eq_false (a b : UInt8) (h : decide (a = b) = false) : (a = b) = False := by simp_all
theorem UInt16.eq_eq_false (a b : UInt16) (h : decide (a = b) = false) : (a = b) = False := by simp_all
theorem UInt32.eq_eq_false (a b : UInt32) (h : decide (a = b) = false) : (a = b) = False := by simp_all
theorem UInt64.eq_eq_false (a b : UInt64) (h : decide (a = b) = false) : (a = b) = False := by simp_all
theorem Fin.eq_eq_false (a b : Fin n) (h : decide (a = b) = false) : (a = b) = False := by simp_all
theorem BitVec.eq_eq_false (a b : BitVec n) (h : decide (a = b) = false) : (a = b) = False := by simp_all
theorem String.eq_eq_false (a b : String) (h : decide (a = b) = false) : (a = b) = False := by simp_all
theorem Char.eq_eq_false (a b : Char) (h : decide (a = b) = false) : (a = b) = False := by simp_all
theorem Nat.dvd_eq_true (a b : Nat) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem Int.dvd_eq_true (a b : Int) (h : decide (a b) = true) : (a b) = True := by simp_all
theorem Nat.dvd_eq_false (a b : Nat) (h : decide (a b) = false) : (a b) = False := by simp_all
theorem Int.dvd_eq_false (a b : Int) (h : decide (a b) = false) : (a b) = False := by simp_all
end Lean.Sym

View File

@@ -518,13 +518,14 @@ syntax location := withPosition(ppGroup(" at" (locationWildcard <|> locationHyp)
assuming these are definitionally equal.
* `change t' at h` will change hypothesis `h : t` to have type `t'`, assuming
assuming `t` and `t'` are definitionally equal.
-/
syntax (name := change) "change " term (location)? : tactic
/--
* `change a with b` will change occurrences of `a` to `b` in the goal,
assuming `a` and `b` are definitionally equal.
* `change a with b at h` similarly changes `a` to `b` in the type of hypothesis `h`.
-/
syntax (name := change) "change " term (location)? : tactic
@[tactic_alt change]
syntax (name := changeWith) "change " term " with " term (location)? : tactic
/--
@@ -545,7 +546,7 @@ introducing new local definitions.
For example, given a local hypotheses if the form `h : let x := v; b x`, then `extract_lets z at h`
introduces a new local definition `z := v` and changes `h` to be `h : b z`.
-/
syntax (name := extractLets) "extract_lets" ppSpace optConfig (ppSpace colGt (ident <|> hole))* (location)? : tactic
syntax (name := extractLets) "extract_lets " optConfig (ppSpace colGt (ident <|> hole))* (location)? : tactic
/--
Lifts `let` and `have` expressions within a term as far out as possible.
@@ -904,13 +905,8 @@ The tactic supports all the same syntax variants and options as the `let` term.
-/
macro "let" c:letConfig d:letDecl : tactic => `(tactic| refine_lift let $c:letConfig $d:letDecl; ?_)
/--
`let rec f : t := e` adds a recursive definition `f` to the current goal.
The syntax is the same as term-mode `let rec`.
The tactic supports all the same syntax variants and options as the `let` term.
-/
@[tactic_name "let rec"]
/-- `let rec f : t := e` adds a recursive definition `f` to the current goal.
The syntax is the same as term-mode `let rec`. -/
syntax (name := letrec) withPosition(atomic("let " &"rec ") letRecDecls) : tactic
macro_rules
| `(tactic| let rec $d) => `(tactic| refine_lift let rec $d; ?_)
@@ -1216,6 +1212,22 @@ while `congr 2` produces the intended `⊢ x + y = y + x`.
syntax (name := congr) "congr" (ppSpace num)? : tactic
/--
In tactic mode, `if h : t then tac1 else tac2` can be used as alternative syntax for:
```
by_cases h : t
· tac1
· tac2
```
It performs case distinction on `h : t` or `h : ¬t` and `tac1` and `tac2` are the subproofs.
You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but
if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed
by the end of the block.
-/
syntax (name := tacDepIfThenElse)
ppRealGroup(ppRealFill(ppIndent("if " binderIdent " : " term " then") ppSpace matchRhsTacticSeq)
ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
/--
In tactic mode, `if t then tac1 else tac2` is alternative syntax for:
@@ -1224,34 +1236,16 @@ by_cases t
· tac1
· tac2
```
It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous hypothesis, and
`tac1` and `tac2` are the subproofs. (It doesn't actually use nondependent `if`, since this wouldn't
add anything to the context and hence would be useless for proving theorems. To actually insert an
`ite` application use `refine if t then ?_ else ?_`.)
The assumptions in each subgoal can be named. `if h : t then tac1 else tac2` can be used as
alternative syntax for:
```
by_cases h : t
· tac1
· tac2
```
It performs case distinction on `h : t` or `h : ¬t`.
You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but
if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed
by the end of the block.
It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous
hypothesis, and `tac1` and `tac2` are the subproofs. (It doesn't actually use
nondependent `if`, since this wouldn't add anything to the context and hence would be
useless for proving theorems. To actually insert an `ite` application use
`refine if t then ?_ else ?_`.)
-/
syntax (name := tacIfThenElse)
ppRealGroup(ppRealFill(ppIndent("if " term " then") ppSpace matchRhsTacticSeq)
ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
@[tactic_alt tacIfThenElse]
syntax (name := tacDepIfThenElse)
ppRealGroup(ppRealFill(ppIndent("if " binderIdent " : " term " then") ppSpace matchRhsTacticSeq)
ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
/--
The tactic `nofun` is shorthand for `exact nofun`: it introduces the assumptions, then performs an
empty pattern match, closing the goal if the introduced pattern is impossible.

View File

@@ -28,8 +28,7 @@ builtin_initialize closedTermCacheExt : EnvExtension ClosedTermCache ←
{ s with map := s.map.insert e c, constNames := s.constNames.insert c, revExprs := e :: s.revExprs })
def cacheClosedTermName (env : Environment) (e : Expr) (n : Name) : Environment :=
closedTermCacheExt.modifyState env fun s =>
{ s with map := s.map.insert e n, constNames := s.constNames.insert n, revExprs := e :: s.revExprs }
closedTermCacheExt.modifyState env fun s => { s with map := s.map.insert e n, constNames := s.constNames.insert n }
def getClosedTermName? (env : Environment) (e : Expr) : Option Name :=
(closedTermCacheExt.getState env).map.find? e

View File

@@ -44,7 +44,7 @@ def log (entry : LogEntry) : CompilerM Unit :=
def tracePrefixOptionName := `trace.compiler.ir
private def isLogEnabledFor (opts : Options) (optName : Name) : Bool :=
match opts.get? optName with
match opts.find optName with
| some (DataValue.ofBool v) => v
| _ => opts.getBool tracePrefixOptionName

View File

@@ -45,4 +45,3 @@ public import Lean.Compiler.LCNF.LambdaLifting
public import Lean.Compiler.LCNF.ReduceArity
public import Lean.Compiler.LCNF.Probing
public import Lean.Compiler.LCNF.Irrelevant
public import Lean.Compiler.LCNF.SplitSCC

View File

@@ -258,4 +258,45 @@ end Check
def Decl.check (decl : Decl) : CompilerM Unit := do
Check.run do decl.value.forCodeM (Check.checkFunDeclCore decl.name decl.params decl.type)
/--
Check whether every local declaration in the local context is used in one of given `decls`.
-/
partial def checkDeadLocalDecls (decls : Array Decl) : CompilerM Unit := do
let (_, s) := visitDecls decls |>.run {}
let usesFVar (binderName : Name) (fvarId : FVarId) :=
unless s.contains fvarId do
throwError "LCNF local context contains unused local variable declaration `{binderName}`"
let lctx := ( get).lctx
lctx.params.forM fun fvarId decl => usesFVar decl.binderName fvarId
lctx.letDecls.forM fun fvarId decl => usesFVar decl.binderName fvarId
lctx.funDecls.forM fun fvarId decl => usesFVar decl.binderName fvarId
where
visitFVar (fvarId : FVarId) : StateM FVarIdHashSet Unit :=
modify (·.insert fvarId)
visitParam (param : Param) : StateM FVarIdHashSet Unit := do
visitFVar param.fvarId
visitParams (params : Array Param) : StateM FVarIdHashSet Unit := do
params.forM visitParam
visitCode (code : Code) : StateM FVarIdHashSet Unit := do
match code with
| .jmp .. | .return .. | .unreach .. => return ()
| .let decl k => visitFVar decl.fvarId; visitCode k
| .fun decl k | .jp decl k =>
visitFVar decl.fvarId; visitParams decl.params; visitCode decl.value
visitCode k
| .cases c => c.alts.forM fun alt => do
match alt with
| .default k => visitCode k
| .alt _ ps k => visitParams ps; visitCode k
visitDecl (decl : Decl) : StateM FVarIdHashSet Unit := do
visitParams decl.params
decl.value.forCodeM visitCode
visitDecls (decls : Array Decl) : StateM FVarIdHashSet Unit :=
decls.forM visitDecl
end Lean.Compiler.LCNF

View File

@@ -156,8 +156,7 @@ mutual
/-- Collect dependencies of the given expression. -/
partial def collectType (type : Expr) : ClosureM Unit := do
if type.hasFVar then
type.forEachWhere Expr.isFVar fun e => collectFVar e.fvarId!
type.forEachWhere Expr.isFVar fun e => collectFVar e.fvarId!
end

View File

@@ -52,10 +52,6 @@ structure Context where
structure State where
decls : Array Decl := {}
/--
Cache for `shouldExtractFVar` in order to avoid superlinear behavior.
-/
fvarDecisionCache : Std.HashMap FVarId Bool := {}
abbrev M := ReaderT Context $ StateRefT State CompilerM
@@ -82,10 +78,6 @@ partial def shouldExtractLetValue (isRoot : Bool) (v : LetValue) : M Bool := do
| _ => true
if !shouldExtract then
return false
if let some decl LCNF.getMonoDecl? name then
-- We don't want to extract constants as root terms
if decl.getArity == 0 then
return false
args.allM shouldExtractArg
| .fvar fnVar args => return ( shouldExtractFVar fnVar) && ( args.allM shouldExtractArg)
| .proj _ _ baseVar => shouldExtractFVar baseVar
@@ -96,18 +88,10 @@ partial def shouldExtractArg (arg : Arg) : M Bool := do
| .type _ | .erased => return true
partial def shouldExtractFVar (fvarId : FVarId) : M Bool := do
if let some result := ( get).fvarDecisionCache[fvarId]? then
return result
if let some letDecl findLetDecl? fvarId then
shouldExtractLetValue false letDecl.value
else
let result go
modify fun s => { s with fvarDecisionCache := s.fvarDecisionCache.insert fvarId result }
return result
where
go : M Bool := do
if let some letDecl findLetDecl? fvarId then
shouldExtractLetValue false letDecl.value
else
return false
return false
end

View File

@@ -8,7 +8,6 @@ module
prelude
public import Lean.Compiler.LCNF.FVarUtil
public import Lean.Compiler.LCNF.PassManager
import Lean.Compiler.IR.CompilerM
public section
@@ -20,27 +19,30 @@ namespace FloatLetIn
The decision of the float mechanism.
-/
inductive Decision where
|
/--
Push into the arm with name `name`.
-/
| arm (name : Name)
/--
arm (name : Name)
| /--
Push into the default arm.
-/
| default
default
|
/--
Don't move this declaration it is needed where it is right now.
-/
| dont
dont
|
/--
No decision has been made yet.
-/
| unknown
unknown
deriving Hashable, BEq, Inhabited, Repr
def Decision.ofAlt : Alt Decision
| .alt name _ _ => .arm name
| .default _ => .default
| .alt name _ _ => .arm name
| .default _ => .default
/--
The context for `BaseFloatM`.
@@ -110,7 +112,6 @@ def ignore? (decl : LetDecl) : BaseFloatM Bool := do
Compute the initial decision for all declarations that `BaseFloatM` collected
up to this point, with respect to `cs`. The initial decisions are:
- `dont` if the declaration is detected by `ignore?`
- `dont` if the a variable used by the declaration is later used as a potentially owned parameter
- `dont` if the declaration is the discriminant of `cs` since we obviously need
the discriminant to be computed before the match.
- `dont` if we see the declaration being used in more than one cases arm
@@ -119,55 +120,20 @@ up to this point, with respect to `cs`. The initial decisions are:
-/
def initialDecisions (cs : Cases) : BaseFloatM (Std.HashMap FVarId Decision) := do
let mut map := Std.HashMap.emptyWithCapacity ( read).decls.length
let owned : Std.HashSet FVarId :=
(map, _) ( read).decls.foldlM (init := (map, owned)) fun (acc, owned) val => do
map ( read).decls.foldrM (init := map) fun val acc => do
if let .let decl := val then
if ( ignore? decl) then
return (acc.insert decl.fvarId .dont, owned)
let (dont, owned) := (visitDecl ( getEnv) val).run owned
if dont then
return (acc.insert val.fvarId .dont, owned)
else
return (acc.insert val.fvarId .unknown, owned)
return acc.insert decl.fvarId .dont
return acc.insert val.fvarId .unknown
if map.contains cs.discr then
map := map.insert cs.discr .dont
(_, map) goCases cs |>.run map
return map
where
visitDecl (env : Environment) (value : CodeDecl) : StateM (Std.HashSet FVarId) Bool := do
match value with
| .let decl => visitLetValue env decl.value
| _ => return false -- will need to investigate whether that can be a problem
visitLetValue (env : Environment) (value : LetValue) : StateM (Std.HashSet FVarId) Bool := do
match value with
| .proj _ _ x => visitArg (.fvar x) true
| .const nm _ args =>
let decl? := IR.findEnvDecl env nm
match decl? with
| none => args.foldlM (fun b arg => visitArg arg false <||> pure b) false
| some decl =>
let mut res := false
for h : i in *...args.size do
if visitArg args[i] (decl.params[i]?.any (·.borrow)) then
res := true
return res
| .fvar x args =>
args.foldlM (fun b arg => visitArg arg false <||> pure b)
( visitArg (.fvar x) false)
| .erased | .lit _ => return false
visitArg (var : Arg) (borrowed : Bool) : StateM (Std.HashSet FVarId) Bool := do
let .fvar v := var | return false
let res := ( get).contains v
unless borrowed do
modify (·.insert v)
return res
goFVar (plannedDecision : Decision) (var : FVarId) : StateRefT (Std.HashMap FVarId Decision) BaseFloatM Unit := do
if let some decision := ( get)[var]? then
if decision matches .unknown then
if decision == .unknown then
modify fun s => s.insert var plannedDecision
else if decision != plannedDecision then
modify fun s => s.insert var .dont

View File

@@ -11,7 +11,6 @@ public import Lean.Compiler.LCNF.Passes
public import Lean.Compiler.LCNF.ToDecl
public import Lean.Compiler.LCNF.Check
import Lean.Meta.Match.MatcherInfo
import Lean.Compiler.LCNF.SplitSCC
public section
namespace Lean.Compiler.LCNF
/--
@@ -51,12 +50,14 @@ The trace can be viewed with `set_option trace.Compiler.step true`.
def checkpoint (stepName : Name) (decls : Array Decl) (shouldCheck : Bool) : CompilerM Unit := do
for decl in decls do
trace[Compiler.stat] "{decl.name} : {decl.size}"
withOptions (fun opts => opts.set `pp.motives.pi false) do
withOptions (fun opts => opts.setBool `pp.motives.pi false) do
let clsName := `Compiler ++ stepName
if ( Lean.isTracingEnabledFor clsName) then
Lean.addTrace clsName m!"size: {decl.size}\n{← ppDecl' decl}"
if shouldCheck then
decl.check
if shouldCheck then
checkDeadLocalDecls decls
def isValidMainType (type : Expr) : Bool :=
let isValidResultName (name : Name) : Bool :=
@@ -73,7 +74,7 @@ def isValidMainType (type : Expr) : Bool :=
namespace PassManager
def run (declNames : Array Name) : CompilerM (Array (Array IR.Decl)) := withAtLeastMaxRecDepth 8192 do
def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRecDepth 8192 do
/-
Note: we need to increase the recursion depth because we currently do to save phase1
declarations in .olean files. Then, we have to recursively compile all dependencies,
@@ -99,33 +100,31 @@ def run (declNames : Array Name) : CompilerM (Array (Array IR.Decl)) := withAtLe
let decls := markRecDecls decls
let manager getPassManager
let isCheckEnabled := compiler.check.get ( getOptions)
let decls runPassManagerPart "compilation (LCNF base)" manager.basePasses decls isCheckEnabled
let decls runPassManagerPart "compilation (LCNF mono)" manager.monoPasses decls isCheckEnabled
let sccs withTraceNode `Compiler.splitSCC (fun _ => return m!"Splitting up SCC") do
splitScc decls
sccs.mapM fun decls => do
let decls runPassManagerPart "compilation (LCNF mono)" manager.monoPassesNoLambda decls isCheckEnabled
if ( Lean.isTracingEnabledFor `Compiler.result) then
for decl in decls do
let decl normalizeFVarIds decl
Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl}"
profileitM Exception "compilation (IR)" ( getOptions) do
let irDecls IR.toIR decls
IR.compile irDecls
where
runPassManagerPart (profilerName : String) (passes : Array Pass) (decls : Array Decl)
(isCheckEnabled : Bool) : CompilerM (Array Decl) := do
profileitM Exception profilerName ( getOptions) do
let mut decls := decls
for pass in passes do
decls withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
withPhase pass.phase <| pass.run decls
withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
return decls
let decls profileitM Exception "compilation (LCNF base)" ( getOptions) do
let mut decls := decls
for pass in manager.basePasses do
decls withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
withPhase pass.phase <| pass.run decls
withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
return decls
let decls profileitM Exception "compilation (LCNF mono)" ( getOptions) do
let mut decls := decls
for pass in manager.monoPasses do
decls withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
withPhase pass.phase <| pass.run decls
withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
return decls
if ( Lean.isTracingEnabledFor `Compiler.result) then
for decl in decls do
let decl normalizeFVarIds decl
Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl}"
profileitM Exception "compilation (IR)" ( getOptions) do
let irDecls IR.toIR decls
IR.compile irDecls
end PassManager
def compile (declNames : Array Name) : CoreM (Array (Array IR.Decl)) :=
def compile (declNames : Array Name) : CoreM (Array IR.Decl) :=
CompilerM.run <| PassManager.run declNames
def showDecl (phase : Phase) (declName : Name) : CoreM Format := do

View File

@@ -87,7 +87,6 @@ pipeline.
structure PassManager where
basePasses : Array Pass
monoPasses : Array Pass
monoPassesNoLambda : Array Pass
deriving Inhabited
instance : ToString Phase where
@@ -115,7 +114,6 @@ private def validatePasses (phase : Phase) (passes : Array Pass) : CoreM Unit :=
def validate (manager : PassManager) : CoreM Unit := do
validatePasses .base manager.basePasses
validatePasses .mono manager.monoPasses
validatePasses .mono manager.monoPassesNoLambda
def findOccurrenceBounds (targetName : Name) (passes : Array Pass) : CoreM (Nat × Nat) := do
let mut lowest := none

View File

@@ -115,8 +115,6 @@ def builtinPassManager : PassManager := {
simp (occurrence := 4) (phase := .mono),
floatLetIn (phase := .mono) (occurrence := 2),
lambdaLifting,
]
monoPassesNoLambda := #[
extendJoinPointContext (phase := .mono) (occurrence := 1),
simp (occurrence := 5) (phase := .mono),
elimDeadBranches,

View File

@@ -213,17 +213,13 @@ def Folder.mkBinary [Literal α] [Literal β] [Literal γ] (folder : α → β
mkLit <| folder arg₁ arg₂
def Folder.mkBinaryDecisionProcedure [Literal α] [Literal β] {r : α β Prop} (folder : (a : α) (b : β) Decidable (r a b)) : Folder := fun args => do
if ( getPhase) < .mono then
return none
let #[.fvar fvarId₁, .fvar fvarId₂] := args | return none
let some arg₁ getLit fvarId₁ | return none
let some arg₂ getLit fvarId₂ | return none
let result := folder arg₁ arg₂ |>.decide
if ( getPhase) < .mono then
if result then
return some <| .const ``Decidable.isTrue [] #[.erased, .erased]
else
return some <| .const ``Decidable.isFalse [] #[.erased, .erased]
else
mkLit result
let boolLit := folder arg₁ arg₂ |>.decide
mkLit boolLit
/--
Provide a folder for an operation with a left neutral element.

View File

@@ -1,52 +0,0 @@
/-
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
module
prelude
public import Lean.Compiler.LCNF.CompilerM
import Lean.Util.SCC
namespace Lean.Compiler.LCNF
namespace SplitScc
partial def findSccCalls (scc : Std.HashMap Name Decl) (decl : Decl) : BaseIO (Std.HashSet Name) := do
match decl.value with
| .code code =>
let (_, calls) goCode code |>.run {}
return calls
| .extern .. => return {}
where
goCode (c : Code) : StateRefT (Std.HashSet Name) BaseIO Unit := do
match c with
| .let decl k =>
if let .const name .. := decl.value then
if scc.contains name then
modify fun s => s.insert name
goCode k
| .fun decl k | .jp decl k =>
goCode decl.value
goCode k
| .cases cases => cases.alts.forM (·.forCodeM goCode)
| .jmp .. | .return .. | .unreach .. => return ()
end SplitScc
public def splitScc (scc : Array Decl) : CompilerM (Array (Array Decl)) := do
if scc.size == 1 then
return #[scc]
let declMap := Std.HashMap.ofArray <| scc.map fun decl => (decl.name, decl)
let callers := Std.HashMap.ofArray <| scc.mapM fun decl => do
let calls SplitScc.findSccCalls declMap decl
return (decl.name, calls.toList)
let newSccs := Lean.SCC.scc (scc.toList.map (·.name)) (callers.getD · [])
trace[Compiler.splitSCC] m!"Split SCC into {newSccs}"
return newSccs.toArray.map (fun scc => scc.toArray.map declMap.get!)
builtin_initialize
registerTraceClass `Compiler.splitSCC (inherited := true)
end Lean.Compiler.LCNF

View File

@@ -543,12 +543,10 @@ def logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CoreM
/-- Wraps the given action for use in `EIO.asTask` etc., discarding its final monadic state. -/
def wrapAsync {α : Type} (act : α CoreM β) (cancelTk? : Option IO.CancelToken) :
CoreM (α EIO Exception β) := do
let (childNGen, parentNGen) := ( getNGen).mkChild
setNGen parentNGen
let (childDeclNGen, parentDeclNGen) := ( getDeclNGen).mkChild
setDeclNGen parentDeclNGen
let (childNGen, parentNGen) := ( getDeclNGen).mkChild
setDeclNGen parentNGen
let st get
let st := { st with auxDeclNGen := childDeclNGen, ngen := childNGen }
let st := { st with auxDeclNGen := childNGen }
let ctx read
let ctx := { ctx with cancelTk? }
let heartbeats := ( IO.getNumHeartbeats) - ctx.initHeartbeats

View File

@@ -226,13 +226,7 @@ def opt [ToJson α] (k : String) : Option α → List (String × Json)
| none => []
| some o => [k, toJson o]
/-- Returns the string value or single key name, if any. -/
def getTag? : Json Option String
| .str tag => some tag
| .obj kvs => guard (kvs.size == 1) *> kvs.minKey?
| _ => none
-- TODO: delete after rebootstrap
/-- Parses a JSON-encoded `structure` or `inductive` constructor. Used mostly by `deriving FromJson`. -/
def parseTagged
(json : Json)
(tag : String)
@@ -265,28 +259,5 @@ def parseTagged
| Except.error err => Except.error err
| Except.error err => Except.error err
/--
Parses a JSON-encoded `structure` or `inductive` constructor, assuming the tag has already been
checked and `nFields` is nonzero. Used mostly by `deriving FromJson`.
-/
def parseCtorFields
(json : Json)
(tag : String)
(nFields : Nat)
(fieldNames? : Option (Array Name)) : Except String (Array Json) := do
let payload getObjVal? json tag
match fieldNames? with
| some fieldNames =>
fieldNames.mapM (getObjVal? payload ·.getString!)
| none =>
if nFields == 1 then
Except.ok #[payload]
else
let fields getArr? payload
if fields.size == nFields then
Except.ok fields
else
Except.error s!"incorrect number of fields: {fields.size} ≟ {nFields}"
end Json
end Lean

View File

@@ -14,72 +14,14 @@ public section
namespace Lean
structure Options where
private map : NameMap DataValue
/--
Whether any option with prefix `trace` is set. This does *not* imply that any of such option is
set to `true` but it does capture the most common case that no such option has ever been touched.
-/
hasTrace : Bool
namespace Options
def empty : Options where
map := {}
hasTrace := false
@[export lean_options_get_empty]
private def getEmpty (_ : Unit) : Options := .empty
@[expose] def Options := KVMap
def Options.empty : Options := {}
instance : Inhabited Options where
default := .empty
instance : ToString Options where
toString o := private toString o.map.toList
instance [Monad m] : ForIn m Options (Name × DataValue) where
forIn o init f := private forIn o.map init f
instance : BEq Options where
beq o1 o2 := private o1.map.beq o2.map
instance : EmptyCollection Options where
emptyCollection := .empty
@[inline] def find? (o : Options) (k : Name) : Option DataValue :=
o.map.find? k
@[deprecated find? (since := "2026-01-15")]
def find := find?
@[inline] def get? {α : Type} [KVMap.Value α] (o : Options) (k : Name) : Option α :=
o.map.find? k |>.bind KVMap.Value.ofDataValue?
@[inline] def get {α : Type} [KVMap.Value α] (o : Options) (k : Name) (defVal : α) : α :=
o.get? k |>.getD defVal
@[inline] def getBool (o : Options) (k : Name) (defVal : Bool := false) : Bool :=
o.get k defVal
@[inline] def contains (o : Options) (k : Name) : Bool :=
o.map.contains k
@[inline] def insert (o : Options) (k : Name) (v : DataValue) : Options where
map := o.map.insert k v
hasTrace := o.hasTrace || (`trace).isPrefixOf k
def set {α : Type} [KVMap.Value α] (o : Options) (k : Name) (v : α) : Options :=
o.insert k (KVMap.Value.toDataValue v)
@[inline] def setBool (o : Options) (k : Name) (v : Bool) : Options :=
o.set k v
def erase (o : Options) (k : Name) : Options where
map := o.map.erase k
-- `erase` is expected to be used even more rarely than `set` so O(n) is fine
hasTrace := o.map.keys.any (`trace).isPrefixOf
def mergeBy (f : Name DataValue DataValue DataValue) (o1 o2 : Options) : Options where
map := o1.map.mergeWith f o2.map
hasTrace := o1.hasTrace || o2.hasTrace
end Options
default := {}
instance : ToString Options := inferInstanceAs (ToString KVMap)
instance [Monad m] : ForIn m Options (Name × DataValue) := inferInstanceAs (ForIn _ KVMap _)
instance : BEq Options := inferInstanceAs (BEq KVMap)
structure OptionDecl where
name : Name
@@ -148,11 +90,11 @@ variable [Monad m] [MonadOptions m]
def getBoolOption (k : Name) (defValue := false) : m Bool := do
let opts getOptions
return opts.get k defValue
return opts.getBool k defValue
def getNatOption (k : Name) (defValue := 0) : m Nat := do
let opts getOptions
return opts.get k defValue
return opts.getNat k defValue
class MonadWithOptions (m : Type Type) where
withOptions (f : Options Options) (x : m α) : m α
@@ -166,10 +108,10 @@ instance [MonadFunctor m n] [MonadWithOptions m] : MonadWithOptions n where
the term being delaborated should be treated as a pattern. -/
def withInPattern [MonadWithOptions m] (x : m α) : m α :=
withOptions (fun o => o.set `_inPattern true) x
withOptions (fun o => o.setBool `_inPattern true) x
def Options.getInPattern (o : Options) : Bool :=
o.get `_inPattern false
o.getBool `_inPattern
/-- A strongly-typed reference to an option. -/
protected structure Option (α : Type) where
@@ -189,20 +131,12 @@ protected def get? [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : Op
protected def get [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : α :=
opts.get opt.name opt.defValue
@[export lean_options_get_bool]
private def getBool (opts : Options) (name : Name) (defValue : Bool) : Bool :=
opts.get name defValue
protected def getM [Monad m] [MonadOptions m] [KVMap.Value α] (opt : Lean.Option α) : m α :=
return opt.get ( getOptions)
protected def set [KVMap.Value α] (opts : Options) (opt : Lean.Option α) (val : α) : Options :=
opts.set opt.name val
@[export lean_options_update_bool]
private def updateBool (opts : Options) (name : Name) (val : Bool) : Options :=
opts.set name val
/-- Similar to `set`, but update `opts` only if it doesn't already contains an setting for `opt.name` -/
protected def setIfNotSet [KVMap.Value α] (opts : Options) (opt : Lean.Option α) (val : α) : Options :=
if opts.contains opt.name then opts else opt.set opts val

View File

@@ -1220,7 +1220,7 @@ Disables the option `doc.verso` while running a parser.
public def withoutVersoSyntax (p : Parser) : Parser where
fn :=
adaptUncacheableContextFn
(fun c => { c with options := c.options.set `doc.verso false })
(fun c => { c with options := c.options.setBool `doc.verso false })
p.fn
info := p.info

View File

@@ -456,7 +456,7 @@ where
withRef tk <| Meta.check e
let e Term.levelMVarToParam ( instantiateMVars e)
-- TODO: add options or notation for setting the following parameters
withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.set `smartUnfolding false }) do
withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
let e withTransparency (mode := TransparencyMode.all) <| reduce e (skipProofs := skipProofs) (skipTypes := skipTypes)
logInfoAt tk e

View File

@@ -274,12 +274,10 @@ def wrapAsync {α β : Type} (act : α → CommandElabM β) (cancelTk? : Option
CommandElabM (α EIO Exception β) := do
let ctx read
let ctx := { ctx with cancelTk? }
let (childNGen, parentNGen) := ( get).ngen.mkChild
modify fun s => { s with ngen := parentNGen }
let (childDeclNGen, parentDeclNGen) := ( getDeclNGen).mkChild
setDeclNGen parentDeclNGen
let (childNGen, parentNGen) := ( getDeclNGen).mkChild
setDeclNGen parentNGen
let st get
let st := { st with auxDeclNGen := childDeclNGen, ngen := childNGen }
let st := { st with auxDeclNGen := childNGen }
return (act · |>.run ctx |>.run' st)
open Language in

View File

@@ -232,7 +232,7 @@ def applyDerivingHandlers (className : Name) (typeNames : Array Name) (setExpose
withScope (fun sc => { sc with
attrs := if setExpose then Unhygienic.run `(Parser.Term.attrInstance| expose) :: sc.attrs else sc.attrs
-- Deactivate some linting options that only make writing deriving handlers more painful.
opts := sc.opts.set `warn.exposeOnPrivate false
opts := sc.opts.setBool `warn.exposeOnPrivate false
-- When any of the types are private, the deriving handler will need access to the private scope
-- and should create private instances.
isPublic := !typeNames.any isPrivateName }) do

View File

@@ -111,18 +111,14 @@ def mkFromJsonBodyForStruct (indName : Name) : TermElabM Term := do
def mkFromJsonBodyForInduct (ctx : Context) (indName : Name) : TermElabM Term := do
let indVal getConstInfoInduct indName
let (ctors, alts) := ( mkAlts indVal).unzip
`(match Json.getTag? json with
| some tag => match tag with
$[| $(ctors.map Syntax.mkStrLit) => $(alts)]*
| _ => Except.error "no inductive constructor matched"
| none => Except.error "no inductive tag found")
let alts mkAlts indVal
let auxTerm alts.foldrM (fun xs x => `(Except.orElseLazy $xs (fun _ => $x))) ( `(Except.error "no inductive constructor matched"))
`($auxTerm)
where
mkAlts (indVal : InductiveVal) : TermElabM (Array (String × Term)) := do
mkAlts (indVal : InductiveVal) : TermElabM (Array Term) := do
let mut alts := #[]
for ctorName in indVal.ctors do
let ctorInfo getConstInfoCtor ctorName
let ctorStr := ctorName.eraseMacroScopes.getString!
let alt do forallTelescopeReducing ctorInfo.type fun xs _ => do
let mut binders := #[]
let mut userNames := #[]
@@ -146,14 +142,11 @@ where
else
``(none)
let stx
if ctorInfo.numFields == 0 then
`(return $(mkIdent ctorName):ident $identNames*)
else
`((Json.parseCtorFields json $(quote ctorStr) $(quote ctorInfo.numFields) $(quote userNamesOpt)).bind
(fun jsons => do
$[let $identNames:ident $fromJsons:doExpr]*
return $(mkIdent ctorName):ident $identNames*))
pure ((ctorStr, stx), ctorInfo.numFields)
`((Json.parseTagged json $(quote ctorName.eraseMacroScopes.getString!) $(quote ctorInfo.numFields) $(quote userNamesOpt)).bind
(fun jsons => do
$[let $identNames:ident $fromJsons:doExpr]*
return $(mkIdent ctorName):ident $identNames*))
pure (stx, ctorInfo.numFields)
alts := alts.push alt
-- the smaller cases, especially the ones without fields are likely faster
let alts' := alts.qsort (fun (_, x) (_, y) => x < y)

View File

@@ -1267,7 +1267,7 @@ def «set_option» (option : Ident) (value : DataValue) : DocM (Block ElabInline
pushInfoLeaf <| .ofOptionInfo { stx := option, optionName, declName := decl.declName }
validateOptionValue optionName decl value
let o getOptions
modify fun s => { s with options := o.set optionName value }
modify fun s => { s with options := o.insert optionName value }
return .empty
/--

View File

@@ -1210,8 +1210,8 @@ private def applyComputedFields (indViews : Array InductiveView) : CommandElabM
computedFields := computedFields.push (declName, computedFieldNames)
withScope (fun scope => { scope with
opts := scope.opts
|>.set `bootstrap.genMatcherCode false
|>.set `elaboratingComputedFields true}) <|
|>.setBool `bootstrap.genMatcherCode false
|>.setBool `elaboratingComputedFields true}) <|
elabCommand <| `(mutual $computedFieldDefs* end)
liftTermElabM do Term.withDeclName indViews[0]!.declName do

View File

@@ -52,7 +52,7 @@ def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
pushInfoLeaf <| .ofOptionInfo { stx := id, optionName, declName := decl.declName }
let rec setOption (val : DataValue) : m Options := do
validateOptionValue optionName decl val
return ( getOptions).set optionName val
return ( getOptions).insert optionName val
match val.isStrLit? with
| some str => setOption (DataValue.ofString str)
| none =>

View File

@@ -290,7 +290,7 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d
let quotSymbol := "`(" ++ suffix ++ "| "
let name := catName ++ `quot
let cmd ← `(
@[term_parser] public meta def $(mkIdent name) : Lean.ParserDescr :=
@[term_parser] meta def $(mkIdent name) : Lean.ParserDescr :=
Lean.ParserDescr.node `Lean.Parser.Term.quot $(quote Lean.Parser.maxPrec)
(Lean.ParserDescr.node $(quote name) $(quote Lean.Parser.maxPrec)
(Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol $(quote quotSymbol))
@@ -312,7 +312,7 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d
let attrName := catName.appendAfter "_parser"
let catDeclName := ``Lean.Parser.Category ++ catName
setEnv (← Parser.registerParserCategory (← getEnv) attrName catName catBehavior catDeclName)
let cmd ← `($[$docString?]? public meta def $(mkIdentFrom stx[2] (`_root_ ++ catDeclName) (canonical := true)) : Lean.Parser.Category := {})
let cmd ← `($[$docString?]? meta def $(mkIdentFrom stx[2] (`_root_ ++ catDeclName) (canonical := true)) : Lean.Parser.Category := {})
declareSyntaxCatQuotParser catName
elabCommand cmd

View File

@@ -309,7 +309,7 @@ where
Add an auxiliary declaration. Only used to create constants that appear in our reflection proof.
-/
mkAuxDecl (name : Name) (value type : Expr) : CoreM Unit :=
withOptions (fun opt => opt.set `compiler.extract_closed false) do
withOptions (fun opt => opt.setBool `compiler.extract_closed false) do
addAndCompile <| .defnDecl {
name := name,
levelParams := [],

View File

@@ -41,8 +41,8 @@ public def findSpec (database : SpecTheorems) (wp : Expr) : MetaM SpecTheorem :=
-- information why the defeq check failed, so we do it again.
withOptions (fun o =>
if o.getBool `trace.Elab.Tactic.Do.spec then
o |>.set `pp.universes true
|>.set `trace.Meta.isDefEq true
o |>.setBool `pp.universes true
|>.setBool `trace.Meta.isDefEq true
else
o) do
withTraceNode `Elab.Tactic.Do.spec (fun _ => return m!"Defeq check for {type} failed.") do

View File

@@ -47,10 +47,10 @@ partial def genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : MetaM Result
mvar.withContext <| withReducible do
let (prf, state) StateRefT'.run (ReaderT.run (onGoal goal ( mvar.getTag)) ctx) { fuel }
mvar.assign prf
for h : idx in *...state.invariants.size do
for h : idx in [:state.invariants.size] do
let mv := state.invariants[idx]
mv.setTag (Name.mkSimple ("inv" ++ toString (idx + 1)))
for h : idx in *...state.vcs.size do
for h : idx in [:state.vcs.size] do
let mv := state.vcs[idx]
mv.setTag (Name.mkSimple ("vc" ++ toString (idx + 1)) ++ ( mv.getTag).eraseMacroScopes)
return { invariants := state.invariants, vcs := state.vcs }

View File

@@ -94,15 +94,14 @@ def ifOutOfFuel (x : VCGenM α) (k : VCGenM α) : VCGenM α := do
def addSubGoalAsVC (goal : MVarId) : VCGenM PUnit := do
goal.freshenLCtxUserNamesSinceIdx ( read).initialCtxSize
let ty goal.getType
-- Here we make `mvar` a synthetic opaque goal upon discharge failure.
-- This is the right call for (previously natural) holes such as loop invariants, which
-- would otherwise lead to spurious instantiations and unwanted renamings (when leaving the
-- scope of a local).
-- We also do this for, e.g. schematic variables. One reason is that at this point, we have
-- already tried to assign them by unification. Another reason is that we want to display the
-- VC to the user as-is, without abstracting any variables in the local context.
-- This only makes sense for synthetic opaque metavariables.
goal.setKind .syntheticOpaque
if ty.isAppOf ``Std.Do.PostCond || ty.isAppOf ``Std.Do.SPred then
-- Here we make `mvar` a synthetic opaque goal upon discharge failure.
-- This is the right call for (previously natural) holes such as loop invariants, which
-- would otherwise lead to spurious instantiations and unwanted renamings (when leaving the
-- scope of a local).
-- But it's wrong for, e.g., schematic variables. The latter should never be PostConds,
-- Invariants or SPreds, hence the condition.
goal.setKind .syntheticOpaque
if ty.isAppOf ``Std.Do.Invariant then
modify fun s => { s with invariants := s.invariants.push goal }
else

View File

@@ -8,7 +8,6 @@ module
prelude
import Lean.DocString
public import Lean.Elab.Command
public import Lean.Parser.Tactic.Doc
public section
@@ -39,42 +38,30 @@ open Lean.Parser.Command
| _ => throwError "Malformed 'register_tactic_tag' command"
/--
Computes a table that heuristically maps parser syntax kinds to their first tokens by inspecting the
Pratt parsing tables for the `tactic syntax kind. If a custom name is provided for the tactic, then
it is returned instead.
Gets the first string token in a parser description. For example, for a declaration like
`syntax "squish " term " with " term : tactic`, it returns `some "squish "`, and for a declaration
like `syntax tactic " <;;;> " tactic : tactic`, it returns `some " <;;;> "`.
Returns `none` for syntax declarations that don't contain a string constant.
-/
def firstTacticTokens [Monad m] [MonadEnv m] : m (NameMap String) := do
let env getEnv
private partial def getFirstTk (e : Expr) : MetaM (Option String) := do
match ( Meta.whnf e).getAppFnArgs with
| (``ParserDescr.node, #[_, _, p]) => getFirstTk p
| (``ParserDescr.trailingNode, #[_, _, _, p]) => getFirstTk p
| (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getFirstTk p
| (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getFirstTk p
| (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getFirstTk p
| (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
| (``ParserDescr.symbol, #[.lit (.strVal tk)]) => pure (some tk)
| (``Parser.withAntiquot, #[_, p]) => getFirstTk p
| (``Parser.leadingNode, #[_, _, p]) => getFirstTk p
| (``HAndThen.hAndThen, #[_, _, _, _, p1, p2]) =>
if let some tk getFirstTk p1 then pure (some tk)
else getFirstTk (.app p2 (.const ``Unit.unit []))
| (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
| (``Parser.symbol, #[.lit (.strVal tk)]) => pure (some tk)
| _ => pure none
let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
| return {}
let mut firstTokens : NameMap String :=
tacticNameExt.toEnvExtension.getState env
|>.importedEntries
|>.push (tacticNameExt.exportEntriesFn env (tacticNameExt.getState env) .exported)
|>.foldl (init := {}) fun names inMods =>
inMods.foldl (init := names) fun names (k, n) =>
names.insert k n
firstTokens := addFirstTokens tactics tactics.tables.leadingTable firstTokens
firstTokens := addFirstTokens tactics tactics.tables.trailingTable firstTokens
return firstTokens
where
addFirstTokens tactics table firsts : NameMap String := Id.run do
let mut firsts := firsts
for (tok, ps) in table do
-- Skip antiquotes
if tok == `«$» then continue
for (p, _) in ps do
for (k, ()) in p.info.collectKinds {} do
if tactics.kinds.contains k then
let tok := tok.toString (escape := false)
-- It's important here that the already-existing mapping is preserved, because it will
-- contain any user-provided custom name, and these shouldn't be overridden.
firsts := firsts.alter k (·.getD tok)
return firsts
/--
Creates some `MessageData` for a parser name.
@@ -84,14 +71,18 @@ identifiable leading token, then that token is shown. Otherwise, the underlying
without an `@`. The name includes metadata that makes infoview hovers and the like work. This
only works for global constants, as the local context is not included.
-/
private def showParserName [Monad m] [MonadEnv m] (firsts : NameMap String) (n : Name) : m MessageData := do
private def showParserName (n : Name) : MetaM MessageData := do
let env getEnv
let params :=
env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
let tok := (( customTacticName n) <|> firsts.get? n).map Std.Format.text |>.getD (format n)
let tok
if let some descr := env.find? n |>.bind (·.value?) then
if let some tk getFirstTk descr then
pure <| Std.Format.text tk.trimAscii.copy
else pure <| format n
else pure <| format n
pure <| .ofFormatWithInfos {
fmt := "`" ++ .tag 0 tok ++ "`",
fmt := "'" ++ .tag 0 tok ++ "'",
infos :=
.ofList [(0, .ofTermInfo {
lctx := .empty,
@@ -102,6 +93,7 @@ private def showParserName [Monad m] [MonadEnv m] (firsts : NameMap String) (n :
})] _
}
/--
Displays all available tactic tags, with documentation.
-/
@@ -114,22 +106,20 @@ Displays all available tactic tags, with documentation.
for (tac, tag) in arr do
mapping := mapping.insert tag (mapping.getD tag {} |>.insert tac)
let firsts firstTacticTokens
let showDocs : Option String MessageData
| none => .nil
| some d => Format.line ++ MessageData.joinSep ((d.split '\n').map (toMessageData String.Slice.copy)).toList Format.line
let showTactics (tag : Name) : CommandElabM MessageData := do
let showTactics (tag : Name) : MetaM MessageData := do
match mapping.find? tag with
| none => pure .nil
| some tacs =>
if tacs.isEmpty then pure .nil
else
let tacs := tacs.toArray.qsort (·.toString < ·.toString) |>.toList
pure (Format.line ++ MessageData.joinSep ( tacs.mapM (showParserName firsts)) ", ")
pure (Format.line ++ MessageData.joinSep ( tacs.mapM showParserName) ", ")
let tagDescrs ( allTagsWithInfo).mapM fun (name, userName, docs) => do
let tagDescrs liftTermElabM <| ( allTagsWithInfo).mapM fun (name, userName, docs) => do
pure <| m!"" ++
MessageData.nestD (m!"`{name}`" ++
(if name.toString != userName then m!"\"{userName}\"" else MessageData.nil) ++
@@ -156,13 +146,13 @@ structure TacticDoc where
/-- Any docstring extensions that have been specified -/
extensionDocs : Array String
def allTacticDocs (includeUnnamed : Bool := true) : MetaM (Array TacticDoc) := do
def allTacticDocs : MetaM (Array TacticDoc) := do
let env getEnv
let allTags :=
tacticTagExt.toEnvExtension.getState env |>.importedEntries
|>.push (tacticTagExt.exportEntriesFn env (tacticTagExt.getState env) .exported)
let all :=
tacticTagExt.toEnvExtension.getState ( getEnv)
|>.importedEntries |>.push (tacticTagExt.exportEntriesFn ( getEnv) (tacticTagExt.getState ( getEnv)) .exported)
let mut tacTags : NameMap NameSet := {}
for arr in allTags do
for arr in all do
for (tac, tag) in arr do
tacTags := tacTags.insert tac (tacTags.getD tac {} |>.insert tag)
@@ -170,18 +160,15 @@ def allTacticDocs (includeUnnamed : Bool := true) : MetaM (Array TacticDoc) := d
let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
| return #[]
let firstTokens firstTacticTokens
for (tac, _) in tactics.kinds do
-- Skip noncanonical tactics
if let some _ := alternativeOfTactic env tac then continue
let userName? : Option String := firstTokens.get? tac
let userName
if let some n := userName? then pure n
else if includeUnnamed then pure tac.toString
else continue
let userName : String
if let some descr := env.find? tac |>.bind (·.value?) then
if let some tk getFirstTk descr then
pure tk.trimAscii.copy
else pure tac.toString
else pure tac.toString
docs := docs.push {
internalName := tac,

View File

@@ -2386,27 +2386,4 @@ def eagerReflBoolTrue : Expr :=
def eagerReflBoolFalse : Expr :=
mkApp2 (mkConst ``eagerReduce [0]) (mkApp3 (mkConst ``Eq [1]) (mkConst ``Bool) (mkConst ``Bool.false) (mkConst ``Bool.false)) reflBoolFalse
/--
Replaces the head constant in a function application chain with a different constant.
Given an expression that is either a constant or a function application chain,
replaces the head constant with `declName` while preserving all arguments and universe levels.
**Examples**:
- `f.replaceFn g` → `g` (where `f` is a constant)
- `(f a b c).replaceFn g` → `g a b c`
- `(@f.{u, v} a b).replaceFn g` → `@g.{u, v} a b`
**Panics**: If the expression is neither a constant nor a function application.
**Use case**: Useful for substituting one function for another while maintaining
the same application structure, such as replacing a theorem with a related theorem
that has the same type and universe parameters.
-/
def Expr.replaceFn (e : Expr) (declName : Name) : Expr :=
match e with
| .app f a => mkApp (f.replaceFn declName) a
| .const _ us => mkConst declName us
| _ => panic! "function application or constant expected"
end Lean

View File

@@ -308,8 +308,8 @@ def setOption (opts : Options) (decl : OptionDecl) (name : Name) (val : String)
match decl.defValue with
| .ofBool _ =>
match val with
| "true" => return opts.set name true
| "false" => return opts.set name false
| "true" => return opts.insert name true
| "false" => return opts.insert name false
| _ =>
throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
it must be true/false"
@@ -317,8 +317,8 @@ def setOption (opts : Options) (decl : OptionDecl) (name : Name) (val : String)
let some val := val.toNat?
| throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
it must be a natural number"
return opts.set name val
| .ofString _ => return opts.set name val
return opts.insert name val
| .ofString _ => return opts.insert name val
| _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \
cannot be set in the command line, use set_option command"
@@ -342,7 +342,7 @@ def reparseOptions (opts : Options) : IO Options := do
If the option is defined in a library, use '-D{`weak ++ name}' to set it conditionally"
let .ofString val := val
| opts' := opts'.set name val -- Already parsed
| opts' := opts'.insert name val -- Already parsed
opts' setOption opts' decl name val

View File

@@ -316,10 +316,9 @@ builtin_initialize typePrefixDenyListExt : SimplePersistentEnvExtension Name (Li
def isDeniedModule (env : Environment) (moduleName : Name) : Bool :=
(moduleDenyListExt.getState env).any fun p => moduleName.anyS (· == p)
def isDeniedPremise (env : Environment) (name : Name) (allowPrivate : Bool := false) : Bool := Id.run do
def isDeniedPremise (env : Environment) (name : Name) : Bool := Id.run do
if name == ``sorryAx then return true
-- Allow private names through if allowPrivate is set (e.g., for currentFile selector)
if name.isInternalDetail && !(allowPrivate && isPrivateName name) then return true
if name.isInternalDetail then return true
if Lean.Meta.isInstanceCore env name then return true
if Lean.Linter.isDeprecated env name then return true
if (nameDenyListExt.getState env).any (fun p => name.anyS (· == p)) then return true
@@ -359,14 +358,14 @@ def currentFile : Selector := fun _ cfg => do
let max := cfg.maxSuggestions
-- Use map₂ from the staged map, which contains locally defined constants
let mut suggestions := #[]
for (name, _) in env.constants.map₂ do
for (name, ci) in env.constants.map₂.toList do
if suggestions.size >= max then
break
-- Allow private names since they're accessible from the current module
if isDeniedPremise env name (allowPrivate := true) then
if isDeniedPremise env name then
continue
if wasOriginallyTheorem env name then
suggestions := suggestions.push { name := name, score := 1.0 }
match ci with
| .thmInfo _ => suggestions := suggestions.push { name := name, score := 1.0 }
| _ => continue
return suggestions
builtin_initialize librarySuggestionsExt : SimplePersistentEnvExtension Name (Option Name)

View File

@@ -74,7 +74,7 @@ def prepareTriggers (names : Array Name) (maxTolerance : Float := 3.0) : MetaM (
let mut map := {}
let env getEnv
let names := names.filter fun n =>
!isDeniedPremise env n && wasOriginallyTheorem env n
!isDeniedPremise env n && Lean.wasOriginallyTheorem env n
for name in names do
let triggers triggerSymbols ( getConstInfo name) maxTolerance
for (trigger, tolerance) in triggers do

View File

@@ -28,7 +28,7 @@ skipping instance arguments and proofs.
public def localSymbolFrequencyMap : MetaM (NameMap Nat) := do
let env := ( getEnv)
env.constants.map₂.foldlM (init := ) (fun acc m ci => do
if isDeniedPremise env m || !wasOriginallyTheorem env m then
if isDeniedPremise env m || !Lean.wasOriginallyTheorem env m then
pure acc
else
ci.type.foldRelevantConstants (init := acc) fun n' acc => return acc.alter n' fun i? => some (i?.getD 0 + 1))

View File

@@ -247,7 +247,7 @@ def ofConstName (constName : Name) (fullNames : Bool := false) : MessageData :=
let msg ofFormatWithInfos <$> match ctx? with
| .none => pure (format constName)
| .some ctx =>
let ctx := if fullNames then { ctx with opts := ctx.opts.set `pp.fullNames fullNames } else ctx
let ctx := if fullNames then { ctx with opts := ctx.opts.insert `pp.fullNames fullNames } else ctx
ppConstNameWithInfos ctx constName
return Dynamic.mk msg)
(fun _ => false)

View File

@@ -124,41 +124,17 @@ def mkInjectiveEqTheoremNameFor (ctorName : Name) : Name :=
private def mkInjectiveEqTheoremType? (ctorVal : ConstructorVal) : MetaM (Option Expr) :=
mkInjectiveTheoremTypeCore? ctorVal true
/--
Collects all components of a nested `And`, as projections.
(Avoids the binders that `MVarId.casesAnd` would introduce.)
-/
private partial def andProjections (e : Expr) : MetaM (Array Expr) := do
let rec go (e : Expr) (t : Expr) (acc : Array Expr) : MetaM (Array Expr) := do
match_expr t with
| And t1 t2 =>
let acc go (mkProj ``And 0 e) t1 acc
let acc go (mkProj ``And 0 e) t2 acc
return acc
| _ =>
return acc.push e
go e ( inferType e) #[]
private def mkInjectiveEqTheoremValue (ctorName : Name) (targetType : Expr) : MetaM Expr := do
forallTelescopeReducing targetType fun xs type => do
let mvar mkFreshExprSyntheticOpaqueMVar type
let [mvarId₁, mvarId₂] mvar.mvarId!.apply (mkConst ``Eq.propIntro)
| throwError "unexpected number of subgoals when proving injective theorem for constructor `{ctorName}`"
let (h, mvarId₁) mvarId₁.intro1
let (_, mvarId₂) mvarId₂.intro1
solveEqOfCtorEq ctorName mvarId₁ h
let mut mvarId₂ := mvarId₂
while true do
let t mvarId₂.getType
let some (conj, body) := t.arrow? | break
match_expr conj with
| And lhs rhs =>
let [mvarId₂'] mvarId₂.applyN (mkApp3 (mkConst `Lean.injEq_helper) lhs rhs body) 1
| throwError "unexpected number of goals after applying `Lean.and_imp`"
mvarId₂ := mvarId₂'
| _ => pure ()
let (h, mvarId₂') mvarId₂.intro1
(_, mvarId₂) substEq mvarId₂' h
try mvarId₂.refl catch _ => throwError (injTheoremFailureHeader ctorName)
let mvarId₂ mvarId₂.casesAnd
if let some mvarId₂ mvarId₂.substEqs then
try mvarId₂.refl catch _ => throwError (injTheoremFailureHeader ctorName)
mkLambdaFVars xs mvar
private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do

View File

@@ -177,16 +177,4 @@ def mkHaveS (x : Name) (t : Expr) (v : Expr) (b : Expr) : m Expr := do
else
mkLetS n newType newVal newBody nondep
def mkAppS₂ (f a₁ a₂ : Expr) : m Expr := do
mkAppS ( mkAppS f a₁) a₂
def mkAppS₃ (f a₁ a₂ a₃ : Expr) : m Expr := do
mkAppS ( mkAppS₂ f a₁ a₂) a₃
def mkAppS₄ (f a₁ a₂ a₃ a₄ : Expr) : m Expr := do
mkAppS ( mkAppS₃ f a₁ a₂ a₃) a₄
def mkAppS₅ (f a₁ a₂ a₃ a₄ a₅ : Expr) : m Expr := do
mkAppS ( mkAppS₄ f a₁ a₂ a₃ a₄) a₅
end Lean.Meta.Sym.Internal

View File

@@ -103,19 +103,7 @@ Applies a backward rule to a goal, returning new subgoals.
2. Assigns the goal metavariable to the theorem application
3. Returns new goals for unassigned arguments (per `resultPos`)
Returns `none` if unification fails.
-/
public def BackwardRule.apply? (mvarId : MVarId) (rule : BackwardRule) : SymM (Option (List MVarId)) := mvarId.withContext do
let decl mvarId.getDecl
if let some result rule.pattern.unify? decl.type then
mvarId.assign (mkValue rule.expr rule.pattern result)
return some <| rule.resultPos.map fun i =>
result.args[i]!.mvarId!
else
return none
/--
Similar to `BackwardRule.apply?`, but throws an error if unification fails.
Throws an error if unification fails.
-/
public def BackwardRule.apply (mvarId : MVarId) (rule : BackwardRule) : SymM (List MVarId) := mvarId.withContext do
let decl mvarId.getDecl

View File

@@ -1,86 +0,0 @@
/-
Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Expr
public import Init.Data.Rat
public section
namespace Lean.Meta.Sym
/-!
Pure functions for extracting values. They are pure (`OptionT Id`) rather than monadic (`MetaM`).
This is possible because `Sym` assumes terms are in canonical form, no `whnf` or
reduction is needed to recognize literals.
-/
def getNatValue? (e : Expr) : OptionT Id Nat := do
let_expr OfNat.ofNat _ n _ := e | failure
let .lit (.natVal n) := n | failure
return n
def getIntValue? (e : Expr) : OptionT Id Int := do
let_expr Neg.neg _ _ a := e | getNatValue? e
let v : Int getNatValue? a
return -v
def getRatValue? (e : Expr) : OptionT Id Rat := do
let_expr HDiv.hDiv _ _ _ _ n d := e | getIntValue? e
let n : Rat getIntValue? n
let d : Rat getNatValue? d
return n / d
structure BitVecValue where
n : Nat
val : BitVec n
def getBitVecValue? (e : Expr) : OptionT Id BitVecValue :=
match_expr e with
| BitVec.ofNat nExpr vExpr => do
let n getNatValue? nExpr
let v getNatValue? vExpr
return n, BitVec.ofNat n v
| BitVec.ofNatLT nExpr vExpr _ => do
let n getNatValue? nExpr
let v getNatValue? vExpr
return n, BitVec.ofNat n v
| OfNat.ofNat α v _ => do
let_expr BitVec n := α | failure
let n getNatValue? n
let .lit (.natVal v) := v | failure
return n, BitVec.ofNat n v
| _ => failure
def getUInt8Value? (e : Expr) : OptionT Id UInt8 := return UInt8.ofNat ( getNatValue? e)
def getUInt16Value? (e : Expr) : OptionT Id UInt16 := return UInt16.ofNat ( getNatValue? e)
def getUInt32Value? (e : Expr) : OptionT Id UInt32 := return UInt32.ofNat ( getNatValue? e)
def getUInt64Value? (e : Expr) : OptionT Id UInt64 := return UInt64.ofNat ( getNatValue? e)
def getInt8Value? (e : Expr) : OptionT Id Int8 := return Int8.ofInt ( getIntValue? e)
def getInt16Value? (e : Expr) : OptionT Id Int16 := return Int16.ofInt ( getIntValue? e)
def getInt32Value? (e : Expr) : OptionT Id Int32 := return Int32.ofInt ( getIntValue? e)
def getInt64Value? (e : Expr) : OptionT Id Int64 := return Int64.ofInt ( getIntValue? e)
structure FinValue where
n : Nat
val : Fin n
def getFinValue? (e : Expr) : OptionT Id FinValue := do
let_expr OfNat.ofNat α v _ := e | failure
let_expr Fin n := α | failure
let n getNatValue? n
let .lit (.natVal v) := v | failure
if h : n = 0 then failure else
let : NeZero n := h
return { n, val := Fin.ofNat n v }
def getCharValue? (e : Expr) : OptionT Id Char := do
let_expr Char.ofNat n := e | failure
let .lit (.natVal n) := n | failure
return Char.ofNat n
def getStringValue? (e : Expr) : Option String :=
match e with
| .lit (.strVal s) => some s
| _ => none
end Lean.Meta.Sym

View File

@@ -1,93 +0,0 @@
/-
Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Meta.Sym.LitValues
public section
namespace Lean.Meta.Sym
/-!
# Offset representation for natural number expressions
This module provides utilities for representing `Nat` expressions in the form `e + k`,
where `e` is an arbitrary expression and `k` is a constant.
This normalization is used during pattern matching and unification.
-/
/--
Represents a natural number expression as a base plus a constant offset.
- `.num k` represents the literal `k`
- `.add e k` represents `e + k`
Used for pattern matching and unification.
-/
inductive Offset where
| num (k : Nat)
| add (e : Expr) (k : Nat)
deriving Inhabited
/-- Increments the constant part of the offset by `k'`. -/
def Offset.inc : Offset Nat Offset
| .num k, k' => .num (k+k')
| .add e k, k' => .add e (k+k')
/--
Returns `some offset` if `e` is an offset term. That is, it is of the form
- `Nat.succ a`, OR
- `a + k` where `k` is a numeral.
Assumption: standard instances are used for `OfNat Nat n` and `HAdd Nat Nat Nat`
-/
partial def isOffset? (e : Expr) : OptionT Id Offset :=
match_expr e with
| Nat.succ a => do
return get a |>.inc 1
| HAdd.hAdd α _ _ _ a b => do
guard (α.isConstOf ``Nat)
let n getNatValue? b
return get a |>.inc n
| _ => failure
where
get (e : Expr) : Offset :=
isOffset? e |>.getD (.add e 0)
/-- Variant of `isOffset?` that first checks if `declName` is `Nat.succ` or `HAdd.hAdd`. -/
def isOffset?' (declName : Name) (p : Expr) : OptionT Id Offset := do
guard (declName == ``Nat.succ || declName == ``HAdd.hAdd)
isOffset? p
/-- Returns `true` if `e` is an offset term.-/
partial def isOffset (e : Expr) : Bool :=
match_expr e with
| Nat.succ _ => true
| HAdd.hAdd α _ _ _ _ b =>
α.isConstOf ``Nat &&
match_expr b with
| OfNat.ofNat _ n _ => (n matches .lit (.natVal _))
| _ => false
| _ => false
/-- Variant of `isOffset?` that first checks if `declName` is `Nat.succ` or `HAdd.hAdd`. -/
def isOffset' (declName : Name) (p : Expr) : Bool :=
(declName == ``Nat.succ || declName == ``HAdd.hAdd) && isOffset p
/--
Converts the given expression into an offset.
Assumptions:
- `e` has type `Nat`.
- standard instances are used for `OfNat Nat n` and `HAdd Nat Nat Nat`.
-/
partial def toOffset (e : Expr) : Offset :=
match_expr e with
| Nat.succ a => toOffset a |>.inc 1
| HAdd.hAdd _ _ _ _ a b => Id.run do
let some n := getNatValue? b | .add e 0
toOffset a |>.inc n
| OfNat.ofNat _ n _ => Id.run do
let .lit (.natVal n) := n | .add e 0
.num n
| _ => .add e 0
end Lean.Meta.Sym

View File

@@ -16,8 +16,6 @@ import Lean.Meta.Sym.IsClass
import Lean.Meta.Sym.MaxFVar
import Lean.Meta.Sym.ProofInstInfo
import Lean.Meta.Sym.AlphaShareBuilder
import Lean.Meta.Sym.LitValues
import Lean.Meta.Sym.Offset
namespace Lean.Meta.Sym
open Internal
@@ -44,10 +42,6 @@ framework (`Sym`). The design prioritizes performance by using a two-phase appro
- `instantiateRevS` ensures maximal sharing of result expressions
-/
/-- Helper function for checking whether types `α` and `β` are definitionally equal during unification/matching. -/
def isDefEqTypes (α β : Expr) : MetaM Bool := do
withReducible <| isDefEq α β
/--
Collects `ProofInstInfo` for all function symbols occurring in `pattern`.
@@ -62,18 +56,11 @@ def mkProofInstInfoMapFor (pattern : Expr) : MetaM (AssocList Name ProofInstInfo
return fnInfos
public structure Pattern where
levelParams : List Name
varTypes : Array Expr
isInstance : Array Bool
pattern : Expr
fnInfos : AssocList Name ProofInstInfo
/--
If `checkTypeMask? = some mask`, then we must check the type of pattern variable `i`
if `mask[i]` is true.
Moreover `mask.size == varTypes.size`.
See `mkCheckTypeMask`
-/
checkTypeMask? : Option (Array Bool)
levelParams : List Name
varTypes : Array Expr
isInstance : Array Bool
pattern : Expr
fnInfos : AssocList Name ProofInstInfo
deriving Inhabited
def uvarPrefix : Name := `_uvar
@@ -92,65 +79,6 @@ def preprocessPattern (declName : Name) : MetaM (List Name × Expr) := do
let type preprocessType type
return (levelParams, type)
/--
Creates a mask indicating which pattern variables require type checking during matching.
When matching a pattern against a target expression, we must ensure that pattern variable
assignments are type-correct. However, checking types for every variable is expensive.
This function identifies which variables actually need type checking.
**Key insight**: A pattern variable appearing as an argument to a function application
does not need its type checked separately, because the type information is already
encoded in the application structure, and we assume the input is type correct.
**Variables that need type checking**:
- Variables in function position: `f x` where `f` is a pattern variable
- Variables in binder domains or bodies: `∀ x : α, β` or `fun x : α => b`
- Variables appearing alone (not as part of any application)
**Variables that skip type checking**:
- Variables appearing only as arguments to applications: in `f x`, the variable `x`
does not need checking because the type of `f` constrains the type of `x`
**Examples**:
- `bv0_eq (x : BitVec 0) : x = 0`: pattern is just `x`, must check type to ensure `BitVec 0`
- `forall_true : (∀ _ : α, True) = True`: `α` appears in binder domain, must check
- `Nat.add_zero (x : Nat) : x + 0 = x`: `x` is argument to `HAdd.hAdd`, no check needed
**Note**: This analysis is conservative. It may mark some variables for checking even when
the type information is redundant (already determined by other constraints). This is
harmless—just extra work, not incorrect behavior.
Returns an array of booleans parallel to the pattern's `varTypes`, where `true` indicates
the variable's type must be checked against the matched subterm's type.
-/
def mkCheckTypeMask (pattern : Expr) (numPatternVars : Nat) : Array Bool :=
let mask := Array.replicate numPatternVars false
go pattern 0 false mask
where
go (e : Expr) (offset : Nat) (isArg : Bool) : Array Bool Array Bool :=
match e with
| .app f a => go f offset isArg go a offset true
| .letE .. => unreachable! -- We zeta-reduce at `preprocessType`
| .const .. | .fvar _ | .sort _ | .mvar _ | .lit _ => id
| .mdata _ b => go b offset isArg
| .proj .. => id -- Should not occur in patterns
| .forallE _ d b _
| .lam _ d b _ => go d offset false go b (offset+1) false
| .bvar idx => fun mask =>
if idx >= offset && !isArg then
let idx := idx - offset
mask.set! (mask.size - idx - 1) true
else
mask
def mkPatternCore (levelParams : List Name) (varTypes : Array Expr) (isInstance : Array Bool)
(pattern : Expr) : MetaM Pattern := do
let fnInfos mkProofInstInfoMapFor pattern
let checkTypeMask := mkCheckTypeMask pattern varTypes.size
let checkTypeMask? := if checkTypeMask.all (· == false) then none else some checkTypeMask
return { levelParams, varTypes, isInstance, pattern, fnInfos, checkTypeMask? }
/--
Creates a `Pattern` from the type of a theorem.
@@ -172,7 +100,9 @@ public def mkPatternFromDecl (declName : Name) (num? : Option Nat := none) : Met
if i < num then
if let .forallE _ d b _ := type then
return ( go (i+1) b (varTypes.push d) (isInstance.push (isClass? ( getEnv) d).isSome))
mkPatternCore levelParams varTypes isInstance type
let pattern := type
let fnInfos mkProofInstInfoMapFor pattern
return { levelParams, varTypes, isInstance, pattern, fnInfos }
go 0 type #[] #[]
/--
@@ -193,8 +123,9 @@ public def mkEqPatternFromDecl (declName : Name) : MetaM (Pattern × Expr) := do
return ( go b (varTypes.push d) (isInstance.push (isClass? ( getEnv) d).isSome))
else
let_expr Eq _ lhs rhs := type | throwError "resulting type for `{.ofConstName declName}` is not an equality"
let pattern mkPatternCore levelParams varTypes isInstance lhs
return (pattern, rhs)
let pattern := lhs
let fnInfos mkProofInstInfoMapFor pattern
return ({ levelParams, varTypes, isInstance, pattern, fnInfos }, rhs)
go type #[] #[]
structure UnifyM.Context where
@@ -208,11 +139,6 @@ structure UnifyM.State where
ePending : Array (Expr × Expr) := #[]
uPending : Array (Level × Level) := #[]
iPending : Array (Expr × Expr) := #[]
/--
Contains the index of the pattern variables that we must check whether its type
matches the type of the value assigned to it.
-/
tPending : Array Nat := #[]
us : List Level := []
args : Array Expr := #[]
@@ -227,14 +153,6 @@ def pushLevelPending (u : Level) (v : Level) : UnifyM Unit :=
def pushInstPending (p : Expr) (e : Expr) : UnifyM Unit :=
modify fun s => { s with iPending := s.iPending.push (p, e) }
/--
Mark pattern variable `i` for type checking. That is, at the end of phase 1
we must check whether the type of this pattern variable is compatible with the type of
the value assigned to it.
-/
def pushCheckTypePending (i : Nat) : UnifyM Unit :=
modify fun s => { s with tPending := s.tPending.push i }
def assignExprIfUnassigned (bidx : Nat) (e : Expr) : UnifyM Unit := do
let s get
let i := s.eAssignment.size - bidx - 1
@@ -251,8 +169,6 @@ def assignExpr (bidx : Nat) (e : Expr) : UnifyM Bool := do
return true
else
modify fun s => { s with eAssignment := s.eAssignment.set! i (some e) }
if ( read).pattern.checkTypeMask?.isSome then
pushCheckTypePending i
return true
def assignLevel (uidx : Nat) (u : Level) : UnifyM Bool := do
@@ -349,43 +265,13 @@ where
let some value fvarId.getValue? | return false
process p value
processOffset (p : Offset) (e : Offset) : UnifyM Bool := do
-- **Note** Recall that we don't assume patterns are maximally shared terms.
match p, e with
| .num _, .num _ => unreachable!
| .num k₁, .add e k₂ =>
if k₁ < k₂ then return false
process (mkNatLit (k₁ - k₂)) e
| .add p k₁, .num k₂ =>
if k₂ < k₁ then return false
process p ( share (mkNatLit (k₂ - k₁)))
| .add p k₁, .add e k₂ =>
if k₁ == k₂ then
process p e
else if k₁ < k₂ then
if k₁ == 0 then return false
process p ( share (mkNatAdd e (mkNatLit (k₂ - k₁))))
else
if k₂ == 0 then return false
process (mkNatAdd p (mkNatLit (k₁ - k₂))) e
processConstApp (declName : Name) (p : Expr) (e : Expr) : UnifyM Bool := do
processApp (p : Expr) (e : Expr) : UnifyM Bool := do
let f := p.getAppFn
let .const declName _ := f | processAppDefault p e
let some info := ( read).pattern.fnInfos.find? declName | process.processAppDefault p e
let numArgs := p.getAppNumArgs
processAppWithInfo p e (numArgs - 1) info
processApp (p : Expr) (e : Expr) : UnifyM Bool := withIncRecDepth do
let f := p.getAppFn
let .const declName _ := f | processAppDefault p e
if ( processConstApp declName p e) then
return true
else if let some p' := isOffset?' declName p then
processOffset p' (toOffset e)
else if let some e' := isOffset? e then
processOffset (toOffset p) e'
else
return false
processAppWithInfo (p : Expr) (e : Expr) (i : Nat) (info : ProofInstInfo) : UnifyM Bool := do
let .app fp ap := p | if e.isApp then return false else process p e
let .app fe ae := e | checkLetVar p e
@@ -483,11 +369,6 @@ structure DefEqM.Context where
If `unify` is `false`, it contains which variables can be assigned.
-/
mvarsNew : Array MVarId := #[]
/--
If a metavariable is in this collection, when we perform the assignment `?m := v`,
we must check whether their types are compatible.
-/
mvarsToCheckType : Array MVarId := #[]
abbrev DefEqM := ReaderT DefEqM.Context SymM
@@ -600,12 +481,6 @@ def mayAssign (t s : Expr) : SymM Bool := do
let tMaxFVarDecl tMaxFVarId.getDecl
return tMaxFVarDecl.index sMaxFVarDecl.index
@[inline] def whenUndefDo (x : DefEqM LBool) (k : DefEqM Bool) : DefEqM Bool := do
match ( x) with
| .true => return true
| .false => return false
| .undef => k
/--
Attempts to solve a unification constraint `t =?= s` where `t` has the form `?m a₁ ... aₙ`
and satisfies the Miller pattern condition (all `aᵢ` are distinct, newly-introduced free variables).
@@ -620,20 +495,17 @@ The `tFn` parameter must equal `t.getAppFn` (enforced by the proof argument).
Remark: `t` may be of the form `?m`.
-/
def tryAssignMillerPattern (tFn : Expr) (t : Expr) (s : Expr) (_ : tFn = t.getAppFn) : DefEqM LBool := do
let .mvar mvarId := tFn | return .undef
if !( isAssignableMVar mvarId) then return .undef
if !( isMillerPatternArgs t) then return .undef
def tryAssignMillerPattern (tFn : Expr) (t : Expr) (s : Expr) (_ : tFn = t.getAppFn) : DefEqM Bool := do
let .mvar mvarId := tFn | return false
if !( isAssignableMVar mvarId) then return false
if !( isMillerPatternArgs t) then return false
let s if t.isApp then
mkLambdaFVarsS t.getAppArgs s
else
pure s
if !( mayAssign tFn s) then return .undef
if ( read).mvarsToCheckType.contains mvarId then
unless ( Sym.isDefEqTypes ( mvarId.getDecl).type ( inferType s)) do
return .false
if !( mayAssign tFn s) then return false
mvarId.assign s
return .true
return true
/--
Structural definitional equality for applications without `ProofInstInfo`.
@@ -659,11 +531,6 @@ where
if ( mvarId.isAssigned) then return false
if !( isAssignableMVar mvarId) then return false
if !( mayAssign t s) then return false
/-
**Note**: we don't need to check the type of `mvarId` here even if the variable is marked for
checking. This is the case because `tryAssignUnassigned` is invoked only from a context where `t` and `s` are the arguments
of function applications.
-/
mvarId.assign s
return true
@@ -752,10 +619,11 @@ def isDefEqMainImpl (t : Expr) (s : Expr) : DefEqM Bool := do
isDefEqMain ( instantiateMVarsS t) s
else if ( isAssignedMVar sFn) then
isDefEqMain t ( instantiateMVarsS s)
else
whenUndefDo (tryAssignMillerPattern tFn t s rfl) do
whenUndefDo (tryAssignMillerPattern sFn s t rfl) do
if let .fvar fvarId₁ := t then
else if ( tryAssignMillerPattern tFn t s rfl) then
return true
else if ( tryAssignMillerPattern sFn s t rfl) then
return true
else if let .fvar fvarId₁ := t then
unless ( read).zetaDelta do return false
let some val₁ fvarId₁.getValue? | return false
isDefEqMain val₁ s
@@ -766,19 +634,17 @@ def isDefEqMainImpl (t : Expr) (s : Expr) : DefEqM Bool := do
else
isDefEqApp tFn t s rfl
abbrev DefEqM.run (unify := true) (zetaDelta := true) (mvarsNew : Array MVarId := #[])
(mvarsToCheckType : Array MVarId := #[]) (x : DefEqM α) : SymM α := do
abbrev DefEqM.run (unify := true) (zetaDelta := true) (mvarsNew : Array MVarId := #[]) (x : DefEqM α) : SymM α := do
let lctx getLCtx
let lctxInitialNextIndex := lctx.decls.size
x { zetaDelta, lctxInitialNextIndex, unify, mvarsNew, mvarsToCheckType }
x { zetaDelta, lctxInitialNextIndex, unify, mvarsNew }
/--
A lightweight structural definitional equality for the symbolic simulation framework.
Unlike the full `isDefEq`, it avoids expensive operations while still supporting Miller pattern unification.
-/
public def isDefEqS (t : Expr) (s : Expr) (unify := true) (zetaDelta := true)
(mvarsNew : Array MVarId := #[]) (mvarsToCheckType : Array MVarId := #[]): SymM Bool := do
DefEqM.run (unify := unify) (zetaDelta := zetaDelta) (mvarsNew := mvarsNew) (mvarsToCheckType := mvarsToCheckType) do
public def isDefEqS (t : Expr) (s : Expr) (unify := true) (zetaDelta := true) (mvarsNew : Array MVarId := #[]) : SymM Bool := do
DefEqM.run (unify := unify) (zetaDelta := zetaDelta) (mvarsNew := mvarsNew) do
isDefEqMain t s
def noPending : UnifyM Bool := do
@@ -789,11 +655,7 @@ def instantiateLevelParamsS (e : Expr) (paramNames : List Name) (us : List Level
-- We do not assume `e` is maximally shared
shareCommon (e.instantiateLevelParams paramNames us)
inductive MkPreResultResult where
| failed
| success (mvarsToCheckType : Array MVarId)
def mkPreResult : UnifyM MkPreResultResult := do
def mkPreResult : UnifyM Unit := do
let us ( get).uAssignment.toList.mapM fun
| some val => pure val
| none => mkFreshLevelMVar
@@ -801,20 +663,9 @@ def mkPreResult : UnifyM MkPreResultResult := do
let varTypes := pattern.varTypes
let isInstance := pattern.isInstance
let eAssignment := ( get).eAssignment
let tPending := ( get).tPending
let mut args := #[]
let mut mvarsToCheckType := #[]
for h : i in *...eAssignment.size do
if let .some val := eAssignment[i] then
if tPending.contains i then
let type := varTypes[i]!
let type instantiateLevelParamsS type pattern.levelParams us
let type instantiateRevBetaS type args
let valType inferType val
-- **Note**: we have to use the default `isDefEq` because the type of `val`
-- is not necessarily normalized.
unless ( isDefEqTypes type valType) do
return .failed
args := args.push val
else
let type := varTypes[i]!
@@ -826,12 +677,8 @@ def mkPreResult : UnifyM MkPreResultResult := do
continue
let mvar mkFreshExprMVar type
let mvar shareCommon mvar
if let some mask := ( read).pattern.checkTypeMask? then
if mask[i]! then
mvarsToCheckType := mvarsToCheckType.push mvar.mvarId!
args := args.push mvar
modify fun s => { s with args, us }
return .success mvarsToCheckType
def processPendingLevel : UnifyM Bool := do
let uPending := ( get).uPending
@@ -857,7 +704,7 @@ def processPendingInst : UnifyM Bool := do
return false
return true
def processPendingExpr (mvarsToCheckType : Array MVarId) : UnifyM Bool := do
def processPendingExpr : UnifyM Bool := do
let ePending := ( get).ePending
if ePending.isEmpty then return true
let pattern := ( read).pattern
@@ -868,7 +715,7 @@ def processPendingExpr (mvarsToCheckType : Array MVarId) : UnifyM Bool := do
let mvarsNew := if unify then #[] else args.filterMap fun
| .mvar mvarId => some mvarId
| _ => none
DefEqM.run unify zetaDelta mvarsNew mvarsToCheckType do
DefEqM.run unify zetaDelta mvarsNew do
for (t, s) in ePending do
let t instantiateLevelParamsS t pattern.levelParams us
let t instantiateRevBetaS t args
@@ -876,11 +723,11 @@ def processPendingExpr (mvarsToCheckType : Array MVarId) : UnifyM Bool := do
return false
return true
def processPending (mvarsToCheckType : Array MVarId) : UnifyM Bool := do
def processPending : UnifyM Bool := do
if ( noPending) then
return true
else
processPendingLevel <&&> processPendingInst <&&> processPendingExpr mvarsToCheckType
processPendingLevel <&&> processPendingInst <&&> processPendingExpr
abbrev UnifyM.run (pattern : Pattern) (unify : Bool) (zetaDelta : Bool) (k : UnifyM α) : SymM α := do
let eAssignment := pattern.varTypes.map fun _ => none
@@ -898,11 +745,9 @@ def mkResult : UnifyM MatchUnifyResult := do
def main (p : Pattern) (e : Expr) (unify : Bool) (zetaDelta : Bool) : SymM (Option (MatchUnifyResult)) :=
UnifyM.run p unify zetaDelta do
unless ( process p.pattern e) do return none
match ( mkPreResult) with
| .failed => return none
| .success mvarsToCheckType =>
unless ( processPending mvarsToCheckType) do return none
return some ( mkResult)
mkPreResult
unless ( processPending) do return none
return some ( mkResult)
/--
Attempts to match expression `e` against pattern `p` using purely syntactic matching.

View File

@@ -7,15 +7,14 @@ module
prelude
public import Lean.Meta.Sym.SymM
import Lean.Meta.Sym.IsClass
import Lean.Meta.Sym.Util
import Lean.Meta.Transform
import Lean.Meta.Tactic.Grind.Util
namespace Lean.Meta.Sym
/--
Preprocesses types that used for pattern matching and unification.
-/
public def preprocessType (type : Expr) : MetaM Expr := do
let type Sym.unfoldReducible type
let type Grind.unfoldReducible type
let type Core.betaReduce type
zetaReduce type

View File

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Meta.Sym.Simp.App
public import Lean.Meta.Sym.Simp.Congr
public import Lean.Meta.Sym.Simp.CongrInfo
public import Lean.Meta.Sym.Simp.DiscrTree
public import Lean.Meta.Sym.Simp.Main
@@ -14,10 +14,3 @@ public import Lean.Meta.Sym.Simp.Rewrite
public import Lean.Meta.Sym.Simp.SimpM
public import Lean.Meta.Sym.Simp.Simproc
public import Lean.Meta.Sym.Simp.Theorems
public import Lean.Meta.Sym.Simp.Have
public import Lean.Meta.Sym.Simp.Lambda
public import Lean.Meta.Sym.Simp.Forall
public import Lean.Meta.Sym.Simp.Debug
public import Lean.Meta.Sym.Simp.EvalGround
public import Lean.Meta.Sym.Simp.Discharger
public import Lean.Meta.Sym.Simp.ControlFlow

View File

@@ -1,481 +0,0 @@
/-
Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Meta.Sym.Simp.SimpM
import Lean.Meta.SynthInstance
import Lean.Meta.Tactic.Simp.Types
import Lean.Meta.Sym.AlphaShareBuilder
import Lean.Meta.Sym.InferType
import Lean.Meta.Sym.Simp.Result
import Lean.Meta.Sym.Simp.CongrInfo
namespace Lean.Meta.Sym.Simp
open Internal
/-!
# 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:
- `fixedPrefix`: Use simple `congrArg`/`congrFun'`/`congr` for trailing arguments. We exploit
the fact that there are no dependent arguments in the suffix and use the cheaper `congrFun'`
instead of `congrFun`.
- `interlaced`: Mix rewritable and fixed arguments. It may have to use `congrFun` for fixed
dependent arguments.
- `congrTheorem`: Apply a pre-generated congruence theorem for dependent arguments
**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.
-/
/--
Helper function for constructing a congruence proof using `congrFun'`, `congrArg`, `congr`.
For the dependent case, use `mkCongrFun`
-/
public def mkCongr (e : Expr) (f a : Expr) (fr : Result) (ar : Result) (_ : e = .app f a) : SymM Result := do
let mkCongrPrefix (declName : Name) : SymM Expr := do
let α inferType a
let u getLevel α
let β inferType e
let v getLevel β
return mkApp2 (mkConst declName [u, v]) α β
match fr, ar with
| .rfl _, .rfl _ => return .rfl
| .step f' hf _, .rfl _ =>
let e' mkAppS f' a
let h := mkApp4 ( mkCongrPrefix ``congrFun') f f' hf a
return .step e' h
| .rfl _, .step a' ha _ =>
let e' mkAppS f a'
let h := mkApp4 ( mkCongrPrefix ``congrArg) a a' f ha
return .step e' h
| .step f' hf _, .step a' ha _ =>
let e' mkAppS f' a'
let h := mkApp6 ( mkCongrPrefix ``congr) f f' a a' hf ha
return .step e' h
/--
Returns a proof using `congrFun`
```
congrFun.{u, v} {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : f = g) (a : α) : f a = g a
```
-/
def mkCongrFun (e : Expr) (f a : Expr) (f' : Expr) (hf : Expr) (_ : e = .app f a) (done := false) : SymM Result := do
let .forallE x _ βx _ whnfD ( inferType f)
| throwError "failed to build congruence proof, function expected{indentExpr f}"
let α inferType a
let u getLevel α
let v getLevel ( inferType e)
let β := Lean.mkLambda x .default α βx
let e' mkAppS f' a
let h := mkApp6 (mkConst ``congrFun [u, v]) α β f f' hf a
return .step e' h done
/--
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.
-/
public def simpOverApplied (e : Expr) (numArgs : Nat) (simpFn : Expr SimpM Result) : SimpM Result := do
let rec visit (e : Expr) (i : Nat) : SimpM Result := do
if i == 0 then
simpFn e
else
let i := i - 1
match h : e with
| .app f a =>
let fr visit f i
let .forallE _ α β _ whnfD ( inferType f) | unreachable!
if !β.hasLooseBVars then
if ( isProp α) then
mkCongr e f a fr .rfl h
else
mkCongr e f a fr ( simp a) h
else match fr with
| .rfl _ => return .rfl
| .step f' hf _ => mkCongrFun e f a f' hf h
| _ => unreachable!
visit e numArgs
/--
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`**:
- `simpOverApplied`: Fully simplifies both base and extra arguments
- `propagateOverApplied`: Only simplifies base, appends extra arguments unchanged
-/
public def propagateOverApplied (e : Expr) (numArgs : Nat) (simpFn : Expr SimpM Result) : SimpM Result := do
let rec visit (e : Expr) (i : Nat) : SimpM Result := do
if i == 0 then
simpFn e
else
let i := i - 1
match h : e with
| .app f a =>
let r visit f i
match r with
| .rfl _ => return r
| .step f' hf done => mkCongrFun e f a f' hf h done
| _ => unreachable!
visit e numArgs
/--
Reduces `type` to weak head normal form and verifies it is a `forall` expression.
If `type` is already a `forall`, returns it unchanged (avoiding unnecessary work).
The result is shared via `share` to maintain maximal sharing invariants.
-/
def whnfToForall (type : Expr) : SymM Expr := do
if type.isForall then return type
let type whnfD type
unless type.isForall do throwError "function type expected{indentD type}"
share type
/--
Returns the type of an expression `e`. If `n > 0`, then `e` is an application
with at least `n` arguments. This function assumes the `n` trailing arguments are non-dependent.
Given `e` of the form `f a₁ a₂ ... aₙ`, the type of `e` is computed by
inferring the type of `f` and traversing the forall telescope.
We use this function to implement `congrFixedPrefix`. Recall that `inferType` is cached.
This function tries to maximize the likelihood of a cache hit. For example,
suppose `e` is `@HAdd.hAdd Nat Nat Nat instAdd 5` and `n = 1`. It is much more likely that
`@HAdd.hAdd Nat Nat Nat instAdd` is already in the cache than
`@HAdd.hAdd Nat Nat Nat instAdd 5`.
-/
def getFnType (e : Expr) (n : Nat) : SymM Expr := do
match n with
| 0 => inferType e
| n+1 =>
let type getFnType e.appFn! n
let .forallE _ _ β _ whnfToForall type | unreachable!
return β
/--
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.
-/
def simpFixedPrefix (e : Expr) (prefixSize : Nat) (suffixSize : Nat) : SimpM Result := do
let numArgs := e.getAppNumArgs
if numArgs prefixSize then
-- Nothing to be done
return .rfl
else if numArgs > prefixSize + suffixSize then
simpOverApplied e (numArgs - prefixSize - suffixSize) (main suffixSize)
else
main (numArgs - prefixSize) e
where
main (n : Nat) (e : Expr) : SimpM Result := do
return ( go n e).1
go (i : Nat) (e : Expr) : SimpM (Result × Expr) := do
if i == 0 then
return (.rfl, default)
else
let .app f a := e | unreachable!
let (hf, fType) go (i-1) f
match hf, ( simp a) with
| .rfl _, .rfl _ => return (.rfl, default)
| .step f' hf _, .rfl _ =>
let .forallE _ α β _ whnfToForall fType | unreachable!
let e' mkAppS f' a
let u getLevel α
let v getLevel β
let h := mkApp6 (mkConst ``congrFun' [u, v]) α β f f' hf a
return (.step e' h, β)
| .rfl _, .step a' ha _ =>
let fType getFnType f (i-1)
let .forallE _ α β _ whnfToForall fType | unreachable!
let e' mkAppS f a'
let u getLevel α
let v getLevel β
let h := mkApp6 (mkConst ``congrArg [u, v]) α β a a' f ha
return (.step e' h, β)
| .step f' hf _, .step a' ha _ =>
let .forallE _ α β _ whnfToForall fType | unreachable!
let e' mkAppS f' a'
let u getLevel α
let v getLevel β
let h := mkApp8 (mkConst ``congr [u, v]) α β f f' a a' hf ha
return (.step e' h, β)
/--
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.
-/
def simpInterlaced (e : Expr) (rewritable : Array Bool) : SimpM Result := do
let numArgs := e.getAppNumArgs
if h : numArgs = 0 then
-- Nothing to be done
return .rfl
else if h : numArgs > rewritable.size then
simpOverApplied e (numArgs - rewritable.size) (go rewritable.size · (Nat.le_refl _))
else
go numArgs e (by omega)
where
go (i : Nat) (e : Expr) (h : i rewritable.size) : SimpM Result := do
if h : i = 0 then
return .rfl
else
match h : e with
| .app f a =>
let fr go (i - 1) f (by omega)
if rewritable[i - 1] then
mkCongr e f a fr ( simp a) h
else match fr with
| .rfl _ => return .rfl
| .step f' hf _ => mkCongrFun e f a f' hf h
| _ => unreachable!
/--
Helper function used at `congrThm`. The idea is to initialize `argResults` lazily
when we get the first non-`.rfl` result.
-/
def pushResult (argResults : Array Result) (numEqs : Nat) (result : Result) : Array Result :=
match result with
| .rfl .. => if argResults.size > 0 then argResults.push result else argResults
| .step .. =>
if argResults.size < numEqs then
Array.replicate numEqs .rfl |>.push result
else
argResults.push result
/--
Simplifies arguments of a function application using a pre-generated congruence theorem.
This strategy is used for functions that have complex argument dependencies, particularly
those with proof arguments or `Decidable` instances. Unlike `congrFixedPrefix` and
`congrInterlaced`, which construct proofs on-the-fly using basic congruence lemmas
(`congrArg`, `congrFun`, `congrFun'`, `congr`), this function applies a specialized congruence theorem
that was pre-generated for the specific function being simplified.
See type `CongrArgKind`.
**Algorithm**:
1. Recursively simplify all `.eq` arguments (via `simpEqArgs`)
2. If all simplifications return `.rfl`, the overall result is `.rfl`
3. Otherwise, construct the final proof by:
- Starting with the congruence theorem's proof term
- Applying original arguments and their simplification results
- Re-synthesizing subsingleton instances when their dependencies change
- Removing unnecessary casts from the result
**Key examples**:
1. `ite`: Has type `{α : Sort u} → (c : Prop) → [Decidable c] → ααα`
- Argument kinds: `[.fixed, .eq, .subsingletonInst, .eq, .eq]`
- When simplifying `ite (x > 0) a b`, if `x > 0` simplifies to `true`, we must
re-synthesize `[Decidable true]` because the original `[Decidable (x > 0)]`
instance is no longer type-correct
2. `GetElem.getElem`: Has type
```
{coll : Type u} → {idx : Type v} → {elem : Type w} → {valid : coll → idx → Prop} →
[GetElem coll idx elem valid] → (xs : coll) → (i : idx) → valid xs i → elem
```
- The proof argument `valid xs i` depends on earlier arguments `xs` and `i`
- When `xs` or `i` are simplified, the proof is adjusted in the `rhs` of the auto-generated
theorem.
-/
def simpUsingCongrThm (e : Expr) (thm : CongrTheorem) : SimpM Result := do
let argKinds := thm.argKinds
/-
Constructs the non-`rfl` result. `argResults` contains the result for arguments with kind `.eq`.
There is at least one non-`rfl` result in `argResults`.
-/
let mkNonRflResult (argResults : Array Result) : SimpM Result := do
let mut proof := thm.proof
let mut type := thm.type
let mut j := 0 -- index at argResults
let mut subst := #[]
let args := e.getAppArgs
for arg in args, kind in argKinds do
proof := mkApp proof arg
type := type.bindingBody!
match kind with
| .fixed => subst := subst.push arg
| .cast => subst := subst.push arg
| .subsingletonInst =>
subst := subst.push arg
let clsNew := type.bindingDomain!.instantiateRev subst
let instNew if ( isDefEqI ( inferType arg) clsNew) then
pure arg
else
let .some val trySynthInstance clsNew | return .rfl
pure val
proof := mkApp proof instNew
subst := subst.push instNew
type := type.bindingBody!
| .eq =>
subst := subst.push arg
match argResults[j]! with
| .rfl _ =>
let h mkEqRefl arg
proof := mkApp2 proof arg h
subst := subst.push arg |>.push h
| .step arg' h _ =>
proof := mkApp2 proof arg' h
subst := subst.push arg' |>.push h
type := type.bindingBody!.bindingBody!
j := j + 1
| _ => unreachable!
let_expr Eq _ _ rhs := type | unreachable!
let rhs := rhs.instantiateRev subst
let hasCast := argKinds.any (· matches .cast)
let rhs if hasCast then Simp.removeUnnecessaryCasts rhs else pure rhs
let rhs share rhs
return .step rhs proof
/-
Recursively simplifies arguments of kind `.eq`. The array `argResults` is initialized lazily
as soon as the simplifier returns a non-`rfl` result for some arguments.
`numEqs` is the number of `.eq` arguments found so far.
-/
let rec simpEqArgs (e : Expr) (i : Nat) (numEqs : Nat) (argResults : Array Result) : SimpM Result := do
match e with
| .app f a =>
match argKinds[i]! with
| .subsingletonInst
| .fixed => simpEqArgs f (i-1) numEqs argResults
| .cast => simpEqArgs f (i-1) numEqs argResults
| .eq => simpEqArgs f (i-1) (numEqs+1) (pushResult argResults numEqs ( simp a))
| _ => unreachable!
| _ =>
if argResults.isEmpty then
return .rfl
else
mkNonRflResult argResults.reverse
let numArgs := e.getAppNumArgs
if numArgs > argKinds.size then
simpOverApplied e (numArgs - argKinds.size) (simpEqArgs · (argKinds.size - 1) 0 #[])
else if numArgs < argKinds.size then
/-
**Note**: under-applied case. This can be optimized, but this case is so
rare that it is not worth doing it. We just reuse `simpOverApplied`
-/
simpOverApplied e e.getAppNumArgs (fun _ => return .rfl)
else
simpEqArgs e (argKinds.size - 1) 0 #[]
/--
Main entry point for simplifying function application arguments.
Dispatches to the appropriate strategy based on the function's `CongrInfo`.
-/
public def simpAppArgs (e : Expr) : SimpM Result := do
let f := e.getAppFn
match ( getCongrInfo f) with
| .none => return .rfl
| .fixedPrefix prefixSize suffixSize => simpFixedPrefix e prefixSize suffixSize
| .interlaced rewritable => simpInterlaced e rewritable
| .congrTheorem thm => simpUsingCongrThm e thm
/--
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.
-/
public def simpAppArgRange (e : Expr) (start stop : Nat) : SimpM Result := do
let numArgs := e.getAppNumArgs
assert! start < stop
if numArgs < start then return .rfl
let numArgs := numArgs - start
let stop := stop - start
let rec visit (e : Expr) (i : Nat) : SimpM Result := do
if i == 0 then
return .rfl
let i := i - 1
match h : e with
| .app f a =>
let fr visit f i
let skip : SimpM Result := do
match fr with
| .rfl _ => return .rfl
| .step f' hf _ => mkCongrFun e f a f' hf h
if i < stop then
let .forallE _ α β _ whnfD ( inferType f) | unreachable!
if !β.hasLooseBVars then
if ( isProp α) then
mkCongr e f a fr .rfl h
else
mkCongr e f a fr ( simp a) h
else skip
else skip
| _ => unreachable!
visit e numArgs
end Lean.Meta.Sym.Simp

View File

@@ -0,0 +1,157 @@
/-
Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Meta.Sym.Simp.SimpM
import Lean.Meta.Sym.AlphaShareBuilder
import Lean.Meta.Sym.InferType
import Lean.Meta.Sym.Simp.Result
import Lean.Meta.Sym.Simp.CongrInfo
namespace Lean.Meta.Sym.Simp
open Internal
/-!
# 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:
- `fixedPrefix`: Use simple `congrArg`/`congrFun'`/`congr` for trailing arguments. We exploit
the fact that there are no dependent arguments in the suffix and use the cheaper `congrFun'`
instead of `congrFun`.
- `interlaced`: Mix rewritable and fixed arguments. It may have to use `congrFun` for fixed
dependent arguments.
- `congrTheorem`: Apply a pre-generated congruence theorem for dependent arguments
**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.
-/
/--
Helper function for constructing a congruence proof using `congrFun'`, `congrArg`, `congr`.
For the dependent case, use `mkCongrFun`
-/
def mkCongr (e : Expr) (f a : Expr) (fr : Result) (ar : Result) (_ : e = .app f a) : SymM Result := do
let mkCongrPrefix (declName : Name) : SymM Expr := do
let α inferType a
let u getLevel α
let β inferType e
let v getLevel β
return mkApp2 (mkConst declName [u, v]) α β
match fr, ar with
| .rfl _, .rfl _ => return .rfl
| .step f' hf _, .rfl _ =>
let e' mkAppS f' a
let h := mkApp4 ( mkCongrPrefix ``congrFun') f f' hf a
return .step e' h
| .rfl _, .step a' ha _ =>
let e' mkAppS f a'
let h := mkApp4 ( mkCongrPrefix ``congrArg) a a' f ha
return .step e' h
| .step f' hf _, .step a' ha _ =>
let e' mkAppS f' a'
let h := mkApp6 ( mkCongrPrefix ``congr) f f' a a' hf ha
return .step e' h
/--
Returns a proof using `congrFun`
```
congrFun.{u, v} {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : f = g) (a : α) : f a = g a
```
-/
def mkCongrFun (e : Expr) (f a : Expr) (f' : Expr) (hf : Expr) (_ : e = .app f a) : SymM Result := do
let .forallE x _ βx _ whnfD ( inferType f)
| throwError "failed to build congruence proof, function expected{indentExpr f}"
let α inferType a
let u getLevel α
let v getLevel ( inferType e)
let β := Lean.mkLambda x .default α βx
let e' mkAppS f' a
let h := mkApp6 (mkConst ``congrFun [u, v]) α β f f' hf a
return .step e' h
/--
Simplify arguments of a function application with a fixed prefix structure.
Recursively simplifies the trailing `suffixSize` arguments, leaving the first
`prefixSize` arguments unchanged.
-/
def congrFixedPrefix (e : Expr) (prefixSize : Nat) (suffixSize : Nat) : SimpM Result := do
let numArgs := e.getAppNumArgs
if numArgs prefixSize then
-- Nothing to be done
return .rfl
else if numArgs > prefixSize + suffixSize then
-- **TODO**: over-applied case
return .rfl
else
go numArgs e
where
go (i : Nat) (e : Expr) : SimpM Result := do
if i == prefixSize then
return .rfl
else
match h : e with
| .app f a => mkCongr e f a ( go (i - 1) f) ( simp a) h
| _ => unreachable!
/--
Simplify 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.
-/
def congrInterlaced (e : Expr) (rewritable : Array Bool) : SimpM Result := do
let numArgs := e.getAppNumArgs
if h : numArgs = 0 then
-- Nothing to be done
return .rfl
else if h : numArgs > rewritable.size then
-- **TODO**: over-applied case
return .rfl
else
go numArgs e (by omega)
where
go (i : Nat) (e : Expr) (h : i rewritable.size) : SimpM Result := do
if h : i = 0 then
return .rfl
else
match h : e with
| .app f a =>
let fr go (i - 1) f (by omega)
if rewritable[i - 1] then
mkCongr e f a fr ( simp a) h
else match fr with
| .rfl _ => return .rfl
| .step f' hf _ => mkCongrFun e f a f' hf h
| _ => unreachable!
/--
Simplify arguments using a pre-generated congruence theorem.
Used for functions with proof or `Decidable` arguments.
-/
def congrThm (_e : Expr) (_ : CongrTheorem) : SimpM Result := do
-- **TODO**
return .rfl
/--
Main entry point for simplifying function application arguments.
Dispatches to the appropriate strategy based on the function's `CongrInfo`.
-/
public def congrArgs (e : Expr) : SimpM Result := do
let f := e.getAppFn
match ( getCongrInfo f) with
| .none => return .rfl
| .fixedPrefix prefixSize suffixSize => congrFixedPrefix e prefixSize suffixSize
| .interlaced rewritable => congrInterlaced e rewritable
| .congrTheorem thm => congrThm e thm
end Lean.Meta.Sym.Simp

View File

@@ -1,146 +0,0 @@
/-
Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Meta.Sym.Simp.SimpM
import Lean.Meta.Sym.AlphaShareBuilder
import Lean.Meta.Sym.InstantiateS
import Lean.Meta.Sym.InferType
import Lean.Meta.Sym.Simp.App
import Lean.Meta.SynthInstance
import Lean.Meta.WHNF
import Lean.Meta.AppBuilder
import Init.Sym.Lemmas
namespace Lean.Meta.Sym.Simp
open Internal
/--
Simplifies a non-dependent `if-then-else` expression.
-/
def simpIte : Simproc := fun e => do
let numArgs := e.getAppNumArgs
if numArgs < 5 then return .rfl (done := true)
propagateOverApplied e (numArgs - 5) fun e => do
let_expr f@ite α c _ a b := e | return .rfl
match ( simp c) with
| .rfl _ =>
if c.isTrue then
return .step a <| mkApp3 (mkConst ``ite_true f.constLevels!) α a b
else if c.isFalse then
return .step b <| mkApp3 (mkConst ``ite_false f.constLevels!) α a b
else
return .rfl (done := true)
| .step c' h _ =>
if c'.isTrue then
return .step a <| mkApp (e.replaceFn ``ite_cond_eq_true) h
else if c'.isFalse then
return .step b <| mkApp (e.replaceFn ``ite_cond_eq_false) h
else
let .some inst' trySynthInstance (mkApp (mkConst ``Decidable) c') | return .rfl
let inst' shareCommon inst'
let e' := e.getBoundedAppFn 4
let e' mkAppS₄ e' c' inst' a b
let h' := mkApp3 (e.replaceFn ``Sym.ite_cond_congr) c' inst' h
return .step e' h' (done := true)
/--
Simplifies a dependent `if-then-else` expression.
-/
def simpDIte : Simproc := fun e => do
let numArgs := e.getAppNumArgs
if numArgs < 5 then return .rfl (done := true)
propagateOverApplied e (numArgs - 5) fun e => do
let_expr f@dite α c _ a b := e | return .rfl
match ( simp c) with
| .rfl _ =>
if c.isTrue then
let a' share <| a.betaRev #[mkConst ``True.intro]
return .step a' <| mkApp3 (mkConst ``dite_true f.constLevels!) α a b
else if c.isFalse then
let b' share <| b.betaRev #[mkConst ``not_false]
return .step b' <| mkApp3 (mkConst ``dite_false f.constLevels!) α a b
else
return .rfl (done := true)
| .step c' h _ =>
if c'.isTrue then
let h' shareCommon <| mkOfEqTrueCore c h
let a share <| a.betaRev #[h']
return .step a <| mkApp (e.replaceFn ``dite_cond_eq_true) h
else if c'.isFalse then
let h' shareCommon <| mkOfEqFalseCore c h
let b share <| b.betaRev #[h']
return .step b <| mkApp (e.replaceFn ``dite_cond_eq_false) h
else
let .some inst' trySynthInstance (mkApp (mkConst ``Decidable) c') | return .rfl
let inst' shareCommon inst'
let e' := e.getBoundedAppFn 4
let h shareCommon h
let a share <| mkLambda `h .default c' (a.betaRev #[mkApp4 (mkConst ``Eq.mpr_prop) c c' h (mkBVar 0)])
let b share <| mkLambda `h .default (mkNot c') (b.betaRev #[mkApp4 (mkConst ``Eq.mpr_not) c c' h (mkBVar 0)])
let e' mkAppS₄ e' c' inst' a b
let h' := mkApp3 (e.replaceFn ``Sym.dite_cond_congr) c' inst' h
return .step e' h' (done := true)
/--
Simplifies a `cond` expression (aka Boolean `if-then-else`).
-/
def simpCond : Simproc := fun e => do
let numArgs := e.getAppNumArgs
if numArgs < 4 then return .rfl (done := true)
propagateOverApplied e (numArgs - 4) fun e => do
let_expr f@cond α c a b := e | return .rfl
match ( simp c) with
| .rfl _ =>
if c.isConstOf ``true then
return .step a <| mkApp3 (mkConst ``cond_true f.constLevels!) α a b
else if c.isConstOf ``false then
return .step b <| mkApp3 (mkConst ``cond_false f.constLevels!) α a b
else
return .rfl (done := true)
| .step c' h _ =>
if c'.isConstOf ``true then
return .step a <| mkApp (e.replaceFn ``Sym.cond_cond_eq_true) h
else if c'.isConstOf ``false then
return .step b <| mkApp (e.replaceFn ``Sym.cond_cond_eq_false) h
else
let e' := e.getBoundedAppFn 3
let e' mkAppS₃ e' c' a b
let h' := mkApp2 (e.replaceFn ``Sym.cond_cond_congr) c' h
return .step e' h' (done := true)
/--
Simplifies a `match`-expression.
-/
def simpMatch (declName : Name) : Simproc := fun e => do
if let some e' reduceRecMatcher? e then
return .step e' ( mkEqRefl e')
let some info getMatcherInfo? declName
| return .rfl
-- **Note**: Simplify only the discriminants
let start := info.numParams + 1
let stop := start + info.numDiscrs
let r simpAppArgRange e start stop
match r with
| .step .. => return r
| _ => return .rfl (done := true)
/--
Simplifies control-flow expressions such as `if-then-else` and `match` expressions.
It visits only the conditions and discriminants.
-/
public def simpControl : Simproc := fun e => do
if !e.isApp then return .rfl
let .const declName _ := e.getAppFn | return .rfl
if declName == ``ite then
simpIte e
else if declName == ``cond then
simpCond e
else if declName == ``dite then
simpDIte e
else
simpMatch declName e
end Lean.Meta.Sym.Simp

View File

@@ -1,50 +0,0 @@
/-
Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Meta.Sym.Simp.SimpM
public import Lean.Meta.Sym.Simp.Discharger
import Lean.Meta.Sym.Simp.Theorems
import Lean.Meta.Sym.Simp.Rewrite
import Lean.Meta.Sym.Util
import Lean.Meta.Tactic.Util
import Lean.Meta.AppBuilder
namespace Lean.Meta.Sym
open Simp
/-!
Helper functions for debugging purposes and creating tests.
-/
public def mkSimprocFor (declNames : Array Name) (d : Discharger := dischargeNone) : MetaM Simproc := do
let mut thms : Theorems := {}
for declName in declNames do
thms := thms.insert ( mkTheoremFromDecl declName)
return thms.rewrite d
public def mkMethods (declNames : Array Name) : MetaM Methods := do
return { post := ( mkSimprocFor declNames) }
public def simpWith (k : Expr SymM Result) (mvarId : MVarId) : MetaM (Option MVarId) := SymM.run do
let mvarId preprocessMVar mvarId
let decl mvarId.getDecl
let target := decl.type
match ( k target) with
| .rfl _ => throwError "`Sym.simp` made no progress "
| .step target' h _ =>
let mvarNew mkFreshExprSyntheticOpaqueMVar target' decl.userName
let h mkAppM ``Eq.mpr #[h, mvarNew]
mvarId.assign h
if target'.isTrue then
mvarNew.mvarId!.assign (mkConst ``True.intro)
return none
else
return some mvarNew.mvarId!
public def simpGoal (declNames : Array Name) (mvarId : MVarId) : MetaM (Option MVarId) := SymM.run do mvarId.withContext do
let methods mkMethods declNames
simpWith (simp · methods) mvarId
end Lean.Meta.Sym

View File

@@ -1,121 +0,0 @@
/-
Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Meta.Sym.Simp.SimpM
import Lean.Meta.AppBuilder
namespace Lean.Meta.Sym.Simp
/-!
# Dischargers for Conditional Rewrite Rules
This module provides dischargers for handling conditional rewrite rules in `Sym.simp`.
A discharger attempts to prove side conditions that arise during rewriting.
## Overview
When applying a conditional rewrite rule `h : P → a = b`, the simplifier must prove
the precondition `P` before using the rule. A `Discharger` is a function that attempts
to construct such proofs.
**Example**: Consider the rewrite rule:
```
theorem div_self (n : Nat) (h : n ≠ 0) : n / n = 1
```
When simplifying `x / x`, the discharger must prove `x ≠ 0` to apply this rule.
## Design
Dischargers work by:
1. Attempting to simplify the side condition to `True`
2. If successful, extracting a proof from the simplification result
3. Returning `none` if the condition cannot be discharged
This integrates naturally with `Simproc`-based simplification.
## Important
When using dischargers that access new local declarations introduced when
visiting binders, it is the user's responsibility to set `wellBehavedMethods := false`.
This setting will instruct `simp` to discard the cache after visiting the binder's body.
-/
/--
A discharger attempts to prove propositions that arise as side conditions during rewriting.
Given a proposition `e : Prop`, returns:
- `some proof` if `e` can be proven
- `none` if `e` cannot be discharged
**Usage**: Dischargers are used by the simplifier when applying conditional rewrite rules.
-/
public abbrev Discharger := Expr SimpM (Option Expr)
def resultToOptionProof (e : Expr) (result : Result) : Option Expr :=
match result with
| .rfl _ => none
| .step e' h _ =>
if e'.isTrue then
some <| mkOfEqTrueCore e h
else
none
/--
Converts a simplification procedure into a discharger.
A `Simproc` can be used as a discharger by simplifying the side condition and
checking if it reduces to `True`. If so, the equality proof is converted to
a proof of the original proposition.
**Algorithm**:
1. Apply the simproc to the side condition `e`
2. If `e` simplifies to `True` (via proof `h : e = True`), return `ofEqTrue h : e`
3. Otherwise, return `none` (cannot discharge)
**Parameters**:
- `p`: A simplification procedure to use for discharging conditions
**Example**: If `p` simplifies `5 < 10` to `True` via proof `h : (5 < 10) = True`,
then `mkDischargerFromSimproc p` returns `ofEqTrue h : 5 < 10`.
-/
public def mkDischargerFromSimproc (p : Simproc) : Discharger := fun e => do
return resultToOptionProof e ( p e)
/--
The default discharger uses the simplifier itself to discharge side conditions.
This creates a natural recursive behavior: when applying conditional rules,
the simplifier is invoked to prove their preconditions. This is effective because:
1. **Ground terms**: Conditions like `5 ≠ 0` are evaluated by simprocs
2. **Recursive simplification**: Complex conditions are reduced to simpler ones
3. **Lemma application**: The simplifier can apply other rewrite rules to conditions
It ensures the cached results are discarded, and increases the discharge depth to avoid
infinite recursion.
-/
public def dischargeSimpSelf : Discharger := fun e => do
if ( readThe Context).dischargeDepth > ( getConfig).maxDischargeDepth then
return none
withoutModifyingCache do
withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do
return resultToOptionProof e ( simp e)
/--
A discharger that fails to prove any side condition.
This is used when conditional rewrite rules should not be applied. It immediately
returns `none` for all propositions, effectively disabling conditional rewriting.
**Use cases**:
- Testing: Isolating unconditional rewriting behavior
- Performance: Avoiding expensive discharge attempts when conditions are unlikely to hold
- Controlled rewriting: Explicitly disabling conditional rules in specific contexts
-/
public def dischargeNone : Discharger := fun _ =>
return none
end Lean.Meta.Sym.Simp

View File

@@ -7,7 +7,6 @@ module
prelude
public import Lean.Meta.Sym.Pattern
public import Lean.Meta.DiscrTree.Basic
import Lean.Meta.Sym.Offset
namespace Lean.Meta.Sym
open DiscrTree
@@ -78,7 +77,7 @@ def pushArgsUsingInfo (infos : Array ProofInstArgInfo) (i : Nat) (e : Expr) (tod
Computes the discrimination tree key for an expression and pushes its subterms onto the todo stack.
Returns `Key.star` for bound variables and `noindex`-annotated terms.
-/
def pushArgs (root : Bool) (fnInfos : AssocList Name ProofInstInfo) (todo : Array Expr) (e : Expr) : Key × Array Expr :=
def pushArgs (fnInfos : AssocList Name ProofInstInfo) (todo : Array Expr) (e : Expr) : Key × Array Expr :=
if hasNoindexAnnotation e then
(.star, todo)
else
@@ -88,15 +87,12 @@ def pushArgs (root : Bool) (fnInfos : AssocList Name ProofInstInfo) (todo : Arra
| .bvar _ => (.star, todo)
| .forallE _ d b _ => (.arrow, todo.push b |>.push d)
| .const declName _ =>
if !root && isOffset' declName e then
(.star, todo)
let numArgs := e.getAppNumArgs
let todo := if let some info := fnInfos.find? declName then
pushArgsUsingInfo info.argsInfo (numArgs - 1) e todo
else
let numArgs := e.getAppNumArgs
let todo := if let some info := fnInfos.find? declName then
pushArgsUsingInfo info.argsInfo (numArgs - 1) e todo
else
pushAllArgs e todo
(.const declName numArgs, todo)
pushAllArgs e todo
(.const declName numArgs, todo)
| .fvar fvarId =>
let numArgs := e.getAppNumArgs
let todo := pushAllArgs e todo
@@ -104,14 +100,14 @@ def pushArgs (root : Bool) (fnInfos : AssocList Name ProofInstInfo) (todo : Arra
| _ => (.other, todo)
/-- Work-list based traversal that builds the key sequence for a pattern. -/
partial def mkPathAux (root : Bool) (fnInfos : AssocList Name ProofInstInfo) (todo : Array Expr) (keys : Array Key) : Array Key :=
partial def mkPathAux (fnInfos : AssocList Name ProofInstInfo) (todo : Array Expr) (keys : Array Key) : Array Key :=
if todo.isEmpty then
keys
else
let e := todo.back!
let todo := todo.pop
let (k, todo) := pushArgs root fnInfos todo e
mkPathAux false fnInfos todo (keys.push k)
let (k, todo) := pushArgs fnInfos todo e
mkPathAux fnInfos todo (keys.push k)
def initCapacity := 8
@@ -119,7 +115,7 @@ def initCapacity := 8
public def Pattern.mkDiscrTreeKeys (p : Pattern) : Array Key :=
let todo : Array Expr := .mkEmpty initCapacity
let keys : Array Key := .mkEmpty initCapacity
mkPathAux true p.fnInfos (todo.push p.pattern) keys
mkPathAux p.fnInfos (todo.push p.pattern) keys
/-- Inserts a pattern into a discrimination tree, associating it with value `v`. -/
public def insertPattern [BEq α] (d : DiscrTree α) (p : Pattern) (v : α) : DiscrTree α :=

View File

@@ -1,567 +0,0 @@
/-
Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Meta.Sym.Simp.SimpM
import Init.Sym.Lemmas
import Init.Data.Int.Gcd
import Lean.Meta.Sym.LitValues
import Lean.Meta.Sym.AlphaShareBuilder
namespace Lean.Meta.Sym.Simp
/-!
# Ground Term Evaluation for `Sym.simp`
This module provides simplification procedures (`Simproc`) for evaluating ground terms
of builtin types. It is designed for the `Sym.Simp` simplifier and addresses
performance issues in the standard `Meta.Simp` simprocs.
## Design Differences from `Meta.Simp` Simprocs
### 1. Pure Value Extraction
It uses the pure `getValue?` functions defined in `Lean.Meta.Sym.LitValues`.
### 2. Proof by Definitional Equality
All evaluation steps produce `Eq.refl` proofs and. The kernel verifies correctness
by checking that the input and output are definitionally equal.
### 3. Specialized Lemmas for Predicates
Predicates (`<`, `≤`, `=`, etc.) use specialized lemmas that short-circuit the
standard `decide` proof chain:
```
-- Standard approach (Meta.Simp)
eq_true (of_decide_eq_true (h : decide (a < b) = true)) : (a < b) = True
-- Specialized lemma (Sym.Simp)
theorem Int.lt_eq_true (a b : Int) (h : decide (a < b) = true) : (a < b) = True :=
eq_true (of_decide_eq_true h)
```
The simproc applies the lemma directly with `rfl` for `h`:
```
Int.lt_eq_true 5 7 rfl : (5 < 7) = True
```
This avoids reconstructing `Decidable` instances at each call site.
### 4. Maximal Sharing
Results are passed through `share` to maintain the invariant that structurally
equal subterms have pointer equality. This enables O(1) cache lookup in the
simplifier.
### 5. Type Dispatch via `match_expr`
Operations dispatch on the type expression directly. It assumes non-standard instances are
**not** used.
**TODO**: additional bit-vector operations, `Char`, `String` support
-/
def skipIfUnchanged (e : Expr) (result : Result) : Result :=
match result with
| .step e' _ _ => if isSameExpr e e' then .rfl else result
| _ => result
abbrev evalUnary [ToExpr α] (toValue? : Expr Option α) (op : α α) (a : Expr) : SimpM Result := do
let some a := toValue? a | return .rfl
let e share <| toExpr (op a)
return .step e (mkApp2 (mkConst ``Eq.refl [1]) (ToExpr.toTypeExpr (α := α)) e) (done := true)
abbrev evalUnaryNat : (op : Nat Nat) (a : Expr) SimpM Result := evalUnary getNatValue?
abbrev evalUnaryInt : (op : Int Int) (a : Expr) SimpM Result := evalUnary getIntValue?
abbrev evalUnaryRat : (op : Rat Rat) (a : Expr) SimpM Result := evalUnary getRatValue?
abbrev evalUnaryUInt8 : (op : UInt8 UInt8) (a : Expr) SimpM Result := evalUnary getUInt8Value?
abbrev evalUnaryUInt16 : (op : UInt16 UInt16) (a : Expr) SimpM Result := evalUnary getUInt16Value?
abbrev evalUnaryUInt32 : (op : UInt32 UInt32) (a : Expr) SimpM Result := evalUnary getUInt32Value?
abbrev evalUnaryUInt64 : (op : UInt64 UInt64) (a : Expr) SimpM Result := evalUnary getUInt64Value?
abbrev evalUnaryInt8 : (op : Int8 Int8) (a : Expr) SimpM Result := evalUnary getInt8Value?
abbrev evalUnaryInt16 : (op : Int16 Int16) (a : Expr) SimpM Result := evalUnary getInt16Value?
abbrev evalUnaryInt32 : (op : Int32 Int32) (a : Expr) SimpM Result := evalUnary getInt32Value?
abbrev evalUnaryInt64 : (op : Int64 Int64) (a : Expr) SimpM Result := evalUnary getInt64Value?
abbrev evalUnaryFin' (op : {n : Nat} Fin n Fin n) (αExpr : Expr) (a : Expr) : SimpM Result := do
let some a := getFinValue? a | return .rfl
let e share <| toExpr (op a.val)
return .step e (mkApp2 (mkConst ``Eq.refl [1]) αExpr e) (done := true)
abbrev evalUnaryBitVec' (op : {n : Nat} BitVec n BitVec n) (αExpr : Expr) (a : Expr) : SimpM Result := do
let some a := getBitVecValue? a | return .rfl
let e share <| toExpr (op a.val)
return .step e (mkApp2 (mkConst ``Eq.refl [1]) αExpr e) (done := true)
abbrev evalBin [ToExpr α] (toValue? : Expr Option α) (op : α α α) (a b : Expr) : SimpM Result := do
let some a := toValue? a | return .rfl
let some b := toValue? b | return .rfl
let e share <| toExpr (op a b)
return .step e (mkApp2 (mkConst ``Eq.refl [1]) (ToExpr.toTypeExpr (α := α)) e) (done := true)
abbrev evalBinNat : (op : Nat Nat Nat) (a b : Expr) SimpM Result := evalBin getNatValue?
abbrev evalBinInt : (op : Int Int Int) (a b : Expr) SimpM Result := evalBin getIntValue?
abbrev evalBinRat : (op : Rat Rat Rat) (a b : Expr) SimpM Result := evalBin getRatValue?
abbrev evalBinUInt8 : (op : UInt8 UInt8 UInt8) (a b : Expr) SimpM Result := evalBin getUInt8Value?
abbrev evalBinUInt16 : (op : UInt16 UInt16 UInt16) (a b : Expr) SimpM Result := evalBin getUInt16Value?
abbrev evalBinUInt32 : (op : UInt32 UInt32 UInt32) (a b : Expr) SimpM Result := evalBin getUInt32Value?
abbrev evalBinUInt64 : (op : UInt64 UInt64 UInt64) (a b : Expr) SimpM Result := evalBin getUInt64Value?
abbrev evalBinInt8 : (op : Int8 Int8 Int8) (a b : Expr) SimpM Result := evalBin getInt8Value?
abbrev evalBinInt16 : (op : Int16 Int16 Int16) (a b : Expr) SimpM Result := evalBin getInt16Value?
abbrev evalBinInt32 : (op : Int32 Int32 Int32) (a b : Expr) SimpM Result := evalBin getInt32Value?
abbrev evalBinInt64 : (op : Int64 Int64 Int64) (a b : Expr) SimpM Result := evalBin getInt64Value?
abbrev evalBinFin' (op : {n : Nat} Fin n Fin n Fin n) (αExpr : Expr) (a b : Expr) : SimpM Result := do
let some a := getFinValue? a | return .rfl
let some b := getFinValue? b | return .rfl
if h : a.n = b.n then
let e share <| toExpr (op a.val (h b.val))
return .step e (mkApp2 (mkConst ``Eq.refl [1]) αExpr e) (done := true)
else
return .rfl
abbrev evalBinBitVec' (op : {n : Nat} BitVec n BitVec n BitVec n) (αExpr : Expr) (a b : Expr) : SimpM Result := do
let some a := getBitVecValue? a | return .rfl
let some b := getBitVecValue? b | return .rfl
if h : a.n = b.n then
let e share <| toExpr (op a.val (h b.val))
return .step e (mkApp2 (mkConst ``Eq.refl [1]) αExpr e) (done := true)
else
return .rfl
abbrev evalPowNat [ToExpr α] (maxExponent : Nat) (toValue? : Expr Option α) (op : α Nat α) (a b : Expr) : SimpM Result := do
let some a := toValue? a | return .rfl
let some b := getNatValue? b | return .rfl
if b > maxExponent then return .rfl
let e share <| toExpr (op a b)
return .step e (mkApp2 (mkConst ``Eq.refl [1]) (ToExpr.toTypeExpr (α := α)) e) (done := true)
abbrev evalPowInt [ToExpr α] (maxExponent : Nat) (toValue? : Expr Option α) (op : α Int α) (a b : Expr) : SimpM Result := do
let some a := toValue? a | return .rfl
let some b := getIntValue? b | return .rfl
if b.natAbs > maxExponent then return .rfl
let e share <| toExpr (op a b)
return .step e (mkApp2 (mkConst ``Eq.refl [1]) (ToExpr.toTypeExpr (α := α)) e) (done := true)
macro "declare_eval_bin" id:ident op:term : command =>
`(def $id:ident (α : Expr) (a b : Expr) : SimpM Result :=
match_expr α with
| Nat => evalBinNat $op a b
| Int => evalBinInt $op a b
| Rat => evalBinRat $op a b
| Fin _ => evalBinFin' $op α a b
| BitVec _ => evalBinBitVec' $op α a b
| UInt8 => evalBinUInt8 $op a b
| UInt16 => evalBinUInt16 $op a b
| UInt32 => evalBinUInt32 $op a b
| UInt64 => evalBinUInt64 $op a b
| Int8 => evalBinInt8 $op a b
| Int16 => evalBinInt16 $op a b
| Int32 => evalBinInt32 $op a b
| Int64 => evalBinInt64 $op a b
| _ => return .rfl
)
declare_eval_bin evalAdd (· + ·)
declare_eval_bin evalSub (· - ·)
declare_eval_bin evalMul (· * ·)
def evalDiv (e : Expr) (α : Expr) (a b : Expr) : SimpM Result :=
match_expr α with
| Nat => evalBinNat (. / .) a b
| Int => evalBinInt (. / .) a b
| Rat => return skipIfUnchanged e ( evalBinRat (. / .) a b)
| Fin _ => evalBinFin' (. / .) α a b
| BitVec _ => evalBinBitVec' (. / .) α a b
| UInt8 => evalBinUInt8 (. / .) a b
| UInt16 => evalBinUInt16 (. / .) a b
| UInt32 => evalBinUInt32 (. / .) a b
| UInt64 => evalBinUInt64 (. / .) a b
| Int8 => evalBinInt8 (. / .) a b
| Int16 => evalBinInt16 (. / .) a b
| Int32 => evalBinInt32 (. / .) a b
| Int64 => evalBinInt64 (. / .) a b
| _ => return .rfl
def evalMod (α : Expr) (a b : Expr) : SimpM Result :=
match_expr α with
| Nat => evalBinNat (· % ·) a b
| Int => evalBinInt (· % ·) a b
| Fin _ => evalBinFin' (· % ·) α a b
| BitVec _ => evalBinBitVec' (· % ·) α a b
| UInt8 => evalBinUInt8 (· % ·) a b
| UInt16 => evalBinUInt16 (· % ·) a b
| UInt32 => evalBinUInt32 (· % ·) a b
| UInt64 => evalBinUInt64 (· % ·) a b
| Int8 => evalBinInt8 (· % ·) a b
| Int16 => evalBinInt16 (· % ·) a b
| Int32 => evalBinInt32 (· % ·) a b
| Int64 => evalBinInt64 (· % ·) a b
| _ => return .rfl
def evalNeg (α : Expr) (a : Expr) : SimpM Result :=
match_expr α with
| Int => evalUnaryInt (- ·) a
| Rat => evalUnaryRat (- ·) a
| Fin _ => evalUnaryFin' (- ·) α a
| BitVec _ => evalUnaryBitVec' (- ·) α a
| UInt8 => evalUnaryUInt8 (- ·) a
| UInt16 => evalUnaryUInt16 (- ·) a
| UInt32 => evalUnaryUInt32 (- ·) a
| UInt64 => evalUnaryUInt64 (- ·) a
| Int8 => evalUnaryInt8 (- ·) a
| Int16 => evalUnaryInt16 (- ·) a
| Int32 => evalUnaryInt32 (- ·) a
| Int64 => evalUnaryInt64 (- ·) a
| _ => return .rfl
def evalComplement (α : Expr) (a : Expr) : SimpM Result :=
match_expr α with
| Int => evalUnaryInt (~~~ ·) a
| BitVec _ => evalUnaryBitVec' (~~~ ·) α a
| UInt8 => evalUnaryUInt8 (~~~ ·) a
| UInt16 => evalUnaryUInt16 (~~~ ·) a
| UInt32 => evalUnaryUInt32 (~~~ ·) a
| UInt64 => evalUnaryUInt64 (~~~ ·) a
| Int8 => evalUnaryInt8 (~~~ ·) a
| Int16 => evalUnaryInt16 (~~~ ·) a
| Int32 => evalUnaryInt32 (~~~ ·) a
| Int64 => evalUnaryInt64 (~~~ ·) a
| _ => return .rfl
def evalInv (α : Expr) (a : Expr) : SimpM Result :=
match_expr α with
| Rat => evalUnaryRat (· ⁻¹) a
| _ => return .rfl
macro "declare_eval_bin_bitwise" id:ident op:term : command =>
`(def $id:ident (α : Expr) (a b : Expr) : SimpM Result :=
match_expr α with
| Nat => evalBinNat $op a b
| Fin _ => evalBinFin' $op α a b
| BitVec _ => evalBinBitVec' $op α a b
| UInt8 => evalBinUInt8 $op a b
| UInt16 => evalBinUInt16 $op a b
| UInt32 => evalBinUInt32 $op a b
| UInt64 => evalBinUInt64 $op a b
| Int8 => evalBinInt8 $op a b
| Int16 => evalBinInt16 $op a b
| Int32 => evalBinInt32 $op a b
| Int64 => evalBinInt64 $op a b
| _ => return .rfl
)
declare_eval_bin_bitwise evalAnd (· &&& ·)
declare_eval_bin_bitwise evalOr (· ||| ·)
declare_eval_bin_bitwise evalXOr (· ^^^ ·)
def evalPow (maxExponent : Nat) (α β : Expr) (a b : Expr) : SimpM Result :=
match_expr β with
| Nat => match_expr α with
| Nat => evalPowNat maxExponent getNatValue? (· ^ ·) a b
| Int => evalPowNat maxExponent getIntValue? (· ^ ·) a b
| Rat => evalPowNat maxExponent getRatValue? (· ^ ·) a b
| UInt8 => evalPowNat maxExponent getUInt8Value? (· ^ ·) a b
| UInt16 => evalPowNat maxExponent getUInt16Value? (· ^ ·) a b
| UInt32 => evalPowNat maxExponent getUInt32Value? (· ^ ·) a b
| UInt64 => evalPowNat maxExponent getUInt64Value? (· ^ ·) a b
| Int8 => evalPowNat maxExponent getInt8Value? (· ^ ·) a b
| Int16 => evalPowNat maxExponent getInt16Value? (· ^ ·) a b
| Int32 => evalPowNat maxExponent getInt32Value? (· ^ ·) a b
| Int64 => evalPowNat maxExponent getInt64Value? (· ^ ·) a b
| _ => return .rfl
| Int => match_expr α with
| Rat => evalPowInt maxExponent getRatValue? (· ^ ·) a b
| _ => return .rfl
| _ => return .rfl
abbrev shift [ShiftLeft α] [ShiftRight α] (left : Bool) (a b : α) : α :=
if left then a <<< b else a >>> b
def evalShift (left : Bool) (α β : Expr) (a b : Expr) : SimpM Result :=
if isSameExpr α β then
match_expr α with
| Nat => evalBinNat (shift left) a b
| Fin _ => if left then evalBinFin' (· <<< ·) α a b else evalBinFin' (· >>> ·) α a b
| BitVec _ => if left then evalBinBitVec' (· <<< ·) α a b else evalBinBitVec' (· >>> ·) α a b
| UInt8 => evalBinUInt8 (shift left) a b
| UInt16 => evalBinUInt16 (shift left) a b
| UInt32 => evalBinUInt32 (shift left) a b
| UInt64 => evalBinUInt64 (shift left) a b
| Int8 => evalBinInt8 (shift left) a b
| Int16 => evalBinInt16 (shift left) a b
| Int32 => evalBinInt32 (shift left) a b
| Int64 => evalBinInt64 (shift left) a b
| _ => return .rfl
else
match_expr β with
| Nat =>
match_expr α with
| Int => do
let some a := getIntValue? a | return .rfl
let some b := getNatValue? b | return .rfl
let e := if left then a <<< b else a >>> b
let e share <| toExpr e
return .step e (mkApp2 (mkConst ``Eq.refl [1]) α e) (done := true)
| BitVec _ => do
let some a := getBitVecValue? a | return .rfl
let some b := getNatValue? b | return .rfl
let e := if left then a.val <<< b else a.val >>> b
let e share <| toExpr e
return .step e (mkApp2 (mkConst ``Eq.refl [1]) α e) (done := true)
| _ => return .rfl
| BitVec _ => do
let_expr BitVec _ := α | return .rfl
let some a := getBitVecValue? a | return .rfl
let some b := getBitVecValue? b | return .rfl
let e := if left then a.val <<< b.val else a.val >>> b.val
let e share <| toExpr e
return .step e (mkApp2 (mkConst ``Eq.refl [1]) α e) (done := true)
| _ => return .rfl
def evalIntGcd (a b : Expr) : SimpM Result := do
let some a := getIntValue? a | return .rfl
let some b := getIntValue? b | return .rfl
let e share <| toExpr (Int.gcd a b)
return .step e (mkApp2 (mkConst ``Eq.refl [1]) Nat.mkType e) (done := true)
def evalIntBMod (a b : Expr) : SimpM Result := do
let some a := getIntValue? a | return .rfl
let some b := getNatValue? b | return .rfl
let e share <| toExpr (Int.bmod a b)
return .step e (mkApp2 (mkConst ``Eq.refl [1]) Int.mkType e) (done := true)
def evalIntBDiv (a b : Expr) : SimpM Result := do
let some a := getIntValue? a | return .rfl
let some b := getNatValue? b | return .rfl
let e share <| toExpr (Int.bdiv a b)
return .step e (mkApp2 (mkConst ``Eq.refl [1]) Int.mkType e) (done := true)
abbrev evalBinPred (toValue? : Expr Option α) (trueThm falseThm : Expr) (op : α α Bool) (a b : Expr) : SimpM Result := do
let some va := toValue? a | return .rfl
let some vb := toValue? b | return .rfl
if op va vb then
let e share <| mkConst ``True
return .step e (mkApp3 trueThm a b eagerReflBoolTrue) (done := true)
else
let e share <| mkConst ``False
return .step e (mkApp3 falseThm a b eagerReflBoolFalse) (done := true)
def evalBitVecPred (n : Expr) (trueThm falseThm : Expr) (op : {n : Nat} BitVec n BitVec n Bool) (a b : Expr) : SimpM Result := do
let some va := getBitVecValue? a | return .rfl
let some vb := getBitVecValue? b | return .rfl
if h : va.n = vb.n then
if op va.val (h vb.val) then
let e share <| mkConst ``True
return .step e (mkApp4 trueThm n a b eagerReflBoolTrue) (done := true)
else
let e share <| mkConst ``False
return .step e (mkApp4 falseThm n a b eagerReflBoolFalse) (done := true)
else
return .rfl
def evalFinPred (n : Expr) (trueThm falseThm : Expr) (op : {n : Nat} Fin n Fin n Bool) (a b : Expr) : SimpM Result := do
let some va := getFinValue? a | return .rfl
let some vb := getFinValue? b | return .rfl
if h : va.n = vb.n then
if op va.val (h vb.val) then
let e share <| mkConst ``True
return .step e (mkApp4 trueThm n a b eagerReflBoolTrue) (done := true)
else
let e share <| mkConst ``False
return .step e (mkApp4 falseThm n a b eagerReflBoolFalse) (done := true)
else
return .rfl
open Lean.Sym
def evalLT (α : Expr) (a b : Expr) : SimpM Result :=
match_expr α with
| Nat => evalBinPred getNatValue? (mkConst ``Nat.lt_eq_true) (mkConst ``Nat.lt_eq_false) (. < .) a b
| Int => evalBinPred getIntValue? (mkConst ``Int.lt_eq_true) (mkConst ``Int.lt_eq_false) (. < .) a b
| Rat => evalBinPred getRatValue? (mkConst ``Rat.lt_eq_true) (mkConst ``Rat.lt_eq_false) (. < .) a b
| Int8 => evalBinPred getInt8Value? (mkConst ``Int8.lt_eq_true) (mkConst ``Int8.lt_eq_false) (. < .) a b
| Int16 => evalBinPred getInt16Value? (mkConst ``Int16.lt_eq_true) (mkConst ``Int16.lt_eq_false) (. < .) a b
| Int32 => evalBinPred getInt32Value? (mkConst ``Int32.lt_eq_true) (mkConst ``Int32.lt_eq_false) (. < .) a b
| Int64 => evalBinPred getInt64Value? (mkConst ``Int64.lt_eq_true) (mkConst ``Int64.lt_eq_false) (. < .) a b
| UInt8 => evalBinPred getUInt8Value? (mkConst ``UInt8.lt_eq_true) (mkConst ``UInt8.lt_eq_false) (. < .) a b
| UInt16 => evalBinPred getUInt16Value? (mkConst ``UInt16.lt_eq_true) (mkConst ``UInt16.lt_eq_false) (. < .) a b
| UInt32 => evalBinPred getUInt32Value? (mkConst ``UInt32.lt_eq_true) (mkConst ``UInt32.lt_eq_false) (. < .) a b
| UInt64 => evalBinPred getUInt64Value? (mkConst ``UInt64.lt_eq_true) (mkConst ``UInt64.lt_eq_false) (. < .) a b
| Fin n => evalFinPred n (mkConst ``Fin.lt_eq_true) (mkConst ``Fin.lt_eq_false) (. < .) a b
| BitVec n => evalBitVecPred n (mkConst ``BitVec.lt_eq_true) (mkConst ``BitVec.lt_eq_false) (. < .) a b
| String => evalBinPred getStringValue? (mkConst ``String.lt_eq_true) (mkConst ``String.lt_eq_false) (. < .) a b
| Char => evalBinPred getCharValue? (mkConst ``Char.lt_eq_true) (mkConst ``Char.lt_eq_false) (. < .) a b
| _ => return .rfl
def evalLE (α : Expr) (a b : Expr) : SimpM Result :=
match_expr α with
| Nat => evalBinPred getNatValue? (mkConst ``Nat.le_eq_true) (mkConst ``Nat.le_eq_false) (. .) a b
| Int => evalBinPred getIntValue? (mkConst ``Int.le_eq_true) (mkConst ``Int.le_eq_false) (. .) a b
| Rat => evalBinPred getRatValue? (mkConst ``Rat.le_eq_true) (mkConst ``Rat.le_eq_false) (. .) a b
| Int8 => evalBinPred getInt8Value? (mkConst ``Int8.le_eq_true) (mkConst ``Int8.le_eq_false) (. .) a b
| Int16 => evalBinPred getInt16Value? (mkConst ``Int16.le_eq_true) (mkConst ``Int16.le_eq_false) (. .) a b
| Int32 => evalBinPred getInt32Value? (mkConst ``Int32.le_eq_true) (mkConst ``Int32.le_eq_false) (. .) a b
| Int64 => evalBinPred getInt64Value? (mkConst ``Int64.le_eq_true) (mkConst ``Int64.le_eq_false) (. .) a b
| UInt8 => evalBinPred getUInt8Value? (mkConst ``UInt8.le_eq_true) (mkConst ``UInt8.le_eq_false) (. .) a b
| UInt16 => evalBinPred getUInt16Value? (mkConst ``UInt16.le_eq_true) (mkConst ``UInt16.le_eq_false) (. .) a b
| UInt32 => evalBinPred getUInt32Value? (mkConst ``UInt32.le_eq_true) (mkConst ``UInt32.le_eq_false) (. .) a b
| UInt64 => evalBinPred getUInt64Value? (mkConst ``UInt64.le_eq_true) (mkConst ``UInt64.le_eq_false) (. .) a b
| Fin n => evalFinPred n (mkConst ``Fin.le_eq_true) (mkConst ``Fin.le_eq_false) (. .) a b
| BitVec n => evalBitVecPred n (mkConst ``BitVec.le_eq_true) (mkConst ``BitVec.le_eq_false) (. .) a b
| String => evalBinPred getStringValue? (mkConst ``String.le_eq_true) (mkConst ``String.le_eq_false) (. .) a b
| Char => evalBinPred getCharValue? (mkConst ``Char.le_eq_true) (mkConst ``Char.le_eq_false) (. .) a b
| _ => return .rfl
def evalEq (α : Expr) (a b : Expr) : SimpM Result :=
if isSameExpr a b then do
let e share <| mkConst ``True
let u getLevel α
return .step e (mkApp2 (mkConst ``eq_self [u]) α a) (done := true)
else match_expr α with
| Nat => evalBinPred getNatValue? (mkConst ``Nat.eq_eq_true) (mkConst ``Nat.eq_eq_false) (. = .) a b
| Int => evalBinPred getIntValue? (mkConst ``Int.eq_eq_true) (mkConst ``Int.eq_eq_false) (. = .) a b
| Rat => evalBinPred getRatValue? (mkConst ``Rat.eq_eq_true) (mkConst ``Rat.eq_eq_false) (. = .) a b
| Int8 => evalBinPred getInt8Value? (mkConst ``Int8.eq_eq_true) (mkConst ``Int8.eq_eq_false) (. = .) a b
| Int16 => evalBinPred getInt16Value? (mkConst ``Int16.eq_eq_true) (mkConst ``Int16.eq_eq_false) (. = .) a b
| Int32 => evalBinPred getInt32Value? (mkConst ``Int32.eq_eq_true) (mkConst ``Int32.eq_eq_false) (. = .) a b
| Int64 => evalBinPred getInt64Value? (mkConst ``Int64.eq_eq_true) (mkConst ``Int64.eq_eq_false) (. = .) a b
| UInt8 => evalBinPred getUInt8Value? (mkConst ``UInt8.eq_eq_true) (mkConst ``UInt8.eq_eq_false) (. = .) a b
| UInt16 => evalBinPred getUInt16Value? (mkConst ``UInt16.eq_eq_true) (mkConst ``UInt16.eq_eq_false) (. = .) a b
| UInt32 => evalBinPred getUInt32Value? (mkConst ``UInt32.eq_eq_true) (mkConst ``UInt32.eq_eq_false) (. = .) a b
| UInt64 => evalBinPred getUInt64Value? (mkConst ``UInt64.eq_eq_true) (mkConst ``UInt64.eq_eq_false) (. = .) a b
| Fin n => evalFinPred n (mkConst ``Fin.eq_eq_true) (mkConst ``Fin.eq_eq_false) (. = .) a b
| BitVec n => evalBitVecPred n (mkConst ``BitVec.eq_eq_true) (mkConst ``BitVec.eq_eq_false) (. = .) a b
| Char => evalBinPred getCharValue? (mkConst ``Char.eq_eq_true) (mkConst ``Char.eq_eq_false) (. = .) a b
| String => evalBinPred getStringValue? (mkConst ``String.eq_eq_true) (mkConst ``String.eq_eq_false) (. = .) a b
| _ => return .rfl
def evalDvd (α : Expr) (a b : Expr) : SimpM Result :=
match_expr α with
| Nat => evalBinPred getNatValue? (mkConst ``Nat.dvd_eq_true) (mkConst ``Nat.dvd_eq_false) (. .) a b
| Int => evalBinPred getIntValue? (mkConst ``Int.dvd_eq_true) (mkConst ``Int.dvd_eq_false) (. .) a b
| _ => return .rfl
abbrev evalBinBoolPred (toValue? : Expr Option α) (op : α α Bool) (a b : Expr) : SimpM Result := do
let some va := toValue? a | return .rfl
let some vb := toValue? b | return .rfl
let r := op va vb
let e share (toExpr r)
return .step e (if r then eagerReflBoolTrue else eagerReflBoolFalse) (done := true)
abbrev evalBinBoolPredNat : (op : Nat Nat Bool) (a b : Expr) SimpM Result := evalBinBoolPred getNatValue?
abbrev evalBinBoolPredInt : (op : Int Int Bool) (a b : Expr) SimpM Result := evalBinBoolPred getIntValue?
abbrev evalBinBoolPredRat : (op : Rat Rat Bool) (a b : Expr) SimpM Result := evalBinBoolPred getRatValue?
abbrev evalBinBoolPredUInt8 : (op : UInt8 UInt8 Bool) (a b : Expr) SimpM Result := evalBinBoolPred getUInt8Value?
abbrev evalBinBoolPredUInt16 : (op : UInt16 UInt16 Bool) (a b : Expr) SimpM Result := evalBinBoolPred getUInt16Value?
abbrev evalBinBoolPredUInt32 : (op : UInt32 UInt32 Bool) (a b : Expr) SimpM Result := evalBinBoolPred getUInt32Value?
abbrev evalBinBoolPredUInt64 : (op : UInt64 UInt64 Bool) (a b : Expr) SimpM Result := evalBinBoolPred getUInt64Value?
abbrev evalBinBoolPredInt8 : (op : Int8 Int8 Bool) (a b : Expr) SimpM Result := evalBinBoolPred getInt8Value?
abbrev evalBinBoolPredInt16 : (op : Int16 Int16 Bool) (a b : Expr) SimpM Result := evalBinBoolPred getInt16Value?
abbrev evalBinBoolPredInt32 : (op : Int32 Int32 Bool) (a b : Expr) SimpM Result := evalBinBoolPred getInt32Value?
abbrev evalBinBoolPredInt64 : (op : Int64 Int64 Bool) (a b : Expr) SimpM Result := evalBinBoolPred getInt64Value?
abbrev evalBinBoolPredFin (op : {n : Nat} Fin n Fin n Bool) (a b : Expr) : SimpM Result := do
let some a := getFinValue? a | return .rfl
let some b := getFinValue? b | return .rfl
if h : a.n = b.n then
let r := op a.val (h b.val)
let e share (toExpr r)
return .step e (if r then eagerReflBoolTrue else eagerReflBoolFalse) (done := true)
else
return .rfl
abbrev evalBinBoolPredBitVec (op : {n : Nat} BitVec n BitVec n Bool) (a b : Expr) : SimpM Result := do
let some a := getBitVecValue? a | return .rfl
let some b := getBitVecValue? b | return .rfl
if h : a.n = b.n then
let r := op a.val (h b.val)
let e share (toExpr r)
return .step e (if r then eagerReflBoolTrue else eagerReflBoolFalse) (done := true)
else
return .rfl
macro "declare_eval_bin_bool_pred" id:ident op:term : command =>
`(def $id:ident (α : Expr) (a b : Expr) : SimpM Result :=
match_expr α with
| Nat => evalBinBoolPredNat $op a b
| Int => evalBinBoolPredInt $op a b
| Rat => evalBinBoolPredRat $op a b
| Fin _ => evalBinBoolPredFin $op a b
| BitVec _ => evalBinBoolPredBitVec $op a b
| UInt8 => evalBinBoolPredUInt8 $op a b
| UInt16 => evalBinBoolPredUInt16 $op a b
| UInt32 => evalBinBoolPredUInt32 $op a b
| UInt64 => evalBinBoolPredUInt64 $op a b
| Int8 => evalBinBoolPredInt8 $op a b
| Int16 => evalBinBoolPredInt16 $op a b
| Int32 => evalBinBoolPredInt32 $op a b
| Int64 => evalBinBoolPredInt64 $op a b
| _ => return .rfl
)
declare_eval_bin_bool_pred evalBEq (· == ·)
declare_eval_bin_bool_pred evalBNe (· != ·)
open Internal in
def evalNot (a : Expr) : SimpM Result :=
/-
**Note**: We added `evalNot` because some abbreviations expanded into `Not`s.
-/
match_expr a with
| True => return .step ( mkConstS ``False) (mkConst ``Sym.not_true_eq) (done := true)
| False => return .step ( mkConstS ``True) (mkConst ``Sym.not_false_eq) (done := true)
| _ => return .rfl
public structure EvalStepConfig where
maxExponent := 255
/--
Simplification procedure that evaluates ground terms of builtin types.
**Important:** This procedure assumes subterms have already been simplified. It evaluates
a single operation on literal arguments only. For example:
- `2 + 3` → evaluates to `5`
- `2 + (3 * 4)` → returns `.rfl` (the argument `3 * 4` is not a literal)
The simplifier is responsible for term traversal, ensuring subterms are reduced
before `evalGround` is called on the parent expression.
-/
public def evalGround (config : EvalStepConfig := {}) : Simproc := fun e =>
match_expr e with
| HAdd.hAdd α _ _ _ a b => evalAdd α a b
| HSub.hSub α _ _ _ a b => evalSub α a b
| HMul.hMul α _ _ _ a b => evalMul α a b
| HDiv.hDiv α _ _ _ a b => evalDiv e α a b
| HMod.hMod α _ _ _ a b => evalMod α a b
| HPow.hPow α β _ _ a b => evalPow config.maxExponent α β a b
| HAnd.hAnd α _ _ _ a b => evalAnd α a b
| HXor.hXor α _ _ _ a b => evalXOr α a b
| HOr.hOr α _ _ _ a b => evalOr α a b
| HShiftLeft.hShiftLeft α β _ _ a b => evalShift (left := true) α β a b
| HShiftRight.hShiftRight α β _ _ a b => evalShift (left := false) α β a b
| Inv.inv α _ a => evalInv α a
| Neg.neg α _ a => return skipIfUnchanged e ( evalNeg α a)
| Complement.complement α _ a => evalComplement α a
| Nat.gcd a b => evalBinNat Nat.gcd a b
| Nat.succ a => evalUnaryNat (· + 1) a
| Int.gcd a b => evalIntGcd a b
| Int.tdiv a b => evalBinInt Int.tdiv a b
| Int.fdiv a b => evalBinInt Int.fdiv a b
| Int.bdiv a b => evalIntBDiv a b
| Int.tmod a b => evalBinInt Int.tmod a b
| Int.fmod a b => evalBinInt Int.fmod a b
| Int.bmod a b => evalIntBMod a b
| LE.le α _ a b => evalLE α a b
| LT.lt α _ a b => evalLT α a b
| Dvd.dvd α _ a b => evalDvd α a b
| Eq α a b => evalEq α a b
| BEq.beq α _ a b => evalBEq α a b
| bne α _ a b => evalBNe α a b
| Not a => evalNot a
| _ => return .rfl
end Lean.Meta.Sym.Simp

View File

@@ -5,10 +5,49 @@ Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Meta.Sym.Simp.SimpM
import Lean.Meta.Sym.AlphaShareBuilder
public import Lean.Meta.Basic
import Lean.Meta.InferType
import Lean.Meta.Closure
import Lean.Meta.AppBuilder
namespace Lean.Meta.Sym.Simp
/--
Given `xs` containing free variables
`(x₁ : α₁) (x₂ : α₂[x₁]) ... (xₙ : αₙ[x₁, ..., x_{n-1}])`
and ` a type of the form [x₁, ..., xₙ]`,
creates the custom function extensionality theorem
```
(f g : (x₁ : α₁) (x₂ : α₂[x₁]) ... (xₙ : αₙ[x₁, ..., x_{n-1}]) β[x₁, ..., xₙ])
(h : x₁ ... xₙ, f x₁ ... xₙ = g x₁ ... xₙ),
f = g
```
The theorem has three arguments `f`, `g`, and `h`.
This auxiliary theorem is used by the simplifier when visiting lambda expressions.
-/
public def mkFunextFor (xs : Array Expr) (β : Expr) : MetaM Expr := do
let type mkForallFVars xs β
let v getLevel β
let w getLevel type
withLocalDeclD `f type fun f =>
withLocalDeclD `g type fun g => do
let eq := mkApp3 (mkConst ``Eq [v]) β (mkAppN f xs) (mkAppN g xs)
withLocalDeclD `h ( mkForallFVars xs eq) fun h => do
let eqv mkLambdaFVars #[f, g] ( mkForallFVars xs eq)
let quotEqv := mkApp2 (mkConst ``Quot [w]) type eqv
withLocalDeclD `f' quotEqv fun f' => do
let lift := mkApp6 (mkConst ``Quot.lift [w, v]) type eqv β
(mkLambda `f .default type (mkAppN (.bvar 0) xs))
(mkLambda `f .default type (mkLambda `g .default type (mkLambda `h .default (mkApp2 eqv (.bvar 1) (.bvar 0)) (mkAppN (.bvar 0) xs))))
f'
let extfunAppVal mkLambdaFVars (#[f'] ++ xs) lift
let extfunApp := extfunAppVal
let quotSound := mkApp5 (mkConst ``Quot.sound [w]) type eqv f g h
let Quot_mk_f := mkApp3 (mkConst ``Quot.mk [w]) type eqv f
let Quot_mk_g := mkApp3 (mkConst ``Quot.mk [w]) type eqv g
let result := mkApp6 (mkConst ``congrArg [w, w]) quotEqv type Quot_mk_f Quot_mk_g extfunApp quotSound
let result mkLambdaFVars #[f, g, h] result
return result
/--
Given `xs` containing free variables
`(x₁ : α₁) (x₂ : α₂[x₁]) ... (xₙ : αₙ[x₁, ..., x_{n-1}])`,
@@ -22,7 +61,7 @@ The theorem has three arguments `p`, `q`, and `h`.
This auxiliary theorem is used by the simplifier when visiting forall expressions.
The proof uses the approach used in `mkFunextFor` followed by an `Eq.ndrec`.
-/
def mkForallCongrFor (xs : Array Expr) : MetaM Expr := do
public def mkForallCongrFor (xs : Array Expr) : MetaM Expr := do
let prop := mkSort 0
let type mkForallFVars xs prop
let w getLevel type
@@ -51,54 +90,4 @@ def mkForallCongrFor (xs : Array Expr) : MetaM Expr := do
let result mkLambdaFVars #[p, q, h] result
return result
open Internal
public def simpArrow (e : Expr) : SimpM Result := do
let p := e.bindingDomain!
let q := e.bindingBody!
match ( simp p), ( simp q) with
| .rfl _, .rfl _ =>
return .rfl
| .step p' h _, .rfl _ =>
let u getLevel p
let v getLevel q
let e' e.updateForallS! p' q
return .step e' <| mkApp4 (mkConst ``implies_congr_left [u, v]) p p' q h
| .rfl _, .step q' h _ =>
let u getLevel p
let v getLevel q
let e' e.updateForallS! p q'
return .step e' <| mkApp4 (mkConst ``implies_congr_right [u, v]) p q q' h
| .step p' h₁ _, .step q' h₂ _ =>
let u getLevel p
let v getLevel q
let e' e.updateForallS! p' q'
return .step e' <| mkApp6 (mkConst ``implies_congr [u, v]) p p' q q' h₁ h₂
public def simpForall (e : Expr) : SimpM Result := do
if e.isArrow then
simpArrow e
else if ( isProp e) then
let n := getForallTelescopeSize e.bindingBody! 1
forallBoundedTelescope e n fun xs b => withoutModifyingCacheIfNotWellBehaved do
main xs b
else
return .rfl
where
main (xs : Array Expr) (b : Expr) : SimpM Result := do
match ( simp b) with
| .rfl _ => return .rfl
| .step b' h _ =>
let h mkLambdaFVars xs h
let e' shareCommonInc ( mkForallFVars xs b')
-- **Note**: consider caching the forall-congr theorems
let hcongr mkForallCongrFor xs
return .step e' (mkApp3 hcongr ( mkLambdaFVars xs b) ( mkLambdaFVars xs b') h)
-- **Note**: Optimize if this is quadratic in practice
getForallTelescopeSize (e : Expr) (n : Nat) : Nat :=
match e with
| .forallE _ _ b _ => if b.hasLooseBVar 0 then getForallTelescopeSize b (n+1) else n
| _ => n
end Lean.Meta.Sym.Simp

View File

@@ -1,438 +0,0 @@
/-
Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Meta.Sym.Simp.SimpM
import Lean.Meta.Sym.Simp.Lambda
import Lean.Meta.Sym.AlphaShareBuilder
import Lean.Meta.Sym.InstantiateS
import Lean.Meta.Sym.ReplaceS
import Lean.Meta.Sym.AbstractS
import Lean.Meta.Sym.InferType
import Lean.Meta.AppBuilder
import Lean.Meta.HaveTelescope
import Lean.Util.CollectFVars
namespace Lean.Meta.Sym.Simp
/-!
# Have-Telescope Simplification for Sym.simp
This module implements efficient simplification of `have`-telescopes (sequences of
non-dependent `let` bindings) in the symbolic simplifier. The key insight is to
transform telescopes into a "parallel" beta-application form, simplify the arguments
independently, and then convert back to `have` form.
## The Problem
Consider a `have`-telescope:
```
have x₁ := v₁
have x₂ := v₂[x₁]
...
have xₙ := vₙ[x₁, ..., xₙ₋₁]
b[x₁, ..., xₙ]
```
Naively generating proofs using `have_congr` leads to **quadratic kernel type-checking time**.
The issue is that when the kernel type-checks congruence proofs, it creates fresh free
variables for each binder, destroying sharing and generating O(n²) terms.
## The Solution: Virtual Parallelization
We transform the sequential `have` telescope into a parallel beta-application:
```
(fun x₁ x₂' ... xₙ' => b[x₁, x₂' x₁, ..., xₙ' (xₙ₋₁' ...)]) v₁ (fun x₁ => v₂[x₁]) ... (fun ... xₙ₋₁ => vₙ[..., xₙ₋₁])
```
Each `xᵢ'` is now a function that takes its dependencies as arguments. This form:
1. Is definitionally equal to the original (so conversion is free)
2. Enables independent simplification of each argument
3. Produces proofs that type-check in linear time using the existing efficient simplification procedure for lambdas.
## Algorithm Overview
1. **`toBetaApp`**: Transform `have`-telescope → parallel beta-application
- Track dependency graph: which `have` depends on which previous `have`s
- Convert each value `vᵢ[x₁, ..., xₖ]` to `(fun y₁ ... yₖ => vᵢ[y₁, ..., yₖ])`
- Build the body with appropriate applications
2. **`simpBetaApp`**: Simplify the beta-application using congruence lemmas
- Simplify function and each argument independently
- Generate proof using `congr`, `congrArg`, `congrFun'`
- This procedure is optimized for functions taking **many** arguments.
3. **`toHave`**: Convert simplified beta-application → `have`-telescope
- Reconstruct the `have` bindings from the lambda structure
- Apply each argument to recover original variable references
-/
/--
Result of converting a `have`-telescope to a parallel beta-application.
Given:
```
have x₁ := v₁; have x₂ := v₂[x₁]; ...; have xₙ := vₙ[...]; b[x₁, ..., xₙ]
```
We produce:
```
(fun x₁ x₂' ... xₙ' => b'[...]) v₁ (fun deps => v₂[deps]) ... (fun deps => vₙ[deps])
```
where each `xᵢ'` has type `deps_type → Tᵢ` and `b'` contains applications `xᵢ' (deps)`.
-/
structure ToBetaAppResult where
/-- Type of the input `have`-expression. -/
α : Expr
/-- The universe level of `α`. -/
u : Level
/-- The beta-application form: `(fun x₁ ... xₙ' => b') v₁ ... (fun deps => vₙ)`. -/
e : Expr
/-- Proof that the original expression equals `e` (by reflexivity + hints, since definitionally equal). -/
h : Expr
/--
Dependency information for each `have`.
`varDeps[i]` contains the indices of previous `have`s that `vᵢ` depends on.
Used by `toHave` to reconstruct the telescope.
-/
varDeps : Array (Array Nat)
/--
The function type: `T₁ → (deps₁ → T₂) → ... → (depsₙ₋₁ → Tₙ) → β`.
Used to compute universe levels for congruence lemmas.
-/
fType : Expr
deriving Inhabited
/--
Collect free variable Ids that appear in `e` and are tracked in `fvarIdToPos`,
sorted by their position in the telescope.
-/
def collectFVarIdsAt (e : Expr) (fvarIdToPos : FVarIdMap Nat) : Array FVarId :=
let s := collectFVars {} e
let fvarIds := s.fvarIds.filter (fvarIdToPos.contains ·)
fvarIds.qsort fun fvarId₁ fvarId₂ =>
let pos₁ := fvarIdToPos.get! fvarId₁
let pos₂ := fvarIdToPos.get! fvarId₂
pos₁ < pos₂
open Internal in
/--
Build a chain of arrows `α₁ → α₂ → ... → αₙ → β` using the `mkForallS` wrapper
(not `.forallE`) to preserve sharing.
-/
def mkArrows (αs : Array Expr) (β : Expr) : SymM Expr := do
go αs.size β (Nat.le_refl _)
where
go (i : Nat) (β : Expr) (h : i αs.size) : SymM Expr := do
match i with
| 0 => return β
| i+1 => go i ( mkForallS `a .default αs[i] β) (by omega)
/--
Transform a `have`-telescope into a parallel beta-application.
**Input**: `have x₁ := v₁; ...; have xₙ := vₙ; b`
**Output**: A `ToBetaAppResult` containing the equivalent beta-application.
## Transformation Details
For each `have xᵢ := vᵢ` where `vᵢ` depends on `xᵢ₁, ..., xᵢₖ` (aka `depsₖ`)
- The argument becomes `fun depsₖ => vᵢ[depsₖ]`
- The type becomes `Dᵢ₁ → ... → Dᵢₖ → Tᵢ` where `Dᵢⱼ` is the type of `xᵢⱼ`
- In the body, `xᵢ` is replaced by `xᵢ' sᵢ₁ ... sᵢₖ` where `sᵢⱼ` is the replacement for `xᵢⱼ`
The proof is `rfl` since the transformation is definitionally equal.
-/
def toBetaApp (haveExpr : Expr) : SymM ToBetaAppResult := do
go haveExpr #[] #[] #[] #[] #[] #[] {}
where
/--
Process the telescope recursively.
- `e`: Current expression (remaining telescope)
- `xs`: Original `have` binders (as fvars)
- `xs'`: New binders with function types (as fvars)
- `args`: Lambda-wrapped values `(fun deps => vᵢ)`
- `subst`: Substitution mapping old vars to applications `xᵢ' sᵢ₁ ... sᵢₖ`
- `types`: Types of the new binders
- `varDeps`: Dependency positions for each `have`
- `fvarIdToPos`: Map from fvar ID to telescope position
-/
go (e : Expr) (xs xs' args subst types : Array Expr) (varDeps : Array (Array Nat)) (fvarIdToPos : FVarIdMap Nat)
: SymM ToBetaAppResult := do
if let .letE n t v b (nondep := true) := e then
assert! !t.hasLooseBVars
withLocalDeclD n t fun x => do
let v := v.instantiateRev xs
let fvarIds := collectFVarIdsAt v fvarIdToPos
let varPos := fvarIds.map (fvarIdToPos.getD · 0)
let ys := fvarIds.map mkFVar
let arg mkLambdaFVars ys v
let t' share ( mkForallFVars ys t)
withLocalDeclD n t' fun x' => do
let args' := fvarIds.map fun fvarId =>
let pos := fvarIdToPos.get! fvarId
subst[pos]!
let v' share <| mkAppN x' args'
let fvarIdToPos := fvarIdToPos.insert x.fvarId! xs.size
go b (xs.push x) (xs'.push x') (args.push arg) (subst.push v') (types.push t') (varDeps.push varPos) fvarIdToPos
else
let e instantiateRevS e subst
let α inferType e
let u getLevel α
let fType mkArrows types α
let e mkLambdaFVarsS xs' e
let e share <| mkAppN e args
let eq := mkApp3 (mkConst ``Eq [u]) α haveExpr e
let h := mkApp2 (mkConst ``Eq.refl [u]) α haveExpr
let h := mkExpectedPropHint h eq
return { α, u, e, h, varDeps, fType }
/--
Strip `n` leading forall binders from a type.
Used to extract the actual type from a function type when we know the number of arguments.
-/
def consumeForallN (type : Expr) (n : Nat) : Expr :=
match n with
| 0 => type
| n+1 => consumeForallN type.bindingBody! n
open Internal in
/--
Eliminate auxiliary applications `xᵢ' sᵢ₁ ... sᵢₖ` in the body when converting back to `have` form.
After simplification, the body contains applications like `xᵢ' deps`. This function
replaces them with the actual `have` variables `xᵢ`.
**Parameters**:
- `e`: Expression containing `xᵢ' deps` applications (with loose bvars)
- `xs`: The actual `have` binders to substitute in
- `varDeps`: Dependency information for each variable
The function uses `replaceS` to traverse `e`, looking for applications of
bound variables at the expected positions.
-/
def elimAuxApps (e : Expr) (xs : Array Expr) (varDeps : Array (Array Nat)) : SymM Expr := do
let n := xs.size
replaceS e fun e offset => do
if offset >= e.looseBVarRange then
return some e
match e.getAppFn with
| .bvar idx =>
if _h : idx >= offset then
if _h : idx < offset + n then
let i := n - (idx - offset) - 1
let expectedNumArgs := varDeps[i]!.size
let numArgs := e.getAppNumArgs
if numArgs > expectedNumArgs then
return none -- Over-applied
else
assert! numArgs == expectedNumArgs
return xs[i]
else
mkBVarS (idx - n)
else
return some e
| _ => return none
/--
Convert a simplified beta-application back to `have` form.
**Input**: `(fun x₁ ... xₙ' => b') v₁ ... vₙ` with dependency info
**Output**: `have x₁ := w₁; ...; have xₙ := wₙ; b`
-/
def toHave (e : Expr) (varDeps : Array (Array Nat)) : SymM Expr :=
e.withApp fun f args => do
if _h : args.size varDeps.size then unreachable! else
let rec go (f : Expr) (xs : Array Expr) (i : Nat) : SymM Expr := do
if _h : i < args.size then
let .lam n t b _ := f | unreachable!
let varPos := varDeps[i]
let ys := varPos.map fun i => xs[i]!
let type := consumeForallN t varPos.size
let val share <| args[i].betaRev ys
withLetDecl (nondep := true) n type val fun x => do
go b (xs.push ( share x)) (i+1)
else
let f elimAuxApps f xs varDeps
let result mkLetFVars (generalizeNondepLet := false) (usedLetOnly := false) xs f
share result
go f #[] 0
/-- Result of extracting universe levels from a non-dependent function type. -/
structure GetUnivsResult where
/-- Universe level of each argument type. -/
argUnivs : Array Level
/-- Universe level of each partial application's result type. -/
fnUnivs : Array Level
/--
Extract universe levels from a function type for use in congruence lemmas.
For `α₁ → α₂ → ... → αₙ → β`:
- `argUnivs[i]` = universe of `αᵢ₊₁`
- `fnUnivs[i]` = universe of `αᵢ₊₁ → ... → β`
These are needed because `congr`, `congrArg`, and `congrFun'` are universe-polymorphic,
and we want to avoid a quadratic overhead.
-/
def getUnivs (fType : Expr) : SymM GetUnivsResult := do
go fType #[]
where
go (type : Expr) (argUnivs : Array Level) : SymM GetUnivsResult := do
match type with
| .forallE _ d b _ =>
go b (argUnivs.push ( getLevel d))
| _ =>
let mut v getLevel type
let mut i := argUnivs.size
let mut fnUnivs := #[]
while i > 0 do
i := i - 1
let u := argUnivs[i]!
v := mkLevelIMax' u v |>.normalize
fnUnivs := fnUnivs.push v
fnUnivs := fnUnivs.reverse
return { argUnivs, fnUnivs }
open Internal in
/--
Simplify a beta-application and generate a proof.
This is the core simplification routine. Given `f a₁ ... aₙ`, it:
1. Simplifies `f` and each `aᵢ` independently
2. Combines the results using appropriate congruence lemmas
## Congruence Lemma Selection
For each application `f a`:
- If both changed: use `congr : f = f' → a = a' → f a = f' a'`
- If only `f` changed: use `congrFun' : f = f' → f a = f' a`
- If only `a` changed: use `congrArg : a = a' → f a = f a'`
- If neither changed: return `.rfl`
-/
def simpBetaApp (e : Expr) (fType : Expr) (fnUnivs argUnivs : Array Level) : SimpM Result := do
return ( go e 0).1
where
go (e : Expr) (i : Nat) : SimpM (Result × Expr) := do
match e with
| .app f a =>
let (rf, fType) go f (i+1)
let r match rf, ( simp a) with
| .rfl _, .rfl _ =>
pure .rfl
| .step f' hf _, .rfl _ =>
let e' mkAppS f' a
let h := mkApp4 ( mkCongrPrefix ``congrFun' fType i) f f' hf a
pure <| .step e' h
| .rfl _, .step a' ha _ =>
let e' mkAppS f a'
let h := mkApp4 ( mkCongrPrefix ``congrArg fType i) a a' f ha
pure <| .step e' h
| .step f' hf _, .step a' ha _ =>
let e' mkAppS f' a'
let h := mkApp6 ( mkCongrPrefix ``congr fType i) f f' a a' hf ha
pure <| .step e' h
return (r, fType.bindingBody!)
| .lam .. => return ( simpLambda e, fType)
| _ => unreachable!
mkCongrPrefix (declName : Name) (fType : Expr) (i : Nat) : SymM Expr := do
let α := fType.bindingDomain!
let β := fType.bindingBody!
let u := argUnivs[i]!
let v := fnUnivs[i]!
return mkApp2 (mkConst declName [u, v]) α β
/-- Intermediate result for `have`-telescope simplification. -/
structure SimpHaveResult where
result : Result
α : Expr
u : Level
/--
Core implementation of `have`-telescope simplification.
## Algorithm
1. Convert the `have`-telescope to beta-application form (`toBetaApp`)
2. Simplify the beta-application (`simpBetaApp`)
3. If changed, convert back to `have` form (`toHave`)
4. Chain the proofs using transitivity
## Proof Structure
```
e₁ = e₂ (by rfl, definitional equality from toBetaApp)
e₂ = e₃ (from simpBetaApp)
e₃ = e₄ (by rfl, definitional equality from toHave)
─────────────────────────────────────────────────────────
e₁ = e₄ (by transitivity)
```
-/
def simpHaveCore (e : Expr) : SimpM SimpHaveResult := do
let e₁ := e
let r toBetaApp e₁
let e₂ := r.e
let { fnUnivs, argUnivs } getUnivs r.fType
match ( simpBetaApp e₂ r.fType fnUnivs argUnivs) with
| .rfl _ => return { result := .rfl, α := r.α, u := r.u }
| .step e₃ h _ =>
let h₁ := mkApp6 (mkConst ``Eq.trans [r.u]) r.α e₁ e₂ e₃ r.h h
let e₄ toHave e₃ r.varDeps
let eq := mkApp3 (mkConst ``Eq [r.u]) r.α e₃ e₄
let h₂ := mkApp2 (mkConst ``Eq.refl [r.u]) r.α e₃
let h₂ := mkExpectedPropHint h₂ eq
let h := mkApp6 (mkConst ``Eq.trans [r.u]) r.α e₁ e₃ e₄ h₁ h₂
return { result := .step e₄ h, α := r.α, u := r.u }
/--
Simplify a `have`-telescope.
This is the main entry point for `have`-telescope simplification in `Sym.simp`.
See module documentation for the algorithm overview.
-/
public def simpHave (e : Expr) : SimpM Result := do
return ( simpHaveCore e).result
/--
Simplify a `have`-telescope and eliminate unused bindings.
This combines simplification with dead variable elimination in a single pass,
avoiding quadratic behavior from multiple passes.
-/
public def simpHaveAndZetaUnused (e₁ : Expr) : SimpM Result := do
let r simpHaveCore e₁
match r.result with
| .rfl _ =>
let e₂ zetaUnused e₁
if isSameExpr e₁ e₂ then
return .rfl
else
let h := mkApp2 (mkConst ``Eq.refl [r.u]) r.α e₂
return .step e₂ h
| .step e₂ h _ =>
let e₃ zetaUnused e₂
if isSameExpr e₂ e₃ then
return r.result
else
let h := mkApp6 (mkConst ``Eq.trans [r.u]) r.α e₁ e₂ e₃ h
(mkApp2 (mkConst ``Eq.refl [r.u]) r.α e₃)
return .step e₃ h
public def simpLet (e : Expr) : SimpM Result := do
if !e.letNondep! then
/-
**Note**: We don't do anything if it is a dependent `let`.
Users may decide to `zeta`-expand them or apply `letToHave` at `pre`/`post`.
-/
return .rfl
else
simpHaveAndZetaUnused e
end Lean.Meta.Sym.Simp

View File

@@ -1,72 +0,0 @@
/-
Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Lean.Meta.Sym.Simp.SimpM
import Lean.Meta.Closure
namespace Lean.Meta.Sym.Simp
/--
Given `xs` containing free variables
`(x₁ : α₁) (x₂ : α₂[x₁]) ... (xₙ : αₙ[x₁, ..., x_{n-1}])`
and `β` a type of the form `β[x₁, ..., xₙ]`,
creates the custom function extensionality theorem
```
∀ (f g : (x₁ : α₁) → (x₂ : α₂[x₁]) → ... → (xₙ : αₙ[x₁, ..., x_{n-1}]) → β[x₁, ..., xₙ])
(h : ∀ x₁ ... xₙ, f x₁ ... xₙ = g x₁ ... xₙ),
f = g
```
The theorem has three arguments `f`, `g`, and `h`.
This auxiliary theorem is used by the simplifier when visiting lambda expressions.
-/
def mkFunextFor (xs : Array Expr) (β : Expr) : MetaM Expr := do
let type mkForallFVars xs β
let v getLevel β
let w getLevel type
withLocalDeclD `f type fun f =>
withLocalDeclD `g type fun g => do
let eq := mkApp3 (mkConst ``Eq [v]) β (mkAppN f xs) (mkAppN g xs)
withLocalDeclD `h ( mkForallFVars xs eq) fun h => do
let eqv mkLambdaFVars #[f, g] ( mkForallFVars xs eq)
let quotEqv := mkApp2 (mkConst ``Quot [w]) type eqv
withLocalDeclD `f' quotEqv fun f' => do
let lift := mkApp6 (mkConst ``Quot.lift [w, v]) type eqv β
(mkLambda `f .default type (mkAppN (.bvar 0) xs))
(mkLambda `f .default type (mkLambda `g .default type (mkLambda `h .default (mkApp2 eqv (.bvar 1) (.bvar 0)) (mkAppN (.bvar 0) xs))))
f'
let extfunAppVal mkLambdaFVars (#[f'] ++ xs) lift
let extfunApp := extfunAppVal
let quotSound := mkApp5 (mkConst ``Quot.sound [w]) type eqv f g h
let Quot_mk_f := mkApp3 (mkConst ``Quot.mk [w]) type eqv f
let Quot_mk_g := mkApp3 (mkConst ``Quot.mk [w]) type eqv g
let result := mkApp6 (mkConst ``congrArg [w, w]) quotEqv type Quot_mk_f Quot_mk_g extfunApp quotSound
let result mkLambdaFVars #[f, g, h] result
return result
public def simpLambda (e : Expr) : SimpM Result := do
lambdaTelescope e fun xs b => withoutModifyingCacheIfNotWellBehaved do
main xs b
where
main (xs : Array Expr) (b : Expr) : SimpM Result := do
match ( simp b) with
| .rfl _ => return .rfl
| .step b' h _ =>
let h mkLambdaFVars xs h
let e' shareCommonInc ( mkLambdaFVars xs b')
let funext getFunext xs b
return .step e' (mkApp3 funext e e' h)
getFunext (xs : Array Expr) (b : Expr) : SimpM Expr := do
let key inferType e
if let some h := ( get).funext.find? { expr := key } then
return h
else
let β inferType b
let h mkFunextFor xs β
modify fun s => { s with funext := s.funext.insert { expr := key } h }
return h
end Lean.Meta.Sym.Simp

View File

@@ -6,16 +6,103 @@ Authors: Leonardo de Moura
module
prelude
public import Lean.Meta.Sym.Simp.SimpM
import Lean.Meta.MonadSimp
import Lean.Meta.HaveTelescope
import Lean.Meta.Sym.AlphaShareBuilder
import Lean.Meta.Sym.InferType
import Lean.Meta.Sym.Simp.Result
import Lean.Meta.Sym.Simp.Simproc
import Lean.Meta.Sym.Simp.App
import Lean.Meta.Sym.Simp.Have
import Lean.Meta.Sym.Simp.Lambda
import Lean.Meta.Sym.Simp.Forall
import Lean.Meta.Sym.Simp.Congr
import Lean.Meta.Sym.Simp.Funext
namespace Lean.Meta.Sym.Simp
open Internal
instance : MonadSimp SimpM where
dsimp e := return e
withNewLemmas _ k := k
simp e := do match ( simp ( share e)) with
| .rfl _ => return .rfl
| .step e' h _ => return .step e' h
def simpLambda (e : Expr) : SimpM Result := do
lambdaTelescope e fun xs b => do
match ( simp b) with
| .rfl _ => return .rfl
| .step b' h _ =>
let h mkLambdaFVars xs h
let e' shareCommonInc ( mkLambdaFVars xs b')
let funext getFunext xs b
return .step e' (mkApp3 funext e e' h)
where
getFunext (xs : Array Expr) (b : Expr) : SimpM Expr := do
let key inferType e
if let some h := ( get).funext.find? { expr := key } then
return h
else
let β inferType b
let h mkFunextFor xs β
modify fun s => { s with funext := s.funext.insert { expr := key } h }
return h
def simpArrow (e : Expr) : SimpM Result := do
let p := e.bindingDomain!
let q := e.bindingBody!
match ( simp p), ( simp q) with
| .rfl _, .rfl _ =>
return .rfl
| .step p' h _, .rfl _ =>
let u getLevel p
let v getLevel q
let e' e.updateForallS! p' q
return .step e' <| mkApp4 (mkConst ``implies_congr_left [u, v]) p p' q h
| .rfl _, .step q' h _ =>
let u getLevel p
let v getLevel q
let e' e.updateForallS! p q'
return .step e' <| mkApp4 (mkConst ``implies_congr_right [u, v]) p q q' h
| .step p' h₁ _, .step q' h₂ _ =>
let u getLevel p
let v getLevel q
let e' e.updateForallS! p' q'
return .step e' <| mkApp6 (mkConst ``implies_congr [u, v]) p p' q q' h₁ h₂
def simpForall (e : Expr) : SimpM Result := do
if e.isArrow then
simpArrow e
else if ( isProp e) then
let n := getForallTelescopeSize e.bindingBody! 1
forallBoundedTelescope e n fun xs b => do
match ( simp b) with
| .rfl _ => return .rfl
| .step b' h _ =>
let h mkLambdaFVars xs h
let e' shareCommonInc ( mkForallFVars xs b')
-- **Note**: consider caching the forall-congr theorems
let hcongr mkForallCongrFor xs
return .step e' (mkApp3 hcongr ( mkLambdaFVars xs b) ( mkLambdaFVars xs b') h)
else
return .rfl
where
-- **Note**: Optimize if this is quadratic in practice
getForallTelescopeSize (e : Expr) (n : Nat) : Nat :=
match e with
| .forallE _ _ b _ => if b.hasLooseBVar 0 then getForallTelescopeSize b (n+1) else n
| _ => n
def simpLet (e : Expr) : SimpM Result := do
if !e.letNondep! then
/-
**Note**: We don't do anything if it is a dependent `let`.
Users may decide to `zeta`-expand them or apply `letToHave` at `pre`/`post`.
-/
return .rfl
else match ( Meta.simpHaveTelescope e) with
| .rfl => return .rfl
| .step e' h => return .step ( shareCommon e') h
def simpApp (e : Expr) : SimpM Result := do
congrArgs e
def simpStep : Simproc := fun e => do
match e with
| .lit _ | .sort _ | .bvar _ | .const .. | .fvar _ | .mvar _ => return .rfl
@@ -29,7 +116,7 @@ def simpStep : Simproc := fun e => do
| .lam .. => simpLambda e
| .forallE .. => simpForall e
| .letE .. => simpLet e
| .app .. => simpAppArgs e
| .app .. => simpApp e
abbrev cacheResult (e : Expr) (r : Result) : SimpM Result := do
modify fun s => { s with cache := s.cache.insert { expr := e } r }

View File

@@ -8,8 +8,6 @@ prelude
public import Lean.Meta.Sym.Simp.SimpM
public import Lean.Meta.Sym.Simp.Simproc
public import Lean.Meta.Sym.Simp.Theorems
public import Lean.Meta.Sym.Simp.App
public import Lean.Meta.Sym.Simp.Discharger
import Lean.Meta.Sym.InstantiateS
import Lean.Meta.Sym.Simp.DiscrTree
namespace Lean.Meta.Sym.Simp
@@ -29,35 +27,20 @@ def mkValue (expr : Expr) (pattern : Pattern) (result : MatchUnifyResult) : Expr
/--
Tries to rewrite `e` using the given theorem.
-/
public def Theorem.rewrite (thm : Theorem) (e : Expr) (d : Discharger := dischargeNone) : SimpM Result := do
public def Theorem.rewrite (thm : Theorem) (e : Expr) : SimpM Result := do
if let some result thm.pattern.match? e then
-- **Note**: Potential optimization: check whether pattern covers all variables.
for arg in result.args do
let .mvar mvarId := arg | pure ()
unless ( mvarId.isAssigned) do
let decl mvarId.getDecl
if let some val d decl.type then
mvarId.assign val
else
-- **Note**: Failed to discharge hypothesis.
return .rfl
let proof := mkValue thm.expr thm.pattern result
let rhs := thm.rhs.instantiateLevelParams thm.pattern.levelParams result.us
let rhs shareCommonInc rhs
let expr instantiateRevBetaS rhs result.args
if isSameExpr e expr then
return .rfl
else
return .step expr proof
return .step expr proof
else
return .rfl
public def Theorems.rewrite (thms : Theorems) (d : Discharger := dischargeNone) : Simproc := fun e => do
for (thm, numExtra) in thms.getMatchWithExtra e do
let result if numExtra == 0 then
thm.rewrite e d
else
simpOverApplied e numExtra (thm.rewrite · d)
public def Theorems.rewrite (thms : Theorems) : Simproc := fun e => do
-- **TODO**: over-applied terms
for thm in thms.getMatch e do
let result thm.rewrite e
if !result.isRfl then
return result
return .rfl

View File

@@ -101,12 +101,8 @@ invalidating the cache and causing O(2^n) behavior on conditional trees.
/-- Configuration options for the structural simplifier. -/
structure Config where
/-- Maximum number of steps that can be performed by the simplifier. -/
maxSteps : Nat := 1000
/--
Maximum depth of reentrant simplifier calls through dischargers.
Prevents infinite loops when conditional rewrite rules trigger recursive discharge attempts.
-/
maxDischargeDepth : Nat := 2
maxSteps : Nat := 0
-- **TODO**: many are still missing
/--
The result of simplifying an expression `e`.
@@ -153,7 +149,6 @@ inductive Result where
Simplified to `e'` with proof `proof : e = e'`.
If `done = true`, skip recursive simplification of `e'`. -/
| step (e' : Expr) (proof : Expr) (done : Bool := false)
deriving Inhabited
private opaque MethodsRefPointed : NonemptyType.{0}
def MethodsRef : Type := MethodsRefPointed.type
@@ -166,7 +161,6 @@ structure Context where
/-- Size of the local context when simplification started.
Used to determine which free variables were introduced during simplification. -/
initialLCtxSize : Nat
dischargeDepth : Nat := 0
/-- Cache mapping expressions (by pointer equality) to their simplified results. -/
abbrev Cache := PHashMap ExprPtr Result
@@ -197,13 +191,14 @@ abbrev Simproc := Expr → SimpM Result
structure Methods where
pre : Simproc := fun _ => return .rfl
post : Simproc := fun _ => return .rfl
discharge? : Expr SimpM (Option Expr) := fun _ => return none
/--
`wellBehavedMethods` must **not** be set to `true` IF their behavior
depends on new hypotheses in the local context. For example, for applying
conditional rewrite rules.
`wellBehavedDischarge` must **not** be set to `true` IF `discharge?`
access local declarations with index >= `Context.lctxInitIndices` when
`contextual := false`.
Reason: it would prevent us from aggressively caching `simp` results.
-/
wellBehavedMethods : Bool := true
wellBehavedDischarge : Bool := true
deriving Inhabited
unsafe def Methods.toMethodsRefImpl (m : Methods) : MethodsRef :=
@@ -241,13 +236,6 @@ abbrev pre : Simproc := fun e => do
abbrev post : Simproc := fun e => do
( getMethods).post e
abbrev withoutModifyingCache (k : SimpM α) : SimpM α := do
let cache getCache
try k finally modify fun s => { s with cache }
abbrev withoutModifyingCacheIfNotWellBehaved (k : SimpM α) : SimpM α := do
if ( getMethods).wellBehavedMethods then k else withoutModifyingCache k
end Simp
abbrev simp (e : Expr) (methods : Simp.Methods := {}) (config : Simp.Config := {}) : SymM Simp.Result := do

View File

@@ -38,9 +38,6 @@ def Theorems.insert (thms : Theorems) (thm : Theorem) : Theorems :=
def Theorems.getMatch (thms : Theorems) (e : Expr) : Array Theorem :=
Sym.getMatch thms.thms e
def Theorems.getMatchWithExtra (thms : Theorems) (e : Expr) : Array (Theorem × Nat) :=
Sym.getMatchWithExtra thms.thms e
def mkTheoremFromDecl (declName : Name) : MetaM Theorem := do
let (pattern, rhs) mkEqPatternFromDecl declName
return { expr := mkConst declName, pattern, rhs }

View File

@@ -6,55 +6,13 @@ Authors: Leonardo de Moura
module
prelude
public import Lean.Meta.Sym.SymM
public import Lean.Meta.Transform
import Init.Grind.Util
import Lean.Meta.WHNF
namespace Lean.Meta.Sym
/--
Returns `true` if `declName` is the name of a grind helper declaration that
should not be unfolded by `unfoldReducible`.
-/
def isGrindGadget (declName : Name) : Bool :=
declName == ``Grind.EqMatch
/--
Auxiliary function for implementing `unfoldReducible` and `unfoldReducibleSimproc`.
Performs a single step.
-/
public def unfoldReducibleStep (e : Expr) : MetaM TransformStep := do
let .const declName _ := e.getAppFn | return .continue
unless ( isReducible declName) do return .continue
if isGrindGadget declName then return .continue
-- See comment at isUnfoldReducibleTarget.
if ( getEnv).isProjectionFn declName then return .continue
let some v unfoldDefinition? e | return .continue
return .visit v
def isUnfoldReducibleTarget (e : Expr) : CoreM Bool := do
let env getEnv
return Option.isSome <| e.find? fun e => Id.run do
let .const declName _ := e | return false
if getReducibilityStatusCore env declName matches .reducible then
-- Remark: it is wasteful to unfold projection functions since
-- kernel projections are folded again in the `foldProjs` preprocessing step.
return !isGrindGadget declName && !env.isProjectionFn declName
else
return false
/--
Unfolds all `reducible` declarations occurring in `e`.
This is meant as a preprocessing step. It does **not** guarantee maximally shared terms
-/
public def unfoldReducible (e : Expr) : MetaM Expr := do
if !( isUnfoldReducibleTarget e) then return e
Meta.transform e (pre := unfoldReducibleStep)
open Grind
/--
Instantiates metavariables, unfold reducible, and applies `shareCommon`.
-/
def preprocessExpr (e : Expr) : SymM Expr := do
shareCommon ( unfoldReducible ( instantiateMVars e))
shareCommon ( instantiateMVars e)
/--
Helper function that removes gaps, instantiate metavariables, and applies `shareCommon`.

View File

@@ -11,7 +11,6 @@ import Lean.Util.ForEachExpr
import Lean.Meta.Tactic.Grind.Util
import Lean.Meta.Match.Basic
import Lean.Meta.Tactic.TryThis
import Lean.Meta.Sym.Util
public section
namespace Lean.Meta.Grind
/-!
@@ -282,7 +281,7 @@ private theorem normConfig_zetaDelta : normConfig.zetaDelta = true := rfl
def preprocessPattern (pat : Expr) (normalizePattern := true) : MetaM Expr := do
let pat instantiateMVars pat
let pat Sym.unfoldReducible pat
let pat unfoldReducible pat
let pat if normalizePattern then normalize pat normConfig else pure pat
let pat detectOffsets pat
let pat foldProjs pat

View File

@@ -8,7 +8,6 @@ prelude
public import Lean.Meta.Tactic.Grind.Types
import Init.Grind.Util
import Lean.Meta.Sym.ExprPtr
import Lean.Meta.Sym.Util
import Lean.Meta.Tactic.Grind.Util
public section
namespace Lean.Meta.Grind
@@ -104,7 +103,7 @@ where
-/
/- We must also apply beta-reduction to improve the effectiveness of the congruence closure procedure. -/
let e Core.betaReduce e
let e Sym.unfoldReducible e
let e unfoldReducible e
/- We must mask proofs occurring in `prop` too. -/
let e visit e
let e eraseIrrelevantMData e

View File

@@ -11,7 +11,6 @@ public import Lean.Meta.Tactic.Grind.Types
import Lean.Meta.Tactic.Grind.Util
import Lean.Meta.Tactic.Grind.MatchDiscrOnly
import Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
import Lean.Meta.Sym.Util
public section
namespace Lean.Meta.Grind
@@ -58,7 +57,7 @@ def preprocessImpl (e : Expr) : GoalM Simp.Result := do
let e' instantiateMVars r.expr
-- Remark: `simpCore` unfolds reducible constants, but it does not consistently visit all possible subterms.
-- So, we must use the following `unfoldReducible` step. It is non-op in most cases
let e' Sym.unfoldReducible e'
let e' unfoldReducible e'
let e' abstractNestedProofs e'
let e' markNestedSubsingletons e'
let e' eraseIrrelevantMData e'
@@ -98,6 +97,6 @@ but ensures assumptions made by `grind` are satisfied.
-/
def preprocessLight (e : Expr) : GoalM Expr := do
let e instantiateMVars e
shareCommon ( canon ( normalizeLevels ( foldProjs ( eraseIrrelevantMData ( markNestedSubsingletons ( Sym.unfoldReducible e))))))
shareCommon ( canon ( normalizeLevels ( foldProjs ( eraseIrrelevantMData ( markNestedSubsingletons ( unfoldReducible e))))))
end Lean.Meta.Grind

View File

@@ -14,7 +14,6 @@ import Lean.Meta.Tactic.Grind.Arith.Simproc
import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
import Lean.Meta.Tactic.Grind.Util
import Lean.Meta.Sym.Util
import Init.Grind.Norm
public section
namespace Lean.Meta.Grind
@@ -137,7 +136,7 @@ builtin_simproc_decl reduceCtorEqCheap (_ = _) := fun e => do
return .done { expr := mkConst ``False, proof? := ( withDefault <| mkEqFalse' ( mkLambdaFVars #[h] ( mkNoConfusion (mkConst ``False) h))) }
builtin_dsimproc_decl unfoldReducibleSimproc (_) := fun e => do
Sym.unfoldReducibleStep e
unfoldReducibleStep e
/-- Returns the array of simprocs used by `grind`. -/
protected def getSimprocs : MetaM (Array Simprocs) := do

View File

@@ -11,7 +11,6 @@ import Lean.ProjFns
import Lean.Meta.WHNF
import Lean.Meta.AbstractNestedProofs
import Lean.Meta.Tactic.Clear
import Lean.Meta.Sym.Util
public section
namespace Lean.Meta.Grind
/--
@@ -56,11 +55,49 @@ def _root_.Lean.MVarId.transformTarget (mvarId : MVarId) (f : Expr → MetaM Exp
mvarId.assign mvarNew
return mvarNew.mvarId!
/--
Returns `true` if `declName` is the name of a grind helper declaration that
should not be unfolded by `unfoldReducible`.
-/
def isGrindGadget (declName : Name) : Bool :=
declName == ``Grind.EqMatch
def isUnfoldReducibleTarget (e : Expr) : CoreM Bool := do
let env getEnv
return Option.isSome <| e.find? fun e => Id.run do
let .const declName _ := e | return false
if getReducibilityStatusCore env declName matches .reducible then
-- Remark: it is wasteful to unfold projection functions since
-- kernel projections are folded again in the `foldProjs` preprocessing step.
return !isGrindGadget declName && !env.isProjectionFn declName
else
return false
/--
Auxiliary function for implementing `unfoldReducible` and `unfoldReducibleSimproc`.
Performs a single step.
-/
def unfoldReducibleStep (e : Expr) : MetaM TransformStep := do
let .const declName _ := e.getAppFn | return .continue
unless ( isReducible declName) do return .continue
if isGrindGadget declName then return .continue
-- See comment at isUnfoldReducibleTarget.
if ( getEnv).isProjectionFn declName then return .continue
let some v unfoldDefinition? e | return .continue
return .visit v
/--
Unfolds all `reducible` declarations occurring in `e`.
-/
def unfoldReducible (e : Expr) : MetaM Expr := do
if !( isUnfoldReducibleTarget e) then return e
Meta.transform e (pre := unfoldReducibleStep)
/--
Unfolds all `reducible` declarations occurring in the goal's target.
-/
def _root_.Lean.MVarId.unfoldReducible (mvarId : MVarId) : MetaM MVarId :=
mvarId.transformTarget Sym.unfoldReducible
mvarId.transformTarget Grind.unfoldReducible
/--
Beta-reduces the goal's target.

View File

@@ -99,8 +99,7 @@ def _root_.Lean.MVarId.getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId
let removeDeps (e : Expr) (candidates : FVarIdHashSet) : MetaM FVarIdHashSet := do
let e instantiateMVars e
let visit : StateRefT FVarIdHashSet MetaM FVarIdHashSet := do
if e.hasFVar then
e.forEachWhere Expr.isFVar fun e => modify fun s => s.erase e.fvarId!
e.forEachWhere Expr.isFVar fun e => modify fun s => s.erase e.fvarId!
get
visit |>.run' candidates
mvarId.withContext do

View File

@@ -786,6 +786,9 @@ def localDeclDependsOnPred [Monad m] [MonadMCtx m] (localDecl : LocalDecl) (pf :
namespace MetavarContext
@[export lean_mk_metavar_ctx]
def mkMetavarContext : Unit MetavarContext := fun _ => {}
/-- Low level API for adding/declaring metavariable declarations.
It is used to implement actions in the monads `MetaM`, `ElabM` and `TacticM`.
It should not be used directly since the argument `(mvarId : MVarId)` is assumed to be "unique". -/

View File

@@ -54,7 +54,7 @@ def externEntry := leading_parser
nonReservedSymbol "extern" >> many (ppSpace >> externEntry)
/--
Declares this tactic to be an alias or alternative form of an existing tactic.
Declare this tactic to be an alias or alternative form of an existing tactic.
This has the following effects:
* The alias relationship is saved
@@ -64,26 +64,13 @@ This has the following effects:
"tactic_alt" >> ppSpace >> ident
/--
Adds one or more tags to a tactic.
Add one or more tags to a tactic.
Tags should be applied to the canonical names for tactics.
-/
@[builtin_attr_parser] def «tactic_tag» := leading_parser
"tactic_tag" >> many1 (ppSpace >> ident)
/--
Sets the tactic's name.
Ordinarily, tactic names are automatically set to the first token in the tactic's parser. If this
process fails, or if the tactic's name should be multiple tokens (e.g. `let rec`), then this
attribute can be used to provide a name.
The tactic's name is used in documentation as well as in completion. Thus, the name should be a
valid prefix of the tactic's syntax.
-/
@[builtin_attr_parser] def «tactic_name» := leading_parser
"tactic_name" >> ppSpace >> (ident <|> strLit)
end Attr
end Lean.Parser

View File

@@ -387,7 +387,7 @@ register_builtin_option internal.parseQuotWithCurrentStage : Bool := {
def evalInsideQuot (declName : Name) : Parser Parser := withFn fun f c s =>
if c.quotDepth > 0 && !c.suppressInsideQuot && internal.parseQuotWithCurrentStage.get c.options && c.env.contains declName then
adaptUncacheableContextFn (fun ctx =>
{ ctx with options := ctx.options.set `interpreter.prefer_native false })
{ ctx with options := ctx.options.setBool `interpreter.prefer_native false })
(evalParserConst declName) c s
else
f c s
@@ -717,7 +717,7 @@ def parserOfStackFn (offset : Nat) : ParserFn := fun ctx s => Id.run do
adaptUncacheableContextFn (fun ctx =>
-- static quotations such as `(e) do not use the interpreter unless the above option is set,
-- so for consistency neither should dynamic quotations using this function
{ ctx with options := ctx.options.set `interpreter.prefer_native (!internal.parseQuotWithCurrentStage.get ctx.options) })
{ ctx with options := ctx.options.setBool `interpreter.prefer_native (!internal.parseQuotWithCurrentStage.get ctx.options) })
(evalParserConst parserName) ctx s
| [.alias alias] =>
match alias with

View File

@@ -52,7 +52,24 @@ example (n : Nat) : n = n := by
optional Term.motive >> sepBy1 Term.matchDiscr ", " >>
" with " >> ppDedent matchAlts
@[builtin_tactic_parser, tactic_alt intro] def introMatch := leading_parser
/--
The tactic
```
intro
| pat1 => tac1
| pat2 => tac2
```
is the same as:
```
intro x
match x with
| pat1 => tac1
| pat2 => tac2
```
That is, `intro` can be followed by match arms and it introduces the values while
doing a pattern match. This is equivalent to `fun` with match arms in term mode.
-/
@[builtin_tactic_parser] def introMatch := leading_parser
nonReservedSymbol "intro" >> matchAlts
builtin_initialize

View File

@@ -191,13 +191,12 @@ builtin_initialize
unless kind == AttributeKind.global do throwAttrMustBeGlobal name kind
let `(«tactic_tag»|tactic_tag $tags*) := stx
| throwError "Invalid `[{name}]` attribute syntax"
if ( getEnv).find? decl |>.isSome then
if !(isTactic ( getEnv) decl) then
throwErrorAt stx "`{.ofConstName decl}` is not a tactic"
throwErrorAt stx "`{decl}` is not a tactic"
if let some tgt' := alternativeOfTactic ( getEnv) decl then
throwErrorAt stx "`{.ofConstName decl}` is an alternative form of `{.ofConstName tgt'}`"
throwErrorAt stx "`{decl}` is an alternative form of `{tgt'}`"
for t in tags do
let tagName := t.getId
@@ -272,81 +271,14 @@ where
| [l] => " * " ++ l ++ "\n\n"
| l::ls => " * " ++ l ++ "\n" ++ String.join (ls.map indentLine) ++ "\n\n"
/--
The mapping between tactics and their custom names.
The first projection in each pair is the tactic name, and the second is the custom name.
-/
builtin_initialize tacticNameExt
: PersistentEnvExtension
(Name × String)
(Name × String)
(NameMap String)
registerPersistentEnvExtension {
mkInitial := pure {},
addImportedFn := fun _ => pure {},
addEntryFn := fun as (src, tgt) => as.insert src tgt,
exportEntriesFn := fun es =>
es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
}
/--
Finds the custom name assigned to `tac`, or returns `none` if there is no such custom name.
-/
def customTacticName [Monad m] [MonadEnv m] (tac : Name) : m (Option String) := do
let env getEnv
match env.getModuleIdxFor? tac with
| some modIdx =>
match (tacticNameExt.getModuleEntries env modIdx).binSearch (tac, default) (Name.quickLt ·.1 ·.1) with
| some (_, val) => return some val
| none => return none
| none => return tacticNameExt.getState env |>.find? tac
builtin_initialize
let name := `tactic_name
registerBuiltinAttribute {
name := name,
ref := by exact decl_name%,
add := fun decl stx kind => do
unless kind == AttributeKind.global do throwAttrMustBeGlobal name kind
let name
match stx with
| `(«tactic_name»|tactic_name $name:str) =>
pure name.getString
| `(«tactic_name»|tactic_name $name:ident) =>
pure (name.getId.toString (escape := false))
| _ => throwError "Invalid `[{name}]` attribute syntax"
if ( getEnv).find? decl |>.isSome then
if !(isTactic ( getEnv) decl) then
throwErrorAt stx m!"`{.ofConstName decl}` is not a tactic"
if let some idx := ( getEnv).getModuleIdxFor? decl then
if let some mod := ( getEnv).allImportedModuleNames[idx]? then
throwErrorAt stx m!"`{.ofConstName decl}` is defined in `{mod}`, but custom names can only be added in the tactic's defining module."
else
throwErrorAt stx m!"`{.ofConstName decl}` is defined in an imported module, but custom names can only be added in the tactic's defining module."
if let some tgt' := alternativeOfTactic ( getEnv) decl then
throwErrorAt stx "`{.ofConstName decl}` is an alternative form of `{.ofConstName tgt'}`"
if let some n customTacticName decl then
throwError m!"The tactic `{.ofConstName decl}` already has the custom name `{n}`"
modifyEnv fun env => tacticNameExt.addEntry env (decl, name)
descr :=
"Registers a custom name for a tactic. This custom name should be a prefix of the " ++
"tactic's syntax, because it is used in completion.",
applicationTime := .beforeElaboration
}
-- Note: this error handler doesn't prevent all cases of non-tactics being added to the data
-- structure. But the module will throw errors during elaboration, and there doesn't seem to be
-- another way to implement this, because the category parser extension attribute runs *after* the
-- attributes specified before a `syntax` command.
/--
Validates that a tactic alternative is actually a tactic, that syntax tagged as tactics are
tactics, and that syntax with tactic names are tactics.
Validates that a tactic alternative is actually a tactic and that syntax tagged as tactics are
tactics.
-/
private def tacticDocsOnTactics : ParserAttributeHook where
postAdd (catName declName : Name) (_builtIn : Bool) := do
@@ -359,8 +291,6 @@ private def tacticDocsOnTactics : ParserAttributeHook where
if let some tags := tacticTagExt.getState ( getEnv) |>.find? declName then
if !tags.isEmpty then
throwError m!"`{.ofConstName declName}` is not a tactic"
if let some n := tacticNameExt.getState ( getEnv) |>.find? declName then
throwError m!"`{MessageData.ofConstName declName}` is not a tactic, but it was assigned a tactic name `{n}`"
builtin_initialize
registerParserAttributeHook tacticDocsOnTactics

View File

@@ -165,7 +165,7 @@ def getOptionsAtCurrPos : DelabM Options := do
let mut opts getOptions
if let some opts' := ctx.optionsPerPos.get? ( getPos) then
for (k, v) in opts' do
opts := opts.set k v
opts := opts.insert k v
return opts
/-- Evaluate option accessor, using subterm-specific options if set. -/
@@ -185,7 +185,7 @@ def withOptionAtCurrPos (k : Name) (v : DataValue) (x : DelabM α) : DelabM α :
let pos getPos
withReader
(fun ctx =>
let opts' := ctx.optionsPerPos.get? pos |>.getD {} |>.set k v
let opts' := ctx.optionsPerPos.get? pos |>.getD {} |>.insert k v
{ ctx with optionsPerPos := ctx.optionsPerPos.insert pos opts' })
x

View File

@@ -142,7 +142,7 @@ def withMDataOptions [Inhabited α] (x : DelabM α) : DelabM α := do
for (k, v) in m do
if (`pp).isPrefixOf k then
let opts := posOpts.get? pos |>.getD {}
posOpts := posOpts.insert pos (opts.set k v)
posOpts := posOpts.insert pos (opts.insert k v)
withReader ({ · with optionsPerPos := posOpts }) $ withMDataExpr x
| _ => x

View File

@@ -22,11 +22,11 @@ abbrev OptionsPerPos := Std.TreeMap SubExpr.Pos Options
def OptionsPerPos.insertAt (optionsPerPos : OptionsPerPos) (pos : SubExpr.Pos) (name : Name) (value : DataValue) : OptionsPerPos :=
let opts := optionsPerPos.get? pos |>.getD {}
optionsPerPos.insert pos <| opts.set name value
optionsPerPos.insert pos <| opts.insert name value
/-- Merges two collections of options, where the second overrides the first. -/
def OptionsPerPos.merge : OptionsPerPos OptionsPerPos OptionsPerPos :=
Std.TreeMap.mergeWith (fun _ => Options.mergeBy (fun _ _ dv => dv))
Std.TreeMap.mergeWith (fun _ => KVMap.mergeBy (fun _ _ dv => dv))
namespace SubExpr

View File

@@ -317,7 +317,7 @@ def checkKnowsType : AnalyzeM Unit := do
throw $ Exception.internal analyzeFailureId
def annotateBoolAt (n : Name) (pos : Pos) : AnalyzeM Unit := do
let opts := ( get).annotations.getD pos {} |>.set n true
let opts := ( get).annotations.getD pos {} |>.setBool n true
trace[pp.analyze.annotate] "{pos} {n}"
modify fun s => { s with annotations := s.annotations.insert pos opts }

View File

@@ -107,9 +107,6 @@ register_builtin_option allowUnsafeReducibility : Bool := {
private def validate (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) : CoreM Unit := do
let suffix := .note "Use `set_option allowUnsafeReducibility true` to override reducibility status validation"
-- Allow global visibility attributes even on non-exported definitions - they may be relevant for
-- downstream non-`module`s.
withoutExporting do
unless allowUnsafeReducibility.get ( getOptions) do
match ( getConstInfo declName) with
| .defnInfo _ =>

View File

@@ -224,22 +224,17 @@ def computeQueries
break
return queries
def importAllUnknownIdentifiersProvider : Name := `allUnknownIdentifiers
def importUnknownIdentifiersProvider : Name := `unknownIdentifiers
def mkUnknownIdentifierCodeActionData (params : CodeActionParams)
(name := importUnknownIdentifiersProvider) : CodeActionResolveData := {
params,
providerName := name
providerResultIndex := 0
: CodeActionResolveData
}
def importAllUnknownIdentifiersProvider : Name := `unknownIdentifiers
def importAllUnknownIdentifiersCodeAction (params : CodeActionParams) (kind : String) : CodeAction := {
title := "Import all unambiguous unknown identifiers"
kind? := kind
data? := some <| toJson <|
mkUnknownIdentifierCodeActionData params importAllUnknownIdentifiersProvider
data? := some <| toJson {
params,
providerName := importAllUnknownIdentifiersProvider
providerResultIndex := 0
: CodeActionResolveData
}
}
private def mkImportText (ctx : Elab.ContextInfo) (mod : Name) :
@@ -316,7 +311,6 @@ def handleUnknownIdentifierCodeAction
insertion.edit
]
}
data? := some <| toJson <| mkUnknownIdentifierCodeActionData params
}
if isExactMatch then
hasUnambiguousImportCodeAction := true
@@ -328,7 +322,6 @@ def handleUnknownIdentifierCodeAction
textDocument := doc.versionedIdentifier
edits := #[insertion.edit]
}
data? := some <| toJson <| mkUnknownIdentifierCodeActionData params
}
if hasUnambiguousImportCodeAction then
unknownIdentifierCodeActions := unknownIdentifierCodeActions.push <|

View File

@@ -597,8 +597,7 @@ def tacticCompletion
(completionInfoPos : Nat)
(ctx : ContextInfo)
: IO (Array ResolvableCompletionItem) := ctx.runMetaM .empty do
-- Don't include tactics that are identified only by their internal parser name
let allTacticDocs Tactic.Doc.allTacticDocs (includeUnnamed := false)
let allTacticDocs Tactic.Doc.allTacticDocs
let items : Array ResolvableCompletionItem := allTacticDocs.map fun tacticDoc => {
label := tacticDoc.userName
detail? := none

View File

@@ -793,24 +793,21 @@ section MessageHandling
rpcEncode resp st.objects |>.map (·) ({st with objects := ·})
return some <| .pure { response? := resp, serialized := resp.compress, isComplete := true }
| "codeAction/resolve" =>
let jsonParams := params
let params RequestM.parseRequestParams CodeAction params
let some data := params.data?
| throw (RequestError.invalidParams "Expected a data field on CodeAction.")
let data RequestM.parseRequestParams CodeActionResolveData data
if data.providerName == importUnknownIdentifiersProvider then
return some <| RequestTask.pure { response? := jsonParams, serialized := jsonParams.compress, isComplete := true }
if data.providerName == importAllUnknownIdentifiersProvider then
return some <| RequestM.asTask do
let unknownIdentifierRanges waitAllUnknownIdentifierMessageRanges st.doc
if unknownIdentifierRanges.isEmpty then
let p := toJson params
return { response? := p, serialized := p.compress, isComplete := true }
let action? handleResolveImportAllUnknownIdentifiersCodeAction? id params unknownIdentifierRanges
let action := action?.getD params
let action := toJson action
return { response? := action, serialized := action.compress, isComplete := true }
return none
if data.providerName != importAllUnknownIdentifiersProvider then
return none
return some <| RequestM.asTask do
let unknownIdentifierRanges waitAllUnknownIdentifierMessageRanges st.doc
if unknownIdentifierRanges.isEmpty then
let p := toJson params
return { response? := p, serialized := p.compress, isComplete := true }
let action? handleResolveImportAllUnknownIdentifiersCodeAction? id params unknownIdentifierRanges
let action := action?.getD params
let action := toJson action
return { response? := action, serialized := action.compress, isComplete := true }
| _ =>
return none

View File

@@ -39,24 +39,15 @@ def GoToKind.determineTargetExprs (kind : GoToKind) (ti : TermInfo) : MetaM (Arr
| _ =>
return #[ instantiateMVars ti.expr]
partial def getInstanceProjectionArg? (e : Expr) : MetaM (Option Expr) := do
let some (e, projInfo) Meta.withReducible <| reduceToProjection? e
def getInstanceProjectionArg? (e : Expr) : MetaM (Option Expr) := do
let env getEnv
let .const n _ := e.getAppFn'
| return none
let some projInfo := env.getProjectionFnInfo? n
| return none
let instIdx := projInfo.numParams
let appArgs := e.getAppArgs
return appArgs[instIdx]?
where
reduceToProjection? (e : Expr) : MetaM (Option (Expr × ProjectionFunctionInfo)) := do
let env getEnv
let .const n _ := e.getAppFn'
| return none
if let some projInfo := env.getProjectionFnInfo? n then
return some (e, projInfo)
-- Unfold reducible definitions when looking for a projection.
-- For example, this ensures that we get `LT.lt` instance projection entries on `GT.gt`.
let some e Meta.unfoldDefinition? e
| return none
reduceToProjection? e
def isInstanceProjection (e : Expr) : MetaM Bool := do
return ( getInstanceProjectionArg? e).isSome

View File

@@ -117,9 +117,8 @@ namespace ModuleRefs
/-- Adds `ref` to the `RefInfo` corresponding to `ref.ident` in `self`. See `RefInfo.addRef`. -/
def addRef (self : ModuleRefs) (ref : Reference) : ModuleRefs :=
self.alter ref.ident fun
| some refInfo => some <| refInfo.addRef ref
| none => some <| RefInfo.empty.addRef ref
let refInfo := self.getD ref.ident RefInfo.empty
self.insert ref.ident (refInfo.addRef ref)
/-- Converts `refs` to a JSON-serializable `Lsp.ModuleRefs` and collects all decls. -/
def toLspModuleRefs (refs : ModuleRefs) : BaseIO (Lsp.ModuleRefs × Decls) := StateT.run (s := ) do
@@ -375,9 +374,9 @@ def dedupReferences (refs : Array Reference) (allowSimultaneousBinderUse := fals
for ref in refs do
let isBinder := if allowSimultaneousBinderUse then some ref.isBinder else none
let key := (ref.ident, isBinder, ref.range)
refsByIdAndRange := refsByIdAndRange.alter key fun
| some ref' => some { ref' with aliases := ref'.aliases ++ ref.aliases }
| none => some ref
refsByIdAndRange := match refsByIdAndRange[key]? with
| some ref' => refsByIdAndRange.insert key { ref' with aliases := ref'.aliases ++ ref.aliases }
| none => refsByIdAndRange.insert key ref
let dedupedRefs := refsByIdAndRange.fold (init := #[]) fun refs _ ref => refs.push ref
return dedupedRefs.qsort (·.range < ·.range)

View File

@@ -284,7 +284,7 @@ def setConfigOption (opts : Options) (arg : String) : IO Options := do
else
-- More options may be registered by imports, so we leave validating them to the elaborator.
-- This (minor) duplication may be resolved later.
return opts.set name val
return opts.insert name val
/--
Process a command-line option parsed by the C++ shell.

View File

@@ -43,9 +43,6 @@ instance : Coe Bool LeanOptionValue where
instance : Coe Nat LeanOptionValue where
coe := LeanOptionValue.ofNat
instance {n : Nat} : OfNat LeanOptionValue n where
ofNat := .ofNat n
instance : FromJson LeanOptionValue where
fromJson?
| (s : String) => Except.ok s
@@ -100,9 +97,9 @@ def LeanOptions.appendArray (self : LeanOptions) (new : Array LeanOption) : Lean
instance : HAppend LeanOptions (Array LeanOption) LeanOptions := LeanOptions.appendArray
def LeanOptions.toOptions (leanOptions : LeanOptions) : Options := Id.run do
let mut options := Options.empty
let mut options := KVMap.empty
for name, optionValue in leanOptions.values do
options := options.set name optionValue.toDataValue
options := options.insert name optionValue.toDataValue
return options
def LeanOptions.fromOptions? (options : Options) : Option LeanOptions := do

Some files were not shown because too many files have changed in this diff Show More