Ethan Day (Jul 24 2021 at 00:30): Ethan Day (Jul 24 2021 at 00:30):What is the idiomatic way to discharge False from hypotheses like S n = n, or S (S n) = n? Right now it seems like I need to prove a lemma for each of those, which makes me think that either I encountered a bug or I am missing something.
Donald Sebastian Leung (Jul 24 2021 at 02:26):lia should work:
From Coq Require Import Lia.
Goal forall n, S n = n -> False.
Proof. lia. Qed.
Disclaimer: not tested, may not compile
Ethan Day (Jul 24 2021 at 02:53):Thank you, I don't think I would have figured that out on my own. I learned Agda first, and my instinct is to try to get the type checker to fail to unify the terms.
Notification Bot (Jul 24 2021 at 02:57):Ethan Day has marked this topic as resolved.
Alexander Gryzlov (Jul 26 2021 at 20:31):I don't think this would work in Agda simply by utilizing constructor disjointness either.
kumar (Aug 09 2021 at 10:23):is this room still active? I had question regarding some proof exercise in cpdt.
although I'm not sure if this is the right place to ask
Ali Caglayan (Aug 09 2021 at 10:31):@kumar You can ask in a new topic.
kumar (Aug 09 2021 at 10:35):@Ali Caglayan Thanks!
Last updated: Sep 23 2023 at 07:01 UTC