Zulip Chat Archive

Stream: general

Topic: simp simp

Eric Wieser (Dec 06 2021 at 16:04):

In this example I need to call simp twice to close the goal:

import data.dfinsupp
import algebra.module.submodule

@[congr[
lemma set_like.dep_congr {ι α β P} [set_like P α]
  {p : ι → P} (f : Π i, p i → β) :
  ∀ {i j} (x : p i) (h : i = j), f i x = f j ⟨x, h ▸ x.prop⟩
| i _ ⟨x, px⟩ rfl := rfl

variables {ι R M : Type*}
  [decidable_eq ι] [add_monoid ι]
  [semiring R] [add_comm_monoid M] [module R M]

example (p : ι → submodule R M) :
  @dfinsupp.single _ (λ i, p i) _ _ (multiplicative.to_add 1) ⟨0, submodule.zero_mem _⟩ =
    dfinsupp.single 0 ⟨0, submodule.zero_mem _⟩ :=
begin
  dsimp only,  -- delta reduce an instance argument, so that simp has to make real progress
  simp,
  simp,
end

Is my @[congr] lemma bad?

Gabriel Ebner (Dec 06 2021 at 16:05):

Are you sure that congr lemma is even used? (The head symbol is a variable, so it won't be found in the index.)

Eric Wieser (Dec 06 2021 at 16:06):

Yes, the second simp fails without it

Eric Wieser (Dec 06 2021 at 16:08):

~~(and the first one amounts to a dsimp only that cleans up an instance argument)~~ edited so that the first simp fails without @[congr]

Eric Wieser (Dec 06 2021 at 16:18):

I suspect the problem is that the congr lemma doesn't let x be replaced with some y on the RHS, but also I can't work out how to state that in a way that congr accepts

Eric Wieser (Dec 06 2021 at 16:29):

set_like isn't to blame either, this fails with a submodule-specific lemma too:

@[congr]
lemma submodule.dep_congr {ι β}
  {p : ι → submodule R M} (f : Π i, p i → β) :
  ∀ {i j} (x : p i) (h : i = j), f i x = f j ⟨x, h ▸ x.prop⟩
| i _ ⟨x, px⟩ rfl := rfl

Gabriel Ebner (Dec 06 2021 at 16:32):

The problem here is the f, not the assumptions.

Eric Wieser (Dec 06 2021 at 16:36):

If I replace f with something specific like pi.single, then @[congr] rejects the lemma:

@[congr]
lemma set_like.dep_congr {ι α P} [decidable_eq ι] [set_like P α]
  {p : ι → P} [Π (i : ι), has_zero ↥(p i)] :
  ∀ {i j} (x : p i) (h : i = j), pi.single i x = pi.single j ⟨x, h ▸ x.prop⟩
| i _ ⟨x, px⟩ rfl := rfl

Gabriel Ebner (Dec 06 2021 at 16:37):

Right, because it won't work in every instance (only when the codomain (p in your example) is non-dependent).

Eric Wieser (Dec 06 2021 at 16:39):

But the codomain of pi.single is dependent in this case?

Gabriel Ebner (Dec 06 2021 at 16:40):

Ah, now I see.

Eric Wieser (Dec 06 2021 at 16:43):

Is the problem that this only applies to specific invocations of pi.single?

Gabriel Ebner (Dec 06 2021 at 16:47):

Yes, that's what the check ensures. I think that check could be removed in core without breaking anything. The simplifier does the matching using unification anyhow afaict.

Eric Wieser (Dec 06 2021 at 16:49):

Conversely, should @[congr] be rejecting my original lemma?

Gabriel Ebner (Dec 06 2021 at 16:49):

If core supported this kind of congr lemma, then you should also allow rewriting in x, i.e., something like i = j → x.1 = y → pi.single i x = pi.single j ⟨y, ...⟩.

Gabriel Ebner (Dec 06 2021 at 16:50):

The set_like.dep_congr lemma is bad because 1) it does higher-order matching, and 2) doesn't allow rewriting in x, and 3) potentially applies to every subterm. There is a lot of stuff the simplifier doesn't like but doesn't reject either, which is fine, we've got linters for that.

Eric Wieser (Dec 06 2021 at 16:53):

x.1 = y isn't allowed in the congr lemma, annoyingly:

-- invalid congruence lemma, 'set_like.dep_congr' argument #13 is not a valid hypothesis, the
-- left-hand-side contains unresolved parameters
@[congr]
lemma set_like.dep_congr {ι α β P} [set_like P α]
  {p : ι → P} (f : Π i, p i → β) :
  ∀ {i j} (x : p i) (y : α) (h : i = j) (h1 : x.1 = y), f i x = f j ⟨y, h1 ▸ h ▸ x.prop⟩
| i _ ⟨x, px⟩ y rfl rfl := rfl

Eric Wieser (Dec 06 2021 at 16:53):

Nor any other attempt to state something like that I can think of, like x = ⟨y.1, h.symm ▸ y.prop⟩

-- invalid congruence lemma, 'set_like.dep_congr' argument #13 is not a valid hypothesis, the
-- right-hand-side must be of the form (m l_1 ... l_n) where m is parameter that was not
-- 'assigned/resolved' yet and l_i's are locals

Gabriel Ebner (Dec 06 2021 at 16:59):

This would be accepted (but it still has the f issue):

@[congr]
lemma set_like.dep_congr {ι α β P} [set_like P α]
  {p : ι → P} (f : Π i, p i → β) :
  ∀ {i j} (x : p i) (y) (h : i = j) (h1 : x = y), f i x = f j ⟨y, by cases x; subst h1; subst h; assumption⟩
| i _ ⟨x, px⟩ y rfl rfl := rfl

Eric Wieser (Dec 06 2021 at 17:01):

That has y : p i rather than y : p j

Eric Wieser (Dec 06 2021 at 17:01):

I should have mentioned that I tried that one; but with that one even simp, simp, simp, simp doesn't close the goal about pi.single...

Gabriel Ebner (Dec 06 2021 at 17:08):

At least simp; refl works.

Gabriel Ebner (Dec 06 2021 at 17:08):

@[congr]
lemma set_like.dep_congr {ι α β P} [set_like P α]
  {p : ι → P} (f : Π i, p i → β) :
  ∀ {i j} (x : p i) (y) (h : i = j) (h1 : x = y), f i x = f j ⟨y.1, by cases x; subst h1; subst h; assumption⟩
| i _ ⟨x, px⟩ y rfl rfl := rfl

Eric Wieser (Dec 06 2021 at 17:09):

It works for my original congr lemma too though

Eric Wieser (Dec 06 2021 at 17:10):

(also that last snippet differs only in coe vs .1; did you find that makes a difference?)

Eric Wieser (Dec 06 2021 at 17:11):

Oh wow it does, thanks!

Eric Wieser (Dec 06 2021 at 17:14):

Although I still need multiple simps in some cases:

example (p : ι → submodule R M) (x : M) (h : x = 0) :
  @pi.single ι (λ i, p i) _ _ (multiplicative.to_add 1) ⟨0, submodule.zero_mem _⟩ =
    pi.single 0 ⟨x, by simp [h, submodule.zero_mem _]⟩ :=
begin
  dsimp only,
  simp, -- leaves behind a `⟨0, _⟩.val` which isn't simp-normal!
  simp, -- gets rid of the above

  subst h,
end

Gabriel Ebner (Dec 06 2021 at 17:28):

If congr lemmas allowed complex arguments you could have a second congr lemma of the form pi.single i ⟨x, h⟩ = pi.single j ⟨y, h⟩ which would avoid the iota-reduction.