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.
120 lines
2.4 KiB
Lean4
120 lines
2.4 KiB
Lean4
/-!
|
||
# Improve zeta-delta tracking for `simp?`
|
||
|
||
https://github.com/leanprover/lean4/issues/6655 reports issues with `simp?` where
|
||
it would over-report local variables. This comes down to two kinds of issues:
|
||
- zeta-delta tracking wasn't being reset, so previous `simp?`s would contribute variables
|
||
- `simp?` would report variables that weren't explicitly mentioned,
|
||
because `whnf` would be run with different configurations during the tracking.
|
||
(e.g. `withInferTypeConfig` enables `zetaDelta`.)
|
||
|
||
This file tests that it resets the tracking and filters the list.
|
||
-/
|
||
|
||
set_option linter.unusedSimpArgs false
|
||
|
||
/-!
|
||
Example from #6655. This used to suggest `simp only [e, d]`.
|
||
-/
|
||
/--
|
||
info: Try this:
|
||
[apply] simp only [e]
|
||
---
|
||
trace: α : Type
|
||
c : α → α
|
||
x : α
|
||
d : α → α := c
|
||
e : α → α := d
|
||
⊢ d x = x
|
||
---
|
||
warning: declaration uses `sorry`
|
||
-/
|
||
#guard_msgs in
|
||
example {α : Type} (c : α → α) (x : α) : c x = x := by
|
||
let d := c
|
||
let e := d
|
||
change e x = x
|
||
simp? [e]
|
||
trace_state
|
||
sorry
|
||
|
||
/-!
|
||
Example from #6655. This used to suggest `simp only [d]`.
|
||
-/
|
||
/--
|
||
info: Try this:
|
||
[apply] simp only
|
||
---
|
||
warning: declaration uses `sorry`
|
||
-/
|
||
#guard_msgs in
|
||
example {α : Type} (c : α → α) (x : α) : c x = x := by
|
||
let d := c
|
||
change d x = x
|
||
simp [d]
|
||
have : x = x := by
|
||
simp?
|
||
sorry
|
||
|
||
/-!
|
||
Example from comments of #6655. This used to suggest `simp only [Int.add_sub_cancel, p]`.
|
||
(N.B. the goal at that point does not have `p` in it!)
|
||
-/
|
||
/--
|
||
info: Try this:
|
||
[apply] simp only [Int.add_sub_cancel]
|
||
-/
|
||
#guard_msgs in
|
||
example (a b : Int) : a + b - b = a := by
|
||
let p := 1
|
||
have h : p = 1 := by
|
||
simp only [p]
|
||
simp?
|
||
|
||
/-!
|
||
Example from https://github.com/leanprover/lean4/pull/7539 by JovanGerb.
|
||
This used to suggest `simp only [a, b] ` and `simp only [a, b]`
|
||
-/
|
||
/--
|
||
info: Try this:
|
||
[apply] simp only [a]
|
||
---
|
||
info: Try this:
|
||
[apply] simp only
|
||
-/
|
||
#guard_msgs in
|
||
example : True := by
|
||
let a := 1
|
||
let b := 2
|
||
have : b = 2 := by simp [a,b]
|
||
have : a = 1 := by simp? [a]
|
||
have : 1 = 1 := by simp?
|
||
trivial
|
||
|
||
/-!
|
||
Test that there is still a deficiency. This should say `simp only [e]`.
|
||
-/
|
||
/--
|
||
info: Try this:
|
||
[apply] simp only [e, c]
|
||
---
|
||
trace: α : Type
|
||
b : α → α
|
||
x : α
|
||
c : α → α := b
|
||
d : α → α := c
|
||
e : α → α := d
|
||
⊢ d x = x
|
||
---
|
||
warning: declaration uses `sorry`
|
||
-/
|
||
#guard_msgs in
|
||
example {α : Type} (b : α → α) (x : α) : b x = x := by
|
||
let c := b
|
||
let d := c
|
||
let e := d
|
||
change e x = x
|
||
simp? [e, c]
|
||
trace_state
|
||
sorry
|