Add files using upload-large-folder tool

backend/core/leanprover--lean4---v4.22.0/src/lean/Std/Time/Zoned/Database.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Zoned.ZonedDateTime
+import Std.Time.Zoned.Database.Basic
+import Std.Time.Zoned.Database.TZdb
+import Std.Time.Zoned.Database.Windows
+import Init.System.Platform
+
+namespace Std
+namespace Time
+namespace Database
+open TimeZone.ZoneRules
+
+set_option linter.all true
+
+/--
+Gets the zone rules for a specific time zone identifier, handling Windows and non-Windows platforms.
+In windows it uses the current `icu.h` in Windows SDK. If it's linux or macos then it will use the `tzdata`
+files.
+-/
+def defaultGetZoneRules : String → IO TimeZone.ZoneRules :=
+  if System.Platform.isWindows
+    then getZoneRules WindowsDb.default
+    else getZoneRules TZdb.default
+
+/--
+Gets the local zone rules, accounting for platform differences.
+In windows it uses the current `icu.h` in Windows SDK. If it's linux or macos then it will use the `tzdata`
+files.
+-/
+def defaultGetLocalZoneRules : IO TimeZone.ZoneRules :=
+  if System.Platform.isWindows
+    then getLocalZoneRules WindowsDb.default
+    else getLocalZoneRules TZdb.default

backend/core/leanprover--lean4---v4.22.0/src/lean/Std/Time/Zoned/Database/Basic.lean

@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Zoned.ZoneRules
+import Std.Time.Zoned.Database.TzIf
+
+namespace Std
+namespace Time
+
+set_option linter.all true
+
+/--
+A timezone database from which we can read the `ZoneRules` of some area by it's id.
+-/
+protected class Database (α : Type) where
+
+  /--
+  Retrieves the zone rules information (`ZoneRules`) for a given area at a specific point in time.
+  -/
+  getZoneRules : α → String → IO TimeZone.ZoneRules
+
+  /--
+  Retrieves the local zone rules information (`ZoneRules`) at a given timestamp.
+  -/
+  getLocalZoneRules : α → IO TimeZone.ZoneRules
+
+namespace TimeZone
+
+/--
+Converts a Boolean value to a corresponding `StdWall` type.
+-/
+def convertWall : Bool → StdWall
+  | true => .standard
+  | false => .wall
+
+/--
+Converts a Boolean value to a corresponding `UTLocal` type.
+-/
+def convertUt : Bool → UTLocal
+  | true => .ut
+  | false => .local
+
+/--
+Converts a given time index into a `LocalTimeType` by using a time zone (`tz`) and its identifier.
+-/
+def convertLocalTimeType (index : Nat) (tz : TZif.TZifV1) (identifier : String) : Option LocalTimeType := do
+  let localType ← tz.localTimeTypes[index]?
+  let offset := Offset.ofSeconds <| .ofInt localType.gmtOffset
+  let abbreviation := tz.abbreviations.getD index (offset.toIsoString true)
+  let wallflag := convertWall (tz.stdWallIndicators.getD index true)
+  let utLocal := convertUt (tz.utLocalIndicators.getD index true)
+
+  return {
+    gmtOffset := offset
+    isDst := localType.isDst
+    abbreviation
+    wall := wallflag
+    utLocal
+    identifier
+  }
+
+/--
+Converts a transition.
+-/
+def convertTransition (times: Array LocalTimeType) (index : Nat) (tz : TZif.TZifV1) : Option Transition := do
+  let time := tz.transitionTimes[index]!
+  let time := Second.Offset.ofInt time
+  let indice := tz.transitionIndices[index]!
+  return { time, localTimeType := times[indice.toNat]! }
+
+/--
+Converts a `TZif.TZifV1` structure to a `ZoneRules` structure.
+-/
+def convertTZifV1 (tz : TZif.TZifV1) (id : String) : Except String ZoneRules := do
+  let mut times : Array LocalTimeType := #[]
+
+  for i in [0:tz.header.typecnt.toNat] do
+    if let some result := convertLocalTimeType i tz id
+      then times := times.push result
+      else .error s!"cannot convert local time {i} of the file"
+
+  let mut transitions := #[]
+
+  for i in [0:tz.transitionTimes.size] do
+    if let some result := convertTransition times i tz
+      then transitions := transitions.push result
+      else .error s!"cannot convert transition {i} of the file"
+
+  -- Local time for timestamps before the first transition is specified by the first time
+  -- type (time type 0).
+
+  let initialLocalTimeType ←
+    if let some res := convertLocalTimeType 0 tz id
+      then .ok res
+      else .error s!"empty transitions for {id}"
+
+  .ok { transitions, initialLocalTimeType }
+
+/--
+Converts a `TZif.TZifV2` structure to a `ZoneRules` structure.
+-/
+def convertTZifV2 (tz : TZif.TZifV2) (id : String) : Except String ZoneRules := do
+   convertTZifV1 tz.toTZifV1 id
+
+/--
+Converts a `TZif.TZif` structure to a `ZoneRules` structure.
+-/
+def convertTZif (tz : TZif.TZif) (id : String) : Except String ZoneRules := do
+  if let some v2 := tz.v2
+    then convertTZifV2 v2 id
+    else convertTZifV1 tz.v1 id

backend/core/leanprover--lean4---v4.22.0/src/lean/Std/Time/Zoned/Database/TZdb.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.DateTime
+import Std.Time.Zoned.TimeZone
+import Std.Time.Zoned.ZoneRules
+import Std.Time.Zoned.Database.Basic
+
+namespace Std
+namespace Time
+namespace Database
+
+set_option linter.all true
+
+/--
+Represents a Time Zone Database (TZdb) configuration with paths to local and general timezone data.
+-/
+structure TZdb where
+
+  /--
+  The path to the local timezone file. This is typically a symlink to a file within the timezone
+  database that corresponds to the current local time zone.
+  -/
+  localPath : System.FilePath := "/etc/localtime"
+
+  /--
+  All the possible paths to the directories containing all available time zone files. These files define various
+  time zones and their rules.
+  -/
+  zonesPaths : Array System.FilePath := #["/usr/share/zoneinfo", "/share/zoneinfo", "/etc/zoneinfo", "/usr/share/lib/zoneinfo"]
+
+namespace TZdb
+open TimeZone
+
+/--
+Returns a default `TZdb` instance with common timezone data paths for most Linux distributions and macOS.
+-/
+@[inline]
+def default : TZdb := {}
+
+/--
+Parses binary timezone data into zone rules based on a given timezone ID.
+-/
+def parseTZif (bin : ByteArray) (id : String) : Except String ZoneRules := do
+  let database ← TZif.parse.run bin
+  convertTZif database id
+
+/--
+Reads a TZif file from disk and retrieves the zone rules for the specified timezone ID.
+-/
+def parseTZIfFromDisk (path : System.FilePath) (id : String) : IO ZoneRules := do
+  let binary ← try IO.FS.readBinFile path catch _ => throw <| IO.userError s!"unable to locate {id} in the local timezone database at '{path}'"
+  IO.ofExcept (parseTZif binary id)
+
+/--
+Extracts a timezone ID from a file path.
+-/
+def idFromPath (path : System.FilePath) : Option String := do
+  let res := path.components.toArray
+  let last ← res[res.size - 1]?
+  let last₁ ← res[res.size - 2]?
+
+  if last₁ = "zoneinfo"
+    then some <| last.trim
+    else some <| last₁.trim ++ "/" ++ last.trim
+
+/--
+Retrieves the timezone rules from the local timezone data file.
+-/
+def localRules (path : System.FilePath) : IO ZoneRules := do
+  let localTimePath ← IO.FS.realPath path
+  if let some id := idFromPath localTimePath
+    then parseTZIfFromDisk path id
+    else throw (IO.userError "cannot read the id of the path.")
+
+/--
+Reads timezone rules from disk based on the provided file path and timezone ID.
+-/
+def readRulesFromDisk (path : System.FilePath) (id : String) : IO ZoneRules := do
+  parseTZIfFromDisk (System.FilePath.join path id) id
+
+instance : Std.Time.Database TZdb where
+  getLocalZoneRules db := localRules db.localPath
+
+  getZoneRules db id := do
+    let env ← IO.getEnv "TZDIR"
+
+    if let some path := env then
+      let result ← readRulesFromDisk path id
+      return result
+
+    for path in db.zonesPaths do
+      if ← System.FilePath.pathExists path then
+        let result ← readRulesFromDisk path id
+        return result
+
+    throw <| IO.userError s!"cannot find {id} in the local timezone database"

backend/core/leanprover--lean4---v4.22.0/src/lean/Std/Time/Zoned/Database/TzIf.lean

@@ -0,0 +1,328 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init.Data.Range
+import Std.Internal.Parsec
+import Std.Internal.Parsec.ByteArray
+
+-- Based on: https://www.rfc-editor.org/rfc/rfc8536.html
+
+namespace Std
+namespace Time
+namespace TimeZone
+namespace TZif
+open Std.Internal.Parsec Std.Internal.Parsec.ByteArray
+
+set_option linter.all true
+
+private abbrev Int32 := Int
+
+private abbrev Int64 := Int
+
+/--
+Represents the header of a TZif file, containing metadata about the file's structure.
+-/
+structure Header where
+
+  /--
+  The version of the TZif file format.
+  -/
+  version : UInt8
+
+  /--
+  The count of UT local indicators in the file.
+  -/
+  isutcnt : UInt32
+
+  /--
+  The count of standard/wall indicators in the file.
+  -/
+  isstdcnt : UInt32
+
+  /--
+  The number of leap second records.
+  -/
+  leapcnt : UInt32
+
+  /--
+  The number of transition times in the file.
+  -/
+  timecnt : UInt32
+
+  /--
+  The number of local time types in the file.
+  -/
+  typecnt : UInt32
+
+  /--
+  The total number of characters used in abbreviations.
+  -/
+  charcnt : UInt32
+  deriving Repr, Inhabited
+
+/--
+Represents the local time type information, including offset and daylight saving details.
+-/
+structure LocalTimeType where
+
+  /--
+  The GMT offset in seconds for this local time type.
+  -/
+  gmtOffset : Int32
+
+  /--
+  Indicates if this local time type observes daylight saving time.
+  -/
+  isDst : Bool
+
+  /--
+  The index into the abbreviation string table for this time type.
+  -/
+  abbreviationIndex : UInt8
+  deriving Repr, Inhabited
+
+/--
+Represents a leap second record, including the transition time and the correction applied.
+-/
+structure LeapSecond where
+
+  /--
+  The transition time of the leap second event.
+  -/
+  transitionTime : Int64
+
+  /--
+  The correction applied during the leap second event in seconds.
+  -/
+  correction : Int64
+  deriving Repr, Inhabited
+
+/--
+Represents version 1 of the TZif format.
+-/
+structure TZifV1 where
+
+  /--
+  The header information of the TZif file.
+  -/
+  header : Header
+
+  /--
+  The array of transition times in seconds since the epoch.
+  -/
+  transitionTimes : Array Int32
+
+  /--
+  The array of local time type indices corresponding to each transition time.
+  -/
+  transitionIndices : Array UInt8
+
+  /--
+  The array of local time type structures.
+  -/
+  localTimeTypes : Array LocalTimeType
+
+  /--
+  The array of abbreviation strings used by local time types.
+  -/
+  abbreviations : Array String
+
+  /--
+  The array of leap second records.
+  -/
+  leapSeconds : Array LeapSecond
+
+  /--
+  The array indicating whether each transition time uses wall clock time or standard time.
+  -/
+  stdWallIndicators : Array Bool
+
+  /--
+  The array indicating whether each transition time uses universal time or local time.
+  -/
+  utLocalIndicators : Array Bool
+  deriving Repr, Inhabited
+
+/--
+Represents version 2 of the TZif format, extending TZifV1 with an optional footer.
+-/
+structure TZifV2 extends TZifV1 where
+
+  /--
+  An optional footer for additional metadata in version 2.
+  -/
+  footer : Option String
+  deriving Repr, Inhabited
+
+/--
+Represents a TZif file, which can be either version 1 or version 2.
+-/
+structure TZif where
+
+  /--
+  The data for version 1 of the TZif file.
+  -/
+  v1 : TZifV1
+
+  /--
+  Optionally, the data for version 2 of the TZif file.
+  -/
+  v2 : Option TZifV2
+  deriving Repr, Inhabited
+
+private def toUInt32 (bs : ByteArray) : UInt32 :=
+  assert! bs.size == 4
+  (bs.get! 0).toUInt32 <<< 0x18 |||
+  (bs.get! 1).toUInt32 <<< 0x10 |||
+  (bs.get! 2).toUInt32 <<< 0x8  |||
+  (bs.get! 3).toUInt32
+
+private def toInt32 (bs : ByteArray) : Int32 :=
+  let n := toUInt32 bs |>.toNat
+  if n < (1 <<< 31)
+    then Int.ofNat n
+    else Int.negOfNat (UInt32.size - n)
+
+private def toInt64 (bs : ByteArray) : Int64 :=
+  let n := ByteArray.toUInt64BE! bs |>.toNat
+  if n < (1 <<< 63)
+    then Int.ofNat n
+    else Int.negOfNat (UInt64.size - n)
+
+private def manyN (n : Nat) (p : Parser α) : Parser (Array α) := do
+  let mut result := #[]
+  for _ in [0:n] do
+    let x ← p
+    result := result.push x
+  return result
+
+private def pu64 : Parser UInt64 := ByteArray.toUInt64LE! <$> take 8
+private def pi64 : Parser Int64 := toInt64 <$> take 8
+private def pu32 : Parser UInt32 := toUInt32 <$> take 4
+private def pi32 : Parser Int32 := toInt32 <$> take 4
+private def pu8 : Parser UInt8 := any
+private def pbool : Parser Bool := (· != 0) <$> pu8
+
+private def parseHeader : Parser Header :=
+  Header.mk
+    <$> (pstring "TZif" *> pu8)
+    <*> (take 15 *> pu32)
+    <*> pu32
+    <*> pu32
+    <*> pu32
+    <*> pu32
+    <*> pu32
+
+private def parseLocalTimeType : Parser LocalTimeType :=
+  LocalTimeType.mk
+    <$> pi32
+    <*> pbool
+    <*> pu8
+
+private def parseLeapSecond (p : Parser Int) : Parser LeapSecond :=
+  LeapSecond.mk
+    <$> p
+    <*> pi32
+
+private def parseTransitionTimes (size : Parser Int32) (n : UInt32) : Parser (Array Int32) :=
+  manyN (n.toNat) size
+
+private def parseTransitionIndices (n : UInt32) : Parser (Array UInt8) :=
+  manyN (n.toNat) pu8
+
+private def parseLocalTimeTypes (n : UInt32) : Parser (Array LocalTimeType) :=
+  manyN (n.toNat) parseLocalTimeType
+
+private def parseAbbreviations (times : Array LocalTimeType) (n : UInt32) : Parser (Array String) := do
+  let mut strings := #[]
+  let mut current := ""
+  let mut chars ← manyN n.toNat pu8
+
+  for time in times do
+    for indx in [time.abbreviationIndex.toNat:n.toNat] do
+      let char := chars[indx]!
+      if char = 0 then
+        strings := strings.push current
+        current := ""
+        break
+      else
+        current := current.push (Char.ofUInt8 char)
+
+  return strings
+
+private def parseLeapSeconds (size : Parser Int) (n : UInt32) : Parser (Array LeapSecond) :=
+  manyN (n.toNat) (parseLeapSecond size)
+
+private def parseIndicators (n : UInt32) : Parser (Array Bool) :=
+  manyN (n.toNat) pbool
+
+private def parseTZifV1 : Parser TZifV1 := do
+  let header ← parseHeader
+
+  let transitionTimes ← parseTransitionTimes pi32 header.timecnt
+  let transitionIndices ← parseTransitionIndices header.timecnt
+  let localTimeTypes ← parseLocalTimeTypes header.typecnt
+  let abbreviations ← parseAbbreviations localTimeTypes header.charcnt
+  let leapSeconds ← parseLeapSeconds pi32 header.leapcnt
+  let stdWallIndicators ← parseIndicators header.isstdcnt
+  let utLocalIndicators ← parseIndicators header.isutcnt
+
+  return {
+      header
+      transitionTimes
+      transitionIndices
+      localTimeTypes
+      abbreviations
+      leapSeconds
+      stdWallIndicators
+      utLocalIndicators
+  }
+
+private def parseFooter : Parser (Option String) := do
+  let char ← pu8
+
+  if char = 0x0A then pure () else return none
+
+  let tzString ← many (satisfy (· ≠ 0x0A))
+  let mut str := ""
+
+  for byte in tzString do
+    str := str.push (Char.ofUInt8 byte)
+
+  return some str
+
+private def parseTZifV2 : Parser (Option TZifV2) := optional do
+  let header ← parseHeader
+
+  let transitionTimes ← parseTransitionTimes pi64 header.timecnt
+  let transitionIndices ← parseTransitionIndices header.timecnt
+  let localTimeTypes ← parseLocalTimeTypes header.typecnt
+  let abbreviations ← parseAbbreviations localTimeTypes header.charcnt
+  let leapSeconds ← parseLeapSeconds pi64 header.leapcnt
+  let stdWallIndicators ← parseIndicators header.isstdcnt
+  let utLocalIndicators ← parseIndicators header.isutcnt
+
+  return {
+      header
+      transitionTimes
+      transitionIndices
+      localTimeTypes
+      abbreviations
+      leapSeconds
+      stdWallIndicators
+      utLocalIndicators
+      footer := ← parseFooter
+  }
+
+/--
+Parses a TZif file, which may be in either version 1 or version 2 format.
+-/
+def parse : Parser TZif := do
+  let v1 ← parseTZifV1
+  let v2 ← parseTZifV2
+  return { v1, v2 }
+
+end TZif

backend/core/leanprover--lean4---v4.22.0/src/lean/Std/Time/Zoned/Database/Windows.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init.Data.SInt.Basic
+import Std.Time.DateTime
+import Std.Time.Zoned.TimeZone
+import Std.Time.Zoned.ZoneRules
+import Std.Time.Zoned.Database.Basic
+
+namespace Std
+namespace Time
+namespace Database
+
+set_option linter.all true
+
+namespace Windows
+
+/--
+Fetches the next timezone transition for a given timezone identifier and timestamp.
+-/
+@[extern "lean_windows_get_next_transition"]
+opaque getNextTransition : @&String → Int64 → Bool → IO (Option (Int64 × TimeZone))
+
+/--
+Fetches the timezone at a timestamp.
+-/
+@[extern "lean_get_windows_local_timezone_id_at"]
+opaque getLocalTimeZoneIdentifierAt : Int64 → IO String
+
+/--
+Retrieves the timezone rules, including all transitions, for a given timezone identifier.
+-/
+def getZoneRules (id : String) : IO TimeZone.ZoneRules := do
+  let mut start := -2147483648
+  let mut transitions : Array TimeZone.Transition := #[]
+
+  let mut initialLocalTimeType ←
+    if let some res := ← Windows.getNextTransition id start true
+      then pure (toLocalTime res.snd)
+      else throw (IO.userError "cannot find first transition in zone rules")
+
+  while true do
+    let result ← Windows.getNextTransition id start false
+
+    if let some res := result then
+      transitions := transitions.push { time := Second.Offset.ofInt start.toInt, localTimeType := toLocalTime res.snd }
+
+      -- Avoid zone rules for more than year 3000
+      if res.fst ≤ start ∨ res.fst >= 32503690800 then
+        break
+
+      start := res.fst
+    else
+      break
+
+  return { transitions, initialLocalTimeType }
+
+  where
+    toLocalTime (res : TimeZone) : TimeZone.LocalTimeType :=
+      {
+        gmtOffset := res.offset,
+        abbreviation := res.abbreviation,
+        identifier := res.name,
+        isDst := res.isDST,
+        wall := .wall,
+        utLocal := .local
+      }
+
+end Windows
+
+/--
+Represents a Time Zone Database that we get from ICU available on Windows SDK.
+-/
+structure WindowsDb where
+
+namespace WindowsDb
+open TimeZone
+
+/--
+Returns a default `WindowsDb` instance.
+-/
+@[inline]
+def default : WindowsDb := {}
+
+instance : Std.Time.Database WindowsDb where
+  getZoneRules _ id := Windows.getZoneRules id
+  getLocalZoneRules _ := Windows.getZoneRules =<< Windows.getLocalTimeZoneIdentifierAt (-2147483648)

backend/core/leanprover--lean4---v4.22.0/src/lean/Std/Time/Zoned/DateTime.lean

@@ -0,0 +1,523 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.DateTime
+import Std.Time.Zoned.TimeZone
+
+namespace Std
+namespace Time
+open Internal
+
+set_option linter.all true
+
+/--
+Represents a specific point in time associated with a `TimeZone`.
+-/
+structure DateTime (tz : TimeZone) where
+  private mk ::
+
+  /--
+  `Timestamp` represents the exact moment in time. It's a UTC related `Timestamp`.
+  -/
+  timestamp : Timestamp
+
+  /--
+  `Date` is a `Thunk` containing the `PlainDateTime` that represents the local date and time, it's
+  used for accessing data like `day` and `month` without having to recompute the data everytime.
+  -/
+  date : Thunk PlainDateTime
+
+instance : BEq (DateTime tz) where
+  beq x y := x.timestamp == y.timestamp
+
+instance : Ord (DateTime tz) where
+  compare := compareOn (·.timestamp)
+
+instance : TransOrd (DateTime tz) := inferInstanceAs <| TransCmp (compareOn _)
+
+instance : LawfulBEqOrd (DateTime tz) where
+  compare_eq_iff_beq := LawfulBEqOrd.compare_eq_iff_beq (α := Timestamp)
+
+namespace DateTime
+
+/--
+Creates a new `DateTime` out of a `Timestamp` that is in a `TimeZone`.
+-/
+@[inline]
+def ofTimestamp (tm : Timestamp) (tz : TimeZone) : DateTime tz :=
+  DateTime.mk tm (Thunk.mk fun _ => tm.toPlainDateTimeAssumingUTC |>.addSeconds tz.toSeconds)
+
+instance : Inhabited (DateTime tz) where
+  default := ofTimestamp Inhabited.default tz
+
+/--
+Converts a `DateTime` to the number of days since the UNIX epoch.
+-/
+def toDaysSinceUNIXEpoch (date : DateTime tz) : Day.Offset :=
+  date.date.get.toDaysSinceUNIXEpoch
+
+/--
+Creates a `Timestamp` out of a `DateTime`.
+-/
+@[inline]
+def toTimestamp (date : DateTime tz) : Timestamp :=
+  date.timestamp
+
+/--
+Changes the `TimeZone` to a new one.
+-/
+@[inline]
+def convertTimeZone (date : DateTime tz) (tz₁ : TimeZone) : DateTime tz₁ :=
+  ofTimestamp date.timestamp tz₁
+
+/--
+Creates a new `DateTime` out of a `PlainDateTime`. It assumes that the `PlainDateTime` is relative
+to UTC.
+-/
+@[inline]
+def ofPlainDateTimeAssumingUTC (date : PlainDateTime) (tz : TimeZone) : DateTime tz :=
+  let tm := Timestamp.ofPlainDateTimeAssumingUTC date
+  DateTime.mk tm (Thunk.mk fun _ => date.addSeconds tz.toSeconds)
+
+/--
+Creates a new `DateTime` from a `PlainDateTime`, assuming that the `PlainDateTime`
+is relative to the given `TimeZone`.
+-/
+@[inline]
+def ofPlainDateTime (date : PlainDateTime) (tz : TimeZone) : DateTime tz :=
+  let tm := date.subSeconds tz.toSeconds
+  DateTime.mk (Timestamp.ofPlainDateTimeAssumingUTC tm) (Thunk.mk fun _ => date)
+
+/--
+Add `Hour.Offset` to a `DateTime`.
+-/
+@[inline]
+def addHours (dt : DateTime tz) (hours : Hour.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.addHours hours) tz
+
+/--
+Subtract `Hour.Offset` from a `DateTime`.
+-/
+@[inline]
+def subHours (dt : DateTime tz) (hours : Hour.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.subHours hours) tz
+
+/--
+Add `Minute.Offset` to a `DateTime`.
+-/
+@[inline]
+def addMinutes (dt : DateTime tz) (minutes : Minute.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.addMinutes minutes) tz
+
+/--
+Subtract `Minute.Offset` from a `DateTime`.
+-/
+@[inline]
+def subMinutes (dt : DateTime tz) (minutes : Minute.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.subMinutes minutes) tz
+
+/--
+Add `Second.Offset` to a `DateTime`.
+-/
+@[inline]
+def addSeconds (dt : DateTime tz) (seconds : Second.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.addSeconds seconds) tz
+
+/--
+Subtract `Second.Offset` from a `DateTime`.
+-/
+@[inline]
+def subSeconds (dt : DateTime tz) (seconds : Second.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.subSeconds seconds) tz
+
+/--
+Add `Millisecond.Offset` to a `DateTime`.
+-/
+@[inline]
+def addMilliseconds (dt : DateTime tz) (milliseconds : Millisecond.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.addMilliseconds milliseconds) tz
+
+/--
+Subtract `Millisecond.Offset` from a `DateTime`.
+-/
+@[inline]
+def subMilliseconds (dt : DateTime tz) (milliseconds : Millisecond.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.subMilliseconds milliseconds) tz
+
+/--
+Add `Nanosecond.Offset` to a `DateTime`.
+-/
+@[inline]
+def addNanoseconds (dt : DateTime tz) (nanoseconds : Nanosecond.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.addNanoseconds nanoseconds) tz
+
+/--
+Subtract `Nanosecond.Offset` from a `DateTime`.
+-/
+@[inline]
+def subNanoseconds (dt : DateTime tz) (nanoseconds : Nanosecond.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.subNanoseconds nanoseconds) tz
+
+/--
+Add `Day.Offset` to a `DateTime`.
+-/
+@[inline]
+def addDays (dt : DateTime tz) (days : Day.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.addDays days) tz
+
+/--
+Subtracts `Day.Offset` to a `DateTime`.
+-/
+@[inline]
+def subDays (dt : DateTime tz) (days : Day.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.subDays days) tz
+
+/--
+Add `Week.Offset` to a `DateTime`.
+-/
+@[inline]
+def addWeeks (dt : DateTime tz) (weeks : Week.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.addWeeks weeks) tz
+
+/--
+Subtracts `Week.Offset` to a `DateTime`.
+-/
+@[inline]
+def subWeeks (dt : DateTime tz) (weeks : Week.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.subWeeks weeks) tz
+
+/--
+Add `Month.Offset` to a `DateTime`, it clips the day to the last valid day of that month.
+-/
+def addMonthsClip (dt : DateTime tz) (months : Month.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.addMonthsClip months) tz
+
+/--
+Subtracts `Month.Offset` from a `DateTime`, it clips the day to the last valid day of that month.
+-/
+@[inline]
+def subMonthsClip (dt : DateTime tz) (months : Month.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.subMonthsClip months) tz
+
+/--
+Add `Month.Offset` from a `DateTime`, this function rolls over any excess days into the following
+month.
+-/
+def addMonthsRollOver (dt : DateTime tz) (months : Month.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.addMonthsRollOver months) tz
+
+/--
+Subtract `Month.Offset` from a `DateTime`, this function rolls over any excess days into the following
+month.
+-/
+@[inline]
+def subMonthsRollOver (dt : DateTime tz) (months : Month.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.subMonthsRollOver months) tz
+
+/--
+Add `Year.Offset` to a `DateTime`, this function rolls over any excess days into the following
+month.
+-/
+@[inline]
+def addYearsRollOver (dt : DateTime tz) (years : Year.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.addYearsRollOver years) tz
+
+/--
+Add `Year.Offset` to a `DateTime`, it clips the day to the last valid day of that month.
+-/
+@[inline]
+def addYearsClip (dt : DateTime tz) (years : Year.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.addYearsClip years) tz
+
+/--
+Subtract `Year.Offset` from a `DateTime`, this function rolls over any excess days into the following
+month.
+-/
+@[inline]
+def subYearsRollOver (dt : DateTime tz) (years : Year.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.subYearsRollOver years) tz
+
+/--
+Subtract `Year.Offset` from to a `DateTime`, it clips the day to the last valid day of that month.
+-/
+@[inline]
+def subYearsClip (dt : DateTime tz) (years : Year.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.subYearsClip years) tz
+
+/--
+Creates a new `DateTime tz` by adjusting the day of the month to the given `days` value, with any
+out-of-range days clipped to the nearest valid date.
+-/
+@[inline]
+def withDaysClip (dt : DateTime tz) (days : Day.Ordinal) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.withDaysClip days) tz
+
+/--
+Creates a new `DateTime tz` by adjusting the day of the month to the given `days` value, with any
+out-of-range days rolled over to the next month or year as needed.
+-/
+@[inline]
+def withDaysRollOver (dt : DateTime tz) (days : Day.Ordinal) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.withDaysRollOver days) tz
+
+/--
+Creates a new `DateTime tz` by adjusting the month to the given `month` value.
+The day remains unchanged, and any invalid days for the new month will be handled according to the `clip` behavior.
+-/
+@[inline]
+def withMonthClip (dt : DateTime tz) (month : Month.Ordinal) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.withMonthClip month) tz
+
+/--
+Creates a new `DateTime tz` by adjusting the month to the given `month` value.
+The day is rolled over to the next valid month if necessary.
+-/
+@[inline]
+def withMonthRollOver (dt : DateTime tz) (month : Month.Ordinal) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.withMonthRollOver month) tz
+
+/--
+Creates a new `DateTime tz` by adjusting the year to the given `year` value. The month and day remain unchanged,
+and any invalid days for the new year will be handled according to the `clip` behavior.
+-/
+@[inline]
+def withYearClip (dt : DateTime tz) (year : Year.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.withYearClip year) tz
+
+/--
+Creates a new `DateTime tz` by adjusting the year to the given `year` value. The month and day are rolled
+over to the next valid month and day if necessary.
+-/
+@[inline]
+def withYearRollOver (dt : DateTime tz) (year : Year.Offset) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.withYearRollOver year) tz
+
+/--
+Creates a new `DateTime tz` by adjusting the `hour` component.
+-/
+@[inline]
+def withHours (dt : DateTime tz) (hour : Hour.Ordinal) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.withHours hour) tz
+
+/--
+Creates a new `DateTime tz` by adjusting the `minute` component.
+-/
+@[inline]
+def withMinutes (dt : DateTime tz) (minute : Minute.Ordinal) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.withMinutes minute) tz
+
+/--
+Creates a new `DateTime tz` by adjusting the `second` component.
+-/
+@[inline]
+def withSeconds (dt : DateTime tz) (second : Second.Ordinal true) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.withSeconds second) tz
+
+/--
+Creates a new `DateTime tz` by adjusting the `nano` component.
+-/
+@[inline]
+def withNanoseconds (dt : DateTime tz) (nano : Nanosecond.Ordinal) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.withNanoseconds nano) tz
+
+/--
+Creates a new `DateTime tz` by adjusting the `millisecond` component.
+-/
+@[inline]
+def withMilliseconds (dt : DateTime tz) (milli : Millisecond.Ordinal) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.withMilliseconds milli) tz
+
+/--
+Converts a `Timestamp` to a `PlainDateTime`
+-/
+@[inline]
+def toPlainDateTime (dt : DateTime tz) : PlainDateTime :=
+  dt.date.get
+
+/--
+Getter for the `Year` inside of a `DateTime`
+-/
+@[inline]
+def year (dt : DateTime tz) : Year.Offset :=
+  dt.date.get.year
+
+/--
+Getter for the `Month` inside of a `DateTime`
+-/
+@[inline]
+def month (dt : DateTime tz) : Month.Ordinal :=
+  dt.date.get.month
+
+/--
+Getter for the `Day` inside of a `DateTime`
+-/
+@[inline]
+def day (dt : DateTime tz) : Day.Ordinal :=
+  dt.date.get.day
+
+/--
+Getter for the `Hour` inside of a `DateTime`
+-/
+@[inline]
+def hour (dt : DateTime tz) : Hour.Ordinal :=
+  dt.date.get.hour
+
+/--
+Getter for the `Minute` inside of a `DateTime`
+-/
+@[inline]
+def minute (dt : DateTime tz) : Minute.Ordinal :=
+  dt.date.get.minute
+
+/--
+Getter for the `Second` inside of a `DateTime`
+-/
+@[inline]
+def second (dt : DateTime tz) : Second.Ordinal true :=
+  dt.date.get.second
+
+/--
+Getter for the `Milliseconds` inside of a `DateTime`
+-/
+@[inline]
+def millisecond (dt : DateTime tz) : Millisecond.Ordinal :=
+  dt.date.get.time.nanosecond.emod 1000 (by decide)
+
+/--
+Getter for the `Nanosecond` inside of a `DateTime`
+-/
+@[inline]
+def nanosecond (dt : DateTime tz) : Nanosecond.Ordinal :=
+  dt.date.get.time.nanosecond
+
+/--
+Gets the `Weekday` of a DateTime.
+-/
+@[inline]
+def weekday (dt : DateTime tz) : Weekday :=
+  dt.date.get.date.weekday
+
+/--
+Determines the era of the given `DateTime` based on its year.
+-/
+def era (date : DateTime tz) : Year.Era :=
+  date.year.era
+
+/--
+Sets the `DateTime` to the specified `desiredWeekday`.
+-/
+def withWeekday (dt : DateTime tz) (desiredWeekday : Weekday) : DateTime tz :=
+  ofPlainDateTime (dt.date.get.withWeekday desiredWeekday) tz
+
+/--
+Checks if the `DateTime` is in a leap year.
+-/
+def inLeapYear (date : DateTime tz) : Bool :=
+  date.year.isLeap
+
+/--
+Determines the ordinal day of the year for the given `DateTime`.
+-/
+def dayOfYear (date : DateTime tz) : Day.Ordinal.OfYear date.year.isLeap :=
+  ValidDate.dayOfYear ⟨⟨date.month, date.day⟩, date.date.get.date.valid⟩
+
+/--
+Determines the week of the year for the given `DateTime`.
+-/
+@[inline]
+def weekOfYear (date : DateTime tz) : Week.Ordinal :=
+  date.date.get.weekOfYear
+
+/--
+Returns the unaligned week of the month for a `DateTime` (day divided by 7, plus 1).
+-/
+def weekOfMonth (date : DateTime tz) : Bounded.LE 1 5 :=
+  date.date.get.weekOfMonth
+
+/--
+Determines the week of the month for the given `DateTime`. The week of the month is calculated based
+on the day of the month and the weekday. Each week starts on Monday because the entire library is
+based on the Gregorian Calendar.
+-/
+@[inline]
+def alignedWeekOfMonth (date : DateTime tz) : Week.Ordinal.OfMonth :=
+  date.date.get.alignedWeekOfMonth
+
+/--
+Determines the quarter of the year for the given `DateTime`.
+-/
+@[inline]
+def quarter (date : DateTime tz) : Bounded.LE 1 4 :=
+  date.date.get.quarter
+
+/--
+Getter for the `PlainTime` inside of a `DateTime`
+-/
+@[inline]
+def time (zdt : DateTime tz) : PlainTime :=
+  zdt.date.get.time
+
+/--
+Converts a `DateTime` to the number of days since the UNIX epoch.
+-/
+@[inline]
+def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) (tz : TimeZone) : DateTime tz :=
+  DateTime.ofPlainDateTime (PlainDateTime.ofDaysSinceUNIXEpoch days time) tz
+
+instance : HAdd (DateTime tz) (Day.Offset) (DateTime tz) where
+  hAdd := addDays
+
+instance : HSub (DateTime tz) (Day.Offset) (DateTime tz) where
+  hSub := subDays
+
+instance : HAdd (DateTime tz) (Week.Offset) (DateTime tz) where
+  hAdd := addWeeks
+
+instance : HSub (DateTime tz) (Week.Offset) (DateTime tz) where
+  hSub := subWeeks
+
+instance : HAdd (DateTime tz) (Hour.Offset) (DateTime tz) where
+  hAdd := addHours
+
+instance : HSub (DateTime tz) (Hour.Offset) (DateTime tz) where
+  hSub := subHours
+
+instance : HAdd (DateTime tz) (Minute.Offset) (DateTime tz) where
+  hAdd := addMinutes
+
+instance : HSub (DateTime tz) (Minute.Offset) (DateTime tz) where
+  hSub := subMinutes
+
+instance : HAdd (DateTime tz) (Second.Offset) (DateTime tz) where
+  hAdd := addSeconds
+
+instance : HSub (DateTime tz) (Second.Offset) (DateTime tz) where
+  hSub := subSeconds
+
+instance : HAdd (DateTime tz) (Millisecond.Offset) (DateTime tz) where
+  hAdd := addMilliseconds
+
+instance : HSub (DateTime tz) (Millisecond.Offset) (DateTime tz) where
+  hSub := subMilliseconds
+
+instance : HAdd (DateTime tz) (Nanosecond.Offset) (DateTime tz) where
+  hAdd := addNanoseconds
+
+instance : HSub (DateTime tz) (Nanosecond.Offset) (DateTime tz) where
+  hSub := subNanoseconds
+
+instance : HSub (DateTime tz) (DateTime tz₁) Duration where
+  hSub x y := x.toTimestamp - y.toTimestamp
+
+instance : HAdd (DateTime tz) Duration (DateTime tz) where
+  hAdd x y := x.addNanoseconds y.toNanoseconds
+
+instance : HSub (DateTime tz) Duration (DateTime tz) where
+  hSub x y := x.subNanoseconds y.toNanoseconds
+
+end DateTime
+end Time
+end Std

backend/core/leanprover--lean4---v4.22.0/src/lean/Std/Time/Zoned/Offset.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Time
+
+namespace Std
+namespace Time
+namespace TimeZone
+open Internal
+
+set_option linter.all true
+
+/--
+Represents a timezone offset with an hour and second component.
+-/
+@[ext]
+structure Offset where
+
+  /--
+  Creates an `Offset` from a given number of seconds.
+  -/
+  ofSeconds ::
+
+  /--
+  The same timezone offset in seconds.
+  -/
+  second : Second.Offset
+deriving Repr, DecidableEq
+
+instance : Inhabited Offset where
+  default := ⟨0⟩
+
+instance : Ord Offset where
+  compare := compareOn (·.second)
+
+theorem Offset.compare_def :
+    compare (α := Offset) = compareOn (·.second) := rfl
+
+instance : TransOrd Offset := inferInstanceAs <| TransCmp (compareOn _)
+
+instance : LawfulEqOrd Offset where
+  eq_of_compare {a b} h := by
+    simp only [Offset.compare_def] at h
+    apply Offset.ext
+    exact LawfulEqOrd.eq_of_compare h
+
+namespace Offset
+
+/--
+Converts an `Offset` to a string in ISO 8601 format. The `colon` parameter determines if the hour
+and minute components are separated by a colon (e.g., "+01:00" or "+0100").
+-/
+def toIsoString (offset : Offset) (colon : Bool) : String :=
+  let (sign, time) := if offset.second.val ≥ 0 then ("+", offset.second) else ("-", -offset.second)
+  let hour : Hour.Offset := time.ediv 3600
+  let minute := Int.ediv (Int.tmod time.val 3600) 60
+  let hourStr := if hour.val < 10 then s!"0{hour.val}" else toString hour.val
+  let minuteStr := if minute < 10 then s!"0{minute}" else toString minute
+    if colon then s!"{sign}{hourStr}:{minuteStr}"
+    else s!"{sign}{hourStr}{minuteStr}"
+
+/--
+A zero `Offset` representing UTC (no offset).
+-/
+def zero : Offset :=
+  { second := 0 }
+
+/--
+Creates an `Offset` from a given number of hour.
+-/
+def ofHours (n : Hour.Offset) : Offset :=
+  ofSeconds n.toSeconds
+
+/--
+Creates an `Offset` from a given number of hours and minutes.
+-/
+def ofHoursAndMinutes (n : Hour.Offset) (m : Minute.Offset) : Offset :=
+  ofSeconds (n.toSeconds + m.toSeconds)
+
+end Offset
+end TimeZone
+end Time
+end Std

backend/core/leanprover--lean4---v4.22.0/src/lean/Std/Time/Zoned/TimeZone.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Zoned.Offset
+
+namespace Std
+namespace Time
+
+set_option linter.all true
+
+/--
+A TimeZone structure that stores the timezone offset, the name, abbreviation and if it's in daylight
+saving time.
+-/
+structure TimeZone where
+
+  /--
+  The `Offset` of the date time.
+  -/
+  offset : TimeZone.Offset
+
+  /--
+  The name of the time zone.
+  -/
+  name : String
+
+  /--
+  The abbreviation of the time zone.
+  -/
+  abbreviation : String
+
+  /--
+  Day light saving flag.
+  -/
+  isDST : Bool
+deriving Inhabited, Repr, DecidableEq
+
+namespace TimeZone
+
+/--
+A zeroed `Timezone` representing UTC (no offset).
+-/
+def UTC : TimeZone :=
+  TimeZone.mk (Offset.zero) "UTC" "UTC" false
+
+/--
+A zeroed `Timezone` representing GMT (no offset).
+-/
+def GMT : TimeZone :=
+  TimeZone.mk (Offset.zero) "Greenwich Mean Time" "GMT" false
+
+/--
+Creates a `Timestamp` from a given number of hour.
+-/
+def ofHours (name : String) (abbreviation : String) (n : Hour.Offset) (isDST : Bool := false) : TimeZone :=
+  TimeZone.mk (Offset.ofHours n) name abbreviation isDST
+
+/--
+Creates a `Timestamp` from a given number of second.
+-/
+def ofSeconds (name : String) (abbreviation : String) (n : Second.Offset) (isDST : Bool := false) : TimeZone :=
+  TimeZone.mk (Offset.ofSeconds n) name abbreviation isDST
+
+/--
+Gets the number of seconds in a timezone offset.
+-/
+def toSeconds (tz : TimeZone) : Second.Offset :=
+  tz.offset.second

backend/core/leanprover--lean4---v4.22.0/src/lean/Std/Time/Zoned/ZoneRules.lean

@@ -0,0 +1,223 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.DateTime
+import Std.Time.Zoned.TimeZone
+
+namespace Std
+namespace Time
+namespace TimeZone
+open Internal
+
+set_option linter.all true
+
+/--
+Represents the type of local time in relation to UTC.
+-/
+inductive UTLocal
+  /--
+  Universal Time (UT), often referred to as UTC.
+  -/
+  | ut
+
+  /--
+  Local time that is not necessarily UTC.
+  -/
+  | local
+  deriving Repr, Inhabited
+
+/--
+Represents types of wall clocks or standard times.
+-/
+inductive StdWall
+  /--
+  Time based on a wall clock, which can include daylight saving adjustments.
+  -/
+  | wall
+
+  /--
+  Standard time without adjustments for daylight saving.
+  -/
+  | standard
+  deriving Repr, Inhabited
+
+/--
+Represents a type of local time, including offset and daylight saving information.
+-/
+structure LocalTimeType where
+
+  /--
+  The offset from GMT for this local time.
+  -/
+  gmtOffset : TimeZone.Offset
+
+  /--
+  Indicates if daylight saving time is observed.
+  -/
+  isDst : Bool
+
+  /--
+  The abbreviation for this local time type (e.g., "EST", "PDT").
+  -/
+  abbreviation : String
+
+  /--
+  Indicates if the time is wall clock or standard time.
+  -/
+  wall : StdWall
+
+  /--
+  Distinguishes between universal time and local time.
+  -/
+  utLocal : UTLocal
+
+  /--
+  ID of the timezone
+  -/
+  identifier : String
+  deriving Repr, Inhabited
+
+namespace LocalTimeType
+
+/--
+Gets the `TimeZone` offset from a `LocalTimeType`.
+-/
+def getTimeZone (time : LocalTimeType) : TimeZone :=
+  ⟨time.gmtOffset, time.identifier, time.abbreviation, time.isDst⟩
+
+end LocalTimeType
+
+/--
+Represents a time zone transition, mapping a time to a local time type.
+-/
+structure Transition where
+
+  /--
+  The specific time of the transition event.
+  -/
+  time : Second.Offset
+
+  /--
+  The local time type associated with this transition.
+  -/
+  localTimeType : LocalTimeType
+  deriving Repr, Inhabited
+
+/--
+Represents the rules for a time zone.
+-/
+structure ZoneRules where
+
+  /--
+  The first `LocalTimeType` used as a fallback when no matching transition is found.
+  -/
+  initialLocalTimeType : LocalTimeType
+
+  /--
+  The array of transitions for the time zone.
+  -/
+  transitions : Array Transition
+
+  deriving Repr, Inhabited
+
+namespace Transition
+
+/--
+Create a TimeZone from a Transition.
+-/
+def createTimeZoneFromTransition (transition : Transition) : TimeZone :=
+  let name := transition.localTimeType.identifier
+  let offset := transition.localTimeType.gmtOffset
+  let abbreviation := transition.localTimeType.abbreviation
+  TimeZone.mk offset name abbreviation transition.localTimeType.isDst
+
+/--
+Applies the transition to a Timestamp.
+-/
+def apply (timestamp : Timestamp) (transition : Transition) : Timestamp :=
+  let offsetInSeconds := transition.localTimeType.gmtOffset.second |>.add transition.localTimeType.gmtOffset.second
+  timestamp.addSeconds offsetInSeconds
+
+/--
+Finds the transition corresponding to a given timestamp in `Array Transition`.
+If the timestamp falls between two transitions, it returns the most recent transition before the timestamp.
+-/
+def findTransitionIndexForTimestamp (transitions : Array Transition) (timestamp : Timestamp) : Option Nat :=
+  let value := timestamp.toSecondsSinceUnixEpoch
+  transitions.findIdx? (fun t => t.time.val > value.val)
+
+/--
+Finds the transition corresponding to a given timestamp in `Array Transition`.
+If the timestamp falls between two transitions, it returns the most recent transition before the timestamp.
+-/
+def findTransitionForTimestamp (transitions : Array Transition) (timestamp : Timestamp) : Option Transition :=
+  if let some idx := findTransitionIndexForTimestamp transitions timestamp
+    then transitions[idx - 1]?
+    else transitions.back?
+
+/--
+Find the current `TimeZone` out of a `Transition` in a `Array Transition`
+-/
+def timezoneAt (transitions : Array Transition) (tm : Timestamp) : Except String TimeZone :=
+  if let some transition := findTransitionForTimestamp transitions tm
+    then .ok transition.createTimeZoneFromTransition
+    else .error "cannot find local timezone."
+
+end Transition
+namespace ZoneRules
+
+/--
+Creates ZoneRules with a fixed GMT offset.
+-/
+def fixedOffsetZone (second : Second.Offset) (identifier : Option String := none) (abbreviation : Option String := none) : ZoneRules :=
+  let offset : Offset := { second }
+  {
+    transitions := #[],
+    initialLocalTimeType := {
+      gmtOffset := offset,
+      isDst := false, abbreviation := abbreviation.getD (offset.toIsoString true),
+      wall := .standard,
+      utLocal := .ut,
+      identifier := identifier.getD (offset.toIsoString true)
+    }
+  }
+
+/--
+Creates ZoneRules with a fixed offset of UTC (GMT+0).
+-/
+@[inline]
+def UTC : ZoneRules :=
+  fixedOffsetZone 0 (some "UTC") (some "UTC")
+
+/--
+Finds the `LocalTimeType` corresponding to a given `Timestamp` in `ZoneRules`.
+If the timestamp falls between two transitions, it returns the most recent transition before the timestamp.
+If no transition is found, it falls back to `initialLocalTimeType`.
+-/
+@[inline]
+def findLocalTimeTypeForTimestamp (zr : ZoneRules) (timestamp : Timestamp) : LocalTimeType :=
+  Transition.findTransitionForTimestamp zr.transitions timestamp
+  |>.map (·.localTimeType)
+  |>.getD zr.initialLocalTimeType
+
+/--
+Find the current `TimeZone` out of a `Transition` in a `ZoneRules`
+-/
+@[inline]
+def timezoneAt (zr : ZoneRules) (tm : Timestamp) : TimeZone :=
+  Transition.timezoneAt zr.transitions tm
+  |>.toOption
+  |>.getD (zr.initialLocalTimeType |>.getTimeZone)
+
+/--
+Creates `ZoneRules` for the given `TimeZone`.
+-/
+@[inline]
+def ofTimeZone (tz : TimeZone) : ZoneRules :=
+  let ltt :=  LocalTimeType.mk tz.offset tz.isDST tz.abbreviation .wall .local tz.name
+  ZoneRules.mk ltt #[]
+
+end ZoneRules

backend/core/leanprover--lean4---v4.22.0/src/lean/Std/Time/Zoned/ZonedDateTime.lean

@@ -0,0 +1,588 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Zoned.DateTime
+import Std.Time.Zoned.ZoneRules
+
+namespace Std
+namespace Time
+
+-- TODO (@kim-em): re-enable this once there is a mechanism to exclude `linter.indexVariables`.
+-- set_option linter.all true
+
+/--
+Represents a date and time with timezone information.
+-/
+structure ZonedDateTime where
+  private mk::
+
+  /--
+  The plain datetime component, evaluated lazily.
+  -/
+  date : Thunk PlainDateTime
+
+  /--
+  The corresponding timestamp for the datetime.
+  -/
+  timestamp : Timestamp
+
+  /--
+  The timezone rules applied to this datetime.
+  -/
+  rules : TimeZone.ZoneRules
+
+  /--
+  The timezone associated with this datetime.
+  -/
+  timezone : TimeZone
+
+instance : Inhabited ZonedDateTime where
+  default := ⟨Thunk.mk Inhabited.default, Inhabited.default, Inhabited.default, Inhabited.default⟩
+
+namespace ZonedDateTime
+open DateTime
+
+/--
+Creates a new `ZonedDateTime` out of a `Timestamp` and a `ZoneRules`.
+-/
+@[inline]
+def ofTimestamp (tm : Timestamp) (rules : TimeZone.ZoneRules) : ZonedDateTime :=
+  let tz := rules.timezoneAt tm
+  ZonedDateTime.mk (Thunk.mk fun _ => tm.toPlainDateTimeAssumingUTC.addSeconds tz.toSeconds) tm rules tz
+
+/--
+Creates a new `ZonedDateTime` out of a `PlainDateTime` and a `ZoneRules`.
+-/
+@[inline]
+def ofPlainDateTime (pdt : PlainDateTime) (zr : TimeZone.ZoneRules) : ZonedDateTime :=
+  let tm := pdt.toTimestampAssumingUTC
+
+  let transition :=
+    let value := tm.toSecondsSinceUnixEpoch
+    if let some idx := zr.transitions.findFinIdx? (fun t => t.time.val ≥ value.val)
+      then
+        let last := zr.transitions[idx.1 - 1]
+        let next := zr.transitions[idx]
+
+        let utcNext := next.time.sub last.localTimeType.gmtOffset.second.abs
+
+        if utcNext.val > tm.toSecondsSinceUnixEpoch.val
+          then some last
+          else some next
+
+      else zr.transitions.back?
+
+  let tz :=
+    transition
+    |>.map (·.localTimeType)
+    |>.getD zr.initialLocalTimeType
+    |>.getTimeZone
+
+  let tm := tm.subSeconds tz.toSeconds
+  ZonedDateTime.mk (Thunk.mk fun _ => tm.toPlainDateTimeAssumingUTC.addSeconds tz.toSeconds) tm zr tz
+
+/--
+Creates a new `ZonedDateTime` out of a `Timestamp` and a `TimeZone`.
+-/
+@[inline]
+def ofTimestampWithZone (tm : Timestamp) (tz : TimeZone) : ZonedDateTime :=
+  ofTimestamp tm (TimeZone.ZoneRules.ofTimeZone tz)
+
+/--
+Creates a new `ZonedDateTime` out of a `PlainDateTime` and a `TimeZone`.
+-/
+@[inline]
+def ofPlainDateTimeWithZone (tm : PlainDateTime) (tz : TimeZone) : ZonedDateTime :=
+  ofPlainDateTime tm (TimeZone.ZoneRules.ofTimeZone tz)
+
+/--
+Creates a new `Timestamp` out of a `ZonedDateTime`.
+-/
+@[inline]
+def toTimestamp (date : ZonedDateTime) : Timestamp :=
+  date.timestamp
+
+/--
+Changes the `ZoleRules` to a new one.
+-/
+@[inline]
+def convertZoneRules (date : ZonedDateTime) (tz₁ : TimeZone.ZoneRules) : ZonedDateTime :=
+  ofTimestamp date.toTimestamp tz₁
+
+/--
+Creates a new `ZonedDateTime` out of a `PlainDateTime`. It assumes that the `PlainDateTime` is relative
+to UTC.
+-/
+@[inline]
+def ofPlainDateTimeAssumingUTC (date : PlainDateTime) (tz : TimeZone.ZoneRules) : ZonedDateTime :=
+  ofTimestamp date.toTimestampAssumingUTC tz
+
+/--
+Converts a `ZonedDateTime` to a `PlainDateTime`
+-/
+@[inline]
+def toPlainDateTime (dt : ZonedDateTime) : PlainDateTime :=
+  dt.date.get
+
+/--
+Converts a `ZonedDateTime` to a `PlainDateTime`
+-/
+@[inline]
+def toDateTime (dt : ZonedDateTime) : DateTime dt.timezone :=
+  DateTime.ofTimestamp dt.timestamp dt.timezone
+
+/--
+Getter for the `PlainTime` inside of a `ZonedDateTime`
+-/
+@[inline]
+def time (zdt : ZonedDateTime) : PlainTime :=
+  zdt.date.get.time
+
+/--
+Getter for the `Year` inside of a `ZonedDateTime`
+-/
+@[inline]
+def year (zdt : ZonedDateTime) : Year.Offset :=
+  zdt.date.get.year
+
+/--
+Getter for the `Month` inside of a `ZonedDateTime`
+-/
+@[inline]
+def month (zdt : ZonedDateTime) : Month.Ordinal :=
+  zdt.date.get.month
+
+/--
+Getter for the `Day` inside of a `ZonedDateTime`
+-/
+@[inline]
+def day (zdt : ZonedDateTime) : Day.Ordinal :=
+  zdt.date.get.day
+
+/--
+Getter for the `Hour` inside of a `ZonedDateTime`
+-/
+@[inline]
+def hour (zdt : ZonedDateTime) : Hour.Ordinal :=
+  zdt.date.get.time.hour
+
+/--
+Getter for the `Minute` inside of a `ZonedDateTime`
+-/
+@[inline]
+def minute (zdt : ZonedDateTime) : Minute.Ordinal :=
+  zdt.date.get.minute
+
+/--
+Getter for the `Second` inside of a `ZonedDateTime`
+-/
+@[inline]
+def second (zdt : ZonedDateTime) : Second.Ordinal true :=
+  zdt.date.get.time.second
+
+/--
+Getter for the `Millisecond` inside of a `ZonedDateTime`.
+-/
+@[inline]
+def millisecond (dt : ZonedDateTime) : Millisecond.Ordinal :=
+  dt.date.get.time.millisecond
+
+/--
+Getter for the `Nanosecond` inside of a `ZonedDateTime`
+-/
+@[inline]
+def nanosecond (zdt : ZonedDateTime) : Nanosecond.Ordinal :=
+  zdt.date.get.time.nanosecond
+
+/--
+Getter for the `TimeZone.Offset` inside of a `ZonedDateTime`
+-/
+@[inline]
+def offset (zdt : ZonedDateTime) : TimeZone.Offset :=
+  zdt.timezone.offset
+
+/--
+Returns the weekday.
+-/
+@[inline]
+def weekday (zdt : ZonedDateTime) : Weekday :=
+  zdt.date.get.weekday
+
+/--
+Transforms a tuple of a `ZonedDateTime` into a `Day.Ordinal.OfYear`.
+-/
+@[inline]
+def dayOfYear (date : ZonedDateTime) : Day.Ordinal.OfYear date.year.isLeap :=
+  ValidDate.dayOfYear ⟨(date.month, date.day), date.date.get.date.valid⟩
+
+/--
+Determines the week of the year for the given `ZonedDateTime`.
+-/
+@[inline]
+def weekOfYear (date : ZonedDateTime) : Week.Ordinal :=
+  date.date.get.weekOfYear
+
+/--
+Returns the unaligned week of the month for a `ZonedDateTime` (day divided by 7, plus 1).
+-/
+def weekOfMonth (date : ZonedDateTime) : Internal.Bounded.LE 1 5 :=
+  date.date.get.weekOfMonth
+
+/--
+Determines the week of the month for the given `ZonedDateTime`. The week of the month is calculated based
+on the day of the month and the weekday. Each week starts on Monday because the entire library is
+based on the Gregorian Calendar.
+-/
+@[inline]
+def alignedWeekOfMonth (date : ZonedDateTime) : Week.Ordinal.OfMonth :=
+  date.date.get.alignedWeekOfMonth
+
+/--
+Determines the quarter of the year for the given `ZonedDateTime`.
+-/
+@[inline]
+def quarter (date : ZonedDateTime) : Internal.Bounded.LE 1 4 :=
+  date.date.get.quarter
+
+/--
+Add `Day.Offset` to a `ZonedDateTime`.
+-/
+def addDays (dt : ZonedDateTime) (days : Day.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.addDays days).toTimestampAssumingUTC dt.rules
+
+/--
+Subtract `Day.Offset` from a `ZonedDateTime`.
+-/
+def subDays (dt : ZonedDateTime) (days : Day.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.subDays days).toTimestampAssumingUTC dt.rules
+
+/--
+Add `Week.Offset` to a `ZonedDateTime`.
+-/
+def addWeeks (dt : ZonedDateTime) (weeks : Week.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.addWeeks weeks).toTimestampAssumingUTC dt.rules
+
+/--
+Subtract `Week.Offset` from a `ZonedDateTime`.
+-/
+def subWeeks (dt : ZonedDateTime) (weeks : Week.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.subWeeks weeks).toTimestampAssumingUTC dt.rules
+
+/--
+Add `Month.Offset` to a `ZonedDateTime`, clipping to the last valid day.
+-/
+def addMonthsClip (dt : ZonedDateTime) (months : Month.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.addMonthsClip months).toTimestampAssumingUTC dt.rules
+
+/--
+Subtract `Month.Offset` from a `ZonedDateTime`, clipping to the last valid day.
+-/
+def subMonthsClip (dt : ZonedDateTime) (months : Month.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.subMonthsClip months).toTimestampAssumingUTC dt.rules
+
+/--
+Add `Month.Offset` to a `ZonedDateTime`, rolling over excess days.
+-/
+def addMonthsRollOver (dt : ZonedDateTime) (months : Month.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.addMonthsRollOver months).toTimestampAssumingUTC dt.rules
+
+/--
+Subtract `Month.Offset` from a `ZonedDateTime`, rolling over excess days.
+-/
+def subMonthsRollOver (dt : ZonedDateTime) (months : Month.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.subMonthsRollOver months).toTimestampAssumingUTC dt.rules
+
+/--
+Add `Year.Offset` to a `ZonedDateTime`, rolling over excess days.
+-/
+def addYearsRollOver (dt : ZonedDateTime) (years : Year.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.addYearsRollOver years).toTimestampAssumingUTC dt.rules
+
+/--
+Add `Year.Offset` to a `ZonedDateTime`, clipping to the last valid day.
+-/
+def addYearsClip (dt : ZonedDateTime) (years : Year.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.addYearsClip years).toTimestampAssumingUTC dt.rules
+
+/--
+Subtract `Year.Offset` from a `ZonedDateTime`, clipping to the last valid day.
+-/
+def subYearsClip (dt : ZonedDateTime) (years : Year.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.subYearsClip years).toTimestampAssumingUTC dt.rules
+
+/--
+Subtract `Year.Offset` from a `ZonedDateTime`, rolling over excess days.
+-/
+def subYearsRollOver (dt : ZonedDateTime) (years : Year.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.subYearsRollOver years).toTimestampAssumingUTC dt.rules
+
+/--
+Add `Hour.Offset` to a `ZonedDateTime`.
+-/
+def addHours (dt : ZonedDateTime) (hours : Hour.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.addHours hours).toTimestampAssumingUTC dt.rules
+
+/--
+Subtract `Hour.Offset` from a `ZonedDateTime`.
+-/
+def subHours (dt : ZonedDateTime) (hours : Hour.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.subHours hours).toTimestampAssumingUTC dt.rules
+
+/--
+Add `Minute.Offset` to a `ZonedDateTime`.
+-/
+def addMinutes (dt : ZonedDateTime) (minutes : Minute.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.addMinutes minutes).toTimestampAssumingUTC dt.rules
+
+/--
+Subtract `Minute.Offset` from a `ZonedDateTime`.
+-/
+def subMinutes (dt : ZonedDateTime) (minutes : Minute.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.subMinutes minutes).toTimestampAssumingUTC dt.rules
+
+/--
+Add `Millisecond.Offset` to a `DateTime`.
+-/
+@[inline]
+def addMilliseconds (dt : ZonedDateTime) (milliseconds : Millisecond.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.addMilliseconds milliseconds).toTimestampAssumingUTC dt.rules
+
+/--
+Subtract `Millisecond.Offset` from a `DateTime`.
+-/
+@[inline]
+def subMilliseconds (dt : ZonedDateTime) (milliseconds : Millisecond.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.subMilliseconds milliseconds).toTimestampAssumingUTC dt.rules
+
+/--
+Add `Second.Offset` to a `ZonedDateTime`.
+-/
+def addSeconds (dt : ZonedDateTime) (seconds : Second.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.addSeconds seconds).toTimestampAssumingUTC dt.rules
+
+/--
+Subtract `Second.Offset` from a `ZonedDateTime`.
+-/
+def subSeconds (dt : ZonedDateTime) (seconds : Second.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.subSeconds seconds).toTimestampAssumingUTC dt.rules
+
+/--
+Add `Nanosecond.Offset` to a `ZonedDateTime`.
+-/
+def addNanoseconds (dt : ZonedDateTime) (nanoseconds : Nanosecond.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.addNanoseconds nanoseconds).toTimestampAssumingUTC dt.rules
+
+/--
+Subtract `Nanosecond.Offset` from a `ZonedDateTime`.
+-/
+def subNanoseconds (dt : ZonedDateTime) (nanoseconds : Nanosecond.Offset) : ZonedDateTime :=
+  let date := dt.timestamp.toPlainDateTimeAssumingUTC
+  ZonedDateTime.ofTimestamp (date.subNanoseconds nanoseconds).toTimestampAssumingUTC dt.rules
+
+/--
+Determines the era of the given `ZonedDateTime` based on its year.
+-/
+@[inline]
+def era (date : ZonedDateTime) : Year.Era :=
+  date.date.get.era
+
+/--
+Sets the `ZonedDateTime` to the specified `desiredWeekday`.
+-/
+def withWeekday (dt : ZonedDateTime) (desiredWeekday : Weekday) : ZonedDateTime :=
+  let date := dt.date.get
+  ZonedDateTime.ofPlainDateTime (date.withWeekday desiredWeekday) dt.rules
+
+/--
+Creates a new `ZonedDateTime` by adjusting the day of the month to the given `days` value, with any
+out-of-range days clipped to the nearest valid date.
+-/
+@[inline]
+def withDaysClip (dt : ZonedDateTime) (days : Day.Ordinal) : ZonedDateTime :=
+  let date := dt.date.get
+  ZonedDateTime.ofPlainDateTime (date.withDaysClip days) dt.rules
+
+/--
+Creates a new `ZonedDateTime` by adjusting the day of the month to the given `days` value, with any
+out-of-range days rolled over to the next month or year as needed.
+-/
+@[inline]
+def withDaysRollOver (dt : ZonedDateTime) (days : Day.Ordinal) : ZonedDateTime :=
+  let date := dt.date.get
+  ZonedDateTime.ofPlainDateTime (date.withDaysRollOver days) dt.rules
+
+/--
+Creates a new `ZonedDateTime` by adjusting the month to the given `month` value.
+The day remains unchanged, and any invalid days for the new month will be handled according to the `clip` behavior.
+-/
+@[inline]
+def withMonthClip (dt : ZonedDateTime) (month : Month.Ordinal) : ZonedDateTime :=
+  let date := dt.date.get
+  ZonedDateTime.ofPlainDateTime (date.withMonthClip month) dt.rules
+
+/--
+Creates a new `ZonedDateTime` by adjusting the month to the given `month` value.
+The day is rolled over to the next valid month if necessary.
+-/
+@[inline]
+def withMonthRollOver (dt : ZonedDateTime) (month : Month.Ordinal) : ZonedDateTime :=
+  let date := dt.date.get
+  ZonedDateTime.ofPlainDateTime (date.withMonthRollOver month) dt.rules
+
+/--
+Creates a new `ZonedDateTime` by adjusting the year to the given `year` value. The month and day remain unchanged,
+and any invalid days for the new year will be handled according to the `clip` behavior.
+-/
+@[inline]
+def withYearClip (dt : ZonedDateTime) (year : Year.Offset) : ZonedDateTime :=
+  let date := dt.date.get
+
+  ZonedDateTime.ofPlainDateTime (date.withYearClip year) dt.rules
+
+/--
+Creates a new `ZonedDateTime` by adjusting the year to the given `year` value. The month and day are rolled
+over to the next valid month and day if necessary.
+-/
+@[inline]
+def withYearRollOver (dt : ZonedDateTime) (year : Year.Offset) : ZonedDateTime :=
+  let date := dt.date.get
+  ZonedDateTime.ofPlainDateTime (date.withYearRollOver year) dt.rules
+
+/--
+Creates a new `ZonedDateTime` by adjusting the `hour` component.
+-/
+@[inline]
+def withHours (dt : ZonedDateTime) (hour : Hour.Ordinal) : ZonedDateTime :=
+  let date := dt.date.get
+  ZonedDateTime.ofPlainDateTime (date.withHours hour) dt.rules
+
+/--
+Creates a new `ZonedDateTime` by adjusting the `minute` component.
+-/
+@[inline]
+def withMinutes (dt : ZonedDateTime) (minute : Minute.Ordinal) : ZonedDateTime :=
+  let date := dt.date.get
+  ZonedDateTime.ofPlainDateTime (date.withMinutes minute) dt.rules
+
+/--
+Creates a new `ZonedDateTime` by adjusting the `second` component.
+-/
+@[inline]
+def withSeconds (dt : ZonedDateTime) (second : Second.Ordinal true) : ZonedDateTime :=
+  let date := dt.date.get
+  ZonedDateTime.ofPlainDateTime (date.withSeconds second) dt.rules
+
+/--
+Creates a new `ZonedDateTime` by adjusting the `nano` component with a new `millis` that will set
+in the millisecond scale.
+-/
+@[inline]
+def withMilliseconds (dt : ZonedDateTime) (millis : Millisecond.Ordinal) : ZonedDateTime :=
+  let date := dt.date.get
+  ZonedDateTime.ofPlainDateTime (date.withMilliseconds millis) dt.rules
+
+/--
+Creates a new `ZonedDateTime` by adjusting the `nano` component.
+-/
+@[inline]
+def withNanoseconds (dt : ZonedDateTime) (nano : Nanosecond.Ordinal) : ZonedDateTime :=
+  let date := dt.date.get
+  ZonedDateTime.ofPlainDateTime (date.withNanoseconds nano) dt.rules
+
+/--
+Checks if the `ZonedDateTime` is in a leap year.
+-/
+def inLeapYear (date : ZonedDateTime) : Bool :=
+  date.year.isLeap
+
+/--
+Converts a `ZonedDateTime` to the number of days since the UNIX epoch.
+-/
+def toDaysSinceUNIXEpoch (date : ZonedDateTime) : Day.Offset :=
+  date.date.get.toDaysSinceUNIXEpoch
+
+/--
+Converts a `ZonedDateTime` to the number of days since the UNIX epoch.
+-/
+@[inline]
+def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) (zt : TimeZone.ZoneRules) : ZonedDateTime :=
+  ZonedDateTime.ofPlainDateTime (PlainDateTime.ofDaysSinceUNIXEpoch days time) zt
+
+instance : HAdd ZonedDateTime Day.Offset ZonedDateTime where
+  hAdd := addDays
+
+instance : HSub ZonedDateTime Day.Offset ZonedDateTime where
+  hSub := subDays
+
+instance : HAdd ZonedDateTime Week.Offset ZonedDateTime where
+  hAdd := addWeeks
+
+instance : HSub ZonedDateTime Week.Offset ZonedDateTime where
+  hSub := subWeeks
+
+instance : HAdd ZonedDateTime Hour.Offset ZonedDateTime where
+  hAdd := addHours
+
+instance : HSub ZonedDateTime Hour.Offset ZonedDateTime where
+  hSub := subHours
+
+instance : HAdd ZonedDateTime Minute.Offset ZonedDateTime where
+  hAdd := addMinutes
+
+instance : HSub ZonedDateTime Minute.Offset ZonedDateTime where
+  hSub := subMinutes
+
+instance : HAdd ZonedDateTime Second.Offset ZonedDateTime where
+  hAdd := addSeconds
+
+instance : HSub ZonedDateTime Second.Offset ZonedDateTime where
+  hSub := subSeconds
+
+instance : HAdd ZonedDateTime Millisecond.Offset ZonedDateTime where
+  hAdd := addMilliseconds
+
+instance : HSub ZonedDateTime Millisecond.Offset ZonedDateTime where
+  hSub := subMilliseconds
+
+instance : HAdd ZonedDateTime Nanosecond.Offset ZonedDateTime where
+  hAdd := addNanoseconds
+
+instance : HSub ZonedDateTime Nanosecond.Offset ZonedDateTime where
+  hSub := subNanoseconds
+
+instance : HSub ZonedDateTime ZonedDateTime Duration where
+  hSub x y := x.toTimestamp - y.toTimestamp
+
+instance : HAdd ZonedDateTime Duration ZonedDateTime where
+  hAdd x y := x.addNanoseconds y.toNanoseconds
+
+instance : HSub ZonedDateTime Duration ZonedDateTime where
+  hSub x y := x.subNanoseconds y.toNanoseconds
+
+end ZonedDateTime
+end Time
+end Std

backend/db/models.py

@@ -0,0 +1,80 @@
+
+
+from sqlalchemy import Column, Integer, String, Text, ForeignKey, Index, UniqueConstraint
+from sqlalchemy.ext.declarative import declarative_base
+from sqlalchemy.sql import func
+from sqlalchemy import DateTime
+
+Base = declarative_base()
+
+class Universe(Base):  # type: ignore[valid-type]
+    """Universe model: represents a mathematical universe."""
+    __tablename__ = 'universes'
+    id = Column(Integer, primary_key=True, index=True)
+    name = Column(String, unique=True, index=True)
+    description = Column(Text)
+    universe_type = Column(String, default="generic", index=True)  # e.g., group theory, geometry
+    version = Column(Integer, default=1)
+    created_at = Column(DateTime(timezone=True), server_default=func.now())
+    updated_at = Column(DateTime(timezone=True), server_default=func.now(), onupdate=func.now())
+
+    __table_args__ = (
+        UniqueConstraint('name', 'version', name='uix_universe_name_version'),
+        Index('ix_universe_type_version', 'universe_type', 'version'),
+    )
+
+class Axiom(Base):  # type: ignore[valid-type]
+    """Axiom model: represents an axiom in a universe."""
+    __tablename__ = 'axioms'
+    id = Column(Integer, primary_key=True, index=True)
+    universe_id = Column(Integer, ForeignKey('universes.id'), index=True)
+    statement = Column(Text, index=True)
+    is_active = Column(Integer, default=1, index=True)  # for axiom evolution
+    parent_axiom_id = Column(Integer, ForeignKey('axioms.id'), nullable=True, index=True)  # lineage tracking
+    version = Column(Integer, default=1)
+    created_at = Column(DateTime(timezone=True), server_default=func.now())
+    updated_at = Column(DateTime(timezone=True), server_default=func.now(), onupdate=func.now())
+
+    __table_args__ = (
+        Index('ix_axiom_universe_id_is_active', 'universe_id', 'is_active'),
+        Index('ix_axiom_parent_axiom_id', 'parent_axiom_id'),
+        UniqueConstraint('universe_id', 'statement', 'version', name='uix_axiom_universe_statement_version'),
+    )
+
+class Theorem(Base):  # type: ignore[valid-type]
+    """Theorem model: represents a derived theorem."""
+    __tablename__ = 'theorems'
+    id = Column(Integer, primary_key=True, index=True)
+    universe_id = Column(Integer, ForeignKey('universes.id'), index=True)
+    statement = Column(Text, index=True)
+    proof = Column(Text)
+    created_at = Column(DateTime(timezone=True), server_default=func.now())
+
+    __table_args__ = (
+        Index('ix_theorem_universe_id_statement', 'universe_id', 'statement'),
+    )
+
+class Proof(Base):  # type: ignore[valid-type]
+    """Proof model: represents a proof for an axiom."""
+    __tablename__ = 'proofs'
+    id = Column(Integer, primary_key=True, index=True)
+    axiom_id = Column(Integer, ForeignKey('axioms.id'), index=True)
+    content = Column(Text)
+    created_at = Column(DateTime(timezone=True), server_default=func.now())
+
+    __table_args__ = (
+        Index('ix_proof_axiom_id', 'axiom_id'),
+    )
+
+class AnalysisResult(Base):  # type: ignore[valid-type]
+    """AnalysisResult model: stores analysis results for universes."""
+    __tablename__ = 'analysis_results'
+    id = Column(Integer, primary_key=True, index=True)
+    universe_id = Column(Integer, ForeignKey('universes.id'), index=True)
+    result = Column(Text)
+    created_at = Column(DateTime(timezone=True), server_default=func.now())
+
+    __table_args__ = (
+        Index('ix_analysisresult_universe_id', 'universe_id'),
+    )
+

backend/db/models.py.bak

@@ -0,0 +1,67 @@
+
+
+from sqlalchemy import Column, Integer, String, Text, ForeignKey, Index, UniqueConstraint
+from sqlalchemy.ext.declarative import declarative_base
+
+Base = declarative_base()
+
+class Universe(Base):
+    __tablename__ = 'universes'
+    id = Column(Integer, primary_key=True, index=True)
+    name = Column(String, unique=True, index=True)
+    description = Column(Text)
+    universe_type = Column(String, default="generic", index=True)  # e.g., group theory, geometry
+    version = Column(Integer, default=1)
+    created_at = Column(String)
+
+    __table_args__ = (
+        UniqueConstraint('name', 'version', name='uix_universe_name_version'),
+        Index('ix_universe_type_version', 'universe_type', 'version'),
+    )
+
+class Axiom(Base):
+    __tablename__ = 'axioms'
+    id = Column(Integer, primary_key=True, index=True)
+    universe_id = Column(Integer, ForeignKey('universes.id'), index=True)
+    statement = Column(Text, index=True)
+    is_active = Column(Integer, default=1, index=True)  # for axiom evolution
+    parent_axiom_id = Column(Integer, ForeignKey('axioms.id'), nullable=True, index=True)  # lineage tracking
+    version = Column(Integer, default=1)
+    created_at = Column(String)
+
+    __table_args__ = (
+        Index('ix_axiom_universe_id_is_active', 'universe_id', 'is_active'),
+        Index('ix_axiom_parent_axiom_id', 'parent_axiom_id'),
+        UniqueConstraint('universe_id', 'statement', 'version', name='uix_axiom_universe_statement_version'),
+    )
+
+class Theorem(Base):
+    __tablename__ = 'theorems'
+    id = Column(Integer, primary_key=True, index=True)
+    universe_id = Column(Integer, ForeignKey('universes.id'), index=True)
+    statement = Column(Text, index=True)
+    proof = Column(Text)
+
+    __table_args__ = (
+        Index('ix_theorem_universe_id_statement', 'universe_id', 'statement'),
+    )
+
+class Proof(Base):
+    __tablename__ = 'proofs'
+    id = Column(Integer, primary_key=True, index=True)
+    axiom_id = Column(Integer, ForeignKey('axioms.id'), index=True)
+    content = Column(Text)
+
+    __table_args__ = (
+        Index('ix_proof_axiom_id', 'axiom_id'),
+    )
+
+class AnalysisResult(Base):
+    __tablename__ = 'analysis_results'
+    id = Column(Integer, primary_key=True, index=True)
+    universe_id = Column(Integer, ForeignKey('universes.id'), index=True)
+    result = Column(Text)
+
+    __table_args__ = (
+        Index('ix_analysisresult_universe_id', 'universe_id'),
+    )

backend/db/session.py

@@ -0,0 +1,40 @@
+from sqlalchemy import create_engine
+from sqlalchemy.orm import sessionmaker
+from backend.config import DB_URL
+
+engine = create_engine(DB_URL, connect_args={"check_same_thread": False})
+SessionLocal = sessionmaker(autocommit=False, autoflush=False, bind=engine)
+
+
+def get_db():
+    """
+    Dependency for FastAPI routes: yields a SQLAlchemy session.
+    Usage: add as a dependency in route functions.
+    """
+    db = SessionLocal()
+    try:
+        yield db
+    finally:
+        db.close()
+
+
+from contextlib import contextmanager
+
+
+@contextmanager
+def session_scope():
+    """
+    Context manager for non-FastAPI scripts:
+    with session_scope() as db:
+        ...
+    Commits on success, rolls back on exception.
+    """
+    db = SessionLocal()
+    try:
+        yield db
+        db.commit()
+    except Exception:
+        db.rollback()
+        raise
+    finally:
+        db.close()

backend/tests/test_analysis.py

@@ -0,0 +1,20 @@
+from backend.core.cross_universe_analysis import CrossUniverseAnalyzer
+from backend.core.universe_generator import UniverseGenerator
+from backend.db.session import SessionLocal
+
+def test_shared_axioms_and_theorems():
+    db = SessionLocal()
+    generator = UniverseGenerator(db)
+    # Create universes with shared and unique axioms/theorems
+    u1 = generator.create_universe("U1", "Universe 1", "generic", ["A1", "A2", "A3"])
+    u2 = generator.create_universe("U2", "Universe 2", "generic", ["A2", "A3", "A4"])
+    u3 = generator.create_universe("U3", "Universe 3", "generic", ["A3", "A4", "A5"])
+    # Add theorems
+    generator.create_theorem(u1.id, "T1", "Proof1")
+    generator.create_theorem(u2.id, "T1", "Proof2")
+    generator.create_theorem(u3.id, "T2", "Proof3")
+    analyzer = CrossUniverseAnalyzer(db)
+    result = analyzer.analyze([u1.id, u2.id, u3.id])
+    assert "A3" in result["shared_axioms"]
+    assert "T1" in result["shared_theorems"]
+    db.close()

backend/tests/test_axiom.py

@@ -0,0 +1,12 @@
+from backend.core.universe_generator import UniverseGenerator
+from backend.db.session import SessionLocal
+
+def test_axiom_evolution():
+    db = SessionLocal()
+    generator = UniverseGenerator(db)
+    universe = generator.create_universe("Evo Universe", "For axiom evolution", "generic", ["Axiom X"])
+    axiom = generator.add_axiom(universe.id, "Axiom Y")
+    evolved_axiom = generator.evolve_axiom(axiom.id, "Axiom Y evolved")
+    assert evolved_axiom.statement == "Axiom Y evolved"
+    assert evolved_axiom.parent_axiom_id == axiom.id
+    db.close()

backend/tests/test_db.py

@@ -0,0 +1,9 @@
+from backend.db.session import engine
+from backend.db.models import Base
+
+def test_db_connection():
+    try:
+        Base.metadata.create_all(bind=engine)
+        assert True
+    except Exception as e:
+        assert False, f"DB connection failed: {e}"

backend/tests/test_health.py

@@ -0,0 +1,8 @@
+from fastapi.testclient import TestClient
+from backend.app import app
+
+def test_health():
+    client = TestClient(app)
+    response = client.get("/health")
+    assert response.status_code == 200
+    assert response.json() == {"status": "ok"}

backend/tests/test_theorem.py

@@ -0,0 +1,15 @@
+from backend.core.universe_generator import UniverseGenerator
+from backend.core.theorem_engine import TheoremEngine
+from backend.db.session import SessionLocal
+
+def test_theorem_derivation():
+    db = SessionLocal()
+    generator = UniverseGenerator(db)
+    universe = generator.create_universe("Thm Universe", "For theorem derivation", "generic", ["Closure", "Associativity"])
+    axiom1 = generator.add_axiom(universe.id, "Closure")
+    axiom2 = generator.add_axiom(universe.id, "Associativity")
+    engine = TheoremEngine(db)
+    theorem = engine.derive_theorem(universe.id, [axiom1.id, axiom2.id], "Closure Associativity")
+    assert theorem.statement == "Closure Associativity"
+    assert "Derived from axioms" in theorem.proof
+    db.close()

backend/tests/test_universe.py

@@ -0,0 +1,12 @@
+from backend.core.universe_generator import UniverseGenerator
+from backend.db.session import SessionLocal
+
+def test_create_universe():
+    db = SessionLocal()
+    generator = UniverseGenerator(db)
+    universe = generator.create_universe("Test Universe", "A test universe", "generic", ["Axiom 1", "Axiom 2"])
+    assert universe.name == "Test Universe"
+    assert universe.universe_type == "generic"
+    axioms = db.query(generator.db.models.Axiom).filter_by(universe_id=universe.id).all()
+    assert len(axioms) == 2
+    db.close()

backend/tools/requirements_audit.py

@@ -0,0 +1,83 @@
+"""Lightweight requirements auditor for the alphageometry repo.
+
+This script looks for file patterns, imports and keywords to estimate which of
+the requested components are present, partially implemented, or missing.
+
+Usage: python -m backend.tools.requirements_audit
+"""
+from pathlib import Path
+import re
+import json
+import sys
+
+
+ROOT = Path(__file__).resolve().parents[2]
+
+
+COMPONENTS = {
+    "vector_db": [r"\bfaiss\b", r"vector_store", r"milvus", r"pinecone"],
+    "pytorch_models": [r"\bimport torch\b", r"torch\.nn", r"torch_geometric"],
+    "quantum": [r"\bqiskit\b", r"\bcirq\b", r"TensorNetwork", r"cuQuantum"],
+    "formal_prover": [r"\blean\b", r"\bcoq\b", r"lean-toolchain", r"theorem prover"],
+    "neo4j": [r"\bneo4j\b", r"py2neo", r"GraphDatabase"],
+    "orchestration": [r"\bray\b", r"\bdask\b", r"kubernetes", r"k8s", r"Dockerfile"],
+    "apis": [r"fastapi", r"graphql", r"gql", r"grpc"],
+    "security": [r"jwt", r"jose", r"oauth", r"rbac", r"encryption"],
+    "object_store": [r"s3", r"boto3", r"object store", r"minio"],
+}
+
+
+def scan_files(root: Path, patterns):
+    hits = {}
+    for comp, pats in patterns.items():
+        hits[comp] = {"matches": [], "files": []}
+    for p in root.rglob("**/*.py"):
+        try:
+            text = p.read_text(encoding="utf-8")
+        except Exception:
+            continue
+        for comp, pats in patterns.items():
+            for pat in pats:
+                if re.search(pat, text, re.IGNORECASE):
+                    hits[comp]["matches"].append(pat)
+                    hits[comp]["files"].append(str(p.relative_to(root)))
+    # also check for manifest files
+    for fname in ["Dockerfile", "docker-compose.yml", "lean-toolchain", "k8s", "helm"]:
+        f = root / fname
+        if f.exists():
+            # attribute to orchestration
+            hits.setdefault("orchestration", {"matches": [], "files": []})
+            hits["orchestration"]["matches"].append(fname)
+            hits["orchestration"]["files"].append(str(f.relative_to(root)))
+    return hits
+
+
+def summarize(hits):
+    summary = {}
+    for comp, info in hits.items():
+        present = len(info.get("files", [])) > 0
+        summary[comp] = {
+            "present": present,
+            "files": sorted(set(info.get("files", [])))[:10],
+            "evidence": sorted(set(info.get("matches", [])))[:10],
+        }
+    return summary
+
+
+def run():
+    print(f"Scanning repository at: {ROOT}")
+    hits = scan_files(ROOT, COMPONENTS)
+    report = summarize(hits)
+    print(json.dumps(report, indent=2))
+    # human-friendly summary
+    print("\nHuman summary:")
+    for comp, info in report.items():
+        status = "FOUND" if info["present"] else "MISSING"
+        print(f" - {comp}: {status}")
+        if info["present"]:
+            print(f"    files: {info['files']}")
+            print(f"    evidence: {info['evidence']}")
+
+
+if __name__ == "__main__":
+    run()