module

public import Mathlib

/-!
# Session oracle for a stock token

A quote carries a price, a time that may be absent and a halt flag that is
true, false or absent. Together with the token's pause flag (true, false or
absent), the trading session (open or held), the current instant and a
freshness allowance, the oracle returns a verdict.
-/

@[expose] public section

namespace EquityOracle

/-- The issuer's quote: a price, an optional time stamp, an optional halt flag. -/
structure Quote where
  price : ℚ
  time : Option ℤ
  halt : Option Bool

/-- The trading session state. -/
inductive Session where
  | isOpen
  | held
  deriving DecidableEq, Repr

/-- The oracle's verdict. -/
inductive Verdict where
  | halted
  | paused
  | unknown
  | held
  | stale
  | isOpen
  deriving DecidableEq, Repr

/-- The verdict, evaluated in the order: halt flag true → halted; pause flag true → paused;
halt flag or time absent → unknown; session held → held; age above allowance → stale;
otherwise open. -/
def verdict (q : Quote) (pause : Option Bool) (s : Session) (now allowance : ℤ) : Verdict :=
  if q.halt = some true then .halted
  else if pause = some true then .paused
  else match q.halt, q.time with
    | none, _ => .unknown
    | _, none => .unknown
    | some _, some t =>
      match s with
      | .held => .held
      | .isOpen => if now - t > allowance then .stale else .isOpen

/-- Main theorem.
1. The verdict is open only when the halt flag is `false`, the time is present (say `t`),
   the pause flag is not `true`, the session is open and the age `now - t` is within the
   allowance.
2. A `true` halt flag yields `halted`, whatever the rest.
3. An absent halt flag never yields `open`; it yields `unknown` unless the pause flag is
   `true` (in which case the specified evaluation order gives `paused`). -/
theorem verdict_open_only_when_clear :
    (∀ (q : Quote) (pause : Option Bool) (s : Session) (now allowance : ℤ),
      verdict q pause s now allowance = .isOpen →
        q.halt = some false ∧ (∃ t, q.time = some t ∧ now - t ≤ allowance) ∧
        pause ≠ some true ∧ s = .isOpen) ∧
    (∀ (q : Quote) (pause : Option Bool) (s : Session) (now allowance : ℤ),
      q.halt = some true → verdict q pause s now allowance = .halted) ∧
    (∀ (q : Quote) (pause : Option Bool) (s : Session) (now allowance : ℤ),
      q.halt = none → verdict q pause s now allowance ≠ .isOpen ∧
        (pause ≠ some true → verdict q pause s now allowance = .unknown)) := by
  refine ⟨?_, ?_, ?_⟩
  · rintro ⟨p, time, halt⟩ pause s now allowance h
    simp only [verdict] at h
    rcases halt with _ | _ | _ <;> rcases time with _ | t <;>
      rcases pause with _ | _ | _ <;> cases s <;> simp_all
  · rintro ⟨p, time, halt⟩ pause s now allowance h
    simp_all [verdict]
  · rintro ⟨p, time, halt⟩ pause s now allowance h
    simp only at h
    subst h
    rcases pause with _ | _ | _ <;> simp [verdict]

/-- Converse: when all conditions hold, the verdict is indeed open. -/
theorem verdict_open_of_clear (q : Quote) (pause : Option Bool) (now allowance t : ℤ)
    (hh : q.halt = some false) (ht : q.time = some t) (hp : pause ≠ some true)
    (hage : now - t ≤ allowance) :
    verdict q pause .isOpen now allowance = .isOpen := by
  rcases q with ⟨p, time, halt⟩
  simp only at hh ht
  subst hh ht
  simp [verdict, hp, not_lt.mpr hage]

end EquityOracle

end