Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Question while learning Coq from Software Foundations book

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question while learning Coq from Software Foundations book


Chronological Thread 
  • From: David P Á <david AT picon.email>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Question while learning Coq from Software Foundations book
  • Date: Wed, 24 May 2017 11:31:24 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=david AT picon.email; spf=Pass smtp.mailfrom=david AT picon.email; spf=None smtp.helo=postmaster AT ns3014420.ip-178-32-223.eu
  • Ironport-phdr: 9a23:Zzl0DxaBjudHs4n9kfk3tTD/LSx+4OfEezUN459isYplN5qZoMq5bnLW6fgltlLVR4KTs6sC0LuI9f2/ESxYuNDa4S9EKMQNHzY+yuwo3CUYQ/S5QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4VvJ6IwxxfTonZFefldyWd0KV6OhRrx6MO98Zx5/yhMp/4t8tNLXLnncag/UbFXAzMqPnwv6sHsqRfNUxaE6GEGUmURnBpIAgzF4w//U5zsrCb0tfdz1TeDM8HuQr86RTqt76FwSB/1kygHLCI28HvWisNrkq1Wpg+qqgFlzI7VZIGVM+d+fr/YcNgHS2dNQtpdWipcCY66coABDfcOPfxAoofguVUOoxuwCwqiCuzhxTBHhGP506Ih3uQ9EgzLxhAsE84AvXnWqtj+KaccUfqyzKnN1TjNYelZ2Sn86IfVah8vu+mDWLZtesfW1EYgDR3FjlSNpoH+JzOV1/gCs2+d7+Z6S+2vjnQoqwB1ojW2wMonl4rHhpoNx1zZ9yh0w5w5KNOmREJhf9KoDpVduzuZOoZ0Ws8vQG9ltDwnxrAHuZO3ZjUGxIgoyhLFdfCLb4qF7xT+X+iLOzh4nmhqeLenihay70egzur8W9Gy0FZRoCdJjsTAu38C2hDN9sSLUPp9/l+41TqS1Q3e6fhILE4qmabCNZIt3LA9moANvkTeBiP2mUP2g7GKdkg85+Sl6efqbq/oq5OCLYN4lB/yP6o0lsG8A+k0Kg0OUHKa+eS42r3j50r5QLBSg/IriKbZrpHaKtkAq66hAg9azoEj6xClAzi41dQXh3gHLFZddBKdk4fpI03OIOz/Dfqnn1usly5ry+naMb3lH5XCNWPOkKzhfLZ4805T0hA/zdFZ55JOC7EOOuj/WkHrtI+QMhhsOAuthu3jFd9V14UEWGvJDLXKHrnVtAqk7/wuL960UyZd7Dr0Nfkpz+bvhng/31IYdKiti8hEIEukF+hrdh3KKUHnhc0MRD8H

On 24/05/2017 6:50, nikhil kaushik wrote:
> How does O becomes 0 when we use it in definition of

This definition is of the Peano naturals. Peano axioms say: there is a
constant (0) which is a natural number. This corresponds to the
constructor O which takes no arguments. Then, for every natural, one can
construct a natural S(n) where S is the successor. This is the 2nd
constructor which takes a nat argument.

> Definition pred (n : nat) : nat :=
> match n with
> | O => O
> | S n' => n'
> end.
>
> I only understood that O represents natural numbers and S takes a natural
> number and return another natural number so S is a function.

O doesn't represent natural numbers, O is a constructor for a natural.
It constructs 0.

> What I do not get is when our defined nat data type is used in
> pred definition how does O represent 0? And how does S n' pattern
> match gives us predecessor of n.

pred gives you the predecessor of a number. Because Coq wants totality
here, pred must be defined for all n, including 0. Unfortunately this
requires us to say that the predecessor of 0 is 0 (since -1 is not in
nat). So hence:

| O => O

matches O and produces O. (pred O) -> O.

And when the natual is of the form S n' the match gives us n'. So say
you have:
S(S(S(O))), which is 3.
You go through the match. Constructors are disjoint so S something can't
match O, so you go to the next one, S n'. So n' becomes the thing inside
the first S, S(S(O)), and the return of the match is that n', which is
2, predecessor of 3.

HTH,
--David.



Archive powered by MHonArc 2.6.18.

Top of Page