-- checked on Agda 2.5.2, standard library 0.13

module reduce-cbn 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₂)

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₃

reduction-unique : {Γ : Cxt} {τ : typ} {e e₁ e₂ : term Γ τ} →
                   reduce e e₁ → reduce e e₂ → e₁ ≡ e₂
reduction-unique (rBeta e₁ v) (rBeta .e₁ .v) = refl
reduction-unique (rBeta e₁ v) (rApp₁ .v ())
reduction-unique (rApp₁ e₂ ()) (rBeta e₁ .e₂)
reduction-unique (rApp₁ e₂ red) (rApp₁ .e₂ red′) with reduction-unique red red′
... | refl = refl

-- 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

-- 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 : {Γ : 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*)