import Wanderbooks.Closing

/-!
# The ledger as a state machine

The engine's command surface (`Ledger`), modelled as the steps it allows:
add an account, start a draft, post, reverse, open a period, close one.
Each step carries the checks the engine makes before it mutates. The
theorems below hold in *every* state reachable from empty books, by any
sequence of commands, of any length.

Mirrors `Ledger::add_account`, `try_create_entry`, `post_entry`,
`reverse_entry`, `create_period`, and `close_period_to`.
-/

namespace Wanderbooks

/-- A journal entry: its id, its date (a day number), its lines. -/
structure Entry where
  id : Nat
  date : Nat
  lines : List Line
  deriving DecidableEq

/-- Every line of some entries, in order. -/
def allLines : List Entry → List Line
  | [] => []
  | e :: es => e.lines ++ allLines es

theorem allLines_append (xs ys : List Entry) : allLines (xs ++ ys) = allLines xs ++ allLines ys := by
  induction xs with
  | nil => rfl
  | cons x xs ih => simp [allLines, ih]

theorem mem_allLines {l : Line} {es : List Entry} : l ∈ allLines es ↔ ∃ e ∈ es, l ∈ e.lines := by
  induction es with
  | nil => simp [allLines]
  | cons e es ih => simp [allLines, ih]

/-- **Any collection of balanced entries nets to zero**: all of them, those
dated through some day, those in some period, any filter at all. -/
theorem net_allLines (es : List Entry) (h : ∀ e ∈ es, net e.lines = 0) : net (allLines es) = 0 := by
  induction es with
  | nil => rfl
  | cons e es ih =>
    simp only [allLines, net_append, h e (by simp), ih (fun x hx => h x (by simp [hx]))]
    rfl

/-- An accounting period: inclusive day range, open or closed. -/
structure Period where
  id : Nat
  start : Nat
  stop : Nat
  closed : Bool
  deriving DecidableEq

/-- Whether a day falls in a period. -/
def Period.contains (p : Period) (d : Nat) : Bool := decide (p.start ≤ d ∧ d ≤ p.stop)

/-- The books: chart, posted entries in posting order, drafts, periods. -/
structure Ledger where
  chart : Chart
  posted : List Entry
  drafts : List Entry
  periods : List Period

/-- Empty books. -/
def Ledger.empty : Ledger := ⟨[], [], [], []⟩

/-- Whether a closed period contains a day. -/
def Ledger.closedOn (L : Ledger) (d : Nat) : Prop :=
  ∃ p ∈ L.periods, p.closed = true ∧ p.contains d = true

/-- Entries dated on or before a day. -/
def through (d : Nat) (es : List Entry) : List Entry := es.filter (fun e => decide (e.date ≤ d))

/-- Mark one period closed. -/
def closeIn (p : Period) (ps : List Period) : List Period :=
  ps.map (fun q => if q = p then { q with closed := true } else q)

/-- The closing entry for period `p` crediting targets `ts`, if there is
anything to close. -/
def closingFor (L : Ledger) (p : Period) (ts : List (Nat × Int)) (id : Nat) : List Entry :=
  if closings (nominalCodes L.chart) (allLines (through p.stop L.posted)) = [] then []
  else [⟨id, p.stop, closingEntry (nominalCodes L.chart) ts (allLines (through p.stop L.posted))⟩]

/-- What the engine allows. -/
inductive Step : Ledger → Ledger → Prop
  /-- `add_account`: codes are unique. -/
  | addAccount (L : Ledger) (a : Nat) (t : AccountType) (h : a ∉ codes L.chart) :
      Step L { L with chart := (a, t) :: L.chart }
  /-- `try_create_entry` (and lines added to it): not in a closed period. -/
  | draft (L : Ledger) (e : Entry) (h : ¬ L.closedOn e.date) :
      Step L { L with drafts := e :: L.drafts }
  /-- `post_entry`: a draft, acceptable, on known accounts, not in a closed
  period. Appends to the log. -/
  | post (L : Ledger) (e : Entry) (hd : e ∈ L.drafts) (ha : Accepted e.lines)
      (hk : ∀ l ∈ e.lines, l.account ∈ codes L.chart) (hc : ¬ L.closedOn e.date) :
      Step L { L with posted := L.posted ++ [e], drafts := L.drafts.filter (· ≠ e) }
  /-- `reverse_entry`: a posted entry's lines, sides flipped, posted on a
  day not in a closed period. -/
  | reverse (L : Ledger) (e : Entry) (he : e ∈ L.posted) (r : Entry)
      (hr : r.lines = reversal e.lines) (hc : ¬ L.closedOn r.date) :
      Step L { L with posted := L.posted ++ [r] }
  /-- `create_period`: periods open. -/
  | openPeriod (L : Ledger) (p : Period) (h : p.closed = false) :
      Step L { L with periods := p :: L.periods }
  /-- `close_period_to`: an open period with no drafts in it, whose last day
  is in no other closed period, with no later period closed, crediting the
  net income to equity targets (not themselves revenue or expense) in
  parts that sum to it. -/
  | close (L : Ledger) (p : Period) (hp : p ∈ L.periods) (hopen : p.closed = false)
      (hdrafts : ∀ d ∈ L.drafts, p.contains d.date = false)
      (hother : ∀ q ∈ L.periods, q.closed = true → q.contains p.stop = false)
      (hlater : ∀ q ∈ L.periods, q.closed = true → q.stop ≤ p.stop)
      (ts : List (Nat × Int))
      (hts : ∀ x ∈ ts, x.1 ∈ codes L.chart ∧ x.1 ∉ nominalCodes L.chart)
      (hsum : total (ts.map Prod.snd)
        = net (closings (nominalCodes L.chart) (allLines (through p.stop L.posted))))
      (id : Nat) :
      Step L { L with posted := L.posted ++ closingFor L p ts id, periods := closeIn p L.periods }

/-- States reachable from empty books. -/
inductive Reachable : Ledger → Prop
  | empty : Reachable Ledger.empty
  | step {L L' : Ledger} : Reachable L → Step L L' → Reachable L'

/-- What holds in every reachable state. -/
structure Inv (L : Ledger) : Prop where
  distinct : Distinct (codes L.chart)
  accepted : ∀ e ∈ L.posted, Accepted e.lines
  known : ∀ e ∈ L.posted, ∀ l ∈ e.lines, l.account ∈ codes L.chart
  draftsOpen : ∀ d ∈ L.drafts, ¬ L.closedOn d.date

theorem closedOn_closeIn (L : Ledger) (p : Period) (d : Nat) :
    ({ L with periods := closeIn p L.periods } : Ledger).closedOn d →
      L.closedOn d ∨ (p ∈ L.periods ∧ p.contains d = true) := by
  rintro ⟨q, hq, hc, hd⟩
  simp only [closeIn, List.mem_map] at hq
  obtain ⟨q', hq', rfl⟩ := hq
  by_cases e : q' = p
  · subst e; right; simp at hd; exact ⟨hq', by simpa [Period.contains] using hd⟩
  · left; simp [e] at hc hd; exact ⟨q', hq', hc, hd⟩

theorem closingFor_lines (L : Ledger) (p : Period) (ts : List (Nat × Int)) (id : Nat) :
    ∀ e ∈ closingFor L p ts id,
      e.date = p.stop ∧ e.lines = closingEntry (nominalCodes L.chart) ts
        (allLines (through p.stop L.posted))
      ∧ closings (nominalCodes L.chart) (allLines (through p.stop L.posted)) ≠ [] := by
  intro e he
  unfold closingFor at he
  split at he
  · simp at he
  · simp at he; subst he; exact ⟨rfl, rfl, by assumption⟩

/-- **Every step preserves the invariant.** -/
theorem Step.inv {L L' : Ledger} (s : Step L L') (h : Inv L) : Inv L' := by
  cases s with
  | addAccount a t ha =>
    exact ⟨⟨ha, h.distinct⟩, h.accepted,
      fun e he l hl => List.mem_cons_of_mem _ (h.known e he l hl), h.draftsOpen⟩
  | draft e hc =>
    refine ⟨h.distinct, h.accepted, h.known, ?_⟩
    intro d hd
    cases hd with
    | head => exact hc
    | tail _ hd => exact h.draftsOpen d hd
  | post e hd ha hk hc =>
    refine ⟨h.distinct, ?_, ?_, ?_⟩
    · intro x hx
      simp only [List.mem_append, List.mem_singleton] at hx
      rcases hx with hx | rfl
      · exact h.accepted x hx
      · exact ha
    · intro x hx
      simp only [List.mem_append, List.mem_singleton] at hx
      rcases hx with hx | rfl
      · exact h.known x hx
      · exact hk
    · intro d hd
      exact h.draftsOpen d ((List.mem_filter.1 hd).1)
  | reverse e he r hr hc =>
    refine ⟨h.distinct, ?_, ?_, h.draftsOpen⟩
    · intro x hx
      simp only [List.mem_append, List.mem_singleton] at hx
      rcases hx with hx | rfl
      · exact h.accepted x hx
      · rw [hr, accepted_reversal_iff]; exact h.accepted e he
    · intro x hx
      simp only [List.mem_append, List.mem_singleton] at hx
      rcases hx with hx | rfl
      · exact h.known x hx
      · intro l hl
        rw [hr] at hl
        simp only [reversal, List.mem_map] at hl
        obtain ⟨l', hl', rfl⟩ := hl
        exact h.known e he l' hl'
  | openPeriod p hp =>
    refine ⟨h.distinct, h.accepted, h.known, ?_⟩
    rintro d hd ⟨q, hq, hc, hdq⟩
    cases hq with
    | head => simp [hp] at hc
    | tail _ hq => exact h.draftsOpen d hd ⟨q, hq, hc, hdq⟩
  | close p hp hopen hdrafts hother hlater ts hts hsum id =>
    refine ⟨h.distinct, ?_, ?_, ?_⟩
    · intro x hx
      simp only [List.mem_append] at hx
      rcases hx with hx | hx
      · exact h.accepted x hx
      · obtain ⟨-, hl, hne⟩ := closingFor_lines L p ts id x hx
        rw [hl]; exact closingEntry_accepted _ _ _ hsum hne
    · intro x hx
      simp only [List.mem_append] at hx
      rcases hx with hx | hx
      · exact h.known x hx
      · obtain ⟨-, hl, -⟩ := closingFor_lines L p ts id x hx
        intro l hl'
        rw [hl] at hl'
        simp only [closingEntry, List.mem_append] at hl'
        rcases hl' with hl' | hl'
        · exact nominalCodes_sub _ _ (closings_account _ _ l hl')
        · obtain ⟨y, hy, e⟩ := equityLines_account ts l hl'
          rw [e]; exact (hts y hy).1
    · intro d hd hcl
      rcases closedOn_closeIn L p d.date hcl with hcl | ⟨-, hc⟩
      · exact h.draftsOpen d hd hcl
      · simp [hdrafts d hd] at hc

/-- **The invariant holds in every reachable state.** -/
theorem Reachable.inv {L : Ledger} (r : Reachable L) : Inv L := by
  induction r with
  | empty => exact ⟨trivial, by simp [Ledger.empty], by simp [Ledger.empty], by simp [Ledger.empty]⟩
  | step _ s ih => exact s.inv ih

/-! ## The books always balance -/

/-- **The books net to zero**: in every reachable state, the posted lines'
debits equal their credits. -/
theorem Reachable.books_net_zero {L : Ledger} (r : Reachable L) : net (allLines L.posted) = 0 :=
  net_allLines _ (fun e he => (r.inv.accepted e he).net_zero)

/-- The same through any day: the books as of any date balance too. -/
theorem Reachable.net_zero_through {L : Ledger} (r : Reachable L) (d : Nat) :
    net (allLines (through d L.posted)) = 0 :=
  net_allLines _ (fun e he => (r.inv.accepted e ((List.mem_filter.1 he).1)).net_zero)

theorem Reachable.covers {L : Ledger} (r : Reachable L) (es : List Entry)
    (hs : ∀ e ∈ es, e ∈ L.posted) : ∀ l ∈ allLines es, l.account ∈ codes L.chart := by
  intro l hl
  obtain ⟨e, he, hl⟩ := mem_allLines.1 hl
  exact r.inv.known e (hs e he) l hl

/-- **The trial balance balances**, in every reachable state. -/
theorem Reachable.trial_balance {L : Ledger} (r : Reachable L) :
    tbDebits (allLines L.posted) (codes L.chart) = tbCredits (allLines L.posted) (codes L.chart) :=
  trial_balance_balances _ _ r.inv.distinct (r.covers _ (fun _ h => h)) r.books_net_zero

/-- **The trial balance as of any date balances.** -/
theorem Reachable.trial_balance_through {L : Ledger} (r : Reachable L) (d : Nat) :
    tbDebits (allLines (through d L.posted)) (codes L.chart)
      = tbCredits (allLines (through d L.posted)) (codes L.chart) :=
  trial_balance_balances _ _ r.inv.distinct
    (r.covers _ (fun _ h => (List.mem_filter.1 h).1)) (r.net_zero_through d)

/-- **The accounting equation holds**, in every reachable state:
Assets = Liabilities + Equity + (Revenue - Expenses). -/
theorem Reachable.accounting_equation {L : Ledger} (r : Reachable L) :
    let ls := allLines L.posted
    typeTotal .asset ls L.chart
      = typeTotal .liability ls L.chart + typeTotal .equity ls L.chart
        + (typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart) :=
  Wanderbooks.accounting_equation _ _ r.inv.distinct (r.covers _ (fun _ h => h)) r.books_net_zero

/-- **The balance sheet as of any date balances.** -/
theorem Reachable.accounting_equation_through {L : Ledger} (r : Reachable L) (d : Nat) :
    let ls := allLines (through d L.posted)
    typeTotal .asset ls L.chart
      = typeTotal .liability ls L.chart + typeTotal .equity ls L.chart
        + (typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart) :=
  Wanderbooks.accounting_equation _ _ r.inv.distinct
    (r.covers _ (fun _ h => (List.mem_filter.1 h).1)) (r.net_zero_through d)

/-! ## Posted is forever -/

/-- **Posting only appends.** No step edits, reorders, or removes a posted
entry. -/
theorem Step.extends {L L' : Ledger} (s : Step L L') : ∃ t, L'.posted = L.posted ++ t := by
  cases s with
  | addAccount => exact ⟨[], by simp⟩
  | draft => exact ⟨[], by simp⟩
  | post e => exact ⟨[e], rfl⟩
  | reverse e _ r => exact ⟨[r], rfl⟩
  | openPeriod => exact ⟨[], by simp⟩
  | close p _ _ _ _ _ ts _ _ id => exact ⟨closingFor L p ts id, rfl⟩

/-- Any number of steps. -/
inductive Steps : Ledger → Ledger → Prop
  | refl (L : Ledger) : Steps L L
  | tail {L M N : Ledger} : Steps L M → Step M N → Steps L N

/-- **Posted is forever**: after any sequence of commands, the old log is
a prefix of the new one. Every posted entry keeps its place and its
lines. -/
theorem Steps.extends {L L' : Ledger} (s : Steps L L') : ∃ t, L'.posted = L.posted ++ t := by
  induction s with
  | refl => exact ⟨[], by simp⟩
  | tail _ s ih =>
    obtain ⟨t, ht⟩ := ih
    obtain ⟨u, hu⟩ := s.extends
    exact ⟨t ++ u, by rw [hu, ht, List.append_assoc]⟩

/-! ## Closed periods are frozen -/

/-- Entries dated in a period. -/
def within (p : Period) (es : List Entry) : List Entry := es.filter (fun e => p.contains e.date)

theorem within_append (p : Period) (xs ys : List Entry) :
    within p (xs ++ ys) = within p xs ++ within p ys := List.filter_append ..

/-- A closed period stays closed. -/
theorem Step.keeps_closed {L L' : Ledger} (s : Step L L') (q : Period) (hq : q ∈ L.periods)
    (hc : q.closed = true) : q ∈ L'.periods := by
  cases s with
  | openPeriod p _ => exact List.mem_cons_of_mem _ hq
  | close p _ hopen =>
    have : q ≠ p := fun e => by subst e; simp [hopen] at hc
    exact List.mem_map.2 ⟨q, hq, by simp [this]⟩
  | _ => exact hq

/-- **A step never changes what a closed period contains.** -/
theorem Step.frozen {L L' : Ledger} (s : Step L L') (q : Period) (hq : q ∈ L.periods)
    (hc : q.closed = true) : within q L'.posted = within q L.posted := by
  have nothing : ∀ e : Entry, ¬ L.closedOn e.date → within q [e] = [] := by
    intro e he
    simp only [within, List.filter_cons, List.filter_nil]
    split
    · exact absurd ⟨q, hq, hc, by assumption⟩ he
    · rfl
  cases s with
  | post e _ _ _ hcl => rw [within_append, nothing e hcl, List.append_nil]
  | reverse e _ r _ hcl => rw [within_append, nothing r hcl, List.append_nil]
  | close p hp hopen hdrafts hother hlater ts hts hsum id =>
    rw [within_append]
    have : within q (closingFor L p ts id) = [] := by
      unfold closingFor
      split
      · rfl
      · simp only [within, List.filter_cons, List.filter_nil]
        rw [hother q hq hc]; rfl
    rw [this, List.append_nil]
  | _ => rfl

/-- **Closed periods are frozen**: once a period is closed, no sequence of
commands adds, removes, or changes an entry dated in it. -/
theorem Steps.frozen {L L' : Ledger} (s : Steps L L') (q : Period) (hq : q ∈ L.periods)
    (hc : q.closed = true) : within q L'.posted = within q L.posted ∧ q ∈ L'.periods := by
  induction s with
  | refl => exact ⟨rfl, hq⟩
  | tail _ s ih =>
    obtain ⟨h1, h2⟩ := ih
    exact ⟨(s.frozen q h2 hc).trans h1, s.keeps_closed q h2 hc⟩

/-! ## Closing -/

/-- **After a close, every revenue and expense account is zero through the
period's last day.** (The trial balance still balances: the close is a
step, and `Reachable.trial_balance` covers every step.) -/
theorem close_zeroes {L : Ledger} (r : Reachable L) (p : Period)
    (ts : List (Nat × Int)) (hts : ∀ x ∈ ts, x.1 ∈ codes L.chart ∧ x.1 ∉ nominalCodes L.chart)
    (id : Nat) (a : Nat) (ha : a ∈ nominalCodes L.chart) :
    movement a (allLines (through p.stop (L.posted ++ closingFor L p ts id))) = 0 := by
  have hd := nominalCodes_distinct _ r.inv.distinct
  have hta : ∀ x ∈ ts, x.1 ≠ a := fun x hx e => (hts x hx).2 (e ▸ ha)
  rw [through, List.filter_append, ← through, allLines_append]
  unfold closingFor
  split
  · rename_i hnil
    simp only [List.filter_nil, allLines, List.append_nil]
    exact closings_eq_nil _ _ hnil a ha
  · simp only [List.filter_cons, Nat.le_refl, decide_true, ite_true, List.filter_nil, allLines,
      List.append_nil]
    exact closingEntry_zeroes _ ts _ hd a ha hta

/-- **A close credits equity with exactly the period's net income**:
revenue minus expenses through its last day, split among the targets. -/
theorem close_credits_net_income (L : Ledger) (p : Period) (ts : List (Nat × Int))
    (hsum : total (ts.map Prod.snd)
      = net (closings (nominalCodes L.chart) (allLines (through p.stop L.posted)))) :
    let ls := allLines (through p.stop L.posted)
    total (ts.map Prod.snd) = typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart := by
  intro ls
  rw [hsum, net_closings_is_net_income]

/-! ## Period statements add up -/

/-- Entries dated after day `b`, through day `c`. -/
def between (b c : Nat) (es : List Entry) : List Entry :=
  es.filter (fun e => decide (b < e.date ∧ e.date ≤ c))

theorem movement_split (a b c : Nat) (h : b ≤ c) (es : List Entry) :
    movement a (allLines (through c es))
      = movement a (allLines (through b es)) + movement a (allLines (between b c es)) := by
  induction es with
  | nil => rfl
  | cons e es ih =>
    simp only [through, between] at ih ⊢
    by_cases h1 : e.date ≤ b
    · have h2 : e.date ≤ c := by omega
      have h3 : ¬ (b < e.date ∧ e.date ≤ c) := by omega
      rw [List.filter_cons_of_pos (by simpa using h2), List.filter_cons_of_pos (by simpa using h1),
        List.filter_cons_of_neg (by simpa using h3)]
      simp only [allLines, movement_append, ih]; omega
    · by_cases h2 : e.date ≤ c
      · have h3 : b < e.date ∧ e.date ≤ c := by omega
        rw [List.filter_cons_of_pos (by simpa using h2), List.filter_cons_of_neg (by simpa using h1),
          List.filter_cons_of_pos (by simpa using h3)]
        simp only [allLines, movement_append, ih]; omega
      · have h3 : ¬ (b < e.date ∧ e.date ≤ c) := by omega
        rw [List.filter_cons_of_neg (by simpa using h2), List.filter_cons_of_neg (by simpa using h1),
          List.filter_cons_of_neg (by simpa using h3)]
        exact ih

theorem typeTotal_split (t : AccountType) (x y z : List Line)
    (h : ∀ a, movement a x = movement a y + movement a z) (c : Chart) :
    typeTotal t x c = typeTotal t y c + typeTotal t z c := by
  induction c with
  | nil => rfl
  | cons p c ih =>
    obtain ⟨a, t'⟩ := p
    simp only [typeTotal, h a, ih]
    split
    · cases t' <;> simp [balance, AccountType.normal, signed] <;> omega
    · omega

/-- **Period statements add up**: every account type's total (so revenue,
expenses, and net income) through day `c` is its total through day `b`
plus its total for the days after `b` through `c`. A year's P&L is the sum
of its months'. -/
theorem statements_add_up (t : AccountType) (b c : Nat) (h : b ≤ c) (es : List Entry)
    (chart : Chart) :
    typeTotal t (allLines (through c es)) chart
      = typeTotal t (allLines (through b es)) chart
        + typeTotal t (allLines (between b c es)) chart :=
  typeTotal_split t _ _ _ (fun a => movement_split a b c h es) chart

end Wanderbooks