List.subset weak implicit

Stream: mathlib4

[Chris B]

The Lean 4 implementation of List.subset makes the bound argument a regular implicit instead of a weak implicit as it was in vanilla mathilb.

-- The new one
protected def subset (l₁ l₂ : List α) := ∀ {a : α}, a ∈ l₁ → a ∈ l₂

This causes some issues that feel like they shouldn't be there; is this a holdover from when weak implicits were supposedly not going to be in Lean 4, or is there a more concrete reason for the change? As an example, this unintuitive failure the exact tactic when the hypothesis exactly matches the goal even with pp set to all:

h2 : l ⊆ x :: y :: l
⊢ l ⊆ x :: y :: l

exact h2

/-
type mismatch
  h2
has type
  ?m.2183 ∈ l → ?m.2183 ∈ x :: y :: l : Prop
but is expected to have type
  l ⊆ x :: y :: l : Prop
-/

With the pp set to all:

h2 : @Subset.subset (List α) (@instSubsetList α) l (@List.cons α x (@List.cons α y l))
⊢ @Subset.subset (List α) (@instSubsetList α) l (@List.cons α x (@List.cons α y l))

exact h2
/-
type mismatch
  @h2 ?m.2183
has type
  @Mem.mem α (List α) (@instMemList α) ?m.2183 l →
    @Mem.mem α (List α) (@instMemList α) ?m.2183 (@List.cons ?m.2139 x (@List.cons ?m.2141 y l)) : Prop
but is expected to have type
  @Subset.subset (List α) (@instSubsetList α) l (@List.cons α x (@List.cons α y l)) : Prop
-/

[Scott Morrison]

I would guess it is a holdover. I tried it out switching to {{ ... }}, and after a few fixes everything works.

[Scott Morrison]

Let me know if you'd like me to make a PR.

[Chris B]

Sure, thanks. It came up in the context of porting the basics for list permutation and multisets, so if you don't get around to it I'll include it in those.