import Wanderbooks.Entry

/-!
# Documents are the subledgers of their control accounts (rules.md B-38)

Every ledger line may carry the document it belongs to (an invoice or a
bill: `Ledger.line_docs`, `arap::DocTag`). A document's figures are the
sum of its tagged lines; a control account's balance is the sum of every
line on it. Mirrors `Ledger::doc_state` (outstanding), `control_check`,
the control guard (`check_control_lines`: every line a command posts on a
control account carries its document) and `reverse_entry` (a mirror line
copies its original's tag).

The headline, `control_agrees`: for every account and any lines at all,
the account's balance is the sum over the documents of what each carries
on it, plus its untagged ("unattached") lines. Both sides sum the same
lines, so it is an identity, not a reconciliation, and it holds through
any date, since a date is a filter on the lines. A document is one `Nat`
here: an injective coding of `DocRef` (invoices and bills in one id
space), which is all the sums need. Then, over the commands:
a document step (an invoice, a bill, a payment, or any entry whose
control lines are tagged) never moves what is unattached; a reversal
moves each document, and what is unattached, by exactly the opposite of
the lines it mirrors (B-38 INVARIANT 3); so books built by these steps
alone have nothing unattached on a control account, ever
(`Reachable.unattached_zero`).
-/

namespace Wanderbooks.Documents

open Wanderbooks

/-- A posted line, its day, and the document it carries (`none`: none). -/
structure TLine where
  line : Line
  date : Nat
  doc : Option Nat
  deriving DecidableEq

/-- A recorded send of an invoice (plan P4b S5, `Sent`, `invoice.sent`):
the invoice, the day, and a code for who sent it, how, to whom and the
channel's own reference. No figure reads it: a send moves no money. -/
structure Send where
  doc : Nat
  day : Nat
  code : Nat
  deriving DecidableEq

/-- A line's signed amount on account `a` (zero on another account). -/
def onAcct (a : Nat) (l : TLine) : Int := if l.line.account = a then l.line.signed else 0

/-- Account `a`'s balance over some lines (the general ledger). -/
def gl (a : Nat) : List TLine → Int
  | [] => 0
  | l :: ls => onAcct a l + gl a ls

/-- What document `d`'s lines on account `a` sum to (`doc_lines`). -/
def docSum (a d : Nat) : List TLine → Int
  | [] => 0
  | l :: ls => (if l.doc = some d then onAcct a l else 0) + docSum a d ls

/-- Account `a`'s lines that carry no document. -/
def unattached (a : Nat) : List TLine → Int
  | [] => 0
  | l :: ls => (if l.doc = none then onAcct a l else 0) + unattached a ls

@[simp] theorem gl_nil (a : Nat) : gl a [] = 0 := rfl
@[simp] theorem docSum_nil (a d : Nat) : docSum a d [] = 0 := rfl
@[simp] theorem unattached_nil (a : Nat) : unattached a [] = 0 := rfl

theorem gl_append (a : Nat) (xs ys : List TLine) : gl a (xs ++ ys) = gl a xs + gl a ys := by
  induction xs with
  | nil => simp
  | cons x xs ih => simp only [List.cons_append, gl, ih]; omega

theorem docSum_append (a d : Nat) (xs ys : List TLine) :
    docSum a d (xs ++ ys) = docSum a d xs + docSum a d ys := by
  induction xs with
  | nil => simp
  | cons x xs ih => simp only [List.cons_append, docSum, ih]; omega

theorem unattached_append (a : Nat) (xs ys : List TLine) :
    unattached a (xs ++ ys) = unattached a xs + unattached a ys := by
  induction xs with
  | nil => simp
  | cons x xs ih => simp only [List.cons_append, unattached, ih]; omega

/-- Every document some lines carry is among `ds`. -/
def Covers (ds : List Nat) (ls : List TLine) : Prop :=
  ∀ l ∈ ls, ∀ k, l.doc = some k → k ∈ ds

/-- **The control account agrees with its documents** (B-38 INVARIANT 1):
for any lines, any account, and any distinct document ids covering the
lines' tags, the balance is the documents' sum plus what is unattached. -/
theorem control_agrees (a : Nat) (ds : List Nat) (hd : Distinct ds) :
    ∀ ls : List TLine, Covers ds ls →
      gl a ls = sumOver (fun d => docSum a d ls) ds + unattached a ls := by
  intro ls
  induction ls with
  | nil => intro _; simp [sumOver_zero]
  | cons l ls ih =>
    intro hc
    have hc' : Covers ds ls := fun m hm => hc m (List.mem_cons_of_mem _ hm)
    simp only [gl, docSum, unattached]
    rw [sumOver_add, ih hc']
    cases h : l.doc with
    | none =>
      simp [sumOver_zero] <;> omega
    | some k =>
      have hk : k ∈ ds := hc l (List.mem_cons_self ..) k h
      have e : sumOver (fun d => if some k = some d then onAcct a l else 0) ds
          = sumOver (fun d => if k = d then onAcct a l else 0) ds :=
        sumOver_congr _ _ ds (fun d _ => by simp)
      simp only [e, sumOver_indicator k (onAcct a l) ds hd hk]
      simp <;> omega

/-- The lines dated on or before day `D`. -/
def through (D : Nat) (ls : List TLine) : List TLine := ls.filter (fun l => decide (l.date ≤ D))

theorem Covers.through {ds : List Nat} {ls : List TLine} (h : Covers ds ls) (D : Nat) :
    Covers ds (through D ls) := fun l hl => h l (List.mem_filter.1 hl).1

/-- **The same through any day**: GL(A, D) = Σ_docs outstanding(d, D) +
unattached(A, D). -/
theorem control_agrees_through (a : Nat) (ds : List Nat) (hd : Distinct ds) (ls : List TLine)
    (hc : Covers ds ls) (D : Nat) :
    gl a (through D ls) = sumOver (fun d => docSum a d (through D ls)) ds
      + unattached a (through D ls) :=
  control_agrees a ds hd _ (hc.through D)

/-! ## The commands -/

/-- A line mirrored by a reversal: its side flipped, its day the
reversal's, its document kept (`reverse_entry_steps` copies the tag). -/
def mirror (D : Nat) (l : TLine) : TLine := { l with line := l.line.reverse, date := D }

theorem onAcct_mirror (a D : Nat) (l : TLine) : onAcct a (mirror D l) = -onAcct a l := by
  unfold onAcct mirror
  by_cases h : l.line.account = a
  · simp [Line.reverse, h]
    have := Line.reverse_signed l.line
    simp [Line.reverse] at this
    exact this
  · simp [Line.reverse, h]

theorem docSum_mirror (a d D : Nat) (ls : List TLine) :
    docSum a d (ls.map (mirror D)) = -docSum a d ls := by
  induction ls with
  | nil => simp
  | cons l ls ih =>
    simp only [List.map_cons, docSum, ih, onAcct_mirror]
    have : (mirror D l).doc = l.doc := rfl
    rw [this]
    by_cases h : l.doc = some d <;> simp [h] <;> omega

theorem unattached_mirror (a D : Nat) (ls : List TLine) :
    unattached a (ls.map (mirror D)) = -unattached a ls := by
  induction ls with
  | nil => simp
  | cons l ls ih =>
    simp only [List.map_cons, unattached, ih, onAcct_mirror]
    have : (mirror D l).doc = l.doc := rfl
    rw [this]
    by_cases h : l.doc = none <;> simp [h] <;> omega

/-- Every line of `ls` on a control account carries a document: what the
control guard requires of every entry a command posts. -/
def Tagged (control : List Nat) (ls : List TLine) : Prop :=
  ∀ l ∈ ls, l.line.account ∈ control → l.doc ≠ none

/-- The books: the control accounts (the receivables and payables roles),
every posted line in order, and the sends recorded (each on its invoice;
plan P4b S5). -/
structure Books where
  control : List Nat
  lines : List TLine
  sends : List Send

/-- The documents some lines carry: the invoices a send can name. -/
def Books.docs (B : Books) : List Nat :=
  B.lines.filterMap (fun l => l.doc)

/-- What the engine allows (S1): a document command, or any entry whose
control lines are all tagged (`Step.document`); a reversal of posted
lines, mirror for mirror, each keeping its tag (`Step.reverse`), dated on
or after them (B-38, "Dating rules"); assigning a document role an
account all of whose lines are documents' (`Step.assign`:
`check_assign_role` SCENARIO 6 refuses one holding an untagged line); and
an account leaving the control accounts once it holds no document's line
(`Step.release`: an assigned role moved off an account no document posted
to; an account holding a document's line stays guarded,
`control_role_of`). -/
inductive Step : Books → Books → Prop
  | document (B : Books) (e : List TLine) (h : Tagged B.control e) :
      Step B { B with lines := B.lines ++ e }
  | reverse (B : Books) (e : List TLine) (he : ∀ l ∈ e, l ∈ B.lines) (D : Nat) :
      Step B { B with lines := B.lines ++ e.map (mirror D) }
  | assign (B : Books) (c : Nat) (h : ∀ l ∈ B.lines, l.line.account = c → l.doc ≠ none) :
      Step B { B with control := c :: B.control }
  | release (B : Books) (c : Nat) (h : ∀ l ∈ B.lines, l.line.account = c → l.doc = none) :
      Step B { B with control := B.control.erase c }
  /-- `mark_sent` (`Ledger::mark_sent`, plan P4b S5): a send is recorded on
  an invoice the books hold, and nothing else changes. It moves no line,
  so every figure stays where it was. -/
  | markSent (B : Books) (s : Send) (h : s.doc ∈ B.docs) :
      Step B { B with sends := s :: B.sends }

/-- **A document step never moves what is unattached** on a control
account: no command adds an untagged control line. -/
theorem Step.document_unattached (B : Books) (e : List TLine) (h : Tagged B.control e)
    (a : Nat) (ha : a ∈ B.control) : unattached a (B.lines ++ e) = unattached a B.lines := by
  rw [unattached_append]
  suffices unattached a e = 0 by omega
  induction e with
  | nil => rfl
  | cons l ls ih =>
    simp only [unattached]
    rw [ih (fun m hm => h m (List.mem_cons_of_mem _ hm))]
    by_cases hn : l.doc = none
    · have hacc : l.line.account ≠ a := fun e => h l (List.mem_cons_self ..) (e ▸ ha) hn
      simp [hn, onAcct, hacc]
    · simp [hn]

/-- **A settlement is a document step**: its entry's every control line
carries its document (a payment or a discount), so the books' rules for
any entry whose control lines are tagged cover it; no new `Step`
constructor is needed (plan P4b S6; rules.md B-42). -/
theorem settle_posts_a_document_step (B : Books) (e : List TLine)
    (h : Tagged B.control e) : Step B { B with lines := B.lines ++ e } :=
  Step.document B e h

/-- **A settlement never moves what is unattached** on a control account:
every control line it posts is its document's (B-42, from
`Step.document_unattached`). -/
theorem settle_unattached (B : Books) (e : List TLine) (h : Tagged B.control e) (a : Nat)
    (ha : a ∈ B.control) : unattached a (B.lines ++ e) = unattached a B.lines :=
  Step.document_unattached B e h a ha

/-- **A reversal moves each document by exactly the opposite of its lines
it mirrors** (B-38 INVARIANT 3), and what is unattached likewise: only
reversing a legacy hand line changes it. -/
theorem Step.reverse_moves (B : Books) (e : List TLine) (D a d : Nat) :
    docSum a d (B.lines ++ e.map (mirror D)) = docSum a d B.lines - docSum a d e
      ∧ unattached a (B.lines ++ e.map (mirror D)) = unattached a B.lines - unattached a e := by
  rw [docSum_append, docSum_mirror, unattached_append, unattached_mirror]
  omega

/-- **Reversing a reversal restores every document** (B-10): the lines,
mirrored twice, sum as the originals did. -/
theorem reverse_twice (a d D D' : Nat) (e : List TLine) :
    docSum a d ((e.map (mirror D)).map (mirror D')) = docSum a d e := by
  rw [docSum_mirror, docSum_mirror]; omega

/-- **A send changes no figure** (plan P4b S5): recording one leaves every
control account's balance, every document's sum on it and what is
unattached exactly as they were, through any day. A send adds a record and
no line, so the engine's own statement (`Ledger::mark_sent`) that a
document's DocState is the same before and after is this, line for line. -/
theorem Step.markSent_changes_no_figure (B : Books) (s : Send) (_h : s.doc ∈ B.docs)
    (a d D : Nat) :
    gl a (through D ({ B with sends := s :: B.sends } : Books).lines)
        = gl a (through D B.lines)
    ∧ docSum a d (through D ({ B with sends := s :: B.sends } : Books).lines)
        = docSum a d (through D B.lines)
    ∧ unattached a (through D ({ B with sends := s :: B.sends } : Books).lines)
        = unattached a (through D B.lines) := by
  exact ⟨rfl, rfl, rfl⟩

/-- States reachable from books with no lines. -/
inductive Reachable : Books → Prop
  | empty (control : List Nat) : Reachable ⟨control, [], []⟩
  | step {B B' : Books} : Reachable B → Step B B' → Reachable B'

theorem Reachable.tagged {B : Books} (r : Reachable B) : Tagged B.control B.lines := by
  induction r with
  | empty => intro l hl; simp at hl
  | step _ s ih =>
    cases s with
    | document e h =>
      intro l hl hc
      rcases List.mem_append.1 hl with hl | hl
      · exact ih l hl hc
      · exact h l hl hc
    | reverse e he D =>
      intro l hl hc
      rcases List.mem_append.1 hl with hl | hl
      · exact ih l hl hc
      · obtain ⟨m, hm, rfl⟩ := List.mem_map.1 hl
        exact ih m (he m hm) (by simpa [mirror, Line.reverse] using hc)
    | assign c h =>
      intro l hl hc
      rcases List.mem_cons.1 hc with hc | hc
      · exact h l hl hc
      · exact ih l hl hc
    | release c h =>
      intro l hl hc
      exact ih l hl (List.mem_of_mem_erase hc)
    | markSent _ _ =>
      -- A send touches no line: the control lines are the ones it found.
      exact ih

/-- **Nothing is ever unattached on a control account** in books these
steps build, through any day, roles assigned and released included:
every control line is a document's. (Books an earlier version wrote, with
hand lines, are covered by the identity `control_agrees` alone; an
account becoming a control account by its first document, holding lines
from before, is outside the model: `control_check` lists those lines.) -/
theorem Reachable.unattached_zero {B : Books} (r : Reachable B) (a : Nat) (ha : a ∈ B.control)
    (D : Nat) : unattached a (through D B.lines) = 0 := by
  have ht := r.tagged
  have : ∀ ls : List TLine, (∀ l ∈ ls, l ∈ B.lines) → unattached a ls = 0 := by
    intro ls
    induction ls with
    | nil => intro _; rfl
    | cons l ls ih =>
      intro hs
      simp only [unattached]
      rw [ih (fun m hm => hs m (List.mem_cons_of_mem _ hm))]
      by_cases hn : l.doc = none
      · have hacc : l.line.account ≠ a :=
          fun e => ht l (hs l (List.mem_cons_self ..)) (e ▸ ha) hn
        simp [hn, onAcct, hacc]
      · simp [hn]
  exact this _ (fun l hl => (List.mem_filter.1 hl).1)

/-- **So the control account is its documents**, exactly, on every day:
GL(A, D) = Σ_docs outstanding(d, D). -/
theorem Reachable.control_is_documents {B : Books} (r : Reachable B) (a : Nat)
    (ha : a ∈ B.control) (ds : List Nat) (hd : Distinct ds) (hc : Covers ds B.lines) (D : Nat) :
    gl a (through D B.lines) = sumOver (fun d => docSum a d (through D B.lines)) ds := by
  rw [control_agrees_through a ds hd B.lines hc D, r.unattached_zero a ha D]; omega

end Wanderbooks.Documents