Skip to content

Instantly share code, notes, and snippets.

@jozefg

jozefg/mltt.agda

Created April 14, 2018 18:39
Show Gist options
  • Save jozefg/40331728c1c084907494969b958d0f5e to your computer and use it in GitHub Desktop.
Save jozefg/40331728c1c084907494969b958d0f5e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
mltt.agda
module mltt where
open import Data.Nat
import Data.Fin as F
open import Data.Sum
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
data Tm : ℕ → Set where
var : ∀ {n} → F.Fin n → Tm n
app : ∀ {n} → Tm n → Tm n → Tm n
lam : ∀ {n} → Tm (suc n) → Tm n
Π : ∀ {n} → Tm n → Tm (suc n) → Tm n
sig : ∀ {n} → Tm n → Tm (suc n) → Tm n
pair : ∀ {n} → Tm n → Tm n → Tm n
split : ∀ {n} → Tm n → Tm (suc (suc n)) → Tm n
U : ∀ {n} → Tm n
weakenTm : {n : ℕ}(m : ℕ) → Tm n → Tm (n + m)
weakenTm m (var x) = var (F.inject+ m x)
weakenTm m (app tm tm₁) = app (weakenTm m tm) (weakenTm m tm₁)
weakenTm m (lam tm) = lam (weakenTm m tm)
weakenTm m (Π l r) = Π (weakenTm m l) (weakenTm m r)
weakenTm m (sig l r) = sig (weakenTm m l) (weakenTm m r)
weakenTm m (pair tm tm₁) = pair (weakenTm m tm) (weakenTm m tm₁)
weakenTm m (split l r) = split (weakenTm m l) (weakenTm m r)
weakenTm m U = U
bumpTm : {n : ℕ} → Tm n → Tm (suc n)
bumpTm = go zero where
go : {n : ℕ}(lower : ℕ) → Tm n → Tm (suc n)
go lower (var x) with lower ≤? F.toℕ x
... | yes _ = var (F.suc x)
... | no _ = var (F.inject₁ x)
go lower (app tm tm₁) = app (go lower tm) (go lower tm₁)
go lower (lam e) = lam (go (suc lower) e)
go lower (Π l r) = Π (go lower l) (go (suc lower) r)
go lower (sig l r) = sig (go lower l) (go (suc lower) r)
go lower (pair tm tm₁) = pair (go lower tm) (go lower tm₁)
go lower (split l r) = split (go lower l) (go (suc (suc lower)) r)
go lower U = U
pushDown : {C : Set}{n : ℕ} → C → F.Fin (suc n) → C ⊎ F.Fin n
pushDown c F.zero = inj₁ c
pushDown c (F.suc F.zero) = inj₂ F.zero
pushDown c (F.suc (F.suc m)) with pushDown c (F.suc m)
... | inj₁ x = inj₁ x
... | inj₂ y = inj₂ (F.suc y)
substTm : {m : ℕ} → Tm m → Tm (suc m) → Tm m
substTm = go where
go : {m : ℕ} → Tm m → Tm (suc m) → Tm m
go new (var x) with pushDown new x
... | inj₁ c = c
... | inj₂ x' = var x'
go new (app e e₁) = app (go new e) (go new e₁)
go new (lam e) = lam (go (bumpTm new) e)
go new (Π e e₁) = Π (go new e) (go (bumpTm new) e₁)
go new (sig e e₁) = sig (go new e) (go (bumpTm new) e₁)
go new (pair e e₁) = pair (go new e) (go new e₁)
go new (split e e₁) = split (go new e) (go (bumpTm (bumpTm new)) e₁)
go new U = U
T : Set
T = Tm 0
data Canon : Set where
lam : Tm 1 → Canon
Π : T → Tm 1 → Canon
sig : T → Tm 1 → Canon
pair : T → T → Canon
U : Canon
canon2tm : Canon → T
canon2tm (lam x) = lam x
canon2tm (Π x x₁) = Π x x₁
canon2tm (sig x x₁) = sig x x₁
canon2tm (pair x x₁) = pair x x₁
canon2tm U = U
data Eval : T → Canon → Set where
lam : ∀ {e} → Eval (lam e) (lam e)
Π : ∀ {e e₁} → Eval (Π e e₁) (Π e e₁)
sig : ∀ {e e₁} → Eval (sig e e₁) (sig e e₁)
pair : ∀ {e e₁} → Eval (pair e e₁) (pair e e₁)
split : ∀ {e e₁ l r v}
→ Eval e (pair l r)
→ Eval (substTm r (substTm (weakenTm 1 l) e₁)) v
→ Eval (split e e₁) v
app : ∀ {e e₁ b v}
→ Eval e (lam b)
→ Eval (substTm e₁ b) v
→ Eval (app e e₁) v
U : Eval U U
-- | This lemma is interesting if we had not fixed an order of evaluation
-- on things like split and app. We did so it's just recurse and rewrite.
deterministic : ∀{c c₁} → (e : T) → Eval e c → Eval e c₁ → c ≡ c₁
deterministic (var ()) ev ev₁
deterministic (app e e₁) (app ev ev₁) (app ev₂ ev₃) with deterministic e ev ev₂
... | refl with deterministic _ ev₁ ev₃
... | refl = refl
deterministic (lam e) lam lam = refl
deterministic U U U = refl
deterministic (Π e e₁) Π Π = refl
deterministic (sig e e₁) sig sig = refl
deterministic (pair e e₁) pair pair = refl
deterministic (split e e₁) (split ev ev₁) (split ev₂ ev₃) with deterministic e ev ev₂
... | refl with deterministic _ ev₁ ev₃
... | refl = refl
-- | (λx.x)(λx.x) ⇒ λx.x
test : Eval (app (lam (var F.zero)) (lam (var F.zero))) (lam (var F.zero))
test = app lam lam
data Context : ℕ → Set where
nil : Context 0
cons : ∀ {n} → Context n → Tm n → Context (suc n)
-- | Given a canonical value we can push it through a context
-- to remove one entry of the context. This is tricky due to
-- the dependency between everything.
substContext : ∀ {n} → Canon → Context (suc n) → Context n
substContext c (cons nil x) = nil
substContext {suc n} c (cons (cons cxt x) x₁) =
cons (substContext c (cons cxt x)) x₁'
where x₁' = substTm (weakenTm n (canon2tm c)) x₁
data type : Canon → Set
data _∷_ : Canon → Canon → Set
data _∈_[_] : {n : ℕ} → Tm n → Tm n → Context n → Set
data type where
is-type : ∀ {c} → c ∷ U → type c
data _∷_ where
pair : ∀ {e e₁ t t₁}
→ e ∈ t [ nil ]
→ e₁ ∈ substTm e t₁ [ nil ]
→ pair e e₁ ∷ sig t t₁
lam : ∀ {b t t₁}
→ b ∈ t₁ [ cons nil t ]
→ lam b ∷ Π t t₁
sig : ∀ {t t₁}
→ t ∈ U [ nil ]
→ t₁ ∈ U [ cons nil t ]
→ sig t t₁ ∷ U
Π : ∀ {t t₁}
→ t ∈ U [ nil ]
→ t₁ ∈ U [ cons nil t ]
→ Π t t₁ ∷ U
splitSubst : ∀ {n} → Tm (suc n) → Tm (suc (suc n))
splitSubst = go 0 where
go : ∀ {n} → ℕ → Tm (suc n) → Tm (suc (suc n))
go target (var x) with F.toℕ x ≤? target | target ≤? F.toℕ x
... | yes p | yes p₁ = pair (var F.zero) (var (F.suc F.zero))
... | yes p | no ¬p = {!!}
... | no ¬p | yes p = {!!}
... | no ¬p | no ¬p₁ = {!!}
go target (app e e₁) = {!!}
go target (lam e) = {!!}
go target (Π e e₁) = {!!}
go target (sig e e₁) = {!!}
go target (pair e e₁) = {!!}
go target (split e e₁) = {!!}
go target U = {!!}
data _∈_[_] where
pair : {n : ℕ}{cxt : Context n} → ∀ {e e₁ t t₁}
→ e ∈ t [ cxt ]
→ e₁ ∈ substTm e t₁ [ cxt ]
→ pair e e₁ ∈ sig t t₁ [ cxt ]
lam : {n : ℕ}{cxt : Context n} → ∀ {b t t₁}
→ b ∈ t₁ [ cons cxt t ]
→ lam b ∈ Π t t₁ [ cxt ]
sig : {n : ℕ}{cxt : Context n} → ∀ {t t₁}
→ t ∈ U [ cxt ]
→ t₁ ∈ U [ cons cxt t ]
→ sig t t₁ ∈ U [ cxt ]
Π : {n : ℕ}{cxt : Context n} → ∀ {t t₁}
→ t ∈ U [ cxt ]
→ t₁ ∈ U [ cons cxt t ]
→ Π t t₁ ∈ U [ cxt ]
split : {n : ℕ}{cxt : Context n} → ∀ {e e₁ t t₁ t₂}
→ e ∈ sig t t₁ [ cxt ]
→ e₁ ∈ substTm t₂ (weakenTm n (pair (var (F.suc F.zero)) (weakenTm 2 (var F.zero)))) [ cons (cons cxt t) t₁ ]
→ split e e₁ ∈ {!!} [ cxt ]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment