!4#3082

Stream: mathlib4

[Chris Hughes]

I've just got this building again. It might be worth making this relatively high priority, because it keeps breaking against master. It also should hopefully restore behaviour a bit closer to mathlib3 and make porting a little easier.

[Scott Morrison]

It would be nice to sort out the Finset.mapEmbedding_apply issue, which seems worrying.

[Chris Hughes]

I'd err on the side of merging and then sorting it out but I'm biased.

[Eric Wieser]

Is there a reason you've put almost all of the PR description below the ---?

[Eric Wieser]

It looks to me like the mapEmbedding_apply failure is due to a missing delta reduction

[Eric Wieser]

That is, I think lean is being confused by the way that RelEmbedding is an alias for OrderEmbedding

[Eric Wieser]

Comparing terms, have := @mapEmbedding_apply α β f a gives

@FunLike.coe (Finset α ↪o Finset β) (Finset α) (fun a => (fun x => Finset β) a) RelHomClass.toFunLike
  (mapEmbedding f) a : (fun x => Finset β) a

but the goal contains

@FunLike.coe ((fun x x_1 => x ⊆ x_1) ↪r fun x x_1 => x ⊆ x_1) (Finset α) (fun a => Finset β) RelHomClass.toFunLike
  (mapEmbedding f) a : Finset β

[Chris Hughes]

Eric Wieser said:

Is there a reason you've put almost all of the PR description below the ---?

Habit. I'll change it I guess.

[Chris Hughes]

abbrev just seems like a bad idea to me. It's not reducible enough.

[Chris Hughes]

I see where the real problem lies. le_eq_subset is a simp lemma. So in Data.Finset.Powerset, dsimp only [RelEmbedding.coe_toEmbedding, mapEmbedding_apply] works but dsimp [RelEmbedding.coe_toEmbedding, mapEmbedding_apply] does not work. So it's probably a bad idea to use OrderEmbedding on things where we simplify le to a different relation.

[Chris Hughes]

Arguably mapEmbedding_apply is not in simp normal form on the LHS

[Chris Hughes]

Interestingly the linter doesn't see a problem here even though simp does not prove mapEmbedding_apply2

@[simp]
theorem mapEmbedding_apply : @FunLike.coe (RelEmbedding (. ≤ .) (. ≤ .)) _ _ _
     (mapEmbedding f) s = map f s :=
  rfl
#align finset.map_embedding_apply Finset.mapEmbedding_apply

@[simp]
theorem mapEmbedding_apply2 : @FunLike.coe (RelEmbedding (. ≤ .) (. ≤ .)) _ _ _
     (mapEmbedding f) s = map f s :=
  by simp

[Chris Hughes]

I'm not sure of the best solution here.

[Yaël Dillies]

order_embedding being an abbreviation of rel_embedding was arguably a bad design decision in the first place. I would personally be happy to make it its own structure.

[Eric Wieser]

It's a shame that (. ⊆ .) ↪r (. ⊆ .) delaborates as (fun x x_1 => x ⊆ x_1) ↪r fun x x_1 => x ⊆ x_1

[Chris Hughes]

Yaël Dillies said:

order_embedding being an abbreviation of rel_embedding was arguably a bad design decision in the first place. I would personally be happy to make it its own structure.

That's a long-term fix that, but I think a temporary fix would be better before that. I could write a new version of mapEmbedding_apply with the LHS in simp normal form perhaps, to be deleted when the refactor goes through?

[Eric Wieser]

Do we know why this only becomes a problem after !4#3082?

[Chris Hughes]

It's not clear. The LHS of mapEmbedding_apply in current mathlib4 contains the following term

@RelEmbedding.toEmbedding (Finset α) (Finset β) (fun x x_1 => x ≤ x_1) (fun x x_1 => x ≤ x_1) (mapEmbedding f) : Finset α ↪ Finset β

simp only [mapEmbedding_apply] can prove a version with subset instead of le

@RelEmbedding.toEmbedding (Finset α) (Finset β) (fun x x_1 => x ⊆ x_1) (fun x x_1 => x ⊆ x_1) (mapEmbedding f) : Finset α ↪ Finset β

So for some reason simp doesn't care about the difference between subset and le here, but it does in the new version.

The code producing this is

theorem mapEmbedding_apply : mapEmbedding f s = map f s :=
  rfl
#align finset.map_embedding_apply Finset.mapEmbedding_apply

theorem mapEmbedding_apply2 : mapEmbedding f s = map f s := by
  dsimp only [le_eq_subset]
  simp only [mapEmbedding_apply]