Support τ (tau) as the circle constant in fork of Mathlib?

Stream: new members

[Xuanmizhen]

Hi, everyone! I'm new here. I'm considering supporting τ = 2π = 6.28318... in Mathlib.
As you may know, τ, defined to be the ratio of a circle’s circumference (length) to its radius, has been advocated for 15 years to be the "true circle constant", according to https://www.tauday.com/tau-manifesto. However, it seems that τ is still not supported in Mathlib.
To support τ, we'll introduce Real.tau, and have Mathlib.Data.Real.Tau.Irrational to prove that τ is irrational, etc.
I still have little knowledge about Lean, and I consider contributing τ as a chance to learn more about the Mathlib. Is there someone interested in this topic? Any suggestions? Glad to hear from you!

[Aaron Liu]

I don't think we need this

[Aaron Liu]

why can't we just use 2 * π everywhere

[Aaron Liu]

for the same reason we do exp 1 instead of defining Real.e

[Xuanmizhen]

Because, π is 1/2 τ, not that τ is 2 * π

[Xuanmizhen]

τists will find it comfortable to write without π.

[Aaron Liu]

well in mathlib π is defined as "twice an arbitrary zero of Real.cos between 1 and 2, which exists by the intermediate value theorem"

[Xuanmizhen]

That's interesting.

[Xuanmizhen]

Then how is Real.cos defined, if I may know?

[Aaron Liu]

anything can be defined in multiple ways and it doesn't really matter which one you pick as long as it's easy to work with and you can prove all the properties

[Xuanmizhen]

My long-term experience has told me that it is always more meaningful and more concise to write in τ, however.

[Aaron Liu]

Xuanmizhen said:

Then how is Real.cos defined, if I may know?

Real.cos is "the real part of Complex.cos", and Complex.cos is defined as z ↦ (exp (z * I) + exp (-z * I)) / 2, and Complex.exp is defined by its taylor series at zero

[Xuanmizhen]

Oh, I don't know Complex has cos before.

[Xuanmizhen]

I will learn what you told me further in the future. Anyway, I still believe my intuition, and one day I will write more elegant definitions with tau in the Mathlib, if I could.

[Xuanmizhen]

Do you know tau before?

[Aaron Liu]

yes

[Xuanmizhen]

Great.

[Xuanmizhen]

I've created an issue on GitHub. https://github.com/leanprover-community/mathlib4/issues/29175

[Patrick Massot]

I'm afraid this won't have any effect. I think you'll be a lot less frustrated if you focus on more productive quests.

[Kevin Buzzard]

Every definition comes with a cost and for the tau proposal, the cost outweighs the benefits. The way to do this if you want to write tau files is just to make tau an abbreviation for 2pi in your local files; this will work fine for everyone. In formalisation the more ways you have to say something the more lemmas you need to relate them and the more inefficient things get. In formalisation we need to be ergonomic.

[Xuanmizhen]

Patrick Massot said:

I'm afraid this won't have any effect. I think you'll be a lot less frustrated if you focus on more productive quests.

I understand. People dealing with τ in Mathlib have to have passion and a lot of spare time, and there's a great probability that I have to do it on my own, but I'll still do it.

[Xuanmizhen]

Kevin Buzzard said:

Every definition comes with a cost and for the tau proposal, the cost outweighs the benefits. The way to do this if you want to write tau files is just to make tau an abbreviation for 2pi in your local files; this will work fine for everyone. In formalisation the more ways you have to say something the more lemmas you need to relate them and the more inefficient things get. In formalisation we need to be ergonomic.

That's a good point to think about! However, I'm afraid that you may underestimate the value of formalising τ completely. We can have a more deeper understanding of the difference between τ and π, and we can see which of them, or both, have their unique meanings.
I don't know when you say ergonomic, whether you are referring to human labor, or you are referring to the cost when compiling. As for the former, I think there would be τists finding it valuable to work with. As for the latter, we may define some more abstract and common behaviors for both τ and π, so they can be reused.

[Robin Arnez]

Well the point is that there are really only three ways this could go:

1. Use τ as the normal form. This is basically impossible due to backwards compatibility.
2. Use π as the normal form and introduce τ merely as an abbreviation that gets simped away immediately (@[simp] abbrev Real.tau := 2 * Real.pi). This is possible but feels a bit pointless.
3. Have both τ and π as normal forms. This only really introduces more complexity, e.g. π + τ = 3 * π is slightly harder to prove than π + 2 * π = 3 * π which already works well with many tactics.

[Xuanmizhen]

Yes. But well, no one would insert both π and τ in a same file.

[Johan Commelin]

This will definitely lead to a proliferation of definitions.

https://www.youtube.com/watch?v=1qpVdwizdvI

Next thing we know, someone will propose $\pi/180$, and call it ${}^\circ$ :see_no_evil:

[Xuanmizhen]

I'm afraid that the author of the video hasn't got the real thing of The Tau Manifesto.

[Xuanmizhen]

In fact, there's a constant called λ in The Tau Manifesto, defined to be τ / 4. We can say that λ has its meaning.

[Damiano Testa]

It is starting to dawn on me that not all of these discussions are ironic...

[Kevin Buzzard]

@Xuanmizhen this is formalization, not mathematics. Formalization has different rules to mathematics. In mathematics it's fine to have $\pi$ and $\tau$ and $\lambda$ if you want them. But in formalization it is not, because one needs what is called a "simp normal form". If we allow all three of these symbols to be "primitive" then this is a massive problem for formalization, because then the number of lemmas we need goes up by a factor of three, causing a huge amout of unnecessary overhead. So we have to decide the precisely one of these is "primitive" and already we decided that the answer is that the primitive one is $\pi$. You might not like that decision, but that decision is not going to change, because changing it would be a gigantic amount of work, for no benefit as far as formalization is concerned; it would just be "churn". So the way to introduce $\tau$ would be to define it to be $2\pi$ and then immediately teach the system to replace $\tau$ by $2\pi$ everywhere (i.e. make $\tau$ not "primitive"). This is completely pointless as far as mathlib is concerned because we gain nothing. It is true that there are some lemmas in mathlib which mention $2\pi$ which then become "simpler" with $\tau$, but from the point of view of formalization it is still a bad idea to make this change, because as I already explained it is more important for formalization to have one "normal form" for everything than it is to have lemmas which are three characters shorter. This is why mathlib is not interested in having $\tau$. Let me stress that rhis is nothing to do with the Tau manifesto debate -- this is a pragmatic decision based on how the formalization of mathematics is done. The fact that some lemmas would be slightly shorter with $\tau$, and some would be slightly longer, and that maybe it is the case that more would be shorter than longer (or maybe it is not the case) is irrelevant; what is relevant is that we cannot support 3 times as many lemmas about fundamental terms in this situation because it is too much pain for too little gain, and we already put too much effort into making $\pi$ the fundamental term.

In short: arguments from formalization override arguments from the Tau manifesto, because mathlib is a formalization project.

There is nothing stopping you having $\tau$ in your own project.

[Xuanmizhen]

@Kevin Buzzard Thanks for telling me about these things. I’ll fork Mathlib and do it on my own, and τists may be interested in it. Now I understand that the standard Mathlib has good reasons not introducing τ, so temporarily I won’t consider contributing τ to Mathlib again. When I get my stuff done, I’ll show the link to my fork here, so everyone can see it. In my project, there would be no π at all.

[Eric Wieser]

For you own project, you can just add:

import Mathlib

open scoped Real in
scoped[Real] notation "τ" => 2 * π

there is no need to fork mathlib

[Xuanmizhen]

No. I'll define τ directly, and prove properties about it.

[Xuanmizhen]

I'll delete pi in my fork.

[Kevin Buzzard]

This (deleting pi) will be a huge undertaking! Good luck!

[Kevin Buzzard]

One thing you will have to decide is that for all the lemmas which mention $\pi$ but not $2\pi$, whether to represent this as tau / 2 or tau * 0.5 or tau * 2^{-1} or 0.5 * tau or ... . Formally, all of these things are different.

[Xuanmizhen]

Okay. Thanks for telling me that.

[Xuanmizhen]

If anyone finds that someone has implemented τ in their Mathlib fork, please let me know, so I don't need to do it again.

[Damiano Testa]

There may be only about 1589 declarations that mention docs#Real.pi.

These are the first 100 (in alphabetical order)

docs#AddChar.zmod_injective
docs#AddChar.zmod_intCast
docs#AddCircle.continuous_toCircle
docs#AddCircle.homeomorphCircle
docs#AddCircle.homeomorphCircle'
docs#AddCircle.homeomorphCircle'_apply
docs#AddCircle.homeomorphCircle'_apply_mk
docs#AddCircle.homeomorphCircle'_symm_apply
docs#AddCircle.homeomorphCircle_apply
docs#AddCircle.injective_toCircle
docs#AddCircle.scaled_exp_map_periodic
docs#AddCircle.toCircle
docs#AddCircle.toCircle_add
docs#AddCircle.toCircle_apply_mk
docs#AddCircle.toCircle_zero
docs#Affine.Simplex.AcuteAngled
docs#Affine.Simplex.Equilateral.acuteAngled
docs#Affine.Simplex.Equilateral.angle_eq_pi_div_three
docs#Affine.Simplex.acuteAngled_reindex_iff
docs#Affine.Triangle.acuteAngled_iff_angle_lt
docs#Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq
docs#Affine.Triangle.circumsphere_eq_of_dist_of_oangle
docs#Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter
docs#AffineSubspace.SSameSide.oangle_sign_eq
docs#Circle.argEquiv
docs#Circle.argEquiv_apply_coe
docs#Circle.argEquiv_symm_apply
docs#Circle.argPartialEquiv
docs#Circle.argPartialEquiv_target
docs#Circle.arg_exp
docs#Circle.exp_add_two_pi
docs#Circle.exp_eq_exp
docs#Circle.exp_eq_one
docs#Circle.exp_inj
docs#Circle.exp_int_mul_two_pi
docs#Circle.exp_pi_ne_one
docs#Circle.exp_sub_two_pi
docs#Circle.exp_two_pi
docs#Circle.exp_two_pi_mul_int
docs#Circle.invOn_arg_exp
docs#Circle.periodic_exp
docs#Circle.surjOn_exp_neg_pi_pi
docs#CircleIntegrable
docs#CircleIntegrable.abs
docs#CircleIntegrable.add
docs#CircleIntegrable.congr_codiscreteWithin
docs#CircleIntegrable.const_smul
docs#CircleIntegrable.neg
docs#CircleIntegrable.out
docs#CircleIntegrable.sum
docs#Collinear.oangle_sign_of_sameRay_vsub
docs#Collinear.two_zsmul_oangle_eq_left
docs#Complex.Gamma_mul_Gamma_add_half
docs#Complex.Gamma_mul_Gamma_one_sub
docs#Complex.Gamma_ne_zero
docs#Complex.Gamma_one_half_eq
docs#Complex.Gammaℂ
docs#Complex.Gammaℂ_add_one
docs#Complex.Gammaℂ_def
docs#Complex.Gammaℂ_one
docs#Complex.Gammaℝ
docs#Complex.Gammaℝ_add_two
docs#Complex.Gammaℝ_def
docs#Complex.Gammaℝ_div_Gammaℝ_one_sub
docs#Complex.Gammaℝ_eq_zero_iff
docs#Complex.Gammaℝ_mul_Gammaℝ_add_one
docs#Complex.Gammaℝ_ne_zero_of_re_pos
docs#Complex.Gammaℝ_one
docs#Complex.Gammaℝ_one_sub_mul_Gammaℝ_one_add
docs#Complex.Gammaℝ_residue_zero
docs#Complex.HadamardThreeLines.norm_mul_invInterpStrip_le_one_of_mem_verticalClosedStrip
docs#Complex.abs_arg_inv
docs#Complex.abs_arg_le_pi
docs#Complex.abs_arg_le_pi_div_two_iff
docs#Complex.abs_arg_lt_pi_div_two_iff
docs#Complex.abs_circleTransformBoundingFunction_le
docs#Complex.abs_eq_one_iff'
docs#Complex.abs_exp_mul_exp_add_exp_neg_le_of_abs_im_le
docs#Complex.angle_div_left_eq_angle_mul_right
docs#Complex.angle_exp_exp
docs#Complex.angle_exp_one
docs#Complex.angle_le_mul_norm_sub
docs#Complex.angle_mul_left
docs#Complex.arctan_tan
docs#Complex.arg
docs#Complex.arg_I
docs#Complex.arg_coe_angle_toReal_eq_arg
docs#Complex.arg_conj
docs#Complex.arg_conj_coe_angle
docs#Complex.arg_cos_add_sin_mul_I
docs#Complex.arg_cos_add_sin_mul_I_eq_toIocMod
docs#Complex.arg_cos_add_sin_mul_I_sub
docs#Complex.arg_eq_neg_pi_div_two_iff
docs#Complex.arg_eq_nhds_of_re_neg_of_im_neg
docs#Complex.arg_eq_nhds_of_re_neg_of_im_pos
docs#Complex.arg_eq_pi_div_two_iff
docs#Complex.arg_eq_pi_iff
docs#Complex.arg_eq_pi_iff_lt_zero
docs#Complex.arg_exp_mul_I
docs#Complex.arg_inv

[Xuanmizhen]

Pretty good.

[Eric Wieser]

https://loogle.lean-lang.org/?q=Real.pi finds many fewer

[Damiano Testa]

Does that also look inside proofs?

[Xuanmizhen]

Are there other things I need to take care of when creating τ in my version of Mathlib?

[Damiano Testa]

Damiano Testa said:

Does that also look inside proofs?

Indeed, docs#AddChar.zmod_injective does not appear if you search for both, but AddChar.zmod_injective uses Real.pi in its proof.

[Xuanmizhen]

Currently, I've got a fork at https://github.com/Xuanmizhen/mathlib4, but I haven't done anything.

[Xuanmizhen]

When I delete π in my fork, I'll see what depend on it.

[Ruben Van de Velde]

Have fun!

[Xuanmizhen]

Is it possible to define tau as the period of sin or cos?

[Notification Bot]

This topic was moved here from #mathlib4 > Support τ (tau) as the circle constant in Mathlib? by Johan Commelin.

[Johan Commelin]

I've moved this out of the #mathlib4 channel, since this is now a discussion about work in a personal fork.

[Johan Commelin]

Xuanmizhen said:

Is it possible to define tau as the period of sin or cos?

Certainly!

[Johan Commelin]

There is probably a lemma in mathlib, showing that they are periodic. The proof might use pi though.

[Xuanmizhen]

OK. Then I think maybe I can prove these lemmas with λ, which is τ / 4. I'll define λ first, prove the period, and define τ.

[Xuanmizhen]

Then prove τ = 4 * λ and λ = (1 / 4) * τ

[Eric Wieser]

(deleted)