Algebraic structure on Bool

Stream: maths

[Wrenna Robson]

I feel like I'm missing something obvious, but do we have + and * and the corresponding algebraic structures defined on Bool?

[Wrenna Robson]

I've just encountered this in the context of finding that Fin n -> Bool doesn't seem to have a 0.

[Kyle Miller]

Bool is a boolean algebra and uses ⊥/⊔/⊓/⊤ rather than 0/+/*/1. I'm not sure if there's a Bool-like that uses algebraic notation.

[Wrenna Robson]

Well, that's not the end of the world, I can use that notation instead as the Pi type inherits it. Though it feels to me like the kind of thing where having both might be desirable - I don't know if it creates too many issues, mind.

[Wrenna Robson]

In particular, I would use + to mean xor, not or.

[Kyle Miller]

Oh, if you want + to mean xor, then you can use Fin 2

[Wrenna Robson]

Right.

[Wrenna Robson]

It's just that (in another thread, not sure how to link) people were talking about defining bitvectors as Fin n -> Bool.

[Wrenna Robson]

I think that in any scenario where you care about bitvectors, you probably want + to mean xor. But you also probably want "or" and "and" as operations.

[Eric Wieser]

Whether you pick X = Bool or X = Fin 2, note that using Fin n -> X for bit vectors means you get and (⊓) and or (⊔) for free.

[Kyle Miller]

Mathlib has a ∆ b notation for symmetric differences at least (which is xor for bool)

[Kyle Miller]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/SymmDiff.html

[Eric Wieser]

Presumably it works just fine for Fin n -> X too

[Kyle Miller]

Yeah: docs#Pi.symmDiff_def

[Reid Barton]

In SMT-LIB "addition of bitvectors" means addition modulo 2^n.
I will grant that "bitvector" seems like an inappropriate word choice, but it's what they use.

[Reid Barton]

This certainly doesn't affect Bool itself and probably also not Fin n -> Bool, but it is a counterexample in practice to

Wrenna Robson said:

I think that in any scenario where you care about bitvectors, you probably want + to mean xor.

[Eric Wieser]

I think there's tension here between the Fin (2^n) representation (where + is obviously addition) and the Fin n -> Fin 2 representation (where + is xor)

[Eric Wieser]

Maybe trying to create a BitVector that claims to be both of these and muddies the water about what the operations mean is a mistake

[Notification Bot]

This topic was moved here from #mathlib4 > Algebraic structure on Bool by Heather Macbeth.

[Yaël Dillies]

docs3#bool.boolean_ring