Stream: Coq users

Topic: ✔ Simple question about syntax/notation

Vinícius Melo (Feb 12 2022 at 10:03):

I'm having trouble understanding a simple proof because of notation.

forall (l l' : list nat) (x a : nat),
perm' l l' ->
(if x =? a then S (num_oc x l) else num_oc x l) =
num_oc x (insere a l')

I don't get what the S () means. What is the difference between S (num_oc x l) and (num_oc x l)?

Enrico Tassi (Feb 12 2022 at 10:16):

try Print nat.

Vinícius Melo (Feb 12 2022 at 10:24):

Enrico Tassi said:

try Print nat.

Inductive nat : Set :=  O : nat | S : nat -> nat.
Arguments S _%nat_scope

I still don't get what it means exactly. S is like a function "Set" that maps nat -> nat? What does it do to (num_oc x l), where (num_oc x l) is the number of occurrences of x in the list l?

Gaëtan Gilbert (Feb 12 2022 at 10:57):

S foo is 1 + foo

Gaëtan Gilbert (Feb 12 2022 at 10:57):

S means successor

Enrico Tassi (Feb 12 2022 at 12:53):

May I suggest you start by reading some introductory material to Coq? Depending on your interest there are many. What do you want to do with Coq?

Karl Palmskog (Feb 12 2022 at 12:56):

see here for an overview of some material: https://github.com/coq-community/awesome-coq#books

In particular, we often recommend https://softwarefoundations.cis.upenn.edu

Vinícius Melo (Feb 12 2022 at 14:43):

Gaëtan Gilbert said:

S foo is 1 + foo

Gaëtan Gilbert said:

S means successor

That makes a lot more sense now!

Enrico Tassi said:

May I suggest you start by reading some introductory material to Coq? Depending on your interest there are many. What do you want to do with Coq?

No problem! I did try and search for it on a few online materials, but I didn't find anything more explicit about S being the succ. I'm taking classes on Mathematical and Computational Logic and Algorithm Analysis, both use coq (or pvs or any other proof assistant).

Vinícius Melo (Feb 12 2022 at 14:43):

Karl Palmskog said:

see here for an overview of some material: https://github.com/coq-community/awesome-coq#books

In particular, we often recommend https://softwarefoundations.cis.upenn.edu

Thanks a lot!

Enrico Tassi (Feb 12 2022 at 16:15):

Great! Good learning then.

Notification Bot (Feb 12 2022 at 16:15):

Enrico Tassi has marked this topic as resolved.

Last updated: Sep 30 2023 at 05:01 UTC