{-# OPTIONS --safe #-}

-- The budget kₐ + kₜ approximates 4.
-- This means for all 0 < ε < 1 we get kₐ + kₜ + ε ≥ 4.
-- It is sufficient to show that for all N > 0 we show that there is such ε = p/q ≤ 1/N.
-- So, given N we have to find p and q such that Np ≤ q and (kₐ + kₜ)q + p ≥ 4q.
-- With our sequence we get e.g.  kₐ + kₜ ≥ 4 - (14m+10)/(m²+5m+3)  so
-- kₐ + kₜ + (14m+10)/(m²+5m+3) ≥ 4 or
-- (kₐ + kₜ)(m²+5m+3) + (14m+10) ≥ 4(m²+5m+3).
-- Picking q = m²+5m+3 and p = 14m+10 we have to show that Np ≤ q meaning (14m+10)N ≤ m²+5m+3.
-- This gives  m²+(5-14N)m+(3-10N) ≥ 0.
-- The positive root is ½(14N - 5 + √2(14N-5)² + 4(10N-3))) =
-- Guess: m ≥ 14N
-- Testing:
-- (14N)² + 14N(5-14N) - 10N + 3 =
-- (14N)² + 70N - (14N)² - 10N + 3 =
-- 60N + 3 ≥ 0
-- More generally,  (MN)²+MN(5-14N)+(3-10N) ≥ 0.
-- (MN)²+MN(5-14N)+(3-10N) =
-- MMN² - 14MN² + 5MN + 3 - 10N =
-- (M-14)MN² + (5M-10)N + 3 ≥ 0
-- So M ≥ 14N.

-- Given N, with p = 196N + 10 and q = 196N² + 70N + 3 we have Np ≤ q
-- and (kₐ + kₜ)q + p ≥ 4q thanks to our sequence for m=n=14N.

open import Library hiding (m; n)
open import Data.Nat using (NonZero)
open import Tree using (ε; _⨮_)
open import SingleTreeGame using (Moves; ε; moves)
open import Sequence using (seq; thm-seq)
open import ResourcedSingleTreeGame using (rempty; module RMoves)
open import Counting using (MoveCounts; count; C:_T:_R:_; thm-counts-seq)

-- Approximation precision as N goes to +∞.

module Approx (N : ℕ) where

open ℕ
open ≤-Reasoning

p : ℕ
p = N *  + 

q : ℕ
q = N * N *  + N *  + 

-- The precision of the approximation is p/q ≤ 1/N.

Fraction = q ≥ N * p

-- The proof of Fraction follows by simple ≤-Reasoning using the ring solver.

fraction : Fraction
fraction = begin
  N * p
  ≤⟨ m≤m+n (N * p) (N *  + ) ⟩
  N * p + (N *  + )
  ≡⟨ step N ⟩
  q
  ∎
  where
  open ≤-Reasoning

  step : ∀ N → N * (N *  + ) + (N *  + ) ≡ N * N *  + N *  + 
  step = ℕ.solve-∀

-- For the proof of Thm we use the move sequence instantiated to m = n = N * 6.

m : ℕ
m = N * 

n : ℕ
n = N * 

mv : Moves
mv = seq m n ε

open MoveCounts (count mv) public using (c#; t#; r#)

module Proofs
  -- 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))
  where

  -- The goal of this module is to show this theorem:
  Thm = q * (kₐ + kₜ) + p ≥ q * 

  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 m n)

  -- Show lem from (thm-counts m n ε (proj₂ hm))
  lem : c# * kₐ + t# * kₜ ≥ r#
  lem with hmv
  ... | leftover , run =
    begin
      r#
    ≤⟨ m≤m+n r# leftover ⟩
      r# + leftover
    ≤⟨ thm-counts mv  ε run ⟩
      c# * kₐ + (t# * kₜ + )
    ≡⟨ cong (c# * kₐ +_) (+-identityʳ (t# * kₜ)) ⟩
      c# * kₐ + t# * kₜ
    ∎

  lem' : (N *  * (N *  + ) + N *  + ) * kₐ + (N *  * (N *  + ) + N *  + ) * kₜ
         ≥ N *  * ( * (N * ) + ) +  * (N * ) + 
  lem' =
    begin
      N *  * ( * (N * ) + ) +  * (N * ) + 
    ≡⟨ sym (cong MoveCounts.r# (thm-counts-seq m n)) ⟩
      r#
    ≤⟨ lem ⟩
      c# * kₐ + t# * kₜ
    ≡⟨ cong (λ x → x * kₐ + t# * kₜ) (cong MoveCounts.c# (thm-counts-seq m n)) ⟩
      (N *  * (N *  + ) + N *  + ) * kₐ + t# * kₜ
    ≡⟨ cong (λ x → (N *  * (N *  + ) + N *  + ) * kₐ + x * kₜ)
             (cong MoveCounts.t# (thm-counts-seq m n)) ⟩
      (N *  * (N *  + ) + N *  + ) * kₐ + (N *  * (N *  + ) + N *  + ) * kₜ
    ∎

  -- For 6N, c#-exp > q (by 6N), so the original 14N chain (which added 28N·(kₐ+kₜ)
  -- to bridge c# up to q) cannot be reused directly.
  -- We instead multiply both sides of the goal by c#-exp and cancel it again at
  -- the end: from lem' (multiplied by q) we get c#-exp·q·(kₐ+kₜ) ≥ r#-exp·q, and
  -- a small ℕ identity (with slack 6N·p) bridges c#-exp·(q·4) to r#-exp·q + c#-exp·p.

  thm : Thm
  thm = *-cancelˡ-≤ (N *  * (N *  + ) + N *  + ) {{nz}}
    (begin
      (N *  * (N *  + ) + N *  + ) * (q * )
    ≤⟨ m≤m+n ((N *  * (N *  + ) + N *  + ) * (q * )) (N *  * p) ⟩
      (N *  * (N *  + ) + N *  + ) * (q * ) + N *  * p
    ≡⟨ step₁ N ⟩
      (N *  * ( * (N * ) + ) +  * (N * ) + ) * q
        + (N *  * (N *  + ) + N *  + ) * p
    ≤⟨ +-monoˡ-≤ ((N *  * (N *  + ) + N *  + ) * p) (*-monoˡ-≤ q lem') ⟩
      ((N *  * (N *  + ) + N *  + ) * kₐ + (N *  * (N *  + ) + N *  + ) * kₜ) * q
        + (N *  * (N *  + ) + N *  + ) * p
    ≡⟨ step₂ N kₐ kₜ ⟩
      (N *  * (N *  + ) + N *  + ) * (q * (kₐ + kₜ) + p)
    ∎)
    where
    open ≤-Reasoning

    step₁ : ∀ N →
        (N *  * (N *  + ) + N *  + ) * ((N * N *  + N *  + ) * ) + N *  * (N *  + )
      ≡ (N *  * ( * (N * ) + ) +  * (N * ) + ) * (N * N *  + N *  + )
        + (N *  * (N *  + ) + N *  + ) * (N *  + )
    step₁ = ℕ.solve-∀

    step₂ : ∀ N kₐ kₜ →
        ((N *  * (N *  + ) + N *  + ) * kₐ + (N *  * (N *  + ) + N *  + ) * kₜ)
          * (N * N *  + N *  + )
        + (N *  * (N *  + ) + N *  + ) * (N *  + )
      ≡ (N *  * (N *  + ) + N *  + ) * ((N * N *  + N *  + ) * (kₐ + kₜ) + (N *  + ))
    step₂ = ℕ.solve-∀

    nz : NonZero (N *  * (N *  + ) + N *  + )
    nz = subst NonZero (sym (+-suc (N *  * (N *  + ) + N * ) )) _

-- -}