-- checked on Agda 2.5.2, standard library 0.13

module reduce-pe where

open import Data.List
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import deBruijn-cbn

-- reduction relation
data reduce {Γ : Cxt} : {τ₁ : typ} → term Γ τ₁ → term Γ τ₁ → Set where
  rBeta : {τ₁ τ₂ : typ} → (e₁ : term (τ₂ ∷ Γ) τ₁) → (v : term Γ τ₂) →
          reduce (App (Val (Fun τ₂ e₁)) v) (sub0 v e₁)
  rApp₁ : {τ₁ τ₂ : typ} → {e₁ e₁′ : term Γ (τ₂ ⇒ τ₁)} → (e₂ : term Γ τ₂) →
          reduce e₁ e₁′ → reduce (App e₁ e₂) (App e₁′ e₂)
  rApp₂ : {τ₁ τ₂ : typ} → (e₁ : term Γ (τ₂ ⇒ τ₁)) → {e₂ e₂′ : term Γ τ₂} →
          reduce e₂ e₂′ → reduce (App e₁ e₂) (App e₁ e₂′)
  rFun  : {τ₁ τ₂ : typ} → {e₁ e₁′ : term (τ₂ ∷ Γ) τ₁} →
          reduce e₁ e₁′ → reduce (Val (Fun τ₂ e₁)) (Val (Fun τ₂ e₁′))

data reduce* {Γ : Cxt} {τ₁ : typ} : term Γ τ₁ → term Γ τ₁ → Set where
  r*Id    : {e : term Γ τ₁} → reduce* e e
  r*Trans : (e₁ e₂ e₃ : term Γ τ₁) →
            reduce e₁ e₂ → reduce* e₂ e₃ → reduce* e₁ e₃

-- equational reasoning
module red-Reasoning {Γ : Cxt} {τ : typ} where
  infix  3 _∎
  infixr 2 _⟶⟨_⟩_ _⟶*⟨_⟩_ _≡⟨_⟩_
  infix  1 begin_

  begin_ : {e₁ e₂ : term Γ τ} →
           reduce* e₁ e₂ → reduce* e₁ e₂
  begin_ red = red

  _⟶⟨_⟩_ : (e₁ {e₂ e₃} : term Γ τ) →
            reduce e₁ e₂ → reduce* e₂ e₃ → reduce* e₁ e₃
  _⟶⟨_⟩_ e₁ {e₂} {e₃} e₁-red-e₂ e₂-red*-e₃ =
    r*Trans e₁ e₂ e₃ e₁-red-e₂ e₂-red*-e₃

  _⟶*⟨_⟩_ : (e₁ {e₂ e₃} : term Γ τ) →
              reduce* e₁ e₂ → reduce* e₂ e₃ → reduce* e₁ e₃
  _⟶*⟨_⟩_ e₁ {.e₁} {e₃} r*Id e₁-red*-e₃ = e₁-red*-e₃
  _⟶*⟨_⟩_ e₁ {.e₃} {e₄} (r*Trans .e₁ e₂ e₃ e₁-red-e₂ e₂-red*-e₃) e₃-red*-e₄ =
    r*Trans e₁ e₂ e₄ e₁-red-e₂ (e₂ ⟶*⟨ e₂-red*-e₃ ⟩ e₃-red*-e₄ )

  _≡⟨_⟩_ : (e₁ {e₂ e₃} : term Γ τ) → e₁ ≡ e₂ → reduce* e₂ e₃ →
             reduce* e₁ e₃
  _≡⟨_⟩_ e₁ {e₂} {e₃} refl e₂-red-e₃ = e₂-red-e₃

  _∎ : (e : term Γ τ) → reduce* e e
  _∎ e = r*Id

rApp₁* : {τ₁ τ₂ : typ} → {Γ : Cxt} → {e₁ e₁′ : term Γ (τ₂ ⇒ τ₁)} →
         (e₂ : term Γ τ₂) → reduce* e₁ e₁′ →
         reduce* (App e₁ e₂) (App e₁′ e₂)
rApp₁* e₂ r*Id = r*Id
rApp₁* e₂ (r*Trans e₁ e₁′ e₁′′ red red*) = begin
    App e₁ e₂
  ⟶⟨ rApp₁ e₂ red ⟩
    App e₁′ e₂
  ⟶*⟨ rApp₁* e₂ red* ⟩
    App e₁′′ e₂
  ∎
  where open red-Reasoning

rApp₂* : {τ₁ τ₂ : typ} → {Γ : Cxt} → (e₁ : term Γ (τ₂ ⇒ τ₁)) →
         {e₂ e₂′ : term Γ τ₂} → reduce* e₂ e₂′ →
         reduce* (App e₁ e₂) (App e₁ e₂′)
rApp₂* e r*Id = r*Id
rApp₂* e (r*Trans e₁ e₂ e₃ red red*) = begin
    App e e₁
  ⟶⟨ rApp₂ e red ⟩
    App e e₂
  ⟶*⟨ rApp₂* e red* ⟩
    App e e₃
  ∎
  where open red-Reasoning

rFun* : {τ₂ τ₁ : typ} → {Γ : Cxt} → {e₁ e₁′ : term (τ₂ ∷ Γ) τ₁} →
        reduce* e₁ e₁′ →
        reduce* (Val (Fun τ₂ e₁)) (Val (Fun τ₂ e₁′))
rFun* r*Id = r*Id
rFun* {τ₂} (r*Trans e₁ e₁′ e₁′′ red red*) = begin
    Val (Fun τ₂ e₁)
  ⟶⟨ rFun red ⟩
    Val (Fun τ₂ e₁′)
  ⟶*⟨ rFun* red* ⟩
    Val (Fun τ₂ e₁′′)
  ∎
  where open red-Reasoning

-- equality relation
data equal {Γ : Cxt} : {τ₁ : typ} → term Γ τ₁ → term Γ τ₁ → Set where
  eqBeta : {τ₁ τ₂ : typ} → (e₁ : term (τ₂ ∷ Γ) τ₁) → (v : term Γ τ₂) →
           equal (App (Val (Fun τ₂ e₁)) v) (sub0 v e₁)
  eqApp₁ : {τ₁ τ₂ : typ} → {e₁ e₁′ : term Γ (τ₂ ⇒ τ₁)} → (e₂ : term Γ τ₂) →
           equal e₁ e₁′ → equal (App e₁ e₂) (App e₁′ e₂)
  eqApp₂ : {τ₁ τ₂ : typ} → (e₁ : term Γ (τ₂ ⇒ τ₁)) → {e₂ e₂′ : term Γ τ₂} →
           equal e₂ e₂′ → equal (App e₁ e₂) (App e₁ e₂′)
  eqFun  : {τ₁ τ₂ : typ} → {e₁ e₁′ : term (τ₂ ∷ Γ) τ₁} →
           equal e₁ e₁′ → equal (Val (Fun τ₂ e₁)) (Val (Fun τ₂ e₁′))
  eqId     : {τ₁ : typ} → {e : term Γ τ₁} →
             equal e e
  eqTrans  : {τ₁ : typ} → (e₁ e₂ e₃ : term Γ τ₁) →
             equal e₁ e₂ → equal e₂ e₃ → equal e₁ e₃
  eqTrans′ : {τ₁ : typ} → (e₁ e₂ e₃ : term Γ τ₁) →
             equal e₂ e₁ → equal e₂ e₃ → equal e₁ e₃

-- equational reasoning
module eq-Reasoning {Γ : Cxt} {τ : typ} where
  infix  3 _∎
  infixr 2 _⟶⟨_⟩_ _⟵⟨_⟩_ _⟷⟨_⟩_ _≡⟨_⟩_
  infix  1 begin_
  
  begin_ : {e₁ e₂ : term Γ τ} →
           equal e₁ e₂ → equal e₁ e₂
  begin_ red = red
  
  _⟶⟨_⟩_ : (e₁ {e₂ e₃} : term Γ τ) →
            equal e₁ e₂ → equal e₂ e₃ → equal e₁ e₃
  _⟶⟨_⟩_ e₁ {e₂} {e₃} e₁-eq-e₂ e₂-eq-e₃ = eqTrans e₁ e₂ e₃ e₁-eq-e₂ e₂-eq-e₃
  
  _⟵⟨_⟩_ : (e₁ {e₂ e₃} : term Γ τ) →
            equal e₂ e₁ → equal e₂ e₃ → equal e₁ e₃
  _⟵⟨_⟩_ e₁ {e₂} {e₃} e₂-eq-e₁ e₂-eq-e₃ = eqTrans′ e₁ e₂ e₃ e₂-eq-e₁ e₂-eq-e₃
  
  _⟷⟨_⟩_ : (e₁ {e₂ e₃} : term Γ τ) →
            equal e₁ e₂ → equal e₂ e₃ → equal e₁ e₃
  _⟷⟨_⟩_ e₁ {e₂} {e₃} e₁-eq-e₂ e₂-eq-e₃ = eqTrans e₁ e₂ e₃ e₁-eq-e₂ e₂-eq-e₃
  
  _≡⟨_⟩_ : (e₁ {e₂ e₃} : term Γ τ) → e₁ ≡ e₂ → equal e₂ e₃ →
             equal e₁ e₃
  _≡⟨_⟩_ e₁ {e₂} {e₃} refl e₂-eq-e₃ = e₂-eq-e₃
  
  _∎ : (e : term Γ τ) → equal e e
  _∎ e = eqId

eq-sym : {Γ : Cxt} {τ : typ} {e₁ e₂ : term Γ τ} → equal e₁ e₂ → equal e₂ e₁
eq-sym {e₁ = e₁} {e₂} eq₁₂ = begin
    e₂
  ⟵⟨ eq₁₂ ⟩
    e₁
  ∎
  where open eq-Reasoning

-- relationship between reduction and equality
reduce-equal : {Γ : Cxt} {τ : typ} {e₁ e₂ : term Γ τ} →
               reduce e₁ e₂ → equal e₁ e₂
reduce-equal (rBeta e v) = eqBeta e v
reduce-equal (rApp₁ e₂ red) = eqApp₁ e₂ (reduce-equal red)
reduce-equal (rApp₂ e₁ red) = eqApp₂ e₁ (reduce-equal red)
reduce-equal (rFun red) = eqFun (reduce-equal red)

reduce*-equal : {Γ : Cxt} {τ : typ} {e₁ e₂ : term Γ τ} →
                reduce* e₁ e₂ → equal e₁ e₂
reduce*-equal r*Id = eqId
reduce*-equal (r*Trans e₁ e₂ e₃ red red*) =
  eqTrans e₁ e₂ e₃ (reduce-equal red) (reduce*-equal red*)

-- various properties
reduce-ren : {Γ Δ : Cxt} (xs : Ren Γ Δ)
              {τ : typ} {e e′ : term Δ τ} →
              reduce e e′ → reduce (ren xs e) (ren xs e′)
reduce-ren xs (rBeta {τ₂ = τ₂} e₁ v)
  rewrite rensub0 xs v e₁ = rBeta (ren (liftr xs) e₁) (ren xs v)
reduce-ren xs (rApp₁ e₂ red) = rApp₁ (ren xs e₂) (reduce-ren xs red)
reduce-ren xs (rApp₂ e₁ red) = rApp₂ (ren xs e₁) (reduce-ren xs red)
reduce-ren xs (rFun red) = rFun (reduce-ren (liftr xs) red)

reduce*-ren : {Γ Δ : Cxt} (xs : Ren Γ Δ)
               {τ : typ} {e e′ : term Δ τ} →
               reduce* e e′ → reduce* (ren xs e) (ren xs e′)
reduce*-ren xs r*Id = r*Id
reduce*-ren xs (r*Trans e₁ e₂ e₃ red red*) = begin
    ren xs e₁
  ⟶⟨ reduce-ren xs red ⟩
    ren xs e₂
  ⟶*⟨ reduce*-ren xs red* ⟩
    ren xs e₃
  ∎
  where open red-Reasoning

{-
reduce*-weak : {Γ Δ : Cxt} {τ σ : typ} {e e′ : term Δ τ} →
               reduce* e e′ → reduce* (weak σ e) (weak σ e′)
reduce*-weak red* = reduce*-ren (wkr renId) red*
-}

ren-weak : {Γ Δ : Cxt} {σ : typ} (τ : typ) (xs : Ren Γ Δ) (e : term Δ σ) →
           ren (liftr xs) (weak τ e) ≡ weak τ (ren xs e)
ren-weak τ xs e = begin
    ren (liftr xs) (weak τ e)
  ≡⟨ refl ⟩
    ren (zero ∷ wkr xs) (ren (wkr renId) e)
  ≡⟨ sym (rencomp (zero ∷ wkr xs) (wkr renId) e) ⟩
    ren (renComp (zero ∷ wkr xs) (wkr renId)) e
  ≡⟨ cong (λ l → ren l e) (lemrr (wkr xs) zero renId) ⟩
    ren (renComp (wkr xs) renId) e
  ≡⟨ cong (λ l → ren l e) (ridr (wkr xs)) ⟩
    ren (wkr xs) e
  ≡⟨ cong (λ l → ren (wkr l) e) (sym (lidr xs)) ⟩
    ren (wkr (renComp renId xs)) e
  ≡⟨ cong (λ l → ren l e) (sym (wkrcomp renId xs)) ⟩
    ren (renComp (wkr renId) xs) e
  ≡⟨ rencomp (wkr renId) xs e ⟩
    ren (wkr renId) (ren xs e)
  ≡⟨ refl ⟩
    weak τ (ren xs e)
  ∎
  where open ≡-Reasoning

equal-ren : {Γ Δ : Cxt} (xs : Ren Γ Δ)
            {τ : typ} {e e′ : term Δ τ} →
            equal e e′ → equal (ren xs e) (ren xs e′)
equal-ren xs (eqBeta e v)
  rewrite rensub0 xs v e = eqBeta (ren (liftr xs) e) (ren xs v)
equal-ren xs (eqApp₁ e₂ eq) = eqApp₁ (ren xs e₂) (equal-ren xs eq)
equal-ren xs (eqApp₂ e₁ eq) = eqApp₂ (ren xs e₁) (equal-ren xs eq)
equal-ren xs (eqFun eq) = eqFun (equal-ren (liftr xs) eq)
equal-ren xs eqId = eqId
equal-ren xs (eqTrans e₁ e₂ e₃ eq₁₂ eq₂₃) =
  eqTrans (ren xs e₁) (ren xs e₂) (ren xs e₃)
          (equal-ren xs eq₁₂) (equal-ren xs eq₂₃)
equal-ren xs (eqTrans′ e₁ e₂ e₃ eq₂₁ eq₂₃) =
  eqTrans′ (ren xs e₁) (ren xs e₂) (ren xs e₃)
           (equal-ren xs eq₂₁) (equal-ren xs eq₂₃)

mutual
  reduce-ne : ∀ {Γ τ} {e e′ : term Γ τ} (ne : ne Γ τ) →
              e ≡ embedNe ne → reduce e e′ → ⊥
  reduce-ne (Var x) refl ()
  reduce-ne (App (Var x) nf) () (rBeta e₁ v)
  reduce-ne (App (App ne x) nf) () (rBeta e₁ v)
  reduce-ne (App ne nf) refl (rApp₁ .(embedNf nf) red)
    with reduce-ne ne refl red
  ... | ()
  reduce-ne (App ne nf) refl (rApp₂ .(embedNe ne) red)
    with reduce-nf nf refl red
  ... | ()
  reduce-ne (App ne₁ nf₁) () (rFun red)

  reduce-nf : ∀ {Γ τ} {e e′ : term Γ τ} (nf : nf Γ τ) →
              e ≡ embedNf nf → reduce e e′ → ⊥
  reduce-nf (Ne ne) refl red = reduce-ne ne refl red
  reduce-nf (Num n) refl ()
  reduce-nf (Fun τ nf) refl (rFun red) = reduce-nf nf refl red

mutual
  reduce*-ne : ∀ {Γ τ} {e : term Γ τ} (ne : ne Γ τ) →
              reduce* (embedNe ne) e → e ≡ embedNe ne
  reduce*-ne ne r*Id = refl
  reduce*-ne ne (r*Trans .(embedNe ne) e₂ e₃ red red*)
    with reduce-ne ne refl red
  ... | ()

  reduce*-nf : ∀ {Γ τ} {e : term Γ τ} (nf : nf Γ τ) →
              reduce* (embedNf nf) e → e ≡ embedNf nf
  reduce*-nf nf r*Id = refl
  reduce*-nf nf (r*Trans .(embedNf nf) e₂ e₃ red red*)
    with reduce-nf nf refl red
  ... | ()