Zulip Chat Archive

Stream: mathlib4

Topic: ofReal_two

Chris Hughes (Mar 10 2023 at 16:34):

What's the canonical proof of ((2 : Real) : Complex) = 2 these days?

Kevin Buzzard (Mar 10 2023 at 17:20):

Does norm_cast do it?

Chris Hughes (Mar 10 2023 at 18:21):

I don't think so, but Data.Complex.Basic has only just been ported, so maybe some attribute is missing.

Gabriel Ebner (Mar 10 2023 at 18:23):

It's certainly something that norm_cast should be able to do.

Gabriel Ebner (Mar 10 2023 at 18:23):

norm_cast needs a different set up for numerals in Lean 4 than it did in Lean 3 though.

Gabriel Ebner (Mar 10 2023 at 18:24):

In Lean 3 you needed cast lemmas for 0, 1, bit0, and bit1.

Gabriel Ebner (Mar 10 2023 at 18:26):

Now you need lemmas for 0, 1, and n (with [Nat.AtLeastTwo n] like this: https://github.com/leanprover-community/mathlib4/blob/5d9a516c7a8c129bd7e0d3fa5e06701515d5ce12/Mathlib/Data/Real/NNReal.lean#L359-L361).

Gabriel Ebner (Mar 10 2023 at 18:27):

Not much thought went into the API, it might be a good idea to introduce a LawfulOfNat class so that you get a lemma that works for all numerals.

Yury G. Kudryashov (Mar 10 2023 at 19:07):

BTW, will

instance [NatCast α] [Zero α] [One α] (n : Nat) : OfNat α n where
  ofNat
    | 0 => 0
    | 1 => 1
    | n => Nat.cast n

cause troubles?

Yury G. Kudryashov (Mar 10 2023 at 19:08):

If not, then we can get rid of AtLeastTwo and use this instance + lemma saying that Nat.Cast n = OfNat.ofNat n.

Yury G. Kudryashov (Mar 10 2023 at 19:09):

@Chris Hughes How do we define natCast for Complex? If it is defined as ofReal (Nat.cast n), then the proof is rfl.

Chris Hughes (Mar 10 2023 at 19:13):

The proof is rfl, but that doesn't mean that simp will prove it.

Chris Hughes (Mar 10 2023 at 19:17):

Also, linarith failed a couple of times because of this

Yury G. Kudryashov (Mar 10 2023 at 19:21):

If you want simp to prove it, then you need a lemma similar to ENNReal.coe_ofNat

Yury G. Kudryashov (Mar 10 2023 at 19:21):

It seems that docs4 still knows nothing about ENNReals.

Gabriel Ebner (Mar 10 2023 at 19:21):

@Yury G. Kudryashov That might work, although I fear it will reduce to Nat.cast (...).succ.succ.

Eric Wieser (Mar 10 2023 at 19:23):

Yury G. Kudryashov said:

BTW, will

instance [NatCast α] [Zero α] [One α] (n : Nat) : OfNat α n where
  ofNat
    | 0 => 0
    | 1 => 1
    | n => Nat.cast n

cause troubles?

docs4#OfNat.ofNat doesn't take an n argument, does it?

Yury G. Kudryashov (Mar 10 2023 at 19:28):

Sorry, I meant

instance [NatCast α] [Zero α] [One α] : (n : Nat) -> OfNat α n
    | 0 => ⟨0⟩
    | 1 => ⟨1⟩
    | n => ⟨Nat.cast n⟩

Yury G. Kudryashov (Mar 10 2023 at 19:29):

BTW, it would be nice to have a command or an attribute that adds ofNat lemma copy of a Nat.cast lemma.

Yury G. Kudryashov (Mar 10 2023 at 19:31):

E.g., it should generate ENNReal.coe_ofNat from ENNReal.coe_nat.

Last updated: Dec 20 2023 at 11:08 UTC