Decidable PythagoreanTriple

Stream: mathlib4

[Markus Schmaus]

I noticed that in Mathlib PythagoreanTriple isn't an instance of Decidable, even though it trivially is decidable.

I was able proof this like so:

import Mathlib

instance : Decidable (PythagoreanTriple x y z) := by
  unfold PythagoreanTriple
  infer_instance

#eval PythagoreanTriple  3 4 5

I have two questions:

• Is this a good way to make such a Prop an instance of Decidable?
• Should I create a PR for code like this, or should I just keep it in my own code base?

[Eric Wieser]

That instance looks totally reasonable to me

[Yaël Dillies]

Yes and yes. That's a reasonable addition to mathlib

[Eric Wieser]

You could golf it slightly by using docs#Int.instDecidableEqInt directly

[Scott Morrison]

inferInstanceAs is useful for these sorts of instances. Doing it this way is quite readable as the the reader can see quickly why it is decidable. The instance name is needlessly obscure.

[Markus Schmaus]

@Scott Morrison Is this what you mean?

import Mathlib
instance : Decidable (PythagoreanTriple x y z) := inferInstanceAs (Decidable (x * x + y * y = z * z))

[Scott Morrison]

Something like that. Is is actually defined using x * x rather than x^2? Who knew? :woman_shrugging:

[Eric Wieser]

I'd recommend

instance : Decidable (PythagoreanTriple x y z) := inferInstanceAs <| Decidable (_ = _)

as that tells the reader all they need to know: it's decidable because it's an equality

[Eric Rodriguez]

Scott Morrison said:

Something like that. Is is actually defined using x * x rather than x^2? Who knew? :woman_shrugging:

A lot of things do that to minimise typeclass arguments, e.g. Even is x+x. Oddly enough (hah) Odd is (iirc) 2 * x + 1

[Eric Rodriguez]

It's a bit of an odd practice

[Patrick Massot]

Eric Rodriguez said:

A lot of things do that to minimise typeclass arguments, e.g. Even is x+x. Oddly enough (hah) Odd is (iirc) 2 * x + 1

Is there any actual use of this definition of Even? It is rather annoying when teaching.

[Eric Wieser]

I guess it lets you talk about "even" elements of a free additive monoid

[Eric Wieser]

It probably also makes the to_additive stuff with IsSquare slightly easier than using smul / pow

[Eric Rodriguez]

things like docs#Even.tsub

[Eric Rodriguez]

because we don't have that many mixins for the CanonicallyOrderedNonsense

[Eric Rodriguez]

as it points out, we can't have Odd.tsub because of this:

-- `Odd.tsub` requires `CanonicallyLinearOrderedSemiring`, which we don't have

[Eric Rodriguez]

(although I'm not sure how that would actually hold as of course 1 - 3 = 1 - 4 = 0, so not sure what the statement would be!)

[Ruben Van de Velde]

Would it say Odd a → Odd b → Even (a - b)?

[Ruben Van de Velde]

That seems vacuously true in the bad cases

[Yaël Dillies]

I was considering adding it, but I would have needed a typeclass that only Nat would satisfy and we already have the lemma on Nat

[Yaël Dillies]

So I was thinking we could just rename Nat.Odd.sub to Odd.tsub and then everybody is happy.

[Eric Rodriguez]

I mean, I'm personally happy to have Odd just required Add and One, but I fear that those that teach will have headaches

[Damiano Testa]

I was probably the one responsible for defining Even as a doubled sum and it was essentially what Eric said: I wanted to unify Even and Square using to_additive. I had not thought of the teaching implications of this design choice. Let me find the relevant thread!

[Damiano Testa]

The mathlib3 PR and the relevant Zulip thread.

[Martin Dvořák]

Eric Rodriguez said:

because we don't have that many mixins for the CanonicallyOrderedNonsense

What are mixins?

[Alex J. Best]

Things like docs#NoTopOrder (typeclasses that take others as parameters), they don't live "in" the heirachy or all blah blahs, so that you can add them as side assumptions, and mix them together