Using mem_carrier ?

Stream: maths

[Nicolás Ojeda Bär]

I'm getting the following error when trying to do rw ← submonoid.mem_carrier to involve the carrier of each of the two terms in the goal. I don't understand the error because the goal seems to have the sought expression. Any ideas?

rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_3 ∈ ?m_4
state:
R : Type u,
_inst_1 : semiring R,
M₁ : Type v,
_inst_4 : add_comm_monoid M₁,
_inst_5 : module R M₁,
M₂ : Type v,
_inst_6 : add_comm_monoid M₂,
_inst_7 : module R M₂,
f : M₁ →ₗ[R] M₂,
p q : submodule R M₁,
h : p ≤ q,
x : M₂
⊢ x ∈ {carrier := ⇑f '' p.carrier, zero_mem' := _, add_mem' := _, smul_mem' := _} →
  x ∈ {carrier := ⇑f '' q.carrier, zero_mem' := _, add_mem' := _, smul_mem' := _}

[Heather Macbeth]

Welcome, @Nicolás Ojeda Bär. Can you please provide a full example with imports (see our page #mwe)?

[Nicolás Ojeda Bär]

Yes, see below (I know the goal can be solved using simp, but I'm trying to figure out why the rw fails):

import group_theory.submonoid

universes u
variables (M : Type u) [add_comm_monoid M]
variable (p : add_submonoid M)

example (x : M) : x ∈ p -> x ∈ p.carrier :=
begin
  rw ← submonoid.mem_carrier
/-
rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_3 ∈ ?m_4
state:
M : Type u,
_inst_1 : add_comm_monoid M,
p : add_submonoid M,
x : M
⊢ x ∈ p → x ∈ p.carrier
-/
end

[Heather Macbeth]

You need to use docs#add_submonoid.mem_carrier, the additive version.

[Heather Macbeth]

(Nice #mwe by the way!)

[Nicolás Ojeda Bär]

Ah, right! Thanks (still trying to wrap my head around all the type classes/coercions)

[Nicolás Ojeda Bär]

Sorry, but coming back to this: I get the same error when trying the following analog with submodule R M in place of add_submonoid M; any ideas?

import algebra.module

universes u v
variables (R : Type u) [semiring R]
variables (M : Type v) [add_comm_monoid M] [module R M]
variable (p : submodule R M)

example (x : M) : x ∈ p -> x ∈ p.carrier :=
begin
  rw ← submodule.mem_carrier
/-
rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_2 ∈ ↑?m_7
state:
R : Type u,
_inst_1 : semiring R,
M : Type v,
_inst_2 : add_comm_monoid M,
_inst_3 : module R M,
p : submodule R M,
x : M
⊢ x ∈ p → x ∈ p.carrier
-/
end

[Heather Macbeth]

In this case you need to rewrite with another lemma first:

  rw ← set_like.mem_coe,
  rw ← submodule.mem_carrier,

This is something about the distinction between the submodule and the underlying set. I don't know much about set_like, maybe someone else will jump in with a more principled explanation.

[Nicolás Ojeda Bär]

Ah right, thanks!

[Kyle Miller]

@Nicolás Ojeda Bär A useful tactic to give you a hint when simp works is squeeeze_simp. With your first MWE it suggests simp only [imp_self, add_submonoid.mem_carrier] and with your second simp only [imp_self, set_like.mem_coe, submodule.mem_carrier]. These coincide with @Heather Macbeth's suggestion, except for the additional imp_self.

[Kyle Miller]

(I rely on squeeze_simp quite a lot.) set_like is a @Eric Wieser creation to unify certain lemmas and constructions for different algebraic subobjects. He can explain more, but I understand that the idea is that things like subgroups, submonoids, submodules, etc., are also subsets of the corresponding algebraic object, and, being subsets, these get standard coercions as subtypes. It used to be that there was a separate submodule.mem_coe (along with duplicates for each subobject) rather than the single set_like.mem_coe.

[Nicolás Ojeda Bär]

Thanks for the explanation, it is useful!

[Scott Morrison]

There's also simp? as an alternative to squeeze_simp. Both try to achieve the same thing (print a list of the lemmas simp siis using), and neither are perfect. I mostly use simp? because it's shorter. :-)

[Kyle Miller]

@Scott Morrison In these examples, for some reason simp? suggested simp only [imp_self], which fails to simplify. What's roughly the difference between simp? and squeeze_simp?

[Kyle Miller]

(They're also both proved by intro h, exact h (or exact id), which isn't so far off from imp_self.)

[Scott Morrison]

squeeze_simp, which came first, analyses the proof term simp generates and tries to reconstruct the relevant list. simp? instead uses some hooks into the C++ code to watch what simp is doing. Both have known problems, that I doubt anyone wants to address before Lean4 make both obsolete, unfortunately. If one doesn't work, try the other. :-)

[Eric Wieser]

simp? is usually much faster, but squeeze_simp is usually more reliable