add context, morphism translation & typing for debruijn terms

This commit is contained in:
Michael Sippel 2024-09-20 21:41:38 +02:00
parent f76cec4a9d
commit 1edbb8d748
4 changed files with 151 additions and 0 deletions

View file

@ -9,6 +9,9 @@ Metatheory.v
terms_debruijn.v terms_debruijn.v
equiv_debruijn.v equiv_debruijn.v
subtype_debruijn.v subtype_debruijn.v
context_debruijn.v
morph_debruijn.v
typing_debruijn.v
subst_lemmas_debruijn.v subst_lemmas_debruijn.v
terms.v terms.v

4
coq/context_debruijn.v Normal file
View file

@ -0,0 +1,4 @@
Require Import Atom.
Require Import terms_debruijn.
Definition context : Type := (list (atom * type_DeBruijn)).

81
coq/morph_debruijn.v Normal file
View file

@ -0,0 +1,81 @@
Require Import terms_debruijn.
Require Import equiv_debruijn.
Require Import subtype_debruijn.
Require Import context_debruijn.
Require Import Atom.
Import AtomImpl.
From Coq Require Import Lists.List.
Import ListNotations.
Open Scope ladder_type_scope.
Open Scope ladder_expr_scope.
(* Given a context, there is a morphism path from τ to τ' *)
Reserved Notation "Γ '|-' σ '~~>' τ" (at level 101).
Inductive morphism_path : context -> type_DeBruijn -> type_DeBruijn -> Prop :=
| M_Sub : forall Γ τ τ',
τ :<= τ' ->
(Γ |- τ ~~> τ')
| M_Single : forall Γ h τ τ',
In (h, [< τ ->morph τ' >]) Γ ->
(Γ |- τ ~~> τ')
| M_Chain : forall Γ τ τ' τ'',
(Γ |- τ ~~> τ') ->
(Γ |- τ' ~~> τ'') ->
(Γ |- τ ~~> τ'')
| M_Lift : forall Γ σ τ τ',
(Γ |- τ ~~> τ') ->
(Γ |- [< σ ~ τ >] ~~> [< σ ~ τ' >])
| M_MapSeq : forall Γ τ τ',
(Γ |- τ ~~> τ') ->
(Γ |- [< [τ] >] ~~> [< [τ'] >])
where "Γ '|-' s '~~>' t" := (morphism_path Γ s t).
Lemma id_morphism_path : forall Γ τ, Γ |- τ ~~> τ.
Proof.
intros.
apply M_Sub, TSubRepr_Refl, TEq_Refl.
Qed.
Reserved Notation "Γ '|-' '[[' σ '~~>' τ ']]' '=' m" (at level 101).
(* some atom for the 'map' function on lists *)
Parameter at_map : atom.
Inductive translate_morphism_path : context -> type_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
| Translate_Descend : forall Γ τ τ',
(τ :<= τ') ->
(Γ |- [[ τ ~~> τ' ]] = [{ λ τ (%0 des τ') }])
| Translate_Lift : forall Γ σ τ τ' m,
(Γ |- τ ~~> τ') ->
(Γ |- [[ τ ~~> τ' ]] = m) ->
(Γ |- [[ [< σ~τ >] ~~> [< σ~τ' >] ]] =
[{ λ (σ ~ τ) (m (%0 des τ)) as σ }])
| Translate_Single : forall Γ h τ τ',
In (h, [< τ ->morph τ' >]) Γ ->
(Γ |- [[ τ ~~> τ' ]] = [{ $h }])
| Translate_Chain : forall Γ τ τ' τ'' m1 m2,
(Γ |- [[ τ ~~> τ' ]] = m1) ->
(Γ |- [[ τ' ~~> τ'' ]] = m2) ->
(Γ |- [[ τ ~~> τ'' ]] = [{ λ τ m2 (m1 %0) }])
| Translate_MapSeq : forall Γ τ τ' m,
(Γ |- [[ τ ~~> τ' ]] = m) ->
(Γ |- [[ [< [τ] >] ~~> [< [τ'] >] ]] =
[{
λ [τ] morph ($at_map # τ # τ' m %0)
}])
where "Γ '|-' '[[' σ '~~>' τ ']]' = m" := (translate_morphism_path Γ σ τ m).

63
coq/typing_debruijn.v Normal file
View file

@ -0,0 +1,63 @@
From Coq Require Import Lists.List.
Import ListNotations.
Require Import Atom.
Require Import terms_debruijn.
Require Import subtype_debruijn.
Require Import context_debruijn.
Require Import morph_debruijn.
Open Scope ladder_type_scope.
Open Scope ladder_expr_scope.
Reserved Notation "Γ '|-' x '\is' X" (at level 101).
Inductive typing : context -> expr_DeBruijn -> type_DeBruijn -> Prop :=
| T_Var : forall Γ x τ,
(In (x, τ) Γ) ->
(Γ |- [{ $x }] \is τ)
| T_Let : forall Γ s σ t τ x,
(Γ |- s \is σ) ->
(((x σ) :: Γ) |- t \is τ) ->
(Γ |- [{ let s in t }] \is τ)
| T_TypeAbs : forall Γ e τ,
(Γ |- e \is τ) ->
(Γ |- [{ Λ e }] \is [< τ >])
| T_TypeApp : forall Γ e σ τ,
(Γ |- e \is [< τ >]) ->
(Γ |- [{ e # σ }] \is (type_open σ τ))
| T_Abs : forall Γ x σ t τ,
(((x σ) :: Γ) |- t \is τ) ->
(Γ |- [{ λ σ t }] \is [< σ -> τ >])
| T_MorphAbs : forall Γ x σ t τ,
(((x σ) :: Γ) |- t \is τ) ->
(Γ |- [{ λ σ 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 τ).