b99356ebcf
This PR globally enables `warning.simp.varHead` (added in #13325) and silences the warning in `Lake.Util.Family.Mathlib` adaptations were already merged as part of adaptations for #13325. This is a separate PR from #13325 due to warning appearing when re-bootstrapping, so we needed `stage0` update before enabling this option.
98 lines
3.5 KiB
Text
98 lines
3.5 KiB
Text
section
|
|
theorem broken1 (x : Nat) : x = x + 0 := by simp
|
|
|
|
/--
|
|
warning: Left-hand side of simp theorem has a variable as head symbol. This means the theorem will be tried on every simp step, which can be expensive. This may be acceptable for `local` or `scoped` simp lemmas.
|
|
Use `set_option warning.simp.varHead false` to disable this warning.
|
|
-/
|
|
#guard_msgs in
|
|
attribute [local simp] broken1
|
|
end
|
|
|
|
section
|
|
theorem broken2 (x : Nat) : x + 0 = x := by simp
|
|
|
|
-- Works in the usual direction
|
|
attribute [local simp] broken2
|
|
|
|
-- Breaks in the other direction
|
|
/--
|
|
warning: Left-hand side of simp theorem has a variable as head symbol. This means the theorem will be tried on every simp step, which can be expensive. This may be acceptable for `local` or `scoped` simp lemmas.
|
|
Use `set_option warning.simp.varHead false` to disable this warning.
|
|
-/
|
|
#guard_msgs in
|
|
attribute [local simp ←] broken2
|
|
end
|
|
|
|
theorem broken3 (x : Nat → Nat) : x 0 = x 0 + 0 := by simp
|
|
|
|
/--
|
|
warning: Left-hand side of simp theorem has a variable as head symbol. This means the theorem will be tried on every simp step, which can be expensive. This may be acceptable for `local` or `scoped` simp lemmas.
|
|
Use `set_option warning.simp.varHead false` to disable this warning.
|
|
-/
|
|
#guard_msgs in
|
|
attribute [simp] broken3
|
|
|
|
theorem broken4 (x : Nat → Nat) : x 0 + 0 = x 0 := by rfl
|
|
|
|
/--
|
|
warning: Left-hand side of simp theorem has a variable as head symbol. This means the theorem will be tried on every simp step, which can be expensive. This may be acceptable for `local` or `scoped` simp lemmas.
|
|
Use `set_option warning.simp.varHead false` to disable this warning.
|
|
-/
|
|
#guard_msgs in
|
|
attribute [simp ←] broken4
|
|
|
|
section
|
|
/--
|
|
warning: Left-hand side of simp theorem has a variable as head symbol. This means the theorem will be tried on every simp step, which can be expensive. This may be acceptable for `local` or `scoped` simp lemmas.
|
|
Use `set_option warning.simp.varHead false` to disable this warning.
|
|
-/
|
|
#guard_msgs in
|
|
@[local simp] theorem broken5 (x : Prop) : x ↔ x ∧ True := by simp
|
|
end
|
|
|
|
theorem broken6 (x : Prop → Prop) : x False ∧ True ↔ x False := by simp
|
|
|
|
/--
|
|
warning: Left-hand side of simp theorem has a variable as head symbol. This means the theorem will be tried on every simp step, which can be expensive. This may be acceptable for `local` or `scoped` simp lemmas.
|
|
Use `set_option warning.simp.varHead false` to disable this warning.
|
|
-/
|
|
#guard_msgs in
|
|
attribute [simp ←] broken6
|
|
|
|
-- Abbrev as head symbol should not trigger the warning (mathlib false positive regression test)
|
|
structure Foo where
|
|
val : Nat
|
|
|
|
abbrev Foo.get (f : Foo) : Nat := f.val
|
|
|
|
theorem Foo.get_mk (n : Nat) : (Foo.mk n).get = n := rfl
|
|
|
|
#guard_msgs in
|
|
attribute [simp] Foo.get_mk
|
|
|
|
-- `.other` head key: lambda as LHS head
|
|
theorem broken8 : (fun x : Nat => x + 0) = (fun x => x) := by ext; omega
|
|
|
|
/--
|
|
warning: Left-hand side of simp theorem is headed by a `.other` key in the discrimination tree (e.g. because it is a lambda expression). This theorem will be tried against all expressions that also have a `.other` key as head, which can cause slowdowns. This may be acceptable for `local` or `scoped` simp lemmas.
|
|
Use `set_option warning.simp.otherHead false` to disable this warning.
|
|
-/
|
|
#guard_msgs in
|
|
attribute [simp] broken8
|
|
|
|
-- Option to disable the `.other` head warning
|
|
section
|
|
#guard_msgs in
|
|
set_option warning.simp.otherHead false in
|
|
attribute [local simp] broken8
|
|
end
|
|
|
|
-- Option to disable the warning
|
|
section
|
|
theorem broken7 (x : Nat) : x = x + 0 := by omega
|
|
|
|
#guard_msgs in
|
|
set_option warning.simp.varHead false in
|
|
attribute [local simp] broken7
|
|
end
|