Skip to content

Instantly share code, notes, and snippets.

@cheery

cheery/newtry.agda

Created January 25, 2023 16:33
Show Gist options
  • Save cheery/0971168e13128c196071128cc3be032d to your computer and use it in GitHub Desktop.
Save cheery/0971168e13128c196071128cc3be032d to your computer and use it in GitHub Desktop.
Download ZIP
Preservation proof doesn't go through.
Raw
newtry.agda
module newtry where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (True; toWitness)
open import Data.Fin
open import Data.Nat
open import Data.Product
open import Data.Empty
open import Data.Unit
data Term (n : ℕ) : Set where
var : Fin n → Term n
app : Term n → Term n → Term n
lam : Term (suc n) → Term n
pi : Term n → Term (suc n) → Term n
u : ℕ → Term n
data Context : ℕ → Set where
∅ : Context zero
_,_ : ∀{n} → Context n → Term n → Context (suc n)
extend' : ∀{n} → Fin (suc n) → Fin n → Fin (suc n)
extend' 0F x = suc x
extend' (suc n) 0F = 0F
extend' (suc n) (suc x) = suc (extend' n x)
extend : ∀{n} → Fin (suc n) → Term n → Term (suc n)
extend n (var x) = var (extend' n x)
extend n (app t v) = app (extend n t) (extend n v)
extend n (lam t) = lam (extend (suc n) t)
extend n (pi t v) = pi (extend n t) (extend (suc n) v)
extend n (u i) = u i
lookup : ∀{n} → Context n → Fin n → Term n
lookup (ctx , x) 0F = extend 0F x
lookup (ctx , x) (suc n) = extend 0F (lookup ctx n)
exts : ∀ {n} (p : Fin (suc n) → Term n) → Fin (suc (suc n)) → Term (suc n)
exts p 0F = var 0F
exts p (suc x) = extend 0F (p x)
subst : ∀{n} → (Fin (suc n) → Term n) → Term (suc n) → Term n
subst p (var x) = p x
subst p (app t v) = app (subst p t) (subst p v)
subst p (lam t) = lam (subst (exts p) t)
subst p (pi t v) = pi (subst p t) (subst (exts p) v)
subst p (u n) = u n
infix 10 _⇒_
infix 10 _⇒*_
_[_] : ∀{n} → Term (suc n) → Term n → Term n
_[_] {n} f x = subst p f
where p : Fin (suc n) → Term n
p 0F = x
p (suc i) = var i
data _⇒_ {n} : Term n → Term n → Set where
betaLam : ∀ {p x y}
→ p [ x ] ≡ y
→ app (lam p) x ⇒ y
etaLam : ∀ {p q}
→ p ⇒ q
→ lam p ⇒ lam q
eta1 : ∀ {p q x}
→ p ⇒ q
→ app p x ⇒ app q x
eta2 : ∀ {p q x}
→ p ⇒ q
→ app x p ⇒ app x q
pi1 : ∀ {p q x}
→ p ⇒ q
→ pi p x ⇒ pi q x
pi2 : ∀ {p q x}
→ p ⇒ q
→ pi x p ⇒ pi x q
data _⇒*_ {n} : Term n → Term n → Set where
refl : ∀ {a} → a ⇒* a
step : ∀ {a b c} → a ⇒ b → b ⇒* c → a ⇒* c
data Normal {n} : Term n → Set
data Neutral {n} : Term n → Set
data Neutral where
var : ∀{n} → Neutral (var n)
app : ∀{x y} → Neutral x → Normal y → Neutral (app x y)
data Normal where
neutral : ∀{x} → Neutral x → Normal x
lam : ∀{x} → Normal x → Normal (lam x)
pi : ∀{x y} → Normal x → Normal y → Normal (pi x y)
u : ∀{n} → Normal (u n)
mutual
neutralNotReduce : ∀{i} {n m : Term i} → (Neutral n) → n ⇒ m → ⊥
neutralNotReduce (app x y) (eta1 xm) = neutralNotReduce x xm
neutralNotReduce (app x y) (eta2 ym) = normalNotReduce y ym
normalNotReduce : ∀{i} {n m : Term i} → (Normal n) → n ⇒ m → ⊥
normalNotReduce (neutral x) nm = neutralNotReduce x nm
normalNotReduce (lam n) (etaLam nm) = normalNotReduce n nm
normalNotReduce (pi x y) (pi1 xm) = normalNotReduce x xm
normalNotReduce (pi x y) (pi2 ym) = normalNotReduce y ym
data _⊢_∶_ {n} : Context n → Term n → Term n → Set where
var : ∀ {G n t}
→ G ⊢ var n ∶ t
app : ∀ {G f a g x y}
→ G ⊢ f ∶ pi a g
→ G ⊢ x ∶ a
→ (app (lam g) x) ⇒* y × Normal y
→ G ⊢ app f x ∶ y
lam : ∀ {G A f B}
→ (G , A) ⊢ f ∶ B
→ G ⊢ lam f ∶ pi A B
pi : ∀ {G x n g}
→ G ⊢ x ∶ u n
→ (G , x) ⊢ g ∶ u n
→ G ⊢ pi x g ∶ u n
u : ∀ {G n}
→ G ⊢ u n ∶ u (suc n)
↑ : ∀ {G x n}
→ G ⊢ x ∶ u n
→ G ⊢ x ∶ u (suc n)
data Progress {n} (t : Term n) : Set where
step : ∀ {v} → t ⇒ v → Progress t
done : Normal t → Progress t
progress : ∀{n ctx} {term type : Term n} → ctx ⊢ term ∶ type → Progress term
progress var = done (neutral var)
progress (app t v conv) with progress t
progress (app t v conv) | step x = step (eta1 x)
progress (app t v conv) | done x with progress v
progress (app t v conv) | done x | step y = step (eta2 y)
progress (app t v conv) | done (neutral x) | done y = done (neutral (app x y))
progress (app t v conv) | done (lam x) | done y = step (betaLam refl)
progress (lam t) with progress t
progress (lam t) | step x = step (etaLam x)
progress (lam t) | done x = done (lam x)
progress (pi t v) with progress t
progress (pi t v) | step x = step (pi1 x)
progress (pi t v) | done x with progress v
progress (pi t v) | done x | step y = step (pi2 y)
progress (pi t v) | done x | done y = done (pi x y)
progress u = done u
progress (↑ t) = progress t
transform : ∀ {n} {g : Term (suc n)} {x q type : Term n}
→ app (lam g) x ⇒* type
→ x ⇒ q
→ app (lam g) q ⇒* type
transform x xq = {!!}
transform' : ∀ {n i} {ctx : Context n} {x q : Term n} {g : Term (suc n)}
→ (ctx , x) ⊢ g ∶ u i
→ (x ⇒ q)
→ (ctx , q) ⊢ g ∶ u i
transform' var trans = {!!}
transform' (app t v x) trans = {!!}
transform' (pi t v) trans = pi (transform' t trans) {!transform' v trans!}
transform' u trans = u
transform' (↑ term) trans = ↑ (transform' term trans)
preserveSubst : ∀{n} {ctx : Context n} {x a type : Term n} {f g : Term (suc n)}
→ ctx ⊢ x ∶ a
→ (ctx , a) ⊢ f ∶ g
→ app (lam g) x ⇒* type × Normal type
→ ctx ⊢ f [ x ] ∶ type
preserveSubst x f (gxn , norm) = {!!}
preserve : ∀{n ctx} {t v type : Term n} → ctx ⊢ t ∶ type → t ⇒ v → ctx ⊢ v ∶ type
preserve (app (lam t) v conv) (betaLam refl) = preserveSubst v t conv
preserve (app t v conv) (eta1 s) = app (preserve t s) v conv
preserve (app t v (TN , nT)) (eta2 s) = app t (preserve v s) (transform TN s , nT)
preserve (lam t) (etaLam s) = lam (preserve t s)
preserve (pi t v) (pi1 s) = pi (preserve t s) (transform' v s)
preserve (pi t v) (pi2 s) = pi t (preserve v s)
preserve (↑ term) s = ↑ (preserve term s)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment