Beginner: stuck on simple proof with negation

Miscellaneous
1

Hello, I just started learning Coq and I’m trying to prove the following thm.

\neg \exists n: nat, \forall m: nat, n = m

Here’s my attempt:

Theorem attempt: ~ exists n: nat, forall m: nat, n = m.
Proof.
  unfold not.
  intros H.
  destruct H as [n H].
  specialize (H (S n)).
  discriminate H. (* Doesn't work *)

Why can I not use discriminate here? What is the correct proof for this?

2

The discriminate tactic is useful when both sides of an equality start with different constructors, which is not the case here. In your case, the proof needs to be a bit more involved, as the contradiction comes from the recursive structure of natural numbers. So, before you can meaningfully use discriminate (or injection), you need to perform a proof by induction on n to consider the various ways n can be built.

1 Like
3

Thanks for your help! Here’s the code that worked:

Theorem attempt: ~ exists n: nat, forall m: nat, n = m.
Proof.
  unfold not.
  intros H.
  destruct H as [n H].
  specialize (H (S n)).
  induction n as [| n' IH].
    - discriminate H.
    - inversion H as [H1]. apply IH in H1. assumption.
Qed.
4

Now try proving the same theorem for bool (~ exists b: bool, forall b’: bool, b = b’)

2 Likes
5

Thanks for your exercise. After it, I realized that using specialize inside destruct cases removes the need to use induction on n for the original proof:

Theorem no_single_nat: ~ exists n: nat, forall m: nat, n = m.
Proof.
  unfold not.
  intros H.
  destruct H as [n H].
  destruct n as [| n'].
  - specialize (H 1). discriminate.
  - specialize (H 0). inversion H.
Qed.