mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
47 lines
1.8 KiB
Lean4
47 lines
1.8 KiB
Lean4
/-!
|
||
# Ensure that `rw ... at h` does not create unknown free variables (issue #2711)
|
||
|
||
## Context
|
||
|
||
`rw ... at h` elaborates its rules with postponed metavariables, which, prior to this test, were
|
||
synthesized after the bulk of the tactic has taken place by `Term.withSynthesize`. Specifically,
|
||
these mvars were synthesized after `replaceLocalDecl` has executed.
|
||
|
||
`replaceLocalDecl` needs to be sure it's not inserting the new, rewritten hypothesis before any
|
||
fvars which the type of that hypothesis now depends on. For example, if the type of `h` got
|
||
rewritten to `f i` where `i` was a local declaration occurring after `h`, `replaceLocalDecl` should
|
||
insert the rewritten `h` after `i`.
|
||
|
||
To ensure this, it traverses the type looking for fvars to find the latest-occurring one. However,
|
||
the pending mvars it might encounter in the type have not even been assigned yet, and so
|
||
`replaceLocalDecl` will not find any fvars when it traverses over them. `Term.withSynthesize` might
|
||
nevertheless assign these mvars to later-occurring fvars afterwards. As such, the type of the
|
||
rewritten hypothesis might become ill-formed at the place `replaceLocalDecl` inserts it once the
|
||
pending mvars are assigned, as it might now include unknown `FVarId`s (the `FVarId`s following the
|
||
insertion spot will have been changed by the insertion).
|
||
|
||
This test reflects the choice to synthesize the pending mvars before `replaceLocalDecl` is
|
||
executed, thus avoiding this issue.
|
||
-/
|
||
|
||
class Bar (α) where a : α
|
||
|
||
def f {α} [Bar α] (a : α) := a
|
||
|
||
def w (_ : α) : Prop := True
|
||
|
||
theorem foo {a : α} [Bar α] : w a = w (f a) := rfl
|
||
|
||
set_option pp.explicit true in
|
||
example : True := by
|
||
have h : w 5 := trivial
|
||
let inst : Bar Nat := ⟨0⟩
|
||
rw [foo] at h
|
||
-- Previous goal state:
|
||
/-
|
||
h✝ : @w Nat 5
|
||
h : @w Nat (@f Nat _uniq.158 5)
|
||
inst : Bar Nat := @Bar.mk Nat 0
|
||
⊢ True
|
||
-/
|