Issues in !4#2530 (Combinatorics.Derangements.Basic)

Stream: mathlib4

[Arien Malec]

I've got most of the issues addressed here. Two remaining that need higher power attention:

1) In atMostOneFixedPointEquivSumDerangements

• we had a universe issue, which I think I've annotated correctly, but now we have a type/sort issue. If I follow the logic on the Lean 3 side, this didn't seem to bother Lean 3 but does worry Lean 4.
• we have a timeout figuring out that if a is DecidableEq then p a is Decidable

2) In derangementsOptionEquivSigmaAtMostOneFixedPoint as far as I can tell, Lean 3 accepted an Equiv to close the goal, but Lean 4 won't. library_search tells me that I can close the goal with a classical assumption, but this requires marking the def as noncomputable

[Eric Wieser]

Are you sure the Lean3 universes in question are the same as the Lean4 ones?

[Arien Malec]

I don't see anything on the Lean 3 side that's not u_1

[Eric Wieser]

docs4#Equiv.subtypeSubtypeEquivSubtypeInter vs docs#equiv.subtype_subtype_equiv_subtype_inter

[Eric Wieser]

The Lean4 one is Sort u, the Lean3 one is Type u

[Arien Malec]

There's the type/sort issue.

[Arien Malec]

It's confusing because when I hover over the type in VS Code, I get Sort u

[Eric Wieser]

So either we should undo the generalization of that def, or we should backport it and see what breaks

[Arien Malec]

(On the Lean 3 side).

[Eric Wieser]

Note that mathport gives an error message about this:

/- warning: equiv.subtype_subtype_equiv_subtype_inter -> Equiv.subtypeSubtypeEquivSubtypeInter is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} (p : α -> Prop) (q : α -> Prop), Equiv.{succ u1, succ u1} (Subtype.{succ u1} (Subtype.{succ u1} α p) (fun (x : Subtype.{succ u1} α p) => q (Subtype.val.{succ u1} α p x))) (Subtype.{succ u1} α (fun (x : α) => And (p x) (q x)))
but is expected to have type
  forall {α : Sort.{u1}} (p : α -> Prop) (q : α -> Prop), Equiv.{max 1 u1, max 1 u1} (Subtype.{max 1 u1} (Subtype.{u1} α p) (fun (x : Subtype.{u1} α p) => q (Subtype.val.{u1} α p x))) (Subtype.{u1} α (fun (x : α) => And (p x) (q x)))
Case conversion may be inaccurate. Consider using '#align equiv.subtype_subtype_equiv_subtype_inter Equiv.subtypeSubtypeEquivSubtypeInterₓ'. -/
/-- A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. -/

[Eric Wieser]

But no one ever reads these because they don't appear till after the port has already happened

[Arien Malec]

Ah, no, that's not right. There's an explicit annotation on the Lean 3 side.

[Arien Malec]

-- A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. -/
@[simps] def subtype_subtype_equiv_subtype_inter {α : Type u} (p q : α → Prop) :
  {x : subtype p // q x.1} ≃ subtype (λ x, p x ∧ q x) :=
(subtype_subtype_equiv_subtype_exists p _).trans $

[Eric Wieser]

Right, that def was ported incorrectly

[Arien Malec]

I'll fix in this PR.

[Eric Wieser]

Or at least, someone made a refactor while porting it, and you're dealing with the fallout from that

[Eric Wieser]

There are quite a lot of declarations with the same Type/Sort generalization in that file.

[Eric Wieser]

I think it's enough of a mess to warrant its own PR fixing all of the errors that mathport is complaining about

[Arien Malec]

lmk if you want me to do the PR or if you want to, and I'll make this PR dependent.

As an update, the Sort -> Type update makes progress, but we are in type/instance inference hell.

[Eric Wieser]

I'd still lean towards backporting a switch to Sort instead

[Arien Malec]

Update on this one: I did the surgical Sort to Type switch to make progress, and I've got the file to the point where this is the only error.

Right now, it times out in instance search for the same reasons as noted here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/instance.20search.20timeouts.20in.20!4.232547

I have a type for the type hole from the Lean 3 side, but that leads to a metavar leaking through the refine'

[Arien Malec]

It's all documented in the file (and I'll add a comment in the PR itself) if anyone wants to take a look.

[Arien Malec]

I've now got it down to either a wanting proof or declaration that DecidablePred (fun (x: α) => x ∈ ({a}ᶜ : Set α))

[Arien Malec]

It feels like membership in a singleton should be decidable...

[Kevin Buzzard]

That sounds the same as decidable equality

[Arien Malec]

In the binding, we have [DecidableEq α] so yeah...

[Eric Wieser]

Eric Wieser said:

I'd still lean towards backporting a switch to Sort instead

Done in #18543

[Arien Malec]

Lmk when it hits the Mathlib4 side & I’ll take a dependency

[Eric Wieser]

You can already mark a dependency from a mathlib4 to a mathlib3 PR, although I guess it won't help you

[Arien Malec]

Documented with a plan in the PR.

In the meantime, any proof that DecidableEq a → DecidablePred (fun (x: α) => x ∈ ({a}ᶜ : Set α)) welcome

[Eric Wieser]

Does lean3 prove it with apply_instance?

[Eric Wieser]

If so, look at the term it produces and work out which piece is missing

[Arien Malec]

Traveling now but will try this.

[Arien Malec]

Lean 3 tells me that that the Lean 3 equivalent of fun (a : α) => Set.Compl.decidableMem {a} a shows what's required, but this isn't accepted on the Lean 4 side, because failed to synthesize instance (j : α) → Decidable (j ∈ {a})

I'll work on adding Decidable (j ∈ {a}), which seems easy given [DecidableEq a]

[Eric Wieser]

That will already exist in lean 3

[Eric Wieser]

Play the same game again and ask lean3 how it found that

[Eric Wieser]

Or use set_option pp.explicit true on your original experiment

[Arien Malec]

That game got confusing very quickly, but this works:

namespace Set

instance singleton.decidableMem {α: Type _} {a j: α} [DecidableEq α] :
    Decidable (j ∈ ({a} : Set α)) := by
      simp [Set.singleton]; infer_instance

end Set

[Eric Wieser]

What instance does lean 3 find for that

[Arien Malec]

That's where things got very confusing...

[Eric Wieser]

What does by show_term { apply_instance } give for that example in lean 3?

[Arien Malec]

don't know how to synthesize placeholder
context:
α : Type u,
a j : α,
_inst_1 : decidable_eq α
⊢ Type ?

[Arien Malec]

oh, that was infer_instance....

set.decidable_set_of j (λ (b : α), b = a)

[Arien Malec]

Which does exist in mathlib4....

docs4#Set.decidableSetOf

[Arien Malec]

And this works too

namespace Set

instance singleton.decidableMem {α: Type _} {a j: α} [DecidableEq α] :
    Decidable (j ∈ ({a} : Set α)) := decidableSetOf j (fun (b : α) => b = a)

end Set

[Eric Wieser]

So it looks like the conclusion is that in Lean 3, typeclass resolution unfolded {x} to {y | y = x}

[Eric Wieser]

But that this doesn't work in lean 4

[Eric Wieser]

I think your instance is reasonable (especially with the last proof), though it should be called Set.decidableMemSingleton.

[Reid Barton]

Yeah this seems to be a recurring issue with decidability (I doubt it is specific to decidability, rather decidability just hits it the most often).

[Eric Wieser]

The lean 4 behavior seems pretty reasonable here, it's just annoying to track down when ported code breaks

[Arien Malec]

!4#2671