open import Relation.Binary 
open import Relation.Binary.PropositionalEquality as PropEq renaming ([_] to [_]ᵢ) 
open import Level hiding (zero; suc)
open import Data.String using (String)
open import Data.Nat as Nat hiding (_*_; _⊔_; _≟_)
open import Data.Bool hiding (_≟_;_∨_)
open import Data.Empty
open import Function using (id)
open import Data.Sum hiding (map) renaming ([_,_] to [_,_]ₛ)
open import Data.Product renaming (Σ to Σₓ;map to mapₓ)
open import Relation.Nullary
open import Relation.Nullary.Decidable hiding (map)
open import Data.List hiding (any) renaming (length to length')
open import Data.List.Relation.Unary.Any as Any hiding (map)
open import Agda.Primitive
open import Data.List.Relation.Binary.Subset.Propositional  
open import Data.List.Relation.Binary.Subset.Propositional.Properties
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
  
open import Stoughton.Chi

module Stoughton.Syntax (𝒞 : Set) (𝒱 : Set) (_≟_ : Decidable {A = 𝒱} _≡_) where

  infixl  _·_
  data Λ : Set where
    c : 𝒞 → Λ    
    v : 𝒱 → Λ
    λ[_∶_]_ : 𝒱 → Λ → Λ → Λ
    Π[_∶_]_ : 𝒱 → Λ → Λ → Λ    
    _·_ : Λ → Λ → Λ

  length : Λ → ℕ
  length (c _)   = 
  length (v _)   = 
  length (λ[ _ ∶ A ] M) = suc (length A + length M)
  length (Π[ _ ∶ A ] B) = suc (length A + length B)
  length (M · N) = suc (length M + length N)

  _-_ : List 𝒱 → 𝒱 → List 𝒱
  xs - x = boolFilter (λ y → not (⌊ x ≟ y ⌋)) xs

  fv : Λ → List 𝒱
  fv (c _)     = []
  fv (v x)     = [ x ]
  fv (M · N)   = fv M ++ fv N
  fv (λ[ x ∶ A ] M) = fv A ++ (fv M - x)
  fv (Π[ x ∶ A ] B) = fv A ++ (fv B - x)

  infix  _*_
  _*_ : 𝒱 → Λ → Set
  x * M = x ∈ fv M

  infix  _#_
  _#_ : 𝒱 → Λ → Set
  x # M = x ∉ fv M
  
  _≈_ : List 𝒱 → List 𝒱 → Set
  xs ≈ ys = xs ⊆ ys × ys ⊆ xs
  
  ∼*ρ : Reflexive _≈_
  ∼*ρ  = ⊆-refl , ⊆-refl

  sym≢ : {x y : 𝒱} → x ≢ y → y ≢ x
  sym≢ {x} {y} x≢y y≡x = x≢y (sym y≡x)
    
  lemma∈-≢ : ∀ {x y xs} → y ∈ xs → x ≢ y → y ∈ xs - x
  lemma∈-≢ {x} {y} {[]} ()
  lemma∈-≢ {x} {y} {(z ∷ xs')} y∈z::xs' x≢y with x ≟ z
  lemma∈-≢ {x} {.x} {(.x ∷ xs')} (here refl) x≢x | yes refl = ⊥-elim (x≢x refl)
  lemma∈-≢ {x} {y} {(.x ∷ xs')} (there y∈xs') x≢y | yes refl = lemma∈-≢ y∈xs' x≢y
  lemma∈-≢ {x} {y} {(.y ∷ xs')} (here refl) x≢y | no y≢x = here refl
  lemma∈-≢ {x} {y} {(z ∷ xs')} (there y∈xs') x≢y | no y≢x = there (lemma∈-≢ y∈xs' x≢y)

  ∈-→≢ : ∀ {x y xs} → x ∈ xs - y → x ≢ y
  ∈-→≢ {x} {y} {[]} ()
  ∈-→≢ {x} {y} {z ∷ xs'} x∈z::xs'-y with y ≟ z
  ∈-→≢ {x} {y} {.y ∷ xs'} x∈xs'-y | yes refl = ∈-→≢ {xs = xs'} x∈xs'-y
  ∈-→≢ {x} {y} {.x ∷ xs'} (here refl) | no y≢x = sym≢ y≢x
  ∈-→≢ {x} {y} {z ∷ xs'} (there x∈xs'-y) | no _ = ∈-→≢ {xs = xs'} x∈xs'-y

  ∈-→∈ : ∀ {x y xs} → x ∈ xs - y → x ∈ xs
  ∈-→∈ {x} {y} {[]} ()
  ∈-→∈ {x} {y} {z ∷ xs'} x∈z::xs'-y with y ≟ z
  ... | yes _ = there (∈-→∈ x∈z::xs'-y)
  ∈-→∈ {x} {y} {.x ∷ xs'} (here refl) | no _ = here refl
  ∈-→∈ {x} {y} {z ∷ xs'} (there x∈xs'-y) | no _ = there (∈-→∈ x∈xs'-y)

  ∈- : ∀ {x y xs} → x ∈ xs - y → x ≢ y × x ∈ xs
  ∈- {xs = xs} x∈xs = ∈-→≢ {xs = xs} x∈xs , ∈-→∈ x∈xs

  infix  _↔_
  _↔_ : Set → Set → Set
  A ↔ B = (A → B) × (B → A)

  appList : {A : Set}{x : A}(xs : List A){ys : List A} → x ∈ xs ++ ys ↔ (x ∈ xs ⊎ x ∈ ys)
  appList xs = ∈-++⁻ xs , [ ∈-++⁺ˡ , ∈-++⁺ʳ xs ]ₛ
  
  delList : ∀ {x y xs} → x ∈ xs - y ↔ x ≢ y × x ∈ xs
  delList = ∈- , λ p → lemma∈-≢ (proj₂ p) (sym≢ (proj₁ p))  

  lemma∉-≢ : ∀ {x y xs} → x ∉ xs - y → x ≢ y → x ∉ xs
  lemma∉-≢ x∉xs-y x≢y x∈xs = ⊥-elim (x∉xs-y (lemma∈-≢ x∈xs (sym≢ x≢y)))
    
  ∉- : ∀ {x} l → x ∉ l - x
  ∉- {x} [] ()
  ∉- {x} (y ∷ xs) x∈y::xs-x with x ≟ y
  ... | yes _ = ∉- xs x∈y::xs-x
  ∉- {x} (y ∷ xs) (here x=y) | no x≢y = ⊥-elim (x≢y x=y)
  ∉- {x} (y ∷ xs) (there x∈xs-x) | no _ = ∉- xs x∈xs-x

  c∉xs++ys→c∉xs : {x : 𝒱} {xs ys : List 𝒱} → x ∉ xs ++ ys → x ∉ xs
  c∉xs++ys→c∉xs {x} {xs} {ys} x∉xs++ys x∈xs = x∉xs++ys (∈-++⁺ˡ x∈xs)

  c∉xs++ys→c∉ys : {x : 𝒱} {xs ys : List 𝒱} → x ∉ xs ++ ys → x ∉ ys
  c∉xs++ys→c∉ys {x} {xs} {ys} x∉xs++ys x∈ys = x∉xs++ys (∈-++⁺ʳ xs x∈ys)

  appListNotIn : ∀ {x} {xs ys : List 𝒱} → x ∉ xs ++ ys ↔ x ∉ xs × x ∉ ys
  appListNotIn {_} {xs} = (λ x∉xs++ys → (c∉xs++ys→c∉xs x∉xs++ys , c∉xs++ys→c∉ys x∉xs++ys)) , λ (x∉xs , x∉ys) x∈xs++ys → [ x∉xs , x∉ys ]ₛ (proj₁ (appList xs) x∈xs++ys)

  delListNotIn : ∀ {x y xs} → x ∉ xs - y ↔ (x ≡ y ⊎ x ∉ xs)
  delListNotIn {x} {y} {xs} = ltr  , [ (λ x≡y x∈xs-y → ⊥-elim (∈-→≢ {xs = xs} x∈xs-y x≡y)) , (λ x∉xs x∈xs-y → ⊥-elim (x∉xs (∈-→∈ x∈xs-y))) ]ₛ
    where
    ltr : ∀ {x y xs} → x ∉ xs - y → (x ≡ y ⊎ x ∉ xs)
    ltr {x} {y} x∉xs-y with x ≟ y
    ltr {x} {.x} _     | yes refl = inj₁ refl
    ltr {x} {y} x∉xs-y | no x≢y = inj₂ (lemma∉-≢ x∉xs-y x≢y)

  ∉→∉- : ∀ {x y l} → x ∉ l → x ∉ l - y
  ∉→∉- x∉l x∈l-y = ⊥-elim (x∉l (∈-→∈ x∈l-y))