Create instance `CommSemiring ℕ+`, err `expected structure`

Stream: mathlib4

[Bernardo Borges]

I was on my way to prove Bezout's Lemma for Positive Naturals (PNat):

-- Bézout's lemma: given x y : ℕ, gcd x y = x * a + y * b, where a = gcd_a x y and
-- b = gcd_b x y are computed by the extended Euclidean algorithm

example
 (m n : ℕ+)
 (u : IsCoprime m n)
 : ∃x y : ℤ, m*x + n*y = 1
 := sorry

But then I get:

failed to synthesize
  CommSemiring ℕ+
Additional diagnostic information may be available using the `set_option diagnostics true` command.

Now, trying to show that this holds, I opened this block from the implementation for Nat:

namespace PNat

instance instCommSemiring : CommSemiring (ℕ+) where
  __ := sorry -- instSemiring
  __ := sorry -- instCommMonoid

end PNat

But before starting I only get the error:
expected structure
What does this mean?
Is is feasible to create this instance somehow?

[Eric Wieser]

It means that sorry is not a structure

[Eric Wieser]

The __ notation only works if you already know what type it is going to be

[Eric Wieser]

So __ : Semiring ℕ+ := sorry would avoid the error...

[Eric Wieser]

... but you're going to be stuck anyway, because there is no 0 : ℕ+

[Eric Wieser]

I suspect the right answer here is to weaken docs#IsCoprime to require [AddSemigroup R] [Monoid R] or something

[Bernardo Borges]

Ok, but then we could argue that another definition of being coprime could be created for PNat without the need of CommSemiring right

[Eric Wieser]

Right, but usually it's better to generalize an existing definition to work for more situations than just duplicate the definition

[Bernardo Borges]

Eric Wieser said:

I suspect the right answer here is to weaken docs#IsCoprime to require [AddSemigroup R] [Monoid R] or something

Do you have any examples of such process of weakening that I can take a look at? It'd help a lot!

[Eric Wieser]

I talked a little bit about this last week, the slides after that have some examples

[Bernardo Borges]

FYI, this is the proof I'm trying to formalize:
image.png

Taken from the book Type Theory and Formal Proof

[Bernardo Borges]

Eric Wieser said:

I talked a little bit about this last week, the slides after that have some examples

Oh wow, fancy slides :star_struck:

[Kevin Buzzard]

@Bernardo Borges just work in integers and add the hypothesis that they're positive. Surely you believe that if m and n are positive integers then the statements "m and n are coprime, when regarded as positive integers" and "m and n are coprime, when regarded as integers" are mathematically equivalent. But mathlib has a stupid definition of coprime in the sense that it make sense in far more generality than is mathematically meaningful. For example the natural numbers 2 and 3 are not coprime when regarded as natural numbers, as far as mathlib is concerned (go to the source code for docs#IsCoprime and see why). So either avoid IsCoprime or avoid natural numbers. If you use both then you will get pathologies.

[Andrew Yang]

import Mathlib.RingTheory.Coprime.Basic

example {a b : ℕ} : IsCoprime a b ↔ a = 1 ∨ b = 1 := by
  refine ⟨fun ⟨x, y, e⟩ ↦ ?_, ?_⟩
  · cases' x with x; · aesop
    cases' y with y; · aesop
    cases' a with a; · aesop
    cases' b with b; · aesop
    ring_nf at e
    simp only [add_right_eq_self, Nat.add_eq_zero,
      one_ne_zero, mul_eq_zero, false_and, add_assoc, ← one_add_one_eq_two] at e
  · rintro (rfl|rfl)
    exacts [⟨1, 0, by simp⟩, ⟨0, 1, by simp⟩]

[Kevin Buzzard]

[told you]

[Eric Wieser]

The above should be in Mathlib and @[simp]

[Eric Wieser]

isCoprime_one_left and isCoprime_one_right make the second branch idealogically shorter

[Kim Morrison]

Eric Wieser said:

The above should be in Mathlib and @[simp]

So people discover more quickly that IsCoprime and Nat combine badly?

[Eric Wieser]

Yes, exactly

[Eric Wieser]

But also, the RHS seems obviously simpler than the LHS to me, which seems like the metric that matters.

[Johan Commelin]

swap(LHS,RHS) in :up: ?

[Junyan Xu]

Kevin Buzzard said:

For example the natural numbers 2 and 3 are not coprime when regarded as natural numbers, as far as mathlib is concerned (go to the source code for docs#IsCoprime and see why).

Fun fact: 2 and 3 generate the unique maximal ideal of ℕ, and you can show ℕ is a LocalRing according to mathlib.

[Kevin Buzzard]

Funnily enough I was just concluding that in another thread...

[Junyan Xu]

I first mentioned this here. I didn't realize so many stuff (including structure sheaf) generalizes to commutative semirings. I have a question about noncommutative local semirings here if anyone is interested :)

[Eric Wieser]

Eric Wieser said:

The above should be in Mathlib and @[simp]

PR'd as #20569