semiring with 0 ≠ 1

Stream: general

[Chris Hughes]

Is there a type class for a semiring with 0 ≠ 1?

[Chris Hughes]

I tried [semiring α] [zero_ne_one_class α] but then I ended up with two different definitions of one.

[Kenny Lau]

try to use old structure command and build a new class

[Kenny Lau]

the diamond death you just experienced

[Johan Commelin]

I tried [semiring α] [zero_ne_one_class α] but then I ended up with two different definitions of one.

Did you also end up with two different definitions of zero?

[Chris Hughes]

Yes.

[Chris Hughes]

Same question for ring.

[Chris Hughes]

Would it have been better to define zero_ne_one_class as

class zero_ne_one_class (α : Type*) [has_zero α] [has_one α] : Prop :=
(zero_ne_one : 0 ≠ 1)

[Mario Carneiro]

Yes. There is not much I can do about it

[Johan Commelin]

Well, we can define our own has_zero_ne_one, right?

[Johan Commelin]

In the way that Chris suggested

[Mario Carneiro]

Sure. I would ask the reason for the use though, it seems not so useful

[Chris Hughes]

I'm doing univariate polys, and I'm trying to prove degree_of (X : uv_polynomial α) = 1

[Mario Carneiro]

how is degree_of defined?

[Mario Carneiro]

and X

[Chris Hughes]

after unfolding it looks like this sup ((single 1 1).support) id = 1

[Chris Hughes]

unfolding single makes it become this sup (ite (1 = 0) ∅ (singleton 1)) id = 1

[Mario Carneiro]

is there decidable equality?

[Mario Carneiro]

or are you classical

[Chris Hughes]

Yes.

[Chris Hughes]

there is decidable equality

[Chris Hughes]

I could probably get around it by proving alternative lemmas like degree_of_monomial. Or just make 0 \ne 1 an argument to the theorem.

[Mario Carneiro]

I used a typeclass nonzero_ring in my metamath formalization of this one. Perhaps is_nonzero can be a typeclass depending on ring instead of has_zero and has_one?

[Mario Carneiro]

nonzero semiring seems like a bad idea though, it's not nearly as nice as it sounds since it is not cancellative

[Kevin Buzzard]

Chris, from a mathematical point of view I am not so sure that people care too much about semirings. However I know lean is different. All I'm saying is that if it's easier to work with rings than semirings then from the point of view of mathematical applications you'll be losing essentially nothing.

[Chris Hughes]

I have the same problem with rings.

[Chris Hughes]

I used a typeclass nonzero_ring in my metamath formalization of this one. Perhaps is_nonzero can be a typeclass depending on ring instead of has_zero and has_one?

Do you mean extending ring or with ring as an argument?

[Mario Carneiro]

nonzero_ring would extends ring, is_nonzero : Prop would have [ring A]