instance [...] by apply_instance

Stream: general

[Damiano Testa]

Dear All,

in PR #7940, I seem to be in the following situation. I introduced one instance and noticed that two instances that existed are now proved by by apply_instance. Thus, I removed these two instances.

However, CI now complains that one of the instances that I deleted is missing.

Before I go and try to minimize an example, I thought of asking here, since I imagine that if this is expected behaviour, someone here in the chat will know!

So, is there ever the need to have an explicit instance available, whose proof is by apply_instance?

Thanks!

[Kevin Buzzard]

I'm no expert but my gut feeling is that there shouldn't be.

[Damiano Testa]

Ok, I will try to minimize an example and debug this: I think that this is what is happening, but I am not entirely sure.

[Damiano Testa]

Not really minimal, but close, I hope!

import data.nat.with_bot

--/-  if you remove the initial two dashes, the lemma below no longer works
instance am_i_needed (M : Type*) [ordered_add_comm_monoid M] :
  covariant_class M M (function.swap (+)) (≤) :=
by apply_instance
--/

lemma add_le_add_new {a b c d : with_bot ℕ} (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d :=
trans (add_le_add_left h₂ _) (add_le_add_right h₁ d)

[Damiano Testa]

At least on my computer, when I remove the two dashes (-) to comment the instance, lemma add_le_add_right in the proof of lemma add_le_add_new no longer works.

[Damiano Testa]

(I would try to minimize this further, but I am meeting a student in 3 minutes and wanted to get this out of the way before that! :upside_down: )

[Mario Carneiro]

it works for me with or without the instance, although maybe I'm not on the latest mathlib

[Kevin Buzzard]

On the adomani_covariant_instances branch it doesn't work.

[Kevin Buzzard]

import data.nat.with_bot

example : ordered_add_comm_monoid (with_bot ℕ) := infer_instance

instance foo (M : Type*) [ordered_add_comm_monoid M] :
  covariant_class M M (function.swap (+)) (≤) := infer_instance

instance bar : covariant_class (with_bot ℕ) (with_bot ℕ)
  (function.swap has_add.add) has_le.le := infer_instance

bar fails without foo on that branch

[Kevin Buzzard]

(and then Lean ends up in that state where if you put a foot wrong you get excessive memory consumption errors which I usually fix by restarting VS Code)

[Damiano Testa]

Kevin, thanks a lot for looking at this! I think that on some version of master, the instance is there, which might explain why it appears to work for Mario. Anyway, I am glad that someone else is seeing the same behaviour, since I was also getting lots of excessive memory afterwards and was not sure whether that had something to do with the issue.

[Damiano Testa]

(in case you do not want to go to the adomani_covariant_instances branch, the with_bot nat appears when doing computations with the degree of polynomials.)

[Damiano Testa]

I went ahead and reintroduced the instances with the by apply_instance proof and a comment before them. I want to make sure that nothing else breaks. If you want to get to the stage where the weirdness happened, this is the commit hash is

6d0a12adbf460f6d506294851cdedbf93d75f7f2

[Damiano Testa]

In case anyone is interested, adding back the two instances proved by by apply_instance made PR #7940 build successfully. You can see that the previous attempt failed and that the only change has been to reintroduce the "automatic" instances.

I am going to leave the PR as awaiting review, but if anyone has an idea of how to make this more efficient, I would be happy to hear any suggestion!

[Damiano Testa]

I tried producing a shorter example, but failed. Still, it seems from the builds of this PR that an instance that can be proven by by apply_instance need not be superfluous.

I left comments about this above the relevant instances: should I do something else?

Ideally, I would like to get rid of these instances, but, for the moment, I can live with keeping them, since I do think that their consequences are useful!

[Kevin Buzzard]

I have seen things like this in mathlib by the way, labelled as "shortcuts for type class inference". Here is a load in data.rat.basic. But I think your problem is different.