Stream: Coq users

Topic: ✔ logical xor


view this post on Zulip walker (Nov 17 2022 at 23:19):

does coq has built in notion of logical xor ?

view this post on Zulip Li-yao (Nov 17 2022 at 23:46):

xorb

view this post on Zulip Alexander Gryzlov (Nov 18 2022 at 12:33):

!= also works :)

view this post on Zulip walker (Nov 18 2022 at 15:46):

but xorb is boolean, I am looking for something like \/ or /\

view this post on Zulip Huỳnh Trần Khanh (Nov 20 2022 at 03:44):

A <-> ~B

view this post on Zulip Paolo Giarrusso (Nov 20 2022 at 05:39):

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

view this post on Zulip James Wood (Nov 21 2022 at 10:17):

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.

view this post on Zulip walker (Nov 21 2022 at 12:59):

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

view this post on Zulip Notification Bot (Nov 21 2022 at 12:59):

walker has marked this topic as resolved.

view this post on Zulip Paolo Giarrusso (Nov 21 2022 at 17:55):

@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

view this post on Zulip Paolo Giarrusso (Nov 21 2022 at 17:56):

(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: Oct 01 2023 at 18:01 UTC