akaka (Oct 29 2020 at 11:31): 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.
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: Oct 13 2024 at 01:02 UTC