{-# OPTIONS --cubical -WnoUnsupportedIndexedMatch #-}
module Dickson where

open import Relation.Binary.PropositionalEquality as PE
open import Data.List
import Data.List as L
open import Data.List.Properties as LP
open import Data.List.Relation.Binary.Pointwise
import Data.List.Relation.Binary.Equality.Propositional as P
import Data.List.Relation.Unary.Linked as RL
import Data.List.Relation.Unary.All as RA
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
import Data.Fin as Fin
import Data.Maybe as M
open import Relation.Nullary hiding (¬_)

open import Cubical.Core.Primitives
import Cubical.Foundations.Prelude as C
open import Cubical.HITs.PropositionalTruncation
import Cubical.HITs.PropositionalTruncation as T

record LocalOperator : Set₁ where
  field
    ∇        : Set → Set
    ∇-return : {A : Set}   → A → ∇ A
    ∇-map    : {A B : Set} → (A → B) → ∇ A → ∇ B
    ∇-join   : {A : Set}   → ∇ (∇ A) → ∇ A
    ∇-isProp : {A : Set}   → C.isProp (∇ A)

¬¬ : (⊥ : Set) → C.isProp ⊥ → LocalOperator
¬¬ ⊥ ⊥-isProp = record
  { ∇        = λ A → (A → ⊥) → ⊥
  ; ∇-return = λ x → λ f → f x
  ; ∇-map    = λ f h → λ k → h (λ x → k (f x))
  ; ∇-join   = λ h k → h (λ z → z k)
  ; ∇-isProp = λ g h i k → ⊥-isProp (g k) (h k) i
  }

module _ {X : Set} {P : X → Set} where
  lookupRA : {xs : List X} → RA.All P xs → (i : Fin.Fin (length xs)) → P (lookup xs i)
  lookupRA (p RA.∷ ps) Fin.zero    = p
  lookupRA (p RA.∷ ps) (Fin.suc i) = lookupRA ps i

  reverseAccRA : {xs ys : List X} → RA.All P xs → RA.All P ys → RA.All P (reverseAcc xs ys)
  reverseAccRA ps RA.[] = ps
  reverseAccRA ps (q RA.∷ qs) = reverseAccRA (q RA.∷ ps) qs

  reverseRA : {xs : List X} → RA.All P xs → RA.All P (reverse xs)
  reverseRA = reverseAccRA RA.[]

module _ where
  subst-zero : {a b : ℕ} → (p : suc a PE.≡ suc b) → subst Fin.Fin p Fin.zero PE.≡ Fin.zero
  subst-zero PE.refl = PE.refl

  subst-suc : {a b : ℕ} → (p : a PE.≡ b) (i : Fin.Fin a) → subst Fin.Fin (cong suc p) (Fin.suc i) PE.≡ Fin.suc (subst Fin.Fin p i)
  subst-suc refl i = PE.refl

  subst-toℕ : {a b : ℕ} (p : a PE.≡ b) (i : Fin.Fin a) → Fin.toℕ (subst Fin.Fin p i) PE.≡ Fin.toℕ i
  subst-toℕ refl i = PE.refl

  lookup-map
    : {X Y : Set} (f : X → Y) (xs : List X) (i : Fin.Fin (length (L.map f xs)))
    → lookup (L.map f xs) i PE.≡ f (lookup xs (subst Fin.Fin (length-map f xs) i))
  lookup-map f (x ∷ xs) Fin.zero rewrite subst-zero (cong suc (length-map f xs)) = PE.refl
  lookup-map f (x ∷ xs) (Fin.suc i) rewrite subst-suc (length-map f xs) i = lookup-map f xs i

module _ {X : Set} {R : X → X → Set} (R-trans : {a b c : X} → R a b → R b c → R a c) where
  transRL : (xs : List X) (i j : Fin.Fin (length xs)) → RL.Linked R xs → i Fin.< j → R (lookup xs i) (lookup xs j)
  transRL (x ∷ .[]) Fin.zero Fin.zero RL.[-] ()
  transRL (x ∷ .[]) Fin.zero (Fin.suc ()) RL.[-] i<j
  transRL (x ∷ y ∷ zs) Fin.zero (Fin.suc Fin.zero) (p RL.∷ ps) i<j = p
  transRL (x ∷ y ∷ zs) Fin.zero (Fin.suc (Fin.suc j)) (p RL.∷ ps) i<j = R-trans p (transRL (y ∷ zs) Fin.zero (Fin.suc j) ps 0<1+n)
  transRL (x ∷ y ∷ zs) (Fin.suc i) (Fin.suc j) (p RL.∷ ps) (s≤s i<j) = transRL (y ∷ zs) i j ps i<j

module Ext {X : Set} (_≼_ : X → X → Set) where
  data _≼⁺_ : M.Maybe X → M.Maybe X → Set where
    here : {a b : X} → a ≼ b → M.just a ≼⁺ M.just b
 
  data _≼*_ : M.Maybe X → M.Maybe X → Set where
    here : {a b : X} → a ≼ b → M.just a ≼* M.just b
    triv : {z : M.Maybe X} → M.nothing ≼* z
 
  inv : {a b : X} → M.just a ≼⁺ M.just b → a ≼ b
  inv (here p) = p

  inv* : {a b : X} → M.just a ≼* M.just b → a ≼ b
  inv* (here p) = p

module _ {X : Set} where
  lookupMaybe : List X → ℕ → M.Maybe X
  lookupMaybe []       n       = M.nothing
  lookupMaybe (x ∷ xs) zero    = M.just x
  lookupMaybe (x ∷ xs) (suc n) = lookupMaybe xs n

  toFun : List X → ℕ → M.Maybe X
  toFun xs n = lookupMaybe (reverse xs) n

  data Ev (P : List X → Set) : List X → Set where
    now    : {xs : List X} → P xs → Ev P xs
    later  : {xs : List X} → ((x : X) → Ev P (x ∷ xs)) → Ev P xs
    squash : {xs : List X} → C.isProp (Ev P xs)

  Ev-map : {P Q : List X → Set} → ((xs : List X) → P xs → Q xs) → {as : List X} → Ev P as → Ev Q as
  Ev-map f (now p) = now (f _ p)
  Ev-map f (later k) = later (λ x → Ev-map f (k x))
  Ev-map f (squash p q i) = squash (Ev-map f p) (Ev-map f q) i

  {-
  Ev-mono : {P : List X → Set} → ({xs ys : List X} → P xs → P (ys ++ xs)) → {as bs : List X} → Ev P as → Ev P (bs ++ as)
  Ev-mono mon (now p) = now (mon p)
  Ev-mono mon (later f) = later (λ x → {!f x!})
  Ev-mono mon (squash p q i) = {!!}
  -}

  module _
    (∇… : LocalOperator)
    (open LocalOperator ∇…)
    (S : List ℕ → Set)
    (S-total : {js : List ℕ} → S js → ∇ (∃[ j ] S (j ∷ js)))
    {P : List X → Set}
    (α : ℕ → X)
    where
    run : {js : List ℕ} → S js → Ev P (L.map α js) → ∇ (∃[ ks ] P (L.map α ks) × S ks)
    run {js} s (now p)        = ∇-return (js , p , s)
    run {js} s (later k)      = ∇-join (∇-map (λ (j , s') → run s' (k (α j))) (S-total s))
    run {js} s (squash p q i) = ∇-isProp (run s p) (run s q) i

  module _ (_≼_ : X → X → Set) where
    open Ext _≼_

    data Ev≼ (P : List X → Set) : List X → Set where
      now    : {xs : List X} → P xs → Ev≼ P xs
      later  : {xs : List X} → ((x : X) → L.head xs ≼* M.just x → Ev≼ P (x ∷ xs)) → Ev≼ P xs
      squash : {xs : List X} → C.isProp (Ev≼ P xs)

    module _
      (∇… : LocalOperator)
      (open LocalOperator ∇…)
      (S : List ℕ → Set)
      (S-total : {js : List ℕ} → S js → ∇ (∃[ j ] S (j ∷ js)))
      {P : List X → Set}
      (α : ℕ → X)
      (α-monotonic-on-S : {j : ℕ} {js : List ℕ} → S (j ∷ js) → L.head (L.map α js) ≼* M.just (α j))
      where
      run≼ : {js : List ℕ} → S js → Ev≼ P (L.map α js) → ∇ (∃[ ks ] P (L.map α ks) × S ks)
      run≼ {js} s (now p)        = ∇-return (js , p , s)
      run≼ {js} s (later k)      = ∇-join (∇-map (λ (j , s') → run≼ s' (k (α j) (α-monotonic-on-S s'))) (S-total s))
      run≼ {js} s (squash p q i) = ∇-isProp (run≼ s p) (run≼ s q) i

module _ {X : Set} (_≼_ : X → X → Set) where
  open Ext _≼_

  Good : List X → Set
  -- Good xs = ∃[ i ] ∃[ j ] i < j × toFun xs i ≼⁺ toFun xs j
  Good xs = ∃[ i ] ∃[ j ] j Fin.< i × lookup xs i ≼ lookup xs j

  GoodM : List X → Set
  GoodM xs = ∃[ i ] ∃[ j ] i < j × toFun xs i ≼⁺ toFun xs j

  TripleM : List X → Set
  TripleM xs = ∃[ i ] ∃[ j ] ∃[ k ] i < j × j < k × toFun xs i ≼⁺ toFun xs j × toFun xs j ≼⁺ toFun xs k

  Triple' : List X → Set
  Triple' xs = ∃[ i ] ∃[ j ] ∃[ k ] k Fin.< j × j Fin.< i × lookup xs i ≼ lookup xs j × lookup xs j ≼ lookup xs k

module Progress
  {X : Set}
  (_≼_ : X → X → Set)
  (well : Ev (Good _≼_) [])
  where

  module Classical (α : ℕ → X) (⊥ : Set) (⊥-isProp : C.isProp ⊥) where
    infix  ¬_
    ¬_ : Set → Set
    ¬ A = A → ⊥

    Happy : ℕ → Set
    Happy m = ∃[ k ] k > m × α m ≼ α k

    Sad : ℕ → Set
    Sad m = ¬ Happy m

    open Ext _<_ using (triv; here) renaming (_≼*_ to _<*_)

    ∇… : LocalOperator
    ∇… = ¬¬ ⊥ ⊥-isProp
    open LocalOperator ∇…

    choose
      : (Q : ℕ → Set)
      → (unbounded : (n : ℕ) → ∇ (∃[ m ] m ≥ n × Q m))
      → (β : ℕ → X) {R : List X → Set}
      → Ev R [] → ∇ (∃[ ks ] R (L.map β ks) × RL.Linked _>_ ks × RA.All Q ks)
    choose Q unbounded β p = run ∇… S S-total β (RL.[] , RA.[]) p
      where
      -- S xs meint: xs ist strikt aufsteigende Folge (rückwärts
      -- gelesen) aus lauter Q-Indizes.
      S : List ℕ → Set
      S ks = RL.Linked _>_ ks × RA.All Q ks

      S-total : {js : List ℕ} → S js → ∇ (∃[ j ] S (j ∷ js))
      S-total {[]}     s = ∇-map (λ (m , m≥0 , sad) → m , RL.[-] , sad RA.∷ (snd s)) (unbounded )
      S-total {j ∷ js} s = ∇-map (λ (m , m>j , sad) → m , m>j RL.∷ (proj₁ s) , sad RA.∷ (snd s)) (unbounded (suc j))

    lemma : ((n : ℕ) → ∇ (∃[ m ] m ≥ n × Sad m)) → ⊥
    lemma unbounded = choose Sad unbounded α well λ (ks , g , s) → paradoxical g s
      where
      -- α (lookup (reverse ks) i~) PE.≡ lookup (reverse (L.map α ks)) i
      paradoxical : {ks : List ℕ} → Good _≼_ (L.map α ks) → RL.Linked _>_ ks × RA.All Sad ks → ⊥
      paradoxical {ks} (i , j , j<i , u≼v) s
        rewrite lookup-map α ks i
        rewrite lookup-map α ks j
        rewrite sym (subst-toℕ (length-map α ks) i)
        rewrite sym (subst-toℕ (length-map α ks) j)
        = lookupRA (snd s) i~ ((lookup ks j~) , (transRL {ℕ} {_>_} (λ p q → <-trans q p) ks j~ i~ (fst s) j<i , u≼v))
        where
        i~ : Fin.Fin (length ks)
        i~ = subst Fin.Fin (length-map α ks) i
        j~ : Fin.Fin (length ks)
        j~ = subst Fin.Fin (length-map α ks) j
      {-
        j~ : Fin.Fin (length (reverse ks))
        j~ = subst Fin.Fin (PE.trans (PE.trans (length-reverse (L.map α ks)) (length-map α ks)) (PE.sym (length-reverse ks)) ) j
        i' = lookup (reverse ks) i
        j' = lookup (reverse ks) j
        dann Sad i' und i' < j', aber α i' ≼ α j' im Widerspruch zu Sad i'
      -}

    potentially-almost-all-happy : ∇ (∃[ a ] ((b : ℕ) → b ≥ a → ∇ (Happy b)))
    potentially-almost-all-happy f = lemma λ n → λ z → f (n , (λ m m≥n sad → z (m , m≥n , sad)))

    module _ (P : List X → Set) where
      go : (a : ℕ) → ((b : ℕ) → b ≥ a → ∇ (Happy b)) → Ev≼ _≼_ P [] → ∇ (∃[ ks ] P (L.map α ks) × RL.Linked _>_ ks)
      go a almost-all-happy p = ∇-map (λ (ks , pr , s) → ks , pr , proj₁ s) (run≼ _≼_ ∇… S S-total α α-monotonic-on-S (RL.[] , RL.[] , RA.[] , RA.[]) p)
        where
        S : List ℕ → Set
        S ks = RL.Linked _>_ ks × RL.Linked (λ i j → α j ≼ α i) ks × RA.All Happy ks × RA.All (a ≤_) ks

        S-total : {js : List ℕ} → S js → ∇ (∃[ j ] S (j ∷ js))
        S-total {[]}     s = ∇-map (λ happy → a , RL.[-] , RL.[-] , happy RA.∷ RA.[] , ≤-refl RA.∷ RA.[]) (almost-all-happy a ≤-refl)
        S-total {j ∷ js} (linked> , linked≽ , (k , k>j , αj≼αk) RA.∷ all-happy , j≥a RA.∷ all-≥a) = ∇-map (λ k-happy → k , (k>j RL.∷ linked>) , ((αj≼αk RL.∷ linked≽) , ((k-happy RA.∷ (k , k>j , αj≼αk) RA.∷ all-happy) , ((≤-trans j≥a (<⇒≤ k>j)) RA.∷ (j≥a RA.∷ all-≥a))))) (almost-all-happy k (≤-trans j≥a (<⇒≤ k>j))) 

        α-monotonic-on-S : {j : ℕ} {js : List ℕ} → S (j ∷ js) → (_≼_ Ext.≼* L.head (L.map α js)) (M.just (α j))
        α-monotonic-on-S {j} {[]} (fst₁ , snd₁) = Ext.triv
        α-monotonic-on-S {j} {k ∷ js} (_ , p RL.∷ _ , _) = Ext.here p

      qed : Ev≼ _≼_ P [] → ∇ (∃[ ks ] P (L.map α ks) × RL.Linked _>_ ks)
      qed p = ∇-join (∇-map (λ (a , almost-all-happy) → go a almost-all-happy p) potentially-almost-all-happy)

  module _ (P : List X → Set) (α : ℕ → X) where
    Claim : Set
    Claim = ∥ ∃[ ks ] P (L.map α ks) × RL.Linked _>_ ks ∥₁

    thm : Ev≼ _≼_ P [] → Claim
    thm p = qed P p ∣_∣₁
      where
      open Classical α Claim isPropPropTrunc

module Example
  {X : Set}
  (_≼_ : X → X → Set)
  (well : Ev (Good _≼_) [])
  where

  open Ext _≼_

  eventually≼-triple : Ev≼ _≼_ (TripleM _≼_) []
  eventually≼-triple = later λ x _ → later λ y x≼y → later λ z y≼z → now ( ,  ,  , (s≤s z≤n) , ((s≤s (s≤s z≤n)) , (here (inv* x≼y)  , here (inv* y≼z))))

  have-triple : (α : ℕ → X) → ∥ ∃[ ks ] TripleM _≼_ (L.map α ks) × RL.Linked _>_ ks ∥₁
  have-triple α = thm (TripleM _≼_) α eventually≼-triple
    where
    open Progress _≼_ well

module Ex where
  {-# TERMINATING #-}
  go : (cruft : List ℕ) → (n : ℕ) → Ev (Good _≤_) (n ∷ cruft)
  f : (cruft : List ℕ) (n m : ℕ) → Ev (Good _≤_) (m ∷ suc n ∷ cruft)

  go cruft zero    = later (λ m → now (Fin.suc Fin.zero , Fin.zero , s≤s z≤n , z≤n))
  go cruft (suc n) = later (f cruft n)

  f cruft n m with suc n ≤? m
  ... | yes 1+n≤m = now (Fin.suc Fin.zero , Fin.zero , s≤s z≤n , 1+n≤m)
  ... | no  1+n≰m = go (suc n ∷ cruft) m

  ℕ-well : Ev (Good _≤_) []
  ℕ-well = later (go [])

  open Example _≤_ ℕ-well

  α₀ : ℕ → ℕ
  α₀  = 
  α₀  = 
  α₀  = 
  α₀  = 
  α₀  = 
  α₀  = 
  α₀  = 
  α₀ _ = 

  ex = have-triple α₀

  ex' = T.map (λ (ks , _) → L.map α₀ ks) ex

{-
module Spam {X : Set} (_≼_ : X → X → Set) (well : Ev (GoodM _≼_) [])
  where

  open Ext _≼_

  add : {xs : List X} (ys : List X) → Fin.Fin (length xs) → Fin.Fin (length (ys ++ xs))
  add {xs} ys n = subst Fin.Fin (PE.sym (length-++ ys)) (length ys Fin.↑ʳ n)

  postulate
    ultra-well : (xs : List X) → Ev (GoodM _≼_) xs

  module Classical (⊥ : List X → Set) (⊥-isProp : (xs : List X) → C.isProp (⊥ xs)) where
    Sad : (xs : List X) → ℕ → Set
    Sad xs i = (ys : List X) → (j : ℕ) → i < j → toFun (ys ++ xs) i ≼⁺ toFun (ys ++ xs) j → ⊥ (ys ++ xs)

{-
    module _ (xs : List X) (no-good-triple : (ys : List X) → TripleM _≼_ (ys ++ xs) → ⊥ (ys ++ xs)) where
      unbounded : Ev (λ xs' → ∃[ i ] Sad xs' i) xs
      unbounded = Ev-map {!!} (ultra-well xs)
        where
        recognize : (ys : List X) → GoodM _≼_ (ys ++ xs) → ∃[ j ] Sad (ys ++ xs) j
        recognize ys (i , j , i<j , u≼v) = j , go
          where
          go : (zs : List X) → (k : ℕ) → (j<k : j < k) → (v≼w : toFun (zs ++ ys ++ xs) j ≼⁺ toFun (zs ++ ys ++ xs) k) → ⊥ (zs ++ ys ++ xs)
          go zs k j<k v≼w
            rewrite sym (++-assoc zs ys xs)
            = no-good-triple (zs ++ ys)
              ( i
              , j
              , k
              , i<j
              , j<k
              , {!!}  -- im Wesentlichen u≼v
              , v≼w
              )
-}

    module _ (no-good-triple : (ys : List X) → TripleM _≼_ ys → ⊥ ys) where
      unbounded : Ev (λ xs' → ∃[ i ] Sad xs' i) []
      unbounded = Ev-map recognize well
        where
        recognize : (ys : List X) → GoodM _≼_ ys → ∃[ j ] Sad ys j
        recognize ys (i , j , i<j , u≼v) = j , go
          where
          go : (zs : List X) → (k : ℕ) → (j<k : j < k) → (v≼w : toFun (zs ++ ys) j ≼⁺ toFun (zs ++ ys) k) → ⊥ (zs ++ ys)
          go zs k j<k v≼w
            rewrite sym (++-assoc zs ys [])
            = no-good-triple (zs ++ ys)
              ( i
              , j
              , k
              , i<j
              , j<k
              , {!!}  -- im Wesentlichen u≼v
              , v≼w
              )

-}