From 6f3b0fbc0b9fecc73b658de8d58d251fbf277422 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sat, 21 Sep 2024 06:48:26 +0200
Subject: [PATCH] typing: use cofinite quantification

---
 coq/typing_debruijn.v | 40 +++++++++++++++++++++++++---------------
 1 file changed, 25 insertions(+), 15 deletions(-)

diff --git a/coq/typing_debruijn.v b/coq/typing_debruijn.v
index d7098d4..51aa417 100644
--- a/coq/typing_debruijn.v
+++ b/coq/typing_debruijn.v
@@ -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 σ τ σ',