## Stream: general

### Topic: simp refuses to work

#### Patrick Massot (Jan 03 2021 at 11:58):

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 (Jan 03 2021 at 16:32):

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 (Jan 05 2021 at 09:59):

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

#### Gabriel Ebner (Jan 05 2021 at 10:07):

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,
/-
[fixed_no_param, fixed_no_param, fixed_no_param, fixed_no_param, fixed]
∀ [_inst_8 : vector_space 𝕜 ↥(F ⊓ ⊤)], findim 𝕜 ↥(F ⊓ ⊤) = findim 𝕜 ↥(F ⊓ ⊤)
-/


#### Kevin Buzzard (Jan 05 2021 at 10:32):

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 (Jan 05 2021 at 10:34):

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

#### Eric Wieser (Jan 05 2021 at 10:36):

Because the type-class instances come after the vector space

Which instances are you referring to?

#### Gabriel Ebner (Jan 05 2021 at 10:37):

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 (Jan 05 2021 at 10:41):

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 (Jan 05 2021 at 10:46):

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 (Jan 05 2021 at 10:46):

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

#### Bryan Gin-ge Chen (Jan 05 2021 at 10:56):

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 (May 01 2022 at 21:36):

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?

Last updated: Aug 03 2023 at 10:10 UTC