/-
What the certificate implies, for any run: every claim is reached from its tree's origin along the drawn
branches, by a walk exactly as long as the time since that origin started.
SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
-/
import Growth.Spec

namespace Growth
namespace Run

/-- `Walk r a c k`: a walk through the graph from `a` to `c` whose links have total length `k`. -/
inductive Walk (r : Run) : Nat → Nat → Nat → Prop
  | nil (v : Nat) : Walk r v v 0
  | cons {a b c w k : Nat} (h : r.HasEdge a b w) (rest : Walk r b c k) : Walk r a c (w + k)

/-- Extending a walk by one link at its end. -/
theorem Walk.snoc {r : Run} {a b c w k : Nat} (walk : r.Walk a b k) (h : r.HasEdge b c w) : r.Walk a c (k + w) := by
  induction walk with
  | nil v => simpa using Walk.cons h (Walk.nil c)
  | cons h' _ ih =>
    have := Walk.cons h' (ih h)
    rwa [← Nat.add_assoc] at this

/-- An origin's claim is reached at its tree's start, by the empty walk. -/
theorem origin_case {r : Run} (ho : r.Origins) {i : Nat} (hown : r.own i < r.trees.length) (hroot : r.origin (r.own i) = i) :
    r.start (r.own i) ≤ r.d i ∧ r.Walk (r.pt (r.origin (r.own i))) (r.pt i) (r.d i - r.start (r.own i)) := by
  have hd := (ho.2.2.1 (r.own i) hown).2.2.1
  rw [hroot] at hd
  refine ⟨Nat.le_of_eq hd.symm, ?_⟩
  rw [hroot, hd, Nat.sub_self]
  exact Walk.nil _

/-- Theorem — every claim is reached along its tree's branches: following parents from any claim gives a walk
    from its tree's origin, as long as the claim's distance minus the tree's start. Properties 1 and 2 are needed. -/
theorem reached {r : Run} (ho : r.Origins) (ht : r.Tight) :
    ∀ i, i < r.claims.length → r.start (r.own i) ≤ r.d i ∧
      r.Walk (r.pt (r.origin (r.own i))) (r.pt i) (r.d i - r.start (r.own i)) := by
  -- Induct on a bound for the claim index: parents are earlier claims, so the chain ends at an origin.
  suffices h : ∀ m, ∀ i, i < r.claims.length → i ≤ m →
      r.start (r.own i) ≤ r.d i ∧ r.Walk (r.pt (r.origin (r.own i))) (r.pt i) (r.d i - r.start (r.own i)) from
    fun i hi => h i i hi (Nat.le_refl _)
  intro m
  induction m with
  | zero =>
    intro i hi hm
    obtain ⟨_, hown, _, _, hroot, hstep⟩ := ht i hi
    by_cases hp : r.par i = i
    · exact origin_case ho hown (hroot hp)
    · exact absurd (Nat.lt_of_lt_of_le (hstep hp).1 hm) (Nat.not_lt_zero _)
  | succ m ihm =>
    intro i hi hm
    obtain ⟨_, hown, _, _, hroot, hstep⟩ := ht i hi
    by_cases hp : r.par i = i
    · exact origin_case ho hown (hroot hp)
    · obtain ⟨hlt, hsame, hnear, hedge, _⟩ := hstep hp
      obtain ⟨hle, walk⟩ := ihm (r.par i) (Nat.lt_trans hlt hi) (Nat.le_of_lt_succ (Nat.lt_of_lt_of_le hlt hm))
      rw [hsame] at hle walk
      have := Walk.snoc walk hedge
      have hlen : r.d (r.par i) - r.start (r.own i) + (r.d i - r.d (r.par i)) = r.d i - r.start (r.own i) := by
        rw [Nat.add_comm]; exact Nat.sub_add_sub_cancel (Nat.le_of_lt hnear) hle
      rw [hlen] at this
      exact ⟨Nat.le_trans hle (Nat.le_of_lt hnear), this⟩

end Run
end Growth