## Stream: Coq users

### Topic: A date type in coq

#### Julin S (Jun 07 2022 at 08:57):

How can we have a type in coq that represents date?

So that the date is correct by construction, taking care of things like

• Leap years (days in February differ)
• Number of days in the month (28/29/30/31)

Maybe dependent types can help?

I guess somebody must've done this already but couldn't find it with web searches.

Maybe we could use subtypes subset types like `{d : nat | d > 0 /\ d < 32}`?

Or would having separate constructors like `D1`, `D2`, ..., `D31` be better?

#### Meven Lennon-Bertrand (Jun 07 2022 at 09:04):

One possible way would be to define a function `days (year : nat) (month : { m : nat | 0 < m <= 12 } : nat` which computes the number of days in a month, and then define your triple using that function to ensure the day is a valid one, something like

``````Record date := { year : nat ; month : { m : nat | 1 <= m <= 12 } ; day : { d : nat | 1 <= d <= days year month } }.
``````

Not sure how easy to use this would be though, this really depends on the kind of things you want to do.

#### Kenji Maillard (Jun 07 2022 at 09:09):

I would rather split the raw data part from the validity criterion, first defining a plain record `Record raw_date := {year : nat ; month : nat ; day : nat }.` and then a function `valid_date : raw_date -> bool` that check that a given raw_date is valid and finally define a subset type if needed `Definition date := { d : raw_date | valid_date d = true }.`. Then functions manipulating dates would first be defined on the computational content and then refined with a lemma stating that they preserve validity.

#### Yannick Forster (Jun 07 2022 at 09:15):

Ping for @Mireia González Bedmar who might be able to comment on your ideas :)

#### Ana de Almeida Borges (Jun 07 2022 at 09:40):

Yannick Forster said:

#### Mireia González Bedmar (Jun 07 2022 at 15:03):

In FormalV we followed an approach similar to what Kenji suggested. Using natural numbers was better because we were able to use known results about arithmetic to prove properties. @Julin S Feel free to ask for any details, and if you want to use the code but the license poses any trouble, you can let me know as well. We plan to have it as an opam package soon.

#### Julin S (Jun 25 2022 at 07:32):

When I made a function like:

``````Definition valid_year (y:nat) : bool :=
(Nat.ltb 0 y) && (Nat.ltb y 9999).
``````

I got a message saying:

``````To avoid stack overflow, large numbers in nat are interpreted as
applications
of Nat.of_num_uint. [abstract-large-number,numbers]
``````

Could it be something to worry about?

#### Guillaume Melquiond (Jun 25 2022 at 07:36):

Yes. You have to keep in mind that `nat` values are unary integers, so 9999 is actually `S (S (S ... O))` with 10000 constructors. So, `nat` is fine if you want manipulate very small integers. But here, you should consider using more compact representations such as `N` or `Z`.

#### Julin S (Jun 25 2022 at 07:39):

Could using such a compact representation make proofs more complex as well?

#### Guillaume Melquiond (Jun 25 2022 at 07:41):

Doing an induction is simpler over `nat`, but that is about the only difference I can think of. Since you are representing dates here, I very much doubt you will ever need to do an induction, so it will make no difference.

#### Julin S (Jun 25 2022 at 10:12):

Would it be possible for us to make use of some notations and have some way to just enter an encoding of a date so that coq can figure out based on the type to see if it's a valid date?

#### Ana de Almeida Borges (Jun 25 2022 at 10:39):

Since validity is decidable, you can define it in `bool` and have Coq automatically compute whether a given date is valid. See for example this definition of min_date and the definition of vdT above

#### Emilio Jesús Gallego Arias (Jun 27 2022 at 11:59):

Did the people doing javascript formal semantics (or java / rust formal semantics) introduce their own date definition too?

#### Paolo Giarrusso (Jun 27 2022 at 20:15):

I'd really hope that was out of scope for formal semantics of a language

#### Paolo Giarrusso (Jun 27 2022 at 20:16):

formalizing dates is valuable of course, but you'd hope the semantics of the core language doesn't depend on it

Last updated: Oct 01 2023 at 18:01 UTC