Zulip Chat Archive

Stream: general

Topic: simp refuses to work


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

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

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Jan 05 2021 at 10:34):

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

view this post on Zulip Eric Wieser (Jan 05 2021 at 10:36):

Because the type-class instances come after the vector space

Which instances are you referring to?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Jan 05 2021 at 10:46):

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

view this post on Zulip 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.


Last updated: May 13 2021 at 18:26 UTC