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?
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.
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.
related: http://formalvindications.com/project/time-manager/
Ping for @Mireia González Bedmar who might be able to comment on your ideas :)
Yannick Forster said:
related: http://formalvindications.com/project/time-manager/
See also the Coq code: https://gitlab.com/formalv/formalv
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.
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?
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
.
Could using such a compact representation make proofs more complex as well?
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.
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?
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
Did the people doing javascript formal semantics (or java / rust formal semantics) introduce their own date definition too?
I'd really hope that was out of scope for formal semantics of a language
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