-- Cut and identity for polarized intuitionistic logic (negative half)
-- Dan Licata, June 2008

open import lib.Prelude
open List using (_++_)  

module foc.NegOnly where

open List.InLists

module Types where
  mutual 
    Atom = String

    data Neg : Set where 
      X⁻  : Atom -> Neg
      _⊃_ : Neg -> Neg -> Neg -- really (↓ _ → _)
      ⊤   : Neg
      _&_  : Neg -> Neg -> Neg
      Stream : Neg -> Neg

  infixr 15 _⊃_
  infixr 19 _&_ 

module Contexts where    
  open Types

  Hyp : Set 
  Hyp = Neg

  Conc : Set
  Conc = Atom

  Ctx : Set
  Ctx = List Hyp

  CtxCtx = List Ctx

module Focus where
  open Types public
  open Contexts public

  data FocJudg : Set where
    LFoc : Neg -> Conc -> FocJudg
    RInv : Neg -> FocJudg
    Neu  : Conc -> FocJudg
    Asms : Ctx  -> FocJudg

  data DPat : Ctx -> Neg -> Conc -> Set where
    De⁻  : forall {x} -> DPat [] (X⁻ x) x
    Dapp : forall {Δ A- B- γ} 
         -> DPat Δ B- γ  
         -> DPat (A- :: Δ) (A- ⊃ B-) γ
    -- no rule for ⊤ 
    Dfst : forall {Δ A- B- γ} 
         -> DPat Δ A- γ  
         -> DPat Δ (A- & B-) γ
    Dsnd : forall {Δ A- B- γ} 
         -> DPat Δ B- γ  
         -> DPat Δ (A- & B-) γ
    Dhead : forall {Δ A- γ} 
         -> DPat Δ A- γ  
         -> DPat Δ (Stream A-) γ
    Dtail : forall {Δ A- γ} 
         -> DPat Δ (Stream A-) γ  
         -> DPat Δ (Stream A-) γ
    
  data _⊢_ :  CtxCtx -> FocJudg -> Set where
    -- negative continuations (k-)
    Cont⁻ : forall {Δ A- γ Γ} 
          -> DPat Δ A- γ -> Γ ⊢ Asms Δ  -- implicit equality check
          -> Γ ⊢ LFoc A- γ

    -- negative values (v-)
    Val⁻ : forall {Γ C- } 
         -> ({Δ : Ctx} {γ : Conc} -> DPat Δ C- γ ->  Δ :: Γ ⊢ Neu γ) 
         -> Γ ⊢ RInv C-

    -- expressions (e)
    L : forall {Γ C- γ} 
      -> (C- ∈∈ Γ)   ->  Γ ⊢ LFoc C- γ
      -> Γ ⊢ Neu γ

    -- substitutions (σ)
    Sub  : {Γ : CtxCtx} -> {Δ : Ctx} 
         -> ({α : Hyp} -> α ∈ Δ -> Γ ⊢ RInv α) 
         -> Γ ⊢ Asms Δ

module Acc where

  open Focus

  mutual
    data Acc (A- : Neg) : Set where
      AN : ({X : Conc} {Δ : Ctx} -> DPat Δ A- X -> AccΔ Δ) -> Acc A-

    data AccΔ (Δ : Ctx) : Set where
      AΔ : ({A- : Neg} -> A- ∈ Δ -> Acc A-) -> AccΔ Δ

  wf : (A- : Neg) -> Acc A-
  wf A- = AN wffn
{- Note: this is the only part of the proof that is specific to the types! -}
   where wffn : {A- : Neg} -> ({X : Conc} {Δ : Ctx} -> DPat Δ A- X -> AccΔ Δ)
         wffn De⁻ = AΔ (List.EW.there {_} {Acc} E[])
         wffn (Dapp d) with (wffn d) 
         ...              | (AΔ a) = AΔ (List.EW.there ((wf _ ) E:: List.EW.fromall a)) 
         wffn (Dfst d) = wffn d
         wffn (Dsnd d) = wffn d
         wffn (Dhead d) = wffn d
         wffn (Dtail d) = wffn d

  wfΔ : (Δ : Ctx) -> AccΔ Δ
  wfΔ Δ = AΔ (\ a -> wf _)

module Ident where

  open Focus     
  open Acc

  mutual
    η- : {Γ : CtxCtx} {A- : Neg} -> Acc A- -> (i : A- ∈∈ Γ) -> Γ ⊢ RInv A-
    η- (AN acc) i = Val⁻ (\ d -> L (List.SW.sS i) (Cont⁻ d (ηsub (acc d) i0)))
  
    ηsub : {Γ : CtxCtx} {Δ : Ctx} -> AccΔ Δ -> (Δ ∈ Γ) -> Γ ⊢ Asms Δ
    ηsub (AΔ acc) Δin = Sub (\a -> η- (acc a) (List.SW.fromin Δin a))

module Weaken where

  open Focus

  open List.Subsets using (_⊆SS_)
  open List.Subset using (_⊆_)

  weaken : {Γ Γ' : CtxCtx} {J : FocJudg} -> Γ ⊆SS Γ' -> Γ ⊢ J -> Γ' ⊢ J
  weaken wv (Cont⁻ d σ) = Cont⁻ d (weaken wv σ)
  weaken wv (Val⁻ f)    = Val⁻ (\d -> weaken (List.Subsets.shiftwv wv _) (f d))
  weaken wv (L x k-) = L (wv x) (weaken wv k-)
  weaken wv (Sub l) = Sub (\a -> weaken wv (l a)) 

module Cut where

  open Focus 
  open Weaken
  open Acc

  open List.In using (_-_)

  open List.SW

  mutual 
    β- : {Γ : CtxCtx} {A- : Neg} {X : Conc} -> Acc A- -> Γ ⊢ RInv A- -> Γ ⊢ LFoc A- X -> Γ ⊢ Neu X
    β- (AN acc) (Val⁻ f) (Cont⁻ d σ) = subst (acc d) i0 σ (f d)

    subst : {Γ : CtxCtx} {J : FocJudg} {Δ : Ctx} 
            -> AccΔ Δ
            -> (i : Δ ∈ Γ) -> (Γ - i) ⊢ Asms Δ -> Γ ⊢ J
            -> (Γ - i) ⊢ J
    subst a i σ (Val⁻ f) = Val⁻ (\ d -> subst a (iS i) (weaken sS σ) (f d))
    subst a i σ (Cont⁻ d σ') = Cont⁻ d (subst a i σ σ')
    subst a i σ (Sub f) = Sub (\ d -> subst a i σ (f d))
{- why doesn't this work? 
    subst (AΔ acc) i (Sub f) (L j k-) with lemma i j
    ... | Inl newj = β- (acc newj) (f newj) (subst (AΔ acc) i (Sub f) k-)
    ... | Inr newj = L newj (subst (AΔ acc) i (Sub f) k-)
-}
    subst a i σ (L j k-) with  (subst a i σ k-)
    ... | k' = help a i σ k' (List.SW.here? i j)  where
      help : {Γ : CtxCtx} {X : Conc} {Δ : Ctx} {A- : Neg}
           -> AccΔ Δ
           -> (i : Δ ∈ Γ) 
           -> (Γ - i) ⊢ Asms Δ 
           -> (Γ - i) ⊢ LFoc A- X
           -> Either (A- ∈ Δ) (A- ∈∈ (Γ - i))
           -> (Γ - i) ⊢ Neu X
      help _ _ _ k- (Inr j') = L j' k-
      help (AΔ a) _ (Sub f) k- (Inl j') = β- (a j') (f j') k-