does coq has built in notion of logical xor ?

`xorb`

`!=`

also works :)

but `xorb`

is boolean, I am looking for something like `\/`

or `/\`

A <-> ~B

Or the stronger `(A /\ ~B) \/ (B /\ ~A)`

...

Its double-negation `~ (~ (A /\ ~ B) /\ ~ (B /\ ~ A))`

is weaker, but also symmetric. I can't really imagine using these on anything other than decidable propositions, so maybe the distinctions don't matter.

Paolo Giarrusso said:

Or the stronger

`(A /\ ~B) \/ (B /\ ~A)`

...

This is how I did it but if A and B are very long, it looks ugly, so I thought maybe there was a nice built in syntax for that

walker has marked this topic as resolved.

@walker you can wrap that in a definition, or create a custom inductive. There's also (next to) nothing built-in about conjunction and disjunction, they're just inductives in the stdlib

(I won't be surprised if there's hardcoded behavior for conjunction and disjunction, but a pure library solution is good enough for xor)

Last updated: Jun 18 2024 at 08:01 UTC