```------------------------------------------------------------------------
-- Lemmas about the initial bag index
------------------------------------------------------------------------

module TotalParserCombinators.InitialBag where

open import Data.List
import Data.List.Effectful
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Membership.Propositional.Properties as M
hiding (⊛-∈↔)
open import Data.List.Relation.Binary.BagAndSetEquality
using () renaming (_∼[_]_ to _List-∼[_]_)
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.Any.Properties
open import Data.Maybe hiding (_>>=_)
open import Data.Product
open import Data.Sum
open import Function.Base
open import Function.Equality using (_⟨\$⟩_)
open import Function.Inverse as Inv using (_↔_)
import Function.Related as Related
open import Level
open import Relation.Binary.PropositionalEquality as P
using (_≡_; refl)
open import Relation.Binary.HeterogeneousEquality as H
using (refl) renaming (_≅_ to _≅′_)

open Inv.Inverse
using () renaming (_⊛_ to _⊛′_)
open Related using (SK-sym)

open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics

------------------------------------------------------------------------
-- Optimisation

private

abstract

⊛-∈↔ : ∀ {A B : Set} (fs : List (A → B)) {xs y} →
(∃₂ λ f x → f ∈ fs × x ∈ xs × y ≡ f x) ↔ y ∈ (fs ⊛′ xs)
⊛-∈↔ = M.⊛-∈↔

------------------------------------------------------------------------
-- Sanity check: The initial set index is correctly defined

mutual

complete : ∀ {Tok R xs x} {p : Parser Tok R xs} →
x ∈ p · [] → x ∈ xs
complete x∈p = complete′ x∈p refl

private

complete′ : ∀ {Tok R xs x s} {p : Parser Tok R xs} →
x ∈ p · s → s ≡ [] → x ∈ xs
complete′ return                                                    refl = to pure↔              ⟨\$⟩ refl
complete′ (∣-left      x∈p₁)                                        refl = to ++↔                ⟨\$⟩ inj₁ (complete x∈p₁)
complete′ (∣-right xs₁ x∈p₂)                                        refl = to (++↔ {P = _≡_ _}
{xs = xs₁})   ⟨\$⟩ inj₂ (complete x∈p₂)
complete′ (<\$> x∈p)                                                 refl = to (map-∈↔ _)         ⟨\$⟩ (_ , complete x∈p , refl)
complete′ (_⊛_   {s₁ = []} {xs = just _}                f∈p₁ x∈p₂)  refl = to (⊛-∈↔ _)           ⟨\$⟩ (_ , _ , complete f∈p₁
, complete x∈p₂ , refl)
complete′ (_>>=_ {s₁ = []} {xs = just xs} {f = just _}  x∈p₁ y∈p₂x) refl = to (>>=-∈↔ {xs = xs}) ⟨\$⟩ (_ , complete x∈p₁
, complete y∈p₂x)
complete′ (cast {xs₁≈xs₂ = xs₁≈xs₂} x∈p)                            refl = to xs₁≈xs₂            ⟨\$⟩ complete x∈p

complete′ (_⊛_   {s₁ = []} {xs = nothing}               f∈p₁ x∈p₂)  refl with complete x∈p₂
... | ()
complete′ (_>>=_ {s₁ = []} {xs = nothing}               x∈p₁ y∈p₂x) refl with complete x∈p₁
... | ()
complete′ (_>>=_ {s₁ = []} {xs = just _}  {f = nothing} x∈p₁ y∈p₂x) refl with complete y∈p₂x
... | ()

complete′ token                     ()
complete′ (_⊛_    {s₁ = _ ∷ _} _ _) ()
complete′ (_>>=_  {s₁ = _ ∷ _} _ _) ()
complete′ (nonempty _)              ()

mutual

sound : ∀ {Tok R xs x} (p : Parser Tok R xs) →
x ∈ xs → x ∈ p · []
sound (return x)              (here refl) = return
sound (_∣_ {xs₁ = xs₁} p₁ p₂) x∈xs with from (++↔ {P = _≡_ _} {xs = xs₁}) ⟨\$⟩ x∈xs
... | inj₁ x∈xs₁ = ∣-left      (sound p₁ x∈xs₁)
... | inj₂ x∈xs₂ = ∣-right xs₁ (sound p₂ x∈xs₂)
sound (f <\$> p) x∈xs with from (map-∈↔ f) ⟨\$⟩ x∈xs
... | (y , y∈xs , refl) = <\$> sound p y∈xs
sound (_⊛_ {fs = fs} {just xs} p₁ p₂) y∈ys
with from (⊛-∈↔ (flatten fs) {xs = xs}) ⟨\$⟩ y∈ys
sound (_⊛_ {fs = nothing} {just xs} p₁ p₂)  y∈ys | (f′ , x′ , ()    , x′∈xs , refl)
sound (_⊛_ {fs = just fs} {just xs} p₁ p₂)  y∈ys | (f′ , x′ , f′∈fs , x′∈xs , refl) =
_⊛_ {fs = ○} {xs = ○} (sound p₁ f′∈fs) (sound p₂ x′∈xs)
sound (_>>=_ {xs = zs} {f = just f} p₁ p₂) y∈ys
with from (>>=-∈↔ {xs = flatten zs} {f = f}) ⟨\$⟩ y∈ys
... | (x , x∈zs , y∈fx) =
_>>=_ {xs = zs} {f = just f} (sound p₁ x∈zs) (sound′ (p₂ x) x∈zs y∈fx)
sound (cast xs₁≈xs₂ p) x∈xs = cast (sound p (from xs₁≈xs₂ ⟨\$⟩ x∈xs))

sound (return _)                 (there ())
sound fail                       ()
sound token                      ()
sound (_⊛_   {xs = nothing} _ _) ()
sound (_>>=_ {f  = nothing} _ _) ()
sound (nonempty _)               ()

private

sound′ : ∀ {Tok R₁ R₂ x y xs} {zs : Maybe (List R₁)}
(p : ∞⟨ zs ⟩Parser Tok R₂ xs) →
x ∈ flatten zs → y ∈ xs → y ∈ ♭? p · []
sound′ {zs = just _}  p _  = sound p
sound′ {zs = nothing} p ()

mutual

sound∘complete : ∀ {Tok R xs x} {p : Parser Tok R xs}
(x∈p : x ∈ p · []) →
sound p (complete x∈p) ≡ x∈p
sound∘complete x∈p = H.≅-to-≡ (sound∘complete′ x∈p refl)

private

sound∘complete′ : ∀ {Tok R xs x s} {p : Parser Tok R xs}
(x∈p : x ∈ p · s) (s≡[] : s ≡ []) →
sound p (complete′ x∈p s≡[]) ≅′ x∈p
sound∘complete′ return                                refl = refl
sound∘complete′ (∣-left {xs₁ = xs₁} {xs₂ = xs₂} x∈p₁) refl
rewrite left-inverse-of (++↔ {P = _≡_ _} {xs = xs₁} {ys = xs₂}) (inj₁ (complete x∈p₁)) =
H.cong _∈_·_.∣-left (sound∘complete′ x∈p₁ refl)
sound∘complete′ (∣-right xs₁ x∈p₂) refl
rewrite left-inverse-of (++↔ {P = _≡_ _} {xs = xs₁}) (inj₂ (complete x∈p₂)) =
H.cong (_∈_·_.∣-right xs₁) (sound∘complete′ x∈p₂ refl)
sound∘complete′ (<\$>_ {f = f} x∈p) refl
rewrite left-inverse-of (map-∈↔ f) (_ , complete x∈p , refl) =
H.cong _∈_·_.<\$>_ (sound∘complete′ x∈p refl)
sound∘complete′ (_⊛_ {s₁ = []} {fs = fs} {xs = just xs} f∈p₁ x∈p₂) refl
with complete f∈p₁ | complete x∈p₂
| from inv ⟨\$⟩ (to inv ⟨\$⟩ (_ , _ , complete f∈p₁ , complete x∈p₂ , refl))
| left-inverse-of inv (_ , _ , complete f∈p₁ , complete x∈p₂ , refl)
| sound∘complete f∈p₁ | sound∘complete x∈p₂
where inv = ⊛-∈↔ (flatten fs) {xs = xs}
sound∘complete′ (_⊛_ {s₁ = []} {fs = nothing} {xs = just xs} _ _) refl | () | _ | _ | _ | _ | _
sound∘complete′ (_⊛_ {s₁ = []} {fs = just fs} {xs = just xs} {p₁ = p₁} {p₂ = p₂}
.(sound p₁ ∈fs) .(sound p₂ ∈xs)) refl
| ∈fs | ∈xs | ._ | refl | refl | refl = refl
sound∘complete′ (_>>=_ {x = x} {y = y} {s₁ = []} {xs = just _} {f = just f} {p₁ = p₁} {p₂ = p₂} x∈p₁ y∈p₂x) refl
rewrite left-inverse-of (>>=-∈↔ {f = f}) (_ , complete x∈p₁ , complete y∈p₂x)
with sound p₁ (complete x∈p₁)
| sound∘complete x∈p₁
| sound′ (p₂ x) (complete x∈p₁) (complete y∈p₂x)
| helper (p₂ x) (complete x∈p₁) y∈p₂x
where
helper : ∀ {Tok R₁ R₂ x y ys} {xs : Maybe (List R₁)}
(p : ∞⟨ xs ⟩Parser Tok R₂ ys) →
(x∈xs : x ∈ flatten xs) (y∈p : y ∈ ♭? p · []) →
sound′ p x∈xs (complete y∈p) ≡ y∈p
helper {xs = nothing} p () _
helper {xs = just _}  p _  y∈p = sound∘complete y∈p
... | ._ | refl | ._ | refl = refl
sound∘complete′ (cast {xs₁≈xs₂ = xs₁≈xs₂} x∈p)             refl with complete x∈p | sound∘complete x∈p
sound∘complete′ (cast {xs₁≈xs₂ = xs₁≈xs₂} .(sound _ x∈xs)) refl | x∈xs | refl
rewrite left-inverse-of xs₁≈xs₂ x∈xs = refl

sound∘complete′ (_⊛_    {s₁ = []} {xs = nothing}              _    x∈p₂)  refl with complete x∈p₂
... | ()
sound∘complete′ (_>>=_  {s₁ = []} {xs = nothing}              x∈p₁ y∈p₂x) refl with complete x∈p₁
... | ()
sound∘complete′ (_>>=_  {s₁ = []} {xs = just _} {f = nothing} x∈p₁ y∈p₂x) refl with complete y∈p₂x
... | ()

sound∘complete′ token                     ()
sound∘complete′ (_⊛_    {s₁ = _ ∷ _} _ _) ()
sound∘complete′ (_>>=_  {s₁ = _ ∷ _} _ _) ()
sound∘complete′ (nonempty _)              ()

complete∘sound : ∀ {Tok R xs x}
(p : Parser Tok R xs) (x∈p : x ∈ xs) →
complete (sound p x∈p) ≡ x∈p
complete∘sound (return x)              (here refl) = refl
complete∘sound (_∣_ {xs₁ = xs₁} p₁ p₂) x∈xs
with from             (++↔ {P = _≡_ _} {xs = xs₁}) ⟨\$⟩ x∈xs
| right-inverse-of (++↔ {P = _≡_ _} {xs = xs₁})     x∈xs
complete∘sound (_∣_ {xs₁ = xs₁} p₁ p₂) .(to ++↔                          ⟨\$⟩ inj₁ x∈xs₁) | inj₁ x∈xs₁ | refl =
P.cong (_⟨\$⟩_ (to ++↔)                          ∘ inj₁) \$ complete∘sound p₁ x∈xs₁
complete∘sound (_∣_ {xs₁ = xs₁} p₁ p₂) .(to (++↔ {P = _≡_ _} {xs = xs₁}) ⟨\$⟩ inj₂ x∈xs₂) | inj₂ x∈xs₂ | refl =
P.cong (_⟨\$⟩_ (to (++↔ {P = _≡_ _} {xs = xs₁})) ∘ inj₂) \$ complete∘sound p₂ x∈xs₂
complete∘sound (f <\$> p) x∈xs
with             from (map-∈↔ f) ⟨\$⟩ x∈xs
| right-inverse-of (map-∈↔ f)     x∈xs
complete∘sound (f <\$> p) .(to (map-∈↔ f) ⟨\$⟩ (y , y∈xs , refl)) | (y , y∈xs , refl) | refl =
P.cong (λ y∈ → to (map-∈↔ _) ⟨\$⟩ (y , y∈ , refl))
(complete∘sound p y∈xs)
complete∘sound (_⊛_ {fs = fs} {just xs} p₁ p₂) y∈ys
with from             (⊛-∈↔ (flatten fs) {xs = xs}) ⟨\$⟩ y∈ys
| right-inverse-of (⊛-∈↔ (flatten fs) {xs = xs})     y∈ys
complete∘sound (_⊛_ {fs = nothing} {xs = just xs} p₁ p₂)
y∈ys                                                | (f′ , x′ , ()    , x′∈xs , refl) | _
complete∘sound (_⊛_ {fs = just fs} {xs = just xs} p₁ p₂)
.(to (⊛-∈↔ _) ⟨\$⟩ (f′ , x′ , f′∈fs , x′∈xs , refl)) | (f′ , x′ , f′∈fs , x′∈xs , refl) | refl =
P.cong₂ (λ f′∈ x′∈ → to (⊛-∈↔ _) ⟨\$⟩ (f′ , x′ , f′∈ , x′∈ , refl))
(complete∘sound p₁ f′∈fs)
(complete∘sound p₂ x′∈xs)
complete∘sound (_>>=_ {xs = zs}      {just f} p₁ p₂) y∈ys
with from             (>>=-∈↔ {xs = flatten zs} {f = f}) ⟨\$⟩ y∈ys
| right-inverse-of (>>=-∈↔ {xs = flatten zs} {f = f})     y∈ys
complete∘sound (_>>=_ {xs = nothing} {just f} p₁ p₂) ._                                           | (x , ()   , y∈fx) | refl
complete∘sound (_>>=_ {xs = just zs} {just f} p₁ p₂) .(to (>>=-∈↔ {f = f}) ⟨\$⟩ (x , x∈zs , y∈fx)) | (x , x∈zs , y∈fx) | refl =
P.cong₂ (λ x∈ y∈ → to (>>=-∈↔ {f = f}) ⟨\$⟩ (x , x∈ , y∈))
(complete∘sound p₁ x∈zs)
(complete∘sound (p₂ x) y∈fx)
complete∘sound (cast xs₁≈xs₂ p) x∈xs
rewrite complete∘sound p (from xs₁≈xs₂ ⟨\$⟩ x∈xs) =
right-inverse-of xs₁≈xs₂ x∈xs

complete∘sound (return _)                 (there ())
complete∘sound fail                       ()
complete∘sound token                      ()
complete∘sound (_⊛_   {xs = nothing} _ _) ()
complete∘sound (_>>=_ {f  = nothing} _ _) ()
complete∘sound (nonempty _)               ()

correct : ∀ {Tok R xs x} {p : Parser Tok R xs} → x ∈ p · [] ↔ x ∈ xs
correct {p = p} = record
{ to         = P.→-to-⟶ complete
; from       = P.→-to-⟶ \$ sound p
; inverse-of = record
{ left-inverse-of  = sound∘complete
; right-inverse-of = complete∘sound p
}
}

------------------------------------------------------------------------
-- Equal parsers have equal initial bags/sets

-- Note that this property holds also for the subbag and subset
-- relations.

cong : ∀ {k Tok R xs₁ xs₂}
{p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
p₁ ∼[ k ] p₂ → initial-bag p₁ List-∼[ k ] initial-bag p₂
cong {xs₁ = xs₁} {xs₂} {p₁} {p₂} p₁≈p₂ {x} =
(x ∈ xs₁)    ↔⟨ SK-sym correct ⟩
x ∈ p₁ · []  ∼⟨ p₁≈p₂ ⟩
x ∈ p₂ · []  ↔⟨ correct ⟩
(x ∈ xs₂)    ∎
where open Related.EquationalReasoning
```