Stream: Coq users

Topic: ✔ logical xor

walker (Nov 17 2022 at 23:19):

does coq has built in notion of logical xor ?

Li-yao (Nov 17 2022 at 23:46):

xorb

Alexander Gryzlov (Nov 18 2022 at 12:33):

!= also works :)

walker (Nov 18 2022 at 15:46):

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

Huỳnh Trần Khanh (Nov 20 2022 at 03:44):

A <-> ~B

Paolo Giarrusso (Nov 20 2022 at 05:39):

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

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.

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

Notification Bot (Nov 21 2022 at 12:59):

walker has marked this topic as resolved.

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

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: Apr 19 2024 at 06:02 UTC