Data.Finset.Sups mathlib4#1663

Stream: mathlib4

[Moritz Firsching]

mathlib4#1663
While porting this, I get twice the error redundant binder annotation update. What is this about and how to fix it?

[Arien Malec]

There's already a u declared

[Arien Malec]

It's weird because when you delete the u, theorems suddenly fail to typecheck, despite making no mention of u (which is confusingly a variable, not a universe) and then the error on the second variable declaration goes away.

[Arien Malec]

I think what's going on is that you can declare a as implicit via then re-declare it as explicit:

variable {a}
-- stuff
variable (a) -- OK

But you can't re-declare it as implicit:

variable {a}
-- stuff
variable {a} -- error about redundant binder annotation update

I assume that the error about u made Lean not process the legal update to s so the (again legal) update back to explicit got the same error.

[Moritz Firsching]

Thanks for the explanation!
I'm still not quite sure how to fix it...

[Kevin Buzzard]

In the lean 3 file on line 222 u is made implicit when it's already implicit. In lean 3 this was a no-op and in lean 4 it's an error. Just remove u from the list.

[Kevin Buzzard]

Oh I see -- and then you have to fix the proofs that mathport has borked because it seems to have choked on the variables line and not made anything implicit at allback to how they were. For example

theorem disjSups_subset_left (ht : t₁ ⊆ t₂) : s ○ t₁ ⊆ s ○ t₂ := by
  exact disjSups_subset Subset.rfl ht
#align finset.disj_sups_subset_left Finset.disjSups_subset_left

theorem disjSups_subset_right (hs : s₁ ⊆ s₂) : s₁ ○ t ⊆ s₂ ○ t :=
  disjSups_subset hs Subset.rfl
#align finset.disj_sups_subset_right Finset.disjSups_subset_right

You can see from the mathlib3 file that this is what the proofs are supposed to be.

[Kevin Buzzard]

theorem disjSups_subset_iff : s ○ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → a ⊔ b ∈ u :=
  forallDisjSups_iff

(again the same as the mathlib3 proof)

[Kevin Buzzard]

@Mario Carneiro it seems that if mathlib3 has any lines of the form

variables {s t u : finset X}
...
variables (s t)
...
variables {s t u}

then Lean 4 complains about the second variables {s t u} (because u is already implicit) but Lean 3 doesn't. As a consequence mathport seems to completely ignore the variables {s t u} line and then translation is messed up because mathport puts in a bunch of _s which weren't there in Lean 3. This happens at least once in mathlib and who knows how often.

[Mario Carneiro]

mathport can't possibly be affected by such an error

[Kevin Buzzard]

Oh OK thanks. Maybe the user did this then :-)

[Mario Carneiro]

I would expect it to just regurgitate a line like variable {s t u} as is

[Kevin Buzzard]

Yes sorry you're right, mathport is emitting the correct code. @Moritz Firsching did you "fix" the proofs above and in fact my suggestions are just to un"fix" them to how mathport had them?

[Moritz Firsching]

thanks, removing the u and reverting my "fixes" worked! I had indeed put in the _ _ _ _