State and prove some theorems

README.md

@@ -25,6 +25,7 @@ $ ./build.sh
 * [3.5.6 RegulateISODate](theories/Section3/RegulateISODate.v)
 * [3.5.7 IsValidISODate](theories/Section3/IsValidISODate.v)
 * [3.5.9 PadISOYear](theories/Section3/PadISOYear.v)
+* [3.5.10 TemporalDateToString](theories/Section3/TemporalDateToString.v)
 * [3.5.12 CompareISODate](theories/Section3/CompareISODate.v)
 ### Section 4
 * [4.5.1 Time Records](theories/Section4/TimeRecord.v)
@@ -79,6 +80,7 @@ $ ./build.sh
 * [13.27 GetUnsignedRoundingMode](theories/Section13/GetUnsignedRoundingMode.v)
 
 ## Inconsistencies
+* [3.5.1 ISO Date Records](theories/Section3/ISODateRecord.v) (Implied consistent, but not explicit)
 * [4.5.10 BalanceTime](theories/Section4/BalanceTime.v)
 * [7.5.21 TimeDurationFromComponents](theories/Section7/TimeDurationFromComponents.v)
 * [7.5.26 TimeDurationFromEpochNanosecondsDifference](theories/Section7/TimeDurationFromEpochNanosecondsDifference.v)
@@ -87,3 +89,19 @@ $ ./build.sh
 
 ## Notes
 * [5.5.3 CombineISODateAndTimeRecord](theories/Section5/Notes/CombineISODateAndTime.v)
+
+## Theorems
+### Proven
+* [RegulateISODate_never_throws_on_constrain](theories/Section3/RegulateISODate.v)
+* [PadISOYear_result_length_at_least_4](theories/Section3/PadISOYear.v)
+* [BalanceTime_IsValidTime](theories/Section4/BalanceTime.v)
+* [DateDurationSign_year_sign_dominates](theories/Section7/DateDurationSign.v)
+* [CompareISODate_eq_zero](theories/Section3/CompareISODate.v)
+* [CompareISODate_eq_implies_eq_zero](theories/Section3/CompareISODate.v)
+
+### Unproven
+* [TemporalDateToString_without_calendar_satisfies_rfc3339](theories/Section3/TemporalDateToString.v)
+* [ISODateTimeToString_without_calendar_satisfies_rfc3339](theories/Section5/ISODateTimeToString.v)
+* [AddTime_adding_zero_no_change](theories/Section4/AddTime.v)
+* [CompareTimeRecord_eq_zero](theories/Section4/CompareTimeRecord.v)
+* [CompareTimeRecord_eq_implies_eq_zero](theories/Section4/CompareTimeRecord.v)

theories/Grammar.v

@@ -0,0 +1,260 @@
+(* Defines regular "grammars" in terms of regular expressions. *)
+
+From Stdlib Require Import Ascii List Strings.String Setoid Program.Equality.
+From Temporal Require Import StringUtil.
+Open Scope string_scope.
+
+(** A regular grammar *)
+Inductive grammar :=
+| nothing
+| empty
+| char (c : ascii)
+| alternative (a b : grammar)
+| sequence (a b : grammar)
+| star (a : grammar).
+
+(** `generates g s` is a proposition which states that the string `s` can be
+    generated by the grammar `g` *)
+Inductive generates : grammar -> string -> Prop :=
+| gen_empty : generates empty EmptyString
+| gen_char : forall c s, generates (char c) (String c s)
+| gen_alt_l : forall s a b, generates a s -> generates (alternative a b) s
+| gen_alt_r : forall s a b, generates b s -> generates (alternative a b) s
+| gen_seq : forall s0 s1 a b, generates a s0 -> generates b s1 -> generates (sequence a b) (s0 ++ s1)
+| gen_star_l : forall a, generates (star a) EmptyString
+| gen_star_r : forall s0 s1 a, generates a s0 -> generates (star a) s1 -> generates (star a) (s0 ++ s1).
+
+Fixpoint ntimes (n : nat) (a : grammar) :=
+  match n with
+  | 0 => a
+  | S n' => sequence a (ntimes n' a)
+  end.
+
+Fixpoint seq (gs : list grammar) :=
+  match gs with
+  | nil => empty
+  | g :: gs' => sequence g (seq gs')
+  end.
+
+Fixpoint alt (gs : list grammar) :=
+  match gs with
+  | nil => nothing
+  | g :: gs' => alternative g (alt gs')
+  end.
+
+Definition maybe a := alternative empty a.
+
+Module Grammar.
+  (* two grammars are equivalent if they generate the same strings *)
+  Definition Equiv (a b : grammar) := forall s, generates a s <-> generates b s.
+
+  Module Equiv.
+    Theorem refl : reflexive grammar Equiv.
+    Proof.
+      unfold reflexive, Equiv.
+      split; intros; assumption.
+    Qed.
+
+    Theorem symm : symmetric grammar Equiv.
+    Proof.
+      unfold symmetric, Equiv.
+      split; apply H.
+    Qed.
+
+    Theorem trans : transitive grammar Equiv.
+    Proof.
+      unfold transitive, Equiv.
+      split.
+      - intros. apply H0. apply H. assumption.
+      - intros. apply H. apply H0. assumption.
+    Qed.
+
+    Add Relation grammar Equiv
+      reflexivity proved by refl
+      symmetry proved by symm
+      transitivity proved by trans
+      as Equiv_rel.
+  End Equiv.
+
+  Theorem alternative_assoc :
+    forall a b c,
+    Equiv (alternative (alternative a b) c) (alternative a (alternative b c)).
+  Proof.
+    split.
+    - intros.
+      dependent induction H.
+      + dependent induction H.
+        apply gen_alt_l; assumption.
+        apply gen_alt_r, gen_alt_l; assumption.
+      + apply gen_alt_r, gen_alt_r; assumption.
+    - intros.
+      dependent induction H.
+      + apply gen_alt_l, gen_alt_l; assumption.
+      + dependent induction H.
+        apply gen_alt_l, gen_alt_r; assumption.
+        apply gen_alt_r; assumption.
+  Qed.
+
+  Theorem alternative_comm :
+    forall a b, Equiv (alternative a b) (alternative b a).
+  Proof.
+    split.
+    - intros.
+      dependent induction H.
+      + apply gen_alt_r.
+        assumption.
+      + apply gen_alt_l.
+        assumption.
+    - intros.
+      dependent induction H.
+      + apply gen_alt_r.
+        assumption.
+      + apply gen_alt_l.
+        assumption.
+  Qed.
+
+  Theorem alternative_nothing : forall a, Equiv a (alternative a nothing).
+  Proof.
+    split.
+    - intros.
+      apply gen_alt_l.
+      assumption.
+    - intros.
+      dependent induction H.
+      + assumption.
+      + inversion H.
+  Qed.
+
+  Theorem sequence_assoc :
+    forall a b c,
+    Equiv (sequence (sequence a b) c) (sequence a (sequence b c)).
+  Proof.
+    split.
+    - intros.
+      dependent induction H.
+      dependent induction H.
+      rewrite append_assoc.
+      apply gen_seq.
+      + assumption.
+      + apply gen_seq; assumption.
+    - intros.
+      dependent induction H.
+      dependent induction H0.
+      rewrite <- append_assoc.
+      apply gen_seq.
+      + apply gen_seq; assumption.
+      + assumption.
+  Qed.
+
+  Theorem sequence_empty_l : forall a, Equiv a (sequence empty a).
+  Proof.
+    split.
+    - intros.
+      rewrite <- append_empty_l.
+      apply gen_seq.
+      + constructor.
+      + assumption.
+    - intros.
+      dependent induction H.
+      dependent induction H.
+      assumption.
+  Qed.
+
+  Theorem sequence_empty_r : forall a, Equiv a (sequence a empty).
+  Proof.
+    split.
+    - intros.
+      rewrite <- append_empty_r.
+      apply gen_seq.
+      + assumption.
+      + constructor.
+    - intros.
+      dependent induction H.
+      dependent induction H0.
+      rewrite append_empty_r.
+      assumption.
+  Qed.
+
+  Theorem sequence_nothing_l : forall a, Equiv nothing (sequence nothing a).
+  Proof.
+    split.
+    - intros.
+      inversion H.
+    - intros.
+      dependent induction H.
+      inversion H.
+  Qed.
+
+  Theorem sequence_nothing_r : forall a, Equiv nothing (sequence a nothing).
+  Proof.
+    split.
+    - intros.
+      inversion H.
+    - intros.
+      dependent induction H.
+      inversion H0.
+  Qed.
+
+  Theorem unfold_star : forall a, Equiv (star a) (maybe (sequence a (star a))).
+  Proof.
+    split.
+    - intros.
+      dependent induction H.
+      + apply gen_alt_l.
+        constructor.
+      + apply gen_alt_r.
+        apply gen_seq; assumption.
+    - intros.
+      dependent induction H; dependent induction H.
+      + apply gen_star_l.
+      + apply gen_star_r; assumption.
+  Qed.
+
+  Theorem sequence_alternative_distrib_l :
+    forall a b c,
+    Equiv (sequence a (alternative b c)) (alternative (sequence a b) (sequence a c)).
+  Proof.
+    split.
+    - intros.
+      dependent induction H.
+      dependent induction H0.
+      + apply gen_alt_l.
+        apply gen_seq; assumption.
+      + apply gen_alt_r.
+        apply gen_seq; assumption.
+    - intros.
+      dependent induction H; dependent induction H.
+      + apply gen_seq.
+        assumption.
+        apply gen_alt_l.
+        assumption.
+      + apply gen_seq.
+        assumption.
+        apply gen_alt_r.
+        assumption.
+  Qed.
+
+  Theorem sequence_alternative_distrib_r :
+    forall a b c,
+    Equiv (sequence (alternative a b) c) (alternative (sequence a c) (sequence b c)).
+  Proof.
+    split.
+    - intros.
+      dependent induction H.
+      dependent induction H.
+      + apply gen_alt_l.
+        apply gen_seq; assumption.
+      + apply gen_alt_r.
+        apply gen_seq; assumption.
+    - intros.
+      dependent induction H; dependent induction H.
+      + apply gen_seq.
+        apply gen_alt_l.
+        assumption.
+        assumption.
+      + apply gen_seq.
+        apply gen_alt_r.
+        assumption.
+        assumption.
+  Qed.
+End Grammar.

theories/RFC3339.v

@@ -0,0 +1,43 @@
+From Stdlib Require Import Ascii List Strings.String.
+From Temporal Require Import Grammar.
+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.
+
+Definition time_hour    := ntimes 2 digit.
+Definition time_minute  := ntimes 2 digit.
+Definition time_second  := ntimes 2 digit.
+Definition time_secfrac := seq (char "." :: digit :: star digit :: nil).
+Definition time_numoffset :=
+  seq (
+    alternative (char "+") (char "-") :: time_hour :: char ":" :: time_minute :: nil
+  ).
+Definition time_offset :=
+  sequence (alternative (char "Z") (char "z"))
+  time_numoffset.
+
+Definition partial_time :=
+  seq (
+    time_hour :: char ":" :: time_minute :: char ":" :: time_second ::
+    maybe time_secfrac :: nil
+  ).
+
+Definition full_date :=
+  seq (date_fullyear :: char "-" :: date_month :: char "-" :: date_mday :: nil).
+
+Definition full_time := sequence partial_time time_offset.
+
+Definition date_time :=
+  seq (full_date :: alternative (char "T") (char "t") :: full_time :: nil).