ACC/DCC

Stream: maths

[Aaron Anderson]

I'm trying to prove that being a UFD is equivalent to (irreducible iff prime) and the ascending chain condition on principal ideals, or equivalently, descending chain condition/well-foundedness of < on associates.

[Aaron Anderson]

I notice that there aren't any typeclasses for ACC or DCC, so I have to talk about well-foundedness of < or > or (a | b and not b | a) a lot, and these ad-hoc descriptions are getting a little messy.

[Aaron Anderson]

Is there a good reason not to define ACC and DCC as classes (or just predicates) for pre-/partial orders, or has it just not been done because it wasn't needed?

[Johan Commelin]

I don't know why they aren't there yet, but I think it makes sense to add them.

[Aaron Anderson]

One possible reason is that there's already a typeclass related to well-foundedness called acc

[Aaron Anderson]

But I think it stands for accessible, and isn't just a property of an order/relation

[Aaron Anderson]

it still makes it awkward to write an abbreviation called ACC...