FLOLAC-STLC-sol.agda

open import Data.Nat
open import Data.Empty
  hiding (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
  hiding ([_])

infix  3 _⊢_ _=β_

infixr 7 _→̇_

infixr 5 ƛ_
infixl 7 _·_
infixl 8 _[_] _⟪_⟫
infixr 9 ᵒ_ `_ #_

data Type : Set where
  ⋆   : Type
  _→̇_ : Type → Type → Type

infixl 7 _⧺_
infixl 6 _,_
infix  4 _∋_

data Context : Set where
  ∅   :                  Context
  _,_ : Context → Type → Context

variable
  Γ Δ Ξ : Context
  A B C : Type

data _∋_ : Context → Type → Set where
  Z   ---------
    : Γ , A ∋ A

  S_ : Γ     ∋ A
       ---------
     → Γ , B ∋ A

variable
  x     : Γ ∋ A

_ : ∅ , A , B ∋ A
_ = S Z 

⊥-elim : ∀ {T : Set} → ⊥ → T
⊥-elim ()

lookup : Context → ℕ → Type
lookup (Γ , A) zero     =  A
lookup (Γ , B) (suc n)  =  lookup Γ n
lookup ∅       _        =  ⊥-elim impossible
  where postulate impossible : ⊥

count : (n : ℕ) → Γ ∋ lookup Γ n
count {Γ = Γ , _} zero     =  Z
count {Γ = Γ , _} (suc n)  =  S (count n)
count {Γ = ∅    }  _       =  ⊥-elim impossible
  where postulate impossible : ⊥

_ :  ∅ , A , B ∋ A
_ = count 1

_ : ∅ , B , A ∋ A
_ = count 0

ext
  : (∀ {A}   →     Γ ∋ A →     Δ ∋ A)
    ---------------------------------
  → (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
ext ρ Z      =  Z
ext ρ (S x)  =  S (ρ x)

_⧺_ : Context → Context → Context
Γ ⧺ ∅       = Γ
Γ ⧺ (Δ , x) = Γ ⧺ Δ , x

data _⊢_ (Γ : Context) : Type → Set where
  `_ : Γ ∋ A
       -----
     → Γ ⊢ A
     
  _·_ : Γ ⊢ A →̇ B
      → Γ ⊢ A
        -----
      → Γ ⊢ B

  ƛ_
    : Γ , A ⊢ B
      ---------
    → Γ ⊢ A →̇ B

variable
  M N L M′ N′ L′ : Γ ⊢ A
  
#_ : (n : ℕ) → Γ ⊢ lookup Γ n
# n  =  ` count n

nat : Type → Type
nat A = (A →̇ A) →̇ A →̇ A

c₀ : ∀ {A} → ∅ ⊢ nat A
c₀ = ƛ ƛ # 0

c₁ : ∀ {A} → ∅ ⊢ nat A
c₁ = ƛ ƛ # 1 · # 0

add : ∀ {A} → ∅ ⊢ nat A →̇ nat A →̇ nat A
add = ƛ ƛ ƛ ƛ # 3 · # 1 · (# 2 · # 1 · # 0)

id : ∅ ⊢ A →̇ A
id = ƛ # 0

id' : ∅ , A ⊢ A →̇ A
id' = ƛ # 1

fst : ∅ ⊢ A →̇ B →̇ A
fst = ƛ ƛ # 1

bool : Type → Type
bool A = A →̇ A →̇ A

if : ∅ ⊢ bool A →̇ A →̇ A →̇ A
if = ƛ ƛ ƛ # 2 · # 1 · # 0

succ : ∅ ⊢ nat A →̇ nat A
succ = ƛ ƛ ƛ # 1 · (# 2 · # 1 · # 0)

Rename : Context → Context → Set
Rename Γ Δ = ∀ {A} → Γ ∋ A → Δ ∋ A

Subst : Context → Context → Set
Subst Γ Δ = ∀ {A} → Γ ∋ A → Δ ⊢ A

rename : Rename Γ Δ
  → (Γ ⊢ A)
  → (Δ ⊢ A)
rename ρ (` x)   = ` ρ x
rename ρ (M · N) = rename ρ M · rename ρ N
rename ρ (ƛ M)   = ƛ rename (ext ρ) M

exts : Subst Γ Δ → Subst (Γ , A) (Δ , A)
exts σ Z     = ` Z
exts σ (S p) = rename S_ (σ p)

_⟪_⟫
  : Γ ⊢ A 
  → Subst Γ Δ
  → Δ ⊢ A
(` x)   ⟪ σ ⟫ = σ x
(M · N) ⟪ σ ⟫ = M ⟪ σ ⟫ · N ⟪ σ ⟫
(ƛ M)   ⟪ σ ⟫ = ƛ M ⟪ exts σ ⟫

subst-zero : {B : Type}
  → Γ ⊢ B
  → Subst (Γ , B) Γ
subst-zero N Z     =  N
subst-zero _ (S x) =  ` x

_[_] : Γ , B ⊢ A
     → Γ ⊢ B
       ---------
     → Γ ⊢ A
_[_] N M =  N ⟪ subst-zero M ⟫

infix 3 _-→_
data _-→_ {Γ} : (M N : Γ ⊢ A) → Set where
  β-ƛ·
    : (ƛ M) · N -→ M [ N ]

  ξ-ƛ
    :   M -→ M′
    → ƛ M -→ ƛ M′    

  ξ-·ₗ
    :     L -→ L′
      ---------------
    → L · M -→ L′ · M
  ξ-·ᵣ
    :     M -→ M′
      ---------------
    → L · M -→ L · M′

data _-↠_ {Γ A} : (M N : Γ ⊢ A) → Set where
  _∎ : (M : Γ ⊢ A)
    → M -↠ M       -- empty list
    
  _-→⟨_⟩_
    : ∀ L          -- this can usually be inferred by the following reduction 
    → L -→ M       -- the head of a list 
    → M -↠ N       -- the tail
      -------
    → L -↠ N

infix  2 _-↠_ 
infixr 2 _-→⟨_⟩_
infix 3 _∎

_ : (ƛ (ƛ # 0) · # 1) · # 0 -↠ (ƛ # 1) · # 0
_ = (ƛ (ƛ # 0) · # 1) · # 0
  -→⟨ ξ-·ₗ (ξ-ƛ β-ƛ·) ⟩
     (ƛ # 0 [ # 1 ]) · # 0
     ∎ 

_-↠⟨_⟩_ : ∀ L
  → L -↠ M → M -↠ N
  -----------------
  → L -↠ N
L -↠⟨ M ∎ ⟩  M-↠N               = M-↠N
L -↠⟨ L -→⟨ L→M′ ⟩ M′-↠M ⟩ M-↠N = L -→⟨ L→M′ ⟩ (_ -↠⟨ M′-↠M ⟩ M-↠N)

infixr 2 _-↠⟨_⟩_

ƛ-↠ : M -↠ M′
      -----------
    → ƛ M -↠ ƛ M′
ƛ-↠ (M ∎)               = ƛ M ∎
ƛ-↠ (M -→⟨ M→N ⟩ N-↠M′) = ƛ M -→⟨ ξ-ƛ M→N ⟩ ƛ-↠ N-↠M′

·ᵣ-↠ : N -↠ N′
  → M · N -↠ M · N′
·ᵣ-↠ {M = M} (N ∎)               = M · N ∎
·ᵣ-↠ {M = M} (N -→⟨ N→M ⟩ M-↠N′) = M · N -→⟨ ξ-·ᵣ N→M ⟩ (·ᵣ-↠ M-↠N′)

·ₗ-↠ : M -↠ M′
  → M · N -↠ M′ · N
·ₗ-↠ {M = M} {N = N} (M ∎)             = M · N ∎
·ₗ-↠ {M = M} {N = N} (M -→⟨ M→M₁ ⟩ M₁-↠M′) =
  M · N -→⟨ ξ-·ₗ M→M₁ ⟩ ·ₗ-↠ M₁-↠M′

·-↠ : M -↠ M′
    → N -↠ N′
    → M · N -↠ M′ · N′
·-↠ {M = M} {M′ = M′} {N = N} {N′ = N′} M-↠M′ N-↠N′ =
  M · N
  -↠⟨ ·ₗ-↠ M-↠M′ ⟩
   M′ · N
  -↠⟨ ·ᵣ-↠ N-↠N′ ⟩
   M′ · N′
   ∎

data _=β_ {Γ : Context} : Γ ⊢ A → Γ ⊢ A → Set where
  =β-beta
    : M -→ N → M =β N

  =β-refl
    : M =β M

  =β-sym
    : N =β M → M =β N

  =β-trans
    : L =β M → M =β N
    → L =β N

HW2 : M -↠ N → (∀ {N} → (M -→ N) → ⊥) → M ≡ N
HW2 (M ∎) M↛           = refl
HW2 (M -→⟨ M→N ⟩ _) M↛ = ⊥-elim (M↛ M→N)

data Neutral : Γ ⊢ A → Set 
data Normal  : Γ ⊢ A → Set 

data Neutral where
  `_  : (x : Γ ∋ A)
    → Neutral (` x)
  _·_ : Neutral L
    → Normal M
    → Neutral (L · M)

data Normal where
  ᵒ_  : Neutral M → Normal M
  ƛ_  : Normal M  → Normal (ƛ M)

normal-soundness  : Normal M  → ¬ (M -→ N)
neutral-soundness : Neutral M → ¬ (M -→ M′)

normal-soundness (ᵒ M↓) M→N       = neutral-soundness M↓ M→N
normal-soundness (ƛ M↓) (ξ-ƛ M→N) = normal-soundness M↓ M→N
neutral-soundness (` x) ()
neutral-soundness (L↓ · M↓) (ξ-·ₗ L→L′) = neutral-soundness L↓ L→L′
neutral-soundness (L↓ · M↓) (ξ-·ᵣ M→M′) = normal-soundness M↓ M→M′

normal-completeness
  : (M : Γ ⊢ A) → (∀ N → ¬ (M -→ N))
  → Normal M 
normal-completeness (` x) M↛ = ᵒ ` x
normal-completeness (ƛ M) ƛM↛ with normal-completeness M M↛
  where M↛ : ∀ N → ¬ (M -→ N)
        M↛ N M→N = ƛM↛ (ƛ N) (ξ-ƛ M→N)
... | M↓ = ƛ M↓
normal-completeness (M · N) MN↛ with normal-completeness M M↛ | normal-completeness N N↛
  where M↛ : ∀ M′ → ¬ (M -→ M′)
        M↛ M′ M↛ = MN↛ (M′ · N) (ξ-·ₗ M↛)
        N↛ : ∀ N′ → ¬ (N -→ N′)
        N↛ N′ N↛ = MN↛ (M · N′) (ξ-·ᵣ N↛)
... | ᵒ M↓ | N↓ = ᵒ (M↓ · N↓)
... | ƛ M↓ | N↓ = ⊥-elim (MN↛ _ β-ƛ· )

data Progress (M : Γ ⊢ A) : Set where
  step
    : M -→ N
      ----------
    → Progress M

  done : Normal M
    → Progress M

progress : (M : Γ ⊢ A)
  → Progress M
progress (` x) = done (ᵒ ` x)
progress (ƛ M) with progress M
... | step r  = step (ξ-ƛ r)
... | done M↓ = done (ƛ M↓)
progress (M · N) with progress M | progress N
... | step r  | _      = step (ξ-·ₗ r)
... | done x  | step r = step (ξ-·ᵣ r)
... | done (ᵒ M↓) | done N↓ = done (ᵒ (M↓ · N↓))
... | done (ƛ M↓) | done N↓ = step β-ƛ·

data Progress′ (M : Γ ⊢ A) : Set where
  step
    : (r : M -→ N)
      ----------
    → Progress′ M

  done : (M↓ : (N : Γ ⊢ A) → M -→ N → ⊥)
    → Progress′ M

--progress′ : (M : Γ ⊢ A) → Progress′ M
--progress′ M = {!!}