Agda-2.3.2.2: examples/TT.agda
{-# OPTIONS --allow-unsolved-metas --no-termination-check #-}
module TT where
module Prelude where
-- Props ------------------------------------------------------------------
data True : Set where
tt : True
data False : Set where
postulate
falseE : (A : Set) -> False -> A
infix 3 _/\_
data _/\_ (P Q : Set) : Set where
andI : P -> Q -> P /\ Q
-- Zero and One -----------------------------------------------------------
data Zero : Set where
data One : Set where
unit : One
-- Natural numbers --------------------------------------------------------
data Nat : Set where
zero : Nat
suc : Nat -> Nat
_+_ : Nat -> Nat -> Nat
zero + m = m
suc n + m = suc (n + m)
module NatEq where
infix 5 _==_
_==_ : Nat -> Nat -> Set
zero == zero = True
suc n == suc m = n == m
_ == _ = False
rewriteEq : (C : Nat -> Set){m n : Nat} -> m == n -> C n -> C m
rewriteEq C {zero} {zero} _ x = x
rewriteEq C {suc _} {suc _} eq x = rewriteEq (\z -> C (suc z)) eq x
rewriteEq C {zero} {suc _} () _
rewriteEq C {suc _} {zero} () _
module Chain {A : Set}(_==_ : A -> A -> Set)
(_trans_ : {x y z : A} -> x == y -> y == z -> x == z)
where
infixl 4 _=-=_
infixl 4 _===_
infixr 8 _since_
_=-=_ : (x : A){y : A} -> x == y -> x == y
x =-= xy = xy
_===_ : {x y z : A} -> x == y -> y == z -> x == z
xy === yz = xy trans yz
_since_ : {x : A}(y : A) -> x == y -> x == y
y since xy = xy
module Fin where
open Prelude
-- Finite sets ------------------------------------------------------------
data Suc (A : Set) : Set where
fzero' : Suc A
fsuc' : A -> Suc A
mutual
data Fin (n : Nat) : Set where
finI : Fin' n -> Fin n
Fin' : Nat -> Set
Fin' zero = Zero
Fin' (suc n) = Suc (Fin n)
fzero : {n : Nat} -> Fin (suc n)
fzero = finI fzero'
fsuc : {n : Nat} -> Fin n -> Fin (suc n)
fsuc i = finI (fsuc' i)
finE : {n : Nat} -> Fin n -> Fin' n
finE (finI i) = i
module FinEq where
infix 5 _==_
_==_ : {n : Nat} -> Fin n -> Fin n -> Set
_==_ {suc _} (finI fzero' ) (finI fzero' ) = True
_==_ {suc _} (finI (fsuc' i)) (finI (fsuc' j)) = i == j
_==_ _ _ = False
rewriteEq : {n : Nat}(C : Fin n -> Set){i j : Fin n} -> i == j -> C j -> C i
rewriteEq {suc _} C {finI fzero' } {finI fzero' } eq x = x
rewriteEq {suc _} C {finI (fsuc' i)} {finI (fsuc' j)} eq x = rewriteEq (\z -> C (fsuc z)) eq x
rewriteEq {suc _} C {finI (fsuc' _)} {finI fzero' } () _
rewriteEq {suc _} C {finI fzero' } {finI (fsuc' _)} () _
rewriteEq {zero} C {finI ()} {_} _ _
module Vec where
open Prelude
open Fin
infixr 15 _::_
-- Vectors ----------------------------------------------------------------
data Nil : Set where
nil' : Nil
data Cons (A As : Set) : Set where
cons' : A -> As -> Cons A As
mutual
data Vec (A : Set)(n : Nat) : Set where
vecI : Vec' A n -> Vec A n
Vec' : Set -> Nat -> Set
Vec' A zero = Nil
Vec' A (suc n) = Cons A (Vec A n)
nil : {A : Set} -> Vec A zero
nil = vecI nil'
_::_ : {A : Set}{n : Nat} -> A -> Vec A n -> Vec A (suc n)
x :: xs = vecI (cons' x xs)
vecE : {A : Set}{n : Nat} -> Vec A n -> Vec' A n
vecE (vecI xs) = xs
vec : {A : Set}(n : Nat) -> A -> Vec A n
vec zero _ = nil
vec (suc n) x = x :: vec n x
map : {n : Nat}{A B : Set} -> (A -> B) -> Vec A n -> Vec B n
map {zero} f (vecI nil') = nil
map {suc n} f (vecI (cons' x xs)) = f x :: map f xs
_!_ : {n : Nat}{A : Set} -> Vec A n -> Fin n -> A
_!_ {zero } _ (finI ())
_!_ {suc n} (vecI (cons' x _ )) (finI fzero') = x
_!_ {suc n} (vecI (cons' _ xs)) (finI (fsuc' i)) = xs ! i
tabulate : {n : Nat}{A : Set} -> (Fin n -> A) -> Vec A n
tabulate {zero} f = nil
tabulate {suc n} f = f fzero :: tabulate (\x -> f (fsuc x))
module Untyped where
open Prelude
open Fin
open Vec
Name = Nat
data Expr (n : Nat) : Set where
eVar : Fin n -> Expr n
eApp : Expr n -> Expr n -> Expr n
eLam : Expr (suc n) -> Expr n
eSet : Expr n
eEl : Expr n
ePi : Expr n
eCon : Name -> Expr n
module ExprEq where
infix 5 _==_
_==_ : {n : Nat} -> Expr n -> Expr n -> Set
eVar i == eVar j = FinEq._==_ i j
eApp e1 e2 == eApp e3 e4 = e1 == e3 /\ e2 == e4
eLam e1 == eLam e2 = e1 == e2
eSet == eSet = True
eEl == eEl = True
ePi == ePi = True
eCon f == eCon g = NatEq._==_ f g
_ == _ = False
rewriteEq : {n : Nat}(C : Expr n -> Set){r s : Expr n} -> r == s -> C s -> C r
rewriteEq C {eVar i } {eVar j } eq x = FinEq.rewriteEq (\z -> C (eVar z)) eq x
rewriteEq C {eLam e1 } {eLam e2 } eq x = rewriteEq (\z -> C (eLam z)) eq x
rewriteEq C {eSet } {eSet } eq x = x
rewriteEq C {eEl } {eEl } eq x = x
rewriteEq C {ePi } {ePi } eq x = x
rewriteEq C {eCon f } {eCon g } eq x = NatEq.rewriteEq (\z -> C (eCon z)) eq x
rewriteEq C {eApp e1 e2} {eApp e3 e4} (andI eq13 eq24) x =
rewriteEq (\z -> C (eApp z e2)) eq13 (
rewriteEq (\z -> C (eApp e3 z)) eq24 x
)
rewriteEq C {eVar _} {eLam _ } () _
rewriteEq C {eVar _} {eSet } () _
rewriteEq C {eVar _} {eEl } () _
rewriteEq C {eVar _} {eCon _ } () _
rewriteEq C {eVar _} {ePi } () _
rewriteEq C {eVar _} {eApp _ _} () _
rewriteEq C {eLam _} {eVar _ } () _
rewriteEq C {eLam _} {eSet } () _
rewriteEq C {eLam _} {eEl } () _
rewriteEq C {eLam _} {eCon _ } () _
rewriteEq C {eLam _} {ePi } () _
rewriteEq C {eLam _} {eApp _ _} () _
rewriteEq C {eSet } {eLam _ } () _
rewriteEq C {eSet } {eVar _ } () _
rewriteEq C {eSet } {eEl } () _
rewriteEq C {eSet } {eCon _ } () _
rewriteEq C {eSet } {ePi } () _
rewriteEq C {eSet } {eApp _ _} () _
rewriteEq C {eEl } {eLam _ } () _
rewriteEq C {eEl } {eSet } () _
rewriteEq C {eEl } {eVar _ } () _
rewriteEq C {eEl } {eCon _ } () _
rewriteEq C {eEl } {ePi } () _
rewriteEq C {eEl } {eApp _ _} () _
rewriteEq C {eCon _} {eLam _ } () _
rewriteEq C {eCon _} {eSet } () _
rewriteEq C {eCon _} {eEl } () _
rewriteEq C {eCon _} {eVar _ } () _
rewriteEq C {eCon _} {ePi } () _
rewriteEq C {eCon _} {eApp _ _} () _
rewriteEq C {ePi } {eLam _ } () _
rewriteEq C {ePi } {eSet } () _
rewriteEq C {ePi } {eEl } () _
rewriteEq C {ePi } {eCon _ } () _
rewriteEq C {ePi } {eVar _ } () _
rewriteEq C {ePi } {eApp _ _} () _
rewriteEq C {eApp _ _} {eLam _ } () _
rewriteEq C {eApp _ _} {eSet } () _
rewriteEq C {eApp _ _} {eEl } () _
rewriteEq C {eApp _ _} {eCon _ } () _
rewriteEq C {eApp _ _} {ePi } () _
rewriteEq C {eApp _ _} {eVar _ } () _
module Typed where
open Prelude
open Fin
open Vec
infixl 15 _&_
infix 13 _!!_
infix 5 _==_
-- Contexts ---------------------------------------------------------------
data CSuc (n : Nat) : Set
Context' : Nat -> Set
Context' zero = Nil
Context' (suc n) = CSuc n
data Context (n : Nat) : Set
data Type {n : Nat}(Γ : Context n) : Set
data CSuc n where
ext : (Γ : Context n) -> Type Γ -> Context' (suc n)
data Context n where
ctxI : Context' n -> Context n
-- Types ------------------------------------------------------------------
_&_ : {n : Nat}(Γ : Context n) -> Type Γ -> Context (suc n)
data Term {n : Nat}(Γ : Context n)(A : Type Γ) : Set
data Type {n} Γ where
SET : Type Γ
Pi : (A : Type Γ) -> Type (Γ & A) -> Type Γ
El : Term Γ SET -> Type Γ
Γ & A = ctxI (ext Γ A)
-- Variables --------------------------------------------------------------
data VarSuc {n : Nat}(Γ : Context n)(B : Type Γ)(A : Type (Γ & B)) : Set
Var' : {n : Nat}(Γ : Context n) -> Type Γ -> Set
Var' {zero} Γ A = Zero
Var' {suc n} (ctxI (ext Γ B)) A = VarSuc Γ B A
_==_ : {n : Nat}{Γ : Context n} -> Type Γ -> Type Γ -> Set
data Ren {n m : Nat}(Γ : Context n)(Δ : Context m) : Set
rename : {n m : Nat}{Γ : Context n}{Δ : Context m} -> Ren Γ Δ -> Type Γ -> Type Δ
upR : {n : Nat}{Γ : Context n}{A : Type Γ} -> Ren Γ (Γ & A)
data Var {n : Nat}(Γ : Context n)(A : Type Γ) : Set
data VarSuc {n} Γ B A where
vzero_ : A == rename upR B -> Var' (Γ & B) A
vsuc_ : (C : Type Γ) -> A == rename upR C -> Var Γ C -> Var' (Γ & B) A
data Var {n} Γ A where
varI : Var' Γ A -> Var Γ A
-- Terms ------------------------------------------------------------------
data Sub {n m : Nat}(Γ : Context n)(Δ : Context m) : Set
subst : {n m : Nat}{Γ : Context n}{Δ : Context m} -> Sub Γ Δ -> Type Γ -> Type Δ
down : {n : Nat}{Γ : Context n}{A : Type Γ} -> Term Γ A -> Sub (Γ & A) Γ
data Term {n} Γ A where
var : (x : Var Γ A) -> Term Γ A
app : {B : Type Γ}{C : Type (Γ & B)} -> Term Γ (Pi B C) -> (t : Term Γ B) ->
A == subst (down t) C -> Term Γ A
lam : {B : Type Γ}{C : Type (Γ & B)} -> Term (Γ & B) C -> A == Pi B C -> Term Γ A
-- Context manipulation ---------------------------------------------------
∅ : Context zero
∅ = ctxI nil'
_!!_ : {n : Nat}(Γ : Context n) -> Fin n -> Type Γ
_!!_ {zero} _ (finI ())
_!!_ {suc _} (ctxI (ext Γ A)) (finI fzero') = rename upR A
_!!_ {suc _} (ctxI (ext Γ A)) (finI (fsuc' i)) = rename upR (Γ !! i)
-- Renamings --------------------------------------------------------------
data ConsRen {n m : Nat}(Γ : Context n)(A : Type Γ)(Δ : Context m) : Set
Ren' : {n m : Nat} -> Context n -> Context m -> Set
Ren' {zero} {m} (ctxI nil') Δ = Nil
Ren' {suc n} {m} (ctxI (ext Γ A)) Δ = ConsRen Γ A Δ
data ConsRen {n m} Γ A Δ where
extRen' : (ρ : Ren Γ Δ) -> Var Δ (rename ρ A) -> Ren' (Γ & A) Δ
data Ren {n m} Γ Δ where
renI : Ren' Γ Δ -> Ren Γ Δ
-- Performing renamings ---------------------------------------------------
rename' : {n m : Nat}{Γ : Context n}{Δ : Context m} -> Ren Γ Δ -> Type Γ -> Type Δ
rename ρ SET = SET
rename ρ A = rename' ρ A
liftR : {n m : Nat}{Γ : Context n}{A : Type Γ}{Δ : Context m} ->
(ρ : Ren Γ Δ) -> Ren (Γ & A) (Δ & rename ρ A)
renameTerm : {n m : Nat}{Γ : Context n}{Δ : Context m}{A : Type Γ}
(ρ : Ren Γ Δ) -> Term Γ A -> Term Δ (rename ρ A)
rename' ρ SET = SET
rename' ρ (Pi A B) = Pi (rename ρ A) (rename (liftR ρ) B)
rename' ρ (El t) = El (renameTerm ρ t)
lookupR : {n m : Nat}{Γ : Context n}{A : Type Γ}{Δ : Context m}
(ρ : Ren Γ Δ)(x : Var Γ A) -> Var Δ (rename ρ A)
cong : {n m : Nat}{Γ : Context n}{Δ : Context m}(f : Type Γ -> Type Δ)
{A B : Type Γ} -> A == B -> f A == f B
_trans_ : {n : Nat}{Γ : Context n}{A B C : Type Γ} -> A == B -> B == C -> A == C
renameSubstCommute :
{n m : Nat}{Γ : Context n}{Δ : Context m}{A : Type Γ}{B : Type (Γ & A)}
{ρ : Ren Γ Δ}{t : Term Γ A} ->
rename ρ (subst (down t) B) == subst (down (renameTerm ρ t)) (rename (liftR ρ) B)
renameTerm ρ (var x) = var (lookupR ρ x)
renameTerm {_}{_}{_}{_}{A} ρ (app{_}{C} s t eq) =
app (renameTerm ρ s) (renameTerm ρ t)
(cong (rename ρ) eq trans renameSubstCommute)
renameTerm ρ (lam t eq) = lam (renameTerm (liftR ρ) t) (cong (rename ρ) eq)
lookupR {zero} _ (varI ())
lookupR {suc n} {_} {ctxI (ext Γ B)} {A} {Δ}
(renI (extRen' ρ z)) (varI (vzero_ eq)) = {!!}
lookupR {suc n} {_} {ctxI (ext Γ B)} {A} {Δ}
(renI (extRen' ρ z)) (varI (vsuc_ C eq x)) = {!!}
-- Building renamings -----------------------------------------------------
extRen : {n m : Nat}{Γ : Context n}{A : Type Γ}{Δ : Context m}
(ρ : Ren Γ Δ) -> Var Δ (rename ρ A) -> Ren (Γ & A) Δ
extRen ρ x = renI (extRen' ρ x)
_coR_ : {n m p : Nat}{Γ : Context n}{Δ : Context m}{Θ : Context p} -> Ren Δ Θ -> Ren Γ Δ -> Ren Γ Θ
liftR {_}{_}{_}{A} ρ = extRen (upR coR ρ) (varI {!!})
idR : {n : Nat} {Γ : Context n} -> Ren Γ Γ
idR = {!!}
_coR_ = {!!}
upR = {!!}
-- Substitutions ----------------------------------------------------------
data ConsSub {n m : Nat}(Γ : Context n)(A : Type Γ)(Δ : Context m) : Set
Sub' : {n m : Nat} -> Context n -> Context m -> Set
Sub' {zero} {m} (ctxI nil') Δ = Nil
Sub' {suc n} {m} (ctxI (ext Γ A)) Δ = ConsSub Γ A Δ
data ConsSub {n m} Γ A Δ where
extSub' : (σ : Sub Γ Δ) -> Term Δ (subst σ A) -> Sub' (Γ & A) Δ
data Sub {n m} Γ Δ where
subI : Sub' Γ Δ -> Sub Γ Δ
-- Performing substitution ------------------------------------------------
subst' : {n m : Nat}{Γ : Context n}{Δ : Context m} -> Sub Γ Δ -> Type Γ -> Type Δ
subst σ SET = SET
subst σ A = subst' σ A
liftS : {n m : Nat}{Γ : Context n}{A : Type Γ}{Δ : Context m} ->
(σ : Sub Γ Δ) -> Sub (Γ & A) (Δ & subst σ A)
substTerm : {n m : Nat}{Γ : Context n}{Δ : Context m}{A : Type Γ} ->
(σ : Sub Γ Δ) -> Term Γ A -> Term Δ (subst σ A)
subst' σ (Pi A B) = Pi (subst σ A) (subst (liftS σ) B)
subst' σ (El t) = El (substTerm σ t)
subst' σ SET = SET
substTerm σ (var x) = {!!}
substTerm σ (app s t eq) = {!!}
substTerm σ (lam t eq) = {!!}
-- Building substitutions -------------------------------------------------
liftS {_}{_}{_}{A} σ = {!!} -- extSub (upS ∘ σ) (var fzero (substCompose upS σ A))
-- Works with hidden args to substCompose when inlined in subst
-- but not here. Weird.
topS : {n : Nat}{Γ : Context n} -> Sub ∅ Γ
topS = subI nil'
extSub : {n m : Nat}{Γ : Context n}{A : Type Γ}{Δ : Context m}
(σ : Sub Γ Δ) -> Term Δ (subst σ A) -> Sub (Γ & A) Δ
extSub σ t = subI (extSub' σ t)
idS : {n : Nat}{Γ : Context n} -> Sub Γ Γ
idS {zero} {ctxI nil'} = topS
idS {suc _} {ctxI (ext Γ A)} = {!!} -- extSub upS (var fzero refl)
convert : {n : Nat}{Γ : Context n}{A B : Type Γ} -> A == B -> Term Γ B -> Term Γ A
_∘_ : {n m p : Nat}{Γ : Context n}{Δ : Context m}{Θ : Context p} -> Sub Δ Θ -> Sub Γ Δ -> Sub Γ Θ
substCompose : {n m p : Nat}{Γ : Context n}{Δ : Context m}{Θ : Context p}
(σ : Sub Δ Θ)(δ : Sub Γ Δ)(A : Type Γ) ->
subst (σ ∘ δ) A == subst σ (subst δ A)
_∘_ {zero} {_}{_} {ctxI nil'} _ _ = topS
_∘_ {suc _}{_}{_} {ctxI (ext Γ A)} σ (subI (extSub' δ t)) =
extSub (σ ∘ δ) (convert (substCompose σ δ A) (substTerm σ t))
upS : {n : Nat}{Γ : Context n}{A : Type Γ} -> Sub Γ (Γ & A)
upS = {!!}
substId : {n : Nat}{Γ : Context n}{A : Type Γ} -> subst idS A == A
down t = extSub idS (convert substId t)
-- Convertibility ---------------------------------------------------------
A == B = {!!}
refl : {n : Nat}{Γ : Context n}{A : Type Γ} -> A == A
refl = {!!}
cong f eq = {!!}
ab trans bc = {!!}
convert eq t = {!!}
-- Properties -------------------------------------------------------------
renameId : {n : Nat}{Γ : Context n}{A : Type Γ} -> rename idR A == A
renameId = {!!}
renameCompose : {n m p : Nat}{Γ : Context n}{Δ : Context m}{Θ : Context p}
(σ : Ren Δ Θ)(δ : Ren Γ Δ)(A : Type Γ) ->
rename (σ coR δ) A == rename σ (rename δ A)
renameCompose σ δ A = {!!}
substId = {!!}
substCompose σ δ A = {!!}
renameSubstCommute = {!!}