/-
Specification of the homepage animation: waves from origins that start in turn on a neighbourhood graph.
SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception

A run is a finite weighted graph over synthetic points and the result the animation draws. Origins start
in turn. Every wave travels at one speed: a point is claimed when a wave reaches it, through the link that
brought it (a branch). A tree that grows `cap` branches before its wave meets another tree's wave ends; it
then holds, fades and frees its points, which later trees may claim again. Distances are times at the shared
speed; meeting times are doubled so they stay whole. The properties below form the certificate; `Growth.Theorems`
proves what they imply. Nothing here concerns real data.
-/
set_option synthInstance.maxHeartbeats 2000000
set_option synthInstance.maxSize 4096

namespace Growth

structure Run where
  /-- Point coordinates, indexed by point number. -/
  points : List (Nat × Nat)
  /-- Links `(a, b, w)` with `a < b`, listed in strictly increasing order; `w` is the link length. -/
  edges : List (Nat × Nat × Nat)
  /-- Distance per drawing step, branch budget, distance between origin slots, hold and fade lengths. -/
  pace : Nat
  cap : Nat
  every : Nat
  hold : Nat
  fade : Nat
  /-- Trees `(origin claim, start, end, first meeting)`; the end is set when an unconnected tree uses its
      budget, the first meeting (doubled) when its wave first meets a live tree's wave. -/
  trees : List (Nat × Nat × Option Nat × Option Nat)
  /-- Claims `(point, tree, distance, parent claim)` in time order; an origin's claim is its own parent. -/
  claims : List (Nat × Nat × Nat × Nat)
  /-- Wave halves `(claim, far point, doubled end, kind)`: the wave leaving the claim's point along the link
      to the far point, drawn until the doubled end; kind 0 crosses, 1 is a branch, 2 is a first meeting. -/
  halves : List (Nat × Nat × Nat × Nat)
  /-- First meetings: the two opposite halves where two trees' waves first met. -/
  meetings : List (Nat × Nat)

namespace Run

def n (r : Run) : Nat := r.points.length
def point (r : Run) (v : Nat) : Nat × Nat := r.points.getD v (0, 0)
def tree (r : Run) (k : Nat) : Nat × Nat × Option Nat × Option Nat := r.trees.getD k (0, 0, none, none)
def origin (r : Run) (k : Nat) : Nat := (r.tree k).1
def start (r : Run) (k : Nat) : Nat := (r.tree k).2.1
def ended (r : Run) (k : Nat) : Option Nat := (r.tree k).2.2.1
def met (r : Run) (k : Nat) : Option Nat := (r.tree k).2.2.2
def claim (r : Run) (i : Nat) : Nat × Nat × Nat × Nat := r.claims.getD i (0, 0, 0, 0)
def pt (r : Run) (i : Nat) : Nat := (r.claim i).1
def own (r : Run) (i : Nat) : Nat := (r.claim i).2.1
def d (r : Run) (i : Nat) : Nat := (r.claim i).2.2.1
def par (r : Run) (i : Nat) : Nat := (r.claim i).2.2.2
def half (r : Run) (h : Nat) : Nat × Nat × Nat × Nat := r.halves.getD h (0, 0, 0, 0)
def meeting (r : Run) (m : Nat) : Nat × Nat := r.meetings.getD m (0, 0)
/-- The tree of the claim a half leaves from. -/
def hown (r : Run) (h : Nat) : Nat := r.own (r.half h).1

/-- A link of length `w` joins `a` and `b`, in either orientation. -/
def HasEdge (r : Run) (a b w : Nat) : Prop := (a, b, w) ∈ r.edges ∨ (b, a, w) ∈ r.edges

/-- The length of the link joining `a` and `b` (zero when there is none). -/
def wt (r : Run) (a b : Nat) : Nat :=
  match r.edges.find? (fun e => (e.1 == a && e.2.1 == b) || (e.1 == b && e.2.1 == a)) with
  | some e => e.2.2
  | none => 0

/-- `x` is no later than an optional end. -/
def Within (o : Option Nat) (x : Nat) : Prop := match o with | some e => x ≤ e | none => True

/-- The number of branches a tree has grown: its claims other than its origin. -/
def branches (r : Run) (k : Nat) : Nat := (r.claims.filter (fun c => c.2.1 == k)).length - 1

/-- Property 1 — origins start in turn: tree `k`'s origin is its own claim at its start, on an origin slot;
    the first starts at zero and each later one later. -/
def Origins (r : Run) : Prop :=
  0 < r.trees.length ∧ r.start 0 = 0 ∧
  (∀ k, k < r.trees.length → r.origin k < r.claims.length ∧ r.own (r.origin k) = k ∧ r.d (r.origin k) = r.start k ∧
    r.par (r.origin k) = r.origin k ∧ r.start k % r.every = 0) ∧
  (∀ k, k < r.trees.length - 1 → r.start k < r.start (k + 1))

/-- Property 2 — tight branches: claims come in time order and none follows its tree's end; every claim other
    than an origin comes from an earlier claim of the same tree, its distance is that claim's distance plus
    the length of the link between them, and its branch is drawn exactly to it. -/
def Tight (r : Run) : Prop :=
  ∀ i, i < r.claims.length → r.pt i < r.n ∧ r.own i < r.trees.length ∧ Within (r.ended (r.own i)) (r.d i) ∧
    (0 < i → r.d (i - 1) ≤ r.d i) ∧
    (r.par i = i → r.origin (r.own i) = i) ∧
    (r.par i ≠ i → r.par i < i ∧ r.own (r.par i) = r.own i ∧ r.d (r.par i) < r.d i ∧
      r.HasEdge (r.pt (r.par i)) (r.pt i) (r.d i - r.d (r.par i)) ∧
      ∃ h ∈ List.range r.halves.length, r.half h = (r.par i, r.pt i, 2 * r.d i, 1))

/-- Property 3 — the budget: a tree whose wave never met another grows at most `cap` branches, and it ends
    exactly when it grows the last of them; a tree that met another never ends. -/
def Budget (r : Run) : Prop :=
  ∀ k, k < r.trees.length →
    (r.met k = none → r.branches k ≤ r.cap ∧ (r.ended k ≠ none ↔ r.branches k = r.cap) ∧
      ∀ e ∈ (r.ended k).toList, ∃ i ∈ List.range r.claims.length, r.own i = k ∧ r.par i ≠ i ∧ r.d i = e) ∧
    (r.met k ≠ none → r.ended k = none)

/-- Property 4 — one tree at a time: a point is claimed again only after the tree that held it ended, held
    and faded. -/
def Exclusive (r : Run) : Prop :=
  ∀ j, j < r.claims.length → ∀ i, i < j → r.pt i = r.pt j →
    ∃ e ∈ (r.ended (r.own i)).toList, e + r.hold + r.fade ≤ r.d j

/-- Property 5 — halves: every half follows a link from its claim's point, drawn from that claim's distance
    for no more than the link's length and not past its tree's end. A branch half reaches its point as that
    point is claimed through it; a meeting half belongs to a recorded meeting. -/
def hc (r : Run) (h : Nat) : Nat := (r.half h).1
def hy (r : Run) (h : Nat) : Nat := (r.half h).2.1
def he (r : Run) (h : Nat) : Nat := (r.half h).2.2.1
def hk (r : Run) (h : Nat) : Nat := (r.half h).2.2.2
def hw (r : Run) (h : Nat) : Nat := r.wt (r.pt (r.hc h)) (r.hy h)

def Halves (r : Run) : Prop :=
  ∀ h, h < r.halves.length →
    r.hc h < r.claims.length ∧ r.HasEdge (r.pt (r.hc h)) (r.hy h) (r.hw h) ∧
      2 * r.d (r.hc h) ≤ r.he h ∧ r.he h ≤ 2 * (r.d (r.hc h) + r.hw h) ∧
      (∀ e ∈ (r.ended (r.own (r.hc h))).toList, r.he h ≤ 2 * e) ∧ r.hk h ≤ 2 ∧
      (r.hk h = 1 → r.he h = 2 * (r.d (r.hc h) + r.hw h) ∧
        ∃ j ∈ List.range r.claims.length, r.pt j = r.hy h ∧ r.par j = r.hc h ∧ r.d j = r.d (r.hc h) + r.hw h) ∧
      (r.hk h = 2 → ∃ m ∈ List.range r.meetings.length, (r.meeting m).1 = h ∨ (r.meeting m).2 = h)

/-- Property 6 — first meetings: a meeting is two opposite meeting halves from different trees that end
    together where the waves meet, at `(d a + w + d b) / 2`; no two meetings join the same two trees; a tree's
    first meeting time is its earliest meeting, and a tree with no meeting has none. -/
def mg (r : Run) (m : Nat) : Nat := (r.meeting m).1
def mh (r : Run) (m : Nat) : Nat := (r.meeting m).2
/-- Meeting `m` involves tree `k`. -/
def Joins (r : Run) (m k : Nat) : Prop := r.hown (r.mg m) = k ∨ r.hown (r.mh m) = k

def Meetings (r : Run) : Prop :=
  (∀ m, m < r.meetings.length →
    r.mg m < r.halves.length ∧ r.mh m < r.halves.length ∧ r.hk (r.mg m) = 2 ∧ r.hk (r.mh m) = 2 ∧
      r.hy (r.mg m) = r.pt (r.hc (r.mh m)) ∧ r.hy (r.mh m) = r.pt (r.hc (r.mg m)) ∧ r.hown (r.mg m) ≠ r.hown (r.mh m) ∧
      r.he (r.mg m) = r.he (r.mh m) ∧ r.he (r.mg m) = r.d (r.hc (r.mg m)) + r.hw (r.mg m) + r.d (r.hc (r.mh m)) ∧
      Within (r.ended (r.hown (r.mg m))) (r.he (r.mg m) / 2) ∧ Within (r.ended (r.hown (r.mh m))) (r.he (r.mg m) / 2)) ∧
  (∀ m, m < r.meetings.length → ∀ m', m' < m →
    ¬ ((r.hown (r.mg m) = r.hown (r.mg m') ∧ r.hown (r.mh m) = r.hown (r.mh m')) ∨
       (r.hown (r.mg m) = r.hown (r.mh m') ∧ r.hown (r.mh m) = r.hown (r.mg m')))) ∧
  (∀ k, k < r.trees.length →
    (r.met k = none ↔ ¬ ∃ m ∈ List.range r.meetings.length, r.Joins m k) ∧
    ∀ t ∈ (r.met k).toList, (∃ m ∈ List.range r.meetings.length, r.Joins m k ∧ r.he (r.mg m) = t) ∧
      ∀ m, m < r.meetings.length → r.Joins m k → t ≤ r.he (r.mg m))

/-- Property 7 — honest links: every link joins two different points, `a < b < n`, length at least 1, links
    are listed in strictly increasing order, and lengths are straight-line distances rounded to the nearest unit. -/
def Links (r : Run) : Prop :=
  (∀ e ∈ r.edges, e.1 < e.2.1 ∧ e.2.1 < r.n ∧ 1 ≤ e.2.2 ∧
    let p := r.point e.1
    let q := r.point e.2.1
    let sq := (p.1 - q.1) * (p.1 - q.1) + (q.1 - p.1) * (q.1 - p.1) + (p.2 - q.2) * (p.2 - q.2) + (q.2 - p.2) * (q.2 - p.2)
    (2 * e.2.2 - 1) * (2 * e.2.2 - 1) ≤ 4 * sq ∧ 4 * sq < (2 * e.2.2 + 1) * (2 * e.2.2 + 1)) ∧
  ∀ k, k < r.edges.length - 1 →
    let e := r.edges.getD k (0, 0, 0)
    let e' := r.edges.getD (k + 1) (0, 0, 0)
    e.1 < e'.1 ∨ (e.1 = e'.1 ∧ e.2.1 < e'.2.1)

/-- The whole specification. -/
def Valid (r : Run) : Prop :=
  r.Origins ∧ r.Tight ∧ r.Budget ∧ r.Exclusive ∧ r.Halves ∧ r.Meetings ∧ r.Links

instance (o : Option Nat) (x : Nat) : Decidable (Within o x) := by unfold Within; split <;> infer_instance
instance (r : Run) (a b w : Nat) : Decidable (r.HasEdge a b w) := by unfold HasEdge; infer_instance
instance (r : Run) : Decidable r.Origins := by unfold Origins; infer_instance
instance (r : Run) : Decidable r.Tight := by unfold Tight; infer_instance
instance (r : Run) : Decidable r.Budget := by unfold Budget; infer_instance
instance (r : Run) : Decidable r.Exclusive := by unfold Exclusive; infer_instance
instance (r : Run) : Decidable r.Halves := by unfold Halves; infer_instance
instance (r : Run) (m k : Nat) : Decidable (r.Joins m k) := by unfold Joins; infer_instance
instance (r : Run) : Decidable r.Meetings := by unfold Meetings; infer_instance
instance (r : Run) : Decidable r.Links := by unfold Links; infer_instance
instance (r : Run) : Decidable r.Valid := by unfold Valid; infer_instance

end Run
end Growth