From 7e6ef4ca96c64cda2d38302d8e0c9b4d6b4ced12 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Sun, 22 Sep 2024 22:49:11 +0200
Subject: [PATCH 1/3] a even preciser type system

now, a mention and a use are different
---
 Capless/Typing.lean | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/Capless/Typing.lean b/Capless/Typing.lean
index 359b7e2b..23b16022 100644
--- a/Capless/Typing.lean
+++ b/Capless/Typing.lean
@@ -8,17 +8,17 @@ namespace Capless
 inductive Typed : Context n m k -> Term n m k -> EType n m k -> CaptureSet n k -> Prop where
 | var :
   Context.Bound Γ x (S^C) ->
-  Typed Γ (Term.var x) (S^{x=x}) {x=x}
+  Typed Γ (Term.var x) (S^{x=x}) {}
 | pack :
-  Typed (Γ.cvar (CBinding.inst C)) (Term.var x) (EType.type T) {x=x} ->
-  Typed Γ (Term.pack C x) (∃c.T) {x=x}
+  Typed (Γ.cvar (CBinding.inst C)) (Term.var x) (EType.type T) Cx.cweaken ->
+  Typed Γ (Term.pack C x) (∃c.T) Cx
 | sub :
   Typed Γ t E1 C1 ->
   (Γ ⊢ C1 <:c C2) ->
   (Γ ⊢ E1 <:e E2) ->
   Typed Γ t E2 C2
 | abs {C : CaptureSet n k} :
-  Typed (Γ,x:T) t E (C.weaken ∪ {x=0}) ->
+  Typed (Γ,x:T) t E C.weaken ->
   Typed Γ (λ(x:T)t) ((∀(x:T)E)^C) {}
 | tabs {C : CaptureSet n k} :
   Typed (Γ,X<:S) t E C ->
@@ -30,18 +30,18 @@ inductive Typed : Context n m k -> Term n m k -> EType n m k -> CaptureSet n k -
   Typed Γ (Term.var x) (EType.type T) {x=x} ->
   Typed Γ (Term.boxed x) ((SType.box T)^{}) {}
 | app :
-  Typed Γ (Term.var x) (EType.type (∀(x:T)E)^C) {x=x} ->
-  Typed Γ (Term.var y) T {x=y} ->
-  Typed Γ (Term.app x y) (E.open y) ({x=x} ∪ {x=y})
+  Typed Γ (Term.var x) (EType.type (∀(x:T)E)^C) C' ->
+  Typed Γ (Term.var y) T C' ->
+  Typed Γ (Term.app x y) (E.open y) (C' ∪ C)
 | tapp :
-  Typed Γ (Term.var x) (EType.type (∀[X<:SType.tvar X]E)^C) {x=x} ->
-  Typed Γ (Term.tapp x X) (E.topen X) {x=x}
+  Typed Γ (Term.var x) (EType.type (∀[X<:SType.tvar X]E)^C) C' ->
+  Typed Γ (Term.tapp x X) (E.topen X) (C' ∪ C)
 | capp :
-  Typed Γ (Term.var x) (EType.type (∀[c]E)^C) {x=x} ->
-  Typed Γ (Term.capp x c) (E.copen c) {x=x}
+  Typed Γ (Term.var x) (EType.type (∀[c]E)^C) C' ->
+  Typed Γ (Term.capp x c) (E.copen c) (C' ∪ C)
 | unbox :
-  Typed Γ (Term.var x) (EType.type (SType.box (S^C))^{}) {} ->
-  Typed Γ (C o- x) (S^C) C
+  Typed Γ (Term.var x) (EType.type (SType.box (S^C))^{}) C' ->
+  Typed Γ (C o- x) (S^C) (C' ∪ C)
 | letin :
   Typed Γ t (EType.type T) C ->
   Typed (Γ,x: T) u E.weaken C.weaken ->  -- which means that x ∉ C and x ∉ fv(E)
@@ -57,6 +57,6 @@ inductive Typed : Context n m k -> Term n m k -> EType n m k -> CaptureSet n k -
   Typed (Γ,c:=C) t E.cweaken C0.cweaken ->
   Typed Γ (let c=C in t) E C0
 
-notation:30 Γ " ⊢ " t " : " E " @ " C => Typed Γ t E C
+notation:40 C "; " Γ:80 " ⊢ " t " : " E => Typed Γ t E C
 
 end Capless

From 91aebae4ab522c06556852750ea42b6b1e2c024f Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Sun, 22 Sep 2024 23:49:45 +0200
Subject: [PATCH 2/3] a new notation

---
 Capless/Typing.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Capless/Typing.lean b/Capless/Typing.lean
index 23b16022..733f76e4 100644
--- a/Capless/Typing.lean
+++ b/Capless/Typing.lean
@@ -57,6 +57,6 @@ inductive Typed : Context n m k -> Term n m k -> EType n m k -> CaptureSet n k -
   Typed (Γ,c:=C) t E.cweaken C0.cweaken ->
   Typed Γ (let c=C in t) E C0
 
-notation:40 C "; " Γ:80 " ⊢ " t " : " E => Typed Γ t E C
+notation:40 Γ:80 "[" C "]" " ⊢ " t " : " E => Typed Γ t E C
 
 end Capless

From 4446b3b4e767a4458042f80306b7d013c15e4540 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Sun, 22 Sep 2024 23:49:51 +0200
Subject: [PATCH 3/3] port the proof

---
 Capless/Inversion/Typing.lean        | 37 +++++++++++++++-------------
 Capless/Renaming/Capture/Typing.lean |  1 +
 Capless/Renaming/Term/Typing.lean    |  2 +-
 Capless/Soundness/Preservation.lean  | 14 +++++------
 Capless/Soundness/Progress.lean      |  8 +++---
 Capless/Subst/Basic.lean             |  2 +-
 Capless/Subst/Capture/Typing.lean    |  5 ++--
 Capless/Subst/Term/Typing.lean       |  2 +-
 Capless/Typing/Basic.lean            | 19 ++++++++++----
 9 files changed, 52 insertions(+), 38 deletions(-)

diff --git a/Capless/Inversion/Typing.lean b/Capless/Inversion/Typing.lean
index e0f87e2a..41dea88e 100644
--- a/Capless/Inversion/Typing.lean
+++ b/Capless/Inversion/Typing.lean
@@ -11,15 +11,18 @@ namespace Capless
 theorem Typed.app_inv'
   (he : t0 = Term.app x y)
   (h : Typed Γ t0 E Ct0) :
-  ∃ T Cf F E0, Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.forall T F))) {x=x}
-    ∧ Typed Γ (Term.var y) (EType.type T) {x=y}
+  ∃ T Cf F E0, Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.forall T F))) {}
+    ∧ Typed Γ (Term.var y) (EType.type T) {}
     ∧ E0 = F.open y
     ∧ ESubtyp Γ E0 E := by
     induction h <;> try (solve | cases he)
-    case app x C T F y h1 h2 _ _ =>
+    case app x C T F C' y h1 h2 _ _ =>
       cases he
       exists T, C, F, (F.open y)
-      repeat (constructor; trivial)
+      repeat (any_goals apply And.intro)
+      all_goals try trivial
+      apply Typed.precise_cv; exact h1
+      apply Typed.precise_cv; exact h2
       apply ESubtyp.refl
     case sub hsub ih =>
       have ih := ih he
@@ -31,8 +34,8 @@ theorem Typed.app_inv'
 
 theorem Typed.app_inv
   (h : Typed Γ (Term.app x y) E Ct) :
-  ∃ T Cf F E0, Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.forall T F))) {x=x}
-    ∧ Typed Γ (Term.var y) (EType.type T) {x=y}
+  ∃ T Cf F E0, Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.forall T F))) {}
+    ∧ Typed Γ (Term.var y) (EType.type T) {}
     ∧ E0 = F.open y
     ∧ ESubtyp Γ E0 E :=
   Typed.app_inv' rfl h
@@ -41,7 +44,7 @@ theorem Typed.tapp_inv'
   (he : t0 = Term.tapp x X)
   (h : Typed Γ t0 E Ct) :
   ∃ Cf F E0,
-    Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.tforall (SType.tvar X) F))) {x=x}
+    Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.tforall (SType.tvar X) F))) {}
     ∧ E0 = F.topen X
     ∧ ESubtyp Γ E0 E := by
   induction h <;> try (solve | cases he)
@@ -49,11 +52,11 @@ theorem Typed.tapp_inv'
     cases he
     repeat (apply Exists.intro)
     apply And.intro
-    { trivial }
+    { apply Typed.precise_cv; trivial }
     apply And.intro
     { trivial }
     { apply ESubtyp.refl }
-  case sub ht hs ih =>
+  case sub hs ih =>
     have ih := ih he
     have ⟨Cf, F, E0, hx, he0, hs0⟩ := ih
     have h := ESubtyp.trans hs0 hs
@@ -62,7 +65,7 @@ theorem Typed.tapp_inv'
 theorem Typed.tapp_inv
   (h : Typed Γ (Term.tapp x X) E Ct) :
   ∃ Cf F E0,
-    Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.tforall (SType.tvar X) F))) {x=x}
+    Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.tforall (SType.tvar X) F))) {}
     ∧ E0 = F.topen X
     ∧ ESubtyp Γ E0 E :=
   Typed.tapp_inv' rfl h
@@ -180,7 +183,7 @@ theorem Typed.capp_inv'
   (he : t0 = Term.capp x c)
   (h : Typed Γ t0 E Ct0) :
   ∃ Cf F E0,
-    Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.cforall F))) {x=x} ∧
+    Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.cforall F))) {} ∧
     E0 = F.copen c ∧
     ESubtyp Γ E0 E := by
   induction h <;> try (solve | cases he)
@@ -188,7 +191,7 @@ theorem Typed.capp_inv'
     cases he
     repeat (apply Exists.intro)
     apply And.intro
-    { trivial }
+    { apply Typed.precise_cv; trivial }
     apply And.intro
     { trivial }
     { apply ESubtyp.refl }
@@ -201,7 +204,7 @@ theorem Typed.capp_inv'
 theorem Typed.capp_inv
   (h : Typed Γ (Term.capp x c) E Ct0) :
   ∃ Cf F E0,
-    Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.cforall F))) {x=x} ∧
+    Typed Γ (Term.var x) (EType.type (CType.capt Cf (SType.cforall F))) {} ∧
     E0 = F.copen c ∧
     ESubtyp Γ E0 E :=
   Typed.capp_inv' rfl h
@@ -216,7 +219,7 @@ theorem Typed.unbox_inv'
   case unbox =>
     cases he
     apply Exists.intro
-    constructor; trivial
+    constructor; apply Typed.precise_cv; trivial
     apply ESubtyp.refl
   case sub hs ih =>
     have ih1 := ih he
@@ -411,11 +414,11 @@ theorem Typed.canonical_form_pack'
   (he1 : t0 = Term.pack C x)
   (he2 : E0 = EType.ex T)
   (h : Typed Γ t0 E0 Ct) :
-  Typed (Γ.cvar (CBinding.inst C)) (Term.var x) (EType.type T) {x=x} := by
+  Typed (Γ.cvar (CBinding.inst C)) (Term.var x) (EType.type T) {} := by
   induction h <;> try (solve | cases he1 | cases he2)
   case pack =>
     cases he1; cases he2
-    trivial
+    apply Typed.precise_cv; trivial
   case sub hs ih =>
     subst he2
     cases hs
@@ -430,7 +433,7 @@ theorem Typed.canonical_form_pack'
 theorem Typed.canonical_form_pack
   (ht : Γ.IsTight)
   (h : Typed Γ (Term.pack C x) (EType.ex T) Ct) :
-  Typed (Γ.cvar (CBinding.inst C)) (Term.var x) (EType.type T) {x=x} :=
+  Typed (Γ.cvar (CBinding.inst C)) (Term.var x) (EType.type T) {} :=
   Typed.canonical_form_pack' ht rfl rfl h
 
 theorem Typed.forall_inv' {v : Term n m k}
diff --git a/Capless/Renaming/Capture/Typing.lean b/Capless/Renaming/Capture/Typing.lean
index d92f73cd..8eb6cc34 100644
--- a/Capless/Renaming/Capture/Typing.lean
+++ b/Capless/Renaming/Capture/Typing.lean
@@ -20,6 +20,7 @@ theorem Typed.crename
     apply pack
     have ih := ih (ρ.cext _)
     simp [Term.crename, EType.crename] at ih
+    rw [CaptureSet.cweaken_crename]
     exact ih
   case sub hsc hsub ih =>
     apply sub
diff --git a/Capless/Renaming/Term/Typing.lean b/Capless/Renaming/Term/Typing.lean
index 53f78769..7c78005e 100644
--- a/Capless/Renaming/Term/Typing.lean
+++ b/Capless/Renaming/Term/Typing.lean
@@ -20,6 +20,7 @@ theorem Typed.rename
     apply Typed.pack
     have ih := ih (ρ.cext _)
     simp [Term.rename, EType.rename] at ih
+    rw [<- CaptureSet.cweaken_rename_comm]
     exact ih
   case sub hsc hs ih =>
     apply Typed.sub
@@ -30,7 +31,6 @@ theorem Typed.rename
     simp [Term.rename, EType.rename, CType.rename, SType.rename]
     apply Typed.abs
     rw [CaptureSet.weaken_rename]
-    rw [<- CaptureSet.ext_rename_singleton_zero (f := f)]
     apply? iht
     apply ρ.ext
   case tabs iht =>
diff --git a/Capless/Soundness/Preservation.lean b/Capless/Soundness/Preservation.lean
index c0859b90..d98ff0ed 100644
--- a/Capless/Soundness/Preservation.lean
+++ b/Capless/Soundness/Preservation.lean
@@ -40,13 +40,13 @@ theorem preservation
       have ⟨hcfs, C0, hcft⟩ := Typed.canonical_form_lam hg hv
       constructor
       constructor
-      { trivial }
+      { exact hs }
       { apply Typed.sub
         { apply Typed.open (h := hcft)
           exact hy }
         { apply Subcapt.refl }
         { subst he1
-          trivial } }
+          exact hs1 } }
       trivial
   case tapply hl =>
     cases ht
@@ -73,7 +73,7 @@ theorem preservation
       have ⟨C0, hct⟩ := Typed.canonical_form_clam hg hv
       constructor
       constructor
-      { trivial }
+      { exact hs }
       { apply Typed.sub
         { apply Typed.copen hct }
         { apply Subcapt.refl }
@@ -89,7 +89,7 @@ theorem preservation
       have hct := Typed.canonical_form_boxed hg hv
       constructor
       constructor
-      { trivial }
+      { exact hs }
       { apply Typed.sub
         exact hct
         apply Subcapt.refl
@@ -101,7 +101,7 @@ theorem preservation
       have ⟨T, E0, C0, htt, htu, hsub⟩ := Typed.letin_inv ht
       constructor
       constructor
-      { trivial }
+      { exact hs }
       { exact htt }
       { constructor
         apply? Typed.sub
@@ -179,8 +179,8 @@ theorem preservation
       have ⟨E0, C0, ht, hsub⟩ := Typed.bindc_inv ht
       constructor
       { constructor; exact hs }
-      { apply Typed.sub
-        exact ht; apply Subcapt.refl
+      { apply Typed.ssub
+        exact ht
         apply ESubtyp.cweaken; exact hsub }
       { apply TypedCont.cweaken; exact hc }
 
diff --git a/Capless/Soundness/Progress.lean b/Capless/Soundness/Progress.lean
index cab3e16a..16c74f24 100644
--- a/Capless/Soundness/Progress.lean
+++ b/Capless/Soundness/Progress.lean
@@ -86,7 +86,7 @@ theorem progress
         apply Reduce.lift
         constructor
     case app =>
-      rename_i x _ _ _ _ hx _ _ _ σ _
+      rename_i x _ _ _ _ _ hx _ _ _ σ _
       have hg := TypedStore.is_tight hs
       have ⟨v0, hb0, hv0⟩ := Store.lookup_exists (σ := σ) (x := x)
       have ⟨Cv, Cv0, htv⟩ := Store.lookup_inv_typing hb0 hs hx
@@ -95,7 +95,7 @@ theorem progress
       apply Progress.step
       apply Reduce.apply
       trivial
-    case tapp x _ _ _ hx _ σ _ =>
+    case tapp x _ _ _ _ hx _ σ _ =>
       have hg := TypedStore.is_tight hs
       have ⟨v0, hb0, hv0⟩ := Store.lookup_exists (σ := σ) (x := x)
       have ⟨Cv, Cv0, htv⟩ := Store.lookup_inv_typing hb0 hs hx
@@ -104,7 +104,7 @@ theorem progress
       apply Progress.step
       apply Reduce.tapply
       trivial
-    case capp x _ _ _ hx _ σ _ =>
+    case capp x _ _ _ _ hx _ σ _ =>
       have hg := TypedStore.is_tight hs
       have ⟨v0, hb0, hv0⟩ := Store.lookup_exists (σ := σ) (x := x)
       have ⟨Cv, Ct0, htv⟩ := Store.lookup_inv_typing hb0 hs hx
@@ -120,7 +120,7 @@ theorem progress
         apply Progress.step
         apply Reduce.lift
         constructor
-    case unbox x _ _ hx _ σ _ =>
+    case unbox x _ _ _ hx _ σ _ =>
       have hg := TypedStore.is_tight hs
       have ⟨v0, hb0, hv0⟩ := Store.lookup_exists (σ := σ) (x := x)
       have ⟨Cv, Cv0, htv⟩ := Store.lookup_inv_typing hb0 hs hx
diff --git a/Capless/Subst/Basic.lean b/Capless/Subst/Basic.lean
index a91f4929..a1e3faa1 100644
--- a/Capless/Subst/Basic.lean
+++ b/Capless/Subst/Basic.lean
@@ -10,7 +10,7 @@ import Capless.Inversion.Context
 namespace Capless
 
 structure VarSubst (Γ : Context n m k) (f : FinFun n n') (Δ : Context n' m k) where
-  map : ∀ x E, Γ.Bound x E -> Typed Δ (Term.var (f x)) (EType.type (E.rename f)) {x=f x}
+  map : ∀ x E, Γ.Bound x E -> Typed Δ (Term.var (f x)) (EType.type (E.rename f)) {}
   tmap : ∀ X b, Γ.TBound X b -> Δ.TBound X (b.rename f)
   cmap : ∀ c b, Γ.CBound c b -> Δ.CBound c (b.rename f)
 
diff --git a/Capless/Subst/Capture/Typing.lean b/Capless/Subst/Capture/Typing.lean
index d666241e..24112077 100644
--- a/Capless/Subst/Capture/Typing.lean
+++ b/Capless/Subst/Capture/Typing.lean
@@ -19,6 +19,7 @@ theorem Typed.csubst
       apply pack
       have ih := ih σ.cext
       simp [EType.crename] at ih
+      rw [CaptureSet.cweaken_crename]
       exact ih
     case sub hsc hs ih =>
       apply sub
@@ -31,12 +32,12 @@ theorem Typed.csubst
       { rw [CaptureSet.weaken_crename]
         apply ih
         apply σ.ext }
-    case tabs hc ih =>
+    case tabs ih =>
       simp [Term.crename, EType.crename, CType.crename, SType.crename]
       apply tabs
       { apply ih
         apply σ.text }
-    case cabs hc ih =>
+    case cabs ih =>
       simp [Term.crename, EType.crename, CType.crename, SType.crename]
       apply cabs
       { rw [CaptureSet.cweaken_crename]
diff --git a/Capless/Subst/Term/Typing.lean b/Capless/Subst/Term/Typing.lean
index 2bf46ed8..eb9a9113 100644
--- a/Capless/Subst/Term/Typing.lean
+++ b/Capless/Subst/Term/Typing.lean
@@ -21,6 +21,7 @@ theorem Typed.subst
     apply pack
     have ih := ih σ.cext
     simp [EType.rename] at ih
+    rw [<- CaptureSet.cweaken_rename_comm]
     exact ih
   case sub hsc hs ih =>
     apply sub
@@ -31,7 +32,6 @@ theorem Typed.subst
     simp [Term.rename, EType.rename, CType.rename, SType.rename]
     apply abs
     { rw [CaptureSet.weaken_rename]
-      rw [<- CaptureSet.ext_rename_singleton_zero (f := f)]
       apply ih
       apply σ.ext }
   case tabs hc ih =>
diff --git a/Capless/Typing/Basic.lean b/Capless/Typing/Basic.lean
index 8ae4e08c..a6e920d5 100644
--- a/Capless/Typing/Basic.lean
+++ b/Capless/Typing/Basic.lean
@@ -27,7 +27,7 @@ theorem Typing.inv_subcapt
 
 theorem Typed.bound_typing
   (hb : Context.Bound Γ x T) :
-  Typed Γ (Term.var x) (EType.type T) {x=x} := by
+  Typed Γ (Term.var x) (EType.type T) {} := by
   cases T
   apply Typed.sub
   apply Typed.var hb
@@ -41,7 +41,7 @@ theorem Typed.precise_capture'
   (he1 : t0 = Term.var x)
   (he2 : E0 = EType.type (CType.capt C S))
   (h : Typed Γ t0 E0 C0) :
-  Typed Γ (Term.var x) (EType.type (CType.capt {x=x} S)) {x=x} := by
+  Typed Γ (Term.var x) (EType.type (CType.capt {x=x} S)) {} := by
   induction h <;> try (solve | cases he1 | cases he2)
   case var => cases he1; cases he2; apply Typed.var; trivial
   case sub hsub ih =>
@@ -61,13 +61,13 @@ theorem Typed.precise_capture'
 
 theorem Typed.precise_capture
   (h : Typed Γ (Term.var x) (EType.type (CType.capt C S)) C0) :
-  Typed Γ (Term.var x) (EType.type (CType.capt {x=x} S)) {x=x} :=
+  Typed Γ (Term.var x) (EType.type (CType.capt {x=x} S)) {} :=
   Typed.precise_capture' rfl rfl h
 
 theorem Typed.precise_cv'
   (he : t0 = Term.var x)
   (h : Typed Γ t0 E C0) :
-  Typed Γ (Term.var x) E {x=x} := by
+  Typed Γ (Term.var x) E {} := by
   induction h <;> try (solve | cases he)
   case var => cases he; apply Typed.var; trivial
   case sub ih =>
@@ -78,7 +78,16 @@ theorem Typed.precise_cv'
 
 theorem Typed.precise_cv
   (h : Typed Γ (Term.var x) E C0) :
-  Typed Γ (Term.var x) E {x=x} :=
+  Typed Γ (Term.var x) E {} :=
   Typed.precise_cv' rfl h
 
+theorem Typed.ssub
+  (h : Γ[C] ⊢ t : E)
+  (hsub : Γ ⊢ E <:e E') :
+  Γ[C] ⊢ t : E' := by
+  apply Typed.sub
+  exact h
+  apply Subcapt.refl
+  exact hsub
+
 end Capless