Stream: Coq users

Topic: Simple properties of natural numbers


view this post on Zulip Pavel Shuhray (May 10 2023 at 06:21):

Hi
What is the names of the following theorems

forall n:nat, S n = 0 -> False.
forall (n,m:nat), S n = S m -> n = m.

How can I find them myself?

view this post on Zulip Laurent Théry (May 10 2023 at 06:30):

Require Import Arith.

(* forall n:nat, S n = 0 -> False. *)
Search (S _ = 0).
(* forall (n,m:nat), S n = S m -> n = m. *)
Search (S _ = S _).

view this post on Zulip Guillaume Melquiond (May 10 2023 at 06:36):

Note also that those properties are corollaries of the fact that S and 0 are constructors. So, you can also use the tactics discriminate and injection, respectively, instead of applying theorems.


Last updated: Mar 29 2024 at 14:01 UTC