Mechanising the translation

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

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

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

Cappy.lean

@@ -0,0 +1,2 @@
+import Cappy.Syntax
+import Cappy.TypeSystem

Cappy/Renaming.lean

@@ -0,0 +1,42 @@
+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 }
+
+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 }
+
+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]
+
+theorem RenameFun.weaken_tweaken :
+  tweaken.comp (weaken : RenameFun n m (n+1) m) = weaken.comp tweaken := by
+  simp [tweaken, weaken, comp]
+  aesop
+
+end Cappy

Cappy/Syntax.lean

@@ -0,0 +1,4 @@
+import Cappy.Syntax.CaptureSet
+import Cappy.Syntax.Type
+import Cappy.Syntax.Term
+import Cappy.Syntax.Context

Cappy/Syntax/CaptureSet.lean

@@ -0,0 +1,87 @@
+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
+
+@[aesop unsafe [50% constructors]]
+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}
+
+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
+
+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)
+
+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
+
+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

Cappy/Syntax/Context.lean

@@ -0,0 +1,2 @@
+import Cappy.Syntax.Context.Core
+import Cappy.Syntax.Context.Properties

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

Cappy/Syntax/Context/Properties.lean

@@ -0,0 +1,65 @@
+import Cappy.Syntax.Context.Core
+import Cappy.Syntax.Type.Properties
+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
+
+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
+
+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

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

Cappy/Syntax/Type.lean

@@ -0,0 +1,2 @@
+import Cappy.Syntax.Type.Core
+import Cappy.Syntax.Type.Properties

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