module Deterministic.Equivalence where
open import Category.Monad
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_)
drop-∷ : ∀ {A} {x : A} {xs ys} → x ∷ xs ⊑ x ∷ ys → ♭ xs ⊑ ♭ ys
drop-∷ (x ∷ p) = ♭ p
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
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 ↔))
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))
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))
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)
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
¬¬ : {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
open RawMonad ¬¬-Monad hiding (_⊗_)
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
⇨ : ∀ 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)
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