Classical

Stream: mathlib4

[Xavier Roblot]

!4#2168 has several instances failing, eg.
failed to synthesize instance Fintype (Sym2 α)
failed to synthesize instance DecidableEq (Sym α n)
These can all be solved by adding open Classical at the beginning of the file.
Is that an acceptable solution (together with a porting note)?

Note that there is proof by rfl that does not work anymore and that I cannot fix...

[Eric Wieser]

That's not a good fix

[Eric Wieser]

Is there a missing forward-port for a dependency of port-status#data/finset/sym?

[Xavier Roblot]

I'll check that

[Eric Wieser]

I will push an update to the dashboard to display that shortly...

[Eric Wieser]

In the meantime, check out the mathlib3 version and work out which instance it's finding

[Xavier Roblot]

Ok, so adding manually the proof for each missing instance does solve the problem. Thanks!

[Xavier Roblot]

I still have a failing rfl though...

[Eric Wieser]

What do you mean by that? The instance still exists, but Lean can no longer find them?

[Xavier Roblot]

Well, I add to add the following lines:

noncomputable instance : DecidableRel (fun x y : α × α ↦ x ≈ y) :=
  Classical.decRel (fun x y : α × α ↦ x ≈ y)
noncomputable instance [Fintype α] : Fintype (Sym2 α) :=
  Quotient.fintype (Sym2.Rel.setoid α)

[Xavier Roblot]

And then Lean stopped complaining about failed to synthesize instance

[Eric Wieser]

What instance is being found in mathlib3?

[Xavier Roblot]

These instances were automatically generated in mathlib3. I just asked Lean3 to tell me explicitly the proof of these instances and copy them to mathlib4.

[Eric Wieser]

These instances were automatically generated in mathlib3

Sure, but all instances have a name. Which instance is it finding?

[Eric Wieser]

Was Classical.decRel really being used in mathlib3?

[Xavier Roblot]

Oh, I see what you mean. I did library_search to find the proof but I should have used show_term instead, I guess.

[Eric Wieser]

Or just use set_option pp.implicit true to inspect the statement

[Xavier Roblot]

The fist one is named sym2.rel.decidable_rel

[Eric Wieser]

Great, does that exist in mathlib4?

[Eric Wieser]

docs4#Sym2.instDecidableRelProdRel ?

[Xavier Roblot]

Nope

[Eric Wieser]

Edited with the real name

[Xavier Roblot]

Ok, it's there and it is imported in the file. Ok, so I use that to prove the instance now?

[Eric Wieser]

No, now you ask "why can lean find this instance in Lean3, but not in Lean4"

[Xavier Roblot]

Let me have a look at it...

[Eric Wieser]

Which might be some combination of:

• There is a bug in lean4
• There is another missing instance it needs
• Mathport didn't port something correctly and your context is not what it's supposed to be
• A human didn't port something correct, either you higher up in the file, or someone else in an upstream file.

[Eric Wieser]

My guess is that probably the fix is

-- porting note: Lean3 unfolded `Sym2` to find this
instance [Fintype α] [DecidableEq α] : Fintype (Sym2 α) :=
  Quotient.fintype _  -- check `infer_instance` doesn't work here

[Eric Wieser]

Eric Wieser said:

I will push an update to the dashboard to display that shortly...

Done, see the link above

[Xavier Roblot]

Eric Wieser said:

My guess is that probably the fix is

-- porting note: Lean3 unfolded `Sym2` to find this
instance [Fintype α] [DecidableEq α] : Fintype (Sym2 α) :=
  Quotient.fintype _  -- check `infer_instance` doesn't work here

This fails with error

failed to synthesize instance
  DecidableRel fun x x_1 => x ≈ x_1

[Kyle Miller]

Did you put that right after Sym2.instDecidableRelProdRel? (right here)

[Xavier Roblot]

Ok, so if I add the lines as Kyle suggested:

instance (α : Type _) [DecidableEq α] : DecidableRel (Sym2.Rel α) := fun x y =>
  decidable_of_bool (relBool x y) (relBool_spec x y)

-- porting note: Lean3 unfolded `Sym2` to find this
instance [Fintype α] [DecidableEq α] : Fintype (Sym2 α) := Quotient.fintype _

I get a new error: the Fintype is in red and it says

invalid binder annotation, type is not a class instance
  ?m.77695
use the command `set_option checkBinderAnnotations false` to disable the check

[Xavier Roblot]

Yeah, that's because Fintype is not imported in this file...

[Xavier Roblot]

Ok, if I import Data.Set.finite so that it knows about fintype and product of fintype being also a fintype, I still get the same error

failed to synthesize instance
  DecidableRel fun x x_1 => x ≈ x_1

[Xavier Roblot]

Same error if I give explicitly the setoid:

instance [Fintype α] [DecidableEq α] : Fintype (Sym2 α) :=
  Quotient.fintype (Sym2.Rel.setoid α)

[Kyle Miller]

The issue is that Fintype is not imported in this file. (Edit: oh, missed that comment in the middle where you said that.)

[Xavier Roblot]

Kyle Miller said:

The issue is that Fintype is not imported in this file.

Yes, I fixed that, but that still does not work...

[Eric Wieser]

Can you give the full error message including the context?

[Eric Wieser]

It's possible that the problem is that Lean4 no longer sees through the equiv symbol

[Xavier Roblot]

Screenshot-2023-02-09-at-15.39.14.png

[Eric Wieser]

I suspect we want a Quotient.fintype' that is expressed in terms of setoid.r instead of \approx

[Eric Wieser]

Can you add that to the line above and see if it helps?

[Kyle Miller]

Here's one way to get it to work:

instance [Fintype α] [DecidableEq α] : Fintype (Sym2 α) :=
  have : DecidableRel (· ≈ · : α × α → α × α → Prop) := instRelDecidable _
  Quotient.fintype _

[Kyle Miller]

I gave the preceding instance a name:

instance instRelDecidable (α : Type _) [DecidableEq α] : DecidableRel (Sym2.Rel α) := fun x y =>
  decidable_of_bool (relBool x y) (relBool_spec x y)

[Eric Wieser]

I'd prefer that we add the fintype' instance to that have statement

[Eric Wieser]

I think this will come up for other quotient types

[Kyle Miller]

What that would make sense for other quotients, here Sym2 uses a global setoid instance on Prod, which isn't great. I'd prefer we fix that instead.

[Eric Wieser]

In that case we should make the DecidableRel (· ≈ · : α × α → α × α → Prop) instance global too (until we make the refactor you suggest)

[Xavier Roblot]

Eric Wieser said:

Can you add that to the line above and see if it helps?

I am going to be afk for the next hour. I’ll try that when I come back

[Eric Wieser]

I think we instead want:

-- name the existing instance
instance instRelDecidable (α : Type _) [DecidableEq α] : DecidableRel (Sym2.Rel α) := fun x y =>
  decidable_of_bool (relBool x y) (relBool_spec x y)

instance instRelDecidable' (α : Type _) [DecidableEq α] : DecidableRel (· ≈ · : α × α → α × α → Prop) :=
  instRelDecidable _

[Xavier Roblot]

Yes, that works!

[Xavier Roblot]

There is another instance that I added to make things work. I'll see if I can fix that using a similar method.

[Xavier Roblot]

The missing instance is DecidableEq (Sym α n) which can be proved by:

instance [DecidableEq α]: DecidableEq (Sym α n) := Subtype.instDecidableEqSubtype

This instance does not exists in mathlib3 nor in mathlib4. In mathlib3, it is synthesized automatically but not in mathlib4 for some reason. Should I jut add it to Data.Sym.Basic where Sym α n is defined?

[Reid Barton]

There seems to be a common theme about synthesizing DecidableEq instances, presumably involving the amount of unfolding that Lean 4 allows differing from Lean 3. It would be great if someone could isolate an example of this.