Partial proof of ISODateTimeToString_without_calendar_satisfies_rfc3339

theories/RFC3339.v

@@ -5,13 +5,6 @@ Open Scope char_scope.
 (* Defines the grammar from RFC 33339 *)
 (* https://www.rfc-editor.org/rfc/rfc3339#section-5.6 *)
 
-Definition digit : grammar :=
-  alt (
-    char "0" :: char "1" :: char "2" :: char "3" :: char "4" ::
-    char "5" :: char "6" :: char "7" :: char "8" :: char "9" ::
-    nil
-  ).
-
 Definition date_fullyear := ntimes 4 digit.
 Definition date_month    := ntimes 2 digit.
 Definition date_mday     := ntimes 2 digit.
@@ -25,8 +18,7 @@ Definition time_numoffset :=
     alternative (char "+") (char "-") :: time_hour :: char ":" :: time_minute :: nil
   ).
 Definition time_offset :=
-  sequence (alternative (char "Z") (char "z"))
-  time_numoffset.
+  alternative (alternative (char "Z") (char "z")) time_numoffset.
 
 Definition partial_time :=
   seq (
@@ -41,3 +33,6 @@ Definition full_time := sequence partial_time time_offset.
 
 Definition date_time :=
   seq (full_date :: alternative (char "T") (char "t") :: full_time :: nil).
+
+Definition date_time_without_offset :=
+  seq (full_date :: alternative (char "T") (char "t") :: partial_time :: nil).

theories/Section12/FormatCalendarAnnotation.v

@@ -1,5 +1,6 @@
 From Stdlib Require Import Strings.String.
 From Temporal Require Import
+  Grammar
   Section12.CalendarType
   Section12.ShowCalendar.
 Open Scope string_scope.
@@ -23,3 +24,10 @@ Definition FormatCalendarAnnotation (id' : CalendarType) (showCalendar : ShowCal
     end in
     "[" ++ flag ++ "u-ca=" ++ idStringValue ++ "]"
   end.
+
+Lemma FormatCalendarAnnotation_never :
+  forall id', generates empty (FormatCalendarAnnotation id' SC_NEVER).
+Proof.
+  intros.
+  constructor.
+Qed.

theories/Section13/FormatFractionalSeconds.v

@@ -3,8 +3,10 @@ From Stdlib Require Import
   Strings.String
   Ascii.
 From Temporal Require Import
+  Grammar
   StringUtil
   Section13.Precision.
+From Temporal Require RFC3339.
 Open Scope string_scope.
 Open Scope Z.
 
@@ -16,7 +18,14 @@ Fixpoint RemoveTrailingZero (s : string) : string :=
     | EmptyString => if eqb c "0"%char then EmptyString else String c EmptyString
     | s'' => String c EmptyString ++ s''
     end
-  end. 
+  end.
+
+Lemma RemoveTrailingZero_some_digits :
+  forall n m nsv mv, 0 < n ->
+  generates
+    (sequence digit (star digit))
+    (RemoveTrailingZero (ToZeroPaddedDecimalString n m nsv mv)).
+Admitted.
 
 (* 13.25 FormatFractionalSeconds *)
 Program Definition FormatFractionalSeconds (subSecondNanoseconds : Z) (precision : Precision) (subSecondNanoseconds_valid : 0 <= subSecondNanoseconds <= 999999999) : string :=
@@ -42,3 +51,52 @@ Program Definition FormatFractionalSeconds (subSecondNanoseconds : Z) (precision
   (*>> 3. Return the string-concatenation of the code unit 0x002E (FULL STOP) and fractionString. <<*)
     "." ++ fractionString'
   end.
+
+Lemma FormatFractionalSeconds_rfc3339 :
+  forall ns p nsv,
+  generates (maybe RFC3339.time_secfrac) (FormatFractionalSeconds ns p nsv).
+Proof.
+  intros.
+  unfold FormatFractionalSeconds.
+  destruct p.
+  - destruct (ns =? 0) eqn: ns_eq_0.
+    + apply gen_alt_l.
+      constructor.
+    + apply gen_alt_r.
+      apply gen_seq.
+      * constructor.
+      * rewrite Z.eqb_neq in ns_eq_0.
+        destruct nsv.
+        assert (l' : 0 < ns). {
+          apply Z.le_neq.
+          split.
+          - assumption.
+          - symmetry.
+            assumption.
+        }
+        eapply Grammar.equiv_elim.
+        apply RemoveTrailingZero_some_digits.
+        assumption.
+        rewrite <- Grammar.sequence_assoc.
+        apply Grammar.sequence_empty_r.
+  - destruct (p =? 0) eqn: p_eq_0.
+    + apply gen_alt_l.
+      constructor.
+    + apply gen_alt_r.
+      apply gen_seq.
+      * constructor.
+      * rewrite Z.eqb_neq in p_eq_0.
+        destruct a.
+        assert (a' : 0 < p). {
+          apply Z.le_neq.
+          split.
+          - assumption.
+          - symmetry.
+            assumption.
+        }
+        eapply Grammar.equiv_elim.
+        apply ToZeroPaddedDecimalString_gt_0_digits.
+        assumption.
+        rewrite <- Grammar.sequence_assoc.
+        apply Grammar.sequence_empty_r.
+Qed.

theories/Section13/FormatTimeString.v

@@ -3,10 +3,12 @@ From Stdlib Require Import
   Strings.String.
 From Temporal Require Import
   Basic
+  Grammar
   StringUtil
   Section13.FormatFractionalSeconds
   Section13.PrecisionPrime
   Section13.Style.
+From Temporal Require RFC3339.
 Open Scope Z.
 
 (* 13.26 FormatTimeString *)
@@ -36,3 +38,31 @@ Definition FormatTimeString (hour minute second subSecondNanoseconds : Z) (preci
   (*>> 7. Return the string-concatenation of hh, separator, mm, separator, ss, and subSecondsPart. <<*)
   hh ++ separator ++ mm ++ separator ++ ss ++ subSecondsPart
   end.
+
+Lemma FormatTimeString_rfc3339 :
+  forall h min s ns precision h0 h1 h2 h3,
+  generates RFC3339.partial_time (FormatTimeString h min s ns (NormalPrecision precision) None h0 h1 h2 h3).
+Proof.
+  intros.
+  unfold FormatTimeString.
+  repeat (apply gen_seq).
+  - apply ToZeroPaddedDecimalString_2_digits.
+    destruct h0.
+    split.
+    * assumption.
+    * now (apply Z.le_trans with (m := 23); try assumption).
+  - constructor.
+  - apply ToZeroPaddedDecimalString_2_digits.
+    destruct h1.
+    split.
+    + assumption.
+    + now (apply Z.le_trans with (m := 59); try assumption).
+  - constructor.
+  - apply ToZeroPaddedDecimalString_2_digits.
+    destruct h2.
+    split.
+    + assumption.
+    + now (apply Z.le_trans with (m := 59); try assumption).
+  - refine (proj1 (Grammar.sequence_empty_r _ _) _).
+    apply FormatFractionalSeconds_rfc3339.
+Qed.

theories/Section3/PadISOYear.v

@@ -1,8 +1,10 @@
 From Stdlib Require Import
   ZArith
   Strings.String
-  Lia.
-From Temporal Require Import StringUtil.
+  Lia
+  Program.Equality.
+From Temporal Require Import Grammar StringUtil.
+From Temporal Require RFC3339.
 Open Scope bool_scope.
 Open Scope string_scope.
 Open Scope Z.
@@ -53,3 +55,28 @@ Proof.
       apply ToZeroPaddedDecimalString_length.
       lia.
 Qed.
+
+Lemma PadISOYear_satisfies_rfc3339 :
+  forall y, 0 <= y <= 9999 -> generates RFC3339.date_fullyear (PadISOYear y).
+Proof.
+  intros.
+  unfold PadISOYear.
+  unfold PadISOYear_obligation_1.
+
+  destruct H.
+  rewrite <- Z.leb_le in H.
+  rewrite <- Z.leb_le in H0.
+  rewrite <- Z.geb_leb in H.
+
+  generalize (Bool.andb_true_iff (y >=? 0) (y <=? 9999)).
+  destruct ((y >=? 0) && (y <=? 9999)).
+  - intros.
+    rewrite Z.geb_leb in H.
+    rewrite Z.leb_le in H.
+    rewrite Z.leb_le in H0.
+    apply ToZeroPaddedDecimalString_4_digits.
+    split; assumption.
+  - rewrite H, H0.
+    intuition auto.
+    discriminate.
+Qed.

theories/Section5/ISODateTimeToString.v

@@ -43,7 +43,59 @@ Next Obligation. destruct isoDateTime. destruct Time. simpl. lia. Qed.
 Next Obligation. destruct isoDateTime. destruct Time. simpl. lia. Qed.
 Next Obligation. destruct isoDateTime. destruct Time. simpl. lia. Qed.
 
+Lemma month_rfc3339 :
+  forall isoDate h,
+  generates RFC3339.date_month (ToZeroPaddedDecimalString (month isoDate) 2 h zero_le_two).
+Proof.
+  intros.
+  apply ToZeroPaddedDecimalString_2_digits.
+  split.
+  - assumption.
+  - destruct (month_valid isoDate).
+    apply Z.le_trans with (m := 12).
+    + assumption.
+    + easy.
+Qed.
+
+Lemma mday_rfc3339 :
+  forall isoDate h,
+  generates RFC3339.date_mday (ToZeroPaddedDecimalString (day isoDate) 2 h zero_le_two).
+Proof.
+  intros.
+  apply ToZeroPaddedDecimalString_2_digits.
+  split.
+  - assumption.
+  - destruct (day_valid isoDate).
+    apply Z.le_trans with (m := 31).
+    + assumption.
+    + easy.
+Qed.
+
 Theorem ISODateTimeToString_without_calendar_satisfies_rfc3339 :
-  forall isoDateTime calendar precision',
-  generates RFC3339.date_time (ISODateTimeToString isoDateTime calendar precision' SC_NEVER).
-Admitted.
+  forall isoDateTime calendar precision,
+  0 <= year (ISODate isoDateTime) <= 9999 ->
+  generates RFC3339.date_time_without_offset (ISODateTimeToString isoDateTime calendar (NormalPrecision precision) SC_NEVER).
+Proof.
+  intros.
+  unfold ISODateTimeToString.
+  rewrite <- append_assoc.
+  rewrite <- append_assoc.
+  rewrite <- append_assoc.
+  rewrite <- append_assoc.
+  apply gen_seq.
+  - repeat (rewrite append_assoc).
+    repeat (try apply gen_seq).
+    + apply PadISOYear_satisfies_rfc3339.
+      assumption.
+    + constructor.
+    + apply month_rfc3339.
+    + constructor.
+    + refine (Grammar.equiv_elim _ (Grammar.sequence_empty_r _)).
+      apply mday_rfc3339.
+  - apply gen_seq.
+    + apply gen_alt_l.
+      constructor.
+    + apply gen_seq.
+      * apply FormatTimeString_rfc3339.
+      * apply FormatCalendarAnnotation_never.
+Qed.

theories/StringUtil.v

@@ -80,6 +80,12 @@ Proof.
     reflexivity.
 Qed.
 
+Lemma append_char_l : forall a s0, String a EmptyString ++ s0 = String a s0.
+Proof.
+  intros.
+  reflexivity.
+Qed.
+
 Lemma length_char_eq :
   forall a a', length (String a EmptyString) = length (String a' EmptyString).
 Proof.
@@ -116,6 +122,18 @@ Proof.
     now inversion H.
 Qed.
 
+Lemma length_empty : forall s, length s = 0 <-> s = EmptyString.
+Proof.
+  split.
+  - intros.
+    destruct s.
+    + reflexivity.
+    + discriminate.
+  - intros.
+    rewrite H.
+    reflexivity.
+Qed.
+
 Lemma length_nonempty : forall s, s <> EmptyString -> 0 < length s.
 Proof.
   intros.