Stream: Coq users

Topic: A date type in coq


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

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?

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

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

view this post on Zulip Yannick Forster (Jun 07 2022 at 09:14):

related: http://formalvindications.com/project/time-manager/

view this post on Zulip Yannick Forster (Jun 07 2022 at 09:15):

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

view this post on Zulip Ana de Almeida Borges (Jun 07 2022 at 09:40):

Yannick Forster said:

related: http://formalvindications.com/project/time-manager/

See also the Coq code: https://gitlab.com/formalv/formalv

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

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

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

view this post on Zulip Julin S (Jun 25 2022 at 07:39):

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (Jun 27 2022 at 20:15):

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

view this post on Zulip 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 13 2024 at 01:02 UTC