{-# OPTIONS --safe #-}

-- Prove that kₐ + kₜ ≥ 4 (in ℕ) is necessary to execute every move sequence.

open import Library
open import Tree using (ε; _⨮_)
open import SingleTreeGame as Game using (moves)
open import Sequence using (seq; thm-seq)
open import ResourcedSingleTreeGame using (rempty; module RMoves)
open import Counting using (count; C:_T:_R:_)

module Necessary
  -- Budget for concat and tail.
  (kₐ kₜ : ℕ)
  -- We assume that this budget is sufficient to execute any legal move sequence.
  (hyp : ∀ mv t
   → moves mv ε ≡ just t
   → ∃ λ leftover → RMoves.rmoves kₐ kₜ mv rempty ≡ just (leftover ⨮ t))
  -- A move sequence that needs  kₐ + kₜ > 3.
  (let mv = seq   Game.ε)
  -- This sequence has the following move count:
  (let (C: c# T: t# R: r#) = count mv)
  -- Number of R moves r# = 82
  -- Number of C moves c# = 27
  -- Number of T moves t# = 27
  where

open ℕ
open ≤-Reasoning

open RMoves kₐ kₜ

-- The move sequence mv is executable, since very sequence ought to.
hmv : ∃ λ leftover → rmoves mv rempty ≡ just (leftover ⨮ ε)
hmv = hyp mv ε (thm-seq  )

-- The resourced execution needs kₐ * 27 + kₜ * 27 ≥ 82.
-- Note that we do not formulate this as 27 * kₐ + 27 * kₜ ≥ 82
-- because this unfolds to a large expression Agda has problems dealing with.
counts-seq-1-11 : kₐ * c# + kₜ * t# ≥ r#
counts-seq-1-11 with hmv
... | leftover , run =
  begin
    r#
  ≤⟨ m≤n+m r# leftover ⟩
    leftover + r#
  ≤⟨ thm-counts' mv  ε run ⟩
     kₐ * c# + kₜ * t#
  ∎

-- It follows that kₐ + kₜ ≤ 3 is impossible.
thm-op : kₐ + kₜ ≤  →  ≤ 
thm-op h = begin
                  ≤⟨ counts-seq-1-11 ⟩
  kₐ *  + kₜ *   ≡⟨ sym (*-distribʳ-+  kₐ kₜ) ⟩
  (kₐ + kₜ) *      ≤⟨ *-monoˡ-≤  h ⟩
   *             ∎

-- By decidability of ≤, we turn this into a positive statement.
thm : kₐ + kₜ ≥ 
thm with  ≤? kₐ + kₜ
thm | yes p = p
thm | no ¬p = ⊥-elim (n≮n  (thm-op (≮⇒≥ ¬p)))