2024-09-20 21:41:38 +02:00
|
|
|
|
From Coq Require Import Lists.List.
|
|
|
|
|
Import ListNotations.
|
2024-09-21 06:48:26 +02:00
|
|
|
|
Require Import Metatheory.
|
2024-09-20 21:41:38 +02:00
|
|
|
|
Require Import Atom.
|
2024-09-21 13:00:57 +02:00
|
|
|
|
Require Import debruijn.
|
|
|
|
|
Require Import subtype.
|
2024-09-21 17:26:26 +02:00
|
|
|
|
Require Import env.
|
2024-09-21 13:00:57 +02:00
|
|
|
|
Require Import morph.
|
2024-09-20 21:41:38 +02:00
|
|
|
|
|
|
|
|
|
Open Scope ladder_type_scope.
|
|
|
|
|
Open Scope ladder_expr_scope.
|
|
|
|
|
|
|
|
|
|
Reserved Notation "Γ '|-' x '\is' X" (at level 101).
|
2024-09-21 17:26:26 +02:00
|
|
|
|
Inductive typing : env -> expr_DeBruijn -> type_DeBruijn -> Prop :=
|
2024-09-20 21:41:38 +02:00
|
|
|
|
| T_Var : forall Γ x τ,
|
2024-09-24 04:28:41 +02:00
|
|
|
|
(env_wf Γ) ->
|
2024-09-22 13:37:11 +02:00
|
|
|
|
(binds x τ Γ) ->
|
2024-09-20 21:41:38 +02:00
|
|
|
|
(Γ |- [{ $x }] \is τ)
|
|
|
|
|
|
2024-09-21 06:48:26 +02:00
|
|
|
|
| T_Let : forall Γ L s σ t τ,
|
2024-09-20 21:41:38 +02:00
|
|
|
|
(Γ |- s \is σ) ->
|
2024-09-21 06:48:26 +02:00
|
|
|
|
(forall x : atom, x `notin` L ->
|
|
|
|
|
( (x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)) ->
|
2024-09-20 21:41:38 +02:00
|
|
|
|
(Γ |- [{ let s in t }] \is τ)
|
|
|
|
|
|
2024-09-24 04:28:41 +02:00
|
|
|
|
| T_TypeAbs : forall Γ L e τ,
|
|
|
|
|
(forall x : atom, x `notin` L ->
|
|
|
|
|
( Γ |- (expr_open_type (ty_fvar x) e) \is τ)) ->
|
2024-09-20 21:41:38 +02:00
|
|
|
|
(Γ |- [{ Λ e }] \is [< ∀ τ >])
|
|
|
|
|
|
|
|
|
|
| T_TypeApp : forall Γ e σ τ,
|
|
|
|
|
(Γ |- e \is [< ∀ τ >]) ->
|
|
|
|
|
(Γ |- [{ e # σ }] \is (type_open σ τ))
|
|
|
|
|
|
2024-09-21 06:48:26 +02:00
|
|
|
|
| T_Abs : forall Γ L σ t τ,
|
|
|
|
|
(forall x : atom, x `notin` L ->
|
|
|
|
|
( (x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)) ->
|
2024-09-20 21:41:38 +02:00
|
|
|
|
(Γ |- [{ λ σ ↦ t }] \is [< σ -> τ >])
|
|
|
|
|
|
2024-09-21 06:48:26 +02:00
|
|
|
|
| T_MorphAbs : forall Γ L σ t τ,
|
|
|
|
|
(forall x : atom, x `notin` L ->
|
|
|
|
|
( (x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)) ->
|
2024-09-20 21:41:38 +02:00
|
|
|
|
(Γ |- [{ λ σ ↦morph t }] \is [< σ ->morph τ >])
|
|
|
|
|
|
|
|
|
|
| T_App : forall Γ f a σ' σ τ,
|
|
|
|
|
(Γ |- f \is [< σ -> τ >]) ->
|
|
|
|
|
(Γ |- a \is σ') ->
|
|
|
|
|
(Γ |- σ' ~~> σ) ->
|
|
|
|
|
(Γ |- [{ f a }] \is τ)
|
|
|
|
|
|
|
|
|
|
| T_MorphFun : forall Γ f σ τ,
|
|
|
|
|
(Γ |- f \is [< σ ->morph τ >]) ->
|
|
|
|
|
(Γ |- f \is [< σ -> τ >])
|
|
|
|
|
|
|
|
|
|
| T_Ascend : forall Γ e τ τ',
|
|
|
|
|
(Γ |- e \is τ) ->
|
|
|
|
|
(Γ |- [{ e as τ' }] \is [< τ' ~ τ >])
|
|
|
|
|
|
|
|
|
|
| T_DescendImplicit : forall Γ x τ τ',
|
|
|
|
|
(Γ |- x \is τ) ->
|
|
|
|
|
(τ :<= τ') ->
|
|
|
|
|
(Γ |- x \is τ')
|
|
|
|
|
|
|
|
|
|
| T_Descend : forall Γ x τ τ',
|
|
|
|
|
(Γ |- x \is τ) ->
|
|
|
|
|
(τ :<= τ') ->
|
|
|
|
|
(Γ |- [{ x des τ' }] \is τ')
|
|
|
|
|
|
|
|
|
|
where "Γ '|-' x '\is' τ" := (typing Γ x τ).
|
2024-09-20 22:04:19 +02:00
|
|
|
|
|
|
|
|
|
|
2024-09-24 04:28:41 +02:00
|
|
|
|
Create HintDb typing_hints.
|
|
|
|
|
Hint Constructors typing :typing_hints.
|
|
|
|
|
|
2024-09-20 22:04:19 +02:00
|
|
|
|
|
|
|
|
|
Reserved Notation "Γ '|-' '[[' e \is τ ']]' '=' f" (at level 101).
|
|
|
|
|
|
2024-09-21 17:26:26 +02:00
|
|
|
|
Inductive translate_typing : env -> expr_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
|
2024-09-20 22:04:19 +02:00
|
|
|
|
|
|
|
|
|
| Expand_Var : forall Γ x τ,
|
|
|
|
|
(Γ |- [{ $x }] \is τ) ->
|
|
|
|
|
(Γ |- [[ [{ $x }] \is τ ]] = [{ $x }])
|
|
|
|
|
|
2024-09-21 06:48:26 +02:00
|
|
|
|
| Expand_Let : forall Γ L e e' t t' σ τ,
|
2024-09-20 22:04:19 +02:00
|
|
|
|
(Γ |- e \is σ) ->
|
2024-09-21 06:48:26 +02:00
|
|
|
|
(forall x : atom, x `notin` L ->
|
2024-09-22 13:37:11 +02:00
|
|
|
|
( (x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ) ->
|
2024-09-24 04:28:41 +02:00
|
|
|
|
( (x,σ)::Γ |- [[ (expr_open (ex_fvar x) t) \is τ ]] = (expr_open (ex_fvar x) t') )
|
2024-09-21 06:48:26 +02:00
|
|
|
|
) ->
|
2024-09-20 22:04:19 +02:00
|
|
|
|
(Γ |- [[ e \is σ ]] = e') ->
|
|
|
|
|
(Γ |- [[ [{ let e in t }] \is τ ]] = [{ let e' in t' }])
|
|
|
|
|
|
2024-09-24 04:28:41 +02:00
|
|
|
|
| Expand_TypeAbs : forall Γ L e e' τ,
|
|
|
|
|
(forall x : atom, x `notin` L ->
|
|
|
|
|
(Γ |- (expr_open_type (ty_fvar x) e) \is τ) ->
|
|
|
|
|
(Γ |- [[ (expr_open_type (ty_fvar x) e) \is τ ]] = (expr_open_type (ty_fvar x) e'))
|
|
|
|
|
) ->
|
2024-09-20 22:04:19 +02:00
|
|
|
|
(Γ |- [[ [{ Λ e }] \is [< ∀ τ >] ]] = [{ Λ e' }])
|
|
|
|
|
|
|
|
|
|
| Expand_TypeApp : forall Γ e e' σ τ,
|
|
|
|
|
(Γ |- e \is [< ∀ τ >]) ->
|
2024-09-24 04:57:16 +02:00
|
|
|
|
(Γ |- [[ e \is [< ∀ τ >] ]] = e') ->
|
2024-09-20 22:04:19 +02:00
|
|
|
|
(Γ |- [[ [{ e # σ }] \is (type_open σ τ) ]] = [{ e' # σ }])
|
|
|
|
|
|
2024-09-21 06:48:26 +02:00
|
|
|
|
| Expand_Abs : forall Γ L σ e e' τ,
|
2024-09-20 22:04:19 +02:00
|
|
|
|
(Γ |- [{ λ σ ↦ e }] \is [< σ -> τ >]) ->
|
2024-09-21 06:48:26 +02:00
|
|
|
|
(forall x : atom, x `notin` L ->
|
|
|
|
|
( (x,σ)::Γ |- (expr_open (ex_fvar x) e) \is τ) ->
|
2024-09-24 04:28:41 +02:00
|
|
|
|
( (x,σ)::Γ |- [[ (expr_open (ex_fvar x) e) \is τ ]] = (expr_open (ex_fvar x) e') )
|
2024-09-21 06:48:26 +02:00
|
|
|
|
) ->
|
2024-09-20 22:04:19 +02:00
|
|
|
|
(Γ |- [[ [{ λ σ ↦ e }] \is [< σ -> τ >] ]] = [{ λ σ ↦ e' }])
|
|
|
|
|
|
2024-09-21 06:48:26 +02:00
|
|
|
|
| Expand_MorphAbs : forall Γ L σ e e' τ,
|
2024-09-20 22:04:19 +02:00
|
|
|
|
(Γ |- [{ λ σ ↦ e }] \is [< σ -> τ >]) ->
|
2024-09-21 06:48:26 +02:00
|
|
|
|
(forall x : atom, x `notin` L ->
|
|
|
|
|
( (x,σ)::Γ |- (expr_open (ex_fvar x) e) \is τ) ->
|
2024-09-24 04:28:41 +02:00
|
|
|
|
( (x,σ)::Γ |- [[ (expr_open (ex_fvar x) e) \is τ ]] = (expr_open (ex_fvar x) e') )
|
2024-09-21 06:48:26 +02:00
|
|
|
|
) ->
|
2024-09-20 22:04:19 +02:00
|
|
|
|
(Γ |- [[ [{ λ σ ↦morph e }] \is [< σ ->morph τ >] ]] = [{ λ σ ↦morph e' }])
|
|
|
|
|
|
|
|
|
|
| Expand_App : forall Γ f f' a a' m σ τ σ',
|
|
|
|
|
(Γ |- f \is [< σ -> τ >]) ->
|
|
|
|
|
(Γ |- a \is σ') ->
|
|
|
|
|
(Γ |- σ' ~~> σ) ->
|
|
|
|
|
(Γ |- [[ f \is [< σ -> τ >] ]] = f') ->
|
|
|
|
|
(Γ |- [[ a \is σ' ]] = a') ->
|
|
|
|
|
(Γ |- [[ σ' ~~> σ ]] = m) ->
|
|
|
|
|
(Γ |- [[ [{ f a }] \is τ ]] = [{ f' (m a') }])
|
|
|
|
|
|
|
|
|
|
| Expand_MorphFun : forall Γ f f' σ τ,
|
|
|
|
|
(Γ |- f \is [< σ ->morph τ >]) ->
|
|
|
|
|
(Γ |- f \is [< σ -> τ >]) ->
|
|
|
|
|
(Γ |- [[ f \is [< σ ->morph τ >] ]] = f') ->
|
|
|
|
|
(Γ |- [[ f \is [< σ -> τ >] ]] = f')
|
|
|
|
|
|
|
|
|
|
| Expand_Ascend : forall Γ e e' τ τ',
|
|
|
|
|
(Γ |- e \is τ) ->
|
|
|
|
|
(Γ |- [{ e as τ' }] \is [< τ' ~ τ >]) ->
|
|
|
|
|
(Γ |- [[ e \is τ ]] = e') ->
|
|
|
|
|
(Γ |- [[ [{ e as τ' }] \is [< τ' ~ τ >] ]] = [{ e' as τ' }])
|
|
|
|
|
|
|
|
|
|
| Expand_Descend : forall Γ e e' τ τ',
|
|
|
|
|
(Γ |- e \is τ) ->
|
|
|
|
|
(τ :<= τ') ->
|
|
|
|
|
(Γ |- [{ e des τ' }] \is τ') ->
|
|
|
|
|
(Γ |- [[ e \is τ ]] = e') ->
|
|
|
|
|
(Γ |- [[ e \is τ' ]] = [{ e' des τ' }])
|
|
|
|
|
|
|
|
|
|
where "Γ '|-' '[[' e '\is' τ ']]' '=' f" := (translate_typing Γ e τ f).
|