Move proof modules under Rfc3339

Main.lean

@@ -34,7 +34,7 @@
                       at a leap second, or NONE outside 1972 to 9999
     ixdtf HEX         prints  OK, then tab-separated: the printed form of
                       the RFC 9557 string, whether the example
-                      application of `Spec.exampleProcessor` must treat
+                      application of `Rfc3339.Spec.exampleProcessor` must treat
                       it as erroneous (`true` or `false`), and the values
                       of the first `u-ca` tag joined by `-`, or `-`;
                       or REJECT
@@ -54,7 +54,7 @@
 -/
 
 import Rfc3339
-import Spec.Ixdtf
+import Rfc3339.Spec.Ixdtf
 
 open Rfc3339
 
@@ -129,7 +129,7 @@ def request (line : String) : Option String :=
         let cal := match e.lookup "u-ca".toList with
           | some t => String.ofList (['-'].intercalate t.values)
           | none => "-"
-        s!"OK\t{e.print}\t{e.erroneous Spec.exampleProcessor}\t{cal}"
+        s!"OK\t{e.print}\t{e.erroneous Rfc3339.Spec.exampleProcessor}\t{cal}"
       | none => "REJECT"
   | ["fromsi", n] => do
     let s ← decimal n

Rfc3339/IxdtfTypes.lean

@@ -1,7 +1,7 @@
 /-
   What an RFC 9557 (IXDTF) timestamp is: an RFC 3339 timestamp, then a
   time zone and tags in brackets. Part of the approved specification,
-  with `Spec.lean` and `Spec/Ixdtf.lean`, since the IXDTF statements are
+  with `Rfc3339/Spec.lean` and `Spec/Ixdtf.lean`, since the IXDTF statements are
   about these types.
 -/
 

Rfc3339/Proofs.lean

@@ -0,0 +1,10 @@
+/-
+  The proofs, under the names the challenge file gives them. The
+  theorems themselves are in `Rfc3339/Proofs/Main.lean`, from the lemmas in the
+  other files.
+-/
+
+import Rfc3339.Proofs.Main
+import Rfc3339.Proofs.FromUnix.Main
+import Rfc3339.Proofs.Leap.Main
+import Rfc3339.Proofs.Ixdtf.Main

Proofs/DayNumber.lean → Rfc3339/Proofs/DayNumber.lean

@@ -5,19 +5,19 @@
 -/
 
 import Rfc3339
-import Spec.Defs
+import Rfc3339.Spec.Defs
 
 namespace Rfc3339.Proofs.DayNumber
 
 open Rfc3339
 
-theorem isLeapYear_eq (y : Nat) : isLeapYear y = Spec.isLeapYear y := by
-  unfold isLeapYear Spec.isLeapYear
+theorem isLeapYear_eq (y : Nat) : isLeapYear y = Rfc3339.Spec.isLeapYear y := by
+  unfold isLeapYear Rfc3339.Spec.isLeapYear
   by_cases h4 : y % 4 = 0 <;> by_cases h100 : y % 100 = 0 <;> by_cases h400 : y % 400 = 0 <;>
     simp [h4, h100, h400]
 
-theorem daysInMonth_eq (y m : Nat) : daysInMonth y m = Spec.daysInMonth y m := by
-  unfold daysInMonth Spec.daysInMonth
+theorem daysInMonth_eq (y m : Nat) : daysInMonth y m = Rfc3339.Spec.daysInMonth y m := by
+  unfold daysInMonth Rfc3339.Spec.daysInMonth
   rw [isLeapYear_eq]
   match m with
   | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 => simp
@@ -27,50 +27,50 @@ theorem daysInMonth_eq (y m : Nat) : daysInMonth y m = Spec.daysInMonth y m := b
     have : ¬ (1 ≤ n + 13 ∧ n + 13 ≤ 12) := by omega
     simp_all
 
-theorem offsetMinutes_eq (o : Offset) : offsetMinutes o = Spec.offsetMinutes o := by
-  cases o <;> simp [offsetMinutes, Spec.offsetMinutes]
+theorem offsetMinutes_eq (o : Offset) : offsetMinutes o = Rfc3339.Spec.offsetMinutes o := by
+  cases o <;> simp [offsetMinutes, Rfc3339.Spec.offsetMinutes]
 
 /-- One more year adds that year's length. -/
 theorem daysBeforeYear_succ (y : Nat) :
-    daysBeforeYear (y + 1) = daysBeforeYear y + Spec.yearLength y := by
-  unfold daysBeforeYear Spec.yearLength
+    daysBeforeYear (y + 1) = daysBeforeYear y + Rfc3339.Spec.yearLength y := by
+  unfold daysBeforeYear Rfc3339.Spec.yearLength
   by_cases h4 : y % 4 = 0
   · by_cases h100 : y % 100 = 0
     · by_cases h400 : y % 400 = 0
-      · have hl : Spec.isLeapYear y = true := by simp [Spec.isLeapYear, h4, h400]
+      · have hl : Rfc3339.Spec.isLeapYear y = true := by simp [Rfc3339.Spec.isLeapYear, h4, h400]
         simp only [hl, ite_true]
         omega
-      · have hl : Spec.isLeapYear y = false := by simp [Spec.isLeapYear, h100, h400]
+      · have hl : Rfc3339.Spec.isLeapYear y = false := by simp [Rfc3339.Spec.isLeapYear, h100, h400]
         simp only [hl, Bool.false_eq_true, ite_false]
         omega
-    · have hl : Spec.isLeapYear y = true := by simp [Spec.isLeapYear, h4, h100]
+    · have hl : Rfc3339.Spec.isLeapYear y = true := by simp [Rfc3339.Spec.isLeapYear, h4, h100]
       simp only [hl, ite_true]
       omega
-  · have hl : Spec.isLeapYear y = false := by simp [Spec.isLeapYear, h4]
+  · have hl : Rfc3339.Spec.isLeapYear y = false := by simp [Rfc3339.Spec.isLeapYear, h4]
     simp only [hl, Bool.false_eq_true, ite_false]
     omega
 
 theorem daysBeforeYear_eq (y : Nat) :
-    daysBeforeYear y = ((List.range y).map Spec.yearLength).sum := by
+    daysBeforeYear y = ((List.range y).map Rfc3339.Spec.yearLength).sum := by
   induction y with
   | zero => rfl
   | succ y ih =>
     rw [daysBeforeYear_succ, ih, List.range_succ, List.map_append, List.sum_append]
     simp
 
 theorem daysBeforeMonth_eq (y m : Nat) (h1 : 1 ≤ m) (h2 : m ≤ 12) :
-    daysBeforeMonth y m = ((List.range (m - 1)).map fun i => Spec.daysInMonth y (i + 1)).sum := by
+    daysBeforeMonth y m = ((List.range (m - 1)).map fun i => Rfc3339.Spec.daysInMonth y (i + 1)).sum := by
   unfold daysBeforeMonth
   rw [isLeapYear_eq]
-  cases hl : Spec.isLeapYear y <;>
+  cases hl : Rfc3339.Spec.isLeapYear y <;>
   match m, h1, h2 with
   | 1, _, _ | 2, _, _ | 3, _, _ | 4, _, _ | 5, _, _ | 6, _, _
   | 7, _, _ | 8, _, _ | 9, _, _ | 10, _, _ | 11, _, _ | 12, _, _ =>
-    simp [List.range_succ, Spec.daysInMonth, hl]
+    simp [List.range_succ, Rfc3339.Spec.daysInMonth, hl]
 
 theorem dayNumber_eq (y m d : Nat) (h1 : 1 ≤ m) (h2 : m ≤ 12) :
-    dayNumber y m d = Spec.dayNumber y m d := by
-  unfold dayNumber Spec.dayNumber
+    dayNumber y m d = Rfc3339.Spec.dayNumber y m d := by
+  unfold dayNumber Rfc3339.Spec.dayNumber
   rw [daysBeforeYear_eq, daysBeforeMonth_eq y m h1 h2]
 
 end Rfc3339.Proofs.DayNumber

Proofs/Format.lean → Rfc3339/Proofs/Format.lean

@@ -1,12 +1,12 @@
 /-
   The printer and the parser of `Rfc3339/Format.lean` against the spec:
-  `asciiUpper` is `Spec.asciiUpper`, a valid timestamp renders as
-  `Spec.render` writes it, and `parseUpper` returns `t` exactly when `t`
+  `asciiUpper` is `Rfc3339.Spec.asciiUpper`, a valid timestamp renders as
+  `Rfc3339.Spec.render` writes it, and `parseUpper` returns `t` exactly when `t`
   is valid and the input is `t.render`. From these, `parse_iff'`.
 -/
 
 import Rfc3339
-import Spec.Defs
+import Rfc3339.Spec.Defs
 
 namespace Rfc3339.Proofs.Format
 
@@ -17,24 +17,24 @@ open Rfc3339
 /-- `Char` order is the order of code points. -/
 theorem le_iff_toNat (a b : Char) : a ≤ b ↔ a.toNat ≤ b.toNat := Iff.rfl
 
-theorem asciiUpper_eq (c : Char) : asciiUpper c = Spec.asciiUpper c := by
-  unfold asciiUpper Spec.asciiUpper
+theorem asciiUpper_eq (c : Char) : asciiUpper c = Rfc3339.Spec.asciiUpper c := by
+  unfold asciiUpper Rfc3339.Spec.asciiUpper
   simp only [le_iff_toNat]
   rfl
 
 theorem print_toList (t : Timestamp) : t.print.toList = t.render := by
   simp [Timestamp.print]
 
-theorem digitChar_eq (n : Nat) (h : n < 10) : Spec.digitChar n = digitChar n := by
-  have : ∀ i : Fin 10, Spec.digitChar i.val = digitChar i.val := by decide
+theorem digitChar_eq (n : Nat) (h : n < 10) : Rfc3339.Spec.digitChar n = digitChar n := by
+  have : ∀ i : Fin 10, Rfc3339.Spec.digitChar i.val = digitChar i.val := by decide
   exact this ⟨n, h⟩
 
-/-- `pad4` and `pad2` write the last digits of any number, as `Spec.digits` does. -/
-theorem digits4 (n : Nat) : Spec.digits 4 n = pad4 n := by
-  simp [Spec.digits, pad4, List.range, List.range.loop, digitChar_eq, Nat.mod_lt]
+/-- `pad4` and `pad2` write the last digits of any number, as `Rfc3339.Spec.digits` does. -/
+theorem digits4 (n : Nat) : Rfc3339.Spec.digits 4 n = pad4 n := by
+  simp [Rfc3339.Spec.digits, pad4, List.range, List.range.loop, digitChar_eq, Nat.mod_lt]
 
-theorem digits2 (n : Nat) : Spec.digits 2 n = pad2 n := by
-  simp [Spec.digits, pad2, List.range, List.range.loop, digitChar_eq, Nat.mod_lt]
+theorem digits2 (n : Nat) : Rfc3339.Spec.digits 2 n = pad2 n := by
+  simp [Rfc3339.Spec.digits, pad2, List.range, List.range.loop, digitChar_eq, Nat.mod_lt]
 
 theorem daysInMonth_le (y m : Nat) : daysInMonth y m ≤ 31 := by
   unfold daysInMonth
@@ -49,7 +49,7 @@ theorem isValid_bounds {t : Timestamp} (h : t.isValid = true) :
   refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> first | omega | simp_all
 
 theorem renderFraction_eq (f : List Nat) (h : ∀ d ∈ f, d < 10) :
-    renderFraction f = if f = [] then [] else ['.'] ++ f.map Spec.digitChar := by
+    renderFraction f = if f = [] then [] else ['.'] ++ f.map Rfc3339.Spec.digitChar := by
   cases f with
   | nil => rfl
   | cons d ds =>
@@ -59,12 +59,12 @@ theorem renderFraction_eq (f : List Nat) (h : ∀ d ∈ f, d < 10) :
     intro x hx
     exact (digitChar_eq x (h x hx)).symm
 
-theorem offset_render_eq (o : Offset) : o.render = Spec.renderOffset o := by
-  cases o <;> simp [Offset.render, Spec.renderOffset, digits2]
+theorem offset_render_eq (o : Offset) : o.render = Rfc3339.Spec.renderOffset o := by
+  cases o <;> simp [Offset.render, Rfc3339.Spec.renderOffset, digits2]
 
-theorem render_eq (t : Timestamp) (h : t.isValid = true) : t.render = Spec.render t := by
+theorem render_eq (t : Timestamp) (h : t.isValid = true) : t.render = Rfc3339.Spec.render t := by
   have hb := isValid_bounds h
-  simp [Timestamp.render, Spec.render, digits4, digits2, renderFraction_eq t.fraction hb.2.2.2.2.2.2.1,
+  simp [Timestamp.render, Rfc3339.Spec.render, digits4, digits2, renderFraction_eq t.fraction hb.2.2.2.2.2.2.1,
     offset_render_eq]
 
 /-! ## Parsing -/
@@ -252,8 +252,8 @@ theorem parseUpper_iff (u : List Char) (t : Timestamp) :
     exact parseUpper_render h
 
 theorem parse_iff' (s : String) (t : Timestamp) :
-    parse s = some t ↔ t.isValid = true ∧ s.toList.map Spec.asciiUpper = Spec.render t := by
-  have hmap : s.toList.map asciiUpper = s.toList.map Spec.asciiUpper :=
+    parse s = some t ↔ t.isValid = true ∧ s.toList.map Rfc3339.Spec.asciiUpper = Rfc3339.Spec.render t := by
+  have hmap : s.toList.map asciiUpper = s.toList.map Rfc3339.Spec.asciiUpper :=
     List.map_congr_left (fun c _ => asciiUpper_eq c)
   rw [parse, hmap, parseUpper_iff]
   constructor

Proofs/Fraction.lean → Rfc3339/Proofs/Fraction.lean

@@ -5,7 +5,7 @@
 -/
 
 import Rfc3339
-import Spec.Defs
+import Rfc3339.Spec.Defs
 
 namespace Rfc3339.Proofs.Fraction
 
@@ -14,30 +14,30 @@ open Rfc3339
 /-- Reading digits after a value `x` already read: `x` is shifted left
     by the number of digits still to come. -/
 theorem foldl_digits (x : Nat) (ds : List Nat) :
-    List.foldl (fun acc d => 10 * acc + d) x ds = x * 10 ^ ds.length + Spec.fractionValue ds := by
+    List.foldl (fun acc d => 10 * acc + d) x ds = x * 10 ^ ds.length + Rfc3339.Spec.fractionValue ds := by
   induction ds generalizing x with
-  | nil => simp [Spec.fractionValue]
+  | nil => simp [Rfc3339.Spec.fractionValue]
   | cons d ds ih =>
-    simp only [Spec.fractionValue, List.foldl_cons, List.length_cons] at *
+    simp only [Rfc3339.Spec.fractionValue, List.foldl_cons, List.length_cons] at *
     rw [ih, ih (10 * 0 + d), Nat.pow_succ, Nat.mul_zero, Nat.zero_add, Nat.add_mul,
       Nat.add_assoc]
     congr 1
     rw [Nat.mul_comm 10 x, Nat.mul_assoc, Nat.mul_comm 10 (10 ^ ds.length)]
 
-theorem fractionValue_nil : Spec.fractionValue [] = 0 := rfl
+theorem fractionValue_nil : Rfc3339.Spec.fractionValue [] = 0 := rfl
 
 theorem fractionValue_cons (d : Nat) (ds : List Nat) :
-    Spec.fractionValue (d :: ds) = d * 10 ^ ds.length + Spec.fractionValue ds := by
+    Rfc3339.Spec.fractionValue (d :: ds) = d * 10 ^ ds.length + Rfc3339.Spec.fractionValue ds := by
   have h := foldl_digits d ds
-  simpa [Spec.fractionValue] using h
+  simpa [Rfc3339.Spec.fractionValue] using h
 
 theorem fractionValue_lt (a : List Nat) (ha : ∀ d ∈ a, d ≤ 9) :
-    Spec.fractionValue a < 10 ^ a.length := by
+    Rfc3339.Spec.fractionValue a < 10 ^ a.length := by
   induction a with
   | nil => simp [fractionValue_nil]
   | cons d ds ih =>
     have hd : d ≤ 9 := ha d (by simp)
-    have hds : Spec.fractionValue ds < 10 ^ ds.length := ih (fun e he => ha e (by simp [he]))
+    have hds : Rfc3339.Spec.fractionValue ds < 10 ^ ds.length := ih (fun e he => ha e (by simp [he]))
     rw [fractionValue_cons, List.length_cons, Nat.pow_succ]
     have h1 : d * 10 ^ ds.length + 10 ^ ds.length ≤ 10 ^ ds.length * 10 := by
       rw [Nat.mul_comm (10 ^ ds.length) 10, ← Nat.succ_mul]
@@ -46,15 +46,15 @@ theorem fractionValue_lt (a : List Nat) (ha : ∀ d ∈ a, d ≤ 9) :
 
 /-- A digit list scaled to `k` digits stays below `10 ^ k`. -/
 theorem scaled_lt (a : List Nat) (ha : ∀ d ∈ a, d ≤ 9) (k : Nat) (hk : a.length ≤ k) :
-    Spec.fractionValue a * 10 ^ (k - a.length) < 10 ^ k := by
+    Rfc3339.Spec.fractionValue a * 10 ^ (k - a.length) < 10 ^ k := by
   have h := Nat.mul_lt_mul_of_pos_right (fractionValue_lt a ha)
     ((Nat.pow_pos (n := k - a.length) (by decide : 0 < 10)))
   rwa [← Nat.pow_add, Nat.add_sub_cancel' hk] at h
 
 /-- Scaling a list with a leading digit: the digit takes the top place. -/
 theorem scaled_cons (d : Nat) (ds : List Nat) (k : Nat) (hk : ds.length ≤ k) :
-    Spec.fractionValue (d :: ds) * 10 ^ (k + 1 - (d :: ds).length) =
-      d * 10 ^ k + Spec.fractionValue ds * 10 ^ (k - ds.length) := by
+    Rfc3339.Spec.fractionValue (d :: ds) * 10 ^ (k + 1 - (d :: ds).length) =
+      d * 10 ^ k + Rfc3339.Spec.fractionValue ds * 10 ^ (k - ds.length) := by
   have e : k + 1 - (d :: ds).length = k - ds.length := by simp only [List.length_cons]; omega
   rw [e, fractionValue_cons, Nat.add_mul, Nat.mul_assoc, ← Nat.pow_add, Nat.add_sub_cancel' hk]
 
@@ -68,8 +68,8 @@ theorem compare_add_left (p x y : Nat) : compare (p + x) (p + y) = compare x y :
 theorem compareFraction_scaled (a b : List Nat) :
     (∀ d ∈ a, d ≤ 9) → (∀ d ∈ b, d ≤ 9) → ∀ k, a.length ≤ k → b.length ≤ k →
       compareFraction a b =
-        compare (Spec.fractionValue a * 10 ^ (k - a.length))
-                (Spec.fractionValue b * 10 ^ (k - b.length)) := by
+        compare (Rfc3339.Spec.fractionValue a * 10 ^ (k - a.length))
+                (Rfc3339.Spec.fractionValue b * 10 ^ (k - b.length)) := by
   induction a, b using compareFraction.induct with
   | case1 =>
     intro _ _ k _ _
@@ -161,8 +161,8 @@ theorem compareFraction_scaled (a b : List Nat) :
 
 theorem compareFraction_eq (a b : List Nat) (ha : ∀ d ∈ a, d ≤ 9) (hb : ∀ d ∈ b, d ≤ 9) :
     compareFraction a b =
-      compare (Spec.fractionValue a * 10 ^ (max a.length b.length - a.length))
-              (Spec.fractionValue b * 10 ^ (max a.length b.length - b.length)) :=
+      compare (Rfc3339.Spec.fractionValue a * 10 ^ (max a.length b.length - a.length))
+              (Rfc3339.Spec.fractionValue b * 10 ^ (max a.length b.length - b.length)) :=
   compareFraction_scaled a b ha hb _ (Nat.le_max_left _ _) (Nat.le_max_right _ _)
 
 end Rfc3339.Proofs.Fraction