simp refuses to work

Stream: general

[Patrick Massot]

Can anyone explain

import linear_algebra.finite_dimensional

open finite_dimensional

example {α : Type*} [semilattice_inf_top α] [has_coe_to_sort α] (a : α) : ↥(a ⊓ ⊤ : α) = ↥a :=
by squeeze_simp

example {𝕜 E : Type*} [field 𝕜] [add_comm_group E] [vector_space 𝕜 E] [finite_dimensional 𝕜 E]
  {F : submodule 𝕜 E} : findim 𝕜 (F ⊓ ⊤ : submodule 𝕜 E) = findim 𝕜 F :=
begin
  -- simp, -- fails
  -- simp only [inf_top_eq], --fail
  rw [inf_top_eq], --works
end

[Bryan Gin-ge Chen]

Not sure if this helps, but here's the trace output for the two examples (I don't really understand the canonize_instances option but it reduced the amount of output in the working case.)

import linear_algebra.finite_dimensional

open finite_dimensional

set_option trace.simplify true
example {α : Type*} [semilattice_inf_top α] [has_coe_to_sort α] (a : α) : ↥(a ⊓ ⊤ : α) = ↥a :=
by simp only [inf_top_eq] {canonize_instances:=ff}
/-
[simplify] eq: ↥(a ⊓ ⊤) = ↥a
[simplify] eq: ↥(a ⊓ ⊤)
[simplify] eq: a ⊓ ⊤
[simplify] eq: a
[simplify] eq: ⊤
[simplify] eq: ⊤
[simplify] eq: has_inf.inf
3. [simplify.rewrite] [inf_top_eq]: a ⊓ ⊤ ==> a
[simplify] eq: coe_sort
[simplify] eq: ↥a
[simplify] eq: a
[simplify] eq: coe_sort
[simplify] eq: eq
-/

example {𝕜 E : Type*} [field 𝕜] [add_comm_group E] [vector_space 𝕜 E] [finite_dimensional 𝕜 E]
  {F : submodule 𝕜 E} : findim 𝕜 (F ⊓ ⊤ : submodule 𝕜 E) = findim 𝕜 F :=
begin
  simp only [inf_top_eq] {canonize_instances:=ff}, --fail
/-
[simplify] eq: findim 𝕜 ↥(F ⊓ ⊤) = findim 𝕜 ↥F
[simplify] eq: findim 𝕜 ↥(F ⊓ ⊤)
[simplify] eq: findim
[simplify] eq: findim 𝕜 ↥F
[simplify] eq: findim
[simplify] eq: eq
-/
end

[Bryan Gin-ge Chen]

@Gabriel Ebner since you're looking at simp things, do you know what might be going on here?

[Gabriel Ebner]

The culprit is findim. Because the type-class instances come after the vector space, the automatically generated congruence lemmas don't permit rewriting the vector space:

import linear_algebra.finite_dimensional
open finite_dimensional tactic
example {𝕜 E : Type*} [field 𝕜] [add_comm_group E] [vector_space 𝕜 E] [finite_dimensional 𝕜 E]
  {F : submodule 𝕜 E} : findim 𝕜 (F ⊓ ⊤ : submodule 𝕜 E) = findim 𝕜 F := by do
`(%%lhs = _) ← target,
lem ← mk_specialized_congr_lemma_simp lhs,
trace lem.arg_kinds,
trace lem.type,
admit
/-
[fixed_no_param, fixed_no_param, fixed_no_param, fixed_no_param, fixed]
∀ [_inst_8 : vector_space 𝕜 ↥(F ⊓ ⊤)], findim 𝕜 ↥(F ⊓ ⊤) = findim 𝕜 ↥(F ⊓ ⊤)
-/

[Kevin Buzzard]

It is a crying shame that we have to come to Gabriel and others of his ilk to ask these questions, and they come up with these brilliant diagnoses involving using clever tricks which are totally undocumented. My system of "starring interesting posts" has failed; I have too much starred now. I don't know what to do about this.

[Bryan Gin-ge Chen]

We could start documenting these clever tricks somewhere on our website.

[Eric Wieser]

Because the type-class instances come after the vector space

Which instances are you referring to?

[Gabriel Ebner]

findim : Π (K : Type u_2) (V : Type u_1) [field K] [add_comm_group V] [vector_space K V], ℕ

Everything that comes after V.

[Alex J. Best]

So does this mean

findim : Π (K : Type u_2) [field K] (V : Type u_1) [add_comm_group V] [vector_space K V], ℕ

is a better definition (which should be an invisible change to uses of findim without an @).
Is this something we should be changing everywhere then?
I guess we could make a linter for this: Like non-instance binders must come as late as possible in the list of binders?

[Gabriel Ebner]

It's not the literal order that matters, but the dependencies. As long as there are type-class arguments that depend on V, you can't rewrite V.

[Eric Wieser]

By "vector space", did you meanV or vector_space K V?

[Bryan Gin-ge Chen]

I suppose it's not feasible to add every possible rewrite that's blocked by this as additional simp lemmas, right?

Maybe rewrite_search would be able to solve this.

[Eric Wieser]

The small congruence changes in lean 3 since this thread was made haven't made any difference. Are we able to reproduce this in Lean 4, or is it fixed there?