```------------------------------------------------------------------------
-- The various approaches are equivalent (at least classically)
------------------------------------------------------------------------

module Deterministic.Equivalence where

open import Coinduction
import Data.BoundedVec.Inefficient as BVec
open import Data.Colist as Colist hiding ([_])
open import Data.Empty
open import Data.Fin
open import Data.Fin.Dec
open import Data.Fin.Props
open import Function
open import Function.Equality using (_⟨\$⟩_)
open import Function.Equivalence
using (equivalent; module Equivalent) renaming (_∘_ to _⟨∘⟩_)
open import Data.List using (List; []; _∷_; [_])
open import Data.Maybe
open import Data.Nat
open import Data.Product renaming (map to _⊗_)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Negation

open import Deterministic.Expr
open import Deterministic.EasyToWorkWith
renaming (_HasTrace_ to _HasTraceW_)
open import Deterministic.EasyToUnderstand
renaming (_HasTrace_ to _HasTraceU_)
open import Deterministic.LongestPrefix
renaming (_HasTrace_ to _HasTraceL_)
open import Deterministic.ShortestExtension
renaming (_HasTrace_ to _HasTraceS_)

------------------------------------------------------------------------
-- A lemma

drop-∷ : ∀ {A} {x : A} {xs ys} → x ∷ xs ⊑ x ∷ ys → ♭ xs ⊑ ♭ ys
drop-∷ (x ∷ p) = ♭ p

------------------------------------------------------------------------
-- EasyToWorkWith to EasyToUnderstand

WtoU : ∀ {e ms} → e HasTraceW ms → e HasTraceU ms
WtoU s i m = equivalent (⇒ _ i s) (⇐ s)
where
⇒ : ∀ ms {m e} i → e HasTraceW ms → ms ⟨ i ⟩= m → e [ i ]= m
⇒ []       i       s        ()
⇒ (m ∷ ms) i       (nop  s) eq   = nop (⇒ (m ∷ ms) i s eq)
⇒ (m ∷ ms) zero    (tick s) refl = tick-zero
⇒ (m ∷ ms) (suc i) (tick s) eq   = tick-suc (⇒ (♭ ms) i (♭ s) eq)

⇐ : ∀ {m ms e i} → e HasTraceW ms → e [ i ]= m → ms ⟨ i ⟩= m
⇐ (nop  s) (nop x)      = ⇐ (♭? s) x
⇐ (tick s) tick-zero    = refl
⇐ (tick s) (tick-suc x) = ⇐ (♭ s) x

------------------------------------------------------------------------
-- EasyToUnderstand to EasyToWorkWith

drop-nopU : ∀ {e i m} → nop e [ i ]= m → ♭ e [ i ]= m
drop-nopU (nop x) = x

nop-lemmaU : ∀ {e ms} → nop e HasTraceU ms → ♭ e HasTraceU ms
nop-lemmaU ↔ i m = equivalent drop-nopU nop ⟨∘⟩ ↔ i m

drop-tick-sucU : ∀ {m m′ e i} → tick m e [ suc i ]= m′ → ♭ e [ i ]= m′
drop-tick-sucU (tick-suc x) = x

tick-lemmaU : ∀ {e m ms} →
tick m e HasTraceU m ∷ ms → ♭ e HasTraceU ♭ ms
tick-lemmaU ↔ i m = equivalent drop-tick-sucU tick-suc ⟨∘⟩ ↔ (suc i) m

mutual

UtoW : ∀ ms e → e HasTraceU ms → e HasTraceW ms
UtoW (m ∷ ms)   e  ↔ = UtoW′ e ↔ (Equivalent.to (↔ 0 m) ⟨\$⟩ refl)
UtoW [] (tick m e) ↔ with Equivalent.from (↔ 0 m) ⟨\$⟩ tick-zero
UtoW [] (tick m e) ↔ | ()
UtoW [] (nop    e) ↔ = nop (♯ UtoW [] (♭ e) (nop-lemmaU ↔))

UtoW′ : ∀ {m ms} e →
e HasTraceU m ∷ ms → e [ 0 ]= m → e HasTraceW m ∷ ms
UtoW′ (nop    e) ↔ (nop x) = nop (UtoW′ (♭ e) (nop-lemmaU ↔) x)
UtoW′ (tick m e) ↔ _       with Equivalent.from (↔ 0 m) ⟨\$⟩ tick-zero
UtoW′ (tick m e) ↔ _       | refl =
tick (♯ UtoW _ (♭ e) (tick-lemmaU ↔))

------------------------------------------------------------------------
-- EasyToWorkWith to LongestPrefix

WtoL : ∀ {e ms} → e HasTraceW ms → e HasTraceL ms
WtoL s = equivalent (longest s) (prefix _ s)
where
longest : ∀ {e ms p} →
e HasTraceW ms → p ⊑Trace[ e ] → fromList p ⊑ ms
longest s        []       = []
longest (nop  s) (nop  x) = longest (♭? s) x
longest (tick s) (tick x) = _ ∷ (♯ longest (♭ s) x)

prefix : ∀ {e ms} p →
e HasTraceW ms → fromList p ⊑ ms → p ⊑Trace[ e ]
prefix []      s        pr        = []
prefix (m ∷ p) (nop  s) (.m ∷ pr) = nop (prefix (m ∷ p) s (m ∷ pr))
prefix (m ∷ p) (tick s) (.m ∷ pr) = tick (prefix p (♭ s) (♭ pr))

------------------------------------------------------------------------
-- LongestPrefix to EasyToWorkWith

nop-lemmaL : ∀ {e ms} → nop e HasTraceL ms → ♭ e HasTraceL ms
nop-lemmaL s = s ⟨∘⟩ equivalent nop drop-nop
where
drop-nop : ∀ {ms e} → ms ⊑Trace[ nop e ] → _
drop-nop []      = []
drop-nop (nop x) = x

tick-lemmaL : ∀ {m e ms} →
tick m e HasTraceL m ∷ ms → ♭ e HasTraceL ♭ ms
tick-lemmaL {m} s =
equivalent drop-∷ (λ x → m ∷ ♯ x) ⟨∘⟩ s ⟨∘⟩ equivalent tick drop-tick
where
drop-tick : ∀ {ms e} → m ∷ ms ⊑Trace[ tick m e ] → ms ⊑Trace[ ♭ e ]
drop-tick (tick x) = x

mutual

LtoW : ∀ e ms → e HasTraceL ms → e HasTraceW ms
LtoW (nop e)     []       s = nop (♯ LtoW (♭ e) [] (nop-lemmaL s))
LtoW (nop e)     (m ∷ ms) s = LtoW′ s (Equivalent.from s ⟨\$⟩ m ∷ ♯ [])
LtoW (tick m  e) []       s with Equivalent.to s ⟨\$⟩ tick []
LtoW (tick m  e) []       s | ()
LtoW (tick m′ e) (m ∷ ms) s with Equivalent.from s ⟨\$⟩ m ∷ ♯ []
LtoW (tick .m e) (m ∷ ms) s | tick x =
tick (♯ LtoW (♭ e) (♭ ms) (tick-lemmaL s))

LtoW′ : ∀ {e m ms} →
e HasTraceL m ∷ ms → [ m ] ⊑Trace[ e ] → e HasTraceW m ∷ ms
LtoW′ s (nop x)  = nop (LtoW′ (nop-lemmaL s) x)
LtoW′ s (tick x) = tick (♯ LtoW _ _ (tick-lemmaL s))

------------------------------------------------------------------------
-- EasyToWorkWith to ShortestExtension

WtoS : ∀ {e ms} → e HasTraceW ms → e HasTraceS ms
WtoS s = (shortest s , λ {_} → prefix s)
where
shortest : ∀ {e ms} → e HasTraceW ms → Trace[ e ]⊑ ms
shortest (nop  s) = nop  (♯ shortest (♭? s))
shortest (tick s) = tick (♯ shortest (♭  s))

prefix : ∀ {ms p e} → e HasTraceW ms → Trace[ e ]⊑ p → ms ⊑ p
prefix {[]}    (nop  s) (nop  x) = []
prefix {_ ∷ _} (nop  s) (nop  x) = prefix s (♭ x)
prefix         (tick s) (tick x) = _ ∷ ♯ prefix (♭ s) (♭ x)

------------------------------------------------------------------------
-- ShortestExtension to EasyToUnderstand

-- One direction is easy.

nop-lemmaS : ∀ {e ms} → nop e HasTraceS ms → ♭ e HasTraceS ms
nop-lemmaS {e} {ms} s = (drop-nop (proj₁ s) , λ p → proj₂ s (nop (♯ p)))
where
drop-nop : Trace[ nop e ]⊑ ms → Trace[ ♭ e ]⊑ ms
drop-nop (nop x) = ♭ x

tick-lemmaS : ∀ {m e ms} →
tick m e HasTraceS m ∷ ms → ♭ e HasTraceS ♭ ms
tick-lemmaS {m} {e} {ms} s =
(drop-tick (proj₁ s) , λ p → drop-∷ (proj₂ s (tick {ms = ♯ _} (♯ p))))
where
drop-tick : Trace[ tick m e ]⊑ m ∷ ms → Trace[ ♭ e ]⊑ ♭ ms
drop-tick (tick x) = ♭ x

⇦ : ∀ {m ms i} e → e HasTraceS ms → e [ i ]= m → ms ⟨ i ⟩= m
⇦ (nop    e) s (nop x)      = ⇦ (♭ e) (nop-lemmaS s) x
⇦ (tick m e) s x            with proj₁ s
⇦ (tick m e) s tick-zero    | tick _ = refl
⇦ (tick m e) s (tick-suc x) | tick _ = ⇦ (♭ e) (tick-lemmaS s) x

-- The other direction is more complicated (at least this particular
-- proof). Given e HasTraceS ms, where ms is non-empty, it appears to
-- be impossible to define an Agda function which computes where in e
-- the first tick is (the naive implementation of the function would
-- probably be correct, but Agda's termination checker would not
-- accept it). Hence the statement of the desired result has been
-- weakened by using double-negation.

¬¬ : {A : Set} {B : A → Set} {T : (x : A) → B x → Set} (P : Set) →
P ≡ (∀ x y → T x y) → Set
¬¬ {T = T} .(∀ x y → T x y) refl = ∀ x y → ¬ ¬ T x y

StoU-statement : Set
StoU-statement = ∀ e ms → e HasTraceS ms → ¬¬ (e HasTraceU ms) refl

-- A key lemma.

prefix : ∀ e i p →
((j : Fin i) → ∃ λ m → p ⟨ toℕ j ⟩= m × e [ toℕ j ]= m) →
(∄ λ m → e [ i ]= m) →
Trace[ e ]⊑ p
prefix (nop e) i p hyp₁ hyp₂ =
nop (♯ prefix (♭ e) i p (id ⊗ (id ⊗ drop-nopU) ∘ hyp₁)
(hyp₂ ∘ (id ⊗ nop)))
prefix (tick m e) zero    p        hyp₁ hyp₂ = ⊥-elim (hyp₂ (, tick-zero))
prefix (tick m e) (suc i) p        hyp₁ hyp₂ with hyp₁ zero
prefix (tick m e) (suc i) []       hyp₁ hyp₂ | (_ , () , _)
prefix (tick m e) (suc i) (.m ∷ p) hyp₁ hyp₂ | (.m , refl , tick-zero) =
tick (♯ prefix (♭ e) i (♭ p)
((id ⊗ (id ⊗ drop-tick-sucU)) ∘ hyp₁ ∘ suc)
(hyp₂ ∘ (id ⊗ tick-suc)))

toColist : ∀ {A n} → BVec.BoundedVec A n → Colist A
toColist = Colist.fromList ∘ BVec.toList

take-lemma₁ : ∀ {A n} (i : Fin (suc n)) (xs : Colist A) {x} →
xs ⟨ n ⟩= x → ¬ xs ⊑ toColist (take (toℕ i) xs)
take-lemma₁ i             []       () p
take-lemma₁ zero          (x ∷ xs) eq ()
take-lemma₁ (suc zero)    (x ∷ xs) eq (.x ∷ p) with ♭ xs | ♭ p
take-lemma₁ (suc zero)    (x ∷ xs) () (.x ∷ p) | .[] | []
take-lemma₁ (suc (suc i)) (x ∷ xs) eq (.x ∷ p) =
take-lemma₁ (suc i) (♭ xs) eq (♭ p)

take-lemma₂ : ∀ {A x} n (xs : Colist A) (i : Fin n) →
xs ⟨ toℕ i ⟩= x → toColist (take n xs) ⟨ toℕ i ⟩= x
take-lemma₂ zero    xs       ()      eq
take-lemma₂ (suc n) []       i       eq = eq
take-lemma₂ (suc n) (x ∷ xs) zero    eq = eq
take-lemma₂ (suc n) (x ∷ xs) (suc i) eq =
take-lemma₂ n (♭ xs) i eq

-- The other direction.

⇨ : ∀ e n ms m → e HasTraceS ms → ms ⟨ n ⟩= m → ¬ ¬ e [ n ]= m
⇨ e n ms m s eq =
sequence rawIApplicative (λ _ → excluded-middle) >>= λ dec →
call/cc {Whatever = ⊥} λ ¬x →
const \$ helper \$ ¬∀⟶∃¬-smallest (suc n) P dec (∃¬⟶¬∀ (¬P ¬x))
where
P : Fin (suc n) → Set
P = λ i → ∃ λ m → e [ toℕ i ]= m

¬P : ¬ e [ n ]= m → ∃ λ i → ¬ P i
¬P ¬x = (fromℕ n , helper ∘ lem)
where
helper : ∄ λ m → e [ n ]= m
helper (m′ , x) with lookup n ms | eq | ⇦ e s x
helper (.m , x) | .(just m) | refl | refl = ¬x x

lem = id ⊗ λ {m} → subst (λ n → e [ n ]= m) (to-from n)

helper : ∄ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
helper (i , ¬x , smallest) = take-lemma₁ i ms eq is-prefix
where
ms′ : Trace
ms′ = toColist (take (toℕ i) ms)

all-defined :
(j : Fin′ i) → ∃ λ m → ms′ ⟨ toℕ j ⟩= m × e [ toℕ j ]= m
all-defined j with toℕ (inject j) | inject-lemma j | smallest j
all-defined j | .(toℕ j) | refl | (m′ , x) =
(m′ , take-lemma₂ (toℕ i) ms j (⇦ e s x) , x)

-- Note the use of proj₂ s here.

is-prefix : ms ⊑ ms′
is-prefix = proj₂ s (prefix e (toℕ i) ms′ all-defined ¬x)

StoU : StoU-statement
StoU e ms s i m =
(λ x → equivalent x (⇦ e s)) <\$> ¬¬-pull (_ ⇒ Id) (⇨ e i ms m s)
where open import Relation.Nullary.Universe
```