Zulip Chat Archive

Stream: general

Topic: enat pain

Johan Commelin (Sep 03 2021 at 19:02):

Is this a known bug?

example (n : ℕ) :
  @eq enat
    (@coe nat enat (@coe_to_lift nat enat (@nat.cast_coe enat (@add_zero_class.to_has_zero enat
      (@add_monoid.to_add_zero_class enat (@add_comm_monoid.to_add_monoid enat enat.add_comm_monoid)))
        enat.has_one (@add_zero_class.to_has_add enat (@add_monoid.to_add_zero_class enat
          (@add_comm_monoid.to_add_monoid enat enat.add_comm_monoid))))) n)
    (@coe nat enat (@coe_to_lift nat enat (@coe_base nat enat enat.has_coe)) n) := rfl -- fails

Johan Commelin (Sep 03 2021 at 19:46):

lemma enat.coe_eq_coe (n : ℕ) :
  @eq enat
    (@coe nat enat (@coe_to_lift nat enat (@nat.cast_coe enat (@add_zero_class.to_has_zero enat
      (@add_monoid.to_add_zero_class enat (@add_comm_monoid.to_add_monoid enat enat.add_comm_monoid)))
        enat.has_one (@add_zero_class.to_has_add enat (@add_monoid.to_add_zero_class enat
          (@add_comm_monoid.to_add_monoid enat enat.add_comm_monoid))))) n)
    (@coe nat enat (@coe_to_lift nat enat (@coe_base nat enat enat.has_coe)) n) :=
begin
  induction n with n ih, { refl },
  simp only [nat.succ_eq_add_one, enat.coe_one, enat.coe_add, nat.cast_add, nat.cast_one, ih],
end

Johan Commelin (Sep 04 2021 at 06:39):

Can some coercion expert please explain how to fix this issue?

Johan Commelin (Sep 04 2021 at 06:56):

I need this for #8994

Yaël Dillies (Sep 04 2021 at 07:35):

I'm not an expert, but I figured out it was because coe_base isn't defeq to nat.cast

Yaël Dillies (Sep 04 2021 at 07:37):

coe_base uses part.some (because enat is part ℕ...) and nat.cast uses the semiring structure.

Yaël Dillies (Sep 04 2021 at 07:39):

I'm of the opinion that the current enat is a pile of pain. I would redefine it as with_top ℕ, because that's what it is. The reason to have it as part ℕ is to have a computable enat.find

Kevin Buzzard (Sep 04 2021 at 07:40):

I would imagine you can have the same diamond with with_top nat

Yaël Dillies (Sep 04 2021 at 07:41):

Yeah, but this time we already thought about it, as many more things are with_top R than part R

Yaël Dillies (Sep 04 2021 at 07:43):

Long answer short: burn coe_base :smiling_imp:

Johan Commelin (Sep 04 2021 at 07:56):

It is important the the coercion is computable? I would think that we can just have the computable version as a plain function, ready to use if someone needs it, and let the coe be whatever is automatically infered.

Yaël Dillies (Sep 04 2021 at 07:57):

Yes, exactly what I'm thinking. But maybe computabilists want to have their say.

Yaël Dillies (Sep 04 2021 at 07:58):

Note that:

It's already a plain function: part.some (maybe there's even an enat specialization?)
Many lemmas will need changing

Johan Commelin (Sep 04 2021 at 12:53):

I will try to fix this

Johan Commelin (Sep 04 2021 at 15:12):

enat.lean compiles again. Let's see about the rest of mathlib.

Yakov Pechersky (Sep 05 2021 at 01:45):

src#enat.has_coe, src#nat.cast_coe

Johan Commelin (Sep 06 2021 at 05:54):

#9023 refactors the coercion.

Johan Commelin (Sep 06 2021 at 12:39):

From the PR description:

The coercion from nat to enat was defined to be enat.some. But another
coercion could be inferred from the additive structure on enat, leading to
confusing goals of the form
↑n = ↑n where the two sides were not defeq.

We now make the coercion inferred from the additive structure the default,
even though it is not computable.

A dedicated function enat.some is introduced, to be used whenever
computability is important.

CI is happy with the PR.