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)?

try `Print nat.`

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?

`S foo`

is `1 + foo`

`S`

means `successor`

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?

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

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).

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!

Great! Good learning then.

Enrico Tassi has marked this topic as resolved.

Last updated: Jun 22 2024 at 15:01 UTC