Lean: Update models with the datetime extension

[adpaco-aws]

Description of changes: Update the Lean models with the datetime extension, including:

• Changes to the evaluator and validator to work with datetime types and methods.
• Fixes existing theorems to work with datetime types and methods.
• Adds new theorems for datetime types and methods (two for each constructor/method).

[shaobo-he-aws]

Nit: it could be (Datetime.lt · ·)

[adpaco-aws]

I didn't know that, thanks! However, I think I'll keep like this since it's more beginner-friendly and we use the same style for IpAddr defintions.

[shaobo-he-aws]

LGTM

[adpaco-aws]

Thanks for the reviews! Ci was failing with errors like this:

error: ././././UnitTest/Datetime.lean:170:59: failed to synthesize
  Neg Duration
Additional diagnostic information may be available using the `set_option diagnostics true` command.
error: ././././UnitTest/Datetime.lean:171:62: failed to synthesize
  OfNat Duration 60000
numerals are polymorphic in Lean, but the numeral `60000` cannot be used in a context where the expected type is
  Duration
due to the absence of the instance above
Additional diagnostic information may be available using the `set_option diagnostics true` command.

when running the unit tests, so I added the instances which are infallible and I don't think they should be used for anything else other than the testing code (noted this in a comment).

I'm also planning on ignoring the DCO check because rebasing here could be complicated.

[emina]

If a simp occurs in the middle of a proof, we want to replace with simp only for robustness in the face of updates.

To figure out what needs to go into a simp only call, replace a simp with simp? in the IDE, and the Lean will give you a suggestion for how to replace that simp with simp only.

[adpaco-aws]

I've added only to most of the simp occurring anywhere other than the "tail" of a proof.

There's a couple of simps that cannot be converted to simp only without inducing errors. It's the only simp statement in the type_of_call_offset_is_sound and type_of_call_durationSince_is_sound theorems. I couldn't fix them - I suppose that's because simp? is not working well in those cases?

[emina]

You can leave them for now. Usually, the tricky case for converting to simp only is when you're replacing a simp that is applied to multiple goals simultaneously. In that case, you have to put the union of the suggestions into simp only by manually copying-pasting, which can get annoying.

[emina]

when running the unit tests, so I added the instances which are infallible and I don't think they should be used for anything else other than the testing code (noted this in a comment).

Can you point me to where in the code these are?

[adpaco-aws]

Can you point me to where in the code these are?

See comment above.

[emina]

LGTM!