From 783dff0095c2f372b4f838f8a55c4e47a657746b Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Wed, 23 Oct 2024 23:29:24 +0200
Subject: [PATCH 01/42] add the cappy library

---
 lakefile.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/lakefile.lean b/lakefile.lean
index a307e98d..b128391f 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -14,3 +14,5 @@ require mathlib from git
 @[default_target]
 lean_lib «Capless» where
   -- add any library configuration options here
+
+lean_lib «Cappy» where

From 549e1097d183192822645462cf35a467f7c9695b Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Wed, 23 Oct 2024 23:29:34 +0200
Subject: [PATCH 02/42] add some basic definitions for cappy

---
 Cappy.lean             |   1 +
 Cappy/CaptureSet.lean  |  51 ++++++++++++++++++
 Cappy/Definitions.lean | 120 +++++++++++++++++++++++++++++++++++++++++
 3 files changed, 172 insertions(+)
 create mode 100644 Cappy.lean
 create mode 100644 Cappy/CaptureSet.lean
 create mode 100644 Cappy/Definitions.lean

diff --git a/Cappy.lean b/Cappy.lean
new file mode 100644
index 00000000..a8da9e27
--- /dev/null
+++ b/Cappy.lean
@@ -0,0 +1 @@
+import Cappy.Definitions
diff --git a/Cappy/CaptureSet.lean b/Cappy/CaptureSet.lean
new file mode 100644
index 00000000..b0da5a2b
--- /dev/null
+++ b/Cappy/CaptureSet.lean
@@ -0,0 +1,51 @@
+import Capless.Tactics
+import Capless.Basic
+import Mathlib.Data.Fin.Basic
+namespace Cappy
+
+inductive CaptureSet : Nat -> Type where
+| empty : CaptureSet n
+| union : CaptureSet n -> CaptureSet n -> CaptureSet n
+| singleton : Fin n -> CaptureSet n
+| reach : Fin n -> CaptureSet n
+| universal : CaptureSet n
+
+@[simp]
+instance : EmptyCollection (CaptureSet n) where
+  emptyCollection := CaptureSet.empty
+
+notation:max "{x=" x "}" => CaptureSet.singleton x
+notation:max "{x*=" c "}" => CaptureSet.reach c
+notation:max "{cap}" => CaptureSet.universal
+
+@[simp]
+instance : Union (CaptureSet n) where
+  union := CaptureSet.union
+
+inductive CaptureSet.Subset : CaptureSet n -> CaptureSet n -> Prop where
+| empty : Subset {} C
+| rfl : Subset C C
+| union_l :
+  Subset C1 C ->
+  Subset C2 C ->
+  Subset (C1 ∪ C2) C
+| union_rl :
+  Subset C C1 ->
+  Subset C (C1 ∪ C2)
+| union_rr :
+  Subset C C2 ->
+  Subset C (C1 ∪ C2)
+
+@[simp]
+instance : HasSubset (CaptureSet n) where
+  Subset := CaptureSet.Subset
+
+def CaptureSet.rename (C : CaptureSet n) (f : Capless.FinFun n n') : CaptureSet n' :=
+  match C with
+  | empty => {}
+  | union C1 C2 => (C1.rename f) ∪ (C2.rename f)
+  | singleton x => {x=(f x)}
+  | reach x => {x*=(f x)}
+  | universal => {cap}
+
+end Cappy
diff --git a/Cappy/Definitions.lean b/Cappy/Definitions.lean
new file mode 100644
index 00000000..2008332a
--- /dev/null
+++ b/Cappy/Definitions.lean
@@ -0,0 +1,120 @@
+import Capless.Tactics
+import Capless.Basic
+import Mathlib.Data.Fin.Basic
+import Cappy.CaptureSet
+namespace Cappy
+
+inductive Annot : Type where
+| eps : Annot
+| use : Annot
+
+structure RenameFun (n m n' m' : Nat) where
+  map : Capless.FinFun n n'
+  tmap : Capless.FinFun m m'
+
+def RenameFun.ext (f : RenameFun n m n' m') : RenameFun (n+1) m (n'+1) m' :=
+  { map := f.map.ext, tmap := f.tmap }
+
+def RenameFun.text (f : RenameFun n m n' m') : RenameFun n (m+1) n' (m'+1) :=
+  { map := f.map, tmap := f.tmap.ext }
+
+def RenameFun.weaken : RenameFun n m (n+1) m :=
+  { map := Capless.FinFun.weaken, tmap := Capless.FinFun.id }
+
+def RenameFun.tweaken : RenameFun n m n (m+1) :=
+  { map := Capless.FinFun.id, tmap := Capless.FinFun.weaken }
+
+mutual
+
+inductive CType : Nat -> Nat -> Type where
+| capt : CaptureSet n -> SType n m -> CType n m
+
+inductive SType : Nat -> Nat -> Type where
+| top : SType n m
+| tvar : Fin m -> SType n m
+| arrow : Annot -> CType n m -> CType (n+1) m -> SType n m
+| tarrow : SType n m -> CType n (m+1) -> SType n m
+| boxed : CType n m -> SType n m
+
+end
+
+notation:max S "^" C => CType.capt C S
+
+mutual
+
+def CType.rename : CType n m -> RenameFun n m n' m' -> CType n' m'
+| CType.capt C S, f => (S.rename f)^(C.rename f.map)
+
+def SType.rename : SType n m -> RenameFun n m n' m' -> SType n' m'
+| SType.top, _ => SType.top
+| SType.tvar x, f => SType.tvar (f.tmap x)
+| SType.arrow a T U, f => SType.arrow a (T.rename f) (U.rename f.ext)
+| SType.tarrow S T, f => SType.tarrow (S.rename f) (T.rename f.text)
+| SType.boxed C, f => SType.boxed (C.rename f)
+
+end
+
+def CType.weaken (T : CType n m) : CType (n+1) m :=
+  T.rename RenameFun.weaken
+
+def SType.weaken (T : SType n m) : SType (n+1) m :=
+  T.rename RenameFun.weaken
+
+def CType.tweaken (T : CType n m) : CType n (m+1) :=
+  T.rename RenameFun.tweaken
+
+def SType.tweaken (T : SType n m) : SType n (m+1) :=
+  T.rename RenameFun.tweaken
+
+inductive Term : Nat -> Nat -> Type where
+| var : Fin n -> Term n m
+| abs : Annot -> CType n m -> Term (n+1) m -> Term n m
+| app : Fin n -> Fin n -> Term n m
+| tabs : SType n m -> Term n (m+1) -> Term n m
+| tapp : Fin m -> SType n m -> Term n m
+| box : Fin n -> Term n m
+| unbox : CaptureSet n -> Fin n -> Term n m
+| letin : Term n m -> Term (n+1) m -> Term n m
+
+inductive Context : Nat -> Nat -> Type where
+| empty : Context 0 0
+| var : Context n m -> CType n m -> Context (n+1) m
+| tvar : Context n m -> SType n m -> Context n (m+1)
+
+inductive Context.Bound : Context n m -> Fin n -> CType n m -> Prop where
+| here :
+  Context.Bound (Context.var Γ T) 0 T.weaken
+| there_var :
+  Context.Bound Γ x T ->
+  Context.Bound (Context.var Γ T') x.succ T.weaken
+| there_tvar :
+  Context.Bound Γ x T ->
+  Context.Bound (Context.tvar Γ S) x T.tweaken
+
+inductive Context.TBound : Context n m -> Fin m -> SType n m -> Prop where
+| here :
+  Context.TBound (Context.tvar Γ S) 0 S.tweaken
+| there_var :
+  Context.TBound Γ x S ->
+  Context.TBound (Context.var Γ T) x S.weaken
+| there_tvar :
+  Context.TBound Γ x S ->
+  Context.TBound (Context.tvar Γ S') x.succ S.tweaken
+
+inductive Subcapt : Context n m -> CaptureSet n -> CaptureSet n -> Prop where
+| sc_trans :
+  Subcapt Γ C1 C2 ->
+  Subcapt Γ C2 C3 ->
+  Subcapt Γ C1 C3
+| sc_var :
+  Context.Bound Γ x (S^C) ->
+  Subcapt Γ {x=x} C
+| sc_elem {C1 C2 : CaptureSet n} :
+  C1 ⊆ C2 ->
+  Subcapt Γ C1 C2
+| sc_set :
+  Subcapt Γ C1 C ->
+  Subcapt Γ C2 C ->
+  Subcapt Γ (C1 ∪ C2) C
+
+end Cappy

From a8ca8fa9a4c16356cdc9ec0827d18ee93d578129 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Wed, 23 Oct 2024 23:39:03 +0200
Subject: [PATCH 03/42] add subtyping

---
 Cappy/Definitions.lean | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/Cappy/Definitions.lean b/Cappy/Definitions.lean
index 2008332a..2dd93c42 100644
--- a/Cappy/Definitions.lean
+++ b/Cappy/Definitions.lean
@@ -39,6 +39,9 @@ inductive SType : Nat -> Nat -> Type where
 end
 
 notation:max S "^" C => CType.capt C S
+notation:50 "∀(x:" T ")" U => SType.arrow Annot.eps T U
+notation:50 "∀(use x:" T ")" U => SType.arrow Annot.use T U
+notation:50 "∀[X<:" S "]" T => SType.tarrow S T
 
 mutual
 
@@ -117,4 +120,41 @@ inductive Subcapt : Context n m -> CaptureSet n -> CaptureSet n -> Prop where
   Subcapt Γ C2 C ->
   Subcapt Γ (C1 ∪ C2) C
 
+mutual
+
+inductive CSubtyp : Context n m -> CType n m -> CType n m -> Prop where
+| capt :
+  Subcapt Γ C1 C2 ->
+  SSubtyp Γ S1 S2 ->
+  CSubtyp Γ (S1^C1) (S2^C2)
+
+inductive SSubtyp : Context n m -> SType n m -> SType n m -> Prop where
+| top :
+  SSubtyp Γ S SType.top
+| refl :
+  SSubtyp Γ S S
+| trans :
+  SSubtyp Γ S1 S2 ->
+  SSubtyp Γ S2 S3 ->
+  SSubtyp Γ S1 S3
+| tvar :
+  Context.TBound Γ X S ->
+  SSubtyp Γ (SType.tvar X) S
+| boxed :
+  CSubtyp Γ T1 T2 ->
+  SSubtyp Γ (SType.boxed T1) (SType.boxed T2)
+| arrow :
+  CSubtyp Γ T2 T1 ->
+  CSubtyp (Γ.var T2) U1 U2 ->
+  SSubtyp Γ (∀(x:T1)U1) (SType.arrow a T2 U2)
+| uarrow :
+  CSubtyp (Γ.var T) U1 U2 ->
+  SSubtyp Γ (∀(use x:T)U1) (∀(use x:T)U2)
+| tarrow :
+  SSubtyp Γ S2 S1 ->
+  CSubtyp (Γ.tvar S2) T1 T2 ->
+  SSubtyp Γ (∀[X<:S1]T1) (∀[X<:S2]T2)
+
+end
+
 end Cappy

From 5d02d8db151610d5411fc3971a99ebbd5923f07f Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 24 Oct 2024 05:55:22 +0200
Subject: [PATCH 04/42] setup cap refine

---
 Cappy/CaptureSet.lean  | 15 +++++++++++++++
 Cappy/Definitions.lean |  2 ++
 2 files changed, 17 insertions(+)

diff --git a/Cappy/CaptureSet.lean b/Cappy/CaptureSet.lean
index b0da5a2b..a5bc16be 100644
--- a/Cappy/CaptureSet.lean
+++ b/Cappy/CaptureSet.lean
@@ -48,4 +48,19 @@ def CaptureSet.rename (C : CaptureSet n) (f : Capless.FinFun n n') : CaptureSet
   | reach x => {x*=(f x)}
   | universal => {cap}
 
+def CaptureSet.weaken (C : CaptureSet n) : CaptureSet (n+1) :=
+  C.rename Capless.FinFun.weaken
+
+structure CapSubst (n n' : Nat) where
+  map : Fin n -> CaptureSet n'
+  rmap : Fin n -> CaptureSet n'
+  capmap : CaptureSet n'
+
+def CaptureSet.subst : CaptureSet n -> CapSubst n n' -> CaptureSet n'
+| empty, _ => {}
+| union C1 C2, σ => (C1.subst σ) ∪ (C2.subst σ)
+| singleton x, σ => (σ.map x)
+| reach x, σ => (σ.rmap x)
+| universal, σ => σ.capmap
+
 end Cappy
diff --git a/Cappy/Definitions.lean b/Cappy/Definitions.lean
index 2dd93c42..452c57d7 100644
--- a/Cappy/Definitions.lean
+++ b/Cappy/Definitions.lean
@@ -157,4 +157,6 @@ inductive SSubtyp : Context n m -> SType n m -> SType n m -> Prop where
 
 end
 
+inductive CapRefine : CaptureSet n -> CType n m -> CType n m -> Prop where
+
 end Cappy

From d555e8df263672ae9ec7498ff030c45a59316867 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 24 Oct 2024 06:54:54 +0200
Subject: [PATCH 05/42] finish cap refine

---
 Cappy/CaptureSet.lean  |  6 ++++++
 Cappy/Definitions.lean | 24 +++++++++++++++++++++++-
 2 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/Cappy/CaptureSet.lean b/Cappy/CaptureSet.lean
index a5bc16be..61915ab0 100644
--- a/Cappy/CaptureSet.lean
+++ b/Cappy/CaptureSet.lean
@@ -63,4 +63,10 @@ def CaptureSet.subst : CaptureSet n -> CapSubst n n' -> CaptureSet n'
 | reach x, σ => (σ.rmap x)
 | universal, σ => σ.capmap
 
+def CapSubst.open_cap (D : CaptureSet n) : CapSubst n n :=
+  { map := λ x => {x=x}, rmap := λ x => {x*=x}, capmap := D }
+
+def CaptureSet.open_cap (C : CaptureSet n) (D : CaptureSet n) : CaptureSet n :=
+  C.subst (CapSubst.open_cap D)
+
 end Cappy
diff --git a/Cappy/Definitions.lean b/Cappy/Definitions.lean
index 452c57d7..b69b9fec 100644
--- a/Cappy/Definitions.lean
+++ b/Cappy/Definitions.lean
@@ -157,6 +157,28 @@ inductive SSubtyp : Context n m -> SType n m -> SType n m -> Prop where
 
 end
 
-inductive CapRefine : CaptureSet n -> CType n m -> CType n m -> Prop where
+mutual
+
+inductive CType.CapRefine : CaptureSet n -> CType n m -> CType n m -> Prop where
+| r_capt :
+  SType.CapRefine D S S' ->
+  CType.CapRefine D (S^C) (S'^(C.open_cap D))
+
+inductive SType.CapRefine : CaptureSet n -> SType n m -> SType n m -> Prop where
+| r_top :
+  SType.CapRefine D top top
+| r_tvar :
+  SType.CapRefine D (SType.tvar X) (SType.tvar X)
+| r_fun :
+  CType.CapRefine (D.weaken ∪ {x=0} ∪ {x*=0}) U U' ->
+  SType.CapRefine D (SType.arrow a T U) (SType.arrow a T U')
+| r_tfun :
+  CType.CapRefine D T T' ->
+  SType.CapRefine D (SType.tarrow S T) (SType.tarrow S T')
+| r_boxed :
+  CType.CapRefine D T T' ->
+  SType.CapRefine D (SType.boxed T) (SType.boxed T')
+
+end
 
 end Cappy

From 8be16e435ae0ab14efd224c545377f5678f8fa6e Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 24 Oct 2024 07:07:13 +0200
Subject: [PATCH 06/42] add typing judgement

---
 Cappy/Definitions.lean | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/Cappy/Definitions.lean b/Cappy/Definitions.lean
index b69b9fec..e59d5d0d 100644
--- a/Cappy/Definitions.lean
+++ b/Cappy/Definitions.lean
@@ -181,4 +181,34 @@ inductive SType.CapRefine : CaptureSet n -> SType n m -> SType n m -> Prop where
 
 end
 
+inductive Typed : CaptureSet n -> Context n m -> Term n m -> CType n m -> Prop where
+| var :
+  Γ.Bound x (S^C) ->
+  S.CapRefine {x*=x} S' ->
+  Typed {x=x} Γ (Term.var x) (S'^{x=x})
+| sub :
+  Typed C Γ t T ->
+  Subcapt Γ C C' ->
+  CSubtyp Γ T T' ->
+  Typed C' Γ t T'
+| abs {C : CaptureSet n} :
+  Typed (C.weaken ∪ {x=0} ∪ {x*=0}) (Γ.var T) t U ->
+  Typed {} Γ (Term.abs Annot.eps T t) ((∀(x:T)U)^C)
+| uabs {C : CaptureSet n} :
+  Typed (C.weaken ∪ {x=0}) (Γ.var T) t U ->
+  Typed {} Γ (Term.abs Annot.use T t) ((∀(use x:T)U)^C)
+| tabs {C : CaptureSet n} :
+  Typed C (Γ.tvar S) t T ->
+  Typed {} Γ (Term.tabs S t) ((∀[X<:S]T)^C)
+| box {C : CaptureSet n} :
+  Typed C Γ (Term.var x) T ->
+  Typed {} Γ (Term.box x) ((SType.boxed T)^{})
+| unbox {C : CaptureSet n} :
+  Typed C Γ (Term.var x) ((SType.boxed (S^C))^{}) ->
+  Typed C Γ (Term.unbox C x) (S^C)
+| letin {C : CaptureSet n} {U : CType n m} :
+  Typed C Γ t T ->
+  Typed C.weaken (Γ.var T) u U.weaken ->
+  Typed C Γ (Term.letin t u) U
+
 end Cappy

From 6204d9fb7495307bce8cfbff126d4f815c458180 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 24 Oct 2024 08:35:36 +0200
Subject: [PATCH 07/42] modularise the proof

---
 Cappy/Definitions.lean             | 215 +----------------------------
 Cappy/Renaming.lean                |  22 +++
 Cappy/{ => Syntax}/CaptureSet.lean |   0
 Cappy/Syntax/Context.lean          |  29 ++++
 Cappy/Syntax/Term.lean             |  14 ++
 Cappy/Syntax/Type.lean             |  55 ++++++++
 Cappy/TypeSystem/Subcapturing.lean |  21 +++
 Cappy/TypeSystem/Subtyping.lean    |  42 ++++++
 Cappy/TypeSystem/Typing.lean       |  59 ++++++++
 9 files changed, 243 insertions(+), 214 deletions(-)
 create mode 100644 Cappy/Renaming.lean
 rename Cappy/{ => Syntax}/CaptureSet.lean (100%)
 create mode 100644 Cappy/Syntax/Context.lean
 create mode 100644 Cappy/Syntax/Term.lean
 create mode 100644 Cappy/Syntax/Type.lean
 create mode 100644 Cappy/TypeSystem/Subcapturing.lean
 create mode 100644 Cappy/TypeSystem/Subtyping.lean
 create mode 100644 Cappy/TypeSystem/Typing.lean

diff --git a/Cappy/Definitions.lean b/Cappy/Definitions.lean
index e59d5d0d..e13163ad 100644
--- a/Cappy/Definitions.lean
+++ b/Cappy/Definitions.lean
@@ -1,214 +1 @@
-import Capless.Tactics
-import Capless.Basic
-import Mathlib.Data.Fin.Basic
-import Cappy.CaptureSet
-namespace Cappy
-
-inductive Annot : Type where
-| eps : Annot
-| use : Annot
-
-structure RenameFun (n m n' m' : Nat) where
-  map : Capless.FinFun n n'
-  tmap : Capless.FinFun m m'
-
-def RenameFun.ext (f : RenameFun n m n' m') : RenameFun (n+1) m (n'+1) m' :=
-  { map := f.map.ext, tmap := f.tmap }
-
-def RenameFun.text (f : RenameFun n m n' m') : RenameFun n (m+1) n' (m'+1) :=
-  { map := f.map, tmap := f.tmap.ext }
-
-def RenameFun.weaken : RenameFun n m (n+1) m :=
-  { map := Capless.FinFun.weaken, tmap := Capless.FinFun.id }
-
-def RenameFun.tweaken : RenameFun n m n (m+1) :=
-  { map := Capless.FinFun.id, tmap := Capless.FinFun.weaken }
-
-mutual
-
-inductive CType : Nat -> Nat -> Type where
-| capt : CaptureSet n -> SType n m -> CType n m
-
-inductive SType : Nat -> Nat -> Type where
-| top : SType n m
-| tvar : Fin m -> SType n m
-| arrow : Annot -> CType n m -> CType (n+1) m -> SType n m
-| tarrow : SType n m -> CType n (m+1) -> SType n m
-| boxed : CType n m -> SType n m
-
-end
-
-notation:max S "^" C => CType.capt C S
-notation:50 "∀(x:" T ")" U => SType.arrow Annot.eps T U
-notation:50 "∀(use x:" T ")" U => SType.arrow Annot.use T U
-notation:50 "∀[X<:" S "]" T => SType.tarrow S T
-
-mutual
-
-def CType.rename : CType n m -> RenameFun n m n' m' -> CType n' m'
-| CType.capt C S, f => (S.rename f)^(C.rename f.map)
-
-def SType.rename : SType n m -> RenameFun n m n' m' -> SType n' m'
-| SType.top, _ => SType.top
-| SType.tvar x, f => SType.tvar (f.tmap x)
-| SType.arrow a T U, f => SType.arrow a (T.rename f) (U.rename f.ext)
-| SType.tarrow S T, f => SType.tarrow (S.rename f) (T.rename f.text)
-| SType.boxed C, f => SType.boxed (C.rename f)
-
-end
-
-def CType.weaken (T : CType n m) : CType (n+1) m :=
-  T.rename RenameFun.weaken
-
-def SType.weaken (T : SType n m) : SType (n+1) m :=
-  T.rename RenameFun.weaken
-
-def CType.tweaken (T : CType n m) : CType n (m+1) :=
-  T.rename RenameFun.tweaken
-
-def SType.tweaken (T : SType n m) : SType n (m+1) :=
-  T.rename RenameFun.tweaken
-
-inductive Term : Nat -> Nat -> Type where
-| var : Fin n -> Term n m
-| abs : Annot -> CType n m -> Term (n+1) m -> Term n m
-| app : Fin n -> Fin n -> Term n m
-| tabs : SType n m -> Term n (m+1) -> Term n m
-| tapp : Fin m -> SType n m -> Term n m
-| box : Fin n -> Term n m
-| unbox : CaptureSet n -> Fin n -> Term n m
-| letin : Term n m -> Term (n+1) m -> Term n m
-
-inductive Context : Nat -> Nat -> Type where
-| empty : Context 0 0
-| var : Context n m -> CType n m -> Context (n+1) m
-| tvar : Context n m -> SType n m -> Context n (m+1)
-
-inductive Context.Bound : Context n m -> Fin n -> CType n m -> Prop where
-| here :
-  Context.Bound (Context.var Γ T) 0 T.weaken
-| there_var :
-  Context.Bound Γ x T ->
-  Context.Bound (Context.var Γ T') x.succ T.weaken
-| there_tvar :
-  Context.Bound Γ x T ->
-  Context.Bound (Context.tvar Γ S) x T.tweaken
-
-inductive Context.TBound : Context n m -> Fin m -> SType n m -> Prop where
-| here :
-  Context.TBound (Context.tvar Γ S) 0 S.tweaken
-| there_var :
-  Context.TBound Γ x S ->
-  Context.TBound (Context.var Γ T) x S.weaken
-| there_tvar :
-  Context.TBound Γ x S ->
-  Context.TBound (Context.tvar Γ S') x.succ S.tweaken
-
-inductive Subcapt : Context n m -> CaptureSet n -> CaptureSet n -> Prop where
-| sc_trans :
-  Subcapt Γ C1 C2 ->
-  Subcapt Γ C2 C3 ->
-  Subcapt Γ C1 C3
-| sc_var :
-  Context.Bound Γ x (S^C) ->
-  Subcapt Γ {x=x} C
-| sc_elem {C1 C2 : CaptureSet n} :
-  C1 ⊆ C2 ->
-  Subcapt Γ C1 C2
-| sc_set :
-  Subcapt Γ C1 C ->
-  Subcapt Γ C2 C ->
-  Subcapt Γ (C1 ∪ C2) C
-
-mutual
-
-inductive CSubtyp : Context n m -> CType n m -> CType n m -> Prop where
-| capt :
-  Subcapt Γ C1 C2 ->
-  SSubtyp Γ S1 S2 ->
-  CSubtyp Γ (S1^C1) (S2^C2)
-
-inductive SSubtyp : Context n m -> SType n m -> SType n m -> Prop where
-| top :
-  SSubtyp Γ S SType.top
-| refl :
-  SSubtyp Γ S S
-| trans :
-  SSubtyp Γ S1 S2 ->
-  SSubtyp Γ S2 S3 ->
-  SSubtyp Γ S1 S3
-| tvar :
-  Context.TBound Γ X S ->
-  SSubtyp Γ (SType.tvar X) S
-| boxed :
-  CSubtyp Γ T1 T2 ->
-  SSubtyp Γ (SType.boxed T1) (SType.boxed T2)
-| arrow :
-  CSubtyp Γ T2 T1 ->
-  CSubtyp (Γ.var T2) U1 U2 ->
-  SSubtyp Γ (∀(x:T1)U1) (SType.arrow a T2 U2)
-| uarrow :
-  CSubtyp (Γ.var T) U1 U2 ->
-  SSubtyp Γ (∀(use x:T)U1) (∀(use x:T)U2)
-| tarrow :
-  SSubtyp Γ S2 S1 ->
-  CSubtyp (Γ.tvar S2) T1 T2 ->
-  SSubtyp Γ (∀[X<:S1]T1) (∀[X<:S2]T2)
-
-end
-
-mutual
-
-inductive CType.CapRefine : CaptureSet n -> CType n m -> CType n m -> Prop where
-| r_capt :
-  SType.CapRefine D S S' ->
-  CType.CapRefine D (S^C) (S'^(C.open_cap D))
-
-inductive SType.CapRefine : CaptureSet n -> SType n m -> SType n m -> Prop where
-| r_top :
-  SType.CapRefine D top top
-| r_tvar :
-  SType.CapRefine D (SType.tvar X) (SType.tvar X)
-| r_fun :
-  CType.CapRefine (D.weaken ∪ {x=0} ∪ {x*=0}) U U' ->
-  SType.CapRefine D (SType.arrow a T U) (SType.arrow a T U')
-| r_tfun :
-  CType.CapRefine D T T' ->
-  SType.CapRefine D (SType.tarrow S T) (SType.tarrow S T')
-| r_boxed :
-  CType.CapRefine D T T' ->
-  SType.CapRefine D (SType.boxed T) (SType.boxed T')
-
-end
-
-inductive Typed : CaptureSet n -> Context n m -> Term n m -> CType n m -> Prop where
-| var :
-  Γ.Bound x (S^C) ->
-  S.CapRefine {x*=x} S' ->
-  Typed {x=x} Γ (Term.var x) (S'^{x=x})
-| sub :
-  Typed C Γ t T ->
-  Subcapt Γ C C' ->
-  CSubtyp Γ T T' ->
-  Typed C' Γ t T'
-| abs {C : CaptureSet n} :
-  Typed (C.weaken ∪ {x=0} ∪ {x*=0}) (Γ.var T) t U ->
-  Typed {} Γ (Term.abs Annot.eps T t) ((∀(x:T)U)^C)
-| uabs {C : CaptureSet n} :
-  Typed (C.weaken ∪ {x=0}) (Γ.var T) t U ->
-  Typed {} Γ (Term.abs Annot.use T t) ((∀(use x:T)U)^C)
-| tabs {C : CaptureSet n} :
-  Typed C (Γ.tvar S) t T ->
-  Typed {} Γ (Term.tabs S t) ((∀[X<:S]T)^C)
-| box {C : CaptureSet n} :
-  Typed C Γ (Term.var x) T ->
-  Typed {} Γ (Term.box x) ((SType.boxed T)^{})
-| unbox {C : CaptureSet n} :
-  Typed C Γ (Term.var x) ((SType.boxed (S^C))^{}) ->
-  Typed C Γ (Term.unbox C x) (S^C)
-| letin {C : CaptureSet n} {U : CType n m} :
-  Typed C Γ t T ->
-  Typed C.weaken (Γ.var T) u U.weaken ->
-  Typed C Γ (Term.letin t u) U
-
-end Cappy
+import Cappy.TypeSystem.Typing
diff --git a/Cappy/Renaming.lean b/Cappy/Renaming.lean
new file mode 100644
index 00000000..78ffc6f0
--- /dev/null
+++ b/Cappy/Renaming.lean
@@ -0,0 +1,22 @@
+import Capless.Tactics
+import Capless.Basic
+namespace Cappy
+
+structure RenameFun (n m n' m' : Nat) where
+  map : Capless.FinFun n n'
+  tmap : Capless.FinFun m m'
+
+def RenameFun.ext (f : RenameFun n m n' m') : RenameFun (n+1) m (n'+1) m' :=
+  { map := f.map.ext, tmap := f.tmap }
+
+def RenameFun.text (f : RenameFun n m n' m') : RenameFun n (m+1) n' (m'+1) :=
+  { map := f.map, tmap := f.tmap.ext }
+
+def RenameFun.weaken : RenameFun n m (n+1) m :=
+  { map := Capless.FinFun.weaken, tmap := Capless.FinFun.id }
+
+def RenameFun.tweaken : RenameFun n m n (m+1) :=
+  { map := Capless.FinFun.id, tmap := Capless.FinFun.weaken }
+
+
+end Cappy
diff --git a/Cappy/CaptureSet.lean b/Cappy/Syntax/CaptureSet.lean
similarity index 100%
rename from Cappy/CaptureSet.lean
rename to Cappy/Syntax/CaptureSet.lean
diff --git a/Cappy/Syntax/Context.lean b/Cappy/Syntax/Context.lean
new file mode 100644
index 00000000..8258b9ae
--- /dev/null
+++ b/Cappy/Syntax/Context.lean
@@ -0,0 +1,29 @@
+import Cappy.Syntax.Type
+namespace Cappy
+
+inductive Context : Nat -> Nat -> Type where
+| empty : Context 0 0
+| var : Context n m -> CType n m -> Context (n+1) m
+| tvar : Context n m -> SType n m -> Context n (m+1)
+
+inductive Context.Bound : Context n m -> Fin n -> CType n m -> Prop where
+| here :
+  Context.Bound (Context.var Γ T) 0 T.weaken
+| there_var :
+  Context.Bound Γ x T ->
+  Context.Bound (Context.var Γ T') x.succ T.weaken
+| there_tvar :
+  Context.Bound Γ x T ->
+  Context.Bound (Context.tvar Γ S) x T.tweaken
+
+inductive Context.TBound : Context n m -> Fin m -> SType n m -> Prop where
+| here :
+  Context.TBound (Context.tvar Γ S) 0 S.tweaken
+| there_var :
+  Context.TBound Γ x S ->
+  Context.TBound (Context.var Γ T) x S.weaken
+| there_tvar :
+  Context.TBound Γ x S ->
+  Context.TBound (Context.tvar Γ S') x.succ S.tweaken
+
+end Cappy
diff --git a/Cappy/Syntax/Term.lean b/Cappy/Syntax/Term.lean
new file mode 100644
index 00000000..3f44be93
--- /dev/null
+++ b/Cappy/Syntax/Term.lean
@@ -0,0 +1,14 @@
+import Cappy.Syntax.Type
+namespace Cappy
+
+inductive Term : Nat -> Nat -> Type where
+| var : Fin n -> Term n m
+| abs : Annot -> CType n m -> Term (n+1) m -> Term n m
+| app : Fin n -> Fin n -> Term n m
+| tabs : SType n m -> Term n (m+1) -> Term n m
+| tapp : Fin m -> SType n m -> Term n m
+| box : Fin n -> Term n m
+| unbox : CaptureSet n -> Fin n -> Term n m
+| letin : Term n m -> Term (n+1) m -> Term n m
+
+end Cappy
diff --git a/Cappy/Syntax/Type.lean b/Cappy/Syntax/Type.lean
new file mode 100644
index 00000000..711d0698
--- /dev/null
+++ b/Cappy/Syntax/Type.lean
@@ -0,0 +1,55 @@
+import Cappy.Syntax.CaptureSet
+import Cappy.Renaming
+
+namespace Cappy
+
+inductive Annot : Type where
+| eps : Annot
+| use : Annot
+
+mutual
+
+inductive CType : Nat -> Nat -> Type where
+| capt : CaptureSet n -> SType n m -> CType n m
+
+inductive SType : Nat -> Nat -> Type where
+| top : SType n m
+| tvar : Fin m -> SType n m
+| arrow : Annot -> CType n m -> CType (n+1) m -> SType n m
+| tarrow : SType n m -> CType n (m+1) -> SType n m
+| boxed : CType n m -> SType n m
+
+end
+
+notation:max S "^" C => CType.capt C S
+notation:50 "∀(x:" T ")" U => SType.arrow Annot.eps T U
+notation:50 "∀(use x:" T ")" U => SType.arrow Annot.use T U
+notation:50 "∀[X<:" S "]" T => SType.tarrow S T
+
+mutual
+
+def CType.rename : CType n m -> RenameFun n m n' m' -> CType n' m'
+| CType.capt C S, f => (S.rename f)^(C.rename f.map)
+
+def SType.rename : SType n m -> RenameFun n m n' m' -> SType n' m'
+| SType.top, _ => SType.top
+| SType.tvar x, f => SType.tvar (f.tmap x)
+| SType.arrow a T U, f => SType.arrow a (T.rename f) (U.rename f.ext)
+| SType.tarrow S T, f => SType.tarrow (S.rename f) (T.rename f.text)
+| SType.boxed C, f => SType.boxed (C.rename f)
+
+end
+
+def CType.weaken (T : CType n m) : CType (n+1) m :=
+  T.rename RenameFun.weaken
+
+def SType.weaken (T : SType n m) : SType (n+1) m :=
+  T.rename RenameFun.weaken
+
+def CType.tweaken (T : CType n m) : CType n (m+1) :=
+  T.rename RenameFun.tweaken
+
+def SType.tweaken (T : SType n m) : SType n (m+1) :=
+  T.rename RenameFun.tweaken
+
+end Cappy
diff --git a/Cappy/TypeSystem/Subcapturing.lean b/Cappy/TypeSystem/Subcapturing.lean
new file mode 100644
index 00000000..d387c117
--- /dev/null
+++ b/Cappy/TypeSystem/Subcapturing.lean
@@ -0,0 +1,21 @@
+import Cappy.Syntax.Context
+namespace Cappy
+
+inductive Subcapt : Context n m -> CaptureSet n -> CaptureSet n -> Prop where
+| sc_trans :
+  Subcapt Γ C1 C2 ->
+  Subcapt Γ C2 C3 ->
+  Subcapt Γ C1 C3
+| sc_var :
+  Context.Bound Γ x (S^C) ->
+  Subcapt Γ {x=x} C
+| sc_elem {C1 C2 : CaptureSet n} :
+  C1 ⊆ C2 ->
+  Subcapt Γ C1 C2
+| sc_set :
+  Subcapt Γ C1 C ->
+  Subcapt Γ C2 C ->
+  Subcapt Γ (C1 ∪ C2) C
+
+
+end Cappy
diff --git a/Cappy/TypeSystem/Subtyping.lean b/Cappy/TypeSystem/Subtyping.lean
new file mode 100644
index 00000000..7ca4e979
--- /dev/null
+++ b/Cappy/TypeSystem/Subtyping.lean
@@ -0,0 +1,42 @@
+import Cappy.TypeSystem.Subcapturing
+namespace Cappy
+
+mutual
+
+inductive CSubtyp : Context n m -> CType n m -> CType n m -> Prop where
+| capt :
+  Subcapt Γ C1 C2 ->
+  SSubtyp Γ S1 S2 ->
+  CSubtyp Γ (S1^C1) (S2^C2)
+
+inductive SSubtyp : Context n m -> SType n m -> SType n m -> Prop where
+| top :
+  SSubtyp Γ S SType.top
+| refl :
+  SSubtyp Γ S S
+| trans :
+  SSubtyp Γ S1 S2 ->
+  SSubtyp Γ S2 S3 ->
+  SSubtyp Γ S1 S3
+| tvar :
+  Context.TBound Γ X S ->
+  SSubtyp Γ (SType.tvar X) S
+| boxed :
+  CSubtyp Γ T1 T2 ->
+  SSubtyp Γ (SType.boxed T1) (SType.boxed T2)
+| arrow :
+  CSubtyp Γ T2 T1 ->
+  CSubtyp (Γ.var T2) U1 U2 ->
+  SSubtyp Γ (∀(x:T1)U1) (SType.arrow a T2 U2)
+| uarrow :
+  CSubtyp (Γ.var T) U1 U2 ->
+  SSubtyp Γ (∀(use x:T)U1) (∀(use x:T)U2)
+| tarrow :
+  SSubtyp Γ S2 S1 ->
+  CSubtyp (Γ.tvar S2) T1 T2 ->
+  SSubtyp Γ (∀[X<:S1]T1) (∀[X<:S2]T2)
+
+end
+
+
+end Cappy
diff --git a/Cappy/TypeSystem/Typing.lean b/Cappy/TypeSystem/Typing.lean
new file mode 100644
index 00000000..03bc595a
--- /dev/null
+++ b/Cappy/TypeSystem/Typing.lean
@@ -0,0 +1,59 @@
+import Cappy.TypeSystem.Subtyping
+import Cappy.Syntax.Term
+namespace Cappy
+
+mutual
+
+inductive CType.CapRefine : CaptureSet n -> CType n m -> CType n m -> Prop where
+| r_capt :
+  SType.CapRefine D S S' ->
+  CType.CapRefine D (S^C) (S'^(C.open_cap D))
+
+inductive SType.CapRefine : CaptureSet n -> SType n m -> SType n m -> Prop where
+| r_top :
+  SType.CapRefine D top top
+| r_tvar :
+  SType.CapRefine D (SType.tvar X) (SType.tvar X)
+| r_fun :
+  CType.CapRefine (D.weaken ∪ {x=0} ∪ {x*=0}) U U' ->
+  SType.CapRefine D (SType.arrow a T U) (SType.arrow a T U')
+| r_tfun :
+  CType.CapRefine D T T' ->
+  SType.CapRefine D (SType.tarrow S T) (SType.tarrow S T')
+| r_boxed :
+  CType.CapRefine D T T' ->
+  SType.CapRefine D (SType.boxed T) (SType.boxed T')
+
+end
+
+inductive Typed : CaptureSet n -> Context n m -> Term n m -> CType n m -> Prop where
+| var :
+  Γ.Bound x (S^C) ->
+  S.CapRefine {x*=x} S' ->
+  Typed {x=x} Γ (Term.var x) (S'^{x=x})
+| sub :
+  Typed C Γ t T ->
+  Subcapt Γ C C' ->
+  CSubtyp Γ T T' ->
+  Typed C' Γ t T'
+| abs {C : CaptureSet n} :
+  Typed (C.weaken ∪ {x=0} ∪ {x*=0}) (Γ.var T) t U ->
+  Typed {} Γ (Term.abs Annot.eps T t) ((∀(x:T)U)^C)
+| uabs {C : CaptureSet n} :
+  Typed (C.weaken ∪ {x=0}) (Γ.var T) t U ->
+  Typed {} Γ (Term.abs Annot.use T t) ((∀(use x:T)U)^C)
+| tabs {C : CaptureSet n} :
+  Typed C (Γ.tvar S) t T ->
+  Typed {} Γ (Term.tabs S t) ((∀[X<:S]T)^C)
+| box {C : CaptureSet n} :
+  Typed C Γ (Term.var x) T ->
+  Typed {} Γ (Term.box x) ((SType.boxed T)^{})
+| unbox {C : CaptureSet n} :
+  Typed C Γ (Term.var x) ((SType.boxed (S^C))^{}) ->
+  Typed C Γ (Term.unbox C x) (S^C)
+| letin {C : CaptureSet n} {U : CType n m} :
+  Typed C Γ t T ->
+  Typed C.weaken (Γ.var T) u U.weaken ->
+  Typed C Γ (Term.letin t u) U
+
+end Cappy

From aed8bdc6a68e1d04c113a6833fa11d78e7dccd1f Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 24 Oct 2024 12:14:22 +0200
Subject: [PATCH 08/42] tweak cappy entry file

---
 Cappy.lean             | 3 ++-
 Cappy/Definitions.lean | 1 -
 Cappy/Syntax.lean      | 4 ++++
 Cappy/TypeSystem.lean  | 3 +++
 4 files changed, 9 insertions(+), 2 deletions(-)
 delete mode 100644 Cappy/Definitions.lean
 create mode 100644 Cappy/Syntax.lean
 create mode 100644 Cappy/TypeSystem.lean

diff --git a/Cappy.lean b/Cappy.lean
index a8da9e27..cd8ce275 100644
--- a/Cappy.lean
+++ b/Cappy.lean
@@ -1 +1,2 @@
-import Cappy.Definitions
+import Cappy.Syntax
+import Cappy.TypeSystem
diff --git a/Cappy/Definitions.lean b/Cappy/Definitions.lean
deleted file mode 100644
index e13163ad..00000000
--- a/Cappy/Definitions.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Cappy.TypeSystem.Typing
diff --git a/Cappy/Syntax.lean b/Cappy/Syntax.lean
new file mode 100644
index 00000000..39e28f7c
--- /dev/null
+++ b/Cappy/Syntax.lean
@@ -0,0 +1,4 @@
+import Cappy.Syntax.CaptureSet
+import Cappy.Syntax.Type
+import Cappy.Syntax.Term
+import Cappy.Syntax.Context
diff --git a/Cappy/TypeSystem.lean b/Cappy/TypeSystem.lean
new file mode 100644
index 00000000..627f761b
--- /dev/null
+++ b/Cappy/TypeSystem.lean
@@ -0,0 +1,3 @@
+import Cappy.TypeSystem.Subcapturing
+import Cappy.TypeSystem.Subtyping
+import Cappy.TypeSystem.Typing

From f86658fa5481135fc51d2b99604f28d7aac4e7e4 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 24 Oct 2024 20:03:41 +0200
Subject: [PATCH 09/42] translation: capture set encoding

---
 Cappy/Translation/CaptureSet.lean | 28 ++++++++++++++++++++++++++++
 Cappy/Translation/TContext.lean   | 10 ++++++++++
 Cappy/Translation/TMap.lean       |  7 +++++++
 3 files changed, 45 insertions(+)
 create mode 100644 Cappy/Translation/CaptureSet.lean
 create mode 100644 Cappy/Translation/TContext.lean
 create mode 100644 Cappy/Translation/TMap.lean

diff --git a/Cappy/Translation/CaptureSet.lean b/Cappy/Translation/CaptureSet.lean
new file mode 100644
index 00000000..52fef643
--- /dev/null
+++ b/Cappy/Translation/CaptureSet.lean
@@ -0,0 +1,28 @@
+import Cappy.Syntax
+import Capless.CaptureSet
+import Cappy.Translation.TContext
+namespace Cappy
+
+/-!
+# Encoding of Capture Sets
+!-/
+
+inductive CaptureSet.Interp : TMap n m k -> Context n m -> CaptureSet n -> Capless.CaptureSet n k -> Capless.CaptureSet n k -> Prop where
+| i_empty :
+  CaptureSet.Interp ρ Γ {} D {}
+| i_union :
+  CaptureSet.Interp ρ Γ C1 D D1 ->
+  CaptureSet.Interp ρ Γ C2 D D2 ->
+  CaptureSet.Interp ρ Γ (C1 ∪ C2) D (D1 ∪ D2)
+| i_singleton :
+  Context.Bound Γ x (S^C) ->
+  CaptureSet.Interp ρ Γ C {c=ρ.reach x} C' ->
+  CaptureSet.Interp ρ Γ {x=x} D C'
+| i_reach :
+  CaptureSet.Interp ρ Γ {x*=x} D {c=ρ.reach x}
+| i_cap :
+  CaptureSet.Interp ρ Γ {cap} D D
+
+notation:20 "⟦" C1 "⟧^" D " ↝c[" ρ " | " Γ "] " C2 => CaptureSet.Interp ρ Γ C1 D C2
+
+end Cappy
diff --git a/Cappy/Translation/TContext.lean b/Cappy/Translation/TContext.lean
new file mode 100644
index 00000000..bfe5e941
--- /dev/null
+++ b/Cappy/Translation/TContext.lean
@@ -0,0 +1,10 @@
+import Capless.Context
+import Capless.Basic
+import Cappy.Translation.TMap
+namespace Cappy
+
+structure TContext (n m k : Nat) where
+  ctx : Capless.Context n m k
+  map : TMap n m k
+
+end Cappy
diff --git a/Cappy/Translation/TMap.lean b/Cappy/Translation/TMap.lean
new file mode 100644
index 00000000..7a4438b7
--- /dev/null
+++ b/Cappy/Translation/TMap.lean
@@ -0,0 +1,7 @@
+namespace Cappy
+
+structure TMap (n m k : Nat) where
+  reach : Fin n -> Fin k
+  treach : Fin m -> Fin k
+
+end Cappy

From 64b54aa762f9d092e051c9b4790493b994ef0466 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 24 Oct 2024 20:14:00 +0200
Subject: [PATCH 10/42] translation: doc

---
 Cappy/Translation/CaptureSet.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/Cappy/Translation/CaptureSet.lean b/Cappy/Translation/CaptureSet.lean
index 52fef643..7106dd3b 100644
--- a/Cappy/Translation/CaptureSet.lean
+++ b/Cappy/Translation/CaptureSet.lean
@@ -5,6 +5,13 @@ namespace Cappy
 
 /-!
 # Encoding of Capture Sets
+
+The `CaptureSet.Interp` derivation defines the encoding of capture sets from Cappy to Capless. It is a 5-place judgement:
+1. The mapping from reach capabilities to capture variables
+2. The type context in Cappy
+3. The input capture set
+4. The interpretation
+5. The output capture set
 !-/
 
 inductive CaptureSet.Interp : TMap n m k -> Context n m -> CaptureSet n -> Capless.CaptureSet n k -> Capless.CaptureSet n k -> Prop where

From 484c3ace102b2d5da6aae693a139464cf5f5f0f6 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 24 Oct 2024 20:14:07 +0200
Subject: [PATCH 11/42] translation: cappy type encoding wip

---
 Cappy/Translation/Type.lean | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 Cappy/Translation/Type.lean

diff --git a/Cappy/Translation/Type.lean b/Cappy/Translation/Type.lean
new file mode 100644
index 00000000..5b3def07
--- /dev/null
+++ b/Cappy/Translation/Type.lean
@@ -0,0 +1,21 @@
+import Cappy.Translation.CaptureSet
+import Capless.Type
+namespace Cappy
+
+/-!
+# Encoding of Types
+!-/
+
+inductive CType.Interp : TMap n m k -> Context n m -> CType n m -> Capless.CaptureSet n k -> Capless.CType n m k -> Prop where
+| i_top :
+  CaptureSet.Interp ρ Γ C D C' ->
+  CType.Interp ρ Γ (SType.top^C) D (⊤^C')
+| i_tvar :
+  CaptureSet.Interp ρ Γ C D C' ->
+  CType.Interp ρ Γ ((SType.tvar X)^C) D ((Capless.SType.tvar X)^C')
+| i_boxed :
+  CaptureSet.Interp ρ Γ C D C' ->
+  CType.Interp ρ Γ T D T' ->
+  CType.Interp ρ Γ ((SType.boxed T)^C) D ((Capless.SType.box T')^C')
+
+end Cappy

From f1a4ad186d77ca7a35ec2ab827f9f06b42e12400 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 24 Oct 2024 21:11:50 +0200
Subject: [PATCH 12/42] cappy: finish the translation

---
 Capless/Type/Core.lean      |  3 +++
 Cappy/Translation/TMap.lean | 40 +++++++++++++++++++++++++++++++++++++
 Cappy/Translation/Type.lean | 32 +++++++++++++++++++++++++++--
 3 files changed, 73 insertions(+), 2 deletions(-)

diff --git a/Capless/Type/Core.lean b/Capless/Type/Core.lean
index 1e649fb7..f21d5d1c 100644
--- a/Capless/Type/Core.lean
+++ b/Capless/Type/Core.lean
@@ -30,4 +30,7 @@ notation:40 "∃c." T => EType.ex T
 instance : Coe (CType n m k) (EType n m k) where
   coe T := EType.type T
 
+instance : Coe (SType n m k) (CType n m k) where
+  coe T := CType.capt {} T
+
 end Capless
diff --git a/Cappy/Translation/TMap.lean b/Cappy/Translation/TMap.lean
index 7a4438b7..a8a91067 100644
--- a/Cappy/Translation/TMap.lean
+++ b/Cappy/Translation/TMap.lean
@@ -1,7 +1,47 @@
+import Aesop
+import Mathlib.Data.Fin.Basic
+import Capless.Basic
 namespace Cappy
 
 structure TMap (n m k : Nat) where
   reach : Fin n -> Fin k
   treach : Fin m -> Fin k
 
+def TMap.ext (ρ : TMap n m k) : TMap (n+1) m (k+1) := by
+  constructor
+  case reach =>
+    have h := ρ.reach
+    apply Capless.FinFun.ext
+    aesop
+  case treach =>
+    have h := ρ.treach
+    intro x
+    apply Fin.succ
+    aesop
+
+def TMap.text (ρ : TMap n m k) : TMap n (m+1) (k+1) := by
+  constructor
+  case reach =>
+    have h := ρ.reach
+    intro x
+    apply Fin.succ
+    aesop
+  case treach =>
+    have h := ρ.treach
+    apply Capless.FinFun.ext
+    aesop
+
+def TMap.cweaken (ρ : TMap n m k) : TMap n m (k+1) := by
+  constructor
+  case reach =>
+    have h := ρ.reach
+    intro x
+    apply Fin.succ
+    aesop
+  case treach =>
+    have h := ρ.treach
+    intro x
+    apply Fin.succ
+    aesop
+
 end Cappy
diff --git a/Cappy/Translation/Type.lean b/Cappy/Translation/Type.lean
index 5b3def07..36570713 100644
--- a/Cappy/Translation/Type.lean
+++ b/Cappy/Translation/Type.lean
@@ -14,8 +14,36 @@ inductive CType.Interp : TMap n m k -> Context n m -> CType n m -> Capless.Captu
   CaptureSet.Interp ρ Γ C D C' ->
   CType.Interp ρ Γ ((SType.tvar X)^C) D ((Capless.SType.tvar X)^C')
 | i_boxed :
-  CaptureSet.Interp ρ Γ C D C' ->
   CType.Interp ρ Γ T D T' ->
-  CType.Interp ρ Γ ((SType.boxed T)^C) D ((Capless.SType.box T')^C')
+  CType.Interp ρ Γ
+     ((SType.boxed T)^{})
+     D
+     ((∀(x:⊤^{})((∀(x:⊤^{})(Capless.EType.type T'.weaken.weaken))^Capless.CaptureSet.empty))^Capless.CaptureSet.empty)
+| i_arrow :
+  CaptureSet.Interp ρ Γ C D C' ->
+  CType.Interp ρ.cweaken Γ T ({c=0}) T' ->
+  CaptureSet.Interp ρ.ext (Γ.var T) ({x*=0}∪{x=0}) {} D1 ->
+  CType.Interp ρ.ext (Γ.var T) U (D.weaken.cweaken ∪ D1) U' ->
+  CType.Interp ρ Γ
+    ((∀(x:T)U)^C)
+    D
+    ((∀[c](Capless.EType.type (∀(x:T')U')^(C'.cweaken)))^({}))
+| i_uarrow :
+  CaptureSet.Interp ρ Γ C D C' ->
+  CType.Interp ρ.cweaken Γ T ({c=0}) T' ->
+  CaptureSet.Interp ρ.ext (Γ.var T) ({x*=0}∪{x=0}) {} D1 ->
+  CType.Interp ρ.ext (Γ.var T) U (D.weaken.cweaken ∪ D1) U' ->
+  CType.Interp ρ Γ
+    ((∀(use x:T)U)^C)
+    D
+    ((∀[c](Capless.EType.type (∀(x:T')U')^(C'.cweaken ∪ {c=0})))^({}))
+| i_tarrow :
+  CaptureSet.Interp ρ Γ C D C' ->
+  CType.Interp ρ.cweaken Γ (S^{}) ({c=0}) (S'^{}) ->
+  CType.Interp ρ.text (Γ.tvar S) T (D.cweaken) T' ->
+  CType.Interp ρ Γ
+    ((∀[X<:S]T)^C)
+    D
+    ((∀[c](Capless.EType.type (∀[X<:S']T')^(C'.cweaken)))^({}))
 
 end Cappy

From 1ab66055cc45d8942c2a51b7fd1bda5f4dddc596 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 24 Oct 2024 21:13:19 +0200
Subject: [PATCH 13/42] cappy: restructure

---
 Cappy/Translation/{ => Encoding}/CaptureSet.lean | 0
 Cappy/Translation/{ => Encoding}/Type.lean       | 2 +-
 2 files changed, 1 insertion(+), 1 deletion(-)
 rename Cappy/Translation/{ => Encoding}/CaptureSet.lean (100%)
 rename Cappy/Translation/{ => Encoding}/Type.lean (97%)

diff --git a/Cappy/Translation/CaptureSet.lean b/Cappy/Translation/Encoding/CaptureSet.lean
similarity index 100%
rename from Cappy/Translation/CaptureSet.lean
rename to Cappy/Translation/Encoding/CaptureSet.lean
diff --git a/Cappy/Translation/Type.lean b/Cappy/Translation/Encoding/Type.lean
similarity index 97%
rename from Cappy/Translation/Type.lean
rename to Cappy/Translation/Encoding/Type.lean
index 36570713..4e7c4703 100644
--- a/Cappy/Translation/Type.lean
+++ b/Cappy/Translation/Encoding/Type.lean
@@ -1,4 +1,4 @@
-import Cappy.Translation.CaptureSet
+import Cappy.Translation.Encoding.CaptureSet
 import Capless.Type
 namespace Cappy
 

From ed647360c69451bd80fd873b5435f40046075a24 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 24 Oct 2024 21:20:52 +0200
Subject: [PATCH 14/42] cappy: typectx encoding wip

---
 Cappy/Translation/Encoding/Context.lean | 9 +++++++++
 Cappy/Translation/TContext.lean         | 5 +++++
 Cappy/Translation/TMap.lean             | 2 ++
 3 files changed, 16 insertions(+)
 create mode 100644 Cappy/Translation/Encoding/Context.lean

diff --git a/Cappy/Translation/Encoding/Context.lean b/Cappy/Translation/Encoding/Context.lean
new file mode 100644
index 00000000..1df7a2da
--- /dev/null
+++ b/Cappy/Translation/Encoding/Context.lean
@@ -0,0 +1,9 @@
+import Cappy.Translation.Encoding.Type
+import Cappy.Translation.TContext
+namespace Cappy
+
+inductive Context.Interp : Context n m -> TContext n m k -> Prop where
+| empty :
+  Context.Interp empty TContext.empty
+
+end Cappy
diff --git a/Cappy/Translation/TContext.lean b/Cappy/Translation/TContext.lean
index bfe5e941..a7a84bb7 100644
--- a/Cappy/Translation/TContext.lean
+++ b/Cappy/Translation/TContext.lean
@@ -7,4 +7,9 @@ structure TContext (n m k : Nat) where
   ctx : Capless.Context n m k
   map : TMap n m k
 
+def TContext.empty : TContext 0 0 0 :=
+  ⟨Capless.Context.empty, TMap.empty⟩
+
+def TContext.var (Γ : TContext n m k) : TContext (n+1) m (k+1) := sorry
+
 end Cappy
diff --git a/Cappy/Translation/TMap.lean b/Cappy/Translation/TMap.lean
index a8a91067..d506e09b 100644
--- a/Cappy/Translation/TMap.lean
+++ b/Cappy/Translation/TMap.lean
@@ -7,6 +7,8 @@ structure TMap (n m k : Nat) where
   reach : Fin n -> Fin k
   treach : Fin m -> Fin k
 
+def TMap.empty : TMap 0 0 0 := ⟨id, id⟩
+
 def TMap.ext (ρ : TMap n m k) : TMap (n+1) m (k+1) := by
   constructor
   case reach =>

From 3b4a6b028bd7fb3f7bb30d7c3f635de4b4097266 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 24 Oct 2024 21:28:16 +0200
Subject: [PATCH 15/42] cappy: typectx encoding

---
 Cappy/Translation/Encoding/Context.lean |  8 ++++++++
 Cappy/Translation/TContext.lean         | 12 +++++++++++-
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/Cappy/Translation/Encoding/Context.lean b/Cappy/Translation/Encoding/Context.lean
index 1df7a2da..1b974909 100644
--- a/Cappy/Translation/Encoding/Context.lean
+++ b/Cappy/Translation/Encoding/Context.lean
@@ -5,5 +5,13 @@ namespace Cappy
 inductive Context.Interp : Context n m -> TContext n m k -> Prop where
 | empty :
   Context.Interp empty TContext.empty
+| var {Γ : Context n m} {Δ : TContext n m k} :
+  Context.Interp Γ Δ ->
+  CType.Interp (Δ.map.cweaken) Γ T {c=0} T' ->
+  Context.Interp (Γ.var T) (Δ.var T')
+| tvar {Γ : Context n m} {Δ : TContext n m k} :
+  Context.Interp Γ Δ ->
+  CType.Interp (Δ.map.cweaken) Γ (S^{}) {c=0} (S'^{}) ->
+  Context.Interp (Γ.tvar S) (Δ.tvar S')
 
 end Cappy
diff --git a/Cappy/Translation/TContext.lean b/Cappy/Translation/TContext.lean
index a7a84bb7..280e9ae2 100644
--- a/Cappy/Translation/TContext.lean
+++ b/Cappy/Translation/TContext.lean
@@ -10,6 +10,16 @@ structure TContext (n m k : Nat) where
 def TContext.empty : TContext 0 0 0 :=
   ⟨Capless.Context.empty, TMap.empty⟩
 
-def TContext.var (Γ : TContext n m k) : TContext (n+1) m (k+1) := sorry
+def TContext.var
+  (Γ : TContext n m k)
+  (T : Capless.CType n m (k+1)) :
+  TContext (n+1) m (k+1) :=
+  ⟨((Γ.ctx,c:CapSet),x:T), Γ.map.ext⟩
+
+def TContext.tvar
+  (Γ : TContext n m k)
+  (S : Capless.SType n m (k+1)) :
+  TContext n (m+1) (k+1) :=
+  ⟨((Γ.ctx,c:CapSet),X<:S), Γ.map.text⟩
 
 end Cappy

From 9ba9a933eddb3b7b9c4ba9a670c0f6d5c0f1eb3b Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 24 Oct 2024 22:30:10 -0700
Subject: [PATCH 16/42] cappy: setup the theorem for subcapturing

---
 Cappy/Translation/Subcapturing.lean | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 Cappy/Translation/Subcapturing.lean

diff --git a/Cappy/Translation/Subcapturing.lean b/Cappy/Translation/Subcapturing.lean
new file mode 100644
index 00000000..51d77f36
--- /dev/null
+++ b/Cappy/Translation/Subcapturing.lean
@@ -0,0 +1,22 @@
+import Cappy.Translation.Encoding.Context
+import Cappy.TypeSystem.Subcapturing
+import Capless.Subcapturing
+import Capless.Subcapturing.Basic
+namespace Cappy
+
+theorem subcapt_enc_monotonic
+  (hg : Context.Interp Γ Δ)
+  (h : Δ.ctx ⊢ D1 <:c D2)
+  (hi1 : CaptureSet.Interp Δ.map Γ C D1 I1)
+  (hi2 : CaptureSet.Interp Δ.map Γ C D2 I2) :
+  (Δ.ctx ⊢ I1 <:c I2) := by
+  induction C
+  case empty =>
+    cases hi1; cases hi2
+    apply Capless.Subcapt.refl
+  case union => sorry
+  case singleton => sorry
+  case reach => sorry
+  case universal => sorry
+
+end Cappy

From 835e7e0db5193c2d5ef5988a9ef48de5003dc868 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Mon, 28 Oct 2024 14:44:39 +0100
Subject: [PATCH 17/42] drop useless file

---
 Capless/playground.lean | 15 ---------------
 1 file changed, 15 deletions(-)
 delete mode 100644 Capless/playground.lean

diff --git a/Capless/playground.lean b/Capless/playground.lean
deleted file mode 100644
index b366fe2b..00000000
--- a/Capless/playground.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-inductive MemKind: Type -- classifies names/members
-| field -- names of term members
-| type  -- names of type members
-
-inductive Ty: Nat -> Type -- for simplicity, just one case
-| bot: Ty n
-
-inductive ComponentSig: Nat -> MemKind -> Type -- classifies the dependent second component of a pair _type_
-| field : Ty n -> ComponentSig n field         -- field member of type T
-| type  : Ty n -> Ty n -> ComponentSig n type  -- type member with interval S .. T
-
-def ComponentSig.interval' (sig : ComponentSig n K) : Ty n × Ty n := by
-  cases sig
-  case field => sorry
-  case type => sorry

From 2a7fe95224d960de14c9807fa881a0d769250f00 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Mon, 28 Oct 2024 14:53:39 +0100
Subject: [PATCH 18/42] cappy: add a theorem for subcapturing

---
 Capless/CaptureSet.lean             |  1 +
 Capless/Subcapturing/Basic.lean     | 24 ++++++++++++++++++++++++
 Cappy/Syntax/CaptureSet.lean        |  1 +
 Cappy/Translation/Subcapturing.lean | 16 +++++++++-------
 4 files changed, 35 insertions(+), 7 deletions(-)

diff --git a/Capless/CaptureSet.lean b/Capless/CaptureSet.lean
index 327647f3..d674eeb9 100644
--- a/Capless/CaptureSet.lean
+++ b/Capless/CaptureSet.lean
@@ -28,6 +28,7 @@ notation:max "{c=" c "}" => CaptureSet.csingleton c
 instance : Union (CaptureSet n k) where
   union := CaptureSet.union
 
+@[aesop unsafe [50% constructors]]
 inductive CaptureSet.Subset : CaptureSet n k → CaptureSet n k → Prop where
 | empty : Subset {} C
 | rfl : Subset C C
diff --git a/Capless/Subcapturing/Basic.lean b/Capless/Subcapturing/Basic.lean
index 5d170ea5..54c06ba6 100644
--- a/Capless/Subcapturing/Basic.lean
+++ b/Capless/Subcapturing/Basic.lean
@@ -6,4 +6,28 @@ theorem Subcapt.refl :
   apply subset
   apply CaptureSet.subset_refl
 
+theorem Subcapt.union_l
+  (h : Subcapt Γ C C2) :
+  Subcapt Γ C (C1 ∪ C2) := by
+  apply Subcapt.trans
+  { exact h }
+  { apply Subcapt.subset
+    aesop }
+
+theorem Subcapt.union_r
+  (h : Subcapt Γ C C1) :
+  Subcapt Γ C (C1 ∪ C2) := by
+  apply Subcapt.trans
+  { exact h }
+  { apply Subcapt.subset
+    aesop }
+
+theorem Subcapt.join
+  (h1 : Subcapt Γ C1 D1)
+  (h2 : Subcapt Γ C2 D2) :
+  Subcapt Γ (C1 ∪ C2) (D1 ∪ D2) := by
+  apply Subcapt.union
+  { apply Subcapt.union_r; assumption }
+  { apply Subcapt.union_l; assumption }
+
 end Capless
diff --git a/Cappy/Syntax/CaptureSet.lean b/Cappy/Syntax/CaptureSet.lean
index 61915ab0..e4d40510 100644
--- a/Cappy/Syntax/CaptureSet.lean
+++ b/Cappy/Syntax/CaptureSet.lean
@@ -22,6 +22,7 @@ notation:max "{cap}" => CaptureSet.universal
 instance : Union (CaptureSet n) where
   union := CaptureSet.union
 
+@[aesop unsafe [50% constructors]]
 inductive CaptureSet.Subset : CaptureSet n -> CaptureSet n -> Prop where
 | empty : Subset {} C
 | rfl : Subset C C
diff --git a/Cappy/Translation/Subcapturing.lean b/Cappy/Translation/Subcapturing.lean
index 51d77f36..21f29c81 100644
--- a/Cappy/Translation/Subcapturing.lean
+++ b/Cappy/Translation/Subcapturing.lean
@@ -5,16 +5,18 @@ import Capless.Subcapturing.Basic
 namespace Cappy
 
 theorem subcapt_enc_monotonic
-  (hg : Context.Interp Γ Δ)
-  (h : Δ.ctx ⊢ D1 <:c D2)
-  (hi1 : CaptureSet.Interp Δ.map Γ C D1 I1)
-  (hi2 : CaptureSet.Interp Δ.map Γ C D2 I2) :
-  (Δ.ctx ⊢ I1 <:c I2) := by
-  induction C
+  (hg : Context.Interp Γ ⟨Δ, ρ⟩)
+  (h : Δ ⊢ D1 <:c D2)
+  (hi1 : CaptureSet.Interp ρ Γ C D1 I1)
+  (hi2 : CaptureSet.Interp ρ Γ C D2 I2) :
+  (Δ ⊢ I1 <:c I2) := by
+  induction C generalizing I1 I2
   case empty =>
     cases hi1; cases hi2
     apply Capless.Subcapt.refl
-  case union => sorry
+  case union C1 C2 ih1 ih2 =>
+    cases hi1; cases hi2
+    sorry
   case singleton => sorry
   case reach => sorry
   case universal => sorry

From ea847697fb9e116d4dd0bfa7eb2a8944f83698dc Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Mon, 28 Oct 2024 15:03:50 +0100
Subject: [PATCH 19/42] cappy: context lookup is injective

---
 Cappy/Syntax/Context.lean            | 31 ++------------------------
 Cappy/Syntax/Context/Core.lean       | 29 ++++++++++++++++++++++++
 Cappy/Syntax/Context/Properties.lean | 33 ++++++++++++++++++++++++++++
 3 files changed, 64 insertions(+), 29 deletions(-)
 create mode 100644 Cappy/Syntax/Context/Core.lean
 create mode 100644 Cappy/Syntax/Context/Properties.lean

diff --git a/Cappy/Syntax/Context.lean b/Cappy/Syntax/Context.lean
index 8258b9ae..ec3052da 100644
--- a/Cappy/Syntax/Context.lean
+++ b/Cappy/Syntax/Context.lean
@@ -1,29 +1,2 @@
-import Cappy.Syntax.Type
-namespace Cappy
-
-inductive Context : Nat -> Nat -> Type where
-| empty : Context 0 0
-| var : Context n m -> CType n m -> Context (n+1) m
-| tvar : Context n m -> SType n m -> Context n (m+1)
-
-inductive Context.Bound : Context n m -> Fin n -> CType n m -> Prop where
-| here :
-  Context.Bound (Context.var Γ T) 0 T.weaken
-| there_var :
-  Context.Bound Γ x T ->
-  Context.Bound (Context.var Γ T') x.succ T.weaken
-| there_tvar :
-  Context.Bound Γ x T ->
-  Context.Bound (Context.tvar Γ S) x T.tweaken
-
-inductive Context.TBound : Context n m -> Fin m -> SType n m -> Prop where
-| here :
-  Context.TBound (Context.tvar Γ S) 0 S.tweaken
-| there_var :
-  Context.TBound Γ x S ->
-  Context.TBound (Context.var Γ T) x S.weaken
-| there_tvar :
-  Context.TBound Γ x S ->
-  Context.TBound (Context.tvar Γ S') x.succ S.tweaken
-
-end Cappy
+import Cappy.Syntax.Context.Core
+import Cappy.Syntax.Context.Properties
diff --git a/Cappy/Syntax/Context/Core.lean b/Cappy/Syntax/Context/Core.lean
new file mode 100644
index 00000000..8258b9ae
--- /dev/null
+++ b/Cappy/Syntax/Context/Core.lean
@@ -0,0 +1,29 @@
+import Cappy.Syntax.Type
+namespace Cappy
+
+inductive Context : Nat -> Nat -> Type where
+| empty : Context 0 0
+| var : Context n m -> CType n m -> Context (n+1) m
+| tvar : Context n m -> SType n m -> Context n (m+1)
+
+inductive Context.Bound : Context n m -> Fin n -> CType n m -> Prop where
+| here :
+  Context.Bound (Context.var Γ T) 0 T.weaken
+| there_var :
+  Context.Bound Γ x T ->
+  Context.Bound (Context.var Γ T') x.succ T.weaken
+| there_tvar :
+  Context.Bound Γ x T ->
+  Context.Bound (Context.tvar Γ S) x T.tweaken
+
+inductive Context.TBound : Context n m -> Fin m -> SType n m -> Prop where
+| here :
+  Context.TBound (Context.tvar Γ S) 0 S.tweaken
+| there_var :
+  Context.TBound Γ x S ->
+  Context.TBound (Context.var Γ T) x S.weaken
+| there_tvar :
+  Context.TBound Γ x S ->
+  Context.TBound (Context.tvar Γ S') x.succ S.tweaken
+
+end Cappy
diff --git a/Cappy/Syntax/Context/Properties.lean b/Cappy/Syntax/Context/Properties.lean
new file mode 100644
index 00000000..e55f01e6
--- /dev/null
+++ b/Cappy/Syntax/Context/Properties.lean
@@ -0,0 +1,33 @@
+import Cappy.Syntax.Context.Core
+namespace Cappy
+
+theorem Context.var_bound_succ'
+  (he1 : Γ0 = Γ.var P) (he2 : x0 = x.succ)
+  (hb : Context.Bound Γ0 x0 T) :
+  ∃ T0, Context.Bound Γ x T0 ∧ T = T0.weaken := by
+  cases hb <;> try (solve | cases he1 | cases he2)
+  cases he1
+  rw [Fin.succ_inj] at he2
+  aesop
+
+theorem Context.var_bound_succ
+  (hb : Context.Bound (Context.var Γ P) x.succ T) :
+  ∃ T0, Context.Bound Γ x T0 ∧ T = T0.weaken :=
+  Context.var_bound_succ' rfl rfl hb
+
+theorem Context.bound_inj
+  (hb1 : Context.Bound Γ x T1)
+  (hb2 : Context.Bound Γ x T2) :
+  T1 = T2 := by
+  induction hb1
+  case here => cases hb2; rfl
+  case there_var ih =>
+    have ⟨T0, hb2, heq⟩ := Context.var_bound_succ hb2
+    have ih := ih hb2
+    aesop
+  case there_tvar ih =>
+    cases hb2; rename_i hb2
+    have ih := ih hb2
+    aesop
+
+end Cappy

From 39f121bf1422161a9ddfac8f10ad5212a6f3f93d Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Mon, 28 Oct 2024 15:04:06 +0100
Subject: [PATCH 20/42] cappy: progress capset encoding monotonic theorem

---
 Cappy/Translation/Subcapturing.lean | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

diff --git a/Cappy/Translation/Subcapturing.lean b/Cappy/Translation/Subcapturing.lean
index 21f29c81..553065d9 100644
--- a/Cappy/Translation/Subcapturing.lean
+++ b/Cappy/Translation/Subcapturing.lean
@@ -16,9 +16,20 @@ theorem subcapt_enc_monotonic
     apply Capless.Subcapt.refl
   case union C1 C2 ih1 ih2 =>
     cases hi1; cases hi2
+    apply Capless.Subcapt.join
+    { aesop }
+    { aesop }
+  case singleton =>
+    cases hi1; cases hi2
+    rename_i hb1 hi1 _ _ hb2 hi2
+    have h := Context.bound_inj hb1 hb2
+    cases h
     sorry
-  case singleton => sorry
-  case reach => sorry
-  case universal => sorry
+  case reach =>
+    cases hi1; cases hi2
+    apply Capless.Subcapt.refl
+  case universal =>
+    cases hi1; cases hi2
+    assumption
 
 end Cappy

From a2e62956f468a4c96aa6141ec3b15a80978b2041 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Mon, 28 Oct 2024 15:09:27 +0100
Subject: [PATCH 21/42] cappy: restructure

---
 .../Translation/Encoding/CaptureSet/Core.lean | 35 ++++++++++++++++++
 .../Encoding/CaptureSet/Properties.lean       |  4 ++
 Cappy/Translation/Subcapturing.lean           | 37 +------------------
 3 files changed, 41 insertions(+), 35 deletions(-)
 create mode 100644 Cappy/Translation/Encoding/CaptureSet/Core.lean
 create mode 100644 Cappy/Translation/Encoding/CaptureSet/Properties.lean

diff --git a/Cappy/Translation/Encoding/CaptureSet/Core.lean b/Cappy/Translation/Encoding/CaptureSet/Core.lean
new file mode 100644
index 00000000..553065d9
--- /dev/null
+++ b/Cappy/Translation/Encoding/CaptureSet/Core.lean
@@ -0,0 +1,35 @@
+import Cappy.Translation.Encoding.Context
+import Cappy.TypeSystem.Subcapturing
+import Capless.Subcapturing
+import Capless.Subcapturing.Basic
+namespace Cappy
+
+theorem subcapt_enc_monotonic
+  (hg : Context.Interp Γ ⟨Δ, ρ⟩)
+  (h : Δ ⊢ D1 <:c D2)
+  (hi1 : CaptureSet.Interp ρ Γ C D1 I1)
+  (hi2 : CaptureSet.Interp ρ Γ C D2 I2) :
+  (Δ ⊢ I1 <:c I2) := by
+  induction C generalizing I1 I2
+  case empty =>
+    cases hi1; cases hi2
+    apply Capless.Subcapt.refl
+  case union C1 C2 ih1 ih2 =>
+    cases hi1; cases hi2
+    apply Capless.Subcapt.join
+    { aesop }
+    { aesop }
+  case singleton =>
+    cases hi1; cases hi2
+    rename_i hb1 hi1 _ _ hb2 hi2
+    have h := Context.bound_inj hb1 hb2
+    cases h
+    sorry
+  case reach =>
+    cases hi1; cases hi2
+    apply Capless.Subcapt.refl
+  case universal =>
+    cases hi1; cases hi2
+    assumption
+
+end Cappy
diff --git a/Cappy/Translation/Encoding/CaptureSet/Properties.lean b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
new file mode 100644
index 00000000..a10ab6fd
--- /dev/null
+++ b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
@@ -0,0 +1,4 @@
+import Cappy.Translation.Encoding.CaptureSet.Core
+namespace Cappy
+
+end Cappy
diff --git a/Cappy/Translation/Subcapturing.lean b/Cappy/Translation/Subcapturing.lean
index 553065d9..e1a4825f 100644
--- a/Cappy/Translation/Subcapturing.lean
+++ b/Cappy/Translation/Subcapturing.lean
@@ -1,35 +1,2 @@
-import Cappy.Translation.Encoding.Context
-import Cappy.TypeSystem.Subcapturing
-import Capless.Subcapturing
-import Capless.Subcapturing.Basic
-namespace Cappy
-
-theorem subcapt_enc_monotonic
-  (hg : Context.Interp Γ ⟨Δ, ρ⟩)
-  (h : Δ ⊢ D1 <:c D2)
-  (hi1 : CaptureSet.Interp ρ Γ C D1 I1)
-  (hi2 : CaptureSet.Interp ρ Γ C D2 I2) :
-  (Δ ⊢ I1 <:c I2) := by
-  induction C generalizing I1 I2
-  case empty =>
-    cases hi1; cases hi2
-    apply Capless.Subcapt.refl
-  case union C1 C2 ih1 ih2 =>
-    cases hi1; cases hi2
-    apply Capless.Subcapt.join
-    { aesop }
-    { aesop }
-  case singleton =>
-    cases hi1; cases hi2
-    rename_i hb1 hi1 _ _ hb2 hi2
-    have h := Context.bound_inj hb1 hb2
-    cases h
-    sorry
-  case reach =>
-    cases hi1; cases hi2
-    apply Capless.Subcapt.refl
-  case universal =>
-    cases hi1; cases hi2
-    assumption
-
-end Cappy
+import Cappy.Translation.Encoding.CaptureSet.Core
+import Cappy.Translation.Encoding.CaptureSet.Properties

From a35de676b4b24a8a145cef01704a3e1b30808a9c Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Mon, 28 Oct 2024 15:11:14 +0100
Subject: [PATCH 22/42] cappy: restructure again

---
 Cappy/Translation/Encoding/CaptureSet.lean    | 37 +----------
 .../Translation/Encoding/CaptureSet/Core.lean | 62 +++++++++----------
 .../Encoding/CaptureSet/Properties.lean       |  5 ++
 Cappy/Translation/Subcapturing.lean           | 37 ++++++++++-
 4 files changed, 73 insertions(+), 68 deletions(-)

diff --git a/Cappy/Translation/Encoding/CaptureSet.lean b/Cappy/Translation/Encoding/CaptureSet.lean
index 7106dd3b..e1a4825f 100644
--- a/Cappy/Translation/Encoding/CaptureSet.lean
+++ b/Cappy/Translation/Encoding/CaptureSet.lean
@@ -1,35 +1,2 @@
-import Cappy.Syntax
-import Capless.CaptureSet
-import Cappy.Translation.TContext
-namespace Cappy
-
-/-!
-# Encoding of Capture Sets
-
-The `CaptureSet.Interp` derivation defines the encoding of capture sets from Cappy to Capless. It is a 5-place judgement:
-1. The mapping from reach capabilities to capture variables
-2. The type context in Cappy
-3. The input capture set
-4. The interpretation
-5. The output capture set
-!-/
-
-inductive CaptureSet.Interp : TMap n m k -> Context n m -> CaptureSet n -> Capless.CaptureSet n k -> Capless.CaptureSet n k -> Prop where
-| i_empty :
-  CaptureSet.Interp ρ Γ {} D {}
-| i_union :
-  CaptureSet.Interp ρ Γ C1 D D1 ->
-  CaptureSet.Interp ρ Γ C2 D D2 ->
-  CaptureSet.Interp ρ Γ (C1 ∪ C2) D (D1 ∪ D2)
-| i_singleton :
-  Context.Bound Γ x (S^C) ->
-  CaptureSet.Interp ρ Γ C {c=ρ.reach x} C' ->
-  CaptureSet.Interp ρ Γ {x=x} D C'
-| i_reach :
-  CaptureSet.Interp ρ Γ {x*=x} D {c=ρ.reach x}
-| i_cap :
-  CaptureSet.Interp ρ Γ {cap} D D
-
-notation:20 "⟦" C1 "⟧^" D " ↝c[" ρ " | " Γ "] " C2 => CaptureSet.Interp ρ Γ C1 D C2
-
-end Cappy
+import Cappy.Translation.Encoding.CaptureSet.Core
+import Cappy.Translation.Encoding.CaptureSet.Properties
diff --git a/Cappy/Translation/Encoding/CaptureSet/Core.lean b/Cappy/Translation/Encoding/CaptureSet/Core.lean
index 553065d9..7106dd3b 100644
--- a/Cappy/Translation/Encoding/CaptureSet/Core.lean
+++ b/Cappy/Translation/Encoding/CaptureSet/Core.lean
@@ -1,35 +1,35 @@
-import Cappy.Translation.Encoding.Context
-import Cappy.TypeSystem.Subcapturing
-import Capless.Subcapturing
-import Capless.Subcapturing.Basic
+import Cappy.Syntax
+import Capless.CaptureSet
+import Cappy.Translation.TContext
 namespace Cappy
 
-theorem subcapt_enc_monotonic
-  (hg : Context.Interp Γ ⟨Δ, ρ⟩)
-  (h : Δ ⊢ D1 <:c D2)
-  (hi1 : CaptureSet.Interp ρ Γ C D1 I1)
-  (hi2 : CaptureSet.Interp ρ Γ C D2 I2) :
-  (Δ ⊢ I1 <:c I2) := by
-  induction C generalizing I1 I2
-  case empty =>
-    cases hi1; cases hi2
-    apply Capless.Subcapt.refl
-  case union C1 C2 ih1 ih2 =>
-    cases hi1; cases hi2
-    apply Capless.Subcapt.join
-    { aesop }
-    { aesop }
-  case singleton =>
-    cases hi1; cases hi2
-    rename_i hb1 hi1 _ _ hb2 hi2
-    have h := Context.bound_inj hb1 hb2
-    cases h
-    sorry
-  case reach =>
-    cases hi1; cases hi2
-    apply Capless.Subcapt.refl
-  case universal =>
-    cases hi1; cases hi2
-    assumption
+/-!
+# Encoding of Capture Sets
+
+The `CaptureSet.Interp` derivation defines the encoding of capture sets from Cappy to Capless. It is a 5-place judgement:
+1. The mapping from reach capabilities to capture variables
+2. The type context in Cappy
+3. The input capture set
+4. The interpretation
+5. The output capture set
+!-/
+
+inductive CaptureSet.Interp : TMap n m k -> Context n m -> CaptureSet n -> Capless.CaptureSet n k -> Capless.CaptureSet n k -> Prop where
+| i_empty :
+  CaptureSet.Interp ρ Γ {} D {}
+| i_union :
+  CaptureSet.Interp ρ Γ C1 D D1 ->
+  CaptureSet.Interp ρ Γ C2 D D2 ->
+  CaptureSet.Interp ρ Γ (C1 ∪ C2) D (D1 ∪ D2)
+| i_singleton :
+  Context.Bound Γ x (S^C) ->
+  CaptureSet.Interp ρ Γ C {c=ρ.reach x} C' ->
+  CaptureSet.Interp ρ Γ {x=x} D C'
+| i_reach :
+  CaptureSet.Interp ρ Γ {x*=x} D {c=ρ.reach x}
+| i_cap :
+  CaptureSet.Interp ρ Γ {cap} D D
+
+notation:20 "⟦" C1 "⟧^" D " ↝c[" ρ " | " Γ "] " C2 => CaptureSet.Interp ρ Γ C1 D C2
 
 end Cappy
diff --git a/Cappy/Translation/Encoding/CaptureSet/Properties.lean b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
index a10ab6fd..bfb6099e 100644
--- a/Cappy/Translation/Encoding/CaptureSet/Properties.lean
+++ b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
@@ -1,4 +1,9 @@
 import Cappy.Translation.Encoding.CaptureSet.Core
 namespace Cappy
 
+theorem CaptureSet.interp_inj
+  (hi1 : CaptureSet.Interp ρ Γ C D I1)
+  (hi2 : CaptureSet.Interp ρ Γ C D I2) :
+  I1 = I2 := sorry
+
 end Cappy
diff --git a/Cappy/Translation/Subcapturing.lean b/Cappy/Translation/Subcapturing.lean
index e1a4825f..553065d9 100644
--- a/Cappy/Translation/Subcapturing.lean
+++ b/Cappy/Translation/Subcapturing.lean
@@ -1,2 +1,35 @@
-import Cappy.Translation.Encoding.CaptureSet.Core
-import Cappy.Translation.Encoding.CaptureSet.Properties
+import Cappy.Translation.Encoding.Context
+import Cappy.TypeSystem.Subcapturing
+import Capless.Subcapturing
+import Capless.Subcapturing.Basic
+namespace Cappy
+
+theorem subcapt_enc_monotonic
+  (hg : Context.Interp Γ ⟨Δ, ρ⟩)
+  (h : Δ ⊢ D1 <:c D2)
+  (hi1 : CaptureSet.Interp ρ Γ C D1 I1)
+  (hi2 : CaptureSet.Interp ρ Γ C D2 I2) :
+  (Δ ⊢ I1 <:c I2) := by
+  induction C generalizing I1 I2
+  case empty =>
+    cases hi1; cases hi2
+    apply Capless.Subcapt.refl
+  case union C1 C2 ih1 ih2 =>
+    cases hi1; cases hi2
+    apply Capless.Subcapt.join
+    { aesop }
+    { aesop }
+  case singleton =>
+    cases hi1; cases hi2
+    rename_i hb1 hi1 _ _ hb2 hi2
+    have h := Context.bound_inj hb1 hb2
+    cases h
+    sorry
+  case reach =>
+    cases hi1; cases hi2
+    apply Capless.Subcapt.refl
+  case universal =>
+    cases hi1; cases hi2
+    assumption
+
+end Cappy

From b9ab9c162f93f70a4835ee6e60dd02dc985f54b2 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Mon, 28 Oct 2024 15:16:23 +0100
Subject: [PATCH 23/42] cappy: props of capture set interp

---
 Cappy/Translation/Encoding/CaptureSet/Properties.lean | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/Cappy/Translation/Encoding/CaptureSet/Properties.lean b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
index bfb6099e..de2b303a 100644
--- a/Cappy/Translation/Encoding/CaptureSet/Properties.lean
+++ b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
@@ -4,6 +4,14 @@ namespace Cappy
 theorem CaptureSet.interp_inj
   (hi1 : CaptureSet.Interp ρ Γ C D I1)
   (hi2 : CaptureSet.Interp ρ Γ C D I2) :
-  I1 = I2 := sorry
+  I1 = I2 := by
+  induction hi1 generalizing I2 <;> try (solve | cases hi2; trivial)
+  case i_union ih1 ih2 =>
+    cases hi2
+    aesop
+  case i_singleton hb1 _ ih =>
+    cases hi2; rename_i hb2 _
+    have h := Context.bound_inj hb1 hb2
+    aesop
 
 end Cappy

From 79c794224775527c3180297eeed4abab779d7e63 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Mon, 28 Oct 2024 15:16:32 +0100
Subject: [PATCH 24/42] cappy: interp preserves subcapt

---
 Cappy/Translation/Subcapturing.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Cappy/Translation/Subcapturing.lean b/Cappy/Translation/Subcapturing.lean
index 553065d9..b3e43b98 100644
--- a/Cappy/Translation/Subcapturing.lean
+++ b/Cappy/Translation/Subcapturing.lean
@@ -24,7 +24,9 @@ theorem subcapt_enc_monotonic
     rename_i hb1 hi1 _ _ hb2 hi2
     have h := Context.bound_inj hb1 hb2
     cases h
-    sorry
+    have h := CaptureSet.interp_inj hi1 hi2
+    cases h
+    apply Capless.Subcapt.refl
   case reach =>
     cases hi1; cases hi2
     apply Capless.Subcapt.refl

From 20b1f322465cd91eab630ca256d82d4efbb00732 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Mon, 28 Oct 2024 15:16:53 +0100
Subject: [PATCH 25/42] cappy: make the theorem leaner

---
 Cappy/Translation/Subcapturing.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Cappy/Translation/Subcapturing.lean b/Cappy/Translation/Subcapturing.lean
index b3e43b98..151ca605 100644
--- a/Cappy/Translation/Subcapturing.lean
+++ b/Cappy/Translation/Subcapturing.lean
@@ -5,7 +5,6 @@ import Capless.Subcapturing.Basic
 namespace Cappy
 
 theorem subcapt_enc_monotonic
-  (hg : Context.Interp Γ ⟨Δ, ρ⟩)
   (h : Δ ⊢ D1 <:c D2)
   (hi1 : CaptureSet.Interp ρ Γ C D1 I1)
   (hi2 : CaptureSet.Interp ρ Γ C D2 I2) :

From 95aa10fa056e8d28947913e80463da2dd3f93485 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Mon, 28 Oct 2024 16:43:46 +0100
Subject: [PATCH 26/42] cappy: capset interp monotonic theorem (II) wip

---
 Cappy/Translation/Subcapturing.lean | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/Cappy/Translation/Subcapturing.lean b/Cappy/Translation/Subcapturing.lean
index 151ca605..250e2402 100644
--- a/Cappy/Translation/Subcapturing.lean
+++ b/Cappy/Translation/Subcapturing.lean
@@ -33,4 +33,24 @@ theorem subcapt_enc_monotonic
     cases hi1; cases hi2
     assumption
 
+theorem subcapt_enc_monotonic_alt
+  (hg : Context.Interp Γ ⟨Δ, ρ⟩)
+  (hsc : Subcapt Γ C1 C2)
+  (hi1 : CaptureSet.Interp ρ Γ C1 D1 I1) :
+  ∃ D2 I2, CaptureSet.Interp ρ Γ C2 D2 I2 ∧ Δ ⊢ I1 <:c I2 := by
+  induction hsc generalizing D1 I1
+  case sc_trans ih1 ih2 =>
+    have ⟨D2, I2, hi2, hsc2⟩ := ih1 hi1
+    have ⟨D3, I3, hi3, hsc3⟩ := ih2 hi2
+    have hsc0 := Capless.Subcapt.trans hsc2 hsc3
+    aesop
+  case sc_var hb1 =>
+    cases hi1; rename_i hb2 hi1
+    have h := Context.bound_inj hb1 hb2
+    cases h
+    have hsc0 := Capless.Subcapt.refl (Γ := Δ) (C := I1)
+    aesop
+  case sc_elem => sorry
+  case sc_set => sorry
+
 end Cappy

From f5120978b8ecd08890f56a34c280a5327a7a7196 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Mon, 28 Oct 2024 16:44:03 +0100
Subject: [PATCH 27/42] cappy: capset interp is complete, attempt 1

---
 .../Encoding/CaptureSet/Properties.lean       | 89 +++++++++++++++++++
 1 file changed, 89 insertions(+)

diff --git a/Cappy/Translation/Encoding/CaptureSet/Properties.lean b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
index de2b303a..9d0774f4 100644
--- a/Cappy/Translation/Encoding/CaptureSet/Properties.lean
+++ b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
@@ -14,4 +14,93 @@ theorem CaptureSet.interp_inj
     have h := Context.bound_inj hb1 hb2
     aesop
 
+theorem CaptureSet.weaken_union {C1 C2 : CaptureSet n} :
+  (C1 ∪ C2).weaken = C1.weaken ∪ C2.weaken := by
+  simp [CaptureSet.weaken, CaptureSet.rename]
+
+theorem CType.weaken_capt :
+  (S^C : CType n m).weaken = S.weaken^C.weaken := by
+  simp [CType.weaken, CType.rename, CaptureSet.weaken, SType.weaken, RenameFun.weaken]
+
+theorem Capless.CaptureSet.weaken_union {C1 C2 : Capless.CaptureSet n k} :
+  (C1 ∪ C2).weaken = C1.weaken ∪ C2.weaken := by
+  simp [Capless.CaptureSet.weaken, Capless.CaptureSet.rename]
+
+theorem Capless.CaptureSet.cweaken_union {C1 C2 : Capless.CaptureSet n k} :
+  (C1 ∪ C2).cweaken = C1.cweaken ∪ C2.cweaken := by
+  simp [Capless.CaptureSet.cweaken, Capless.CaptureSet.crename]
+
+theorem Capless.CaptureSet.weaken_csingleton :
+  ({c=x} : Capless.CaptureSet n k).weaken = {c=x} := by
+  simp [Capless.CaptureSet.weaken, Capless.CaptureSet.rename]
+
+theorem TMap.ext_reach_succ {ρ : TMap n m k} :
+  ρ.ext.reach x.succ = (ρ.reach x).succ := by
+  simp [TMap.ext, Capless.FinFun.ext]
+
+theorem CaptureSet.interp_weaken
+  (hi : CaptureSet.Interp ρ Γ C D I) :
+  CaptureSet.Interp ρ.ext (Γ.var P) C.weaken D.cweaken.weaken I.cweaken.weaken := by
+  induction hi
+  case i_empty =>
+    simp [CaptureSet.weaken, CaptureSet.rename]
+    simp [Capless.CaptureSet.weaken, Capless.CaptureSet.rename]
+    constructor
+  case i_union ih1 ih2 =>
+    rw [CaptureSet.weaken_union]
+    rw [Capless.CaptureSet.cweaken_union, Capless.CaptureSet.weaken_union]
+    constructor <;> assumption
+  case i_singleton hb hi0 ih =>
+    simp [CaptureSet.weaken, CaptureSet.rename, Capless.FinFun.weaken]
+    have hb1 := Context.Bound.there_var (T' := P) hb
+    constructor
+    exact hb1
+    rw [TMap.ext_reach_succ]
+    rw [Capless.CaptureSet.cweaken_csingleton] at ih
+    rw [Capless.CaptureSet.weaken_csingleton] at ih
+    exact ih
+  case i_reach =>
+    simp [CaptureSet.weaken, CaptureSet.rename]
+    constructor
+  case i_cap =>
+    simp [CaptureSet.weaken, CaptureSet.rename]
+    constructor
+
+theorem CaptureSet.interp_complete :
+  ∃ I, CaptureSet.Interp ρ Γ C D I := by
+  rename_i n m k
+  induction n generalizing m k
+  case zero =>
+    induction C generalizing D
+    case empty => constructor; constructor
+    case union ih1 ih2 =>
+      have ⟨I1, ih1⟩ := ih1 (D := D)
+      have ⟨I2, ih2⟩ := ih2 (D := D)
+      constructor; constructor <;> assumption
+    case singleton x0 => apply Fin.elim0; assumption
+    case reach => constructor; constructor
+    case universal => constructor; constructor
+  case succ n0 ih =>
+    induction C generalizing D
+    case empty => constructor; constructor
+    case union ih1 ih2 =>
+      have ⟨I1, ih1⟩ := ih1 (D := D)
+      have ⟨I2, ih2⟩ := ih2 (D := D)
+      constructor; constructor <;> assumption
+    case singleton x0 =>
+      cases x0 using Fin.cases
+      case zero =>
+        cases Γ; rename_i Γ0 P
+        cases P; rename_i C S
+        have hb0 := Context.Bound.here (Γ := Γ0) (T := (S^C))
+        rw [CType.weaken_capt] at hb0
+        constructor
+        constructor
+        { exact hb0 }
+        { sorry }
+        all_goals sorry
+      case succ x0 => sorry
+    case reach => constructor; constructor
+    case universal => constructor; constructor
+
 end Cappy

From eefb1279ed160dcca9e334fa40e84d1f72337456 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Mon, 28 Oct 2024 17:03:29 +0100
Subject: [PATCH 28/42] wip

---
 .../Encoding/CaptureSet/Properties.lean       | 34 +++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/Cappy/Translation/Encoding/CaptureSet/Properties.lean b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
index 9d0774f4..c1b407e6 100644
--- a/Cappy/Translation/Encoding/CaptureSet/Properties.lean
+++ b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
@@ -66,6 +66,40 @@ theorem CaptureSet.interp_weaken
     simp [CaptureSet.weaken, CaptureSet.rename]
     constructor
 
+inductive CaptureSet.Lift : CaptureSet n -> CaptureSet n' -> Prop where
+| refl : CaptureSet.Lift C C
+| step :
+  CaptureSet.Lift C C' ->
+  CaptureSet.Lift C C'.weaken
+
+theorem CaptureSet.lift_empty'
+  (he : C0 = {})
+  (hl : CaptureSet.Lift C0 C) : C = {} := by
+  induction hl
+  case refl => assumption
+  case step hl => aesop
+
+theorem CaptureSet.lift_empty
+  (hl : CaptureSet.Lift ({} : CaptureSet n) C) : C = {} :=
+  CaptureSet.lift_empty' rfl hl
+
+theorem CaptureSet.interp_complete'
+  (hl : CaptureSet.Lift C C') :
+  ∃ I, CaptureSet.Interp ρ Γ C' D I := by
+  rename_i n n' m k
+  induction n generalizing n' m k
+  case zero =>
+    induction C generalizing C' D
+    case empty =>
+      have h := CaptureSet.lift_empty hl
+      cases h
+      constructor; constructor
+    case union => sorry
+    case singleton => sorry
+    case reach => sorry
+    case universal => sorry
+  case succ => sorry
+
 theorem CaptureSet.interp_complete :
   ∃ I, CaptureSet.Interp ρ Γ C D I := by
   rename_i n m k

From b060a7c627e46de96b8956e1cdfd64b2eb14dbdf Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Tue, 29 Oct 2024 01:15:36 +0100
Subject: [PATCH 29/42] cappy: wip

---
 .../Encoding/CaptureSet/Properties.lean       | 33 ++++++++++++++++++-
 1 file changed, 32 insertions(+), 1 deletion(-)

diff --git a/Cappy/Translation/Encoding/CaptureSet/Properties.lean b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
index c1b407e6..279600d9 100644
--- a/Cappy/Translation/Encoding/CaptureSet/Properties.lean
+++ b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
@@ -83,6 +83,32 @@ theorem CaptureSet.lift_empty
   (hl : CaptureSet.Lift ({} : CaptureSet n) C) : C = {} :=
   CaptureSet.lift_empty' rfl hl
 
+theorem CaptureSet.lift_union'
+  (he : C0 = C1 ∪ C2)
+  (hl : CaptureSet.Lift C0 D) :
+  ∃ D1 D2, CaptureSet.Lift C1 D1 ∧ CaptureSet.Lift C2 D2 ∧ D = D1 ∪ D2 := by
+  induction hl
+  case refl =>
+    constructor; constructor
+    constructor; constructor
+    constructor; constructor
+    assumption
+  case step hl ih =>
+    have ih := ih he
+    have ⟨D1, D2, ih1, ih2, he⟩ := ih
+    apply Exists.intro D1.weaken
+    apply Exists.intro D2.weaken
+    constructor
+    constructor; assumption
+    constructor
+    constructor; assumption
+    rw [he, CaptureSet.weaken_union]
+
+theorem CaptureSet.lift_union
+  (hl : CaptureSet.Lift (C1 ∪ C2) D) :
+  ∃ D1 D2, CaptureSet.Lift C1 D1 ∧ CaptureSet.Lift C2 D2 ∧ D = D1 ∪ D2 := by
+  apply CaptureSet.lift_union' rfl hl
+
 theorem CaptureSet.interp_complete'
   (hl : CaptureSet.Lift C C') :
   ∃ I, CaptureSet.Interp ρ Γ C' D I := by
@@ -94,7 +120,12 @@ theorem CaptureSet.interp_complete'
       have h := CaptureSet.lift_empty hl
       cases h
       constructor; constructor
-    case union => sorry
+    case union ih1 ih2 =>
+      have ⟨D1, D2, hl1, hl2, he⟩ := CaptureSet.lift_union hl
+      have ⟨I1, hi1⟩ := ih1 (D := D) hl1
+      have ⟨I2, hi2⟩ := ih2 (D := D) hl2
+      rw [he]
+      constructor; constructor <;> assumption
     case singleton => sorry
     case reach => sorry
     case universal => sorry

From 61dc22eda63a7c023f732af908bbc321b9ad7c55 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Tue, 29 Oct 2024 13:23:37 +0100
Subject: [PATCH 30/42] cappy: wip

---
 Cappy/Syntax/Context/Properties.lean          |  28 +++
 .../Encoding/CaptureSet/Properties.lean       | 221 ++++++++++++------
 2 files changed, 181 insertions(+), 68 deletions(-)

diff --git a/Cappy/Syntax/Context/Properties.lean b/Cappy/Syntax/Context/Properties.lean
index e55f01e6..18209fc7 100644
--- a/Cappy/Syntax/Context/Properties.lean
+++ b/Cappy/Syntax/Context/Properties.lean
@@ -30,4 +30,32 @@ theorem Context.bound_inj
     have ih := ih hb2
     aesop
 
+theorem Context.bound_exists {x : Fin n} {Γ : Context n m} :
+  ∃ T, Context.Bound Γ x T := by
+  induction Γ
+  case empty => apply Fin.elim0 x
+  case var ih =>
+    cases x using Fin.cases
+    case zero => constructor; constructor
+    case succ x0 =>
+      have ⟨T0, ih⟩ := ih (x := x0)
+      constructor; constructor
+      assumption
+  case tvar ih =>
+    have ⟨T0, ih⟩ := ih (x := x)
+    constructor; constructor
+    assumption
+
+theorem Context.var_bound_succ_exists {x : Fin (n+1)} {Γ : Context (n+1) m} :
+  ∃ T, Context.Bound Γ x (CType.weaken T) := by
+  cases Γ
+  case var Γ0 P0 =>
+    cases x using Fin.cases
+    case zero => constructor; constructor
+    case succ x0 =>
+      have ⟨T0, h0⟩ := Context.bound_exists (Γ := Γ0) (x := x0)
+      constructor; constructor
+      assumption
+  case tvar Γ0 R0 => sorry
+
 end Cappy
diff --git a/Cappy/Translation/Encoding/CaptureSet/Properties.lean b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
index 279600d9..5f622b2c 100644
--- a/Cappy/Translation/Encoding/CaptureSet/Properties.lean
+++ b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
@@ -40,31 +40,30 @@ theorem TMap.ext_reach_succ {ρ : TMap n m k} :
 
 theorem CaptureSet.interp_weaken
   (hi : CaptureSet.Interp ρ Γ C D I) :
-  CaptureSet.Interp ρ.ext (Γ.var P) C.weaken D.cweaken.weaken I.cweaken.weaken := by
-  induction hi
+  ∃ I', CaptureSet.Interp ρ' (Γ.var P) C.weaken D' I' := by
+  induction hi generalizing ρ' D'
   case i_empty =>
-    simp [CaptureSet.weaken, CaptureSet.rename]
-    simp [Capless.CaptureSet.weaken, Capless.CaptureSet.rename]
-    constructor
+    simp [weaken, rename]
+    constructor; constructor
   case i_union ih1 ih2 =>
+    have ⟨I1, ih1⟩ := ih1 (ρ' := ρ') (D' := D')
+    have ⟨I2, ih2⟩ := ih2 (ρ' := ρ') (D' := D')
     rw [CaptureSet.weaken_union]
-    rw [Capless.CaptureSet.cweaken_union, Capless.CaptureSet.weaken_union]
-    constructor <;> assumption
-  case i_singleton hb hi0 ih =>
-    simp [CaptureSet.weaken, CaptureSet.rename, Capless.FinFun.weaken]
+    constructor; constructor <;> assumption
+  case i_singleton x0 _ _ _ _ _ hb _ ih =>
     have hb1 := Context.Bound.there_var (T' := P) hb
-    constructor
-    exact hb1
-    rw [TMap.ext_reach_succ]
-    rw [Capless.CaptureSet.cweaken_csingleton] at ih
-    rw [Capless.CaptureSet.weaken_csingleton] at ih
-    exact ih
+    simp [CType.weaken_capt] at hb1
+    simp [weaken, rename, Capless.FinFun.weaken]
+    have ⟨I, ih⟩ := ih (ρ' := ρ') (D' := {c=ρ'.reach x0.succ})
+    constructor; constructor
+    { exact hb1 }
+    { exact ih }
   case i_reach =>
-    simp [CaptureSet.weaken, CaptureSet.rename]
-    constructor
+    simp [weaken, rename, Capless.FinFun.weaken]
+    constructor; constructor
   case i_cap =>
-    simp [CaptureSet.weaken, CaptureSet.rename]
-    constructor
+    simp [weaken, rename]
+    constructor; constructor
 
 inductive CaptureSet.Lift : CaptureSet n -> CaptureSet n' -> Prop where
 | refl : CaptureSet.Lift C C
@@ -109,63 +108,149 @@ theorem CaptureSet.lift_union
   ∃ D1 D2, CaptureSet.Lift C1 D1 ∧ CaptureSet.Lift C2 D2 ∧ D = D1 ∪ D2 := by
   apply CaptureSet.lift_union' rfl hl
 
-theorem CaptureSet.interp_complete'
-  (hl : CaptureSet.Lift C C') :
-  ∃ I, CaptureSet.Interp ρ Γ C' D I := by
-  rename_i n n' m k
-  induction n generalizing n' m k
-  case zero =>
-    induction C generalizing C' D
-    case empty =>
-      have h := CaptureSet.lift_empty hl
-      cases h
-      constructor; constructor
-    case union ih1 ih2 =>
-      have ⟨D1, D2, hl1, hl2, he⟩ := CaptureSet.lift_union hl
-      have ⟨I1, hi1⟩ := ih1 (D := D) hl1
-      have ⟨I2, hi2⟩ := ih2 (D := D) hl2
-      rw [he]
-      constructor; constructor <;> assumption
-    case singleton => sorry
-    case reach => sorry
-    case universal => sorry
-  case succ => sorry
-
-theorem CaptureSet.interp_complete :
-  ∃ I, CaptureSet.Interp ρ Γ C D I := by
-  rename_i n m k
-  induction n generalizing m k
-  case zero =>
-    induction C generalizing D
+theorem CaptureSet.lift_cap'
+  (he : C0 = {cap})
+  (hl : CaptureSet.Lift C0 D) :
+  D = {cap} := by
+  induction hl
+  case refl => aesop
+  case step ih =>
+    have ih := ih he
+    rw [ih]
+    simp [CaptureSet.weaken, CaptureSet.rename]
+
+theorem CaptureSet.lift_cap
+  (hl : CaptureSet.Lift ({cap} : CaptureSet n) D) :
+  D = {cap} :=
+  CaptureSet.lift_cap' rfl hl
+
+theorem CaptureSet.lift_reach'
+  (he : C0 = {x*=x})
+  (hl : CaptureSet.Lift C0 D) :
+  ∃ y, D = {x*=y} := by
+  induction hl
+  case refl => aesop
+  case step ih =>
+    have ⟨y0, ih⟩ := ih he
+    rw [ih]
+    simp [CaptureSet.weaken, CaptureSet.rename]
+
+theorem CaptureSet.lift_reach
+  (hl : CaptureSet.Lift {x*=xC0} D) :
+  ∃ y, D = {x*=y} :=
+  CaptureSet.lift_reach' rfl hl
+
+-- theorem CaptureSet.interp_complete'
+--   (hl : CaptureSet.Lift C C') :
+--   ∃ I, CaptureSet.Interp ρ Γ C' D I := by
+--   rename_i n n' m k
+--   induction n generalizing n' m k
+--   case zero =>
+--     induction C generalizing C' D
+--     case empty =>
+--       have h := CaptureSet.lift_empty hl
+--       cases h
+--       constructor; constructor
+--     case union ih1 ih2 =>
+--       have ⟨D1, D2, hl1, hl2, he⟩ := CaptureSet.lift_union hl
+--       have ⟨I1, hi1⟩ := ih1 (D := D) hl1
+--       have ⟨I2, hi2⟩ := ih2 (D := D) hl2
+--       rw [he]
+--       constructor; constructor <;> assumption
+--     case singleton x0 => apply Fin.elim0 x0
+--     case reach x0 => apply Fin.elim0 x0
+--     case universal =>
+--       have h := CaptureSet.lift_cap hl
+--       rw [h]
+--       constructor; constructor
+--   case succ n0 ih =>
+--     induction C generalizing C' D
+--     case empty =>
+--       have h := CaptureSet.lift_empty hl
+--       cases h
+--       constructor; constructor
+--     case union ih1 ih2 =>
+--       have ⟨D1, D2, hl1, hl2, he⟩ := CaptureSet.lift_union hl
+--       have ⟨I1, hi1⟩ := ih1 (D := D) hl1
+--       have ⟨I2, hi2⟩ := ih2 (D := D) hl2
+--       rw [he]
+--       constructor; constructor <;> assumption
+--     case singleton x =>
+--       cases x using Fin.cases
+--       case zero => sorry
+--       case succ x0 => sorry
+--     case reach =>
+--       have ⟨y0, h0⟩ := CaptureSet.lift_reach hl
+--       rw [h0]
+--       constructor; constructor
+--     case universal =>
+--       have h := CaptureSet.lift_cap hl
+--       cases h
+--       constructor; constructor
+
+def CaptureSet.InterpComplete (Γ : Context n m) :=
+  ∀ {k} (ρ : TMap n m k) C D, ∃ I, CaptureSet.Interp ρ Γ C D I
+
+theorem CaptureSet.interp_complete' :
+  InterpComplete Γ := by
+  induction Γ <;> (unfold InterpComplete; intro k ρ C D)
+  case empty =>
+    induction C
     case empty => constructor; constructor
     case union ih1 ih2 =>
-      have ⟨I1, ih1⟩ := ih1 (D := D)
-      have ⟨I2, ih2⟩ := ih2 (D := D)
+      have ⟨I1, ih1⟩ := ih1
+      have ⟨I2, ih2⟩ := ih2
       constructor; constructor <;> assumption
-    case singleton x0 => apply Fin.elim0; assumption
-    case reach => constructor; constructor
+    case singleton x0 => apply Fin.elim0 x0
+    case reach x0 => apply Fin.elim0 x0
     case universal => constructor; constructor
-  case succ n0 ih =>
-    induction C generalizing D
+  case var Γ0 P0 ih =>
+    induction C
     case empty => constructor; constructor
     case union ih1 ih2 =>
-      have ⟨I1, ih1⟩ := ih1 (D := D)
-      have ⟨I2, ih2⟩ := ih2 (D := D)
+      have ⟨I1, ih1⟩ := ih1
+      have ⟨I2, ih2⟩ := ih2
       constructor; constructor <;> assumption
-    case singleton x0 =>
-      cases x0 using Fin.cases
-      case zero =>
-        cases Γ; rename_i Γ0 P
-        cases P; rename_i C S
-        have hb0 := Context.Bound.here (Γ := Γ0) (T := (S^C))
-        rw [CType.weaken_capt] at hb0
-        constructor
-        constructor
-        { exact hb0 }
-        { sorry }
-        all_goals sorry
-      case succ x0 => sorry
+    case singleton x0 => sorry
     case reach => constructor; constructor
     case universal => constructor; constructor
+  case tvar Γ0 S0 ih => sorry
+
+-- theorem CaptureSet.interp_complete :
+--   ∃ I, CaptureSet.Interp ρ Γ C D I := by
+--   rename_i n m k
+--   induction n generalizing m k
+--   case zero =>
+--     induction C generalizing D
+--     case empty => constructor; constructor
+--     case union ih1 ih2 =>
+--       have ⟨I1, ih1⟩ := ih1 (D := D)
+--       have ⟨I2, ih2⟩ := ih2 (D := D)
+--       constructor; constructor <;> assumption
+--     case singleton x0 => apply Fin.elim0; assumption
+--     case reach => constructor; constructor
+--     case universal => constructor; constructor
+--   case succ n0 ih =>
+--     induction C generalizing D
+--     case empty => constructor; constructor
+--     case union ih1 ih2 =>
+--       have ⟨I1, ih1⟩ := ih1 (D := D)
+--       have ⟨I2, ih2⟩ := ih2 (D := D)
+--       constructor; constructor <;> assumption
+--     case singleton x0 =>
+--       cases x0 using Fin.cases
+--       case zero =>
+--         cases Γ; rename_i Γ0 P
+--         cases P; rename_i C S
+--         have hb0 := Context.Bound.here (Γ := Γ0) (T := (S^C))
+--         rw [CType.weaken_capt] at hb0
+--         constructor
+--         constructor
+--         { exact hb0 }
+--         { sorry }
+--         all_goals sorry
+--       case succ x0 => sorry
+--     case reach => constructor; constructor
+--     case universal => constructor; constructor
 
 end Cappy

From 22abb209a71e2904caafd45f43666cfff0aca4fd Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Wed, 30 Oct 2024 01:36:42 +0100
Subject: [PATCH 31/42] cappy: capset renaming composes

---
 Cappy/Syntax/CaptureSet.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/Cappy/Syntax/CaptureSet.lean b/Cappy/Syntax/CaptureSet.lean
index e4d40510..d7c791b7 100644
--- a/Cappy/Syntax/CaptureSet.lean
+++ b/Cappy/Syntax/CaptureSet.lean
@@ -70,4 +70,11 @@ def CapSubst.open_cap (D : CaptureSet n) : CapSubst n n :=
 def CaptureSet.open_cap (C : CaptureSet n) (D : CaptureSet n) : CaptureSet n :=
   C.subst (CapSubst.open_cap D)
 
+theorem CaptureSet.rename_comp {C : CaptureSet n} :
+  (C.rename f).rename g = C.rename (g.comp f) := by
+  induction C generalizing f g <;> try (solve | simp [rename])
+  case union ih1 ih2 =>
+    simp [rename]
+    aesop
+
 end Cappy

From 8dac5c725fce4d808eab11436a5255799db53e20 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Wed, 30 Oct 2024 01:43:44 +0100
Subject: [PATCH 32/42] cappy: type renaming props

---
 Cappy/Renaming.lean               | 12 +++++++
 Cappy/Syntax/Type.lean            | 57 ++-----------------------------
 Cappy/Syntax/Type/Core.lean       | 55 +++++++++++++++++++++++++++++
 Cappy/Syntax/Type/Properties.lean | 38 +++++++++++++++++++++
 4 files changed, 107 insertions(+), 55 deletions(-)
 create mode 100644 Cappy/Syntax/Type/Core.lean
 create mode 100644 Cappy/Syntax/Type/Properties.lean

diff --git a/Cappy/Renaming.lean b/Cappy/Renaming.lean
index 78ffc6f0..a49bae09 100644
--- a/Cappy/Renaming.lean
+++ b/Cappy/Renaming.lean
@@ -18,5 +18,17 @@ def RenameFun.weaken : RenameFun n m (n+1) m :=
 def RenameFun.tweaken : RenameFun n m n (m+1) :=
   { map := Capless.FinFun.id, tmap := Capless.FinFun.weaken }
 
+def RenameFun.comp (g : RenameFun n' m' n'' m'') (f : RenameFun n m n' m') : RenameFun n m n'' m'' :=
+  { map := g.map ∘ f.map, tmap := g.tmap ∘ f.tmap }
+
+theorem RenameFun.comp_ext {g : RenameFun n' m' n'' m''} {f : RenameFun n m n' m'} :
+  (g.comp f).ext = g.ext.comp f.ext := by
+  simp [RenameFun.comp, RenameFun.ext]
+  simp [Capless.FinFun.ext_comp_ext]
+
+theorem RenameFun.comp_text {g : RenameFun n' m' n'' m''} {f : RenameFun n m n' m'} :
+  (g.comp f).text = g.text.comp f.text := by
+  simp [RenameFun.comp, RenameFun.text]
+  simp [Capless.FinFun.ext_comp_ext]
 
 end Cappy
diff --git a/Cappy/Syntax/Type.lean b/Cappy/Syntax/Type.lean
index 711d0698..fb18a5d7 100644
--- a/Cappy/Syntax/Type.lean
+++ b/Cappy/Syntax/Type.lean
@@ -1,55 +1,2 @@
-import Cappy.Syntax.CaptureSet
-import Cappy.Renaming
-
-namespace Cappy
-
-inductive Annot : Type where
-| eps : Annot
-| use : Annot
-
-mutual
-
-inductive CType : Nat -> Nat -> Type where
-| capt : CaptureSet n -> SType n m -> CType n m
-
-inductive SType : Nat -> Nat -> Type where
-| top : SType n m
-| tvar : Fin m -> SType n m
-| arrow : Annot -> CType n m -> CType (n+1) m -> SType n m
-| tarrow : SType n m -> CType n (m+1) -> SType n m
-| boxed : CType n m -> SType n m
-
-end
-
-notation:max S "^" C => CType.capt C S
-notation:50 "∀(x:" T ")" U => SType.arrow Annot.eps T U
-notation:50 "∀(use x:" T ")" U => SType.arrow Annot.use T U
-notation:50 "∀[X<:" S "]" T => SType.tarrow S T
-
-mutual
-
-def CType.rename : CType n m -> RenameFun n m n' m' -> CType n' m'
-| CType.capt C S, f => (S.rename f)^(C.rename f.map)
-
-def SType.rename : SType n m -> RenameFun n m n' m' -> SType n' m'
-| SType.top, _ => SType.top
-| SType.tvar x, f => SType.tvar (f.tmap x)
-| SType.arrow a T U, f => SType.arrow a (T.rename f) (U.rename f.ext)
-| SType.tarrow S T, f => SType.tarrow (S.rename f) (T.rename f.text)
-| SType.boxed C, f => SType.boxed (C.rename f)
-
-end
-
-def CType.weaken (T : CType n m) : CType (n+1) m :=
-  T.rename RenameFun.weaken
-
-def SType.weaken (T : SType n m) : SType (n+1) m :=
-  T.rename RenameFun.weaken
-
-def CType.tweaken (T : CType n m) : CType n (m+1) :=
-  T.rename RenameFun.tweaken
-
-def SType.tweaken (T : SType n m) : SType n (m+1) :=
-  T.rename RenameFun.tweaken
-
-end Cappy
+import Cappy.Syntax.Type.Core
+import Cappy.Syntax.Type.Properties
diff --git a/Cappy/Syntax/Type/Core.lean b/Cappy/Syntax/Type/Core.lean
new file mode 100644
index 00000000..711d0698
--- /dev/null
+++ b/Cappy/Syntax/Type/Core.lean
@@ -0,0 +1,55 @@
+import Cappy.Syntax.CaptureSet
+import Cappy.Renaming
+
+namespace Cappy
+
+inductive Annot : Type where
+| eps : Annot
+| use : Annot
+
+mutual
+
+inductive CType : Nat -> Nat -> Type where
+| capt : CaptureSet n -> SType n m -> CType n m
+
+inductive SType : Nat -> Nat -> Type where
+| top : SType n m
+| tvar : Fin m -> SType n m
+| arrow : Annot -> CType n m -> CType (n+1) m -> SType n m
+| tarrow : SType n m -> CType n (m+1) -> SType n m
+| boxed : CType n m -> SType n m
+
+end
+
+notation:max S "^" C => CType.capt C S
+notation:50 "∀(x:" T ")" U => SType.arrow Annot.eps T U
+notation:50 "∀(use x:" T ")" U => SType.arrow Annot.use T U
+notation:50 "∀[X<:" S "]" T => SType.tarrow S T
+
+mutual
+
+def CType.rename : CType n m -> RenameFun n m n' m' -> CType n' m'
+| CType.capt C S, f => (S.rename f)^(C.rename f.map)
+
+def SType.rename : SType n m -> RenameFun n m n' m' -> SType n' m'
+| SType.top, _ => SType.top
+| SType.tvar x, f => SType.tvar (f.tmap x)
+| SType.arrow a T U, f => SType.arrow a (T.rename f) (U.rename f.ext)
+| SType.tarrow S T, f => SType.tarrow (S.rename f) (T.rename f.text)
+| SType.boxed C, f => SType.boxed (C.rename f)
+
+end
+
+def CType.weaken (T : CType n m) : CType (n+1) m :=
+  T.rename RenameFun.weaken
+
+def SType.weaken (T : SType n m) : SType (n+1) m :=
+  T.rename RenameFun.weaken
+
+def CType.tweaken (T : CType n m) : CType n (m+1) :=
+  T.rename RenameFun.tweaken
+
+def SType.tweaken (T : SType n m) : SType n (m+1) :=
+  T.rename RenameFun.tweaken
+
+end Cappy
diff --git a/Cappy/Syntax/Type/Properties.lean b/Cappy/Syntax/Type/Properties.lean
new file mode 100644
index 00000000..7aeee880
--- /dev/null
+++ b/Cappy/Syntax/Type/Properties.lean
@@ -0,0 +1,38 @@
+import Cappy.Syntax.Type.Core
+namespace Cappy
+
+mutual
+
+theorem CType.rename_comp {T : CType n m} :
+  (T.rename f).rename g = T.rename (g.comp f) :=
+  match T with
+  | CType.capt C S => by
+    simp [CType.rename]
+    apply And.intro
+    { apply CaptureSet.rename_comp }
+    { apply SType.rename_comp }
+
+theorem SType.rename_comp {S : SType n m} :
+  (S.rename f).rename g = S.rename (g.comp f) :=
+  match S with
+  | SType.top => by simp [SType.rename]
+  | SType.tvar X => by simp [SType.rename, RenameFun.comp]
+  | SType.arrow a T U => by
+    simp [SType.rename]
+    apply And.intro
+    { apply CType.rename_comp }
+    { simp [RenameFun.comp_ext]
+      apply CType.rename_comp }
+  | SType.tarrow S T => by
+    simp [SType.rename]
+    apply And.intro
+    { apply SType.rename_comp }
+    { simp [RenameFun.comp_text]
+      apply CType.rename_comp }
+  | SType.boxed T => by
+    simp [SType.rename]
+    apply CType.rename_comp
+
+end
+
+end Cappy

From e9d4d2290785683609ea104913fb4324afae5e4e Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Wed, 30 Oct 2024 01:48:13 +0100
Subject: [PATCH 33/42] cappy: tweaken and weaken comm

---
 Cappy/Renaming.lean               | 5 +++++
 Cappy/Syntax/Type/Properties.lean | 6 ++++++
 2 files changed, 11 insertions(+)

diff --git a/Cappy/Renaming.lean b/Cappy/Renaming.lean
index a49bae09..217a55da 100644
--- a/Cappy/Renaming.lean
+++ b/Cappy/Renaming.lean
@@ -31,4 +31,9 @@ theorem RenameFun.comp_text {g : RenameFun n' m' n'' m''} {f : RenameFun n m n'
   simp [RenameFun.comp, RenameFun.text]
   simp [Capless.FinFun.ext_comp_ext]
 
+theorem RenameFun.weaken_tweaken :
+  tweaken.comp (weaken : RenameFun n m (n+1) m) = weaken.comp tweaken := by
+  simp [tweaken, weaken, comp]
+  aesop
+
 end Cappy
diff --git a/Cappy/Syntax/Type/Properties.lean b/Cappy/Syntax/Type/Properties.lean
index 7aeee880..f3e13988 100644
--- a/Cappy/Syntax/Type/Properties.lean
+++ b/Cappy/Syntax/Type/Properties.lean
@@ -35,4 +35,10 @@ theorem SType.rename_comp {S : SType n m} :
 
 end
 
+theorem CType.tweaken_weaken {T : CType n m} :
+  T.weaken.tweaken = T.tweaken.weaken := by
+  simp [CType.weaken, CType.tweaken]
+  simp [CType.rename_comp]
+  simp [RenameFun.weaken_tweaken]
+
 end Cappy

From 00e899fa9cada9c0e60d2c564651a1f254a7d2d5 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Wed, 30 Oct 2024 01:49:06 +0100
Subject: [PATCH 34/42] cappy: context props

---
 Cappy/Syntax/Context/Properties.lean | 26 +++++++++++++++-----------
 1 file changed, 15 insertions(+), 11 deletions(-)

diff --git a/Cappy/Syntax/Context/Properties.lean b/Cappy/Syntax/Context/Properties.lean
index 18209fc7..760198bf 100644
--- a/Cappy/Syntax/Context/Properties.lean
+++ b/Cappy/Syntax/Context/Properties.lean
@@ -1,4 +1,5 @@
 import Cappy.Syntax.Context.Core
+import Cappy.Syntax.Type.Properties
 namespace Cappy
 
 theorem Context.var_bound_succ'
@@ -46,16 +47,19 @@ theorem Context.bound_exists {x : Fin n} {Γ : Context n m} :
     constructor; constructor
     assumption
 
-theorem Context.var_bound_succ_exists {x : Fin (n+1)} {Γ : Context (n+1) m} :
-  ∃ T, Context.Bound Γ x (CType.weaken T) := by
-  cases Γ
-  case var Γ0 P0 =>
-    cases x using Fin.cases
-    case zero => constructor; constructor
-    case succ x0 =>
-      have ⟨T0, h0⟩ := Context.bound_exists (Γ := Γ0) (x := x0)
-      constructor; constructor
-      assumption
-  case tvar Γ0 R0 => sorry
+inductive CType.Weakened : CType n m -> Prop where
+| mk :
+  CType.Weakened (CType.weaken T)
+
+theorem Context.bound_weaken
+  (hb : Context.Bound Γ x T) :
+  T.Weakened := by
+  induction hb
+  case here => constructor
+  case there_var => constructor
+  case there_tvar ih =>
+    cases ih
+    simp [CType.tweaken_weaken]
+    constructor
 
 end Cappy

From 7afff695f03349b5f38ec7eb7101a7911af7d9db Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Wed, 30 Oct 2024 11:32:55 +0100
Subject: [PATCH 35/42] cappy: capset rename id

---
 Cappy/Syntax/CaptureSet.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/Cappy/Syntax/CaptureSet.lean b/Cappy/Syntax/CaptureSet.lean
index d7c791b7..4d6b3a16 100644
--- a/Cappy/Syntax/CaptureSet.lean
+++ b/Cappy/Syntax/CaptureSet.lean
@@ -77,4 +77,11 @@ theorem CaptureSet.rename_comp {C : CaptureSet n} :
     simp [rename]
     aesop
 
+theorem CaptureSet.rename_id {C : CaptureSet n} :
+  C.rename Capless.FinFun.id = C := by
+  induction C <;> try (solve | simp [rename, Capless.FinFun.id])
+  case union ih1 ih2 =>
+    simp [rename]
+    aesop
+
 end Cappy

From d81bfbc05b67e169f24aa9ed7ea3840fac1ca0e5 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Wed, 30 Oct 2024 11:37:15 +0100
Subject: [PATCH 36/42] cappy: phew! capset interp is complete

---
 Cappy/Renaming.lean                           |   3 +
 .../Encoding/CaptureSet/Properties.lean       | 190 +++++++-----------
 Cappy/Translation/TMap.lean                   |  20 ++
 3 files changed, 99 insertions(+), 114 deletions(-)

diff --git a/Cappy/Renaming.lean b/Cappy/Renaming.lean
index 217a55da..3be59edd 100644
--- a/Cappy/Renaming.lean
+++ b/Cappy/Renaming.lean
@@ -18,6 +18,9 @@ def RenameFun.weaken : RenameFun n m (n+1) m :=
 def RenameFun.tweaken : RenameFun n m n (m+1) :=
   { map := Capless.FinFun.id, tmap := Capless.FinFun.weaken }
 
+def RenameFun.id : RenameFun n m n m :=
+  { map := Capless.FinFun.id, tmap := Capless.FinFun.id }
+
 def RenameFun.comp (g : RenameFun n' m' n'' m'') (f : RenameFun n m n' m') : RenameFun n m n'' m'' :=
   { map := g.map ∘ f.map, tmap := g.tmap ∘ f.tmap }
 
diff --git a/Cappy/Translation/Encoding/CaptureSet/Properties.lean b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
index 5f622b2c..04263d5a 100644
--- a/Cappy/Translation/Encoding/CaptureSet/Properties.lean
+++ b/Cappy/Translation/Encoding/CaptureSet/Properties.lean
@@ -22,6 +22,11 @@ theorem CType.weaken_capt :
   (S^C : CType n m).weaken = S.weaken^C.weaken := by
   simp [CType.weaken, CType.rename, CaptureSet.weaken, SType.weaken, RenameFun.weaken]
 
+theorem CType.tweaken_capt :
+  (S^C : CType n m).tweaken = S.tweaken^C := by
+  simp [CType.tweaken, CType.rename, SType.tweaken, RenameFun.tweaken]
+  simp [CaptureSet.rename_id]
+
 theorem Capless.CaptureSet.weaken_union {C1 C2 : Capless.CaptureSet n k} :
   (C1 ∪ C2).weaken = C1.weaken ∪ C2.weaken := by
   simp [Capless.CaptureSet.weaken, Capless.CaptureSet.rename]
@@ -38,33 +43,6 @@ theorem TMap.ext_reach_succ {ρ : TMap n m k} :
   ρ.ext.reach x.succ = (ρ.reach x).succ := by
   simp [TMap.ext, Capless.FinFun.ext]
 
-theorem CaptureSet.interp_weaken
-  (hi : CaptureSet.Interp ρ Γ C D I) :
-  ∃ I', CaptureSet.Interp ρ' (Γ.var P) C.weaken D' I' := by
-  induction hi generalizing ρ' D'
-  case i_empty =>
-    simp [weaken, rename]
-    constructor; constructor
-  case i_union ih1 ih2 =>
-    have ⟨I1, ih1⟩ := ih1 (ρ' := ρ') (D' := D')
-    have ⟨I2, ih2⟩ := ih2 (ρ' := ρ') (D' := D')
-    rw [CaptureSet.weaken_union]
-    constructor; constructor <;> assumption
-  case i_singleton x0 _ _ _ _ _ hb _ ih =>
-    have hb1 := Context.Bound.there_var (T' := P) hb
-    simp [CType.weaken_capt] at hb1
-    simp [weaken, rename, Capless.FinFun.weaken]
-    have ⟨I, ih⟩ := ih (ρ' := ρ') (D' := {c=ρ'.reach x0.succ})
-    constructor; constructor
-    { exact hb1 }
-    { exact ih }
-  case i_reach =>
-    simp [weaken, rename, Capless.FinFun.weaken]
-    constructor; constructor
-  case i_cap =>
-    simp [weaken, rename]
-    constructor; constructor
-
 inductive CaptureSet.Lift : CaptureSet n -> CaptureSet n' -> Prop where
 | refl : CaptureSet.Lift C C
 | step :
@@ -140,57 +118,55 @@ theorem CaptureSet.lift_reach
   ∃ y, D = {x*=y} :=
   CaptureSet.lift_reach' rfl hl
 
--- theorem CaptureSet.interp_complete'
---   (hl : CaptureSet.Lift C C') :
---   ∃ I, CaptureSet.Interp ρ Γ C' D I := by
---   rename_i n n' m k
---   induction n generalizing n' m k
---   case zero =>
---     induction C generalizing C' D
---     case empty =>
---       have h := CaptureSet.lift_empty hl
---       cases h
---       constructor; constructor
---     case union ih1 ih2 =>
---       have ⟨D1, D2, hl1, hl2, he⟩ := CaptureSet.lift_union hl
---       have ⟨I1, hi1⟩ := ih1 (D := D) hl1
---       have ⟨I2, hi2⟩ := ih2 (D := D) hl2
---       rw [he]
---       constructor; constructor <;> assumption
---     case singleton x0 => apply Fin.elim0 x0
---     case reach x0 => apply Fin.elim0 x0
---     case universal =>
---       have h := CaptureSet.lift_cap hl
---       rw [h]
---       constructor; constructor
---   case succ n0 ih =>
---     induction C generalizing C' D
---     case empty =>
---       have h := CaptureSet.lift_empty hl
---       cases h
---       constructor; constructor
---     case union ih1 ih2 =>
---       have ⟨D1, D2, hl1, hl2, he⟩ := CaptureSet.lift_union hl
---       have ⟨I1, hi1⟩ := ih1 (D := D) hl1
---       have ⟨I2, hi2⟩ := ih2 (D := D) hl2
---       rw [he]
---       constructor; constructor <;> assumption
---     case singleton x =>
---       cases x using Fin.cases
---       case zero => sorry
---       case succ x0 => sorry
---     case reach =>
---       have ⟨y0, h0⟩ := CaptureSet.lift_reach hl
---       rw [h0]
---       constructor; constructor
---     case universal =>
---       have h := CaptureSet.lift_cap hl
---       cases h
---       constructor; constructor
-
 def CaptureSet.InterpComplete (Γ : Context n m) :=
   ∀ {k} (ρ : TMap n m k) C D, ∃ I, CaptureSet.Interp ρ Γ C D I
 
+theorem CaptureSet.interp_weaken
+  (hi : CaptureSet.Interp ρ Γ C D I) :
+  ∃ I', CaptureSet.Interp ρ' (Γ.var P) C.weaken D' I' := by
+  induction hi generalizing ρ' D'
+  case i_empty =>
+    simp [weaken, rename]
+    constructor; constructor
+  case i_union ih1 ih2 =>
+    have ⟨I1, ih1⟩ := ih1 (ρ' := ρ') (D' := D')
+    have ⟨I2, ih2⟩ := ih2 (ρ' := ρ') (D' := D')
+    rw [CaptureSet.weaken_union]
+    constructor; constructor <;> assumption
+  case i_singleton x0 _ _ _ _ _ hb _ ih =>
+    have hb1 := Context.Bound.there_var (T' := P) hb
+    simp [CType.weaken_capt] at hb1
+    simp [weaken, rename, Capless.FinFun.weaken]
+    have ⟨I, ih⟩ := ih (ρ' := ρ') (D' := {c=ρ'.reach x0.succ})
+    constructor; constructor
+    { exact hb1 }
+    { exact ih }
+  case i_reach =>
+    simp [weaken, rename, Capless.FinFun.weaken]
+    constructor; constructor
+  case i_cap =>
+    simp [weaken, rename]
+    constructor; constructor
+
+theorem CaptureSet.interp_tweaken
+  (hi : CaptureSet.Interp ρ Γ C D I) :
+  ∃ I', CaptureSet.Interp ρ' (Γ.tvar S) C D' I' := by
+  induction hi generalizing ρ' D'
+  case i_empty => constructor; constructor
+  case i_union ih1 ih2 =>
+    have ⟨I1, ih1⟩ := ih1 (ρ' := ρ') (D' := D')
+    have ⟨I2, ih2⟩ := ih2 (ρ' := ρ') (D' := D')
+    constructor; constructor <;> assumption
+  case i_singleton x0 _ _ _ _ _ hb0 _ ih =>
+    have ⟨I0, hi0⟩ := ih (ρ' := ρ') (D' := {c=ρ'.reach x0})
+    have hb := Context.Bound.there_tvar (S := S) hb0
+    simp [CType.tweaken_capt] at hb
+    constructor; constructor
+    { exact hb }
+    { exact hi0 }
+  case i_reach => constructor; constructor
+  case i_cap => constructor; constructor
+
 theorem CaptureSet.interp_complete' :
   InterpComplete Γ := by
   induction Γ <;> (unfold InterpComplete; intro k ρ C D)
@@ -211,46 +187,32 @@ theorem CaptureSet.interp_complete' :
       have ⟨I1, ih1⟩ := ih1
       have ⟨I2, ih2⟩ := ih2
       constructor; constructor <;> assumption
-    case singleton x0 => sorry
+    case singleton x0 =>
+      cases P0; rename_i C0 S0
+      have ⟨T0, hb0⟩ := Context.bound_exists (Γ:=Γ0.var (S0^C0)) (x:=x0)
+      cases hb0
+      case here =>
+        have hb0 := Context.Bound.here (Γ := Γ0) (T := (S0^C0))
+        simp [CType.weaken_capt] at hb0
+        have ⟨I0, ih0⟩ := ih (ρ := ρ.strip) (C := C0) (D := {})
+        have ⟨I1, ih1⟩ := CaptureSet.interp_weaken (ρ':=ρ) (D':={c=ρ.reach 0}) (P:=(S0^C0)) ih0
+        constructor
+        constructor
+        { exact hb0 }
+        { exact ih1 }
+      case there_var x0 T0 hb0 =>
+        have ⟨I0, ih0⟩ := ih (ρ := ρ.strip) (C:={x=x0}) (D:={})
+        have ih1 := CaptureSet.interp_weaken (ρ':=ρ) (D':=D) (P:=(S0^C0)) ih0
+        exact ih1
     case reach => constructor; constructor
     case universal => constructor; constructor
-  case tvar Γ0 S0 ih => sorry
-
--- theorem CaptureSet.interp_complete :
---   ∃ I, CaptureSet.Interp ρ Γ C D I := by
---   rename_i n m k
---   induction n generalizing m k
---   case zero =>
---     induction C generalizing D
---     case empty => constructor; constructor
---     case union ih1 ih2 =>
---       have ⟨I1, ih1⟩ := ih1 (D := D)
---       have ⟨I2, ih2⟩ := ih2 (D := D)
---       constructor; constructor <;> assumption
---     case singleton x0 => apply Fin.elim0; assumption
---     case reach => constructor; constructor
---     case universal => constructor; constructor
---   case succ n0 ih =>
---     induction C generalizing D
---     case empty => constructor; constructor
---     case union ih1 ih2 =>
---       have ⟨I1, ih1⟩ := ih1 (D := D)
---       have ⟨I2, ih2⟩ := ih2 (D := D)
---       constructor; constructor <;> assumption
---     case singleton x0 =>
---       cases x0 using Fin.cases
---       case zero =>
---         cases Γ; rename_i Γ0 P
---         cases P; rename_i C S
---         have hb0 := Context.Bound.here (Γ := Γ0) (T := (S^C))
---         rw [CType.weaken_capt] at hb0
---         constructor
---         constructor
---         { exact hb0 }
---         { sorry }
---         all_goals sorry
---       case succ x0 => sorry
---     case reach => constructor; constructor
---     case universal => constructor; constructor
+  case tvar Γ0 S0 ih =>
+    have ⟨I0, h0⟩ := ih (ρ:=ρ.tstrip) (C:=C) (D:=D)
+    have h1 := CaptureSet.interp_tweaken (ρ':=ρ) (D':=D) (S:=S0) h0
+    exact h1
+
+theorem CaptureSet.interp_complete :
+  ∃ I, CaptureSet.Interp ρ Γ C D I :=
+  CaptureSet.interp_complete' ρ C D
 
 end Cappy
diff --git a/Cappy/Translation/TMap.lean b/Cappy/Translation/TMap.lean
index d506e09b..8d77a296 100644
--- a/Cappy/Translation/TMap.lean
+++ b/Cappy/Translation/TMap.lean
@@ -46,4 +46,24 @@ def TMap.cweaken (ρ : TMap n m k) : TMap n m (k+1) := by
     apply Fin.succ
     aesop
 
+def TMap.strip (ρ : TMap (n+1) m k) : TMap n m k := by
+  constructor
+  case reach =>
+    have h := ρ.reach
+    intro n
+    exact h (n.succ)
+  case treach =>
+    have h := ρ.treach
+    aesop
+
+def TMap.tstrip (ρ : TMap n (m+1) k) : TMap n m k := by
+  constructor
+  case reach =>
+    have h := ρ.reach
+    aesop
+  case treach =>
+    have h := ρ.treach
+    intro m
+    exact h (m.succ)
+
 end Cappy

From 5fb357aecdd5d2070c6942b1e7af075f99cae47c Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Wed, 30 Oct 2024 12:25:43 +0100
Subject: [PATCH 37/42] cappy: the second monotonic thereom for subcapturing

---
 Cappy/Translation/Subcapturing.lean | 52 ++++++++++++++++++++++++++---
 1 file changed, 47 insertions(+), 5 deletions(-)

diff --git a/Cappy/Translation/Subcapturing.lean b/Cappy/Translation/Subcapturing.lean
index 250e2402..dd162917 100644
--- a/Cappy/Translation/Subcapturing.lean
+++ b/Cappy/Translation/Subcapturing.lean
@@ -4,7 +4,7 @@ import Capless.Subcapturing
 import Capless.Subcapturing.Basic
 namespace Cappy
 
-theorem subcapt_enc_monotonic
+theorem CaptureSet.interp_monotonic_subcapt
   (h : Δ ⊢ D1 <:c D2)
   (hi1 : CaptureSet.Interp ρ Γ C D1 I1)
   (hi2 : CaptureSet.Interp ρ Γ C D2 I2) :
@@ -33,8 +33,39 @@ theorem subcapt_enc_monotonic
     cases hi1; cases hi2
     assumption
 
-theorem subcapt_enc_monotonic_alt
-  (hg : Context.Interp Γ ⟨Δ, ρ⟩)
+theorem CaptureSet.interp_monotonic_subset
+  (hi1 : CaptureSet.Interp ρ Γ C1 D I1)
+  (hi2 : CaptureSet.Interp ρ Γ C2 D I2)
+  (hsub : C1 ⊆ C2) :
+  I1 ⊆ I2 := by
+  induction hsub generalizing I1 I2
+  case empty => cases hi1; aesop
+  case rfl =>
+    have h := CaptureSet.interp_inj hi1 hi2
+    aesop
+  case union_l =>
+    cases hi1
+    aesop
+  case union_rl => cases hi2; aesop
+  case union_rr => cases hi2; aesop
+
+theorem CaptureSet.interp_meet
+  (h1 : CaptureSet.Interp ρ Γ C D1 I1)
+  (h2 : CaptureSet.Interp ρ Γ C D2 I2) :
+  ∃ D3 I3,
+    CaptureSet.Interp ρ Γ C D3 I3 ∧
+    (Δ ⊢ I1 <:c I3) ∧ (Δ ⊢ I2 <:c I3) := by
+  have ⟨I3, h3⟩ := CaptureSet.interp_complete (ρ := ρ) (Γ := Γ) (C := C) (D := D1 ∪ D2)
+  apply Exists.intro (D1 ∪ D2)
+  apply Exists.intro I3
+  constructor; assumption
+  constructor
+  { apply CaptureSet.interp_monotonic_subcapt (hi1 := h1) (hi2 := h3)
+    apply Capless.Subcapt.subset; aesop }
+  { apply CaptureSet.interp_monotonic_subcapt (hi1 := h2) (hi2 := h3)
+    apply Capless.Subcapt.subset; aesop }
+
+theorem CaptureSet.interp_monotonic_alt
   (hsc : Subcapt Γ C1 C2)
   (hi1 : CaptureSet.Interp ρ Γ C1 D1 I1) :
   ∃ D2 I2, CaptureSet.Interp ρ Γ C2 D2 I2 ∧ Δ ⊢ I1 <:c I2 := by
@@ -50,7 +81,18 @@ theorem subcapt_enc_monotonic_alt
     cases h
     have hsc0 := Capless.Subcapt.refl (Γ := Δ) (C := I1)
     aesop
-  case sc_elem => sorry
-  case sc_set => sorry
+  case sc_elem C1 C2 hs =>
+    have ⟨I2, hi2⟩ := CaptureSet.interp_complete (ρ:=ρ) (Γ:=Γ) (C:=C2) (D:=D1)
+    have h := CaptureSet.interp_monotonic_subset hi1 hi2 hs
+    have h := Capless.Subcapt.subset (Γ:=Δ) h
+    aesop
+  case sc_set C1 C2 C _ _ ih1 ih2 =>
+    cases hi1; rename_i I11 I12 hi11 hi12
+    have ⟨D21, I21, h21, hs21⟩ := ih1 hi11
+    have ⟨D22, I22, h22, hs22⟩ := ih2 hi12
+    have ⟨D3, I3, hi3, hs1, hs2⟩ := CaptureSet.interp_meet (Δ:=Δ) h21 h22
+    apply Exists.intro D3; apply Exists.intro I3
+    constructor; assumption
+    apply Capless.Subcapt.union <;> (apply Capless.Subcapt.trans <;> assumption)
 
 end Cappy

From 2f1260a433cfa1b0e0ac3e04b4aa725541e665a4 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Wed, 30 Oct 2024 12:28:47 +0100
Subject: [PATCH 38/42] cappy: wip

---
 Cappy/Translation/Subtyping.lean | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 Cappy/Translation/Subtyping.lean

diff --git a/Cappy/Translation/Subtyping.lean b/Cappy/Translation/Subtyping.lean
new file mode 100644
index 00000000..3a8a6268
--- /dev/null
+++ b/Cappy/Translation/Subtyping.lean
@@ -0,0 +1,4 @@
+import Cappy.Translation.Subcapturing
+namespace Cappy
+
+end Cappy

From 31e582854f58b68485d41cd97574d3ca8f6028cf Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Fri, 1 Nov 2024 15:39:44 +0100
Subject: [PATCH 39/42] cappy: towards kernel fsub

---
 Cappy/TypeSystem/Subtyping.lean | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/Cappy/TypeSystem/Subtyping.lean b/Cappy/TypeSystem/Subtyping.lean
index 7ca4e979..3e32e618 100644
--- a/Cappy/TypeSystem/Subtyping.lean
+++ b/Cappy/TypeSystem/Subtyping.lean
@@ -1,6 +1,12 @@
 import Cappy.TypeSystem.Subcapturing
 namespace Cappy
 
+inductive SubAnnot : Annot -> Annot -> Prop where
+| refl :
+  SubAnnot a a
+| use :
+  SubAnnot Annot.eps Annot.use
+
 mutual
 
 inductive CSubtyp : Context n m -> CType n m -> CType n m -> Prop where
@@ -25,16 +31,12 @@ inductive SSubtyp : Context n m -> SType n m -> SType n m -> Prop where
   CSubtyp Γ T1 T2 ->
   SSubtyp Γ (SType.boxed T1) (SType.boxed T2)
 | arrow :
-  CSubtyp Γ T2 T1 ->
-  CSubtyp (Γ.var T2) U1 U2 ->
-  SSubtyp Γ (∀(x:T1)U1) (SType.arrow a T2 U2)
-| uarrow :
+  SubAnnot a1 a2 ->
   CSubtyp (Γ.var T) U1 U2 ->
-  SSubtyp Γ (∀(use x:T)U1) (∀(use x:T)U2)
+  SSubtyp Γ (SType.arrow a1 T U1) (SType.arrow a2 T U2)
 | tarrow :
-  SSubtyp Γ S2 S1 ->
-  CSubtyp (Γ.tvar S2) T1 T2 ->
-  SSubtyp Γ (∀[X<:S1]T1) (∀[X<:S2]T2)
+  CSubtyp (Γ.tvar S) T1 T2 ->
+  SSubtyp Γ (∀[X<:S]T1) (∀[X<:S]T2)
 
 end
 

From 0cf80a7b780484e7272eb2eaaaef2faa2955bfe9 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Sat, 2 Nov 2024 17:45:59 +0100
Subject: [PATCH 40/42] cappy: revise the translation of universal types

---
 Cappy/Translation/Encoding/Type.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cappy/Translation/Encoding/Type.lean b/Cappy/Translation/Encoding/Type.lean
index 4e7c4703..7e2a8a90 100644
--- a/Cappy/Translation/Encoding/Type.lean
+++ b/Cappy/Translation/Encoding/Type.lean
@@ -40,7 +40,7 @@ inductive CType.Interp : TMap n m k -> Context n m -> CType n m -> Capless.Captu
 | i_tarrow :
   CaptureSet.Interp ρ Γ C D C' ->
   CType.Interp ρ.cweaken Γ (S^{}) ({c=0}) (S'^{}) ->
-  CType.Interp ρ.text (Γ.tvar S) T (D.cweaken) T' ->
+  CType.Interp ρ.text (Γ.tvar S) T (D.cweaken ∪ {c=0}) T' ->
   CType.Interp ρ Γ
     ((∀[X<:S]T)^C)
     D

From 05807892730d8bd17d70f77e2dec145e96f76a20 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Sat, 2 Nov 2024 17:46:12 +0100
Subject: [PATCH 41/42] cappy: subtyping translation proof

---
 Cappy/Translation/Subtyping.lean | 47 ++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)

diff --git a/Cappy/Translation/Subtyping.lean b/Cappy/Translation/Subtyping.lean
index 3a8a6268..a96f73ae 100644
--- a/Cappy/Translation/Subtyping.lean
+++ b/Cappy/Translation/Subtyping.lean
@@ -1,4 +1,51 @@
 import Cappy.Translation.Subcapturing
+import Cappy.TypeSystem
+import Capless.Subtyping
 namespace Cappy
 
+def CType.interp_monotonic.motive_1
+  (Γ : Context n m)
+  (T1 T2 : CType n m)
+  (_ : CSubtyp Γ T1 T2) : Prop :=
+  ∀ {k} {Δ : Capless.Context n m k} {ρ} (_ : Context.Interp Γ ⟨Δ, ρ⟩)
+    {D1 Q1} (_ : CType.Interp ρ Γ T1 D1 Q1),
+  ∃ D2 Q2,
+    CType.Interp ρ Γ T2 D2 Q2 ∧
+    (Δ ⊢ Q1 <: Q2)
+
+def CType.interp_monotonic.motive_2
+  (Γ : Context n m)
+  (S1 S2 : SType n m)
+  (_ : SSubtyp Γ S1 S2) : Prop :=
+  ∀ {k} {Δ : Capless.Context n m k} {ρ} (_ : Context.Interp Γ ⟨Δ, ρ⟩)
+    {C D1 Q1} (_ : CType.Interp ρ Γ (S1^C) D1 Q1),
+  ∃ D2 Q2,
+    CType.Interp ρ Γ (S2^C) D2 Q2 ∧
+    (Δ ⊢ Q1 <: Q2)
+
+
+theorem CType.interp_monotonic
+  (hg : Context.Interp Γ ⟨Δ, ρ⟩)
+  (hsub : CSubtyp Γ T1 T2)
+  (hi : CType.Interp ρ Γ T1 D1 Q1) :
+  ∃ D2 Q2,
+    CType.Interp ρ Γ T2 D2 Q2 ∧
+    (Δ ⊢ Q1 <: Q2) := by
+  apply CSubtyp.rec
+    (motive_1 := CType.interp_monotonic.motive_1)
+    (motive_2 := CType.interp_monotonic.motive_2)
+    (t := hsub)
+    (D1 := D1)
+  all_goals try assumption
+  case capt =>
+    repeat intro
+    sorry
+  case top => sorry
+  case refl => sorry
+  case trans => sorry
+  case tvar => sorry
+  case boxed => sorry
+  case arrow => sorry
+  case tarrow => sorry
+
 end Cappy

From 6d9f83e152dba23af1fd0b703a3905b551aa23de Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Sun, 3 Nov 2024 12:39:06 +0000
Subject: [PATCH 42/42] cappy: staging

---
 Cappy/Translation/Subtyping.lean | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/Cappy/Translation/Subtyping.lean b/Cappy/Translation/Subtyping.lean
index a96f73ae..641d1db6 100644
--- a/Cappy/Translation/Subtyping.lean
+++ b/Cappy/Translation/Subtyping.lean
@@ -3,6 +3,13 @@ import Cappy.TypeSystem
 import Capless.Subtyping
 namespace Cappy
 
+theorem CType.interp_monotonic_cs
+  (hi : CType.Interp ρ Γ (S^C1) D1 Q1)
+  (hs : Subcapt Γ C1 C2) :
+  ∃ D2 Q2,
+    CType.Interp ρ Γ (S^C2) D2 Q2 ∧
+    Capless.CSubtyp Δ Q1 Q2 := sorry
+
 def CType.interp_monotonic.motive_1
   (Γ : Context n m)
   (T1 T2 : CType n m)
@@ -23,7 +30,6 @@ def CType.interp_monotonic.motive_2
     CType.Interp ρ Γ (S2^C) D2 Q2 ∧
     (Δ ⊢ Q1 <: Q2)
 
-
 theorem CType.interp_monotonic
   (hg : Context.Interp Γ ⟨Δ, ρ⟩)
   (hsub : CSubtyp Γ T1 T2)
@@ -39,6 +45,8 @@ theorem CType.interp_monotonic
   all_goals try assumption
   case capt =>
     repeat intro
+    rename_i hsc hs ih _ Δ ρ hg D1 Q1 hi1
+    unfold interp_monotonic.motive_2 at ih
     sorry
   case top => sorry
   case refl => sorry