Compare commits

...

2 commits

2 changed files with 28 additions and 18 deletions

View file

@ -54,13 +54,13 @@ Parameter at_map : atom.
Inductive translate_morphism_path : context -> type_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
| Translate_Descend : forall Γ τ τ',
(τ :<= τ') ->
(Γ |- [[ τ ~~> τ' ]] = [{ λ τ (%0 des τ') }])
(Γ |- [[ τ ~~> τ' ]] = [{ λ τ morph (%0 des τ') }])
| Translate_Lift : forall Γ σ τ τ' m,
(Γ |- τ ~~> τ') ->
(Γ |- [[ τ ~~> τ' ]] = m) ->
(Γ |- [[ [< σ~τ >] ~~> [< σ~τ' >] ]] =
[{ λ (σ ~ τ) (m (%0 des τ)) as σ }])
[{ λ (σ ~ τ) morph (m (%0 des τ)) as σ }])
| Translate_Single : forall Γ h τ τ',
In (h, [< τ ->morph τ' >]) Γ ->
@ -69,7 +69,7 @@ Inductive translate_morphism_path : context -> type_DeBruijn -> type_DeBruijn ->
| Translate_Chain : forall Γ τ τ' τ'' m1 m2,
(Γ |- [[ τ ~~> τ' ]] = m1) ->
(Γ |- [[ τ' ~~> τ'' ]] = m2) ->
(Γ |- [[ τ ~~> τ'' ]] = [{ λ τ m2 (m1 %0) }])
(Γ |- [[ τ ~~> τ'' ]] = [{ λ τ morph m2 (m1 %0) }])
| Translate_MapSeq : forall Γ τ τ' m,
(Γ |- [[ τ ~~> τ' ]] = m) ->

View file

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