module stlc.value.properities where

open import stlc.value.equality public

open import stlc.catComb.properities.propA
open import stlc.catComb.properities.propB

open import stlc.monad.impl

--- INJECTIVE ---
≣injective : ∀ {A B s s' t t'} {f : CatComb A B} → ⟨ f ∣ s ⟩= t → ⟨ f ∣ s' ⟩= t' → s ≣ s' → t ≣ t'

--- REFLEXIVE ---
≣refl : ∀ {A} {t : CatCombValue A} → t ≣ t
≣refl {t = ⟨⟩} = unit
≣refl {t = `nat x} = nat
≣refl {t = t , t₁} = pair ≣refl ≣refl
≣refl {t = cur x t} = cur (λ { r x₁ x₂ → ≣injective x₁ x₂ (pair ≣refl (_⇔_.from ≣⇔≣' r)) })
≣refl {t = L t} = inl ≣refl
≣refl {t = R t} = inr ≣refl
≣refl {t = []} = nil
≣refl {t = t ⦂ t₁} = cons ≣refl ≣refl

≣'refl : ∀ {A} {t : CatCombValue A} → t ≣' t
≣'refl {A} = _⇔_.to (≣⇔≣' {A}) ≣refl

--- SYMMETRIC ---
≣sym : ∀ {A} {t t' : CatCombValue A} → t ≣ t' → t' ≣ t
≣'sym : ∀ {A} {t t' : CatCombValue A} → t ≣' t' → t' ≣' t

≣'sym {A} x = _⇔_.to (≣⇔≣' {A}) (≣sym (_⇔_.from (≣⇔≣' {A}) x))

≣sym unit = unit
≣sym nat = nat
≣sym (pair x x₁) = pair (≣sym x) (≣sym x₁)
≣sym (cur {A} x) = cur (λ { x₁ x₂ x₃ → ≣sym (x (≣'sym {A = A} x₁) x₃ x₂)})
≣sym (inl x) = inl (≣sym x)
≣sym (inr x) = inr (≣sym x)
≣sym nil = nil
≣sym (cons x x₁) = cons (≣sym x) (≣sym x₁)

--- TRANSITIVE ---
≣trans : ∀ {A} {t t₁ t₂ : CatCombValue A} → t ≣ t₁ → t₁ ≣ t₂ → t ≣ t₂

≣trans-cur : ∀ {A B C D D₁ s s₁ s₂ s'' s''' t t'} {f : CatComb (C × A) B} {g : CatComb (D × A) B} {g₁ : CatComb (D₁ × A) B} → ⟨ g₁ ∣ s''' , s₂ ⟩= t' → ⟨ f ∣ s , s₁ ⟩= t → s₁ ≣' s₂ → ({s₃ : CatCombValue A} {s₄ : CatCombValue A} {t₁ : CatCombValue B} {t'' : CatCombValue B} → s₃ ≣' s₄ → ⟨ g ∣ s'' , s₃ ⟩= t₁ → ⟨ g₁ ∣ s''' , s₄ ⟩= t'' → t₁ ≣ t'') → ({s₃ : CatCombValue A} {s₄ : CatCombValue A} {t₁ : CatCombValue B} {t'' : CatCombValue B} → s₃ ≣' s₄ → ⟨ f ∣ s , s₃ ⟩= t₁ → ⟨ g ∣ s'' , s₄ ⟩= t'' → t₁ ≣ t'') → t ≣ t'
≣trans-cur {A} {s₂ = s₂} {s'' = s''} {g = g} x x₁ x₂ x₃ x₄ with ⦅ t₁ , ⦅ fst , snd ⦆ ⦆ ← propA g (propB (s'' , s₂)) with e₁ ← x₄ x₂ x₁ fst | e₂ ← x₃ (≣'refl {A = A}) fst x = ≣trans e₁ e₂

≣trans unit unit = unit
≣trans nat nat = nat
≣trans (pair x x₁) (pair y y₁) = pair (≣trans x y) (≣trans x₁ y₁)
≣trans (cur x) (cur x₁) = cur (λ { x₂ x₃ x₄ → ≣trans-cur x₄ x₃ x₂ x₁ x}) --- TODO: use propA
≣trans (inl x) (inl y) = inl (≣trans x y)
≣trans (inr x) (inr y) = inr (≣trans x y)
≣trans nil nil = nil
≣trans (cons x x₁) (cons y y₁) = cons (≣trans x y) (≣trans x₁ y₁)

≣'trans : ∀ {A} {t t₁ t₂ : CatCombValue A} → t ≣' t₁ → t₁ ≣' t₂ → t ≣' t₂
≣'trans {A} x y = _⇔_.to (≣⇔≣' {A}) (≣trans (_⇔_.from (≣⇔≣' {A}) x) (_⇔_.from (≣⇔≣' {A}) y))

--- MICS ---
fmap-≣ : ∀ {A B s s' t t'} → ⟨ fmap {A} {B} ∣ s ⟩= t → ⟨ fmap ∣ s' ⟩= t' → s ≣ s' → t ≣ t'
fmap-≣ ev-fmap-nil ev-fmap-nil (pair _ nil) = nil
fmap-≣ (ev-fmap-cons x x₁) (ev-fmap-cons y y₁) (pair (cur w) (cons z₁ z₂)) = cons (w (_⇔_.to ≣⇔≣' z₁) x₁ y₁) (fmap-≣ x y (pair (cur w) z₂))

concatList-≣ : ∀ {A h h' t t' u u'} → ⟨ concatList {A} ∣ h , t ⟩= u → ⟨ concatList ∣ h' , t' ⟩= u' → h ≣ h' → t ≣ t' → u ≣ u'
concatList-≣ ev-concatList-nil-left ev-concatList-nil-left nil w = w
concatList-≣ (ev-concatList-cons-left x) (ev-concatList-cons-left y) (cons z z₁) w = cons z (concatList-≣ (ev-comp ev-swap x) (ev-comp ev-swap y) z₁ w)

flat-≣ : ∀ {A s s' t t'} → ⟨ flat {A} ∣ s ⟩= t → ⟨ flat ∣ s' ⟩= t' → s ≣ s' → t ≣ t'
flat-≣ ev-flat-nil ev-flat-nil nil = nil
flat-≣ (ev-flat-cons x x₁) (ev-flat-cons y y₁) (cons z z₁) = concatList-≣ x₁ y₁ z (flat-≣ (ev-comp (ev-pair ev-unit ev-id) x) (ev-comp (ev-pair ev-unit ev-id) y) z₁)

≣injective-cont2 : ∀ {A A₁ A₂ B C D R} {s₁ s''' s₂ s₃ s₄ s₅ s₆ s₇ t t'} {f₂ : CatComb (A₁ × B ⇒ R) R} {f₃ : CatComb (A₂ × B ⇒ R) R} {g₁ : CatComb (D × A) ((B ⇒ R) ⇒ R)} {f₁ : CatComb (C × A) ((B ⇒ R) ⇒ R)} → cur f₁ s₁ ≣ cur g₁ s''' → s₃ ≣' s₆ → s₂ ≣' s₅ → ⟨ f₁ ∣ s₁ , s₃ ⟩= cur f₂ s₄ → ⟨ g₁ ∣ s''' , s₆ ⟩= cur f₃ s₇ → ⟨ f₂ ∣ s₄ , s₂ ⟩= t → ⟨ f₃ ∣ s₇ , s₅ ⟩= t' → t ≣' t'
≣injective-cont2 (cur x) x₁ x₂ x₃ x₄ x₅ x₆ with cur y ← x x₁ x₃ x₄ = _⇔_.to ≣⇔≣' (y x₂ x₅ x₆)

≣injective-cont1 : ∀ {A A₁ A₂ B R} {s₁ s₂ : CatCombValue (B ⇒ R)} {t t' : CatCombValue R} {t₁ t'' : CatCombValue (A ⇒ (B ⇒ R) ⇒ R)} {s : CatCombValue A₁} {s'' : CatCombValue A₂} {f g} → s₁ ≣' s₂ → t₁ ≣ t'' → cur f s ≣ cur g s'' → ⟨ f ∣ s , cur (app ∘ ⟨ app ∘ ⟨ p₂ ∘ p₁ ∘ p₁ , p₂ ⟩ , p₂ ∘ p₁ ⟩) (cur f s , t₁ , s₁) ⟩= t → ⟨ g ∣ s'' , cur (app ∘ ⟨ app ∘ ⟨ p₂ ∘ p₁ ∘ p₁ , p₂ ⟩ , p₂ ∘ p₁ ⟩) (cur g s'' , t'' , s₂) ⟩= t' → t ≣ t'
≣injective-cont1 x x₁ (cur x₂) x₃ x₄ = x₂ (λ {x₅ (ev-comp (ev-pair (ev-comp ev-p2p1p1-p2 (ev-app y₂)) (ev-comp ev-p1 ev-p2)) (ev-app y)) (ev-comp (ev-pair (ev-comp ev-p2p1p1-p2 (ev-app z₂)) (ev-comp ev-p1 ev-p2)) (ev-app z)) → ≣injective-cont2 x₁ x₅ x y₂ z₂ y z}) x₃ x₄

≣injective-state : ∀ {A A₁ A₂ A₃ A₄ A₅ B C D E s s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈ s₉ s₁₀ s₁₁ t t'} {f : CatComb (A × B) (C × D)} {f₃ : CatComb (A₁ × B) (C × D)} {f₁ : CatComb (A₂ × D) (C ⇒ E)} {f₄ : CatComb (A₃ × D) (C ⇒ E)} {f₂ : CatComb (A₄ × C) E} {f₅ : CatComb (A₅ × C) E} → s₁ ≣' s₆ → cur f s ≣ cur f₃ s₇ → cur f₁ s₄ ≣ cur f₄ s₁₀ → ⟨ f ∣ s , s₁ ⟩= (s₂ , s₃) → ⟨ f₁ ∣ s₄ , s₃ ⟩= cur f₂ s₅ → ⟨ f₂ ∣ s₅ , s₂ ⟩= t → ⟨ f₃ ∣ s₇ , s₆ ⟩= (s₈ , s₉) → ⟨ f₄ ∣ s₁₀ , s₉ ⟩= cur f₅ s₁₁ → ⟨ f₅ ∣ s₁₁ , s₈ ⟩= t' → t ≣ t'
≣injective-state x (cur x₁) (cur x₂) x₃ x₄ x₅ x₆ x₇ x₈ with (pair y₁ y₂) ← x₁ x x₃ x₆ with cur z ← x₂ (_⇔_.to ≣⇔≣' y₂) x₄ x₇ = z (_⇔_.to ≣⇔≣' y₁) x₅ x₈

≣injective {f = !} ev-unit ev-unit z = ≣refl
≣injective {f = nat x₁} ev-nat ev-nat z = ≣refl
≣injective {f = id} ev-id ev-id z = z
≣injective {f = f ∘ f₁} (ev-comp x x₁) (ev-comp y y₁) z = ≣injective x₁ y₁ (≣injective x y z)
≣injective {f = ⟨ f , f₁ ⟩} (ev-pair x x₁) (ev-pair y y₁) z = pair (≣injective x y z) (≣injective x₁ y₁ z)
≣injective {f = p₁} ev-p1 ev-p1 (pair z z₁) = z
≣injective {f = p₂} ev-p2 ev-p2 (pair z z₁) = z₁
≣injective {f = cur f} ev-cur ev-cur z = cur (λ {s'' x x₁ → ≣injective x x₁ (pair z (_⇔_.from ≣⇔≣' s''))})
≣injective {f = app} (ev-app x) (ev-app y) (pair (cur x₁) z₁) = x₁ (_⇔_.to ≣⇔≣' z₁) x y
≣injective {f = [ f , f₁ ]} (ev-copair1 x) (ev-copair1 y) (pair z (inl z₁)) = ≣injective x y (pair z z₁)
≣injective {f = [ f , f₁ ]} (ev-copair1 x) (ev-copair2 y) (pair z ())
≣injective {f = [ f , f₁ ]} (ev-copair2 x) (ev-copair1 y) (pair z ())
≣injective {f = [ f , f₁ ]} (ev-copair2 x) (ev-copair2 y) (pair z (inr z₁)) = ≣injective x y (pair z z₁)
≣injective {f = i1} ev-i1 ev-i1 z = inl z
≣injective {f = i2} ev-i2 ev-i2 z = inr z
≣injective {f = nil} ev-nil ev-nil unit = nil
≣injective {f = cons} ev-cons ev-cons (pair z z₁) = cons z z₁
≣injective {f = it f f₁} (ev-it-nil x) (ev-it-nil y) (pair z z₁) = ≣injective x y z
≣injective {f = it f f₁} (ev-it-nil x) (ev-it-cons y y₁) (pair z ())
≣injective {f = it f f₁} (ev-it-cons x x₁) (ev-it-nil y) (pair z ())
≣injective {f = it f f₁} (ev-it-cons x x₁) (ev-it-cons y y₁) (pair z (cons z₁ z₂)) = ≣injective x₁ y₁ (pair z (pair z₁ (≣injective x y (pair z z₂))))
≣injective {f = ret {m = exception}} (ev-ret ev-i1) (ev-ret ev-i1) z = inl z
≣injective {f = ret {m = state}} (ev-ret ev-cur) (ev-ret ev-cur) z = cur (λ {x ev-swap ev-swap → pair (_⇔_.from ≣⇔≣' x) z})
≣injective {f = ret {m = nondeterminism}} (ev-ret ev-ret-nondet) (ev-ret ev-ret-nondet) z = cons z nil
≣injective {f = ret {m = continuation}} (ev-ret ev-cur) (ev-ret ev-cur) z = cur (λ {x (ev-comp ev-swap (ev-app x₁)) (ev-comp ev-swap (ev-app x₂)) → _⇔_.from ≣⇔≣' (x (_⇔_.to ≣⇔≣' z) x₁ x₂)})
≣injective {f = bind {s = exception}} (ev-bind (ev-comp ev-swap (ev-copair1 (ev-app x₁)))) (ev-bind (ev-comp ev-swap (ev-copair1 (ev-app y₁)))) (pair (inl z) (cur x)) = x (_⇔_.to ≣⇔≣' z) x₁ y₁
≣injective {f = bind {s = exception}} (ev-bind (ev-comp ev-swap (ev-copair1 x₁))) (ev-bind (ev-comp ev-swap (ev-copair2 y₁))) (pair () z₁)
≣injective {f = bind {s = exception}} (ev-bind (ev-comp ev-swap (ev-copair2 x₁))) (ev-bind (ev-comp ev-swap (ev-copair1 y₁))) (pair () z₁)
≣injective {f = bind {s = exception}} (ev-bind (ev-comp ev-swap (ev-copair2 (ev-comp ev-p2 ev-i2)))) (ev-bind (ev-comp ev-swap (ev-copair2 (ev-comp ev-p2 ev-i2)))) (pair (inr z) x) = inr z
≣injective {f = bind {s = state}} (ev-bind ev-cur) (ev-bind ev-cur) (pair w₁ w₂) = cur (λ {x (ev-bind-state (ev-app y₁) (ev-app y₂) (ev-app y₃)) (ev-bind-state (ev-app z₁) (ev-app z₂) (ev-app z₃)) → ≣injective-state x w₁ w₂ y₁ y₂ y₃ z₁ z₂ z₃})
≣injective {f = bind {s = nondeterminism}} (ev-bind (ev-comp ev-swap (ev-comp x₁ x₂))) (ev-bind (ev-comp ev-swap (ev-comp y₁ y₂))) (pair z₁ z₂) = flat-≣ x₂ y₂ (fmap-≣ x₁ y₁ (pair z₂ z₁))
≣injective {f = bind {s = continuation}} (ev-bind ev-cur) (ev-bind ev-cur) (pair z z₁) = cur (λ { x (ev-bind-cont (ev-app x₁)) (ev-bind-cont (ev-app x₂)) → ≣injective-cont1 x z₁ z x₁ x₂})