From 1edbb8d7481641216b0ac8052b3f9d4dc1a21437 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Fri, 20 Sep 2024 21:41:38 +0200
Subject: [PATCH] add context, morphism translation & typing for debruijn terms

---
 coq/_CoqProject        |  3 ++
 coq/context_debruijn.v |  4 +++
 coq/morph_debruijn.v   | 81 ++++++++++++++++++++++++++++++++++++++++++
 coq/typing_debruijn.v  | 63 ++++++++++++++++++++++++++++++++
 4 files changed, 151 insertions(+)
 create mode 100644 coq/context_debruijn.v
 create mode 100644 coq/morph_debruijn.v
 create mode 100644 coq/typing_debruijn.v

diff --git a/coq/_CoqProject b/coq/_CoqProject
index a81a62d..5f61850 100644
--- a/coq/_CoqProject
+++ b/coq/_CoqProject
@@ -9,6 +9,9 @@ Metatheory.v
 terms_debruijn.v
 equiv_debruijn.v
 subtype_debruijn.v
+context_debruijn.v
+morph_debruijn.v
+typing_debruijn.v
 subst_lemmas_debruijn.v
 
 terms.v
diff --git a/coq/context_debruijn.v b/coq/context_debruijn.v
new file mode 100644
index 0000000..45d61d0
--- /dev/null
+++ b/coq/context_debruijn.v
@@ -0,0 +1,4 @@
+Require Import Atom.
+Require Import terms_debruijn.
+
+Definition context : Type := (list (atom * type_DeBruijn)).
diff --git a/coq/morph_debruijn.v b/coq/morph_debruijn.v
new file mode 100644
index 0000000..f4b5872
--- /dev/null
+++ b/coq/morph_debruijn.v
@@ -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).
diff --git a/coq/typing_debruijn.v b/coq/typing_debruijn.v
new file mode 100644
index 0000000..d1675a5
--- /dev/null
+++ b/coq/typing_debruijn.v
@@ -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 τ).