Do we need a definition for `(Is)BooleanRing`?

[onestruggler]

Here, boolean algebra gives a commutative ring, but it shoud give more than that, .i.e., a boolean ring. On the other hand, there is no more other boolean ring except for the one comes from a boolean algebra. I am not sure if we need such a defintion. On the other other hand, at least, a usage will be clarifing the correspondence between boolean algebras and boolean rings.

agda-stdlib/src/Algebra/Lattice/Properties/BooleanAlgebra.agda

Line 527 in 6db08b3

⊕-∧-commutativeRing : CommutativeRing _ _

[jamesmckinna]

There probably is/may be some archeology to go through here (NB I have not myself done so!) about the DefaultXorRing implementation, as well as Biased versions of Algebra.Lattice.{Structures|Bundles}?
Would it make sense to add IsBooleanRing to Algebra.Lattice.Structures.Biased and go from there?

[JacquesCarette]

While it "makes sense" to add IsBooleanRing to Algebra.Lattice.Structures.Biased, it also pretty much insures no one's going to find it... IsBooleanRing in my mind is part of the 'usual' Algebra hierarchy. It's a theorem that it is isomorphic to something that naturally finds a home in Algebra.Lattice.

[jamesmckinna]

Hmmm, aren't all the Biased constructions expressions of 'theorems'... as in, 'smart constructors' are 'proofs' of derivable/admissible properties, under PAT. Cf. Groups as Loops/Quasigroups?

As for discoverability (but, as ever, grep, though a very blunt instrument, would find it for you?) I'd be happy with it under Algebra.Structures, but once the theorem is proved (moreover: where?) is there subsequently any further role for it? (Apologies for my ignorance on this one, for all I know, the ring aspect is more important than the order-theoretic one?)

UPDATED: I went away and did some reading. @JacquesCarette I'm convinced, on two grounds:

• the axiomatisation would be 'straightforward', consisting of isRing and *-idem fields
• (I hadn't realised): these define a full subcategory of Ring

On the second point, do we (ever) attempt to be systematic, or otherwise exploit, fullness of subcategories in stdlib (if so: how?), and is this a (the?) measure of 'interestingness' of of sub-Structure/Bundles?

So, to the title of the issue: yes!

[jamesmckinna]

Hmmm... I've been experimenting towards a PR for this... but I'm not even clear what the API should be:

• the 'obvious' would/should be

  record IsBooleanRing
         (_+_ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isRing : IsRing _+_ _*_ -_ 0# 1#
    *-idem : Idempotent _*_

  from which we can then prove (eg see https://en.wikipedia.org/wiki/Boolean_ring#Properties_of_Boolean_rings)
  • *-comm : Commutative _*_
  • x+x≈0 : ∀ x → (x + x) ≈ 0#
  • etc.
• but to do so within the existing discipline of Algebra.Structures (few or no additional manifest fields requiring non-trivial equational reasoning; such things should be postponed to Algebra.Properties.X...?), it might be easier to declare a less minimal interface

  record IsBooleanRing
         (_+_ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0# 1#
    *-idem : Idempotent _*_
    x+x≈0 : ∀ x → (x + x) ≈ 0#
    ...

  and then write a Biased smart constructor which instantiates all the redundant fields...?

I realised I am not clear how (best) to proceed given the current organisation of Algebra.Structures and Algebra.Bundles, which don't seem to permit incremental bootstrapping of IsY structures with Properties.X for IsX substructures... cf. the earlier #2571 and the current #2761 .

Advice/discussion welcome!

NB. I realise that Algebra.Consequences is one way to provide such 'escapes'/dependency cycle breaks, where properties can be proved without requiring an IsX value to be in scope, but after a while, it's again not clear what's being achieved if all properties of a given structure need to be in scope in order to write the proofs involved...

[jamesmckinna]

In the end, in #2763 I've followed convention by delegating the 'interesting' proofs to Properties, even though that means that neither the structure, nor the bundle, has immediate access to the proofs of:

• *-comm : Commutative _*_
• x+x≈0 : ∀ x → x + x ≈ 0#

and hence to the other associated structures/bundles.

I'm still of the view that such indirection is not, in the end, desirable, so welcome discussion of how to tackle that... better. Cf. #2762 .

[JacquesCarette]

Much hesitation on this. I'm sure we could muddle through sensibly for BooleanRing, but that's just the tip of the iceberg. I wouldn't want to set the wrong precedent here and then quickly yearn for v4.0!

(I'm not saying that anything that @jamesmckinna is wrong, I'm saying that I can't wrap my head around the bigger problem well enough to have a cogent opinion at the moment. For one, it does indeed seem that the Algebra.Consequences approach does not really scale very well.)

[jamesmckinna]

Ditto. re: "much hesitation"... #2763 is one possible solution, but I'm far from convinced it's the right one... sigh

[JacquesCarette]

Oh, as far as 'right' is concerned, I am quite convinced that the only way to do what we want would be for Agda to have features for representing theories and other parametrized bundles of information in much more flexible ways.

Declarations in Agda are a solidly second-class language. It probably does not need to be full first-class, but sure needs more features!

Lean and Rocq are in the same boat. In both those cases, they are actively using meta-programming to get the job done.

[jamesmckinna]

Re: v4.0
We could consider (whatever becomes of) #2763 for v2.x, and that would leave us a chance to reconsider for v3.0... not least since I got #2762 down 'on paper', and hence no longer cluttering my mind while thinking about the 'orthodox' solution to this issue ...

Hoping that v4.0 might be the eventual opportunity for (some) hypothetical-rewrites to enter the picture...

[jamesmckinna]

Re: Agda declarations
Nice analysis, shame about the conclusion(s) for our competitors...?
But can we internalise record-level meta-programming via Data.Record?