Stream: Coq users

Topic: Proof in coq

view this post on Zulip akaka (Oct 29 2020 at 11:31):

Can someone help me in proving this using coq script ((q -> p) -> p) -> ((p -> q) -> q) ?
I tried using the identity a -> b = ~ a \/ b but couldn't proceed further.

view this post on Zulip Karl Palmskog (Oct 29 2020 at 11:53):

Coq doesn't generally support "identities" of properties like the one you suggested. You can either add more axioms (e.g., an incarnation of the law of excluded middle) or reformulate the theorem to be about booleans if you want to use (a -> b) <-> (~ a \/ b)

Last updated: Feb 01 2023 at 11:04 UTC