[ add ] BooleanRing plus Properties

[jamesmckinna]

Fixes #2704
Outstanding issue:

• should the base structure be IsRing or IsRingWithoutOne?

TODO:

• relationships between BooleanRing and BooleanAlgebra (which does require a 1#, IIUC)

[JacquesCarette]

Hmm, if the base is Ring, then it would make sense if there were properties of 1 proved here too. If 1 is not really involved (except that, well, it is in a BooleanRing), maybe RingWithoutOne is fine.

I guess it would be really weird for a "boolean ring" to have only false but not true. And then clearly - is not not!

Probably this means that the main file needs more comments.

[Taneb]

A thought on this:

If * is idempotent, then 1 = -1 * -1 = -1, so -x = -1 * x = 1 * x = x, so -_ ~ id. (not not!)

Can we have this based on semiring, and prove it's a ring? Note that this is only possible if we do have a multiplicative identity

[jamesmckinna]

@Taneb wrote:

A thought on this:

I wasn't sure what to make of this...

If * is idempotent, then 1 = -1 * -1 = -1, so -x = -1 * x = 1 * x = x, so -_ ~ id. (not not!)

... so such a proof would then indeed rely on rule-of-signs, and that would make this PR blocking on #2761

Can we have this based on semiring, and prove it's a ring? Note that this is only possible if we do have a multiplicative identity

Ah!? By defining -_ = id? Intriguing! But we would need some kind of Cancellative structure on the underlying +-commutativeMonoid in order to prove x+x≈0 : ∀ x → x + x ≈ 0# so that -_ = id would then define an additive inverse?

[jamesmckinna]

Cf. @JacquesCarette 's #2761 (comment) about Algebra.Consequences...
... anticipating the need for (1 + x) * (1 + y) ≈ 1 + x + y + x * y, I added the simple binomial expansion formula to Algebra.Consequences.*, as we precisely don't have a structure corresponding to SemiringWithoutOneOrZero (as it were).

[jamesmckinna]

@Taneb I think you are right, to the extent that:

• an IsCommutativeMonoid _+_ 0# satisfying Cancellative _+_, plus
• an IsMonoid _*_ 1# satisfying Idempotent _*_, plus
• _*_ DistributesOver _+_

will have, as now in the current Algebra.Properties.BooleanRing:

• x*y+y*x≈0
• y≈x⇒x+y≈0
  and hence
• +-inverse-unique for - x = x, by Cancellative _+_

Thus the additive structure will in fact be an IsAbelianGroup _+_ 0, so we would indeed have an Is(Commutative)Ring _+_ _*_ id 0 1.

So for now, I'll replace the uses of +-inverse-unique by appeals to Cancellative _+_ in the PR.

Let me know if you want to change the underlying API to:

record IsBooleanRing
         (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isSemiring : IsSemiring + * 0# 1#
    +-cancel   : Cancellative +
    *-idem     : Idempotent *

  open IsSemiring isSemiring public

  +-cancelˡ : LeftCancellative +
  +-cancelˡ = proj₁ +-cancel

  +-cancelʳ : RightCancellative +
  +-cancelʳ = proj₂ +-cancel

  *-isIdempotentMonoid :  IsIdempotentMonoid * 1#
  *-isIdempotentMonoid = record { isMonoid = *-isMonoid ; idem = *-idem }

  open IsIdempotentMonoid *-isIdempotentMonoid public
    using () renaming (isBand to *-isBand)

Everything indeed seems to work with such definition... but maybe that should be called IsBooleanSemiring, and leave the other definitions as they stand, but with isBooleanRing as a derivable property of BooleanSemirings?

UPDATED: so committed, with various knock-ons such as needing to introduce a stub for Algebra.Properties.CommutativeRing, plus some figuring out to do about re-exports... advice welcome, please!

[jamesmckinna]

Hmm, not sure if after all that refactoring that I have the public re-exports exactly correct.