67 lines
1.7 KiB
Coq
67 lines
1.7 KiB
Coq
Require Import Autosubst2.syntax List.
|
||
|
||
Reserved Notation "Γ ⊢ a ;; ℓ ∈ A" (at level 70).
|
||
|
||
Definition get_level a :=
|
||
match a with
|
||
| Fixed ℓ => ℓ
|
||
| Floating ℓ => ℓ
|
||
end.
|
||
|
||
Inductive lookup {A} : nat -> list A -> A -> Prop :=
|
||
| here A Γ : lookup 0 (cons A Γ) A
|
||
| there i Γ A B :
|
||
lookup i Γ A ->
|
||
lookup (S i) (cons B Γ) A.
|
||
|
||
Definition ctx := list (Level * Ty).
|
||
|
||
Definition squash a :=
|
||
match a with
|
||
| Fixed ℓ => false
|
||
| Floating ℓ => true
|
||
end.
|
||
|
||
Fixpoint fixed_ctx (Γ : ctx) :=
|
||
match Γ with
|
||
| nil => nil
|
||
| (a, _) :: Γ => squash a :: fixed_ctx Γ
|
||
end.
|
||
|
||
(* false <= true *)
|
||
(* A term is liftable if it remains well-typed raising the levels of the floating levels to the current level *)
|
||
Fixpoint liftable Φ (a : Tm) :=
|
||
match a with
|
||
| VarTm i => lookup i Φ false
|
||
| FlApp a b => liftable Φ a /\ liftable Φ b
|
||
| App a b => liftable Φ a
|
||
| FlAbs a => liftable (false :: Φ) a
|
||
| Abs a => liftable (false :: Φ) a
|
||
end.
|
||
|
||
Inductive Wt (Γ : ctx) : Tm -> bool -> Ty -> Prop :=
|
||
| T_Var ℓ i ℓ0 A :
|
||
Bool.le (get_level ℓ0) ℓ ->
|
||
lookup i Γ (ℓ0, A) ->
|
||
Γ ⊢ VarTm i ;; ℓ ∈ A
|
||
|
||
| T_FlApp ℓ a b A B :
|
||
Γ ⊢ b ;; ℓ ∈ FlFun A B ->
|
||
Γ ⊢ a ;; ℓ ∈ A ->
|
||
Γ ⊢ FlApp b a ;; ℓ ∈ B
|
||
|
||
| T_FlAbs ℓ a A B :
|
||
(Floating ℓ, A) :: Γ ⊢ a ;; ℓ ∈ B ->
|
||
Γ ⊢ FlAbs a ;; ℓ ∈ FlFun A B
|
||
|
||
| T_App ℓ ℓ0 a b A B :
|
||
Γ ⊢ b ;; ℓ ∈ Fun ℓ0 A B ->
|
||
Γ ⊢ a ;; ℓ0 ∈ A ->
|
||
liftable (fixed_ctx Γ) a ->
|
||
Γ ⊢ App b a ;; ℓ ∈ A
|
||
|
||
| T_Abs ℓ ℓ0 b A B :
|
||
(Fixed ℓ0, A) :: Γ ⊢ b ;; ℓ ∈ B ->
|
||
Γ ⊢ Abs b ;; ℓ ∈ Fun ℓ0 A B
|
||
|
||
where "Γ ⊢ a ;; ℓ ∈ A" := (Wt Γ a ℓ A).
|