{-# OPTIONS --allow-unsolved-metas #-}

open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_)


module LogRel
  {{ Α : Set }}    -- type level constants
  {{ C : Set }}    -- term level constants

  {{ Var : Set }}  -- variables
  {{ decEqVar : Decidable (_≡_ {A = Var}) }}

  {{  Κ : Set }}   -- proof term constants


  where

import SyntaxRew
open SyntaxRew 
  {{ Α }}    -- type level constants
  {{ C }}    -- term level constants

  {{ Var }}  -- variables
  {{ decEqVar }} -- unification variables

  {{ Κ }}    -- proof term constants
  --private


-- logic relation
mutual
  data logrel : Sig → Prog → Ctx → MT → MT → Set where
    ldecide : {S : Sig} {P : Prog} {Γ : Ctx} {e : MT} {A : T} {e' : MT} {-κ : Κ-} {D : De} →
      logreldec S P Γ e' D e (go (at A)) →
      -- κ ∷ D ∈P P → 
      -- (S + P + Γ ⊢MT e' ∷De D) →
      logrelced S P Γ e' D → 
      logrel S P Γ e (go (at A))

    l∃R : {S : Sig} {P : Prog} {Γ : Ctx} {e : MT} {G : Go} {M : t} {A : T} {x : Var} →
      logrel S P Γ e (go (G [ M / x ]Go) ) →
      S + Γ ⊢ M ∷ A →
      logrel S P Γ (< M , e >M) (go (∃Go x A G))

    l⇒R : {S : Sig} {P : Prog} {Γ : Ctx} {κ : Κ} {e : MT} {D : De} {G : Go} →
      logrel S (P , κ ∷ D) Γ e (go G) →
      logrel S P Γ (lamM κ e) (go (D ⇒ G))

    l∀R : {S : Sig} {P : Prog} {Γ : Ctx} {e : MT} {A : T} {G : Go} {x : Var} {c : C} →
      logrel (S , c ∷T A) P Γ ( e [ (const c) / x ]MT ) (go (G [ const c / x ]Go)) →
      logrel S P Γ e (go (∀Go x A G))


    logrefl : ∀ {S P Γ A} →
      S ⊢prog P →
      logrel S P Γ (go (at A)) (go (at A))

    lap : {S : Sig} {P : Prog} {Γ Γ₁ : Ctx} {e₁ e₂ ê ê' : MT} {θ : Θ S Γ₁ Γ} →
      logrel S P Γ ê' ê →
      e₁ ≡ θ ΘMT e₂ →
      logrel S P Γ (e₁ apM ê') (e₂ apM ê)

    lex : {S : Sig} {P : Prog} {Γ Γ₁ : Ctx} {M M' : t } {e : MT} {ê : MT} {θ : Θ S Γ₁ Γ} →
      logrel S P Γ e ê →
      M' ≡ θ Θt M →
      logrel S P Γ (< M' , e >M) (< M , ê >M)


    llam : {S : Sig} {P : Prog} {Γ : Ctx} {κ : Κ} {-D : De-} {e : MT} {ê : MT} →
      logrel S P Γ e ê →
      logrel S P Γ (lamM κ e) (lamM κ ê)

  data logreldec  : Sig → Prog → Ctx → MT → De → MT → MT → Set where

    linit : {S : Sig} {P : Prog} {Γ : Ctx} {e : MT} { e' : MT} {A A' : T} →
      e ≡ e' → A ≡ A' →
      logreldec S P Γ e (at A) e' (go (at A'))


    l⇒L : {S : Sig} {P : Prog} {Γ : Ctx} {e e₁ e₂ : MT} {A₁ A₂ : T} {D : De} →

      logrel S P Γ e₁ (go (at A₁)) →
      logreldec S P Γ (e apM e₁) D e₂ (go (at A₂)) →
      logreldec S P Γ e (at A₁ ⇒ D) e₂ (go (at A₂))

    l∀L : {S : Sig} {P : Prog} {Γ : Ctx} { e e₂ : MT} {x : Var} {A₁ A₂ : T} {D : De} {M : t} →
      logreldec S P Γ e (D [ M / x ]De) e₂ (go (at A₂)) →
      S + Γ ⊢ M ∷ A₁ →
      logreldec S P Γ e (∀De x A₁ D) e₂ (go (at A₂))

{-
    l⇒L : {S : Sig} {P : Prog} {Γ : Ctx} {e e₁ e₂ : MT} {G₁ G₂ : Go} {D : De} →

      logrel S P Γ e₁ (go G₁) →
      logreldec S P Γ (e apM e₁) D e₂ (go G₂) →
      logreldec S P Γ e (G₁ ⇒ D) e₂ (go G₂)

    l∀L : {S : Sig} {P : Prog} {Γ : Ctx} { e e₂ : MT} {x : Var} {G : Go} { A : T} {D : De} {M : t} →
      logreldec S P Γ e (D [ M / x ]De) e₂ (go G) →
      S + Γ ⊢ M ∷ A →
      logreldec S P Γ e (∀De x A D) e₂ (go G)
-}

    lapdec : {S : Sig} {P : Prog} {Γ₁ Γ : Ctx} {e' e'' e₁ e₂ : MT} {ê : MT} {D₁ : De} {θ : Θ S Γ₁ Γ}→
      logreldec S P Γ e'' D₁ e'  ê →
      θ ΘMT e₂ ≡ e₁ →
      logreldec S P Γ e'' D₁ (e₁ apM e') (e₂ apM ê)


    lexdec : {S : Sig} {P : Prog} {Γ₁ Γ : Ctx } {θ : Θ S Γ₁ Γ } {Γ : Ctx} {M M' : t } {e e₁ : MT} {ê : MT} {D₁ : De} →
      logreldec S P Γ e₁ D₁ e  ê →
      θ Θt M ≡ M' →
      logreldec S P Γ e₁ D₁ (< M' , e >M) (< M , ê >M)


    llamdec : {S : Sig} {P : Prog}  {Γ : Ctx} {κ : Κ} {D : De} {e e₁ : MT} {ê : MT} {D₁ : De} →
      logreldec S (P , κ ∷ D) Γ e₁ D₁ e ê →
      logreldec S P Γ e₁ D₁ (lamM κ e) (lamM κ ê)




  data logrelced : Sig → Prog → Ctx → MT → De → Set where

    ldecide⁻ : ∀ {S P Γ Γ₁ D κ } {θ : Θ S Γ₁ Γ} →
      κ ∷ D ∈P P → 
      S ⊢prog P →
      logrelced S P Γ (symbM κ) (θ ΘDe D)


    l⇒L⁻ : ∀ {S P Γ A D e e'} →
      logrelced S P Γ e (at A ⇒ D) →
      logrel S P Γ e' (go (at A)) →
      logrelced S P Γ (e apM e') D


    --l∀L⁻ : ∀ {S P Γ e x A D M} →
    --  logrelced S P Γ e (∀De x A D) →
    --  S + Γ ⊢ M ∷ A → 
    --  logrelced S P Γ e (D [ M / x ]De)
    --l∀L⁻ : ∀ {S P Γ e x A D} →
    --  logrelced S P Γ e (∀De x A D) →
    --  logrelced S P (Γ , x ∷ A) e D

    l∀L⁻ : ∀ {S P Γ e x A D} →
      logrelced S P (Γ , x ∷ A) e D →
      logrelced S P Γ e (∀De x A D)


  {-
  ldecide : {S : Sig} {P : Prog} {Γ : Ctx} {e : MT} {A : T} {e' : MT} {-κ : Κ-} {D : De} →
    logreldec S P Γ e' D e (go (at A)) →
    -- κ ∷ D ∈P P → 
    (S + P + Γ ⊢MT e' ∷De D) →
    logrel S P Γ e (go (at A))
-}
{-

    wf-symbM-de : ∀ {S P Γ κ D} → S ⊢prog P → κ ∷ D ∈P P → S + P + Γ ⊢MT (symbM κ) ∷De D

    wf-apM-de : ∀ {S P Γ e e' G D} → S + P + Γ ⊢MT e ∷De (G ⇒ D) → S + P + Γ ⊢MT e' ∷Go G  →  S + P + Γ ⊢MT e apM e' ∷De D

    wf-forallM-de : ∀ {S P Γ x A₁ D e M} → S + P + Γ ⊢MT e ∷De ∀De x A₁ D → S + Γ ⊢ M ∷ A₁  →  S + P + Γ ⊢MT e  ∷De ( D [ M / x ]De )


  data _+_+_⊢MT_∷Go_ : Sig → Prog → Ctx → MT → Go → Set where

    wf-symbM-go : ∀ {S P Γ κ A} → S ⊢prog P → κ ∷ (at A) ∈P P → S + P + Γ ⊢MT (symbM κ) ∷Go (at A)
-}


open import Data.Product using (∃ ; _,_ ; ∃₂ ; _×_)
open import Relation.Binary.PropositionalEquality using (refl)



{- syntactic validity of logrel  -}
log-val-sig : {S : Sig} {P : Prog} {Γ : Ctx} {e e' : MT}  →
  logrel S P Γ e e' →
  ⊢ S

logdec-val-sig : {S : Sig} {P : Prog} {Γ : Ctx} {e e' e₁ : MT} {D : De} →
  logreldec S P Γ e₁ D e e' →
  ⊢ S

log-val-sig (ldecide x x₁) = logdec-val-sig x
log-val-sig (l∃R log x₁) = log-val-sig log
log-val-sig (l⇒R log) = log-val-sig log
log-val-sig (l∀R log) with log-val-sig log
... | ⊢_.,∷-wfctx-c res x₁ = res
log-val-sig (logrefl x) = impl-val-sig x
log-val-sig (lap log x) = log-val-sig log
log-val-sig (lex log x) = log-val-sig log
log-val-sig (llam log) = log-val-sig log

logdec-val-sig (linit x x₁) = {!≡-val-sig!}
logdec-val-sig (l⇒L x ldec) = logdec-val-sig ldec
logdec-val-sig (l∀L ldec x₁) = logdec-val-sig ldec
logdec-val-sig (lapdec ldec x) = logdec-val-sig ldec
logdec-val-sig (lexdec ldec x) = logdec-val-sig ldec
logdec-val-sig (llamdec ldec) = logdec-val-sig ldec


{- syntactic validity of logrel  -}
log-val-prog : {S : Sig} {P : Prog} {Γ : Ctx} {e e' : MT}  →
  logrel S P Γ e e' →
  S ⊢prog P

logdec-val-prog : {S : Sig} {P : Prog} {Γ : Ctx} {e e' e₁ : MT} {D : De} →
  logreldec S P Γ e₁ D e e' →
  S ⊢prog P


logced-val-prog : {S : Sig} {P : Prog} {Γ : Ctx} {e : MT} {D : De} →
  logrelced S P Γ e D →
  S ⊢prog P


log-val-prog (ldecide x y ) = logdec-val-prog x 
log-val-prog (l∃R log x₁) = log-val-prog log
log-val-prog (l⇒R log) with log-val-prog log
... | ,∷-prog res x x₁ = res
log-val-prog (l∀R log) with log-val-prog log
... | res = strenghten-val-sig res {- c FRESH !!! -}
log-val-prog (lap log x) = log-val-prog log
log-val-prog (lex log x) = log-val-prog log
log-val-prog (llam log) = log-val-prog log
log-val-prog (logrefl x) = x

logdec-val-prog (linit x x₁ ) = {!impl-valid-≡!}
logdec-val-prog (l⇒L x logdec) = logdec-val-prog logdec
logdec-val-prog (l∀L logdec x₁) = logdec-val-prog logdec
-- logdec-val-prog (lapdec logdec) = logdec-val-prog logdec
logdec-val-prog (lapdec x x₁) = logdec-val-prog x
logdec-val-prog (lexdec x x₁) = logdec-val-prog x
logdec-val-prog (llamdec x) with logdec-val-prog x
... | ,∷-prog p x₁ x₂ = p

logced-val-prog (ldecide⁻ x x₁) = x₁
logced-val-prog (l⇒L⁻ lced x) = log-val-prog x
logced-val-prog (l∀L⁻ lced) = logced-val-prog lced

{-
  logic relation can be weaken uder sig
-}
log-weaken-sig : {S : Sig} {P : Prog} {Γ : Ctx} {e  e' : MT} {c : C} {A : T} →
  logrel S P Γ e e' →
  ⊢ (S , c ∷T A) →
  logrel (S , c ∷T A)  P Γ e e'

logdec-weaken-sig : {S : Sig} {P : Prog} {Γ : Ctx} {e  e' : MT} {c : C} {A A₁ : T} {D : De} →
  logreldec S P Γ e' D e (go (at A)) →
  ⊢ (S , c ∷T A₁) →
  logreldec (S , c ∷T A₁) P Γ e' D e (go (at A))

log-weaken-sig (ldecide x x₁) wfS = ldecide (logdec-weaken-sig x wfS) {!!}
log-weaken-sig (l∃R log x₁) wfS = l∃R (log-weaken-sig log wfS) (trm-weaken-sig x₁ wfS)
log-weaken-sig (l⇒R log) wfS = l⇒R (log-weaken-sig log wfS)
log-weaken-sig (l∀R log) wfS = l∀R ({!log-weaken-sig!})
log-weaken-sig (logrefl x) wfS = logrefl (prog-weaken-sig x wfS)
log-weaken-sig (lap log x) wfS = lap (log-weaken-sig log wfS) {!w x!}
log-weaken-sig (lex log x) wfS = lex (log-weaken-sig log wfS) {!x!}
log-weaken-sig (llam log) wfS = llam (log-weaken-sig log wfS)

logdec-weaken-sig = {!!}


{-
  logic relation can be weaken under prog
-}

log-weaken-prog : {S : Sig} {P : Prog} {Γ : Ctx} {e  e' : MT} {κ : Κ} {D : De} →
  logrel S P Γ e e' →
  S ⊢prog (P , κ ∷ D) →
  logrel S (P , κ ∷ D) Γ e e'


logdec-weaken-prog : {S : Sig} {P : Prog} {Γ : Ctx} {e  e'' e''' : MT} {κ : Κ} {D D' : De} →
  logreldec S P Γ e D' e'' e''' →
  S ⊢prog (P , κ ∷ D) →
  logreldec S (P , κ ∷ D) Γ e D' e'' e'''


logced-weaken-prog : {S : Sig} {P : Prog} {Γ : Ctx} {e : MT} {κ : Κ} {D D' : De} →
  logrelced S P Γ e D' →
  S ⊢prog (P , κ ∷ D) →
  logrelced S (P , κ ∷ D) Γ e D'


log-weaken-prog (ldecide ldec lced) wf
  = ldecide (logdec-weaken-prog ldec wf) (logced-weaken-prog lced wf)
log-weaken-prog (l∃R log wfM) wf = l∃R (log-weaken-prog log wf) wfM
log-weaken-prog (l⇒R log) wf = l⇒R {!swap κ κ₁ !}
log-weaken-prog (l∀R log) wf = l∀R (log-weaken-prog log (prog-weaken-sig wf (log-val-sig log)))
log-weaken-prog (logrefl wf') wf = logrefl wf
log-weaken-prog (lap log refl) wf = lap (log-weaken-prog log wf) refl
log-weaken-prog (lex log refl) wf = lex (log-weaken-prog log wf) refl
log-weaken-prog (llam log) wf = llam (log-weaken-prog log wf)

logdec-weaken-prog (linit refl refl) wf = linit refl refl
logdec-weaken-prog (l⇒L log ldec) wf
  = l⇒L (log-weaken-prog log wf) (logdec-weaken-prog ldec wf)
logdec-weaken-prog (l∀L ldec wfM) wf = l∀L (logdec-weaken-prog ldec wf) wfM
logdec-weaken-prog (lapdec ldec refl) wf = lapdec (logdec-weaken-prog ldec wf) refl
logdec-weaken-prog (lexdec ldec refl) wf = lexdec (logdec-weaken-prog ldec wf) refl
logdec-weaken-prog (llamdec ldec) wf = llamdec (logdec-weaken-prog {!!} {!!})

logced-weaken-prog (ldecide⁻ κ∷D∈P wf') wf = ldecide⁻ (there κ∷D∈P) wf
logced-weaken-prog (l⇒L⁻ lced log) wf
  = l⇒L⁻ (logced-weaken-prog lced wf) (log-weaken-prog log wf)
logced-weaken-prog (l∀L⁻ lced) wf = l∀L⁻ (logced-weaken-prog lced wf)






-- if logrel is with proof term then the annotating MT is PT as well


pt : {S : Sig} {P : Prog} {Γ : Ctx}  {A : T} {e : PT } { e₁ : MT } {D₁ : De} →

  logreldec S P Γ e₁ D₁ (inMT e) (go (at A)) →
  ∃ λ e₁' → e₁ ≡ inMT e₁'

pt {e = e} (linit y refl) = e , y
pt {e = e} {e₁ = e₁} (l⇒L log ldec) with pt ldec
... | symbP x , ()
pt {e = e} {.(inMT e')} (l⇒L log ldec) | (e' apP e'') , refl = e' , refl
... | < x , e' >P , ()
... | lamP x e' , ()
pt {e = e} {e₁} (l∀L ldec x₂) = pt ldec



-- substitutivity


import Syntax
open import Relation.Binary.PropositionalEquality using (subst)


{-
-- substitutivity of wfGo and wfDe

qwi : ∀ {S : Sig} {Γ : Ctx} {A B : T} {x : Var} {M : t} →
      S + Γ ⊢ A ∷T o →
      S + Γ ⊢ M ∷ B →
      x ∷ B ∈ Γ →
      S + Γ ⊢ (A [ M / x ]T) ∷T o

qwi = {!!}

buq : ∀ {S : Sig} {Γ : Ctx}  {D : De} {x : Var} {M : t} {B : T} →
      S + Γ ⊢ D ∷De →
      S + Γ ⊢ M ∷ B →
      x ∷ B ∈ Γ →      
      {- x ∉ Γ -}
      S + Γ ⊢ D [ M / x ]De ∷De

bur : ∀ {S : Sig} {Γ : Ctx} {G : Go} {x : Var} {M : t} {B : T} →
      S + Γ ⊢ G ∷Go →
      S + Γ ⊢ M ∷ B →
      x ∷ B ∈ Γ →      
      {- x ∉ Γ -}
      S + Γ ⊢ G [ M / x ]Go ∷Go


buq (Syntax.at-de x₁) wfM inΓ = Syntax.at-de (qwi x₁ wfM inΓ)
buq (Syntax.⇒-de x₁ wf) wfM inΓ = Syntax.⇒-de (bur x₁  wfM inΓ ) (buq wf  wfM inΓ )
buq (Syntax.∀-de wf) wfM inΓ  = Syntax.∀-de {!x ≠ y!}

bur (Syntax.at-go x₁)  wfM inΓ = {!!}
bur (Syntax.⇒-go x₁ wf)  wfM inΓ = Syntax.⇒-go (buq x₁  wfM inΓ ) (bur wf  wfM inΓ )
bur (Syntax.∃-go wf)  wfM inΓ  = {!∃-go ?!}
bur (Syntax.∀-go wf)  wfM inΓ  = Syntax.∀-go {!x ‌≠ y!}
-}



-- stable under substitution
log-stab : ∀ {S : Sig} {P : Prog} {Γ : Ctx} {x : Var} {κ : Κ}
           {e₁ e₂ : MT} {D : De} {M : t} →
         logrel S (P , κ ∷ D) Γ e₁ e₂ →
         logrel S (P , κ ∷ (D [ M / x ]De)) Γ e₁ e₂


ldec-stab :  ∀ {S : Sig} {P : Prog} {Γ : Ctx} {x : Var} {κ : Κ}
           {e₁ e' : MT} {D D' : De} {A : T} {M : t} →
           logreldec S (P , κ ∷ D) Γ e' D' e₁ (go (at A)) →
           logreldec S (P , κ ∷ (D [ M / x ]De)) Γ e' D' e₁ (go (at A))

lced-stab : ∀ {S : Sig} {P : Prog} {Γ : Ctx} {x : Var} {κ : Κ}
           { e' : MT} {D D' : De} {M : t} →
            logrelced S (P , κ ∷ D) Γ e' D' →
            logrelced S (P , κ ∷ (D [ M / x ]De)) Γ e' D'


log-stab (ldecide x₁ x₂) = ldecide (ldec-stab x₁) (lced-stab x₂)
log-stab (l∃R log x₂) = l∃R (log-stab log) x₂
log-stab (l⇒R log) = l⇒R {!log-stab log!}
log-stab (l∀R log) = l∀R (log-stab log)
log-stab (logrefl x₁) = logrefl (prog-stab x₁)
log-stab (lap log x₁) = lap (log-stab log) x₁
log-stab (lex log x₁) = lex (log-stab log) x₁
log-stab (llam log) = llam (log-stab log)

ldec-stab (linit x₁ x₂) = linit x₁ x₂
ldec-stab (l⇒L x₁ ldec) = l⇒L (log-stab x₁) (ldec-stab ldec)
ldec-stab (l∀L ldec x₂) = l∀L (ldec-stab ldec) x₂

lced-stab (ldecide⁻ Syntax.here x₂) = ldecide⁻ {!!} (prog-stab x₂)
lced-stab (ldecide⁻ (Syntax.there x₁) x₂) = ldecide⁻ (there x₁) (prog-stab x₂)
lced-stab (l⇒L⁻ lced x₁) = l⇒L⁻ (lced-stab lced) (log-stab x₁)
lced-stab (l∀L⁻ lced) = l∀L⁻ (lced-stab lced)


log-subst : ∀ {S : Sig} {P : Prog} {Γ : Ctx} {e e'  : MT} 
              {B : T} { M : t } { x : Var } {G : Go} →
            logrel S P (Γ) e (go G) →
            S + Γ ⊢ M ∷ B → 
            logrel S P Γ e (go (G [ M / x ]Go))

logdec-subst : {S : Sig} {P : Prog} {Γ' : Ctx} {e e'  : MT} 
                 {M : t} {D : De} {A : T} {x : Var} →
            logreldec S P Γ' e' D e (go (at A)) →
            logreldec S P Γ' e' (D [ M / x ]De) e (go (at (A )))

logced-subst : ∀ {S P Γ e x A D M} →

    logrelced S P (Γ , x ∷ A) e D →
    S + Γ ⊢ M ∷ A → 
    logrelced S P Γ e (D [ M / x ]De)


log-subst (ldecide x₁ x₂) wfM = ldecide (logdec-subst {!x₁!}) (logced-subst {!logced-weak!} wfM)
log-subst (l∃R log x₂) wfM =  {!l∃R !}
log-subst (l⇒R log) wfM = l⇒R (log-stab (log-subst log wfM))
log-subst (l∀R log) wfM = l∀R ( {!log-weaken-sig!})
log-subst (logrefl x₁) wfM =  {!!}


logdec-subst (linit x₁ x₂) = linit x₁ {!!}
logdec-subst (l⇒L x₁ ldec) = l⇒L (log-subst x₁ {!!}) (logdec-subst ldec)
logdec-subst (l∀L ldec x₂) = l∀L (logdec-subst {!ldec!}) {!trm-subst!}

logced-subst (ldecide⁻ x₁ x₂) wfM = {!!} -- ldecide⁻ {!prog-stab!} ?
logced-subst (l⇒L⁻ lced x₁) wfM =  l⇒L⁻ (logced-subst lced wfM) (log-subst {!x₁!} wfM)
logced-subst (l∀L⁻ lced) wfM = l∀L⁻ {!weaken!}



{-
  IN LogRel.Subst
-}


lced-∀lift' : ∀ {S P Γ e x A A₁ D G } →
  logrelced S P Γ (e) G →
  G ≡ (at A₁ ⇒ ∀De x A D) →
  logrelced S P (Γ , x ∷ A) (e) (at A₁ ⇒ D)

lced-∀lift' (ldecide⁻ x₁ x₂) eq = {!!}
lced-∀lift' (l⇒L⁻ lced x₁) refl = l⇒L⁻ {!!} {!!}
lced-∀lift' (l∀L⁻ lced) ()


lced-∀lift : ∀ {S P Γ e x A A₁ D } →
  logrelced S P Γ (e) (at A₁ ⇒ ∀De x A D) →
  logrelced S P (Γ , x ∷ A) (e) (at A₁ ⇒ D)

{-
lced-∀lift (ldecide⁻ x₁ x₂) = {!!}
lced-∀lift (l⇒L⁻ lced x₁) = {!!}
-}
lced-∀lift = {!!}

lced-∀inv : ∀ {S P Γ e x A D} →
  logrelced S P Γ (e) (∀De x A D) →
  logrelced S P (Γ , x ∷ A) (e) D

{-
lced-∀inv (ldecide⁻ x₁ x₂) = {!!}
lced-∀inv (l⇒L⁻ lced x₁) = l⇒L⁻ ((lced-∀lift lced)) {!!}
lced-∀inv (l∀L⁻ lced) = lced
-}
lced-∀inv = {!!}

{- lifting of inference rules -}


open import Syntax using (symbP ; <_,_>P ; lamP )


lift-ldecide-pt : {S : Sig} {P : Prog} {Γ : Ctx } {e e₁ : PT} {D : De}  {A : T} →
  logreldec S P Γ (inMT e₁) D (inMT e) (go (at A)) →
  logrelced S P Γ (inMT e₁) D →
  logrel S P Γ (inMT e) (go (at A))
 
lift-ldecide-pt (linit eq refl) lced
  with injective-inMT eq
... | refl = ldecide (linit refl refl) lced

lift-ldecide-pt (l⇒L log ldec) lced
  with pt ldec
... | symbP x₁ , ()
... | < _ , e₃ >P , ()
... | lamP _ e₃ , ()
... | (e₃ apP e₄) , eq
  with inspect-apM eq
... | e' , refl  = ldecide ldec (l⇒L⁻ lced log)

lift-ldecide-pt (l∀L ldec wfM) lced
  with pt ldec
... | e' , eq
  with injective-inMT eq
... | refl = lift-ldecide-pt ldec (logced-subst (lced-∀inv lced) wfM)



lift-ldecide : {S : Sig} {P : Prog} {Γ Γ' : Ctx} {e' : MT}
      {θ' : Θ S Γ Γ' } {C : RewC } {A :  T} {κ : Κ} {D : De} →
    logreldec S P Γ' (symbM κ) D e' (go (at A)) →
    logrelced S P Γ' (symbM κ) D →
    logrel S P Γ' ((θ' ΘC C) [ e' ]) (C [ go (at A) ])

lift-ldecide {C = SyntaxRew.●} logdec logced = ldecide logdec logced
lift-ldecide {C = x SyntaxRew.ap C} logdec logced = lap (lift-ldecide logdec logced) refl
lift-ldecide {C = SyntaxRew.< x , C >} logdec logced = lex (lift-ldecide logdec logced) refl
lift-ldecide {C = SyntaxRew.lam x C} logdec logced = llam (lift-ldecide logdec logced)



lift-∃R : {S : Sig} {P : Prog}  {Γ₁ Γ : Ctx} {A : T} {e : MT} {C : RewC} {θ : Θ S Γ₁ Γ }
  {x : Var} {M : t} {G : Go} →
  logrel S P Γ e  (go G)  →
  S + Γ ⊢ M ∷ A →
  logrel S P Γ ((θ ΘC C) [ < M , e >M ] ) (C [ go (∃Go x A G) ])

lift-∃R {C = SyntaxRew.●} logrel wf = l∃R (log-subst logrel wf) wf

lift-∃R {C = x SyntaxRew.ap C} logrel wf = lap (lift-∃R logrel wf) refl
lift-∃R {C = SyntaxRew.< x , C >} logrel wf = lex (lift-∃R logrel wf) refl
lift-∃R {C = SyntaxRew.lam x C} logrel wf = llam (lift-∃R logrel wf)



lift-⇒R : {S : Sig} {P : Prog} {Γ₁ Γ : Ctx} {κ : Κ} {e : MT} {C : RewC}  {θ : Θ S Γ₁ Γ }
  {G : Go} {D : De} →
  logrel S (P , κ ∷ D) Γ e  (go G) →
  logrel S P Γ ((θ ΘC C) [ lamM κ e ] ) (C [ go (D ⇒ G) ])
lift-⇒R {C = SyntaxRew.●} log = l⇒R log
lift-⇒R {C = x SyntaxRew.ap C} log = lap (lift-⇒R log) refl
lift-⇒R {C = SyntaxRew.< x , C >} log = lex (lift-⇒R log) refl
lift-⇒R {C = SyntaxRew.lam x C} log = llam (lift-⇒R log)


lift-∀R : {S : Sig} {P : Prog} {Γ₁ Γ : Ctx} {x : Var} {e : MT} {C : RewC}
  {A : T} {G : Go} {θ : Θ S Γ₁ Γ } →
  logrel S P Γ e (go G) →
  logrel S P Γ ((θ ΘC C) [ e ]) (C [ go (∀Go x A G) ])
lift-∀R {C = SyntaxRew.●} log = l∀R ({!log-weaken-sig log ?!})
lift-∀R {C = x₁ SyntaxRew.ap C} log = lap (lift-∀R log) refl
lift-∀R {C = SyntaxRew.< x₁ , C >} log = lex (lift-∀R log) refl
lift-∀R {C = SyntaxRew.lam x₁ C} log = llam (lift-∀R log)


{-
lift-linit : {S : Sig} {P : Prog} {Γ : Ctx} {e e' e₁ : MT} {A A' A₁ : T} →
      S + Γ ⊢ e ∷ A ≣T e' ∷ A'  →
      logreldec S P Γ C (at A) (e' apM (go (at A₁))) (go (at A'))

lift-linit eq eq' log = {!!}
-}

lift-linit : {S : Sig} {P : Prog} {Γ Γ' : Ctx} {A A' : T} {e' : MT}
      {σ : Θ S Γ Γ'}  {C : RewC} →
    S + Γ' ⊢ σ ΘT A ≡T σ ΘT A' ∷ o →
    logrelced S P Γ e' (at A') →
    logreldec S P Γ' e' (at A') (C [ e' ]) (C [ go (at A) ])

lift-linit {C = SyntaxRew.●} wf lced = linit refl {!wf !}
lift-linit {C = x SyntaxRew.ap C} wf lced = lapdec {θ = ε} (lift-linit wf lced) {!refl!}
lift-linit {C = SyntaxRew.< x , C >} wf lced = lexdec {θ = ε} (lift-linit wf lced) {!refl!}
lift-linit {C = SyntaxRew.lam x C} wf lced = llamdec (lift-linit wf {!weaken!})



lift-⇒L : {S : Sig} {P : Prog} {Γ : Ctx} {e e₁ e₂ ê₂  : MT} {A₁ : T} {D : De} →
   logrel S P Γ e₁ (go (at A₁)) →
   logreldec S P Γ (e apM e₁) D e₂ ê₂ →
   logreldec S P Γ e (at A₁ ⇒ D) e₂ ê₂

lift-⇒L {ê₂ = SyntaxRew.symbM x} log ()
lift-⇒L {ê₂ = go (at x)} log ldec = l⇒L log ldec

lift-⇒L {ê₂ = go (x ⇒ x₁)} log ()
lift-⇒L {ê₂ = go (∃Go x x₁ x₂)} log ()
lift-⇒L {ê₂ = go (∀Go x x₁ x₂)} log ()

lift-⇒L {ê₂ = ê₂ SyntaxRew.apM ê₃} log (lapdec ldec refl)
  = lapdec (lift-⇒L log ldec) refl

lift-⇒L {ê₂ = SyntaxRew.< x , ê₂ >M} log (lexdec ldec refl)
  = lexdec (lift-⇒L log ldec) refl
  
lift-⇒L {ê₂ = SyntaxRew.lamM x ê₂} log (llamdec ldec)
  = llamdec (lift-⇒L (log-weaken-prog log (logdec-val-prog ldec)) ldec)


lift-∀L : {S : Sig} {P : Prog} {Γ : Ctx} { e e₂ ê : MT} {x : Var} {A₁ : T} {D : De} {M : t}  →
   logreldec S P Γ e (D [ M / x ]De) e₂ ê →
   S + Γ ⊢ M ∷ A₁ →
   logreldec S P Γ e (∀De x A₁ D) e₂ ê
lift-∀L {ê = symbM κ} () S+Γ⊢M∷A
lift-∀L {ê = go (at A)} ldec S+Γ⊢M∷A = l∀L ldec S+Γ⊢M∷A
lift-∀L {ê = go (_ ⇒ G)} () S+Γ⊢M∷A
lift-∀L {ê = go (∃Go x A G)} () S+Γ⊢M∷A 
lift-∀L {ê = go (∀Go x A G)} () S+Γ⊢M∷A 
lift-∀L {ê = ê apM ê₁} (lapdec ldec x) S+Γ⊢M∷A = lapdec (lift-∀L ldec S+Γ⊢M∷A) x
-- lift-∀L {ê = ê apM ê₁} () _
lift-∀L {ê = < M , ê >M} (lexdec ldex x) S+Γ⊢M∷A = lexdec (lift-∀L ldex S+Γ⊢M∷A) x
--lift-∀L {ê = < M , ê >M} () S+Γ⊢M∷A
lift-∀L {ê = lamM κ ê} (llamdec ldec) S+Γ⊢M∷A = llamdec (lift-∀L ldec S+Γ⊢M∷A)
--lift-∀L {ê = lamM κ ê} () S+Γ⊢M∷A



lift-∀L' : {S : Sig} {P : Prog} {Γ₁ Γ : Ctx} { e e₂ ê : MT} {x : Var} {A₁ : T} {D : De} {M : t}
  {C : RewC}  {θ : Θ S Γ₁ Γ } →
   logreldec S P Γ e (D [ M / x ]De) e₂ ê →
   S + Γ ⊢ M ∷ A₁ →
   logreldec S P Γ e (∀De x A₁ D)  ((θ ΘC C) [ e₂ ]) (C [  ê ] )

lift-∀L' {C = SyntaxRew.●} ldec wf = lift-∀L ldec wf
lift-∀L' {C = x₁ SyntaxRew.ap C} ldec wf = lapdec (lift-∀L' ldec wf) refl
lift-∀L' {C = SyntaxRew.< x₁ , C >} ldec wf = lexdec (lift-∀L' ldec wf) refl
lift-∀L' {C = SyntaxRew.lam x₁ C} ldec wf = llamdec (lift-∀L' {!ldec!} wf)