syntaxAlchemist/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

typing: use cofinite quantification

Browse source
This commit is contained in:
Michael Sippel 2024-09-21 06:48:26 +02:00
parent 67e4c13d57
commit 6f3b0fbc0b
Signed by: senvas
GPG key ID: F96CF119C34B64A6
1 changed files with 25 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
coq/typing_debruijn.v
View file

@ -1,5 +1,6 @@
From Coq Require Import Lists.List. From Coq Require Import Lists.List.
Import ListNotations. Import ListNotations.
Require Import Metatheory.
Require Import Atom. Require Import Atom.
Require Import terms_debruijn. Require Import terms_debruijn.
Require Import subtype_debruijn. Require Import subtype_debruijn.
@ -15,9 +16,10 @@ Inductive typing : context -> expr_DeBruijn -> type_DeBruijn -> Prop :=
(In (x, τ) Γ) -> (In (x, τ) Γ) ->
(Γ |- [{ $x }] \is τ) (Γ |- [{ $x }] \is τ)
| T_Let : forall Γ s σ t τ x, | T_Let : forall Γ L s σ t τ,
(Γ |- s \is σ) -> (Γ |- s \is σ) ->
(((x σ) :: Γ) |- t \is τ) -> (forall x : atom, x `notin` L ->
( (x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)) ->
(Γ |- [{ let s in t }] \is τ) (Γ |- [{ let s in t }] \is τ)
| T_TypeAbs : forall Γ e τ, | T_TypeAbs : forall Γ e τ,
@ -28,12 +30,14 @@ Inductive typing : context -> expr_DeBruijn -> type_DeBruijn -> Prop :=
(Γ |- e \is [< ∀ τ >]) -> (Γ |- e \is [< ∀ τ >]) ->
(Γ |- [{ e # σ }] \is (type_open σ τ)) (Γ |- [{ e # σ }] \is (type_open σ τ))
| T_Abs : forall Γ x σ t τ, | T_Abs : forall Γ L σ t τ,
(((x σ) :: Γ) |- t \is τ) -> (forall x : atom, x `notin` L ->
( (x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)) ->
(Γ |- [{ λ σ ↦ t }] \is [< σ -> τ >]) (Γ |- [{ λ σ ↦ t }] \is [< σ -> τ >])
| T_MorphAbs : forall Γ x σ t τ, | T_MorphAbs : forall Γ L σ t τ,
(((x σ) :: Γ) |- t \is τ) -> (forall x : atom, x `notin` L ->
( (x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)) ->
(Γ |- [{ λ σ ↦morph t }] \is [< σ ->morph τ >]) (Γ |- [{ λ σ ↦morph t }] \is [< σ ->morph τ >])
| T_App : forall Γ f a σ' σ τ, | T_App : forall Γ f a σ' σ τ,
@ -72,11 +76,13 @@ Inductive translate_typing : context -> expr_DeBruijn -> type_DeBruijn -> expr_D
(Γ |- [{ $x }] \is τ) -> (Γ |- [{ $x }] \is τ) ->
(Γ |- [[ [{ $x }] \is τ ]] = [{ $x }]) (Γ |- [[ [{ $x }] \is τ ]] = [{ $x }])
| Expand_Let : forall Γ x e e' t t' σ τ, | Expand_Let : forall Γ L e e' t t' σ τ,
(Γ |- e \is σ) -> (Γ |- e \is σ) ->
((x,σ)::Γ |- t \is τ) -> (forall x : atom, x `notin` L ->
( (x,σ)::Γ |- (expr_open t (ex_fvar x)) \is τ) ->
( (x,σ)::Γ |- [[ t \is τ ]] = t' )
) ->
(Γ |- [[ e \is σ ]] = e') -> (Γ |- [[ e \is σ ]] = e') ->
((x,σ)::Γ |- [[ t \is τ ]] = t') ->
(Γ |- [[ [{ let e in t }] \is τ ]] = [{ let e' in t' }]) (Γ |- [[ [{ let e in t }] \is τ ]] = [{ let e' in t' }])
| Expand_TypeAbs : forall Γ e e' τ, | Expand_TypeAbs : forall Γ e e' τ,
@ -89,16 +95,20 @@ Inductive translate_typing : context -> expr_DeBruijn -> type_DeBruijn -> expr_D
(Γ |- [[ e \is τ ]] = e') -> (Γ |- [[ e \is τ ]] = e') ->
(Γ |- [[ [{ e # σ }] \is (type_open σ τ) ]] = [{ e' # σ }]) (Γ |- [[ [{ e # σ }] \is (type_open σ τ) ]] = [{ e' # σ }])
| Expand_Abs : forall Γ x σ e e' τ, | Expand_Abs : forall Γ L σ e e' τ,
((x,σ)::Γ |- e \is τ) ->
(Γ |- [{ λ σ ↦ e }] \is [< σ -> τ >]) -> (Γ |- [{ λ σ ↦ e }] \is [< σ -> τ >]) ->
((x,σ)::Γ |- [[ e \is τ ]] = e') -> (forall x : atom, x `notin` L ->
( (x,σ)::Γ |- (expr_open (ex_fvar x) e) \is τ) ->
( (x,σ)::Γ |- [[ e \is τ ]] = e' )
) ->
(Γ |- [[ [{ λ σ ↦ e }] \is [< σ -> τ >] ]] = [{ λ σ ↦ e' }]) (Γ |- [[ [{ λ σ ↦ e }] \is [< σ -> τ >] ]] = [{ λ σ ↦ e' }])
| Expand_MorphAbs : forall Γ x σ e e' τ, | Expand_MorphAbs : forall Γ L σ e e' τ,
((x,σ)::Γ |- e \is τ) ->
(Γ |- [{ λ σ ↦ e }] \is [< σ -> τ >]) -> (Γ |- [{ λ σ ↦ e }] \is [< σ -> τ >]) ->
((x,σ)::Γ |- [[ e \is τ ]] = e') -> (forall x : atom, x `notin` L ->
( (x,σ)::Γ |- (expr_open (ex_fvar x) e) \is τ) ->
( (x,σ)::Γ |- [[ e \is τ ]] = e' )
) ->
(Γ |- [[ [{ λ σ ↦morph e }] \is [< σ ->morph τ >] ]] = [{ λ σ ↦morph e' }]) (Γ |- [[ [{ λ σ ↦morph e }] \is [< σ ->morph τ >] ]] = [{ λ σ ↦morph e' }])
| Expand_App : forall Γ f f' a a' m σ τ σ', | Expand_App : forall Γ f f' a a' m σ τ σ',