Zulip Chat Archive

Stream: new members

Topic: extracting to_fun


Sigma (Jan 19 2022 at 06:43):

When using lean ive run into this issue a lot where there are certain terms that become completely opaque. For example,

import ring_theory.power_series.basic

noncomputable theory

variables {M : Type*} [ring M]

instance coer : has_coe M (power_series M) := {
  coe := λ m, power_series.mk (λ n, ite (0 = n) m 0),
}

lemma coe_hom : ring_hom M (power_series M) := {
  to_fun := λ m, m,
  map_one' := sorry,
  map_mul' := sorry,
  map_zero' := sorry,
  map_add' := sorry,
}

lemma opaque : coe_hom.to_fun = (λ m : M, m) := begin
  sorry,
end

I cannot interact with the coe_hom.to_fun in any way, besides when i simp it becomes ⇑coe_hom. refl fails, simp doesn't do anything useful, unfold coe_hom.to_fun fails, what's happening and how do I get around it?

Huỳnh Trần Khanh (Jan 19 2022 at 07:06):

disclaimer: I'm not a mathematician. lemma coe_hom should be def coe_hom though because ring_hom isn't a Prop

once you fix this things should work as usual but don't quote me on this

Yaël Dillies (Jan 19 2022 at 08:05):

ext works

Yaël Dillies (Jan 19 2022 at 08:07):

But mostly coe_hom is a lemma when it should be a def. This works

def coe_hom : ring_hom M (power_series M) := {
  to_fun := λ m, m,
  map_one' := sorry,
  map_mul' := sorry,
  map_zero' := sorry,
  map_add' := sorry }

lemma opaque : coe_hom.to_fun = (λ m : M, m) := by { ext, refl }

but if you replace it with lemma coe_hom ... it fails, because that makes Lean throw away the definition.


Last updated: Dec 20 2023 at 11:08 UTC