Stream: Coq users

Topic: ✔ Beginner: discriminate with variables


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Notification Bot (Jul 24 2021 at 02:57):

Ethan Day has marked this topic as resolved.

view this post on Zulip Alexander Gryzlov (Jul 26 2021 at 20:31):

I don't think this would work in Agda simply by utilizing constructor disjointness either.

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Aug 09 2021 at 10:31):

@kumar You can ask in a new topic.

view this post on Zulip kumar (Aug 09 2021 at 10:35):

@Ali Caglayan Thanks!


Last updated: Jan 31 2023 at 13:02 UTC