kernel slow to accept refl proof

Stream: general

[Kevin Buzzard]

Yael isolated a nice simple version of a phenomenon I've seen a couple of times now, where tactic mode is quick to accept a theorem as true, but the kernel then spends a long time convincing itself. This is some kind of "heavy refl" I think but of a very specific nature. Consider the following code:

import group_theory.free_abelian_group

example (α : Type) [monoid α] (x : free_abelian_group α) :
  x * 0 = 0 :=
begin
  refl -- works super-quickly
end

example (α : Type) [monoid α] (x y : free_abelian_group α) :
  x * y * 0 = x * (y * 0) :=
begin
  refl, -- works instantly
  sorry, -- tactic failed, there are no goals to be solved
end

It seems that in this set-up, x * 0 is defeq to 0 and the first example compiles with no problem. The second example, which of course should also be refl, also seems to compile without problem, you get the goals accomplished message, and an error on the sorry complaining that there are no goals left. Commenting out the sorry though makes the proof compilation time shoot up to about 5 seconds on my relatively new laptop, and although I only have a poor understanding of what's going on what I think is happening is that tactic mode accepted the refl fine but the kernel seems to be having second thoughts about it for quite some time.

Switching on the profiler doesn't seem to help at all; it just reports everything as happening quickly, it's perhaps not profiling that last step where the kernel has to check it believes the proof term which has been constructed. I've seen situations like this before but this is by far the simplest one. Is it worth trying to demathlibify this or are examples which use only core Lean already known?

Note that

example (α : Type) [monoid α] (x y : free_abelian_group α) :
  x * y * 0 = x * (y * 0) :=
begin
  simp,
end

works fine and is also very quick. Is there more than one kind of "heavy refl"? The kind which takes a long time to work in tactic mode, and then a different kind like this one which is quick in tactic mode but then takes a long time in the kernel? Or are they all like this? Sorry if I'm talking nonsense about kernels, I don't really understand how all this works really.

[Kevin Buzzard]

import group_theory.free_abelian_group

example (α : Type) [monoid α] (x y : free_abelian_group α) :
  x * (y * 0) = 0 :=
begin
  refl, -- quick
end

example (α : Type) [monoid α] (x y : free_abelian_group α) :
  (x * y) * 0 = 0 :=
begin
  refl, -- quick
end

example (α : Type) [monoid α] (x y : free_abelian_group α) :
  (x * y) * 0 = x * (y * 0) :=
begin
  refl, -- very slow (but quick if you add `sorry` after)
end

[Kevin Buzzard]

This is different to the non-transitivity of rfl at the end of section 3.7 of the reference manual; there the refl just fails quickly, and adding a sorry afterwards doesn't change anything.

[Kevin Buzzard]

Completely coincidentally Bhavik just showed me another very short example of apparently a totally different nature:

import analysis.special_functions.pow

lemma timeout : (0 : ℝ) < 128 ^ (500 : ℝ) :=
begin
  norm_num1,
  sorry, -- no goals to be solved
end

[Bhavik Mehta]

It gets even shorter!

import analysis.special_functions.pow

lemma timeout : (0 : ℝ) < 1 ^ (20 : ℝ) :=
begin
  norm_num1,
end

[Bhavik Mehta]

My guess is that this is a bug in how norm_num deals with real powers?

[Bhavik Mehta]

(0 : ℝ) < 1 ^ (20 : ℕ) is fine, and (0 : ℝ) < 1 ^ (19 : ℝ) is fine

[Bhavik Mehta]

(in my case it's easily worked-around though, with rpow_pos_of_pos)

[Kevin Buzzard]

@Gabriel Ebner @Mario Carneiro is this issue well-understood?

[Kevin Buzzard]

I'm interested because I feel like it's the only issue I ever run into with Lean 3 where I feel at a loss about how to solve it. Many other weird timeouts are fixed by making universes explicit, or using noncomputable!, but this one is nasty and I have no understanding of it.

[Mario Carneiro]

When there is a surprising performance cliff in norm_num kernel check time, the usual diagnosis is a bug in the proof construction. The reason it isn't always just a failure is because lean has all sorts of definitional equalities, so when you apply things which are of the wrong type lean just tries to unfold things until it works, leading to a huge cost. In this case, the bug was that it was expecting (20:ℝ) = ↑(20:ℕ) and I gave it ↑(20:ℕ) = (20:ℝ). This works even though it's wrong, because ↑(20:ℕ) and (20:ℝ) are defeq (at great expense)

[Kevin Buzzard]

Aah so this looks like it's totally unrelated to the x*y*0 slowness.

[Reid Barton]

In the original x*y*0 issue, I would guess that the elaborator has chosen some good sequence of unfoldings but the kernel chose a bad one; unfortunately there doesn't seem to be any sort of logging in the kernel is_def_eq check so I'm not sure how to debug it effectively

[Mario Carneiro]

#14099

[Kyle Miller]

I can't figure out how rfl : x*y*0=x*(y*0) works at all. I thought it was defined in terms of list concatenation (with multiple levels of quotients), but this identity doesn't work for lists concatenation directly:

example (α : Type) (x y : list α) :
  x ++ y ++ [] = x ++ (y ++ []) :=
begin
  refl, -- fails
end

Unless somehow the concatenation is reversed?

example (α : Type) (x y : list α) :
  ([] ++ x) ++ y = [] ++ (x ++ y) :=
begin
  refl, -- ok
end

[Reid Barton]

This is multiplication in the (additive) free abelian group on a monoid

[Reid Barton]

docs#free_abelian_group.semigroup

[Mario Carneiro]

Here's a simpler version:

import group_theory.free_abelian_group

namespace free_abelian_group
variables (α : Type) [monoid α] (x y : free_abelian_group α)

-- true but hard
example {β} [add_comm_group β] (f g : α → β) :
  lift f (abelianization.of $ free_group.mk []) =
  lift g (abelianization.of $ free_group.mk []) :=
rfl

-- true but harder, times out
example {β} [add_comm_group β] (f g : α → β) :
  lift (lift f) (abelianization.of $ free_group.mk []) =
  lift (lift g) (abelianization.of $ free_group.mk []) :=
rfl

[Mario Carneiro]

I think lift is not stated in a very defeq-friendly way

[Mario Carneiro]

well, really this kind of thing is never easy, not sure that we need to do anything about it

[Mario Carneiro]

the basic issue is that the heuristic f x =?= g y <- f =?= g, x =?= y is easy to mislead but also really important in practice

[Mario Carneiro]

In certain cases like this one, we want the iota reduction to take precedence (i.e. lift f (mk x) ~> f x) rather than going off on a wild goose chase on lift f (mk x) =?= lift g (mk x) <- f =?= g when we know f x and g x are obviously equal, but after they've been wrapped in this many layers of definition it is really hard to tell that this is still an iota rule

[Bhavik Mehta]

Mario Carneiro said:

#14099

Thanks for this!