Zulip Chat Archive
Stream: mathlib4
Topic: simp timeing out
Scott Morrison (Nov 14 2022 at 05:07):
@Yakov Pechersky, I think your latest commit to mathlib4#550 is window dressing, and probably should be reverted. The problem here is that a perfectly easy simp is timing out. We don't want to replace it with a rw, but find out what is going on.
Yakov Pechersky (Nov 14 2022 at 05:08):
Agreed.
Scott Morrison (Nov 14 2022 at 05:08):
I think we must have a bunch of bad simp lemmas that are causing simp to spiral out of control, and that we need a new linter to catch.
Scott Morrison (Nov 14 2022 at 05:08):
But I don't know what's going wrong yet.
Yakov Pechersky (Nov 14 2022 at 05:08):
I'm seeing some weirdness in here too:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/logic.2Eequiv.2Edefs.20causing.20elaboration.20issues.20in.20Simps.20tests/near/309528121.2E01
Scott Morrison (Nov 14 2022 at 05:09):
When I add set_option trace.Meta.Tactic.simp.rewrite true in Logic.Equiv.Function at commit https://github.com/leanprover-community/mathlib4/pull/550/commits/d6d3b834517bb0ba128a1d4cefec4f86f94a6e2f, I get:
Scott Morrison (Nov 14 2022 at 05:10):
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (Equiv.symm a₁✝ = a₁) = (Equiv.symm a₁✝ = a₂) ==> Equiv.symm a₁✝ = a₁ ↔ Equiv.symm a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (Equiv.symm a₁✝ = a₁) = (Equiv.symm a₁✝ = a₂) ==> Equiv.symm a₁✝ = a₁ ↔ Equiv.symm a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (Equiv.symm a₁✝ = a₁) = (Equiv.symm a₁✝ = a₂) ==> Equiv.symm a₁✝ = a₁ ↔ Equiv.symm a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (Equiv.symm a₁✝ = a₁) = (Equiv.symm a₁✝ = a₂) ==> Equiv.symm a₁✝ = a₁ ↔ Equiv.symm a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (Equiv.symm a₁✝ = a₁) = (Equiv.symm a₁✝ = a₂) ==> Equiv.symm a₁✝ = a₁ ↔ Equiv.symm a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (h.toFun <$> a₁✝ = a₁) = (h.toFun <$> a₁✝ = a₂) ==> h.toFun <$> a₁✝ = a₁ ↔ h.toFun <$> a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (h.toFun <$> a₁✝ = a₁) = (h.toFun <$> a₁✝ = a₂) ==> h.toFun <$> a₁✝ = a₁ ↔ h.toFun <$> a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (h.toFun <$> a₁✝ = a₁) = (h.toFun <$> a₁✝ = a₂) ==> h.toFun <$> a₁✝ = a₁ ↔ h.toFun <$> a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (h.toFun <$> a₁✝ = a₁) = (h.toFun <$> a₁✝ = a₂) ==> h.toFun <$> a₁✝ = a₁ ↔ h.toFun <$> a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (h.toFun <$> a₁✝ = a₁) = (h.toFun <$> a₁✝ = a₂) ==> h.toFun <$> a₁✝ = a₁ ↔ h.toFun <$> a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (Functor.map a₁✝ = a₁) = (Functor.map a₁✝ = a₂) ==> Functor.map a₁✝ = a₁ ↔ Functor.map a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (Functor.map a₁✝ = a₁) = (Functor.map a₁✝ = a₂) ==> Functor.map a₁✝ = a₁ ↔ Functor.map a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (Functor.map a₁✝ = a₁) = (Functor.map a₁✝ = a₂) ==> Functor.map a₁✝ = a₁ ↔ Functor.map a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (Functor.map a₁✝ = a₁) = (Functor.map a₁✝ = a₂) ==> Functor.map a₁✝ = a₁ ↔ Functor.map a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (Functor.map a₁✝ = a₁) = (Functor.map a₁✝ = a₂) ==> Functor.map a₁✝ = a₁ ↔ Functor.map a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (@Functor.map f a₁✝ = a₁) =
(@Functor.map f a₁✝ = a₂) ==> @Functor.map f a₁✝ = a₁ ↔ @Functor.map f a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (@Functor.map f a₁✝ = a₁) =
(@Functor.map f a₁✝ = a₂) ==> @Functor.map f a₁✝ = a₁ ↔ @Functor.map f a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (@Functor.map f a₁✝ = a₁) =
(@Functor.map f a₁✝ = a₂) ==> @Functor.map f a₁✝ = a₁ ↔ @Functor.map f a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (@Functor.map f a₁✝ = a₁) =
(@Functor.map f a₁✝ = a₂) ==> @Functor.map f a₁✝ = a₁ ↔ @Functor.map f a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (@Functor.map f a₁✝ = a₁) =
(@Functor.map f a₁✝ = a₂) ==> @Functor.map f a₁✝ = a₁ ↔ @Functor.map f a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, ((Equiv.symm h).toFun <$> a₁✝ = a₁) =
((Equiv.symm h).toFun <$> a₁✝ = a₂) ==> (Equiv.symm h).toFun <$> a₁✝ = a₁ ↔ (Equiv.symm h).toFun <$> a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, ((Equiv.symm h).toFun <$> a₁✝ = a₁) =
((Equiv.symm h).toFun <$> a₁✝ = a₂) ==> (Equiv.symm h).toFun <$> a₁✝ = a₁ ↔ (Equiv.symm h).toFun <$> a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, ((Equiv.symm h).toFun <$> a₁✝ = a₁) =
((Equiv.symm h).toFun <$> a₁✝ = a₂) ==> (Equiv.symm h).toFun <$> a₁✝ = a₁ ↔ (Equiv.symm h).toFun <$> a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, ((Equiv.symm h).toFun <$> a₁✝ = a₁) =
((Equiv.symm h).toFun <$> a₁✝ = a₂) ==> (Equiv.symm h).toFun <$> a₁✝ = a₁ ↔ (Equiv.symm h).toFun <$> a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, ((Equiv.symm h).toFun <$> a₁✝ = a₁) =
((Equiv.symm h).toFun <$> a₁✝ = a₂) ==> (Equiv.symm h).toFun <$> a₁✝ = a₁ ↔ (Equiv.symm h).toFun <$> a₁✝ = a₂
[Meta.Tactic.simp.rewrite] Functor.map_map:1000, (Equiv.symm h).toFun <$> h.toFun <$> x ==> ((Equiv.symm h).toFun ∘ h.toFun) <$> x
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, ((Equiv.symm h).toFun ∘ a₁✝ = a₁) =
((Equiv.symm h).toFun ∘ a₁✝ = a₂) ==> (Equiv.symm h).toFun ∘ a₁✝ = a₁ ↔ (Equiv.symm h).toFun ∘ a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, ((Equiv.symm h).toFun ∘ a₁✝ = a₁) =
((Equiv.symm h).toFun ∘ a₁✝ = a₂) ==> (Equiv.symm h).toFun ∘ a₁✝ = a₁ ↔ (Equiv.symm h).toFun ∘ a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, ((Equiv.symm h).toFun ∘ a₁✝ = a₁) =
((Equiv.symm h).toFun ∘ a₁✝ = a₂) ==> (Equiv.symm h).toFun ∘ a₁✝ = a₁ ↔ (Equiv.symm h).toFun ∘ a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, ((Equiv.symm h).toFun ∘ a₁✝ = a₁) =
((Equiv.symm h).toFun ∘ a₁✝ = a₂) ==> (Equiv.symm h).toFun ∘ a₁✝ = a₁ ↔ (Equiv.symm h).toFun ∘ a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, ((Equiv.symm h).toFun ∘ a₁✝ = a₁) =
((Equiv.symm h).toFun ∘ a₁✝ = a₂) ==> (Equiv.symm h).toFun ∘ a₁✝ = a₁ ↔ (Equiv.symm h).toFun ∘ a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @Equiv.symm_comp_self:1000, (Equiv.symm h).toFun ∘ h.toFun ==> id
[Meta.Tactic.simp.rewrite] @id_map:1000, id <$> a₁ ==> a₁
[Meta.Tactic.simp.rewrite] @id_map:1000, id <$> a₂ ==> a₂
[Meta.Tactic.simp.rewrite] @id_map:1000, id <$> a₁ ==> a₁
[Meta.Tactic.simp.rewrite] @id_map:1000, id <$> a₁ ==> a₁
[Meta.Tactic.simp.rewrite] @id_map:1000, id <$> a₂ ==> a₂
[Meta.Tactic.simp.rewrite] @id_map:1000, id <$> a₂ ==> a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝ = a₁) = (a₁✝ = a₂) ==> a₁✝ = a₁ ↔ a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝ = a₁) = (a₁✝ = a₂) ==> a₁✝ = a₁ ↔ a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝ = a₁) = (a₁✝ = a₂) ==> a₁✝ = a₁ ↔ a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝ = a₁) = (a₁✝ = a₂) ==> a₁✝ = a₁ ↔ a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝ = a₁) = (a₁✝ = a₂) ==> a₁✝ = a₁ ↔ a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @id_map:1000, id <$> x ==> x
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁) = (x = a₂) ==> x = a₁ ↔ x = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁) = (x = a₂) ==> x = a₁ ↔ x = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁) = (x = a₂) ==> x = a₁ ↔ x = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁) = (x = a₂) ==> x = a₁ ↔ x = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁✝) = a₁ ==> x = a₁✝ ↔ a₁
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁✝) = a₂ ==> x = a₁✝ ↔ a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁✝ ↔ a₁) = (x = a₁✝ ↔ a₂) ==> (x = a₁✝ ↔ a₁) ↔ (x = a₁✝ ↔ a₂)
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁) = (x = a₂) ==> x = a₁ ↔ x = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁) = (x = a₂) ==> x = a₁ ↔ x = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁) = (x = a₂) ==> x = a₁ ↔ x = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁✝ ↔ a₁) = (x = a₁✝ ↔ a₂) ==> (x = a₁✝ ↔ a₁) ↔ (x = a₁✝ ↔ a₂)
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁✝ ↔ a₁) = (x = a₁✝ ↔ a₂) ==> (x = a₁✝ ↔ a₁) ↔ (x = a₁✝ ↔ a₂)
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁) = (x = a₂) ==> x = a₁ ↔ x = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁✝ ↔ a₁) = (x = a₁✝ ↔ a₂) ==> (x = a₁✝ ↔ a₁) ↔ (x = a₁✝ ↔ a₂)
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁) = (x = a₂) ==> x = a₁ ↔ x = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁) = (x = a₂) ==> x = a₁ ↔ x = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (x = a₁✝ ↔ a₁) = (x = a₁✝ ↔ a₂) ==> (x = a₁✝ ↔ a₁) ↔ (x = a₁✝ ↔ a₂)
[Meta.Tactic.simp.rewrite] @eq_self:1000, x = x ==> True
on the left_inv line, and then
Scott Morrison (Nov 14 2022 at 05:10):
tactic 'simp' failed, nested error:
(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (Equiv.symm a₁✝ = a₁) = (Equiv.symm a₁✝ = a₂) ==> Equiv.symm a₁✝ = a₁ ↔ Equiv.symm a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (Equiv.symm a₁✝ = a₁) = (Equiv.symm a₁✝ = a₂) ==> Equiv.symm a₁✝ = a₁ ↔ Equiv.symm a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (Equiv.symm a₁✝ = a₁) = (Equiv.symm a₁✝ = a₂) ==> Equiv.symm a₁✝ = a₁ ↔ Equiv.symm a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (Equiv.symm a₁✝ = a₁) = (Equiv.symm a₁✝ = a₂) ==> Equiv.symm a₁✝ = a₁ ↔ Equiv.symm a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (Equiv.symm a₁✝ = a₁) = (Equiv.symm a₁✝ = a₂) ==> Equiv.symm a₁✝ = a₁ ↔ Equiv.symm a₁✝ = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
[Meta.Tactic.simp.rewrite] @eq_iff_iff:1000, (a₁✝.toFun = a₁) = (a₁✝.toFun = a₂) ==> a₁✝.toFun = a₁ ↔ a₁✝.toFun = a₂
on the right_inv line.
Scott Morrison (Nov 14 2022 at 05:10):
I have to run now...
Yakov Pechersky (Nov 14 2022 at 05:35):
It slows down even in the Logic.Equiv.Defs file itself. I've removed all the simp tags, yet
theorem cast_eq_iff_heq {α β} (h : α = β) {a : α} {b : β} : Equiv.cast h a = b ↔ HEq a b :=
by subst h
simp [coe_refl]
is still slow.
Scott Morrison (Nov 14 2022 at 07:17):
Still away from the computer, but I suspect it is Data.Quot. We should turn off all the lift...mk type simp lemmas, which are probably all bad for Lean 4.
Scott Morrison (Nov 14 2022 at 09:59):
I've turned off all the lift.*mk.* lemmas, and now simp is fast again. We really need a linter to catch simp lemmas where, after unfolding reducible definitions, the head of the LHS is variable.
Scott Morrison (Nov 14 2022 at 09:59):
For this PR, I think we can just proceed with these simp lemmas in Data.Quot turned off.
Scott Morrison (Nov 14 2022 at 10:00):
(Probably I turned off more simp lemmas than is really necessary?)
Gabriel Ebner (Nov 15 2022 at 05:56):
https://github.com/leanprover/std4/pull/26
Last updated: Dec 20 2023 at 11:08 UTC