failed to synthesize type class instance

Stream: general

[Kenny Lau]

class foo : Type.

theorem zero_eq_zero_of_foo [foo] : 0 = 0 := rfl

example : 0 = 0 := by rw zero_eq_zero_of_foo

[Kenny Lau]

error:

invalid rewrite tactic, failed to synthesize type class instance
state:
⊢ 0 = 0

[Kenny Lau]

is it possible to know which type class instance it failed to synthesize?

[Mario Carneiro]

I think it failed to synthesize foo

[Mario Carneiro]

more to the point, you can just provide the explicit args to the rewrite, and that should be enough to get typeclass inference to trigger

[Mario Carneiro]

I think you can also write something like rw @zero_eq_zero_of_foo _ so that the typeclass inference is done beforehand instead of in the rewrite

[Bernd Losert]

This is the error:

error: failed to synthesize type class instance for
α : Type u_1,
β : Type u_2,
f : α → β,
t : convergence_space β,
x : α,
l l' : filter α,
hl : l.ne_bot,
h₀ : l ≤ l',
h₁ : conv (map f l') (f x),
h₂ : map f l ≤ map f l'
⊢ l.ne_bot
state:
α : Type u_1,
β : Type u_2,
f : α → β,
t : convergence_space β,
x : α,
l l' : filter α,
hl : l.ne_bot,
h₀ : l ≤ l',
h₁ : conv (map f l') (f x),
h₂ : map f l ≤ map f l'
⊢ conv (map f l) (f x)

I don't understand this. It seems that it needs an l.ne_bot, but there is one already, namely hl. I am at a loss about what to do here.

[Yury G. Kudryashov]

An #mwe would help

[Bernd Losert]

I tried making a mwe, but they all work.

[Yury G. Kudryashov]

Does lemma assume (hl : l.ne_bot) or [hl : l.ne_bot]? In the former case, you need resetI.

[Bernd Losert]

It uses [hl : l.ne_bot].

[Bernd Losert]

Here's the lemma:

(le_conv : ∀ {x : α} {l l' : filter α} [ne_bot l], l ≤ l' → conv l' x → conv l x)

[Yury G. Kudryashov]

You need resetI or introI

[Yury G. Kudryashov]

Why do you need ne_bot here?

[Bernd Losert]

In this silly example: the [ne_bot l] works without me doing anything special:

def foo (l : filter α) [ne_bot l] : filter α := l
theorem bar (l : filter α) [ne_bot l] (f : α → β) : filter β :=
begin
  intros,
  have l' : filter β, from foo (map f l),
  exact l'
end

[Bernd Losert]

Yury G. Kudryashov said:

Why do you need ne_bot here?

That's part of the lemma.

[Yury G. Kudryashov]

What is the statement of the lemma you're trying to prove?

[Yury G. Kudryashov]

IMHO conv shouldn't assume ne_bot, and the trivial filter should converge to any point.

[Yury G. Kudryashov]

(note that the same sequence can converge to two different points in a non-Hausdorff topological space)

[Bernd Losert]

Ah, I just noticed something. In the silly example, if I replace intros with intros l lh f, then it stops working. I'm also doing this in the real proof.

[Yury G. Kudryashov]

Why do you need intros in the example?

[Bernd Losert]

Is there a special rule regarding intros of variables for instance arguments.

[Bernd Losert]

The intros is there to simulate what I'm doing in the real proof.

[Yury G. Kudryashov]

Is it actually

theorem bar (l : filter α) [ne_bot l] (f : α → β) : filter β :=

or

theorem bar : ∀ (l : filter α) [ne_bot l] (f : α → β), filter β :=

[Bernd Losert]

It's the first one.

[Yury G. Kudryashov]

This intros is a no-op.

[Bernd Losert]

Ah, OK.

[Bernd Losert]

Let me use a forall then.

[Yury G. Kudryashov]

Use introI or intros l hl, resetI to introduce instance vars.

[Bernd Losert]

Aha. It produces the same error.

[Yury G. Kudryashov]

And these lemmas should not need [ne_bot l].

[Bernd Losert]

Yury G. Kudryashov said:

Use introI or intros l hl, resetI to introduce instance vars.

It works. Cool. Where is this documented? Is it in "Theorem Provinig in Lean"?

[Yury G. Kudryashov]

tactic#resetI

[Bernd Losert]

Ah, so it's a mathlib specific tactic? It's not part of core Lean? Interesting.

[Bernd Losert]

I need the [ne_bot l] since I need to rule out the bottom filter.

[Yury G. Kudryashov]

Why do you need to rule out the bottom filter?

[Yury G. Kudryashov]

If conv l x corresponds to l ≤ nhds x, then you should have ∀ x, conv ⊥ x.

[Bernd Losert]

I'm working in the more general setting of convergence spaces, so there are no neighborhoods. But yeah, I want to rule out ∀ x, conv ⊥ x because that will always be the case according to the convergence space axioms without the [ne_bot l] constraint.

[Yury G. Kudryashov]

Why do you want to rule out this?

[Yury G. Kudryashov]

A topological space should define a convergence space, and in a topological space this is true.

[Bernd Losert]

Is it? I may be misunderstanding something. If the space is Hausdorff, then every filter has at most one limit. This won't work if the bottom filter converges to everything. Unless... Hausdorff means that every ne_bot filter has at most one limit.

[Yury G. Kudryashov]

If the space is Hausdorff, then every nontrivial filter has at most one limit.

[Yury G. Kudryashov]

docs#tendsto_nhds_unique

[Bernd Losert]

OK. That's the part that was missing in my mind. It's a bit confusing since Lean allows the bottom filter to be a filter, but in the literature this is ruled out.

[Yury G. Kudryashov]

It is very convenient to have a docs#complete_lattice structure on filters.

[Yury G. Kudryashov]

But you have to adjust statements/proofs from textbooks.

[Bernd Losert]

Yeah. I'm having some problem adjusting things as you can tell.

[Bernd Losert]

Thanks for your help. Much appreciated.

[Reid Barton]

I think using the class ne_bot is not helping here. You can also just write (hl : l ≠ ⊥) and it should make life simpler and easier.