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

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.

https://github.com/agda/agda-stdlib/blob/6db08b3b2af9f220c016d2a79ace400ae60006a8/src/Algebra/Lattice/Properties/BooleanAlgebra.agda#L527

Apr 17 '25 05:04 onestruggler

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?

Apr 17 '25 08:04 jamesmckinna

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.

Apr 21 '25 15:04 JacquesCarette

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!

Apr 22 '25 12:04 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...

Jul 08 '25 13:07 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 .

Jul 10 '25 14:07 jamesmckinna

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.)

Jul 10 '25 20:07 JacquesCarette

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

Jul 10 '25 21:07 jamesmckinna

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.

Jul 10 '25 22:07 JacquesCarette

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...

Jul 11 '25 11:07 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?

Jul 11 '25 11:07 jamesmckinna

I think things are fundamentally in the realm of meta-programming, one way or another. Either we take some internal representation (Data.Record or something like it) and export it to actual Agda records, or we go one step further and do the whole quote->manipulate->export thing. It's the 'export' step that I don't think can be done right now. Though maybe I should experiment some more with Agda's meta-programming facilities.

Jul 11 '25 13:07 JacquesCarette

To summarise the (current) design decisions taken in #2763 : add

IsBooleanSemiring defined as

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

and

IsBooleanRing defined as

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

Jul 23 '25 12:07 jamesmckinna