3.6. Roundtrip Theorem🔗

Parsing the canonical string representation of any datetime recovers the original value. This is the headline user-facing property — parse and toString? are mutually inverse wherever toString? is defined — and it is what underpins toString?_injective above.

theorem

Cedar.Thm.Datetime.parse_toString_roundtrip {d : Datetime}
  {str : String} (h : toString? d = some str) :
  Datetime.parse str = some d
Cedar.Thm.Datetime.parse_toString_roundtrip
  {d : Datetime} {str : String}
  (h : toString? d = some str) :
  Datetime.parse str = some d

parse ∘ toString? roundtrip: every successfully serialized datetime parses back to the original value.

It is a direct corollary of completeness: a successfully serialized string is well-formed with computed value d.val.toInt, so completeness parses it back to d. The total-Option phrasing packages the same fact without a side hypothesis on definedness:

theorem

Cedar.Thm.Datetime.bind_parse_toString? (d : Datetime) :
  (toString? d).bind Datetime.parse =
    Option.map (fun x => d) (toString? d)
Cedar.Thm.Datetime.bind_parse_toString?
  (d : Datetime) :
  (toString? d).bind Datetime.parse =
    Option.map (fun x => d) (toString? d)

Total Option formulation of the partial serialization roundtrip.

All theorems above are machine-checked, contain no proof placeholders, and rely only on the three standard axioms (propext, Classical.choice, Quot.sound).