## 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