module Definition.Untyped {a} (M : Set a) where
open import Tools.Fin
open import Tools.Nat
open import Tools.Product
open import Tools.List
open import Tools.PropositionalEquality as PE hiding (subst)
open import Definition.Untyped.NotParametrised public
private
variable
p p′ p₁ p₂ q q₁ q₂ r : M
n m ℓ : Nat
b : BinderMode
s : SigmaMode
bs bs′ : List _
ts ts′ : GenTs _ _ _
infix 30 ΠΣ⟨_⟩_,_▷_▹_
infix 30 Π_,_▷_▹_
infix 30 Σ_,_▷_▹_
infix 30 Σₚ_,_▷_▹_
infix 30 Σᵣ_,_▷_▹_
infix 30 Σ⟨_⟩_,_▷_▹_
infixl 30 _∘⟨_⟩_
infixl 30 _∘_
infix 30 ⟦_⟧_▹_
infixl 30 _ₛ•ₛ_ _•ₛ_ _ₛ•_
infix 25 _[_]
infix 25 _[_]₀
infix 25 _[_]↑
infix 25 _[_,_]
infix 25 _[_]↑²
data Kind : (ns : List Nat) → Set a where
Ukind : Kind []
Binderkind : (b : BinderMode) (p q : M) → Kind (0 ∷ 1 ∷ [])
Lamkind : (p : M) → Kind (1 ∷ [])
Appkind : (p : M) → Kind (0 ∷ 0 ∷ [])
Prodkind : SigmaMode → (p : M) → Kind (0 ∷ 0 ∷ [])
Fstkind : (p : M) → Kind (0 ∷ [])
Sndkind : (p : M) → Kind (0 ∷ [])
Prodreckind : (r p q : M) → Kind (1 ∷ 0 ∷ 2 ∷ [])
Natkind : Kind []
Zerokind : Kind []
Suckind : Kind (0 ∷ [])
Natreckind : (p q r : M) → Kind (1 ∷ 0 ∷ 2 ∷ 0 ∷ [])
Unitkind : Kind []
Starkind : Kind []
Emptykind : Kind []
Emptyreckind : (p : M) → Kind (0 ∷ 0 ∷ [])
data Term (n : Nat) : Set a where
var : (x : Fin n) → Term n
gen : {bs : List Nat} (k : Kind bs) (ts : GenTs Term n bs) → Term n
private
variable
A F H t u t′ u′ v : Term n
B E G : Term (1+ n)
k k′ : Kind _
pattern U = gen Ukind []
pattern ℕ = gen Natkind []
pattern Empty = gen Emptykind []
pattern Unit = gen Unitkind []
pattern ΠΣ⟨_⟩_,_▷_▹_ b p q F G = gen (Binderkind b p q) (F ∷ G ∷ [])
pattern Π_,_▷_▹_ p q F G = gen (Binderkind BMΠ p q) (F ∷ G ∷ [])
pattern Σₚ_,_▷_▹_ p q F G = gen (Binderkind (BMΣ Σₚ) p q) (F ∷ G ∷ [])
pattern Σᵣ_,_▷_▹_ p q F G = gen (Binderkind (BMΣ Σᵣ) p q) (F ∷ G ∷ [])
pattern Σ_,_▷_▹_ p q F G = gen (Binderkind (BMΣ _) p q) (F ∷ G ∷ [])
pattern Σ⟨_⟩_,_▷_▹_ s p q F G =
gen (Binderkind (BMΣ s) p q) (F ∷ G ∷ [])
pattern lam p t = gen (Lamkind p) (t ∷ [])
pattern _∘⟨_⟩_ t p u = gen (Appkind p) (t ∷ u ∷ [])
pattern _∘_ t u = gen (Appkind _) (t ∷ u ∷ [])
pattern prodₚ p t u = gen (Prodkind Σₚ p) (t ∷ u ∷ [])
pattern prodᵣ p t u = gen (Prodkind Σᵣ p) (t ∷ u ∷ [])
pattern prod m p t u = gen (Prodkind m p) (t ∷ u ∷ [])
pattern prod! t u = gen (Prodkind _ _) (t ∷ u ∷ [])
pattern fst p t = gen (Fstkind p) (t ∷ [])
pattern snd p t = gen (Sndkind p) (t ∷ [])
pattern prodrec r p q A t u = gen (Prodreckind r p q) (A ∷ t ∷ u ∷ [])
pattern zero = gen Zerokind []
pattern suc t = gen Suckind (t ∷ [])
pattern natrec p q r A z s n = gen (Natreckind p q r) (A ∷ z ∷ s ∷ n ∷ [])
pattern star = gen Starkind []
pattern emptyrec p A t = gen (Emptyreckind p) (A ∷ t ∷ [])
data BindingType : Set a where
BM : BinderMode → (p q : M) → BindingType
pattern BΠ p q = BM BMΠ p q
pattern BΠ! = BΠ _ _
pattern BΣ s p q = BM (BMΣ s) p q
pattern BΣ! = BΣ _ _ _
pattern BΣᵣ = BΣ Σᵣ _ _
pattern BΣₚ = BΣ Σₚ _ _
⟦_⟧_▹_ : BindingType → Term n → Term (1+ n) → Term n
⟦ BΠ p q ⟧ F ▹ G = Π p , q ▷ F ▹ G
⟦ BΣ m p q ⟧ F ▹ G = Σ⟨ m ⟩ p , q ▷ F ▹ G
B-PE-injectivity : ∀ W W' → ⟦ W ⟧ F ▹ G PE.≡ ⟦ W' ⟧ H ▹ E
→ F PE.≡ H × G PE.≡ E × W PE.≡ W'
B-PE-injectivity (BΠ p q) (BΠ .p .q) PE.refl =
PE.refl , PE.refl , PE.refl
B-PE-injectivity (BΣ p q m) (BΣ .p .q .m) PE.refl =
PE.refl , PE.refl , PE.refl
BΠ-PE-injectivity : ∀ {p p′ q q′} → BΠ p q PE.≡ BΠ p′ q′ → p PE.≡ p′ × q PE.≡ q′
BΠ-PE-injectivity PE.refl = PE.refl , PE.refl
BΣ-PE-injectivity :
∀ {p p′ q q′ m m′} →
BΣ m p q PE.≡ BΣ m′ p′ q′ → p PE.≡ p′ × q PE.≡ q′ × m PE.≡ m′
BΣ-PE-injectivity PE.refl = PE.refl , PE.refl , PE.refl
suc-PE-injectivity : suc t PE.≡ suc u → t PE.≡ u
suc-PE-injectivity PE.refl = PE.refl
prod-PE-injectivity : ∀ {m m′} → prod m p t u PE.≡ prod m′ p′ t′ u′
→ m PE.≡ m′ × p PE.≡ p′ × t PE.≡ t′ × u PE.≡ u′
prod-PE-injectivity PE.refl = PE.refl , PE.refl , PE.refl , PE.refl
data Neutral : Term n → Set a where
var : (x : Fin n) → Neutral (var x)
∘ₙ : Neutral t → Neutral (t ∘⟨ p ⟩ u)
fstₙ : Neutral t → Neutral (fst p t)
sndₙ : Neutral t → Neutral (snd p t)
natrecₙ : Neutral v → Neutral (natrec p q r G t u v)
prodrecₙ : Neutral t → Neutral (prodrec r p q A t u)
emptyrecₙ : Neutral t → Neutral (emptyrec p A t)
data Whnf {n : Nat} : Term n → Set a where
Uₙ : Whnf U
ΠΣₙ : Whnf (ΠΣ⟨ b ⟩ p , q ▷ A ▹ B)
ℕₙ : Whnf ℕ
Unitₙ : Whnf Unit
Emptyₙ : Whnf Empty
lamₙ : Whnf (lam p t)
zeroₙ : Whnf zero
sucₙ : Whnf (suc t)
starₙ : Whnf star
prodₙ : Whnf (prod s p t u)
ne : Neutral t → Whnf t
U≢ne : Neutral A → U PE.≢ A
U≢ne () PE.refl
ℕ≢ne : Neutral A → ℕ PE.≢ A
ℕ≢ne () PE.refl
Empty≢ne : Neutral A → Empty PE.≢ A
Empty≢ne () PE.refl
Unit≢ne : Neutral A → Unit PE.≢ A
Unit≢ne () PE.refl
B≢ne : ∀ W → Neutral A → ⟦ W ⟧ F ▹ G PE.≢ A
B≢ne (BΠ p q) () PE.refl
B≢ne (BΣ m p q) () PE.refl
ΠΣ≢ne : ∀ b → Neutral A → ΠΣ⟨ b ⟩ p , q ▷ F ▹ G PE.≢ A
ΠΣ≢ne BMΠ () PE.refl
ΠΣ≢ne (BMΣ s) () PE.refl
U≢B : ∀ W → U PE.≢ ⟦ W ⟧ F ▹ G
U≢B (BΠ p q) ()
U≢B (BΣ m p q) ()
U≢ΠΣ : ∀ b → U PE.≢ ΠΣ⟨ b ⟩ p , q ▷ F ▹ G
U≢ΠΣ BMΠ ()
U≢ΠΣ (BMΣ s) ()
ℕ≢B : ∀ W → ℕ PE.≢ ⟦ W ⟧ F ▹ G
ℕ≢B (BΠ p q) ()
ℕ≢B (BΣ m p q) ()
ℕ≢ΠΣ : ∀ b → ℕ PE.≢ ΠΣ⟨ b ⟩ p , q ▷ F ▹ G
ℕ≢ΠΣ BMΠ ()
ℕ≢ΠΣ (BMΣ s) ()
Empty≢B : ∀ W → Empty PE.≢ ⟦ W ⟧ F ▹ G
Empty≢B (BΠ p q) ()
Empty≢B (BΣ m p q) ()
Empty≢ΠΣ : ∀ b → Empty PE.≢ ΠΣ⟨ b ⟩ p , q ▷ F ▹ G
Empty≢ΠΣ BMΠ ()
Empty≢ΠΣ (BMΣ _) ()
Unit≢B : ∀ W → Unit PE.≢ ⟦ W ⟧ F ▹ G
Unit≢B (BΠ p q) ()
Unit≢B (BΣ m p q) ()
Unit≢ΠΣ : ∀ b → Unit PE.≢ ΠΣ⟨ b ⟩ p , q ▷ F ▹ G
Unit≢ΠΣ BMΠ ()
Unit≢ΠΣ (BMΣ _) ()
Π≢Σ : ∀ {m} → Π p₁ , q₁ ▷ F ▹ G PE.≢ Σ⟨ m ⟩ p₂ , q₂ ▷ H ▹ E
Π≢Σ ()
Σₚ≢Σᵣ : Σₚ p₁ , q₁ ▷ F ▹ G PE.≢ Σᵣ p₂ , q₂ ▷ H ▹ E
Σₚ≢Σᵣ ()
zero≢ne : Neutral t → zero PE.≢ t
zero≢ne () PE.refl
suc≢ne : Neutral t → suc u PE.≢ t
suc≢ne () PE.refl
prod≢ne : ∀ {m} → Neutral v → prod m p t u PE.≢ v
prod≢ne () PE.refl
data Natural {n : Nat} : Term n → Set a where
zeroₙ : Natural zero
sucₙ : Natural (suc t)
ne : Neutral t → Natural t
data Type {n : Nat} : Term n → Set a where
ΠΣₙ : Type (ΠΣ⟨ b ⟩ p , q ▷ A ▹ B)
ℕₙ : Type ℕ
Emptyₙ : Type Empty
Unitₙ : Type Unit
ne : Neutral t → Type t
⟦_⟧-type : ∀ (W : BindingType) → Type (⟦ W ⟧ F ▹ G)
⟦ BΠ p q ⟧-type = ΠΣₙ
⟦ BΣ m p q ⟧-type = ΠΣₙ
data Function {n : Nat} : Term n → Set a where
lamₙ : Function (lam p t)
ne : Neutral t → Function t
data Product {n : Nat} : Term n → Set a where
prodₙ : ∀ {m} → Product (prod m p t u)
ne : Neutral t → Product t
naturalWhnf : Natural t → Whnf t
naturalWhnf sucₙ = sucₙ
naturalWhnf zeroₙ = zeroₙ
naturalWhnf (ne x) = ne x
typeWhnf : Type A → Whnf A
typeWhnf ΠΣₙ = ΠΣₙ
typeWhnf ℕₙ = ℕₙ
typeWhnf Emptyₙ = Emptyₙ
typeWhnf Unitₙ = Unitₙ
typeWhnf (ne x) = ne x
functionWhnf : Function t → Whnf t
functionWhnf lamₙ = lamₙ
functionWhnf (ne x) = ne x
productWhnf : Product t → Whnf t
productWhnf prodₙ = prodₙ
productWhnf (ne x) = ne x
⟦_⟧ₙ : (W : BindingType) → Whnf (⟦ W ⟧ F ▹ G)
⟦_⟧ₙ (BΠ p q) = ΠΣₙ
⟦_⟧ₙ (BΣ m p q) = ΠΣₙ
data Numeral {n : Nat} : Term n → Set a where
zeroₙ : Numeral zero
sucₙ : Numeral t → Numeral (suc t)
data No-η-equality {n : Nat} : Term n → Set a where
Uₙ : No-η-equality U
Σᵣₙ : No-η-equality (Σᵣ p , q ▷ A ▹ B)
Emptyₙ : No-η-equality Empty
ℕₙ : No-η-equality ℕ
neₙ : Neutral A → No-η-equality A
No-η-equality→Whnf : No-η-equality A → Whnf A
No-η-equality→Whnf = λ where
Uₙ → Uₙ
Σᵣₙ → ΠΣₙ
Emptyₙ → Emptyₙ
ℕₙ → ℕₙ
(neₙ n) → ne n
mutual
wkGen : {m n : Nat} {bs : List Nat} (ρ : Wk m n) (c : GenTs (Term) n bs) → GenTs (Term) m bs
wkGen ρ [] = []
wkGen ρ (_∷_ {b = b} t c) = (wk (liftn ρ b) t) ∷ (wkGen ρ c)
wk : {m n : Nat} (ρ : Wk m n) (t : Term n) → Term m
wk ρ (var x) = var (wkVar ρ x)
wk ρ (gen k c) = gen k (wkGen ρ c)
wk1 : Term n → Term (1+ n)
wk1 = wk (step id)
wkNeutral : ∀ ρ → Neutral t → Neutral {n = n} (wk ρ t)
wkNeutral ρ (var n) = var (wkVar ρ n)
wkNeutral ρ (∘ₙ n) = ∘ₙ (wkNeutral ρ n)
wkNeutral ρ (fstₙ n) = fstₙ (wkNeutral ρ n)
wkNeutral ρ (sndₙ n) = sndₙ (wkNeutral ρ n)
wkNeutral ρ (natrecₙ n) = natrecₙ (wkNeutral ρ n)
wkNeutral ρ (prodrecₙ n) = prodrecₙ (wkNeutral ρ n)
wkNeutral ρ (emptyrecₙ e) = emptyrecₙ (wkNeutral ρ e)
wkNatural : ∀ ρ → Natural t → Natural {n = n} (wk ρ t)
wkNatural ρ sucₙ = sucₙ
wkNatural ρ zeroₙ = zeroₙ
wkNatural ρ (ne x) = ne (wkNeutral ρ x)
wkType : ∀ ρ → Type t → Type {n = n} (wk ρ t)
wkType ρ ΠΣₙ = ΠΣₙ
wkType ρ ℕₙ = ℕₙ
wkType ρ Emptyₙ = Emptyₙ
wkType ρ Unitₙ = Unitₙ
wkType ρ (ne x) = ne (wkNeutral ρ x)
wkFunction : ∀ ρ → Function t → Function {n = n} (wk ρ t)
wkFunction ρ lamₙ = lamₙ
wkFunction ρ (ne x) = ne (wkNeutral ρ x)
wkProduct : ∀ ρ → Product t → Product {n = n} (wk ρ t)
wkProduct ρ prodₙ = prodₙ
wkProduct ρ (ne x) = ne (wkNeutral ρ x)
wkWhnf : ∀ ρ → Whnf t → Whnf {n = n} (wk ρ t)
wkWhnf ρ Uₙ = Uₙ
wkWhnf ρ ΠΣₙ = ΠΣₙ
wkWhnf ρ ℕₙ = ℕₙ
wkWhnf ρ Emptyₙ = Emptyₙ
wkWhnf ρ Unitₙ = Unitₙ
wkWhnf ρ lamₙ = lamₙ
wkWhnf ρ prodₙ = prodₙ
wkWhnf ρ zeroₙ = zeroₙ
wkWhnf ρ sucₙ = sucₙ
wkWhnf ρ starₙ = starₙ
wkWhnf ρ (ne x) = ne (wkNeutral ρ x)
Subst : Nat → Nat → Set a
Subst m n = Fin n → Term m
head : Subst m (1+ n) → Term m
head σ = σ x0
tail : Subst m (1+ n) → Subst m n
tail σ x = σ (x +1)
substVar : (σ : Subst m n) (x : Fin n) → Term m
substVar σ x = σ x
idSubst : Subst n n
idSubst = var
wk1Subst : Subst m n → Subst (1+ m) n
wk1Subst σ x = wk1 (σ x)
liftSubst : (σ : Subst m n) → Subst (1+ m) (1+ n)
liftSubst σ x0 = var x0
liftSubst σ (x +1) = wk1Subst σ x
liftSubstn : {k m : Nat} → Subst k m → (n : Nat) → Subst (n + k) (n + m)
liftSubstn σ Nat.zero = σ
liftSubstn σ (1+ n) = liftSubst (liftSubstn σ n)
toSubst : Wk m n → Subst m n
toSubst pr x = var (wkVar pr x)
mutual
substGen : {bs : List Nat} (σ : Subst m n) (g : GenTs (Term) n bs) → GenTs (Term) m bs
substGen σ [] = []
substGen σ (_∷_ {b = b} t ts) = t [ liftSubstn σ b ] ∷ (substGen σ ts)
_[_] : (t : Term n) (σ : Subst m n) → Term m
var x [ σ ] = substVar σ x
gen x c [ σ ] = gen x (substGen σ c)
consSubst : Subst m n → Term m → Subst m (1+ n)
consSubst σ t x0 = t
consSubst σ t (x +1) = σ x
sgSubst : Term n → Subst n (1+ n)
sgSubst = consSubst idSubst
_ₛ•ₛ_ : Subst ℓ m → Subst m n → Subst ℓ n
_ₛ•ₛ_ σ σ′ x = σ′ x [ σ ]
_•ₛ_ : Wk ℓ m → Subst m n → Subst ℓ n
_•ₛ_ ρ σ x = wk ρ (σ x)
_ₛ•_ : Subst ℓ m → Wk m n → Subst ℓ n
_ₛ•_ σ ρ x = σ (wkVar ρ x)
_[_]₀ : (t : Term (1+ n)) (s : Term n) → Term n
t [ s ]₀ = t [ sgSubst s ]
_[_]↑ : (t : Term (1+ n)) (s : Term (1+ n)) → Term (1+ n)
t [ s ]↑ = t [ consSubst (wk1Subst idSubst) s ]
_[_,_] : (t : Term (1+ (1+ n))) (s s′ : Term n) → Term n
t [ s , s′ ] = t [ consSubst (sgSubst s) s′ ]
_[_]↑² : (t : Term (1+ n)) (s : Term (1+ (1+ n))) → Term (1+ (1+ n))
t [ s ]↑² = t [ consSubst (wk1Subst (wk1Subst idSubst)) s ]
B-subst : (σ : Subst m n) (W : BindingType) (F : Term n) (G : Term (1+ n))
→ (⟦ W ⟧ F ▹ G) [ σ ] PE.≡ ⟦ W ⟧ F [ σ ] ▹ (G [ liftSubst σ ])
B-subst σ (BΠ p q) F G = PE.refl
B-subst σ (BΣ m p q) F G = PE.refl
gen-cong⁻¹ :
gen {bs = bs} k ts ≡ gen {bs = bs′} k′ ts′ →
∃ λ (eq : bs ≡ bs′) →
PE.subst Kind eq k ≡ k′ ×
PE.subst (GenTs Term _) eq ts ≡ ts′
gen-cong⁻¹ refl = refl , refl , refl
∷-cong⁻¹ :
∀ {b} {t t′ : Term (b + n)} →
GenTs._∷_ {A = Term} {b = b} t ts ≡ t′ ∷ ts′ →
t ≡ t′ × ts ≡ ts′
∷-cong⁻¹ refl = refl , refl