module PLFA.Properties where

open import Relation.Binary.PropositionalEquality
  using (_≡_; _≢_; refl; sym; cong; cong₂)
open import Data.String using (String; _≟_)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product
  using (_×_; proj₁; proj₂; ∃; ∃-syntax)
  renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Function using (_∘_)
-- open import PLFA.Isomorphism
open import PLFA.Lambda

-- GOAL
-- by Progress and Preservation

{-

defined a lot of notions
* syntax of the lambda calculus
* evaluation by small step operational semantics
* syntax of types
* relation between (contexts) terms and types

so far missing: the link between semantics and the type system

we expect: 
if a term is well-typed, then it will reduce without type mismatches
(i.e., we will not encounter terms like "zero · M" or "suc (lam x ⇒ M)")
our typing rules will reject such terms, but who knows what happens during evaluation?

this is formalized as follows:
1. preservation: if M is typed and M reduces to N, then N is also typed (at the same type)
2. progress: a typed term M is either a value or it can make a reduction step

-}

-- * -- values do not reduce

V¬—→ : ∀ {M N} →
  Value M →
  ¬ (M —→ N)

V¬—→ V-ƛ ()
V¬—→ V-zero ()
V¬—→ (V-suc value-M) (ξ-suc M->N) = V¬—→ value-M M->N

—→¬V : ∀ {M N} →
  M —→ N →
  ¬ Value M

—→¬V (β-ƛ x) ()
—→¬V β-zero ()
—→¬V (β-suc x) ()
—→¬V β-μ ()
—→¬V (ξ-·₁ M->N) ()
—→¬V (ξ-·₂ x M->N) ()
—→¬V (ξ-suc M->N) (V-suc value-M) = —→¬V M->N value-M
—→¬V (ξ-case M->N) ()


-- * -- canonical forms and their relation to values

{- characterization of typed values -}

-- * -- progress (as a datatype: step, done)

{- a typed term is either a value or it can make a step -}

data Progress (M : Term) : Set where

  step : ∀ {N} → M —→ N → Progress M

  done : Value M → Progress M

{- a term that can neither reduce nor is a value:  " zero · zero "
-}

progress : ∀ {M} {T} → 
  ∅ ⊢ M ⦂ T →
  Progress M

progress (⇒-I ⊢M) = done V-ƛ
progress (⇒-E ⊢M ⊢M₁)
  with progress ⊢M
... | step M->N = step (ξ-·₁ M->N)
progress (⇒-E (⇒-I ⊢M) ⊢M₁) | done V-ƛ
  with progress ⊢M₁
... | step N->N' = step (ξ-·₂ V-ƛ N->N')
... | done value-N = step (β-ƛ value-N)
progress ℕ-I-zero = done V-zero
progress (ℕ-I-suc ⊢M)
  with progress ⊢M
... | step M->N = step (ξ-suc M->N)
... | done value-M = done (V-suc value-M)
progress (ℕ-E-case ⊢M ⊢M₁ ⊢M₂)
  with progress ⊢M
... | step M->N = step (ξ-case M->N)
... | done V-zero = step β-zero
... | done (V-suc value-M) = step (β-suc value-M)
progress (μ-E ⊢M) = step β-μ

-- * -- intermezzo: rename, weaken, drop, swap

{-
a context is a renaming of another context if it can satisfy the same bindings as the other

formally:

Δ is a renaming of Γ if
(∀ x → Γ ∋ x ⦂ T → Δ ∋ x ⦂ T)
-}

Renaming : Context → Context → Set
Renaming Γ Δ = ∀ {y T} → Γ ∋ y ⦂ T → Δ ∋ y ⦂ T

ext :
  ∀ { Γ Δ } { x } { A } →
  Renaming Γ Δ →
  Renaming (Γ , x ⦂ A) (Δ , x ⦂ A)

ext ρ Z = Z
ext ρ (S y≢x y∈Γ) = S y≢x (ρ y∈Γ)

rename :
  ∀ { Γ Δ } →
  Renaming Γ Δ →
  ----------------------------------------
  (∀ {M T} → Γ ⊢ M ⦂ T → Δ ⊢ M ⦂ T)

rename ρ (var x⦂T) = var (ρ x⦂T)
rename ρ (⇒-I ⊢M) = ⇒-I (rename (ext ρ) ⊢M)
rename ρ (⇒-E ⊢M ⊢M₁) = ⇒-E (rename ρ ⊢M) (rename ρ ⊢M₁)
rename ρ ℕ-I-zero = ℕ-I-zero
rename ρ (ℕ-I-suc ⊢M) = ℕ-I-suc (rename ρ ⊢M)
rename ρ (ℕ-E-case ⊢L ⊢M ⊢N) = ℕ-E-case (rename ρ ⊢L) (rename ρ ⊢M) (rename (ext ρ) ⊢N)
rename ρ (μ-E ⊢M) = μ-E (rename (ext ρ) ⊢M)

weaken :
  ∀ { Γ } { N } { A } →
  (⊢N : ∅ ⊢ N ⦂ A) →
  Γ ⊢ N ⦂ A

weaken ⊢N = rename (λ{ () }) ⊢N

drop :
  ∀ {Γ} {y} {A B} →
  Renaming ((Γ , y ⦂ A) , y ⦂ B) (Γ , y ⦂ B)

drop Z = Z
drop (S x≢y Z) = ⊥-elim (x≢y refl)
drop (S x≢y (S x≢y₁ x∈Γ)) = S x≢y x∈Γ
  
swap :
  ∀ { Γ } { y z } { A B } → 
  (y≢z : z ≢ y) →
  Renaming (Γ , y ⦂ A , z ⦂ B) (Γ , z ⦂ B , y ⦂ A)

swap y≢z Z = S y≢z Z
swap y≢z (S x≢z Z) = Z
swap y≢z (S x≢z (S x≢y x⦂t)) = S x≢y (S x≢z x⦂t)

subst-preserve :
  ∀ { Γ } { M N } { x } { A T }
  (⊢N      : ∅ ⊢ N ⦂ A) →
  (⊢M      : Γ , x ⦂ A ⊢ M ⦂ T) →
  ----------------------------------------
  Γ ⊢ M [ x := N ] ⦂ T

subst-preserve {x = x} ⊢N (var{x = y} y⦂T)
  with x ≟ y
subst-preserve {x = x} ⊢N (var {x = _} Z) | no ¬p = ⊥-elim (¬p refl)
subst-preserve {x = x} ⊢N (var {x = _} (S x₁ y⦂T)) | no ¬p = var y⦂T
subst-preserve {x = x} ⊢N (var {x = _} Z) | yes refl = weaken ⊢N
subst-preserve {x = x} ⊢N (var {x = _} (S x≢x y⦂T)) | yes refl = ⊥-elim (x≢x refl)
subst-preserve {x = x} ⊢N (⇒-I{ x = y} ⊢M)
  with x ≟ y
... | yes refl = ⇒-I (rename drop ⊢M)
... | no x≢y = ⇒-I (subst-preserve ⊢N (rename (swap (λ y≡x → x≢y (sym y≡x))) ⊢M))
subst-preserve ⊢N (⇒-E ⊢M ⊢M₁) = ⇒-E (subst-preserve ⊢N ⊢M) (subst-preserve ⊢N ⊢M₁)
subst-preserve ⊢N ℕ-I-zero = ℕ-I-zero
subst-preserve ⊢N (ℕ-I-suc ⊢M) = ℕ-I-suc (subst-preserve ⊢N ⊢M)
subst-preserve {x = x } ⊢N (ℕ-E-case{x = y} ⊢L ⊢M₁ ⊢M₂)
  with x ≟ y
... | yes refl = ℕ-E-case (subst-preserve ⊢N ⊢L) (subst-preserve ⊢N ⊢M₁) (rename drop ⊢M₂)
... | no x≢y  = ℕ-E-case (subst-preserve ⊢N ⊢L) (subst-preserve ⊢N ⊢M₁) (subst-preserve ⊢N (rename (swap (x≢y ∘ sym)) ⊢M₂))
subst-preserve {x = x} ⊢N (μ-E{x = y} ⊢M)
  with x ≟ y
... | yes refl = μ-E (rename drop ⊢M)
... | no x≢y  = μ-E (subst-preserve ⊢N (rename (swap (x≢y ∘ sym)) ⊢M))


-- * -- preservation

preserve : ∀ {M N} {T} → 
  ∅ ⊢ M ⦂ T →
  M —→ N →
  ∅ ⊢ N ⦂ T

preserve (⇒-E (⇒-I ⊢M) ⊢N) (β-ƛ value-N) = subst-preserve ⊢N ⊢M
preserve (ℕ-E-case ⊢M ⊢M₁ ⊢M₂) β-zero = ⊢M₁
preserve (ℕ-E-case (ℕ-I-suc ⊢L) ⊢M ⊢N) (β-suc value-L) = subst-preserve ⊢L ⊢N
preserve (μ-E ⊢M) β-μ = subst-preserve (μ-E ⊢M) ⊢M
preserve (⇒-E ⊢M ⊢M₁) (ξ-·₁ M->M')
  with preserve ⊢M M->M'
... | ⊢M' = ⇒-E ⊢M' ⊢M₁
preserve (⇒-E ⊢M ⊢N) (ξ-·₂ x N->N')
  with preserve ⊢N N->N'
... | ⊢N' = ⇒-E ⊢M ⊢N'
preserve (ℕ-I-suc ⊢M) (ξ-suc M->M')
  with preserve ⊢M M->M'
... | ⊢M' = ℕ-I-suc ⊢M'
preserve (ℕ-E-case ⊢L ⊢M ⊢N) (ξ-case L->L')
  with preserve ⊢L L->L'
... | ⊢L' = ℕ-E-case ⊢L' ⊢M ⊢N