Stream: Coq users

Topic: ✔ Simple question about syntax/notation


view this post on Zulip Kard Zorn (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)?

view this post on Zulip Enrico Tassi (Feb 12 2022 at 10:16):

try Print nat.

view this post on Zulip Kard Zorn (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?

view this post on Zulip Gaëtan Gilbert (Feb 12 2022 at 10:57):

S foo is 1 + foo

view this post on Zulip Gaëtan Gilbert (Feb 12 2022 at 10:57):

S means successor

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kard Zorn (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). But I am indeed mentally challenged.

view this post on Zulip Kard Zorn (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!

view this post on Zulip Enrico Tassi (Feb 12 2022 at 16:15):

Great! Good learning then.

view this post on Zulip Notification Bot (Feb 12 2022 at 16:15):

Enrico Tassi has marked this topic as resolved.


Last updated: Feb 06 2023 at 12:04 UTC