From a18337f9b63405cf4a120faed72644c97c4e9f27 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 9 Dec 2024 18:37:57 +0000 Subject: [PATCH 01/84] init system capybara --- Capybara.lean | 1 + Capybara/Syntax.lean | 0 lakefile.lean | 2 ++ 3 files changed, 3 insertions(+) create mode 100644 Capybara.lean create mode 100644 Capybara/Syntax.lean diff --git a/Capybara.lean b/Capybara.lean new file mode 100644 index 00000000..b7ad3ef2 --- /dev/null +++ b/Capybara.lean @@ -0,0 +1 @@ +import «Capybara».Syntax diff --git a/Capybara/Syntax.lean b/Capybara/Syntax.lean new file mode 100644 index 00000000..e69de29b diff --git a/lakefile.lean b/lakefile.lean index a307e98d..1aedd2aa 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 «Capybara» where From 4cf7f497d274b68dace553d03c7cc3a860ad546f Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 9 Dec 2024 18:47:53 +0000 Subject: [PATCH 02/84] add syntax constructs --- Capybara/Syntax/CaptureSet.lean | 10 ++++++++++ Capybara/Syntax/Mode.lean | 12 ++++++++++++ Capybara/Syntax/Term.lean | 16 ++++++++++++++++ Capybara/Syntax/Type.lean | 27 +++++++++++++++++++++++++++ 4 files changed, 65 insertions(+) create mode 100644 Capybara/Syntax/CaptureSet.lean create mode 100644 Capybara/Syntax/Mode.lean create mode 100644 Capybara/Syntax/Term.lean create mode 100644 Capybara/Syntax/Type.lean diff --git a/Capybara/Syntax/CaptureSet.lean b/Capybara/Syntax/CaptureSet.lean new file mode 100644 index 00000000..7a7d8964 --- /dev/null +++ b/Capybara/Syntax/CaptureSet.lean @@ -0,0 +1,10 @@ +import Capybara.Syntax.Mode +namespace Capybara + +inductive CaptureSet : Nat -> Nat -> Type where +| empty : CaptureSet n k +| union : CaptureSet n k -> CaptureSet n k -> CaptureSet n k +| singleton : Fin n -> Mode -> CaptureSet n k +| csingleton : Fin k -> Mode -> CaptureSet n k + +end Capybara diff --git a/Capybara/Syntax/Mode.lean b/Capybara/Syntax/Mode.lean new file mode 100644 index 00000000..96c83592 --- /dev/null +++ b/Capybara/Syntax/Mode.lean @@ -0,0 +1,12 @@ +namespace Capybara + +inductive Mutability : Type where +| readonly : Mutability +| default : Mutability + +inductive Mode : Type where +| M : Mutability -> Mode +| drop : Mode + + +end Capybara diff --git a/Capybara/Syntax/Term.lean b/Capybara/Syntax/Term.lean new file mode 100644 index 00000000..46d03baa --- /dev/null +++ b/Capybara/Syntax/Term.lean @@ -0,0 +1,16 @@ +import Capybara.Syntax.Type +namespace Capybara + +inductive Term : Nat -> Nat -> Nat -> Type where +| var : Fin n -> Term n m k +| lam : CType n m k -> Term (n+1) m k -> Term n m k +| tlam : SType n m k -> Term n (m+1) k -> Term n m k +| clam : Kind -> Term n m (k+1) -> Term n m k +| pack : CaptureSet n k -> Fin n -> Term n m k +| app : Fin n -> Fin n -> Term n m k +| tapp : Fin n -> SType n m k -> Term n m k +| capp : Fin n -> CaptureSet n k -> Term n m k +| letin : Term n m k -> Term (n+1) m k -> Term n m k +| unpack : Term n m k -> Term (n+1) m (k+1) -> Term n m k + +end Capybara diff --git a/Capybara/Syntax/Type.lean b/Capybara/Syntax/Type.lean new file mode 100644 index 00000000..5e9e0148 --- /dev/null +++ b/Capybara/Syntax/Type.lean @@ -0,0 +1,27 @@ +import Capybara.Syntax.CaptureSet +namespace Capybara + +inductive Kind : Type where +| Imm : Kind +| Mut : Kind +| Fresh : Kind + +mutual + +inductive EType : Nat -> Nat -> Nat -> Type where +| type : CType n m k -> EType n m k +| ex : CType n m (k+1) -> EType n m k + +inductive CType : Nat -> Nat -> Nat -> Type where +| capt : CaptureSet n k -> Mutability -> SType n m k -> CType n m k + +inductive SType : Nat -> Nat -> Nat -> Type where +| top : SType n m k +| tvar : Fin m -> SType n m k +| tarrow : SType n m k -> EType n (m+1) k -> SType n m k +| arrow : CType n m k -> EType (n+1) m k -> SType n m k +| carrow : Kind -> EType n m (k+1) -> SType n m k + +end + +end Capybara From 2ec75ec2d0c924abd2c342292010c06d23135d87 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 9 Dec 2024 18:48:37 +0000 Subject: [PATCH 03/84] populate Syntax.lean --- Capybara/Syntax.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Capybara/Syntax.lean b/Capybara/Syntax.lean index e69de29b..1094be29 100644 --- a/Capybara/Syntax.lean +++ b/Capybara/Syntax.lean @@ -0,0 +1,4 @@ +import Capybara.Syntax.Mode +import Capybara.Syntax.CaptureSet +import Capybara.Syntax.Type +import Capybara.Syntax.Term From 4ce82f3534e417d5c3548cfabf12da35ce5710fc Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 9 Dec 2024 19:01:18 +0000 Subject: [PATCH 04/84] capture set renaming --- Capybara/Morphism/Core.lean | 6 ++++++ Capybara/Syntax/CaptureSet.lean | 26 ++++++++++++++++++++++++++ Capybara/Syntax/Mode.lean | 3 +++ 3 files changed, 35 insertions(+) create mode 100644 Capybara/Morphism/Core.lean diff --git a/Capybara/Morphism/Core.lean b/Capybara/Morphism/Core.lean new file mode 100644 index 00000000..2ef985df --- /dev/null +++ b/Capybara/Morphism/Core.lean @@ -0,0 +1,6 @@ +import Mathlib.Data.Fin.Basic +namespace Capybara + +def FinFun (n : Nat) (n' : Nat) : Type := Fin n -> Fin n' + +end Capybara diff --git a/Capybara/Syntax/CaptureSet.lean b/Capybara/Syntax/CaptureSet.lean index 7a7d8964..3a628ca9 100644 --- a/Capybara/Syntax/CaptureSet.lean +++ b/Capybara/Syntax/CaptureSet.lean @@ -1,4 +1,5 @@ import Capybara.Syntax.Mode +import Capybara.Morphism.Core namespace Capybara inductive CaptureSet : Nat -> Nat -> Type where @@ -7,4 +8,29 @@ inductive CaptureSet : Nat -> Nat -> Type where | singleton : Fin n -> Mode -> CaptureSet n k | csingleton : Fin k -> Mode -> CaptureSet n k +instance : EmptyCollection (CaptureSet n k) where + emptyCollection := CaptureSet.empty + +instance : Union (CaptureSet n k) where + union := CaptureSet.union + +notation:40 "{x@" m ":=" x "}" => CaptureSet.singleton x m +notation:40 "{x=" x "}" => {x@ε:=x} +notation:40 "{c@" m ":=" x "}" => CaptureSet.csingleton x m +notation:40 "{c=" x "}" => {c@ε:=x} + +def CaptureSet.rename (C : CaptureSet n k) (f : Fin n -> Fin n') : CaptureSet n' k := + match C with + | empty => {} + | union C1 C2 => (C1.rename f) ∪ (C2.rename f) + | singleton x m => {x@m:=f x} + | csingleton x m => {c@m:=x} + +def CaptureSet.crename (C : CaptureSet n k) (f : Fin k -> Fin k') : CaptureSet n k' := + match C with + | empty => {} + | union C1 C2 => (C1.crename f) ∪ (C2.crename f) + | singleton x m => {x@m:=x} + | csingleton x m => {c@m:=f x} + end Capybara diff --git a/Capybara/Syntax/Mode.lean b/Capybara/Syntax/Mode.lean index 96c83592..aefa647a 100644 --- a/Capybara/Syntax/Mode.lean +++ b/Capybara/Syntax/Mode.lean @@ -8,5 +8,8 @@ inductive Mode : Type where | M : Mutability -> Mode | drop : Mode +notation "ro" => Mode.M Mutability.readonly +notation "ε" => Mode.M Mutability.default +notation "drop" => Mode.drop end Capybara From f0f2bcfa40f5315ea1b936a44332c484a699aab9 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 10 Dec 2024 10:40:50 +0100 Subject: [PATCH 05/84] type renaming, add subst --- Capybara/Morphism/Core.lean | 11 +++++++++ Capybara/Morphism/Subst.lean | 21 ++++++++++++++++ Capybara/Syntax/CaptureSet.lean | 37 +--------------------------- Capybara/Syntax/CaptureSet/Core.lean | 36 +++++++++++++++++++++++++++ Capybara/Syntax/Type.lean | 28 +-------------------- Capybara/Syntax/Type/Core.lean | 32 ++++++++++++++++++++++++ Capybara/Syntax/Type/Renaming.lean | 25 +++++++++++++++++++ 7 files changed, 127 insertions(+), 63 deletions(-) create mode 100644 Capybara/Morphism/Subst.lean create mode 100644 Capybara/Syntax/CaptureSet/Core.lean create mode 100644 Capybara/Syntax/Type/Core.lean create mode 100644 Capybara/Syntax/Type/Renaming.lean diff --git a/Capybara/Morphism/Core.lean b/Capybara/Morphism/Core.lean index 2ef985df..8f326800 100644 --- a/Capybara/Morphism/Core.lean +++ b/Capybara/Morphism/Core.lean @@ -3,4 +3,15 @@ namespace Capybara def FinFun (n : Nat) (n' : Nat) : Type := Fin n -> Fin n' +def FinFun.ext (f : FinFun n n') : FinFun (n+1) (n'+1) := by + intro x + cases x using Fin.cases + case zero => exact 0 + case succ x0 => exact Fin.succ (f x0) + +structure Renaming (n m k n' m' k' : Nat) where + var : FinFun n n' + tvar : FinFun m m' + cvar : FinFun k k' + end Capybara diff --git a/Capybara/Morphism/Subst.lean b/Capybara/Morphism/Subst.lean new file mode 100644 index 00000000..9cdceec7 --- /dev/null +++ b/Capybara/Morphism/Subst.lean @@ -0,0 +1,21 @@ +import Capybara.Syntax.Type +import Capybara.Syntax.CaptureSet +namespace Capybara + +structure Subst (n m k n' m' k' : Nat) where + var : FinFun n n' + tvar : Fin m -> SType n' m' k' + cvar : Fin k -> CaptureSet n' k' + +def Renaming.lift (ρ : Renaming n1 m1 k1 n2 m2 k2) : Subst n1 m1 k1 n2 m2 k2 := by + constructor + case var => exact ρ.var + case tvar => + intro x + apply SType.tvar + exact ρ.tvar x + case cvar => + intro c + exact {c=ρ.cvar c} + +end Capybara diff --git a/Capybara/Syntax/CaptureSet.lean b/Capybara/Syntax/CaptureSet.lean index 3a628ca9..d6c208f1 100644 --- a/Capybara/Syntax/CaptureSet.lean +++ b/Capybara/Syntax/CaptureSet.lean @@ -1,36 +1 @@ -import Capybara.Syntax.Mode -import Capybara.Morphism.Core -namespace Capybara - -inductive CaptureSet : Nat -> Nat -> Type where -| empty : CaptureSet n k -| union : CaptureSet n k -> CaptureSet n k -> CaptureSet n k -| singleton : Fin n -> Mode -> CaptureSet n k -| csingleton : Fin k -> Mode -> CaptureSet n k - -instance : EmptyCollection (CaptureSet n k) where - emptyCollection := CaptureSet.empty - -instance : Union (CaptureSet n k) where - union := CaptureSet.union - -notation:40 "{x@" m ":=" x "}" => CaptureSet.singleton x m -notation:40 "{x=" x "}" => {x@ε:=x} -notation:40 "{c@" m ":=" x "}" => CaptureSet.csingleton x m -notation:40 "{c=" x "}" => {c@ε:=x} - -def CaptureSet.rename (C : CaptureSet n k) (f : Fin n -> Fin n') : CaptureSet n' k := - match C with - | empty => {} - | union C1 C2 => (C1.rename f) ∪ (C2.rename f) - | singleton x m => {x@m:=f x} - | csingleton x m => {c@m:=x} - -def CaptureSet.crename (C : CaptureSet n k) (f : Fin k -> Fin k') : CaptureSet n k' := - match C with - | empty => {} - | union C1 C2 => (C1.crename f) ∪ (C2.crename f) - | singleton x m => {x@m:=x} - | csingleton x m => {c@m:=f x} - -end Capybara +import Capybara.Syntax.CaptureSet.Core diff --git a/Capybara/Syntax/CaptureSet/Core.lean b/Capybara/Syntax/CaptureSet/Core.lean new file mode 100644 index 00000000..3a628ca9 --- /dev/null +++ b/Capybara/Syntax/CaptureSet/Core.lean @@ -0,0 +1,36 @@ +import Capybara.Syntax.Mode +import Capybara.Morphism.Core +namespace Capybara + +inductive CaptureSet : Nat -> Nat -> Type where +| empty : CaptureSet n k +| union : CaptureSet n k -> CaptureSet n k -> CaptureSet n k +| singleton : Fin n -> Mode -> CaptureSet n k +| csingleton : Fin k -> Mode -> CaptureSet n k + +instance : EmptyCollection (CaptureSet n k) where + emptyCollection := CaptureSet.empty + +instance : Union (CaptureSet n k) where + union := CaptureSet.union + +notation:40 "{x@" m ":=" x "}" => CaptureSet.singleton x m +notation:40 "{x=" x "}" => {x@ε:=x} +notation:40 "{c@" m ":=" x "}" => CaptureSet.csingleton x m +notation:40 "{c=" x "}" => {c@ε:=x} + +def CaptureSet.rename (C : CaptureSet n k) (f : Fin n -> Fin n') : CaptureSet n' k := + match C with + | empty => {} + | union C1 C2 => (C1.rename f) ∪ (C2.rename f) + | singleton x m => {x@m:=f x} + | csingleton x m => {c@m:=x} + +def CaptureSet.crename (C : CaptureSet n k) (f : Fin k -> Fin k') : CaptureSet n k' := + match C with + | empty => {} + | union C1 C2 => (C1.crename f) ∪ (C2.crename f) + | singleton x m => {x@m:=x} + | csingleton x m => {c@m:=f x} + +end Capybara diff --git a/Capybara/Syntax/Type.lean b/Capybara/Syntax/Type.lean index 5e9e0148..672c18ca 100644 --- a/Capybara/Syntax/Type.lean +++ b/Capybara/Syntax/Type.lean @@ -1,27 +1 @@ -import Capybara.Syntax.CaptureSet -namespace Capybara - -inductive Kind : Type where -| Imm : Kind -| Mut : Kind -| Fresh : Kind - -mutual - -inductive EType : Nat -> Nat -> Nat -> Type where -| type : CType n m k -> EType n m k -| ex : CType n m (k+1) -> EType n m k - -inductive CType : Nat -> Nat -> Nat -> Type where -| capt : CaptureSet n k -> Mutability -> SType n m k -> CType n m k - -inductive SType : Nat -> Nat -> Nat -> Type where -| top : SType n m k -| tvar : Fin m -> SType n m k -| tarrow : SType n m k -> EType n (m+1) k -> SType n m k -| arrow : CType n m k -> EType (n+1) m k -> SType n m k -| carrow : Kind -> EType n m (k+1) -> SType n m k - -end - -end Capybara +import Capybara.Syntax.Type.Core diff --git a/Capybara/Syntax/Type/Core.lean b/Capybara/Syntax/Type/Core.lean new file mode 100644 index 00000000..b9891b56 --- /dev/null +++ b/Capybara/Syntax/Type/Core.lean @@ -0,0 +1,32 @@ +import Capybara.Syntax.CaptureSet +namespace Capybara + +inductive Kind : Type where +| Imm : Kind +| Mut : Kind +| Fresh : Kind + +mutual + +inductive EType : Nat -> Nat -> Nat -> Type where +| type : CType n m k -> EType n m k +| ex : CType n m (k+1) -> EType n m k + +inductive CType : Nat -> Nat -> Nat -> Type where +| capt : CaptureSet n k -> Mutability -> SType n m k -> CType n m k + +inductive SType : Nat -> Nat -> Nat -> Type where +| top : SType n m k +| tvar : Fin m -> SType n m k +| tarrow : SType n m k -> EType n (m+1) k -> SType n m k +| arrow : CType n m k -> EType (n+1) m k -> SType n m k +| carrow : Kind -> EType n m (k+1) -> SType n m k + +end + +notation:50 "⊤" => SType.top +notation:40 "[X<:" S "]->" T => SType.tarrow S T +notation:40 "(x:" S ")->" T => SType.arrow S T +notation:40 "[c:" S "]->" T => SType.carrow S T + +end Capybara diff --git a/Capybara/Syntax/Type/Renaming.lean b/Capybara/Syntax/Type/Renaming.lean new file mode 100644 index 00000000..6215bddc --- /dev/null +++ b/Capybara/Syntax/Type/Renaming.lean @@ -0,0 +1,25 @@ +import Capybara.Syntax.Type.Core +namespace Capybara + +mutual + +def EType.rename (E : EType n m k) (f : FinFun n n') : EType n' m k := + match E with + | EType.type T => EType.type (T.rename f) + | EType.ex T => EType.ex (T.rename f) + +def CType.rename (T : CType n m k) (f : FinFun n n') : CType n' m k := + match T with + | CType.capt C m S => CType.capt (C.rename f) m (S.rename f) + +def SType.rename (S : SType n m k) (f : FinFun n n') : SType n' m k := + match S with + | SType.top => SType.top + | SType.tvar x => SType.tvar x + | SType.arrow T E => (x:T.rename f)->(E.rename f.ext) + | SType.carrow k E => [c:k]->(E.rename f) + | SType.tarrow S T => [X<:S.rename f]->(T.rename f) + +end + +end Capybara From 9755b29d08916d18bdfe4a361d58ef939799d37d Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 10 Dec 2024 11:48:50 +0100 Subject: [PATCH 06/84] finish subst of capture set --- Capybara/Morphism/Subst.lean | 4 +-- Capybara/Syntax/CaptureSet.lean | 1 + Capybara/Syntax/CaptureSet/Core.lean | 40 ++++++++++++++++++++------- Capybara/Syntax/CaptureSet/Subst.lean | 15 ++++++++++ Capybara/Syntax/Type/Core.lean | 2 +- Capybara/Syntax/Type/Renaming.lean | 16 +++++++---- Capybara/Syntax/Type/Subst.lean | 24 ++++++++++++++++ 7 files changed, 84 insertions(+), 18 deletions(-) create mode 100644 Capybara/Syntax/CaptureSet/Subst.lean create mode 100644 Capybara/Syntax/Type/Subst.lean diff --git a/Capybara/Morphism/Subst.lean b/Capybara/Morphism/Subst.lean index 9cdceec7..a58c4b51 100644 --- a/Capybara/Morphism/Subst.lean +++ b/Capybara/Morphism/Subst.lean @@ -1,5 +1,5 @@ -import Capybara.Syntax.Type -import Capybara.Syntax.CaptureSet +import Capybara.Syntax.Type.Core +import Capybara.Syntax.CaptureSet.Core namespace Capybara structure Subst (n m k n' m' k' : Nat) where diff --git a/Capybara/Syntax/CaptureSet.lean b/Capybara/Syntax/CaptureSet.lean index d6c208f1..071ea092 100644 --- a/Capybara/Syntax/CaptureSet.lean +++ b/Capybara/Syntax/CaptureSet.lean @@ -1 +1,2 @@ import Capybara.Syntax.CaptureSet.Core +import Capybara.Syntax.CaptureSet.Subst diff --git a/Capybara/Syntax/CaptureSet/Core.lean b/Capybara/Syntax/CaptureSet/Core.lean index 3a628ca9..ef81ca09 100644 --- a/Capybara/Syntax/CaptureSet/Core.lean +++ b/Capybara/Syntax/CaptureSet/Core.lean @@ -19,18 +19,38 @@ notation:40 "{x=" x "}" => {x@ε:=x} notation:40 "{c@" m ":=" x "}" => CaptureSet.csingleton x m notation:40 "{c=" x "}" => {c@ε:=x} -def CaptureSet.rename (C : CaptureSet n k) (f : Fin n -> Fin n') : CaptureSet n' k := +def CaptureSet.rename + (C : CaptureSet n k) + (ρ : Renaming n m k n' m' k') : + CaptureSet n' k' := match C with | empty => {} - | union C1 C2 => (C1.rename f) ∪ (C2.rename f) - | singleton x m => {x@m:=f x} - | csingleton x m => {c@m:=x} + | union C1 C2 => (C1.rename ρ) ∪ (C2.rename ρ) + | singleton x m => {x@m:=ρ.var x} + | csingleton x m => {c@m:=ρ.cvar x} -def CaptureSet.crename (C : CaptureSet n k) (f : Fin k -> Fin k') : CaptureSet n k' := - match C with - | empty => {} - | union C1 C2 => (C1.crename f) ∪ (C2.crename f) - | singleton x m => {x@m:=x} - | csingleton x m => {c@m:=f x} +def CaptureSet.qualified + (C : CaptureSet n k) + (m : Mode) : + CaptureSet n k := + match C, m with + | empty, _ => {} + | union C1 C2, m => (C1.qualified m) ∪ (C2.qualified m) + | singleton x m0, ε => singleton x m0 + | singleton x _, m => singleton x m + | csingleton x m0, ε => csingleton x m0 + | csingleton x _, m => csingleton x m + +theorem CaptureSet.empty_def : + ({} : CaptureSet n k) = CaptureSet.empty := rfl + +theorem CaptureSet.union_def (C1 C2 : CaptureSet n k) : + (C1 ∪ C2) = CaptureSet.union C1 C2 := rfl + +@[simp] +theorem CaptureSet.qualified_default {C : CaptureSet n k} : + C.qualified ε = C := by + induction C <;> simp [CaptureSet.qualified, CaptureSet.empty_def] + case union ih1 ih2 => simp [CaptureSet.union_def, ih1, ih2] end Capybara diff --git a/Capybara/Syntax/CaptureSet/Subst.lean b/Capybara/Syntax/CaptureSet/Subst.lean new file mode 100644 index 00000000..000773aa --- /dev/null +++ b/Capybara/Syntax/CaptureSet/Subst.lean @@ -0,0 +1,15 @@ +import Capybara.Syntax.CaptureSet.Core +import Capybara.Morphism.Subst +namespace Capybara + +def CaptureSet.subst + (C : CaptureSet n k) + (σ : Subst n m k n' m' k') : + CaptureSet n' k' := + match C with + | empty => {} + | union C1 C2 => (C1.subst σ) ∪ (C2.subst σ) + | singleton x m => {x@m:=σ.var x} + | csingleton c m => (σ.cvar c).qualified m + +end Capybara diff --git a/Capybara/Syntax/Type/Core.lean b/Capybara/Syntax/Type/Core.lean index b9891b56..cf566b26 100644 --- a/Capybara/Syntax/Type/Core.lean +++ b/Capybara/Syntax/Type/Core.lean @@ -1,4 +1,4 @@ -import Capybara.Syntax.CaptureSet +import Capybara.Syntax.CaptureSet.Core namespace Capybara inductive Kind : Type where diff --git a/Capybara/Syntax/Type/Renaming.lean b/Capybara/Syntax/Type/Renaming.lean index 6215bddc..679bdd90 100644 --- a/Capybara/Syntax/Type/Renaming.lean +++ b/Capybara/Syntax/Type/Renaming.lean @@ -3,14 +3,20 @@ namespace Capybara mutual -def EType.rename (E : EType n m k) (f : FinFun n n') : EType n' m k := +def EType.rename + (E : EType n m k) + (ρ : Renaming n m k n' m' k') : + EType n' m' k' := match E with - | EType.type T => EType.type (T.rename f) - | EType.ex T => EType.ex (T.rename f) + | EType.type T => EType.type (T.rename ρ) + | EType.ex T => EType.ex (T.rename ρ) -def CType.rename (T : CType n m k) (f : FinFun n n') : CType n' m k := +def CType.rename + (T : CType n m k) + (ρ : Renaming n m k n' m' k') : + CType n' m' k' := match T with - | CType.capt C m S => CType.capt (C.rename f) m (S.rename f) + | CType.capt C m S => CType.capt (C.rename ρ) m (S.rename ρ) def SType.rename (S : SType n m k) (f : FinFun n n') : SType n' m k := match S with diff --git a/Capybara/Syntax/Type/Subst.lean b/Capybara/Syntax/Type/Subst.lean new file mode 100644 index 00000000..8ddf63a8 --- /dev/null +++ b/Capybara/Syntax/Type/Subst.lean @@ -0,0 +1,24 @@ +import Capybara.Morphism.Subst +import Capybara.Syntax.Type.Core +namespace Capybara + +mutual + +def EType.subst + (E : EType n m k) + (σ : Subst n m k n' m' k') : + EType n' m' k' := sorry + +def CType.subst + (T : CType n m k) + (σ : Subst n m k n' m' k') : + CType n' m' k' := sorry + +def SType.subst + (S : SType n m k) + (σ : Subst n m k n' m' k') : + SType n' m' k' := sorry + +end + +end Capybara From c7eceb3dcb7b5cc6c2bd536b9d4c909ccca8e51a Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 16 Dec 2024 22:37:53 +0100 Subject: [PATCH 07/84] farewell, subst, let's do mnf --- Capybara/Morphism/Subst.lean | 21 --------------------- Capybara/Syntax/CaptureSet.lean | 1 - Capybara/Syntax/CaptureSet/Subst.lean | 15 --------------- Capybara/Syntax/Type/Subst.lean | 24 ------------------------ 4 files changed, 61 deletions(-) delete mode 100644 Capybara/Morphism/Subst.lean delete mode 100644 Capybara/Syntax/CaptureSet/Subst.lean delete mode 100644 Capybara/Syntax/Type/Subst.lean diff --git a/Capybara/Morphism/Subst.lean b/Capybara/Morphism/Subst.lean deleted file mode 100644 index a58c4b51..00000000 --- a/Capybara/Morphism/Subst.lean +++ /dev/null @@ -1,21 +0,0 @@ -import Capybara.Syntax.Type.Core -import Capybara.Syntax.CaptureSet.Core -namespace Capybara - -structure Subst (n m k n' m' k' : Nat) where - var : FinFun n n' - tvar : Fin m -> SType n' m' k' - cvar : Fin k -> CaptureSet n' k' - -def Renaming.lift (ρ : Renaming n1 m1 k1 n2 m2 k2) : Subst n1 m1 k1 n2 m2 k2 := by - constructor - case var => exact ρ.var - case tvar => - intro x - apply SType.tvar - exact ρ.tvar x - case cvar => - intro c - exact {c=ρ.cvar c} - -end Capybara diff --git a/Capybara/Syntax/CaptureSet.lean b/Capybara/Syntax/CaptureSet.lean index 071ea092..d6c208f1 100644 --- a/Capybara/Syntax/CaptureSet.lean +++ b/Capybara/Syntax/CaptureSet.lean @@ -1,2 +1 @@ import Capybara.Syntax.CaptureSet.Core -import Capybara.Syntax.CaptureSet.Subst diff --git a/Capybara/Syntax/CaptureSet/Subst.lean b/Capybara/Syntax/CaptureSet/Subst.lean deleted file mode 100644 index 000773aa..00000000 --- a/Capybara/Syntax/CaptureSet/Subst.lean +++ /dev/null @@ -1,15 +0,0 @@ -import Capybara.Syntax.CaptureSet.Core -import Capybara.Morphism.Subst -namespace Capybara - -def CaptureSet.subst - (C : CaptureSet n k) - (σ : Subst n m k n' m' k') : - CaptureSet n' k' := - match C with - | empty => {} - | union C1 C2 => (C1.subst σ) ∪ (C2.subst σ) - | singleton x m => {x@m:=σ.var x} - | csingleton c m => (σ.cvar c).qualified m - -end Capybara diff --git a/Capybara/Syntax/Type/Subst.lean b/Capybara/Syntax/Type/Subst.lean deleted file mode 100644 index 8ddf63a8..00000000 --- a/Capybara/Syntax/Type/Subst.lean +++ /dev/null @@ -1,24 +0,0 @@ -import Capybara.Morphism.Subst -import Capybara.Syntax.Type.Core -namespace Capybara - -mutual - -def EType.subst - (E : EType n m k) - (σ : Subst n m k n' m' k') : - EType n' m' k' := sorry - -def CType.subst - (T : CType n m k) - (σ : Subst n m k n' m' k') : - CType n' m' k' := sorry - -def SType.subst - (S : SType n m k) - (σ : Subst n m k n' m' k') : - SType n' m' k' := sorry - -end - -end Capybara From a8996d82383cd0b21c4cd0d7e6cf96a4bdccbfd0 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 16 Dec 2024 22:47:59 +0100 Subject: [PATCH 08/84] finish renaming --- Capybara/Morphism/Core.lean | 24 ++++++++++++++++++++++++ Capybara/Syntax/Term.lean | 26 +++++++++++++++++++++++--- Capybara/Syntax/Type.lean | 1 + Capybara/Syntax/Type/Renaming.lean | 12 ++++++------ 4 files changed, 54 insertions(+), 9 deletions(-) diff --git a/Capybara/Morphism/Core.lean b/Capybara/Morphism/Core.lean index 8f326800..7bbc9a6b 100644 --- a/Capybara/Morphism/Core.lean +++ b/Capybara/Morphism/Core.lean @@ -14,4 +14,28 @@ structure Renaming (n m k n' m' k' : Nat) where tvar : FinFun m m' cvar : FinFun k k' +def Renaming.ext (ρ : Renaming n m k n' m' k') : + Renaming (n+1) m k (n'+1) m' k' := + { + var := ρ.var.ext + tvar := ρ.tvar + cvar := ρ.cvar + } + +def Renaming.text (ρ : Renaming n m k n' m' k') : + Renaming n (m+1) k n' (m'+1) k' := + { + var := ρ.var + tvar := ρ.tvar.ext + cvar := ρ.cvar + } + +def Renaming.cext (ρ : Renaming n m k n' m' k') : + Renaming n m (k+1) n' m' (k'+1) := + { + var := ρ.var + tvar := ρ.tvar + cvar := ρ.cvar.ext + } + end Capybara diff --git a/Capybara/Syntax/Term.lean b/Capybara/Syntax/Term.lean index 46d03baa..e3fb73eb 100644 --- a/Capybara/Syntax/Term.lean +++ b/Capybara/Syntax/Term.lean @@ -6,11 +6,31 @@ inductive Term : Nat -> Nat -> Nat -> Type where | lam : CType n m k -> Term (n+1) m k -> Term n m k | tlam : SType n m k -> Term n (m+1) k -> Term n m k | clam : Kind -> Term n m (k+1) -> Term n m k -| pack : CaptureSet n k -> Fin n -> Term n m k +| pack : Fin k -> Fin n -> Term n m k | app : Fin n -> Fin n -> Term n m k -| tapp : Fin n -> SType n m k -> Term n m k -| capp : Fin n -> CaptureSet n k -> Term n m k +| tapp : Fin n -> Fin m -> Term n m k +| capp : Fin n -> Fin k -> Term n m k | letin : Term n m k -> Term (n+1) m k -> Term n m k | unpack : Term n m k -> Term (n+1) m (k+1) -> Term n m k +| bindc : CaptureSet n k -> Term n m (k+1) -> Term n m k +| bindt : SType n m k -> Term n (m+1) k -> Term n m k + +def Term.rename + (t : Term n m k) + (ρ : Renaming n m k n' m' k') : + Term n' m' k' := + match t with + | var x => var (ρ.var x) + | lam t1 t2 => lam (t1.rename ρ) (t2.rename ρ.ext) + | tlam t1 t2 => tlam (t1.rename ρ) (t2.rename ρ.text) + | clam k t => clam k (t.rename ρ.cext) + | pack x y => pack (ρ.cvar x) (ρ.var y) + | app x y => app (ρ.var x) (ρ.var y) + | tapp x X => tapp (ρ.var x) (ρ.tvar X) + | capp x c => capp (ρ.var x) (ρ.cvar c) + | letin t1 t2 => letin (t1.rename ρ) (t2.rename ρ.ext) + | unpack t1 t2 => unpack (t1.rename ρ) (t2.rename ρ.cext.ext) + | bindc C t => bindc (C.rename ρ) (t.rename ρ.cext) + | bindt T t => bindt (T.rename ρ) (t.rename ρ.text) end Capybara diff --git a/Capybara/Syntax/Type.lean b/Capybara/Syntax/Type.lean index 672c18ca..d9ec83cb 100644 --- a/Capybara/Syntax/Type.lean +++ b/Capybara/Syntax/Type.lean @@ -1 +1,2 @@ import Capybara.Syntax.Type.Core +import Capybara.Syntax.Type.Renaming diff --git a/Capybara/Syntax/Type/Renaming.lean b/Capybara/Syntax/Type/Renaming.lean index 679bdd90..33f0a023 100644 --- a/Capybara/Syntax/Type/Renaming.lean +++ b/Capybara/Syntax/Type/Renaming.lean @@ -9,7 +9,7 @@ def EType.rename EType n' m' k' := match E with | EType.type T => EType.type (T.rename ρ) - | EType.ex T => EType.ex (T.rename ρ) + | EType.ex T => EType.ex (T.rename ρ.cext) def CType.rename (T : CType n m k) @@ -18,13 +18,13 @@ def CType.rename match T with | CType.capt C m S => CType.capt (C.rename ρ) m (S.rename ρ) -def SType.rename (S : SType n m k) (f : FinFun n n') : SType n' m k := +def SType.rename (S : SType n m k) (ρ : Renaming n m k n' m' k') : SType n' m' k' := match S with | SType.top => SType.top - | SType.tvar x => SType.tvar x - | SType.arrow T E => (x:T.rename f)->(E.rename f.ext) - | SType.carrow k E => [c:k]->(E.rename f) - | SType.tarrow S T => [X<:S.rename f]->(T.rename f) + | SType.tvar x => SType.tvar (ρ.tvar x) + | SType.arrow T E => (x:T.rename ρ)->(E.rename ρ.ext) + | SType.carrow k E => [c:k]->(E.rename ρ.cext) + | SType.tarrow S T => [X<:S.rename ρ]->(T.rename ρ.text) end From 8e23e5a621a03d68ce9221bca03cbeb246b08ae2 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 16 Dec 2024 23:00:13 +0100 Subject: [PATCH 09/84] rename aliasing constructs --- Capybara/Syntax/Term.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Capybara/Syntax/Term.lean b/Capybara/Syntax/Term.lean index e3fb73eb..d6a88425 100644 --- a/Capybara/Syntax/Term.lean +++ b/Capybara/Syntax/Term.lean @@ -12,8 +12,8 @@ inductive Term : Nat -> Nat -> Nat -> Type where | capp : Fin n -> Fin k -> Term n m k | letin : Term n m k -> Term (n+1) m k -> Term n m k | unpack : Term n m k -> Term (n+1) m (k+1) -> Term n m k -| bindc : CaptureSet n k -> Term n m (k+1) -> Term n m k -| bindt : SType n m k -> Term n (m+1) k -> Term n m k +| calias : CaptureSet n k -> Term n m (k+1) -> Term n m k +| talias : SType n m k -> Term n (m+1) k -> Term n m k def Term.rename (t : Term n m k) @@ -30,7 +30,7 @@ def Term.rename | capp x c => capp (ρ.var x) (ρ.cvar c) | letin t1 t2 => letin (t1.rename ρ) (t2.rename ρ.ext) | unpack t1 t2 => unpack (t1.rename ρ) (t2.rename ρ.cext.ext) - | bindc C t => bindc (C.rename ρ) (t.rename ρ.cext) - | bindt T t => bindt (T.rename ρ) (t.rename ρ.text) + | calias C t => calias (C.rename ρ) (t.rename ρ.cext) + | talias T t => talias (T.rename ρ) (t.rename ρ.text) end Capybara From 7e8c61a8c209283b243e38ce224be96156ef8341 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 16 Dec 2024 23:00:22 +0100 Subject: [PATCH 10/84] add context --- Capybara/Syntax/Context.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 Capybara/Syntax/Context.lean diff --git a/Capybara/Syntax/Context.lean b/Capybara/Syntax/Context.lean new file mode 100644 index 00000000..549cc0af --- /dev/null +++ b/Capybara/Syntax/Context.lean @@ -0,0 +1,14 @@ +import Capybara.Syntax.Type +namespace Capybara + +/-! +An indexed context. A `Context n m k` contains `n` term variables, +`m` type variables, and `k` capture set variables. +!-/ +inductive Context : Nat -> Nat -> Nat -> Type where +| empty : Context 0 0 0 +| cons : Context n m k -> CType n m k -> Context (n+1) m k +| tcons : Context n m k -> SType n m k -> Context n (m+1) k +| ccons : Context n m k -> CaptureSet n k -> Context n m (k+1) + +end Capybara From cd9027c61d04051f67a31d916b8da0465aea2105 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 16 Dec 2024 23:10:13 +0100 Subject: [PATCH 11/84] add weaken map --- Capybara/Morphism/Core.lean | 78 +++++++++++++++++++++++++++++++++++++ 1 file changed, 78 insertions(+) diff --git a/Capybara/Morphism/Core.lean b/Capybara/Morphism/Core.lean index 7bbc9a6b..1b0e3dc3 100644 --- a/Capybara/Morphism/Core.lean +++ b/Capybara/Morphism/Core.lean @@ -1,19 +1,61 @@ import Mathlib.Data.Fin.Basic namespace Capybara +/-! +# Morphisms +This module defines morphisms between contexts in the Capybara type system. + +## Main definitions + +- `FinFun n n'`: A function mapping finite indices from dimension `n` to dimension `n'` +- `Renaming n m k n' m' k'`: A renaming morphism that maps between contexts with dimensions: + - `n` term variables to `n'` term variables + - `m` type variables to `m'` type variables + - `k` capture set variables to `k'` capture set variables + +## Implementation Notes + +Renamings are used to implement variable substitution and weakening in a well-typed way. +The three dimensions (term, type, and capture set variables) are handled separately but +in parallel through the `Renaming` structure. + +Each dimension can be extended independently through the `ext`, `text` and `cext` operations +which add a new variable while preserving the existing mapping. + +note: Sonnet wrote this documentation. +-/ + +/-! +A renaming function maps indices from one dimension to another. +-/ def FinFun (n : Nat) (n' : Nat) : Type := Fin n -> Fin n' +/-! +Extend a renaming function by one on the term variable dimension. +-/ def FinFun.ext (f : FinFun n n') : FinFun (n+1) (n'+1) := by intro x cases x using Fin.cases case zero => exact 0 case succ x0 => exact Fin.succ (f x0) +def FinFun.id {n : Nat} : FinFun n n := fun x => x + +def FinFun.weaken {n : Nat} : FinFun n (n+1) := by + intro x + exact Fin.succ x + +/-! +A renaming function, which maps the three dimensions of a context (term, type, and capture set variables). +-/ structure Renaming (n m k n' m' k' : Nat) where var : FinFun n n' tvar : FinFun m m' cvar : FinFun k k' +/-! +Extend a renaming function by one on the term variable dimension. +-/ def Renaming.ext (ρ : Renaming n m k n' m' k') : Renaming (n+1) m k (n'+1) m' k' := { @@ -22,6 +64,9 @@ def Renaming.ext (ρ : Renaming n m k n' m' k') : cvar := ρ.cvar } +/-! +Extend a renaming function by one on the type variable dimension. +-/ def Renaming.text (ρ : Renaming n m k n' m' k') : Renaming n (m+1) k n' (m'+1) k' := { @@ -30,6 +75,9 @@ def Renaming.text (ρ : Renaming n m k n' m' k') : cvar := ρ.cvar } +/-! +Extend a renaming function by one on the capture set variable dimension. +-/ def Renaming.cext (ρ : Renaming n m k n' m' k') : Renaming n m (k+1) n' m' (k'+1) := { @@ -38,4 +86,34 @@ def Renaming.cext (ρ : Renaming n m k n' m' k') : cvar := ρ.cvar.ext } +/-! +Weaken the renaming by one on the term variable dimension. +-/ +def Renaming.weaken : Renaming n m k (n+1) m k := + { + var := FinFun.weaken + tvar := FinFun.id + cvar := FinFun.id + } + +/-! +Weaken the renaming by one on the type variable dimension. +-/ +def Renaming.tweaken : Renaming n m k n (m+1) k := + { + var := FinFun.id + tvar := FinFun.weaken + cvar := FinFun.id + } + +/-! +Weaken the renaming by one on the capture variable dimension. +-/ +def Renaming.cweaken : Renaming n m k n m (k+1) := + { + var := FinFun.id + tvar := FinFun.id + cvar := FinFun.weaken + } + end Capybara From 56d8be979314e337cdf08b214405093e3ff5132b Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 16 Dec 2024 23:14:43 +0100 Subject: [PATCH 12/84] weakening --- Capybara/Syntax/CaptureSet/Core.lean | 26 +++++++++++++++++++++ Capybara/Syntax/Type.lean | 1 + Capybara/Syntax/Type/Weakening.lean | 34 ++++++++++++++++++++++++++++ 3 files changed, 61 insertions(+) create mode 100644 Capybara/Syntax/Type/Weakening.lean diff --git a/Capybara/Syntax/CaptureSet/Core.lean b/Capybara/Syntax/CaptureSet/Core.lean index ef81ca09..49558dac 100644 --- a/Capybara/Syntax/CaptureSet/Core.lean +++ b/Capybara/Syntax/CaptureSet/Core.lean @@ -2,23 +2,35 @@ import Capybara.Syntax.Mode import Capybara.Morphism.Core namespace Capybara +/-! +Capture set definitions. +-/ inductive CaptureSet : Nat -> Nat -> Type where | empty : CaptureSet n k | union : CaptureSet n k -> CaptureSet n k -> CaptureSet n k | singleton : Fin n -> Mode -> CaptureSet n k | csingleton : Fin k -> Mode -> CaptureSet n k +/-! +Instance definitions for capture sets. +-/ instance : EmptyCollection (CaptureSet n k) where emptyCollection := CaptureSet.empty instance : Union (CaptureSet n k) where union := CaptureSet.union +/-! +Notation for capture sets. +-/ notation:40 "{x@" m ":=" x "}" => CaptureSet.singleton x m notation:40 "{x=" x "}" => {x@ε:=x} notation:40 "{c@" m ":=" x "}" => CaptureSet.csingleton x m notation:40 "{c=" x "}" => {c@ε:=x} +/-! +Renaming functions for capture sets. +-/ def CaptureSet.rename (C : CaptureSet n k) (ρ : Renaming n m k n' m' k') : @@ -29,6 +41,9 @@ def CaptureSet.rename | singleton x m => {x@m:=ρ.var x} | csingleton x m => {c@m:=ρ.cvar x} +/-! +Mode qualification. +-/ def CaptureSet.qualified (C : CaptureSet n k) (m : Mode) : @@ -41,6 +56,17 @@ def CaptureSet.qualified | csingleton x m0, ε => csingleton x m0 | csingleton x _, m => csingleton x m +/-! +Weakening functions for capture sets. +-/ +def CaptureSet.weaken : CaptureSet n k -> CaptureSet (n+1) k := + fun C => C.rename (Renaming.weaken (m:=0)) +def CaptureSet.cweaken : CaptureSet n k -> CaptureSet n (k+1) := + fun C => C.rename (Renaming.cweaken (m:=0)) + +/-! +Basic theorems. +-/ theorem CaptureSet.empty_def : ({} : CaptureSet n k) = CaptureSet.empty := rfl diff --git a/Capybara/Syntax/Type.lean b/Capybara/Syntax/Type.lean index d9ec83cb..f5c9a880 100644 --- a/Capybara/Syntax/Type.lean +++ b/Capybara/Syntax/Type.lean @@ -1,2 +1,3 @@ import Capybara.Syntax.Type.Core import Capybara.Syntax.Type.Renaming +import Capybara.Syntax.Type.Weakening diff --git a/Capybara/Syntax/Type/Weakening.lean b/Capybara/Syntax/Type/Weakening.lean new file mode 100644 index 00000000..c1e69891 --- /dev/null +++ b/Capybara/Syntax/Type/Weakening.lean @@ -0,0 +1,34 @@ +import Capybara.Syntax.Type.Renaming +namespace Capybara + +/-! +Term weakening functions. +-/ +def EType.weaken : EType n m k -> EType (n+1) m k := + fun E => E.rename Renaming.weaken +def CType.weaken : CType n m k -> CType (n+1) m k := + fun T => T.rename Renaming.weaken +def SType.weaken : SType n m k -> SType (n+1) m k := + fun S => S.rename Renaming.weaken + +/-! +Type weakening functions. +-/ +def EType.tweaken : EType n m k -> EType n (m+1) k := + fun E => E.rename Renaming.tweaken +def CType.tweaken : CType n m k -> CType n (m+1) k := + fun T => T.rename Renaming.tweaken +def SType.tweaken : SType n m k -> SType n (m+1) k := + fun S => S.rename Renaming.tweaken + +/-! +Capture set weakening functions. +-/ +def EType.cweaken : EType n m k -> EType n m (k+1) := + fun E => E.rename Renaming.cweaken +def CType.cweaken : CType n m k -> CType n m (k+1) := + fun T => T.rename Renaming.cweaken +def SType.cweaken : SType n m k -> SType n m (k+1) := + fun S => S.rename Renaming.cweaken + +end Capybara From fb23eccda06349028026f160c229e88fc13daafb Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 16 Dec 2024 23:22:29 +0100 Subject: [PATCH 13/84] finish context lookup --- Capybara/Syntax/Context.lean | 94 +++++++++++++++++++++++++++++++++++- 1 file changed, 92 insertions(+), 2 deletions(-) diff --git a/Capybara/Syntax/Context.lean b/Capybara/Syntax/Context.lean index 549cc0af..137a1ece 100644 --- a/Capybara/Syntax/Context.lean +++ b/Capybara/Syntax/Context.lean @@ -1,6 +1,46 @@ +import Mathlib.Data.Fin.Basic import Capybara.Syntax.Type namespace Capybara +/-! +Type binding and capture set binding. + +Type binding can be either a type parameter (abstract) or +a concrete type alias. Similarly, capture set binding can be +a capture set parameter (abstract) or a concrete capture set alias. +-/ +inductive TBinding : Nat -> Nat -> Nat -> Type where +| param : SType n m k -> TBinding n m k +| alias : SType n m k -> TBinding n m k + +inductive CBinding : Nat -> Nat -> Type where +| param : Kind -> CBinding n k +| alias : CaptureSet n k -> CBinding n k + +notation:max "tparam" S => TBinding.param S +notation:max "talias" S => TBinding.alias S +notation:max "cparam" k => CBinding.param k +notation:max "calias" C => CBinding.alias C + +/-! +Weakening functions for type and capture set binding. +-/ +def TBinding.weaken : TBinding n m k -> TBinding (n+1) m k +| TBinding.param T => TBinding.param (T.weaken) +| TBinding.alias T => TBinding.alias (T.weaken) +def CBinding.weaken : CBinding n k -> CBinding (n+1) k +| CBinding.param k => CBinding.param k +| CBinding.alias C => CBinding.alias (C.weaken) +def TBinding.tweaken : TBinding n m k -> TBinding n (m+1) k +| TBinding.param T => TBinding.param (T.tweaken) +| TBinding.alias T => TBinding.alias (T.tweaken) +def TBinding.cweaken : TBinding n m k -> TBinding n m (k+1) +| TBinding.param T => TBinding.param (T.cweaken) +| TBinding.alias T => TBinding.alias (T.cweaken) +def CBinding.cweaken : CBinding n k -> CBinding n (k+1) +| CBinding.param k => CBinding.param k +| CBinding.alias C => CBinding.alias (C.cweaken) + /-! An indexed context. A `Context n m k` contains `n` term variables, `m` type variables, and `k` capture set variables. @@ -8,7 +48,57 @@ An indexed context. A `Context n m k` contains `n` term variables, inductive Context : Nat -> Nat -> Nat -> Type where | empty : Context 0 0 0 | cons : Context n m k -> CType n m k -> Context (n+1) m k -| tcons : Context n m k -> SType n m k -> Context n (m+1) k -| ccons : Context n m k -> CaptureSet n k -> Context n m (k+1) +| tcons : Context n m k -> TBinding n m k -> Context n (m+1) k +| ccons : Context n m k -> CBinding n k -> Context n m (k+1) + +instance : EmptyCollection (Context 0 0 0) := + ⟨Context.empty⟩ + +theorem Context.empty_def : + ({} : Context 0 0 0) = Context.empty := rfl + +notation:20 Γ ",x:" T => Context.cons Γ T +notation:20 Γ ",X:" T => Context.tcons Γ T +notation:20 Γ ",c:" C => Context.ccons Γ C + +/-! +Context lookup. + +`Context.Lookup`, `Context.LookupT`, and `Context.LookupC` look up the three dimensions of a context, +respectively. +-/ +inductive Context.Lookup : Context n m k -> Fin n -> CType n m k -> Prop where +| here : Context.Lookup (Γ,x:T) 0 T.weaken +| there : + Context.Lookup Γ x T -> + Context.Lookup (Γ,x:T) (x.succ) T.weaken +| tthere : + Context.Lookup Γ x T -> + Context.Lookup (Γ,X:B) x (T.tweaken) +| cthere : + Context.Lookup Γ x T -> + Context.Lookup (Γ,c:B) x (T.cweaken) +inductive Context.LookupT : Context n m k -> Fin m -> TBinding n m k -> Prop where +| here : Context.LookupT (Γ,X:T) 0 T.tweaken +| there : + Context.LookupT Γ X S -> + Context.LookupT (Γ,x:T) X S.weaken +| tthere : + Context.LookupT Γ X T -> + Context.LookupT (Γ,X:B) (X.succ) T.tweaken +| cthere : + Context.LookupT Γ X T -> + Context.LookupT (Γ,c:B) X T.cweaken +inductive Context.LookupC : Context n m k -> Fin k -> CBinding n k -> Prop where +| here : Context.LookupC (Γ,c:C) 0 C.cweaken +| there : + Context.LookupC Γ c C -> + Context.LookupC (Γ,x:T) c C.weaken +| tthere : + Context.LookupC Γ c C -> + Context.LookupC (Γ,X:B) c C +| cthere : + Context.LookupC Γ c C -> + Context.LookupC (Γ,c:B) (c.succ) C.cweaken end Capybara From c6889eecefe74ecae0824b378ac00ae9c2f1f857 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 16 Dec 2024 23:23:56 +0100 Subject: [PATCH 14/84] term weakening --- Capybara/Syntax/Term.lean | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/Capybara/Syntax/Term.lean b/Capybara/Syntax/Term.lean index d6a88425..04c401cf 100644 --- a/Capybara/Syntax/Term.lean +++ b/Capybara/Syntax/Term.lean @@ -1,6 +1,31 @@ import Capybara.Syntax.Type namespace Capybara +/-! +# Term Syntax +This module defines the syntax of terms in the Capybara language. + +## Main Definitions + +- `Term n m k`: Terms with `n` term variables, `m` type variables, and `k` capture set variables +- `Term.rename`: Renaming operation for terms + +## Term Constructors + +- Variables: `var` +- Functions: `lam` (term abstraction), `tlam` (type abstraction), `clam` (capture set abstraction) +- Applications: `app` (term application), `tapp` (type application), `capp` (capture set application) +- Capture set operations: `pack` (capture set creation), `unpack` (capture set elimination) +- Let bindings: `letin` (term binding) +- Aliases: `calias` (capture set alias), `talias` (type alias) + +The indices `n`, `m`, and `k` track the number of term variables, type variables, and capture set variables +in scope, respectively. This ensures well-scopedness of terms through the type system. +-/ + +/-! +Term definitions. +-/ inductive Term : Nat -> Nat -> Nat -> Type where | var : Fin n -> Term n m k | lam : CType n m k -> Term (n+1) m k -> Term n m k @@ -15,6 +40,9 @@ inductive Term : Nat -> Nat -> Nat -> Type where | calias : CaptureSet n k -> Term n m (k+1) -> Term n m k | talias : SType n m k -> Term n (m+1) k -> Term n m k +/-! +Renaming operation for terms. +-/ def Term.rename (t : Term n m k) (ρ : Renaming n m k n' m' k') : @@ -33,4 +61,14 @@ def Term.rename | calias C t => calias (C.rename ρ) (t.rename ρ.cext) | talias T t => talias (T.rename ρ) (t.rename ρ.text) +/-! +Weakening operation for terms. +-/ +def Term.weaken : Term n m k -> Term (n+1) m k := + fun t => t.rename Renaming.weaken +def Term.tweaken : Term n m k -> Term n (m+1) k := + fun t => t.rename Renaming.tweaken +def Term.cweaken : Term n m k -> Term n m (k+1) := + fun t => t.rename Renaming.cweaken + end Capybara From e7e862b83fc9804194b6b0f0361deec762d51bc0 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 16 Dec 2024 23:24:17 +0100 Subject: [PATCH 15/84] add type context to the index --- Capybara/Syntax.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Capybara/Syntax.lean b/Capybara/Syntax.lean index 1094be29..d234b8b0 100644 --- a/Capybara/Syntax.lean +++ b/Capybara/Syntax.lean @@ -2,3 +2,4 @@ import Capybara.Syntax.Mode import Capybara.Syntax.CaptureSet import Capybara.Syntax.Type import Capybara.Syntax.Term +import Capybara.Syntax.Context From 906d6ecbb60bbd3d3b664c3ac25e34a4ea701132 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 16 Dec 2024 23:25:42 +0100 Subject: [PATCH 16/84] init type system --- Capybara/StaticSemantics.lean | 2 ++ Capybara/StaticSemantics/Subcapturing.lean | 4 ++++ Capybara/StaticSemantics/Subtyping.lean | 5 +++++ 3 files changed, 11 insertions(+) create mode 100644 Capybara/StaticSemantics.lean create mode 100644 Capybara/StaticSemantics/Subcapturing.lean create mode 100644 Capybara/StaticSemantics/Subtyping.lean diff --git a/Capybara/StaticSemantics.lean b/Capybara/StaticSemantics.lean new file mode 100644 index 00000000..f810b8a2 --- /dev/null +++ b/Capybara/StaticSemantics.lean @@ -0,0 +1,2 @@ +import Capybara.StaticSemantics.Subcapturing +import Capybara.StaticSemantics.Subtyping diff --git a/Capybara/StaticSemantics/Subcapturing.lean b/Capybara/StaticSemantics/Subcapturing.lean new file mode 100644 index 00000000..d9ebe14d --- /dev/null +++ b/Capybara/StaticSemantics/Subcapturing.lean @@ -0,0 +1,4 @@ +import Capybara.Syntax +namespace Capybara + +end Capybara diff --git a/Capybara/StaticSemantics/Subtyping.lean b/Capybara/StaticSemantics/Subtyping.lean new file mode 100644 index 00000000..529a3689 --- /dev/null +++ b/Capybara/StaticSemantics/Subtyping.lean @@ -0,0 +1,5 @@ +import Capybara.Syntax +import Capybara.StaticSemantics.Subcapturing +namespace Capybara + +end Capybara From 4ffa54d6095337ce39ee169ce165ee5e53261e6c Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 16 Dec 2024 23:30:48 +0100 Subject: [PATCH 17/84] add subsetting --- Capybara/Syntax/CaptureSet/Core.lean | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/Capybara/Syntax/CaptureSet/Core.lean b/Capybara/Syntax/CaptureSet/Core.lean index 49558dac..89acca7e 100644 --- a/Capybara/Syntax/CaptureSet/Core.lean +++ b/Capybara/Syntax/CaptureSet/Core.lean @@ -24,9 +24,9 @@ instance : Union (CaptureSet n k) where Notation for capture sets. -/ notation:40 "{x@" m ":=" x "}" => CaptureSet.singleton x m -notation:40 "{x=" x "}" => {x@ε:=x} +notation:40 "{x:=" x "}" => {x@ε:=x} notation:40 "{c@" m ":=" x "}" => CaptureSet.csingleton x m -notation:40 "{c=" x "}" => {c@ε:=x} +notation:40 "{c:=" x "}" => {c@ε:=x} /-! Renaming functions for capture sets. @@ -79,4 +79,21 @@ theorem CaptureSet.qualified_default {C : CaptureSet n k} : induction C <;> simp [CaptureSet.qualified, CaptureSet.empty_def] case union ih1 ih2 => simp [CaptureSet.union_def, ih1, ih2] +/-! +Subset relation for capture sets. +-/ +inductive CaptureSet.Subset : CaptureSet n k -> CaptureSet n k -> Prop where +| empty : CaptureSet.Subset {} C +| refl : CaptureSet.Subset C C +| union_l : + CaptureSet.Subset C1 C -> + CaptureSet.Subset C2 C -> + CaptureSet.Subset (C1 ∪ C2) C +| union_rl : + CaptureSet.Subset C C1 -> + CaptureSet.Subset C (C1 ∪ C2) +| union_rr : + CaptureSet.Subset C C2 -> + CaptureSet.Subset C (C1 ∪ C2) + end Capybara From bbf3e10871c37fb1725028f813e0671c1f8ee745 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 16 Dec 2024 23:32:53 +0100 Subject: [PATCH 18/84] add instance for notation --- Capybara/Syntax/CaptureSet/Core.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Capybara/Syntax/CaptureSet/Core.lean b/Capybara/Syntax/CaptureSet/Core.lean index 89acca7e..eb0a172b 100644 --- a/Capybara/Syntax/CaptureSet/Core.lean +++ b/Capybara/Syntax/CaptureSet/Core.lean @@ -80,7 +80,7 @@ theorem CaptureSet.qualified_default {C : CaptureSet n k} : case union ih1 ih2 => simp [CaptureSet.union_def, ih1, ih2] /-! -Subset relation for capture sets. +Subset relation for capture sets. It is defined inductively. -/ inductive CaptureSet.Subset : CaptureSet n k -> CaptureSet n k -> Prop where | empty : CaptureSet.Subset {} C @@ -96,4 +96,7 @@ inductive CaptureSet.Subset : CaptureSet n k -> CaptureSet n k -> Prop where CaptureSet.Subset C C2 -> CaptureSet.Subset C (C1 ∪ C2) +instance : HasSubset (CaptureSet n k) where + Subset := CaptureSet.Subset + end Capybara From 8d5b9864d723045e84941cb592d0713436618519 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 16 Dec 2024 23:45:14 +0100 Subject: [PATCH 19/84] Finish subcapturing --- Capybara/StaticSemantics/Subcapturing.lean | 37 ++++++++++++++++++++++ Capybara/Syntax/CaptureSet/Core.lean | 3 ++ 2 files changed, 40 insertions(+) diff --git a/Capybara/StaticSemantics/Subcapturing.lean b/Capybara/StaticSemantics/Subcapturing.lean index d9ebe14d..1413156a 100644 --- a/Capybara/StaticSemantics/Subcapturing.lean +++ b/Capybara/StaticSemantics/Subcapturing.lean @@ -1,4 +1,41 @@ import Capybara.Syntax namespace Capybara +/-! +Subcapturing relation. + +There are three structural rules: +- `subset`: if `C1 ⊆ C2`, then `C1` subcaptures `C2`. +- `trans`: if `C1` subcaptures `C2` and `C2` subcaptures `C3`, then `C1` subcaptures `C3`. +- `union`: if `C1` subcaptures `C` and `C2` subcaptures `C`, then `C1 ∪ C2` subcaptures `C`. + +Two rules for variables, one for default (mutable) captures and the other for read-only captures. Two similar rules for capture set aliases. +-/ +inductive Subcapturing : Context n m k -> CaptureSet n k -> CaptureSet n k -> Prop where +| subset : + (C1 ⊆ C2) -> + Subcapturing Γ C1 C2 +| trans : + Subcapturing Γ C1 C2 -> + Subcapturing Γ C2 C3 -> + Subcapturing Γ C1 C3 +| union : + Subcapturing Γ C1 C -> + Subcapturing Γ C2 C -> + Subcapturing Γ (C1 ∪ C2) C +| ro : + Subcapturing Γ (C.ro) C +| var : + Context.Lookup Γ x (CType.capt C m S) -> + Subcapturing Γ ({x:=x}) (C.qualified (Mode.M m)) +| rovar : + Context.Lookup Γ x (CType.capt C m S) -> + Subcapturing Γ ({x@ro:=x}) (C.qualified ro) +| cvar_l : + Context.LookupC Γ c (calias C) -> + Subcapturing Γ ({c@m:=c}) (C.qualified m) +| cvar_r : + Context.LookupC Γ c (calias C) -> + Subcapturing Γ (C.qualified m) ({c@m:=c}) + end Capybara diff --git a/Capybara/Syntax/CaptureSet/Core.lean b/Capybara/Syntax/CaptureSet/Core.lean index eb0a172b..76a71baa 100644 --- a/Capybara/Syntax/CaptureSet/Core.lean +++ b/Capybara/Syntax/CaptureSet/Core.lean @@ -56,6 +56,9 @@ def CaptureSet.qualified | csingleton x m0, ε => csingleton x m0 | csingleton x _, m => csingleton x m +def CaptureSet.ro (C : CaptureSet n k) : CaptureSet n k := + C.qualified ro + /-! Weakening functions for capture sets. -/ From a38da84084b96b653559b3228354d8d3ec833aa0 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 16 Dec 2024 23:47:01 +0100 Subject: [PATCH 20/84] add an order, `MorePermissive` --- Capybara/Syntax/Mode.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Capybara/Syntax/Mode.lean b/Capybara/Syntax/Mode.lean index aefa647a..2da8622e 100644 --- a/Capybara/Syntax/Mode.lean +++ b/Capybara/Syntax/Mode.lean @@ -12,4 +12,12 @@ notation "ro" => Mode.M Mutability.readonly notation "ε" => Mode.M Mutability.default notation "drop" => Mode.drop +/-! +Which mutability mode is more permissive? +-/ +inductive MorePermissive : Mutability -> Mutability -> Prop where +| readonly : MorePermissive Mutability.readonly Mutability.default +| refl : MorePermissive m m + + end Capybara From 566925ef141018cc2568130798406e1dc883ee28 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 16 Dec 2024 23:59:17 +0100 Subject: [PATCH 21/84] Finish subtyping --- Capybara/StaticSemantics/Subcapturing.lean | 2 + Capybara/StaticSemantics/Subtyping.lean | 48 ++++++++++++++++++++++ Capybara/Syntax/Type/Core.lean | 9 +++- 3 files changed, 58 insertions(+), 1 deletion(-) diff --git a/Capybara/StaticSemantics/Subcapturing.lean b/Capybara/StaticSemantics/Subcapturing.lean index 1413156a..6c2e28da 100644 --- a/Capybara/StaticSemantics/Subcapturing.lean +++ b/Capybara/StaticSemantics/Subcapturing.lean @@ -38,4 +38,6 @@ inductive Subcapturing : Context n m k -> CaptureSet n k -> CaptureSet n k -> Pr Context.LookupC Γ c (calias C) -> Subcapturing Γ (C.qualified m) ({c@m:=c}) +notation:50 Γ "⊢c" C1 "<:" C2 => Subcapturing Γ C1 C2 + end Capybara diff --git a/Capybara/StaticSemantics/Subtyping.lean b/Capybara/StaticSemantics/Subtyping.lean index 529a3689..c83b72eb 100644 --- a/Capybara/StaticSemantics/Subtyping.lean +++ b/Capybara/StaticSemantics/Subtyping.lean @@ -2,4 +2,52 @@ import Capybara.Syntax import Capybara.StaticSemantics.Subcapturing namespace Capybara +mutual + +inductive SSubtyping : Context n m k -> SType n m k -> SType n m k -> Prop +| top : + SSubtyping Γ S ⊤ +| refl : + SSubtyping Γ S S +| trans : + SSubtyping Γ S1 S2 -> + SSubtyping Γ S2 S3 -> + SSubtyping Γ S1 S3 +| tvar : + Context.LookupT Γ X (tparam S) -> + SSubtyping Γ (SType.tvar X) S +| arrow : + CSubtyping Γ T2 T1 -> + ESubtyping (Γ,x:T2) E1 E2 -> + SSubtyping Γ ((x:T1)->E1) ((x:T2)->E2) +| tarrow : + SSubtyping Γ S2 S1 -> + ESubtyping (Γ,X:tparam S2) E1 E2 -> + SSubtyping Γ ([X<:S1]->E1) ([X<:S2]->E2) +| carrow : + ESubtyping (Γ,c:cparam K) E1 E2 -> + SSubtyping Γ ([c:K]->E1) ([c:K]->E2) +| talias_l : + Context.LookupT Γ X (talias S) -> + SSubtyping Γ (SType.tvar X) S +| talias_r : + Context.LookupT Γ X (talias S) -> + SSubtyping Γ S (SType.tvar X) + +inductive CSubtyping : Context n m k -> CType n m k -> CType n m k -> Prop +| capt : + SSubtyping Γ S1 S2 -> + (Γ ⊢c C1 <: C2) -> + CSubtyping Γ (S1^[m]C1) (S2^[m]C2) + +inductive ESubtyping : Context n m k -> EType n m k -> EType n m k -> Prop +| type : + CSubtyping Γ T1 T2 -> + ESubtyping Γ (EType.type T1) (EType.type T2) +| ex : + CSubtyping (Γ,c:cparam Kind.Fresh) T1 T2 -> + ESubtyping Γ (EType.ex T1) (EType.ex T2) + +end + end Capybara diff --git a/Capybara/Syntax/Type/Core.lean b/Capybara/Syntax/Type/Core.lean index cf566b26..804307f4 100644 --- a/Capybara/Syntax/Type/Core.lean +++ b/Capybara/Syntax/Type/Core.lean @@ -1,6 +1,9 @@ import Capybara.Syntax.CaptureSet.Core namespace Capybara +/-! +Kinds of capture set parameters. +-/ inductive Kind : Type where | Imm : Kind | Mut : Kind @@ -24,9 +27,13 @@ inductive SType : Nat -> Nat -> Nat -> Type where end -notation:50 "⊤" => SType.top +/-! +Notation for types. +-/ +notation:max "⊤" => SType.top notation:40 "[X<:" S "]->" T => SType.tarrow S T notation:40 "(x:" S ")->" T => SType.arrow S T notation:40 "[c:" S "]->" T => SType.carrow S T +notation:50 S "^[" m "]" C => CType.capt C m S end Capybara From ce42515001ac924538150fc4c069aed66e998a96 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 17 Dec 2024 00:41:43 +0100 Subject: [PATCH 22/84] add notations --- Capybara/StaticSemantics/Subcapturing.lean | 2 +- Capybara/StaticSemantics/Subtyping.lean | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/Capybara/StaticSemantics/Subcapturing.lean b/Capybara/StaticSemantics/Subcapturing.lean index 6c2e28da..a04ac941 100644 --- a/Capybara/StaticSemantics/Subcapturing.lean +++ b/Capybara/StaticSemantics/Subcapturing.lean @@ -38,6 +38,6 @@ inductive Subcapturing : Context n m k -> CaptureSet n k -> CaptureSet n k -> Pr Context.LookupC Γ c (calias C) -> Subcapturing Γ (C.qualified m) ({c@m:=c}) -notation:50 Γ "⊢c" C1 "<:" C2 => Subcapturing Γ C1 C2 +notation:50 Γ " ⊢c " C1 "<:" C2 => Subcapturing Γ C1 C2 end Capybara diff --git a/Capybara/StaticSemantics/Subtyping.lean b/Capybara/StaticSemantics/Subtyping.lean index c83b72eb..825a95c9 100644 --- a/Capybara/StaticSemantics/Subtyping.lean +++ b/Capybara/StaticSemantics/Subtyping.lean @@ -50,4 +50,8 @@ inductive ESubtyping : Context n m k -> EType n m k -> EType n m k -> Prop end +notation:50 Γ " ⊢s " S1 " <: " S2 => SSubtyping Γ S1 S2 +notation:50 Γ " ⊢ " C1 " <: " C2 => CSubtyping Γ C1 C2 +notation:50 Γ " ⊢e " E1 " <: " E2 => ESubtyping Γ E1 E2 + end Capybara From 0ce7a71cc1a86544475af0e64ce14cfed3170b1f Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 7 Jan 2025 15:19:41 +0100 Subject: [PATCH 23/84] add CaptureRoot --- Capybara/StaticSemantics/CaptureRoot.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 Capybara/StaticSemantics/CaptureRoot.lean diff --git a/Capybara/StaticSemantics/CaptureRoot.lean b/Capybara/StaticSemantics/CaptureRoot.lean new file mode 100644 index 00000000..1b528762 --- /dev/null +++ b/Capybara/StaticSemantics/CaptureRoot.lean @@ -0,0 +1,15 @@ +import Capybara.Syntax +namespace Capybara + +/-! +A capture root is a qualified access to an abstract capture variable. +-/ +structure Root (k : Nat) where + c : Fin k + m : Mode + +inductive Roots (k : Nat) where +| empty : Roots k +| cons : Root k -> Roots k -> Roots k + +end Capybara From d7bf821e39bc9e6a636e7e7d40a3059ab3ad91f6 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 7 Jan 2025 15:40:10 +0100 Subject: [PATCH 24/84] finish capture root --- Capybara/StaticSemantics/CaptureRoot.lean | 49 +++++++++++++++++++---- 1 file changed, 42 insertions(+), 7 deletions(-) diff --git a/Capybara/StaticSemantics/CaptureRoot.lean b/Capybara/StaticSemantics/CaptureRoot.lean index 1b528762..2bad24bc 100644 --- a/Capybara/StaticSemantics/CaptureRoot.lean +++ b/Capybara/StaticSemantics/CaptureRoot.lean @@ -2,14 +2,49 @@ import Capybara.Syntax namespace Capybara /-! -A capture root is a qualified access to an abstract capture variable. +A capture root is a set of qualified access to abstract capture variables. -/ -structure Root (k : Nat) where - c : Fin k - m : Mode +inductive CaptureRoot (k : Nat) where +| empty : CaptureRoot k +| union : CaptureRoot k -> CaptureRoot k -> CaptureRoot k +| singleton : Fin k -> Mode -> CaptureRoot k -inductive Roots (k : Nat) where -| empty : Roots k -| cons : Root k -> Roots k -> Roots k +/-! +Instances of `CaptureRoot`: empty, union. +-/ + +instance : EmptyCollection (CaptureRoot k) := ⟨CaptureRoot.empty⟩ +instance : Union (CaptureRoot k) := ⟨CaptureRoot.union⟩ + +/-! +The capture root of a capture set under a context. + +The relation `CaptureSet.Root C Γ D` defines how a capture set `C` maps to its root capture variables `D` +under the context `Γ`. The root captures represent the original abstract capture variables that are the +source of the captures in the set. This relation is defined inductively with the following cases: + +* Empty: An empty capture set maps to an empty root set +* Union: The root of a union of capture sets is the union of their roots +* Singleton: A singleton capture of a variable maps to the root of its type's capture set +* Parameter: A singleton capture of a parameter maps directly to that parameter with its mode +* Alias: A singleton capture of an alias maps to the root of its aliased capture set +-/ +inductive CaptureSet.Root : CaptureSet n k -> Context n m k -> CaptureRoot k -> Prop where +| empty : CaptureSet.Root {} Context.empty {} +| union : + Root C1 Γ D1 -> + Root C2 Γ D2 -> + Root (C1 ∪ C2) Γ (D1 ∪ D2) +| singleton : + Context.Lookup Γ x (CType.capt C m0 S0) -> + CaptureSet.Root (C.qualified m) Γ D -> + CaptureSet.Root ({x@m:=x}) Γ D +| csingleton_param : + Context.LookupC Γ c (cparam k) -> + CaptureSet.Root ({c@m:=c}) Γ (CaptureRoot.singleton c m) +| csingleton_alias : + Context.LookupC Γ c (calias C) -> + CaptureSet.Root (C.qualified m) Γ D -> + CaptureSet.Root ({c@m:=c}) Γ D end Capybara From 16eefc7bd4ab4bd100a77b30f409cf385a7d0a6d Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 7 Jan 2025 15:52:31 +0100 Subject: [PATCH 25/84] def: kinding of capture roots --- Capybara/StaticSemantics/Kinding.lean | 30 +++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 Capybara/StaticSemantics/Kinding.lean diff --git a/Capybara/StaticSemantics/Kinding.lean b/Capybara/StaticSemantics/Kinding.lean new file mode 100644 index 00000000..01b947d1 --- /dev/null +++ b/Capybara/StaticSemantics/Kinding.lean @@ -0,0 +1,30 @@ +import Capybara.Syntax +import Capybara.StaticSemantics.CaptureRoot +namespace Capybara + +/-! +Kinding of capture roots. +- `empty` and `union` are structural rules +- `k_ro`: a readonly access is immutable +- `k_imm`: any access to an immutable capture set variable is immutable +- `k_mut`: any access can be counted as mutable +- `k_fresh`: access to a fresh capture set variable is fresh +-/ +inductive CaptureRoot.Kinding : Context n m k -> CaptureRoot k -> Kind -> Prop where +| empty : CaptureRoot.Kinding Γ {} Kind.Imm +| union : + CaptureRoot.Kinding Γ D1 K -> + CaptureRoot.Kinding Γ D2 K -> + CaptureRoot.Kinding Γ (D1 ∪ D2) K +| k_ro : + CaptureRoot.Kinding Γ (CaptureRoot.singleton c ro) Kind.Imm +| k_imm : + Context.LookupC Γ c (cparam Kind.Imm) -> + CaptureRoot.Kinding Γ (CaptureRoot.singleton c m) Kind.Imm +| k_mut : + CaptureRoot.Kinding Γ (CaptureRoot.singleton c m) Kind.Mut +| k_fresh : + Context.LookupC Γ c (cparam Kind.Fresh) -> + CaptureRoot.Kinding Γ (CaptureRoot.singleton c m) Kind.Fresh + +end Capybara From e19416d0eaf000bbdb47a1c1260121fe45e2d233 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 7 Jan 2025 15:53:36 +0100 Subject: [PATCH 26/84] def: capture set kinding --- Capybara/StaticSemantics/Kinding.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Capybara/StaticSemantics/Kinding.lean b/Capybara/StaticSemantics/Kinding.lean index 01b947d1..e3ad0f71 100644 --- a/Capybara/StaticSemantics/Kinding.lean +++ b/Capybara/StaticSemantics/Kinding.lean @@ -27,4 +27,13 @@ inductive CaptureRoot.Kinding : Context n m k -> CaptureRoot k -> Kind -> Prop w Context.LookupC Γ c (cparam Kind.Fresh) -> CaptureRoot.Kinding Γ (CaptureRoot.singleton c m) Kind.Fresh +/-! +Kinding of capture sets is defined by the kinding of its root capture variables. +-/ +inductive CaptureSet.Kinding : Context n m k -> CaptureSet n k -> Kind -> Prop where +| mk : + CaptureSet.Root C Γ D -> + D.Kinding Γ K -> + CaptureSet.Kinding Γ C K + end Capybara From 778c581f671361e9b9d0da105fbb4149e8c51e85 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 7 Jan 2025 15:55:56 +0100 Subject: [PATCH 27/84] def: CaptureRoot.HasElem --- Capybara/StaticSemantics/CaptureRoot.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/Capybara/StaticSemantics/CaptureRoot.lean b/Capybara/StaticSemantics/CaptureRoot.lean index 2bad24bc..f323437a 100644 --- a/Capybara/StaticSemantics/CaptureRoot.lean +++ b/Capybara/StaticSemantics/CaptureRoot.lean @@ -47,4 +47,17 @@ inductive CaptureSet.Root : CaptureSet n k -> Context n m k -> CaptureRoot k -> CaptureSet.Root (C.qualified m) Γ D -> CaptureSet.Root ({c@m:=c}) Γ D +/-! +Membership of an access in a capture root. +-/ +inductive CaptureRoot.HasElem : CaptureRoot k -> Fin k -> Mode -> Prop where +| union_l : + HasElem D1 c m -> + HasElem (D1 ∪ D2) c m +| union_r : + HasElem D2 c m -> + HasElem (D1 ∪ D2) c m +| singleton : + HasElem (CaptureRoot.singleton c m) c m + end Capybara From 4623472c652a1c86ee4d2f88c042963093ec8e2e Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 7 Jan 2025 15:59:05 +0100 Subject: [PATCH 28/84] def: chaining --- Capybara/StaticSemantics/Chaining.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 Capybara/StaticSemantics/Chaining.lean diff --git a/Capybara/StaticSemantics/Chaining.lean b/Capybara/StaticSemantics/Chaining.lean new file mode 100644 index 00000000..6dc719d1 --- /dev/null +++ b/Capybara/StaticSemantics/Chaining.lean @@ -0,0 +1,14 @@ +import Capybara.StaticSemantics.CaptureRoot +namespace Capybara + +def CaptureRoot.Chaining (D1 D2 : CaptureRoot k) : Prop := + ∀c, HasElem D1 c drop -> (∀m, HasElem D2 c m -> False) + +inductive CaptureSet.Chaining : Context n m k -> CaptureSet n k -> CaptureSet n k -> Prop where +| mk : + CaptureSet.Root C1 Γ D1 -> + CaptureSet.Root C2 Γ D2 -> + D1.Chaining D2 -> + CaptureSet.Chaining Γ C1 C2 + +end Capybara From ca386ad1912a123c16adb51287ce6c411ae2b2a5 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 7 Jan 2025 22:41:05 +0100 Subject: [PATCH 29/84] staging --- Capybara/StaticSemantics/Separation.lean | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 Capybara/StaticSemantics/Separation.lean diff --git a/Capybara/StaticSemantics/Separation.lean b/Capybara/StaticSemantics/Separation.lean new file mode 100644 index 00000000..32b22808 --- /dev/null +++ b/Capybara/StaticSemantics/Separation.lean @@ -0,0 +1,4 @@ +import Capybara.StaticSemantics.CaptureRoot +namespace Capybara + +end Capybara From 099607cc580329c86c1d28e99977308947f8cb60 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 7 Jan 2025 22:49:47 +0100 Subject: [PATCH 30/84] def: define Separation --- Capybara/StaticSemantics/Separation.lean | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/Capybara/StaticSemantics/Separation.lean b/Capybara/StaticSemantics/Separation.lean index 32b22808..e381ab43 100644 --- a/Capybara/StaticSemantics/Separation.lean +++ b/Capybara/StaticSemantics/Separation.lean @@ -1,4 +1,24 @@ import Capybara.StaticSemantics.CaptureRoot namespace Capybara +/-! +Separation checking for capture roots. +-/ +def CaptureRoot.Separation (Γ : Context n m k) (D1 D2 : CaptureRoot k) : Prop := + -- Two capture roots are separated if given any shared access m1 c and m2 c, + ∀m1 m2 c, HasElem D1 c m1 -> HasElem D2 c m2 -> + -- either both are read-only, or + ((m1 = ro ∧ m2 = ro) ∨ + -- c is an immutable capture variable + (Γ.LookupC c (cparam Kind.Imm))) + +inductive CaptureSet.Separation : Context n m k -> CaptureSet n k -> CaptureSet n k -> Prop where +| mk : + CaptureSet.Root C1 Γ D1 -> + CaptureSet.Root C2 Γ D2 -> + CaptureRoot.Separation Γ D1 D2 -> + CaptureSet.Separation Γ C1 C2 + +notation:50 Γ " ⊢ " C1 " ⋈ " C2 => CaptureSet.Separation Γ C1 C2 + end Capybara From e06110d7a33e7321bc7e71215725065df95b2d8e Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 7 Jan 2025 22:49:57 +0100 Subject: [PATCH 31/84] infra: add notation for chainning --- Capybara/StaticSemantics/Chaining.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Capybara/StaticSemantics/Chaining.lean b/Capybara/StaticSemantics/Chaining.lean index 6dc719d1..d657ff21 100644 --- a/Capybara/StaticSemantics/Chaining.lean +++ b/Capybara/StaticSemantics/Chaining.lean @@ -11,4 +11,6 @@ inductive CaptureSet.Chaining : Context n m k -> CaptureSet n k -> CaptureSet n D1.Chaining D2 -> CaptureSet.Chaining Γ C1 C2 +notation:50 Γ " ⊢ " C1 " >> " C2 => CaptureSet.Chaining Γ C1 C2 + end Capybara From 23f7f0e458a1660d301924d1fa81acb1dd889bfa Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 7 Jan 2025 22:52:21 +0100 Subject: [PATCH 32/84] def: add capture root drop --- Capybara/StaticSemantics/CaptureRoot.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Capybara/StaticSemantics/CaptureRoot.lean b/Capybara/StaticSemantics/CaptureRoot.lean index f323437a..8139739e 100644 --- a/Capybara/StaticSemantics/CaptureRoot.lean +++ b/Capybara/StaticSemantics/CaptureRoot.lean @@ -60,4 +60,12 @@ inductive CaptureRoot.HasElem : CaptureRoot k -> Fin k -> Mode -> Prop where | singleton : HasElem (CaptureRoot.singleton c m) c m +/-! +Qualifying all access in a capture root to `drop`. +-/ +def CaptureRoot.drop : CaptureRoot k -> CaptureRoot k +| CaptureRoot.empty => CaptureRoot.empty +| CaptureRoot.union D1 D2 => CaptureRoot.union (CaptureRoot.drop D1) (CaptureRoot.drop D2) +| CaptureRoot.singleton c _ => CaptureRoot.singleton c drop + end Capybara From 1cf68493dd365156dc40491097ea132254435ce1 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 7 Jan 2025 22:54:46 +0100 Subject: [PATCH 33/84] def: rename `MorePermissive` to `LessPermissive` --- Capybara/Syntax/Mode.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Capybara/Syntax/Mode.lean b/Capybara/Syntax/Mode.lean index 2da8622e..9f492eda 100644 --- a/Capybara/Syntax/Mode.lean +++ b/Capybara/Syntax/Mode.lean @@ -13,11 +13,11 @@ notation "ε" => Mode.M Mutability.default notation "drop" => Mode.drop /-! -Which mutability mode is more permissive? +Given `m1` and `m2`, `LessPermissive m1 m2` means that `m1` is less permissive than `m2`. -/ -inductive MorePermissive : Mutability -> Mutability -> Prop where -| readonly : MorePermissive Mutability.readonly Mutability.default -| refl : MorePermissive m m +inductive LessPermissive : Mutability -> Mutability -> Prop where +| readonly : LessPermissive Mutability.readonly Mutability.default +| refl : LessPermissive m m end Capybara From df7099b541d9b567f98e70e4a65deb61f6ed6b84 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 7 Jan 2025 22:58:15 +0100 Subject: [PATCH 34/84] def: typing judgement wip --- Capybara/StaticSemantics/Typing.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 Capybara/StaticSemantics/Typing.lean diff --git a/Capybara/StaticSemantics/Typing.lean b/Capybara/StaticSemantics/Typing.lean new file mode 100644 index 00000000..f2099a87 --- /dev/null +++ b/Capybara/StaticSemantics/Typing.lean @@ -0,0 +1,14 @@ +import Capybara.StaticSemantics.CaptureRoot +import Capybara.StaticSemantics.Chaining +import Capybara.StaticSemantics.Separation +import Capybara.StaticSemantics.Subtyping +namespace Capybara + +inductive Typed : CaptureSet n k -> Context n m k -> Term n m k -> EType n m k -> Prop where +| var : + Γ.Lookup x (CType.capt C m S) -> + LessPermissive m' m -> + -------------------------------- + Typed ({x@Mode.M m':=x}) Γ (Term.var x) (EType.type (CType.capt ({x:=x}) m' S)) + +end Capybara From 0bb595369542539687f29938980b77c499bce865 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 8 Jan 2025 14:24:42 +0100 Subject: [PATCH 35/84] def: typing (WIP) --- Capybara/Morphism/Core.lean | 33 +++++++++++++++++++++++ Capybara/StaticSemantics/CaptureRoot.lean | 16 +++++++---- Capybara/StaticSemantics/Typing.lean | 22 +++++++++++++++ Capybara/Syntax/CaptureSet/Core.lean | 6 +++++ Capybara/Syntax/Mode.lean | 1 + Capybara/Syntax/Type.lean | 1 + Capybara/Syntax/Type/Core.lean | 1 + Capybara/Syntax/Type/Opening.lean | 7 +++++ 8 files changed, 82 insertions(+), 5 deletions(-) create mode 100644 Capybara/Syntax/Type/Opening.lean diff --git a/Capybara/Morphism/Core.lean b/Capybara/Morphism/Core.lean index 1b0e3dc3..2e6803f8 100644 --- a/Capybara/Morphism/Core.lean +++ b/Capybara/Morphism/Core.lean @@ -41,10 +41,22 @@ def FinFun.ext (f : FinFun n n') : FinFun (n+1) (n'+1) := by def FinFun.id {n : Nat} : FinFun n n := fun x => x +/-! +A weaken function that shifts all indices by one. +-/ def FinFun.weaken {n : Nat} : FinFun n (n+1) := by intro x exact Fin.succ x +/-! +Open a bound variable. +-/ +def FinFun.open {n : Nat} (x : Fin n) : FinFun (n+1) n := by + intro y + cases y using Fin.cases + case zero => exact x + case succ y0 => exact y0 + /-! A renaming function, which maps the three dimensions of a context (term, type, and capture set variables). -/ @@ -116,4 +128,25 @@ def Renaming.cweaken : Renaming n m k n m (k+1) := cvar := FinFun.weaken } +def Renaming.open (x : Fin n) : Renaming (n+1) m k n m k := + { + var := FinFun.open x + tvar := FinFun.id + cvar := FinFun.id + } + +def Renaming.topen (X : Fin m) : Renaming n (m+1) k n m k := + { + var := FinFun.id + tvar := FinFun.open X + cvar := FinFun.id + } + +def Renaming.copen (X : Fin k) : Renaming n m (k+1) n m k := + { + var := FinFun.id + tvar := FinFun.id + cvar := FinFun.open X + } + end Capybara diff --git a/Capybara/StaticSemantics/CaptureRoot.lean b/Capybara/StaticSemantics/CaptureRoot.lean index 8139739e..323d3b87 100644 --- a/Capybara/StaticSemantics/CaptureRoot.lean +++ b/Capybara/StaticSemantics/CaptureRoot.lean @@ -1,4 +1,5 @@ import Capybara.Syntax +import Capybara.StaticSemantics.Subcapturing namespace Capybara /-! @@ -61,11 +62,16 @@ inductive CaptureRoot.HasElem : CaptureRoot k -> Fin k -> Mode -> Prop where HasElem (CaptureRoot.singleton c m) c m /-! -Qualifying all access in a capture root to `drop`. +All capture roots are dropped by this capture set. -/ -def CaptureRoot.drop : CaptureRoot k -> CaptureRoot k -| CaptureRoot.empty => CaptureRoot.empty -| CaptureRoot.union D1 D2 => CaptureRoot.union (CaptureRoot.drop D1) (CaptureRoot.drop D2) -| CaptureRoot.singleton c _ => CaptureRoot.singleton c drop +inductive CaptureRoot.Dropped : CaptureRoot k -> CaptureSet n k -> Prop where +| empty : CaptureRoot.Dropped {} C +| union : + Dropped D1 C -> + Dropped D2 C -> + Dropped (D1 ∪ D2) C +| singleton : + Subcapturing Γ ({c@drop:=c}) C -> + Dropped (CaptureRoot.singleton c m) C end Capybara diff --git a/Capybara/StaticSemantics/Typing.lean b/Capybara/StaticSemantics/Typing.lean index f2099a87..acebb348 100644 --- a/Capybara/StaticSemantics/Typing.lean +++ b/Capybara/StaticSemantics/Typing.lean @@ -2,6 +2,7 @@ import Capybara.StaticSemantics.CaptureRoot import Capybara.StaticSemantics.Chaining import Capybara.StaticSemantics.Separation import Capybara.StaticSemantics.Subtyping +import Capybara.StaticSemantics.Kinding namespace Capybara inductive Typed : CaptureSet n k -> Context n m k -> Term n m k -> EType n m k -> Prop where @@ -10,5 +11,26 @@ inductive Typed : CaptureSet n k -> Context n m k -> Term n m k -> EType n m k - LessPermissive m' m -> -------------------------------- Typed ({x@Mode.M m':=x}) Γ (Term.var x) (EType.type (CType.capt ({x:=x}) m' S)) +| pack : + Typed C' Γ (Term.var x) (EType.type (T.copen c)) -> + CaptureSet.Root ({c:=c}) Γ R -> + CaptureRoot.Kinding Γ R Kind.Fresh -> + CaptureRoot.Dropped R C' -> + ----------------------------------------------------- + Typed C' Γ (Term.pack c x) (EType.ex T) +| sub : + Typed C Γ t E -> + (Γ ⊢c C <: C') -> + (Γ ⊢e E <: E') -> + -------------------------------- + Typed C' Γ t E' +| abs : + Typed (C.weaken ∪ CaptureSet.span x) (Γ,x:T) t E -> + -------------------------------- + Typed {} Γ (Term.lam T t) (EType.type (((x:T)->E)^[ε]C)) +| tabs : + Typed C (Γ,X:tparam S) t E -> + -------------------------------- + Typed C Γ (Term.tlam S t) (EType.type (([X<:S]->E)^[ε]C)) end Capybara diff --git a/Capybara/Syntax/CaptureSet/Core.lean b/Capybara/Syntax/CaptureSet/Core.lean index 76a71baa..1ff8fad5 100644 --- a/Capybara/Syntax/CaptureSet/Core.lean +++ b/Capybara/Syntax/CaptureSet/Core.lean @@ -102,4 +102,10 @@ inductive CaptureSet.Subset : CaptureSet n k -> CaptureSet n k -> Prop where instance : HasSubset (CaptureSet n k) where Subset := CaptureSet.Subset +/-! +Spanning a capture set over a variable. +-/ +def CaptureSet.span (x : Fin n) : CaptureSet n k := + ({x:=x}) ∪ ({x@ro:=x}) ∪ ({x@drop:=x}) + end Capybara diff --git a/Capybara/Syntax/Mode.lean b/Capybara/Syntax/Mode.lean index 9f492eda..0ca54f2e 100644 --- a/Capybara/Syntax/Mode.lean +++ b/Capybara/Syntax/Mode.lean @@ -10,6 +10,7 @@ inductive Mode : Type where notation "ro" => Mode.M Mutability.readonly notation "ε" => Mode.M Mutability.default +notation "ε" => Mutability.default notation "drop" => Mode.drop /-! diff --git a/Capybara/Syntax/Type.lean b/Capybara/Syntax/Type.lean index f5c9a880..5718ef89 100644 --- a/Capybara/Syntax/Type.lean +++ b/Capybara/Syntax/Type.lean @@ -1,3 +1,4 @@ import Capybara.Syntax.Type.Core import Capybara.Syntax.Type.Renaming import Capybara.Syntax.Type.Weakening +import Capybara.Syntax.Type.Opening diff --git a/Capybara/Syntax/Type/Core.lean b/Capybara/Syntax/Type/Core.lean index 804307f4..f17e1faf 100644 --- a/Capybara/Syntax/Type/Core.lean +++ b/Capybara/Syntax/Type/Core.lean @@ -35,5 +35,6 @@ notation:40 "[X<:" S "]->" T => SType.tarrow S T notation:40 "(x:" S ")->" T => SType.arrow S T notation:40 "[c:" S "]->" T => SType.carrow S T notation:50 S "^[" m "]" C => CType.capt C m S +notation:50 S "^" C => CType.capt C ε S end Capybara diff --git a/Capybara/Syntax/Type/Opening.lean b/Capybara/Syntax/Type/Opening.lean new file mode 100644 index 00000000..088b8070 --- /dev/null +++ b/Capybara/Syntax/Type/Opening.lean @@ -0,0 +1,7 @@ +import Capybara.Syntax.Type.Renaming +namespace Capybara + +def CType.copen (T : CType n m (k+1)) (c : Fin k) : CType n m k := + T.rename (Renaming.copen c) + +end Capybara From ae402c645ded190e65f6a42ae2a7a5bb2e23a67d Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 15 Jan 2025 12:08:35 +0800 Subject: [PATCH 36/84] staging --- Capybara/StaticSemantics/Typing.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Capybara/StaticSemantics/Typing.lean b/Capybara/StaticSemantics/Typing.lean index acebb348..5c203672 100644 --- a/Capybara/StaticSemantics/Typing.lean +++ b/Capybara/StaticSemantics/Typing.lean @@ -30,7 +30,7 @@ inductive Typed : CaptureSet n k -> Context n m k -> Term n m k -> EType n m k - Typed {} Γ (Term.lam T t) (EType.type (((x:T)->E)^[ε]C)) | tabs : Typed C (Γ,X:tparam S) t E -> - -------------------------------- + --------------------------------- Typed C Γ (Term.tlam S t) (EType.type (([X<:S]->E)^[ε]C)) end Capybara From fa60488de28167da0ccc06ce4b708bb53be49440 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 15 Jan 2025 12:16:33 +0800 Subject: [PATCH 37/84] lib: add finite set --- Capybara/Lib/FiniteSet.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 Capybara/Lib/FiniteSet.lean diff --git a/Capybara/Lib/FiniteSet.lean b/Capybara/Lib/FiniteSet.lean new file mode 100644 index 00000000..cd9b0e1f --- /dev/null +++ b/Capybara/Lib/FiniteSet.lean @@ -0,0 +1,11 @@ +namespace Capybara + +/-! + +-/ +inductive FiniteSet : Type -> Type where +| empty : FiniteSet A +| union : FiniteSet A -> FiniteSet A -> FiniteSet A +| singleton : A -> FiniteSet A + +end Capybara From 85982a3d54b618e085f5a4f1a97a823512dbf90a Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 15 Jan 2025 12:23:55 +0800 Subject: [PATCH 38/84] lib: operations and properties for finite set --- Capybara/Lib.lean | 1 + Capybara/Lib/FiniteSet.lean | 49 +++++++++++++++++++++++++++++++++++-- 2 files changed, 48 insertions(+), 2 deletions(-) create mode 100644 Capybara/Lib.lean diff --git a/Capybara/Lib.lean b/Capybara/Lib.lean new file mode 100644 index 00000000..922414e3 --- /dev/null +++ b/Capybara/Lib.lean @@ -0,0 +1 @@ +import Capybara.Lib.FiniteSet diff --git a/Capybara/Lib/FiniteSet.lean b/Capybara/Lib/FiniteSet.lean index cd9b0e1f..06adec97 100644 --- a/Capybara/Lib/FiniteSet.lean +++ b/Capybara/Lib/FiniteSet.lean @@ -1,11 +1,56 @@ namespace Capybara /-! - --/ +Inductively defined finite sets. +!-/ inductive FiniteSet : Type -> Type where | empty : FiniteSet A | union : FiniteSet A -> FiniteSet A -> FiniteSet A | singleton : A -> FiniteSet A +/-! +Instances for finite sets: empty collection, union, singleton. +!-/ +@[simp] +instance : EmptyCollection (FiniteSet A) where + emptyCollection := FiniteSet.empty + +@[simp] +instance : Union (FiniteSet A) where + union := FiniteSet.union + +@[simp] +instance : Singleton A (FiniteSet A) where + singleton := FiniteSet.singleton + +/-! +Definition of the renaming operator. +!-/ +def FiniteSet.rename : FiniteSet A -> (A -> B) -> FiniteSet B +| FiniteSet.empty, _ => {} +| FiniteSet.union s1 s2, f => (s1.rename f) ∪ (s2.rename f) +| FiniteSet.singleton a, f => {f a} + +/-! +Membership. +!-/ +inductive FiniteSet.HasElem : FiniteSet A -> A -> Prop where +| singleton : FiniteSet.HasElem {a} a +| union_l : FiniteSet.HasElem s1 a -> FiniteSet.HasElem (s1 ∪ s2) a +| union_r : FiniteSet.HasElem s2 a -> FiniteSet.HasElem (s1 ∪ s2) a + +instance : Membership (FiniteSet A) A where + mem := fun a A => FiniteSet.HasElem A a + +/-! +Properties of finite sets. +!-/ +theorem FiniteSet.rename_empty : FiniteSet.rename {} f = {} := rfl + +theorem FiniteSet.rename_singleton : FiniteSet.rename {a} f = {f a} := rfl + +theorem FiniteSet.rename_union : + FiniteSet.rename (s1 ∪ s2) f = (s1.rename f) ∪ (s2.rename f) := + rfl + end Capybara From 9c30d57681082506a7f1710f06488e980f2ee93a Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 16 Jan 2025 16:57:47 +0800 Subject: [PATCH 39/84] def: migrate type to the latest version --- Capybara/Syntax/Type/Core.lean | 15 ++++++++------- Capybara/Syntax/Type/Renaming.lean | 11 ++++++++++- 2 files changed, 18 insertions(+), 8 deletions(-) diff --git a/Capybara/Syntax/Type/Core.lean b/Capybara/Syntax/Type/Core.lean index f17e1faf..dd526bc1 100644 --- a/Capybara/Syntax/Type/Core.lean +++ b/Capybara/Syntax/Type/Core.lean @@ -2,12 +2,11 @@ import Capybara.Syntax.CaptureSet.Core namespace Capybara /-! -Kinds of capture set parameters. +Separation degree. -/ -inductive Kind : Type where -| Imm : Kind -| Mut : Kind -| Fresh : Kind +inductive SepDegree : Nat -> Nat -> Type where +| Mut : CaptureSet n k -> SepDegree n k +| Imm : CaptureSet n k -> SepDegree n k mutual @@ -23,7 +22,8 @@ inductive SType : Nat -> Nat -> Nat -> Type where | tvar : Fin m -> SType n m k | tarrow : SType n m k -> EType n (m+1) k -> SType n m k | arrow : CType n m k -> EType (n+1) m k -> SType n m k -| carrow : Kind -> EType n m (k+1) -> SType n m k +| carrow : SepDegree n k -> EType n m (k+1) -> SType n m k +| farrow : CType n m (k+1) -> EType (n+1) m (k+1) -> SType n m k end @@ -33,7 +33,8 @@ Notation for types. notation:max "⊤" => SType.top notation:40 "[X<:" S "]->" T => SType.tarrow S T notation:40 "(x:" S ")->" T => SType.arrow S T -notation:40 "[c:" S "]->" T => SType.carrow S T +notation:40 "[c:" D "]->" T => SType.carrow D T +notation:40 "[c:Fresh](x:" T ")->" E => SType.farrow T E notation:50 S "^[" m "]" C => CType.capt C m S notation:50 S "^" C => CType.capt C ε S diff --git a/Capybara/Syntax/Type/Renaming.lean b/Capybara/Syntax/Type/Renaming.lean index 33f0a023..3ae3482b 100644 --- a/Capybara/Syntax/Type/Renaming.lean +++ b/Capybara/Syntax/Type/Renaming.lean @@ -1,6 +1,14 @@ import Capybara.Syntax.Type.Core namespace Capybara +def SepDegree.rename + (D : SepDegree n k) + (ρ : Renaming n m k n' m' k') : + SepDegree n' k' := + match D with + | Imm C => Imm (C.rename ρ) + | Mut C => Mut (C.rename ρ) + mutual def EType.rename @@ -23,7 +31,8 @@ def SType.rename (S : SType n m k) (ρ : Renaming n m k n' m' k') : SType n' m' | SType.top => SType.top | SType.tvar x => SType.tvar (ρ.tvar x) | SType.arrow T E => (x:T.rename ρ)->(E.rename ρ.ext) - | SType.carrow k E => [c:k]->(E.rename ρ.cext) + | SType.carrow D E => [c:D.rename ρ]->(E.rename ρ.cext) + | SType.farrow T E => [c:Fresh](x:T.rename ρ.cext)->(E.rename ρ.cext.ext) | SType.tarrow S T => [X<:S.rename ρ]->(T.rename ρ.text) end From 27f50e38a37b367099308b09dacc592dcabdebfd Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 16 Jan 2025 17:00:32 +0800 Subject: [PATCH 40/84] def: update `Term` --- Capybara/Syntax/Term.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Capybara/Syntax/Term.lean b/Capybara/Syntax/Term.lean index 04c401cf..e236a339 100644 --- a/Capybara/Syntax/Term.lean +++ b/Capybara/Syntax/Term.lean @@ -13,7 +13,7 @@ This module defines the syntax of terms in the Capybara language. ## Term Constructors - Variables: `var` -- Functions: `lam` (term abstraction), `tlam` (type abstraction), `clam` (capture set abstraction) +- Functions: `lam` (term abstraction), `tlam` (type abstraction), `clam` (capture abstraction), `flam` (fresh capture abstraction) - Applications: `app` (term application), `tapp` (type application), `capp` (capture set application) - Capture set operations: `pack` (capture set creation), `unpack` (capture set elimination) - Let bindings: `letin` (term binding) @@ -30,7 +30,8 @@ inductive Term : Nat -> Nat -> Nat -> Type where | var : Fin n -> Term n m k | lam : CType n m k -> Term (n+1) m k -> Term n m k | tlam : SType n m k -> Term n (m+1) k -> Term n m k -| clam : Kind -> Term n m (k+1) -> Term n m k +| clam : SepDegree n k -> Term n m (k+1) -> Term n m k +| flam : CType n m (k+1) -> Term (n+1) m (k+1) -> Term n m k | pack : Fin k -> Fin n -> Term n m k | app : Fin n -> Fin n -> Term n m k | tapp : Fin n -> Fin m -> Term n m k @@ -51,7 +52,8 @@ def Term.rename | var x => var (ρ.var x) | lam t1 t2 => lam (t1.rename ρ) (t2.rename ρ.ext) | tlam t1 t2 => tlam (t1.rename ρ) (t2.rename ρ.text) - | clam k t => clam k (t.rename ρ.cext) + | clam D t => clam (D.rename ρ) (t.rename ρ.cext) + | flam T t => flam (T.rename ρ.cext) (t.rename ρ.cext.ext) | pack x y => pack (ρ.cvar x) (ρ.var y) | app x y => app (ρ.var x) (ρ.var y) | tapp x X => tapp (ρ.var x) (ρ.tvar X) From e9770dd01670f32613ded5937574d62783b5cd81 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 16 Jan 2025 17:03:41 +0800 Subject: [PATCH 41/84] def: `Context` --- Capybara/Syntax/Context.lean | 20 +++++++++++++++++--- Capybara/Syntax/Type/Weakening.lean | 6 ++++++ 2 files changed, 23 insertions(+), 3 deletions(-) diff --git a/Capybara/Syntax/Context.lean b/Capybara/Syntax/Context.lean index 137a1ece..4e586058 100644 --- a/Capybara/Syntax/Context.lean +++ b/Capybara/Syntax/Context.lean @@ -2,6 +2,13 @@ import Mathlib.Data.Fin.Basic import Capybara.Syntax.Type namespace Capybara +/-! +Kind of a capture set parameter. +-/ +inductive CKind : Nat -> Nat -> Type where +| Sep : SepDegree n k -> CKind n k +| Fresh : CKind n k + /-! Type binding and capture set binding. @@ -13,8 +20,9 @@ inductive TBinding : Nat -> Nat -> Nat -> Type where | param : SType n m k -> TBinding n m k | alias : SType n m k -> TBinding n m k + inductive CBinding : Nat -> Nat -> Type where -| param : Kind -> CBinding n k +| param : CKind n k -> CBinding n k | alias : CaptureSet n k -> CBinding n k notation:max "tparam" S => TBinding.param S @@ -28,8 +36,11 @@ Weakening functions for type and capture set binding. def TBinding.weaken : TBinding n m k -> TBinding (n+1) m k | TBinding.param T => TBinding.param (T.weaken) | TBinding.alias T => TBinding.alias (T.weaken) +def CKind.weaken : CKind n k -> CKind (n+1) k +| CKind.Sep D => CKind.Sep (D.weaken) +| CKind.Fresh => CKind.Fresh def CBinding.weaken : CBinding n k -> CBinding (n+1) k -| CBinding.param k => CBinding.param k +| CBinding.param k => CBinding.param (k.weaken) | CBinding.alias C => CBinding.alias (C.weaken) def TBinding.tweaken : TBinding n m k -> TBinding n (m+1) k | TBinding.param T => TBinding.param (T.tweaken) @@ -37,8 +48,11 @@ def TBinding.tweaken : TBinding n m k -> TBinding n (m+1) k def TBinding.cweaken : TBinding n m k -> TBinding n m (k+1) | TBinding.param T => TBinding.param (T.cweaken) | TBinding.alias T => TBinding.alias (T.cweaken) +def CKind.cweaken : CKind n k -> CKind n (k+1) +| CKind.Sep D => CKind.Sep (D.cweaken) +| CKind.Fresh => CKind.Fresh def CBinding.cweaken : CBinding n k -> CBinding n (k+1) -| CBinding.param k => CBinding.param k +| CBinding.param k => CBinding.param (k.cweaken) | CBinding.alias C => CBinding.alias (C.cweaken) /-! diff --git a/Capybara/Syntax/Type/Weakening.lean b/Capybara/Syntax/Type/Weakening.lean index c1e69891..80a7ee02 100644 --- a/Capybara/Syntax/Type/Weakening.lean +++ b/Capybara/Syntax/Type/Weakening.lean @@ -10,6 +10,9 @@ def CType.weaken : CType n m k -> CType (n+1) m k := fun T => T.rename Renaming.weaken def SType.weaken : SType n m k -> SType (n+1) m k := fun S => S.rename Renaming.weaken +def SepDegree.weaken : SepDegree n k -> SepDegree (n+1) k +| SepDegree.Imm C => SepDegree.Imm (C.weaken) +| SepDegree.Mut C => SepDegree.Mut (C.weaken) /-! Type weakening functions. @@ -30,5 +33,8 @@ def CType.cweaken : CType n m k -> CType n m (k+1) := fun T => T.rename Renaming.cweaken def SType.cweaken : SType n m k -> SType n m (k+1) := fun S => S.rename Renaming.cweaken +def SepDegree.cweaken : SepDegree n k -> SepDegree n (k+1) +| SepDegree.Imm C => SepDegree.Imm (C.cweaken) +| SepDegree.Mut C => SepDegree.Mut (C.cweaken) end Capybara From 4f77c6f90060465e13181ab99d32a6449a1e5219 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 16 Jan 2025 20:56:54 +0800 Subject: [PATCH 42/84] def: less-permissive --- Capybara/Syntax/Mode.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Capybara/Syntax/Mode.lean b/Capybara/Syntax/Mode.lean index 0ca54f2e..60006ab8 100644 --- a/Capybara/Syntax/Mode.lean +++ b/Capybara/Syntax/Mode.lean @@ -16,9 +16,13 @@ notation "drop" => Mode.drop /-! Given `m1` and `m2`, `LessPermissive m1 m2` means that `m1` is less permissive than `m2`. -/ -inductive LessPermissive : Mutability -> Mutability -> Prop where +inductive Mutability.LessPermissive : Mutability -> Mutability -> Prop where | readonly : LessPermissive Mutability.readonly Mutability.default | refl : LessPermissive m m +inductive Mode.LessPermissive : Mode -> Mode -> Prop where +| M : Mutability.LessPermissive m1 m2 -> LessPermissive (Mode.M m1) (Mode.M m2) +| drop : LessPermissive m Mode.drop +| refl : LessPermissive m m end Capybara From 468512d325bc3824d82c6ddda9d01cc5b068542c Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Fri, 17 Jan 2025 04:42:25 +0800 Subject: [PATCH 43/84] def: fresh capture application --- Capybara/Syntax/Term.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Capybara/Syntax/Term.lean b/Capybara/Syntax/Term.lean index e236a339..d9e7bb78 100644 --- a/Capybara/Syntax/Term.lean +++ b/Capybara/Syntax/Term.lean @@ -36,6 +36,7 @@ inductive Term : Nat -> Nat -> Nat -> Type where | app : Fin n -> Fin n -> Term n m k | tapp : Fin n -> Fin m -> Term n m k | capp : Fin n -> Fin k -> Term n m k +| fapp : Fin n -> Fin k -> Fin n -> Term n m k | letin : Term n m k -> Term (n+1) m k -> Term n m k | unpack : Term n m k -> Term (n+1) m (k+1) -> Term n m k | calias : CaptureSet n k -> Term n m (k+1) -> Term n m k @@ -58,6 +59,7 @@ def Term.rename | app x y => app (ρ.var x) (ρ.var y) | tapp x X => tapp (ρ.var x) (ρ.tvar X) | capp x c => capp (ρ.var x) (ρ.cvar c) + | fapp x c y => fapp (ρ.var x) (ρ.cvar c) (ρ.var y) | letin t1 t2 => letin (t1.rename ρ) (t2.rename ρ.ext) | unpack t1 t2 => unpack (t1.rename ρ) (t2.rename ρ.cext.ext) | calias C t => calias (C.rename ρ) (t.rename ρ.cext) From c4de6916a7734c631c5a7f046c354091d3834477 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Fri, 17 Jan 2025 12:43:52 +0800 Subject: [PATCH 44/84] def: subcapturing --- Capybara/StaticSemantics/Subcapturing.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Capybara/StaticSemantics/Subcapturing.lean b/Capybara/StaticSemantics/Subcapturing.lean index a04ac941..0ae5110e 100644 --- a/Capybara/StaticSemantics/Subcapturing.lean +++ b/Capybara/StaticSemantics/Subcapturing.lean @@ -23,8 +23,9 @@ inductive Subcapturing : Context n m k -> CaptureSet n k -> CaptureSet n k -> Pr Subcapturing Γ C1 C -> Subcapturing Γ C2 C -> Subcapturing Γ (C1 ∪ C2) C -| ro : - Subcapturing Γ (C.ro) C +| mode {C : CaptureSet n k} : + Mode.LessPermissive m1 m2 -> + Subcapturing Γ (C.qualified m1) (C.qualified m2) | var : Context.Lookup Γ x (CType.capt C m S) -> Subcapturing Γ ({x:=x}) (C.qualified (Mode.M m)) From 243000a3d15ac5581d9dce888dd30cc91574d8e1 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 19 Jan 2025 18:03:32 +0800 Subject: [PATCH 45/84] def: subtyping --- Capybara/StaticSemantics/Subtyping.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Capybara/StaticSemantics/Subtyping.lean b/Capybara/StaticSemantics/Subtyping.lean index 825a95c9..52d29efc 100644 --- a/Capybara/StaticSemantics/Subtyping.lean +++ b/Capybara/StaticSemantics/Subtyping.lean @@ -25,7 +25,7 @@ inductive SSubtyping : Context n m k -> SType n m k -> SType n m k -> Prop ESubtyping (Γ,X:tparam S2) E1 E2 -> SSubtyping Γ ([X<:S1]->E1) ([X<:S2]->E2) | carrow : - ESubtyping (Γ,c:cparam K) E1 E2 -> + ESubtyping (Γ,c:cparam (CKind.Sep K)) E1 E2 -> SSubtyping Γ ([c:K]->E1) ([c:K]->E2) | talias_l : Context.LookupT Γ X (talias S) -> @@ -45,7 +45,7 @@ inductive ESubtyping : Context n m k -> EType n m k -> EType n m k -> Prop CSubtyping Γ T1 T2 -> ESubtyping Γ (EType.type T1) (EType.type T2) | ex : - CSubtyping (Γ,c:cparam Kind.Fresh) T1 T2 -> + CSubtyping (Γ,c:cparam CKind.Fresh) T1 T2 -> ESubtyping Γ (EType.ex T1) (EType.ex T2) end From 8f583a158a6d07fe502f2f0c821e4d459dbfa082 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 20 Jan 2025 10:22:47 +0800 Subject: [PATCH 46/84] def: `ReachRoot` --- Capybara/StaticSemantics/ReachRoot.lean | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 Capybara/StaticSemantics/ReachRoot.lean diff --git a/Capybara/StaticSemantics/ReachRoot.lean b/Capybara/StaticSemantics/ReachRoot.lean new file mode 100644 index 00000000..9096cd5f --- /dev/null +++ b/Capybara/StaticSemantics/ReachRoot.lean @@ -0,0 +1,25 @@ +import Capybara.Syntax +namespace Capybara + +/-! +`ReachRoot Γ C m c` means that the root `c` is reachable at access mode `m` from the capture set `C` under the context `Γ`. +-/ +inductive ReachRoot : Context n m k -> CaptureSet n k -> Mode -> Fin k -> Prop where +| union_l : + ReachRoot Γ C1 m c -> + ReachRoot Γ (C1 ∪ C2) m c +| union_r : + ReachRoot Γ C2 m c -> + ReachRoot Γ (C1 ∪ C2) m c +| var : + Context.Lookup Γ x (S^[m]C) -> + ReachRoot Γ ((C.qualified (Mode.M m)).qualified mu) mu' c -> + ReachRoot Γ ({x@mu:=x}) mu' c +| cvar_alias : + Context.LookupC Γ c (calias C) -> + ReachRoot Γ (C.qualified mu) mu' c' -> + ReachRoot Γ ({c@mu:=c}) mu' c' +| cvar : + ReachRoot Γ ({c@mu:=c}) mu c + +end Capybara From aac5bc91c8c6d1ce22aac3c2e100fec0dd5a49c2 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 20 Jan 2025 10:29:48 +0800 Subject: [PATCH 47/84] def: chaining --- Capybara/StaticSemantics/Chaining.lean | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/Capybara/StaticSemantics/Chaining.lean b/Capybara/StaticSemantics/Chaining.lean index d657ff21..6c7e2e33 100644 --- a/Capybara/StaticSemantics/Chaining.lean +++ b/Capybara/StaticSemantics/Chaining.lean @@ -1,15 +1,13 @@ -import Capybara.StaticSemantics.CaptureRoot +import Capybara.StaticSemantics.ReachRoot namespace Capybara -def CaptureRoot.Chaining (D1 D2 : CaptureRoot k) : Prop := - ∀c, HasElem D1 c drop -> (∀m, HasElem D2 c m -> False) +/-! +`Γ ⊢ C1 >> C2` means that the effects of `C1` and `C2` are chainable. -inductive CaptureSet.Chaining : Context n m k -> CaptureSet n k -> CaptureSet n k -> Prop where -| mk : - CaptureSet.Root C1 Γ D1 -> - CaptureSet.Root C2 Γ D2 -> - D1.Chaining D2 -> - CaptureSet.Chaining Γ C1 C2 +Specifically, anything that has been dropped from `C1` cannot be mentioned by `C2` any more. +-/ +def CaptureSet.Chaining (Γ : Context n m k) (C1 C2 : CaptureSet n k) : Prop := + ∀c, ReachRoot Γ C1 drop c -> ∀m, ReachRoot Γ C2 m c -> False notation:50 Γ " ⊢ " C1 " >> " C2 => CaptureSet.Chaining Γ C1 C2 From 62d0d7f9b3aeb1d8cf550bf6b67f2ef5b3007797 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 20 Jan 2025 10:44:34 +0800 Subject: [PATCH 48/84] def: rearrange --- Capybara/StaticSemantics/CaptureRoot.lean | 84 +++++------------------ Capybara/StaticSemantics/Chaining.lean | 2 +- Capybara/StaticSemantics/ReachRoot.lean | 25 ------- Capybara/StaticSemantics/Separation.lean | 36 +++++----- 4 files changed, 35 insertions(+), 112 deletions(-) delete mode 100644 Capybara/StaticSemantics/ReachRoot.lean diff --git a/Capybara/StaticSemantics/CaptureRoot.lean b/Capybara/StaticSemantics/CaptureRoot.lean index 323d3b87..9096cd5f 100644 --- a/Capybara/StaticSemantics/CaptureRoot.lean +++ b/Capybara/StaticSemantics/CaptureRoot.lean @@ -1,77 +1,25 @@ import Capybara.Syntax -import Capybara.StaticSemantics.Subcapturing namespace Capybara /-! -A capture root is a set of qualified access to abstract capture variables. +`ReachRoot Γ C m c` means that the root `c` is reachable at access mode `m` from the capture set `C` under the context `Γ`. -/ -inductive CaptureRoot (k : Nat) where -| empty : CaptureRoot k -| union : CaptureRoot k -> CaptureRoot k -> CaptureRoot k -| singleton : Fin k -> Mode -> CaptureRoot k - -/-! -Instances of `CaptureRoot`: empty, union. --/ - -instance : EmptyCollection (CaptureRoot k) := ⟨CaptureRoot.empty⟩ -instance : Union (CaptureRoot k) := ⟨CaptureRoot.union⟩ - -/-! -The capture root of a capture set under a context. - -The relation `CaptureSet.Root C Γ D` defines how a capture set `C` maps to its root capture variables `D` -under the context `Γ`. The root captures represent the original abstract capture variables that are the -source of the captures in the set. This relation is defined inductively with the following cases: - -* Empty: An empty capture set maps to an empty root set -* Union: The root of a union of capture sets is the union of their roots -* Singleton: A singleton capture of a variable maps to the root of its type's capture set -* Parameter: A singleton capture of a parameter maps directly to that parameter with its mode -* Alias: A singleton capture of an alias maps to the root of its aliased capture set --/ -inductive CaptureSet.Root : CaptureSet n k -> Context n m k -> CaptureRoot k -> Prop where -| empty : CaptureSet.Root {} Context.empty {} -| union : - Root C1 Γ D1 -> - Root C2 Γ D2 -> - Root (C1 ∪ C2) Γ (D1 ∪ D2) -| singleton : - Context.Lookup Γ x (CType.capt C m0 S0) -> - CaptureSet.Root (C.qualified m) Γ D -> - CaptureSet.Root ({x@m:=x}) Γ D -| csingleton_param : - Context.LookupC Γ c (cparam k) -> - CaptureSet.Root ({c@m:=c}) Γ (CaptureRoot.singleton c m) -| csingleton_alias : - Context.LookupC Γ c (calias C) -> - CaptureSet.Root (C.qualified m) Γ D -> - CaptureSet.Root ({c@m:=c}) Γ D - -/-! -Membership of an access in a capture root. --/ -inductive CaptureRoot.HasElem : CaptureRoot k -> Fin k -> Mode -> Prop where +inductive ReachRoot : Context n m k -> CaptureSet n k -> Mode -> Fin k -> Prop where | union_l : - HasElem D1 c m -> - HasElem (D1 ∪ D2) c m + ReachRoot Γ C1 m c -> + ReachRoot Γ (C1 ∪ C2) m c | union_r : - HasElem D2 c m -> - HasElem (D1 ∪ D2) c m -| singleton : - HasElem (CaptureRoot.singleton c m) c m - -/-! -All capture roots are dropped by this capture set. --/ -inductive CaptureRoot.Dropped : CaptureRoot k -> CaptureSet n k -> Prop where -| empty : CaptureRoot.Dropped {} C -| union : - Dropped D1 C -> - Dropped D2 C -> - Dropped (D1 ∪ D2) C -| singleton : - Subcapturing Γ ({c@drop:=c}) C -> - Dropped (CaptureRoot.singleton c m) C + ReachRoot Γ C2 m c -> + ReachRoot Γ (C1 ∪ C2) m c +| var : + Context.Lookup Γ x (S^[m]C) -> + ReachRoot Γ ((C.qualified (Mode.M m)).qualified mu) mu' c -> + ReachRoot Γ ({x@mu:=x}) mu' c +| cvar_alias : + Context.LookupC Γ c (calias C) -> + ReachRoot Γ (C.qualified mu) mu' c' -> + ReachRoot Γ ({c@mu:=c}) mu' c' +| cvar : + ReachRoot Γ ({c@mu:=c}) mu c end Capybara diff --git a/Capybara/StaticSemantics/Chaining.lean b/Capybara/StaticSemantics/Chaining.lean index 6c7e2e33..ee53107d 100644 --- a/Capybara/StaticSemantics/Chaining.lean +++ b/Capybara/StaticSemantics/Chaining.lean @@ -1,4 +1,4 @@ -import Capybara.StaticSemantics.ReachRoot +import Capybara.StaticSemantics.CaptureRoot namespace Capybara /-! diff --git a/Capybara/StaticSemantics/ReachRoot.lean b/Capybara/StaticSemantics/ReachRoot.lean deleted file mode 100644 index 9096cd5f..00000000 --- a/Capybara/StaticSemantics/ReachRoot.lean +++ /dev/null @@ -1,25 +0,0 @@ -import Capybara.Syntax -namespace Capybara - -/-! -`ReachRoot Γ C m c` means that the root `c` is reachable at access mode `m` from the capture set `C` under the context `Γ`. --/ -inductive ReachRoot : Context n m k -> CaptureSet n k -> Mode -> Fin k -> Prop where -| union_l : - ReachRoot Γ C1 m c -> - ReachRoot Γ (C1 ∪ C2) m c -| union_r : - ReachRoot Γ C2 m c -> - ReachRoot Γ (C1 ∪ C2) m c -| var : - Context.Lookup Γ x (S^[m]C) -> - ReachRoot Γ ((C.qualified (Mode.M m)).qualified mu) mu' c -> - ReachRoot Γ ({x@mu:=x}) mu' c -| cvar_alias : - Context.LookupC Γ c (calias C) -> - ReachRoot Γ (C.qualified mu) mu' c' -> - ReachRoot Γ ({c@mu:=c}) mu' c' -| cvar : - ReachRoot Γ ({c@mu:=c}) mu c - -end Capybara diff --git a/Capybara/StaticSemantics/Separation.lean b/Capybara/StaticSemantics/Separation.lean index e381ab43..01988462 100644 --- a/Capybara/StaticSemantics/Separation.lean +++ b/Capybara/StaticSemantics/Separation.lean @@ -1,24 +1,24 @@ -import Capybara.StaticSemantics.CaptureRoot +import Capybara.StaticSemantics.ReachRoot namespace Capybara -/-! -Separation checking for capture roots. --/ -def CaptureRoot.Separation (Γ : Context n m k) (D1 D2 : CaptureRoot k) : Prop := - -- Two capture roots are separated if given any shared access m1 c and m2 c, - ∀m1 m2 c, HasElem D1 c m1 -> HasElem D2 c m2 -> - -- either both are read-only, or - ((m1 = ro ∧ m2 = ro) ∨ - -- c is an immutable capture variable - (Γ.LookupC c (cparam Kind.Imm))) +-- /-! +-- Separation checking for capture roots. +-- -/ +-- def CaptureRoot.Separation (Γ : Context n m k) (D1 D2 : CaptureRoot k) : Prop := +-- -- Two capture roots are separated if given any shared access m1 c and m2 c, +-- ∀m1 m2 c, HasElem D1 c m1 -> HasElem D2 c m2 -> +-- -- either both are read-only, or +-- ((m1 = ro ∧ m2 = ro) ∨ +-- -- c is an immutable capture variable +-- (Γ.LookupC c (cparam Kind.Imm))) -inductive CaptureSet.Separation : Context n m k -> CaptureSet n k -> CaptureSet n k -> Prop where -| mk : - CaptureSet.Root C1 Γ D1 -> - CaptureSet.Root C2 Γ D2 -> - CaptureRoot.Separation Γ D1 D2 -> - CaptureSet.Separation Γ C1 C2 +-- inductive CaptureSet.Separation : Context n m k -> CaptureSet n k -> CaptureSet n k -> Prop where +-- | mk : +-- CaptureSet.Root C1 Γ D1 -> +-- CaptureSet.Root C2 Γ D2 -> +-- CaptureRoot.Separation Γ D1 D2 -> +-- CaptureSet.Separation Γ C1 C2 -notation:50 Γ " ⊢ " C1 " ⋈ " C2 => CaptureSet.Separation Γ C1 C2 +-- notation:50 Γ " ⊢ " C1 " ⋈ " C2 => CaptureSet.Separation Γ C1 C2 end Capybara From ad446369c820330f109ee855294d2d7860c4317d Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 20 Jan 2025 11:03:30 +0800 Subject: [PATCH 49/84] def: separation checking --- Capybara/StaticSemantics/CaptureRoot.lean | 32 +++++++++++------ Capybara/StaticSemantics/Separation.lean | 44 +++++++++++++---------- Capybara/Syntax/Type/Core.lean | 10 ++++-- Capybara/Syntax/Type/Renaming.lean | 3 +- Capybara/Syntax/Type/Weakening.lean | 6 ++-- 5 files changed, 58 insertions(+), 37 deletions(-) diff --git a/Capybara/StaticSemantics/CaptureRoot.lean b/Capybara/StaticSemantics/CaptureRoot.lean index 9096cd5f..9e82e05e 100644 --- a/Capybara/StaticSemantics/CaptureRoot.lean +++ b/Capybara/StaticSemantics/CaptureRoot.lean @@ -1,25 +1,37 @@ import Capybara.Syntax namespace Capybara +structure CaptureRoot (k : Nat) : Type where + m : Mode + c : Fin k + /-! `ReachRoot Γ C m c` means that the root `c` is reachable at access mode `m` from the capture set `C` under the context `Γ`. -/ -inductive ReachRoot : Context n m k -> CaptureSet n k -> Mode -> Fin k -> Prop where +inductive ReachRoot : Context n m k -> CaptureSet n k -> CaptureRoot k -> Prop where | union_l : - ReachRoot Γ C1 m c -> - ReachRoot Γ (C1 ∪ C2) m c + ReachRoot Γ C1 ⟨m,c⟩ -> + ReachRoot Γ (C1 ∪ C2) ⟨m,c⟩ | union_r : - ReachRoot Γ C2 m c -> - ReachRoot Γ (C1 ∪ C2) m c + ReachRoot Γ C2 ⟨m,c⟩ -> + ReachRoot Γ (C1 ∪ C2) ⟨m,c⟩ | var : Context.Lookup Γ x (S^[m]C) -> - ReachRoot Γ ((C.qualified (Mode.M m)).qualified mu) mu' c -> - ReachRoot Γ ({x@mu:=x}) mu' c + ReachRoot Γ ((C.qualified (Mode.M m)).qualified mu) ⟨mu',c⟩ -> + ReachRoot Γ ({x@mu:=x}) ⟨mu',c⟩ | cvar_alias : Context.LookupC Γ c (calias C) -> - ReachRoot Γ (C.qualified mu) mu' c' -> - ReachRoot Γ ({c@mu:=c}) mu' c' + ReachRoot Γ (C.qualified mu) ⟨mu',c'⟩ -> + ReachRoot Γ ({c@mu:=c}) ⟨mu',c'⟩ | cvar : - ReachRoot Γ ({c@mu:=c}) mu c + Context.LookupC Γ c (cparam K) -> + ReachRoot Γ ({c@mu:=c}) ⟨mu,c⟩ + +inductive RORoot : Context n m k -> CaptureRoot k -> Prop where +| ro : + RORoot Γ ⟨ro,c⟩ +| imm : + Context.LookupC Γ c (cparam (CKind.Sep ⟨SepMode.Imm, D⟩)) -> + RORoot Γ ⟨Mode.M m,c⟩ end Capybara diff --git a/Capybara/StaticSemantics/Separation.lean b/Capybara/StaticSemantics/Separation.lean index 01988462..1dfc03ae 100644 --- a/Capybara/StaticSemantics/Separation.lean +++ b/Capybara/StaticSemantics/Separation.lean @@ -1,24 +1,32 @@ -import Capybara.StaticSemantics.ReachRoot +import Capybara.StaticSemantics.CaptureRoot namespace Capybara --- /-! --- Separation checking for capture roots. --- -/ --- def CaptureRoot.Separation (Γ : Context n m k) (D1 D2 : CaptureRoot k) : Prop := --- -- Two capture roots are separated if given any shared access m1 c and m2 c, --- ∀m1 m2 c, HasElem D1 c m1 -> HasElem D2 c m2 -> --- -- either both are read-only, or --- ((m1 = ro ∧ m2 = ro) ∨ --- -- c is an immutable capture variable --- (Γ.LookupC c (cparam Kind.Imm))) +/-! +Separation checking. +-/ --- inductive CaptureSet.Separation : Context n m k -> CaptureSet n k -> CaptureSet n k -> Prop where --- | mk : --- CaptureSet.Root C1 Γ D1 -> --- CaptureSet.Root C2 Γ D2 -> --- CaptureRoot.Separation Γ D1 D2 -> --- CaptureSet.Separation Γ C1 C2 +inductive RootSeparation : Context n m k -> CaptureRoot k -> CaptureRoot k -> Prop where +| symm : + RootSeparation Γ r1 r2 -> + RootSeparation Γ r2 r1 +| ro : + RORoot Γ r1 -> + RORoot Γ r2 -> + RootSeparation Γ r1 r2 +| rw : + RootSeparation Γ ⟨ε,c1⟩ r2 -> + RootSeparation Γ ⟨ro,c1⟩ r2 +| sep : + Context.LookupC Γ c (cparam (CKind.Sep ⟨s,D⟩)) -> + ReachRoot Γ D r2 -> + RootSeparation Γ ⟨ε,c⟩ r2 +| fresh : + Context.LookupC Γ c1 (cparam CKind.Fresh) -> + Context.LookupC Γ c2 (cparam CKind.Fresh) -> + (c1 ≠ c2) -> + RootSeparation Γ ⟨μ1,c1⟩ ⟨μ2,c2⟩ --- notation:50 Γ " ⊢ " C1 " ⋈ " C2 => CaptureSet.Separation Γ C1 C2 +def Separation (Γ : Context n m k) (C1 C2 : CaptureSet n k) : Prop := + ∀r1 r2, ReachRoot Γ C1 r1 -> ReachRoot Γ C2 r2 -> RootSeparation Γ r1 r2 end Capybara diff --git a/Capybara/Syntax/Type/Core.lean b/Capybara/Syntax/Type/Core.lean index dd526bc1..aad5b764 100644 --- a/Capybara/Syntax/Type/Core.lean +++ b/Capybara/Syntax/Type/Core.lean @@ -1,12 +1,16 @@ import Capybara.Syntax.CaptureSet.Core namespace Capybara +inductive SepMode : Type where +| Mut : SepMode +| Imm : SepMode + /-! Separation degree. -/ -inductive SepDegree : Nat -> Nat -> Type where -| Mut : CaptureSet n k -> SepDegree n k -| Imm : CaptureSet n k -> SepDegree n k +structure SepDegree (n k : Nat) : Type where + mode : SepMode + degree : CaptureSet n k mutual diff --git a/Capybara/Syntax/Type/Renaming.lean b/Capybara/Syntax/Type/Renaming.lean index 3ae3482b..030b71d1 100644 --- a/Capybara/Syntax/Type/Renaming.lean +++ b/Capybara/Syntax/Type/Renaming.lean @@ -6,8 +6,7 @@ def SepDegree.rename (ρ : Renaming n m k n' m' k') : SepDegree n' k' := match D with - | Imm C => Imm (C.rename ρ) - | Mut C => Mut (C.rename ρ) + | ⟨s, C⟩ => ⟨s, C.rename ρ⟩ mutual diff --git a/Capybara/Syntax/Type/Weakening.lean b/Capybara/Syntax/Type/Weakening.lean index 80a7ee02..9967f9cb 100644 --- a/Capybara/Syntax/Type/Weakening.lean +++ b/Capybara/Syntax/Type/Weakening.lean @@ -11,8 +11,7 @@ def CType.weaken : CType n m k -> CType (n+1) m k := def SType.weaken : SType n m k -> SType (n+1) m k := fun S => S.rename Renaming.weaken def SepDegree.weaken : SepDegree n k -> SepDegree (n+1) k -| SepDegree.Imm C => SepDegree.Imm (C.weaken) -| SepDegree.Mut C => SepDegree.Mut (C.weaken) +| ⟨sm, C⟩ => ⟨sm, C.weaken⟩ /-! Type weakening functions. @@ -34,7 +33,6 @@ def CType.cweaken : CType n m k -> CType n m (k+1) := def SType.cweaken : SType n m k -> SType n m (k+1) := fun S => S.rename Renaming.cweaken def SepDegree.cweaken : SepDegree n k -> SepDegree n (k+1) -| SepDegree.Imm C => SepDegree.Imm (C.cweaken) -| SepDegree.Mut C => SepDegree.Mut (C.cweaken) +| ⟨sm, C⟩ => ⟨sm, C.cweaken⟩ end Capybara From 0f9d3bd8ac084ff1318fcf750641f9ca1b6b4b92 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 20 Jan 2025 11:08:20 +0800 Subject: [PATCH 50/84] def: kinding --- Capybara/StaticSemantics/Kinding.lean | 45 +++++++-------------------- 1 file changed, 12 insertions(+), 33 deletions(-) diff --git a/Capybara/StaticSemantics/Kinding.lean b/Capybara/StaticSemantics/Kinding.lean index e3ad0f71..6217b266 100644 --- a/Capybara/StaticSemantics/Kinding.lean +++ b/Capybara/StaticSemantics/Kinding.lean @@ -1,39 +1,18 @@ import Capybara.Syntax import Capybara.StaticSemantics.CaptureRoot +import Capybara.StaticSemantics.Separation namespace Capybara -/-! -Kinding of capture roots. -- `empty` and `union` are structural rules -- `k_ro`: a readonly access is immutable -- `k_imm`: any access to an immutable capture set variable is immutable -- `k_mut`: any access can be counted as mutable -- `k_fresh`: access to a fresh capture set variable is fresh --/ -inductive CaptureRoot.Kinding : Context n m k -> CaptureRoot k -> Kind -> Prop where -| empty : CaptureRoot.Kinding Γ {} Kind.Imm -| union : - CaptureRoot.Kinding Γ D1 K -> - CaptureRoot.Kinding Γ D2 K -> - CaptureRoot.Kinding Γ (D1 ∪ D2) K -| k_ro : - CaptureRoot.Kinding Γ (CaptureRoot.singleton c ro) Kind.Imm -| k_imm : - Context.LookupC Γ c (cparam Kind.Imm) -> - CaptureRoot.Kinding Γ (CaptureRoot.singleton c m) Kind.Imm -| k_mut : - CaptureRoot.Kinding Γ (CaptureRoot.singleton c m) Kind.Mut -| k_fresh : - Context.LookupC Γ c (cparam Kind.Fresh) -> - CaptureRoot.Kinding Γ (CaptureRoot.singleton c m) Kind.Fresh - -/-! -Kinding of capture sets is defined by the kinding of its root capture variables. --/ -inductive CaptureSet.Kinding : Context n m k -> CaptureSet n k -> Kind -> Prop where -| mk : - CaptureSet.Root C Γ D -> - D.Kinding Γ K -> - CaptureSet.Kinding Γ C K +inductive CaptureSet.Kinding : Context n m k -> CaptureSet n k -> CKind n k -> Prop where +| fresh : + (∀c m, ReachRoot Γ C ⟨Mode.M m,c⟩ -> Context.LookupC Γ c (cparam CKind.Fresh)) -> + CaptureSet.Kinding Γ C CKind.Fresh +| sep_mut : + Separation Γ C D -> + CaptureSet.Kinding Γ C (CKind.Sep ⟨SepMode.Mut, D⟩) +| sep_imm : + Separation Γ C D -> + (∀r, ReachRoot Γ C r -> RORoot Γ r) -> + CaptureSet.Kinding Γ C (CKind.Sep ⟨SepMode.Imm, D⟩) end Capybara From 7fa6f22171a4f94f7dff7a1661b3d56cd98ede17 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 20 Jan 2025 11:11:01 +0800 Subject: [PATCH 51/84] def: make chaining up-to-date --- Capybara/StaticSemantics/Chaining.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Capybara/StaticSemantics/Chaining.lean b/Capybara/StaticSemantics/Chaining.lean index ee53107d..bcac19f1 100644 --- a/Capybara/StaticSemantics/Chaining.lean +++ b/Capybara/StaticSemantics/Chaining.lean @@ -7,7 +7,7 @@ namespace Capybara Specifically, anything that has been dropped from `C1` cannot be mentioned by `C2` any more. -/ def CaptureSet.Chaining (Γ : Context n m k) (C1 C2 : CaptureSet n k) : Prop := - ∀c, ReachRoot Γ C1 drop c -> ∀m, ReachRoot Γ C2 m c -> False + ∀c, ReachRoot Γ C1 ⟨drop,c⟩ -> ∀m, ReachRoot Γ C2 ⟨m,c⟩ -> False notation:50 Γ " ⊢ " C1 " >> " C2 => CaptureSet.Chaining Γ C1 C2 From 2ab6bdcd698ec1603c05e5b1088c57b01177715d Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 21 Jan 2025 09:02:31 +0800 Subject: [PATCH 52/84] def: typing wip --- Capybara/StaticSemantics/Kinding.lean | 8 ++++---- Capybara/StaticSemantics/Typing.lean | 22 +++++++++++++++------- 2 files changed, 19 insertions(+), 11 deletions(-) diff --git a/Capybara/StaticSemantics/Kinding.lean b/Capybara/StaticSemantics/Kinding.lean index 6217b266..77fdef9b 100644 --- a/Capybara/StaticSemantics/Kinding.lean +++ b/Capybara/StaticSemantics/Kinding.lean @@ -3,16 +3,16 @@ import Capybara.StaticSemantics.CaptureRoot import Capybara.StaticSemantics.Separation namespace Capybara -inductive CaptureSet.Kinding : Context n m k -> CaptureSet n k -> CKind n k -> Prop where +inductive Kinding : Context n m k -> CaptureSet n k -> CKind n k -> Prop where | fresh : (∀c m, ReachRoot Γ C ⟨Mode.M m,c⟩ -> Context.LookupC Γ c (cparam CKind.Fresh)) -> - CaptureSet.Kinding Γ C CKind.Fresh + Kinding Γ C CKind.Fresh | sep_mut : Separation Γ C D -> - CaptureSet.Kinding Γ C (CKind.Sep ⟨SepMode.Mut, D⟩) + Kinding Γ C (CKind.Sep ⟨SepMode.Mut, D⟩) | sep_imm : Separation Γ C D -> (∀r, ReachRoot Γ C r -> RORoot Γ r) -> - CaptureSet.Kinding Γ C (CKind.Sep ⟨SepMode.Imm, D⟩) + Kinding Γ C (CKind.Sep ⟨SepMode.Imm, D⟩) end Capybara diff --git a/Capybara/StaticSemantics/Typing.lean b/Capybara/StaticSemantics/Typing.lean index 5c203672..d9e5ed4a 100644 --- a/Capybara/StaticSemantics/Typing.lean +++ b/Capybara/StaticSemantics/Typing.lean @@ -5,32 +5,40 @@ import Capybara.StaticSemantics.Subtyping import Capybara.StaticSemantics.Kinding namespace Capybara +/-! +`RootDropped Γ C D` means that any capture root in `C` is dropped in `D`. +-/ +def RootDropped (Γ : Context n m k) (C D : CaptureSet n k) : Prop := + ∀ m c, ReachRoot Γ C ⟨m,c⟩ -> (Γ ⊢c {c@drop:=c} <: D) + +/-! +The typing relation. +-/ inductive Typed : CaptureSet n k -> Context n m k -> Term n m k -> EType n m k -> Prop where | var : Γ.Lookup x (CType.capt C m S) -> - LessPermissive m' m -> + Mutability.LessPermissive m' m -> -------------------------------- Typed ({x@Mode.M m':=x}) Γ (Term.var x) (EType.type (CType.capt ({x:=x}) m' S)) | pack : Typed C' Γ (Term.var x) (EType.type (T.copen c)) -> - CaptureSet.Root ({c:=c}) Γ R -> - CaptureRoot.Kinding Γ R Kind.Fresh -> - CaptureRoot.Dropped R C' -> + RootDropped Γ ({c:=c}) C' -> + Kinding Γ ({c:=c}) CKind.Fresh -> ----------------------------------------------------- Typed C' Γ (Term.pack c x) (EType.ex T) | sub : Typed C Γ t E -> (Γ ⊢c C <: C') -> (Γ ⊢e E <: E') -> - -------------------------------- + ----------------------------------- Typed C' Γ t E' | abs : Typed (C.weaken ∪ CaptureSet.span x) (Γ,x:T) t E -> - -------------------------------- + ------------------------------------------------------------ Typed {} Γ (Term.lam T t) (EType.type (((x:T)->E)^[ε]C)) | tabs : Typed C (Γ,X:tparam S) t E -> - --------------------------------- + ------------------------------------------------------------ Typed C Γ (Term.tlam S t) (EType.type (([X<:S]->E)^[ε]C)) end Capybara From 051633859ef6849168e5d8830f94170c95068118 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 21 Jan 2025 10:01:33 +0800 Subject: [PATCH 53/84] def: application rules --- Capybara/StaticSemantics/Chaining.lean | 5 ++- Capybara/StaticSemantics/Typing.lean | 43 +++++++++++++++++++++++--- Capybara/Syntax/Type/Opening.lean | 9 ++++++ 3 files changed, 52 insertions(+), 5 deletions(-) diff --git a/Capybara/StaticSemantics/Chaining.lean b/Capybara/StaticSemantics/Chaining.lean index bcac19f1..b574bdf3 100644 --- a/Capybara/StaticSemantics/Chaining.lean +++ b/Capybara/StaticSemantics/Chaining.lean @@ -6,9 +6,12 @@ namespace Capybara Specifically, anything that has been dropped from `C1` cannot be mentioned by `C2` any more. -/ -def CaptureSet.Chaining (Γ : Context n m k) (C1 C2 : CaptureSet n k) : Prop := +def Chaining (Γ : Context n m k) (C1 C2 : CaptureSet n k) : Prop := ∀c, ReachRoot Γ C1 ⟨drop,c⟩ -> ∀m, ReachRoot Γ C2 ⟨m,c⟩ -> False +def DroppedChaining (Γ : Context n m k) (C1 C2 : CaptureSet n k) : Prop := + ∀μ c, ReachRoot Γ C1 ⟨μ,c⟩ -> ∀m, ReachRoot Γ C2 ⟨m,c⟩ -> False + notation:50 Γ " ⊢ " C1 " >> " C2 => CaptureSet.Chaining Γ C1 C2 end Capybara diff --git a/Capybara/StaticSemantics/Typing.lean b/Capybara/StaticSemantics/Typing.lean index d9e5ed4a..8f68f381 100644 --- a/Capybara/StaticSemantics/Typing.lean +++ b/Capybara/StaticSemantics/Typing.lean @@ -26,19 +26,54 @@ inductive Typed : CaptureSet n k -> Context n m k -> Term n m k -> EType n m k - Kinding Γ ({c:=c}) CKind.Fresh -> ----------------------------------------------------- Typed C' Γ (Term.pack c x) (EType.ex T) -| sub : +| subc : Typed C Γ t E -> (Γ ⊢c C <: C') -> - (Γ ⊢e E <: E') -> ----------------------------------- - Typed C' Γ t E' + Typed C' Γ t E | abs : - Typed (C.weaken ∪ CaptureSet.span x) (Γ,x:T) t E -> + Typed (C.weaken ∪ CaptureSet.span 0) (Γ,x:T) t E -> ------------------------------------------------------------ Typed {} Γ (Term.lam T t) (EType.type (((x:T)->E)^[ε]C)) | tabs : Typed C (Γ,X:tparam S) t E -> ------------------------------------------------------------ Typed C Γ (Term.tlam S t) (EType.type (([X<:S]->E)^[ε]C)) +| cabs : + Typed C.cweaken (Γ,c:cparam (CKind.Sep D)) t E -> + ------------------------------------------------------------ + Typed C Γ (Term.clam D t) (EType.type (([c:D]->E)^[ε]C)) +| fabs : + Typed (C.cweaken.weaken ∪ CaptureSet.span 0) ((Γ,c:cparam CKind.Fresh),x:T) t E -> + ------------------------------------------------------------ + Typed C Γ (Term.flam T t) (EType.type (([c:Fresh](x:T)->E)^[ε]C)) +| app : + Typed C' Γ (Term.var x) (EType.type (((x:T)->E)^[ε]Cf)) -> + Typed C' Γ (Term.var y) (EType.type T0) -> + (Γ ⊢ T0 <: T) -> + Chaining Γ ({x:=x}) ({x:=y}) -> + Chaining Γ ({x:=y}) ({x:=x}) -> + ------------------------------------------------------------ + Typed C' Γ (Term.app x y) (E.open y) +| tapp : + Typed C' Γ (Term.var x) (EType.type (([X<:S]->E)^[ε]Cf)) -> + (Γ ⊢s (SType.tvar X) <: S) -> + ------------------------------------------------------------ + Typed C' Γ (Term.tapp x X) (E.topen X) +| capp : + Typed C' Γ (Term.var x) (EType.type (([c:D]->E)^[ε]Cf)) -> + Kinding Γ ({c:=c}) (CKind.Sep D) -> + ------------------------------------------------------------ + Typed C' Γ (Term.capp x c) (E.copen c) +| fapp : + Typed C' Γ (Term.var x) (EType.type (([c:Fresh](x:T)->E)^[ε]Cf)) -> + Typed C' Γ (Term.var y) (EType.type T0) -> + (Γ ⊢ T0 <: (T.copen c)) -> + RootDropped Γ ({c:=c}) C' -> + Kinding Γ ({c:=c}) CKind.Fresh -> + DroppedChaining Γ ({c:=c}) ({x:=x}) -> + ------------------------------------------------------------ + Typed C' Γ (Term.fapp x c y) ((E.copen c).open y) + end Capybara diff --git a/Capybara/Syntax/Type/Opening.lean b/Capybara/Syntax/Type/Opening.lean index 088b8070..77707ebe 100644 --- a/Capybara/Syntax/Type/Opening.lean +++ b/Capybara/Syntax/Type/Opening.lean @@ -4,4 +4,13 @@ namespace Capybara def CType.copen (T : CType n m (k+1)) (c : Fin k) : CType n m k := T.rename (Renaming.copen c) +def EType.open (T : EType (n+1) m k) (x : Fin n) : EType n m k := + T.rename (Renaming.open x) + +def EType.topen (T : EType n (m+1) k) (X : Fin m) : EType n m k := + T.rename (Renaming.topen X) + +def EType.copen (T : EType n m (k+1)) (c : Fin k) : EType n m k := + T.rename (Renaming.copen c) + end Capybara From 3038d91dd7fc9c91127e22adb21a40380ae9409e Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 21 Jan 2025 10:22:38 +0800 Subject: [PATCH 54/84] def: finish typing --- Capybara/StaticSemantics/Typing.lean | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/Capybara/StaticSemantics/Typing.lean b/Capybara/StaticSemantics/Typing.lean index 8f68f381..73461f03 100644 --- a/Capybara/StaticSemantics/Typing.lean +++ b/Capybara/StaticSemantics/Typing.lean @@ -74,6 +74,19 @@ inductive Typed : CaptureSet n k -> Context n m k -> Term n m k -> EType n m k - DroppedChaining Γ ({c:=c}) ({x:=x}) -> ------------------------------------------------------------ Typed C' Γ (Term.fapp x c y) ((E.copen c).open y) - +| letin : + Typed C1 Γ t (EType.type T) -> + Typed C2.weaken (Γ,x:T) u E0 -> + ((Γ,x:T) ⊢e E0 <: E.weaken) -> + Chaining Γ C1 C2 -> + ------------------------------------------------------------ + Typed (C1 ∪ C2) Γ (Term.letin t u) E +| unpack : + Typed C1 Γ t (EType.ex T) -> + Typed (C2.cweaken.weaken ∪ CaptureSet.span 0) ((Γ,c:cparam CKind.Fresh),x:T) u E0 -> + (((Γ,c:cparam CKind.Fresh),x:T) ⊢e E0 <: E.cweaken.weaken) -> + Chaining Γ C1 C2 -> + ------------------------------------------------------------ + Typed (C1 ∪ C2) Γ (Term.unpack t u) E end Capybara From 9ea81ebf3eeb2ddc7e71d01cff2c5326850e457e Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 21 Jan 2025 10:27:11 +0800 Subject: [PATCH 55/84] lib: cleanup In the end, not used --- Capybara/Lib/FiniteSet.lean | 56 ------------------------------------- 1 file changed, 56 deletions(-) delete mode 100644 Capybara/Lib/FiniteSet.lean diff --git a/Capybara/Lib/FiniteSet.lean b/Capybara/Lib/FiniteSet.lean deleted file mode 100644 index 06adec97..00000000 --- a/Capybara/Lib/FiniteSet.lean +++ /dev/null @@ -1,56 +0,0 @@ -namespace Capybara - -/-! -Inductively defined finite sets. -!-/ -inductive FiniteSet : Type -> Type where -| empty : FiniteSet A -| union : FiniteSet A -> FiniteSet A -> FiniteSet A -| singleton : A -> FiniteSet A - -/-! -Instances for finite sets: empty collection, union, singleton. -!-/ -@[simp] -instance : EmptyCollection (FiniteSet A) where - emptyCollection := FiniteSet.empty - -@[simp] -instance : Union (FiniteSet A) where - union := FiniteSet.union - -@[simp] -instance : Singleton A (FiniteSet A) where - singleton := FiniteSet.singleton - -/-! -Definition of the renaming operator. -!-/ -def FiniteSet.rename : FiniteSet A -> (A -> B) -> FiniteSet B -| FiniteSet.empty, _ => {} -| FiniteSet.union s1 s2, f => (s1.rename f) ∪ (s2.rename f) -| FiniteSet.singleton a, f => {f a} - -/-! -Membership. -!-/ -inductive FiniteSet.HasElem : FiniteSet A -> A -> Prop where -| singleton : FiniteSet.HasElem {a} a -| union_l : FiniteSet.HasElem s1 a -> FiniteSet.HasElem (s1 ∪ s2) a -| union_r : FiniteSet.HasElem s2 a -> FiniteSet.HasElem (s1 ∪ s2) a - -instance : Membership (FiniteSet A) A where - mem := fun a A => FiniteSet.HasElem A a - -/-! -Properties of finite sets. -!-/ -theorem FiniteSet.rename_empty : FiniteSet.rename {} f = {} := rfl - -theorem FiniteSet.rename_singleton : FiniteSet.rename {a} f = {f a} := rfl - -theorem FiniteSet.rename_union : - FiniteSet.rename (s1 ∪ s2) f = (s1.rename f) ∪ (s2.rename f) := - rfl - -end Capybara From bd5d5dc27a105e519d498219bd574795dac5727e Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 22 Jan 2025 10:53:57 +0800 Subject: [PATCH 56/84] lib: cleanup --- Capybara/Lib.lean | 1 - 1 file changed, 1 deletion(-) delete mode 100644 Capybara/Lib.lean diff --git a/Capybara/Lib.lean b/Capybara/Lib.lean deleted file mode 100644 index 922414e3..00000000 --- a/Capybara/Lib.lean +++ /dev/null @@ -1 +0,0 @@ -import Capybara.Lib.FiniteSet From 4a9e370b9eed123deae7c6db1320045c190185f4 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 22 Jan 2025 16:40:14 +0800 Subject: [PATCH 57/84] proof(rebind): init --- Capybara/Morphism/Core.lean | 90 ++++++++++++++++ Capybara/Morphism/Rebinding.lean | 30 ++++++ Capybara/StaticSemantics.lean | 1 + Capybara/Syntax/CaptureSet.lean | 1 + Capybara/Syntax/CaptureSet/Core.lean | 2 + Capybara/Syntax/CaptureSet/Properties.lean | 28 +++++ Capybara/Syntax/Context.lean | 49 +++++---- Capybara/Syntax/Type.lean | 1 + Capybara/Syntax/Type/Properties.lean | 117 +++++++++++++++++++++ 9 files changed, 297 insertions(+), 22 deletions(-) create mode 100644 Capybara/Morphism/Rebinding.lean create mode 100644 Capybara/Syntax/CaptureSet/Properties.lean create mode 100644 Capybara/Syntax/Type/Properties.lean diff --git a/Capybara/Morphism/Core.lean b/Capybara/Morphism/Core.lean index 2e6803f8..4157d66c 100644 --- a/Capybara/Morphism/Core.lean +++ b/Capybara/Morphism/Core.lean @@ -149,4 +149,94 @@ def Renaming.copen (X : Fin k) : Renaming n m (k+1) n m k := cvar := FinFun.open X } +def Renaming.id : Renaming n m k n m k := + { + var := FinFun.id + tvar := FinFun.id + cvar := FinFun.id + } + +def FinFun.comp (f : FinFun n n') (g : FinFun n' n'') : FinFun n n'' := + fun x => g (f x) + +def Renaming.comp (ρ : Renaming n m k n' m' k') (ρ' : Renaming n' m' k' n'' m'' k'') : Renaming n m k n'' m'' k'' := + { + var := ρ.var.comp ρ'.var + tvar := ρ.tvar.comp ρ'.tvar + cvar := ρ.cvar.comp ρ'.cvar + } + +/-! +Basic properties of renamings. +-/ +theorem Renaming.ext_var_zero {ρ : Renaming n m k n' m' k'} : ρ.ext.var 0 = 0 := by + simp [Renaming.ext] + rfl + +theorem Renaming.ext_var_succ {ρ : Renaming n m k n' m' k'} {x : Fin n} : ρ.ext.var (Fin.succ x) = Fin.succ (ρ.var x) := by + simp [Renaming.ext] + rfl + +theorem FinFun.id_comp_id {n : Nat} : FinFun.comp (n:=n) FinFun.id FinFun.id = FinFun.id := by rfl + +theorem Renaming.id_comp_id {n m k : Nat} : Renaming.comp (n:=n) (m:=m) (k:=k) Renaming.id Renaming.id = Renaming.id := by rfl + +theorem FinFun.id_ext {n : Nat} : FinFun.ext (n:=n) FinFun.id = FinFun.id := by + funext x0 + cases x0 using Fin.cases + case zero => simp [FinFun.id, FinFun.ext] + case succ x0 => simp [FinFun.id, FinFun.ext] + +theorem Renaming.id_ext {n m k : Nat} : Renaming.ext (n:=n) (m:=m) (k:=k) Renaming.id = Renaming.id := by simp [Renaming.ext, Renaming.id, FinFun.id_ext] + +theorem Renaming.id_text {n m k : Nat} : Renaming.text (n:=n) (m:=m) (k:=k) Renaming.id = Renaming.id := by simp [Renaming.text, Renaming.id, FinFun.id_ext] + +theorem Renaming.id_cext {n m k : Nat} : Renaming.cext (n:=n) (m:=m) (k:=k) Renaming.id = Renaming.id := by simp [Renaming.cext, Renaming.id, FinFun.id_ext] + +theorem FinFun.comp_ext {f : FinFun n n'} {g : FinFun n' n''} : (f.comp g).ext = f.ext.comp g.ext := by + funext x + cases x using Fin.cases + case zero => rfl + case succ x0 => simp [FinFun.comp, FinFun.ext] + +theorem Renaming.comp_ext {ρ : Renaming n m k n' m' k'} {ρ' : Renaming n' m' k' n'' m'' k''} : + (ρ.comp ρ').ext = ρ.ext.comp ρ'.ext := by + simp [Renaming.ext, Renaming.comp, FinFun.comp_ext] + +theorem Renaming.comp_text {ρ : Renaming n m k n' m' k'} {ρ' : Renaming n' m' k' n'' m'' k''} : + (ρ.comp ρ').text = ρ.text.comp ρ'.text := by + simp [Renaming.text, Renaming.comp, FinFun.comp_ext] + +theorem Renaming.comp_cext {ρ : Renaming n m k n' m' k'} {ρ' : Renaming n' m' k' n'' m'' k''} : + (ρ.comp ρ').cext = ρ.cext.comp ρ'.cext := by + simp [Renaming.cext, Renaming.comp, FinFun.comp_ext] + +theorem FinFun.comp_weaken {f : FinFun n n'} : + f.comp FinFun.weaken = FinFun.weaken.comp (f.ext) := by + funext x + simp [FinFun.comp, FinFun.weaken, FinFun.ext] + +theorem FinFun.comp_id {f : FinFun n n'} : f.comp FinFun.id = f := by + funext x + simp [FinFun.comp, FinFun.id] + +theorem FinFun.id_comp {f : FinFun n n'} : FinFun.id.comp f = f := by + funext x + simp [FinFun.comp, FinFun.id] + +theorem Renaming.comp_weaken {ρ : Renaming n m k n' m' k'} : + ρ.comp Renaming.weaken = Renaming.weaken.comp ρ.ext := by + simp [Renaming.weaken, Renaming.comp, Renaming.ext] + simp [FinFun.comp_weaken, FinFun.comp_id, FinFun.id_comp] + +theorem Renaming.comp_tweaken {ρ : Renaming n m k n' m' k'} : + ρ.comp Renaming.tweaken = Renaming.tweaken.comp ρ.text := by + simp [Renaming.tweaken, Renaming.comp, Renaming.text] + simp [FinFun.comp_weaken, FinFun.comp_id, FinFun.id_comp] + +theorem Renaming.comp_cweaken {ρ : Renaming n m k n' m' k'} : + ρ.comp Renaming.cweaken = Renaming.cweaken.comp ρ.cext := by + simp [Renaming.cweaken, Renaming.comp, Renaming.cext] + simp [FinFun.comp_weaken, FinFun.comp_id, FinFun.id_comp] + end Capybara diff --git a/Capybara/Morphism/Rebinding.lean b/Capybara/Morphism/Rebinding.lean new file mode 100644 index 00000000..2666d6a6 --- /dev/null +++ b/Capybara/Morphism/Rebinding.lean @@ -0,0 +1,30 @@ +import Capless.Tactics +import Capybara.Syntax +import Capybara.Morphism.Core +namespace Capybara + +structure Rebinding (Γ : Context n m k) (Δ : Context n' m' k') where + ρ : Renaming n m k n' m' k' + var : ∀ {x T}, Γ.Lookup x T -> Δ.Lookup (ρ.var x) (T.rename ρ) + tvar : ∀ {X S}, Γ.LookupT X S -> Δ.LookupT (ρ.tvar X) (S.rename ρ) + cvar : ∀ {c K}, Γ.LookupC c K -> Δ.LookupC (ρ.cvar c) (K.rename ρ) + +def Rebinding.ext (θ : Rebinding Γ Δ) : Rebinding (Γ,x:T) (Δ,x:T.rename θ.ρ) := by + constructor + case ρ => exact θ.ρ.ext + case var => + intro x T hb + cases hb with + | here => + simp [Renaming.ext_var_zero] + simp [<-CType.rename_weaken] + constructor + | there h => + simp [Renaming.ext_var_succ] + simp [<-CType.rename_weaken] + constructor + apply θ.var; easy + case tvar => sorry + case cvar => sorry + +end Capybara diff --git a/Capybara/StaticSemantics.lean b/Capybara/StaticSemantics.lean index f810b8a2..b7e1f581 100644 --- a/Capybara/StaticSemantics.lean +++ b/Capybara/StaticSemantics.lean @@ -1,2 +1,3 @@ import Capybara.StaticSemantics.Subcapturing import Capybara.StaticSemantics.Subtyping +import Capybara.StaticSemantics.Typing diff --git a/Capybara/Syntax/CaptureSet.lean b/Capybara/Syntax/CaptureSet.lean index d6c208f1..8dedb7ca 100644 --- a/Capybara/Syntax/CaptureSet.lean +++ b/Capybara/Syntax/CaptureSet.lean @@ -1 +1,2 @@ import Capybara.Syntax.CaptureSet.Core +import Capybara.Syntax.CaptureSet.Properties diff --git a/Capybara/Syntax/CaptureSet/Core.lean b/Capybara/Syntax/CaptureSet/Core.lean index 1ff8fad5..0a300d3f 100644 --- a/Capybara/Syntax/CaptureSet/Core.lean +++ b/Capybara/Syntax/CaptureSet/Core.lean @@ -14,9 +14,11 @@ inductive CaptureSet : Nat -> Nat -> Type where /-! Instance definitions for capture sets. -/ +@[simp] instance : EmptyCollection (CaptureSet n k) where emptyCollection := CaptureSet.empty +@[simp] instance : Union (CaptureSet n k) where union := CaptureSet.union diff --git a/Capybara/Syntax/CaptureSet/Properties.lean b/Capybara/Syntax/CaptureSet/Properties.lean new file mode 100644 index 00000000..d2236620 --- /dev/null +++ b/Capybara/Syntax/CaptureSet/Properties.lean @@ -0,0 +1,28 @@ +import Capybara.Syntax.CaptureSet.Core +namespace Capybara + +/-! +# Properties of capture sets + +## Renaming identity +We can show that renaming by the identity renaming yields the same capture set. +-/ +@[simp] +theorem CaptureSet.rename_id {C : CaptureSet n k} : C.rename (Renaming.id (m:=m)) = C := by + induction C <;> simp [CaptureSet.rename] + case union ih1 ih2 => simp [ih1, ih2] + case singleton => simp [Renaming.id, FinFun.id] + case csingleton => simp [Renaming.id, FinFun.id] + +/-! +## Composition of renamings +In the following, we show that renaming composes. +-/ +theorem CaptureSet.rename_comp {C : CaptureSet n k} : + (C.rename ρ).rename ρ' = C.rename (ρ.comp ρ') := by + induction C <;> simp [CaptureSet.rename] + case union ih1 ih2 => simp [ih1, ih2] + case singleton => simp [Renaming.comp, FinFun.comp] + case csingleton => simp [Renaming.comp, FinFun.comp] + +end Capybara diff --git a/Capybara/Syntax/Context.lean b/Capybara/Syntax/Context.lean index 4e586058..792bf0d1 100644 --- a/Capybara/Syntax/Context.lean +++ b/Capybara/Syntax/Context.lean @@ -20,7 +20,6 @@ inductive TBinding : Nat -> Nat -> Nat -> Type where | param : SType n m k -> TBinding n m k | alias : SType n m k -> TBinding n m k - inductive CBinding : Nat -> Nat -> Type where | param : CKind n k -> CBinding n k | alias : CaptureSet n k -> CBinding n k @@ -30,30 +29,36 @@ notation:max "talias" S => TBinding.alias S notation:max "cparam" k => CBinding.param k notation:max "calias" C => CBinding.alias C +/-! +Renaming functions for type and capture set binding. +-/ +def CKind.rename : CKind n k -> Renaming n m k n' m' k' -> CKind n' k' +| CKind.Sep D, ρ => CKind.Sep (D.rename ρ) +| CKind.Fresh, _ => CKind.Fresh +def TBinding.rename : TBinding n m k -> Renaming n m k n' m' k' -> TBinding n' m' k' +| TBinding.param T, ρ => TBinding.param (T.rename ρ) +| TBinding.alias T, ρ => TBinding.alias (T.rename ρ) +def CBinding.rename : CBinding n k -> Renaming n m k n' m' k' -> CBinding n' k' +| CBinding.param k, ρ => CBinding.param (k.rename ρ) +| CBinding.alias C, ρ => CBinding.alias (C.rename ρ) + /-! Weakening functions for type and capture set binding. -/ -def TBinding.weaken : TBinding n m k -> TBinding (n+1) m k -| TBinding.param T => TBinding.param (T.weaken) -| TBinding.alias T => TBinding.alias (T.weaken) -def CKind.weaken : CKind n k -> CKind (n+1) k -| CKind.Sep D => CKind.Sep (D.weaken) -| CKind.Fresh => CKind.Fresh -def CBinding.weaken : CBinding n k -> CBinding (n+1) k -| CBinding.param k => CBinding.param (k.weaken) -| CBinding.alias C => CBinding.alias (C.weaken) -def TBinding.tweaken : TBinding n m k -> TBinding n (m+1) k -| TBinding.param T => TBinding.param (T.tweaken) -| TBinding.alias T => TBinding.alias (T.tweaken) -def TBinding.cweaken : TBinding n m k -> TBinding n m (k+1) -| TBinding.param T => TBinding.param (T.cweaken) -| TBinding.alias T => TBinding.alias (T.cweaken) -def CKind.cweaken : CKind n k -> CKind n (k+1) -| CKind.Sep D => CKind.Sep (D.cweaken) -| CKind.Fresh => CKind.Fresh -def CBinding.cweaken : CBinding n k -> CBinding n (k+1) -| CBinding.param k => CBinding.param (k.cweaken) -| CBinding.alias C => CBinding.alias (C.cweaken) +def TBinding.weaken (B : TBinding n m k) : TBinding (n+1) m k := + B.rename (Renaming.weaken) +def CKind.weaken (K : CKind n k) : CKind (n+1) k := + K.rename (Renaming.weaken (m:=0)) +def CBinding.weaken (B : CBinding n k) : CBinding (n+1) k := + B.rename (Renaming.weaken (m:=0)) +def TBinding.tweaken (B : TBinding n m k) : TBinding n (m+1) k := + B.rename (Renaming.tweaken) +def TBinding.cweaken (B : TBinding n m k) : TBinding n m (k+1) := + B.rename (Renaming.cweaken) +def CKind.cweaken (K : CKind n k) : CKind n (k+1) := + K.rename (Renaming.cweaken (m:=0)) +def CBinding.cweaken (B : CBinding n k) : CBinding n (k+1) := + B.rename (Renaming.cweaken (m:=0)) /-! An indexed context. A `Context n m k` contains `n` term variables, diff --git a/Capybara/Syntax/Type.lean b/Capybara/Syntax/Type.lean index 5718ef89..3383628f 100644 --- a/Capybara/Syntax/Type.lean +++ b/Capybara/Syntax/Type.lean @@ -2,3 +2,4 @@ import Capybara.Syntax.Type.Core import Capybara.Syntax.Type.Renaming import Capybara.Syntax.Type.Weakening import Capybara.Syntax.Type.Opening +import Capybara.Syntax.Type.Properties diff --git a/Capybara/Syntax/Type/Properties.lean b/Capybara/Syntax/Type/Properties.lean new file mode 100644 index 00000000..3b5558d7 --- /dev/null +++ b/Capybara/Syntax/Type/Properties.lean @@ -0,0 +1,117 @@ +import Capybara.Syntax.CaptureSet +import Capybara.Syntax.Type.Renaming +import Capybara.Syntax.Type.Weakening +namespace Capybara + + +/-! +# Basic properties of type renamings + +## Renaming identity +First, we show that renaming by the identity renaming yields the separation degree. +-/ +theorem SepDegree.rename_id {D : SepDegree n k} : D.rename (Renaming.id (m:=m)) = D := by + cases D; simp [SepDegree.rename] + +/-! +Then, we show that renaming by the identity renaming yields the type. +-/ +mutual + +theorem EType.rename_id {E : EType n m k} : E.rename Renaming.id = E := + match E with + | .ex T => by + simp [EType.rename] + simp [Renaming.id_cext] + simp [CType.rename_id] + | .type T => by + simp [EType.rename] + simp [CType.rename_id] + +theorem CType.rename_id {C : CType n m k} : C.rename Renaming.id = C := + match C with + | .capt C' m S => by + simp [CType.rename] + simp [SType.rename_id] + +theorem SType.rename_id {S : SType n m k} : S.rename Renaming.id = S := + match S with + | .top => rfl + | .tvar i => by + simp [SType.rename, Renaming.id] + rfl + | .tarrow S' T => by + simp [SType.rename] + simp [Renaming.id_text] + simp [SType.rename_id, EType.rename_id] + | .arrow C T => by + simp [SType.rename] + simp [Renaming.id_ext] + simp [CType.rename_id, EType.rename_id] + | .carrow D T => by + simp [SType.rename] + simp [Renaming.id_cext] + simp [EType.rename_id, SepDegree.rename_id] + | .farrow C T => by + simp [SType.rename] + simp [Renaming.id_cext, Renaming.id_ext] + simp [CType.rename_id, EType.rename_id] + +end + +/-! +## Renaming composition +-/ +theorem SepDegree.rename_comp {D : SepDegree n k} : + (D.rename ρ).rename ρ' = D.rename (ρ.comp ρ') := by + cases D; simp [SepDegree.rename, CaptureSet.rename_comp] + +mutual + +theorem EType.rename_comp {E : EType n m k} : + (E.rename ρ).rename ρ' = E.rename (ρ.comp ρ') := + match E with + | .type T => by + simp [EType.rename] + simp [CType.rename_comp] + | .ex T => by + simp [EType.rename] + simp [CType.rename_comp, Renaming.comp_cext] + +theorem CType.rename_comp {C : CType n m k} : + (C.rename ρ).rename ρ' = C.rename (ρ.comp ρ') := + match C with + | .capt m' C' S => by + simp [CType.rename, SType.rename_comp] + simp [CaptureSet.rename_comp] + +theorem SType.rename_comp {S : SType n m k} : + (S.rename ρ).rename ρ' = S.rename (ρ.comp ρ') := + match S with + | .top => by + simp [SType.rename] + | .tvar i => by + simp [SType.rename, Renaming.comp, FinFun.comp] + | .tarrow S' T => by + simp [SType.rename] + simp [SType.rename_comp, EType.rename_comp, Renaming.comp_text] + | .arrow C T => by + simp [SType.rename] + simp [CType.rename_comp, EType.rename_comp, Renaming.comp_ext] + | .carrow D T => by + simp [SType.rename] + simp [EType.rename_comp, SepDegree.rename_comp, Renaming.comp_cext] + | .farrow C T => by + simp [SType.rename] + simp [CType.rename_comp, EType.rename_comp, Renaming.comp_cext, Renaming.comp_ext] + +end + +/-! +## Corollaries of renaming composition +-/ +theorem CType.rename_weaken {T : CType n m k} : + (T.rename ρ).weaken = T.weaken.rename ρ.ext := by + simp [CType.weaken, CType.rename_comp, Renaming.comp_weaken] + +end Capybara From f9aa1283460647cb5567ffeb198e3b52ed0f3154 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 22 Jan 2025 17:03:59 +0800 Subject: [PATCH 58/84] proof(rebind): wip --- Capybara/Morphism/Rebinding.lean | 14 ++- Capybara/Syntax/CaptureSet/Properties.lean | 6 + Capybara/Syntax/Context.lean | 125 +-------------------- Capybara/Syntax/Context/Core.lean | 123 ++++++++++++++++++++ Capybara/Syntax/Context/Properties.lean | 31 +++++ Capybara/Syntax/Type/Properties.lean | 4 + 6 files changed, 178 insertions(+), 125 deletions(-) create mode 100644 Capybara/Syntax/Context/Core.lean create mode 100644 Capybara/Syntax/Context/Properties.lean diff --git a/Capybara/Morphism/Rebinding.lean b/Capybara/Morphism/Rebinding.lean index 2666d6a6..1e287016 100644 --- a/Capybara/Morphism/Rebinding.lean +++ b/Capybara/Morphism/Rebinding.lean @@ -24,7 +24,17 @@ def Rebinding.ext (θ : Rebinding Γ Δ) : Rebinding (Γ,x:T) (Δ,x:T.rename θ. simp [<-CType.rename_weaken] constructor apply θ.var; easy - case tvar => sorry - case cvar => sorry + case tvar => + intro X S hb + cases hb + case there hb => + simp [<-TBinding.rename_weaken] + constructor + apply θ.tvar; easy + case cvar => + intro c B hb + cases hb + case there hb => + sorry end Capybara diff --git a/Capybara/Syntax/CaptureSet/Properties.lean b/Capybara/Syntax/CaptureSet/Properties.lean index d2236620..f96c63ac 100644 --- a/Capybara/Syntax/CaptureSet/Properties.lean +++ b/Capybara/Syntax/CaptureSet/Properties.lean @@ -25,4 +25,10 @@ theorem CaptureSet.rename_comp {C : CaptureSet n k} : case singleton => simp [Renaming.comp, FinFun.comp] case csingleton => simp [Renaming.comp, FinFun.comp] +theorem CaptureSet.rename_weaken {C : CaptureSet n k} : + (C.rename ρ).weaken = C.weaken.rename ρ.ext := by + simp [CaptureSet.weaken] + sorry + + end Capybara diff --git a/Capybara/Syntax/Context.lean b/Capybara/Syntax/Context.lean index 792bf0d1..085eccf9 100644 --- a/Capybara/Syntax/Context.lean +++ b/Capybara/Syntax/Context.lean @@ -1,123 +1,2 @@ -import Mathlib.Data.Fin.Basic -import Capybara.Syntax.Type -namespace Capybara - -/-! -Kind of a capture set parameter. --/ -inductive CKind : Nat -> Nat -> Type where -| Sep : SepDegree n k -> CKind n k -| Fresh : CKind n k - -/-! -Type binding and capture set binding. - -Type binding can be either a type parameter (abstract) or -a concrete type alias. Similarly, capture set binding can be -a capture set parameter (abstract) or a concrete capture set alias. --/ -inductive TBinding : Nat -> Nat -> Nat -> Type where -| param : SType n m k -> TBinding n m k -| alias : SType n m k -> TBinding n m k - -inductive CBinding : Nat -> Nat -> Type where -| param : CKind n k -> CBinding n k -| alias : CaptureSet n k -> CBinding n k - -notation:max "tparam" S => TBinding.param S -notation:max "talias" S => TBinding.alias S -notation:max "cparam" k => CBinding.param k -notation:max "calias" C => CBinding.alias C - -/-! -Renaming functions for type and capture set binding. --/ -def CKind.rename : CKind n k -> Renaming n m k n' m' k' -> CKind n' k' -| CKind.Sep D, ρ => CKind.Sep (D.rename ρ) -| CKind.Fresh, _ => CKind.Fresh -def TBinding.rename : TBinding n m k -> Renaming n m k n' m' k' -> TBinding n' m' k' -| TBinding.param T, ρ => TBinding.param (T.rename ρ) -| TBinding.alias T, ρ => TBinding.alias (T.rename ρ) -def CBinding.rename : CBinding n k -> Renaming n m k n' m' k' -> CBinding n' k' -| CBinding.param k, ρ => CBinding.param (k.rename ρ) -| CBinding.alias C, ρ => CBinding.alias (C.rename ρ) - -/-! -Weakening functions for type and capture set binding. --/ -def TBinding.weaken (B : TBinding n m k) : TBinding (n+1) m k := - B.rename (Renaming.weaken) -def CKind.weaken (K : CKind n k) : CKind (n+1) k := - K.rename (Renaming.weaken (m:=0)) -def CBinding.weaken (B : CBinding n k) : CBinding (n+1) k := - B.rename (Renaming.weaken (m:=0)) -def TBinding.tweaken (B : TBinding n m k) : TBinding n (m+1) k := - B.rename (Renaming.tweaken) -def TBinding.cweaken (B : TBinding n m k) : TBinding n m (k+1) := - B.rename (Renaming.cweaken) -def CKind.cweaken (K : CKind n k) : CKind n (k+1) := - K.rename (Renaming.cweaken (m:=0)) -def CBinding.cweaken (B : CBinding n k) : CBinding n (k+1) := - B.rename (Renaming.cweaken (m:=0)) - -/-! -An indexed context. A `Context n m k` contains `n` term variables, -`m` type variables, and `k` capture set variables. -!-/ -inductive Context : Nat -> Nat -> Nat -> Type where -| empty : Context 0 0 0 -| cons : Context n m k -> CType n m k -> Context (n+1) m k -| tcons : Context n m k -> TBinding n m k -> Context n (m+1) k -| ccons : Context n m k -> CBinding n k -> Context n m (k+1) - -instance : EmptyCollection (Context 0 0 0) := - ⟨Context.empty⟩ - -theorem Context.empty_def : - ({} : Context 0 0 0) = Context.empty := rfl - -notation:20 Γ ",x:" T => Context.cons Γ T -notation:20 Γ ",X:" T => Context.tcons Γ T -notation:20 Γ ",c:" C => Context.ccons Γ C - -/-! -Context lookup. - -`Context.Lookup`, `Context.LookupT`, and `Context.LookupC` look up the three dimensions of a context, -respectively. --/ -inductive Context.Lookup : Context n m k -> Fin n -> CType n m k -> Prop where -| here : Context.Lookup (Γ,x:T) 0 T.weaken -| there : - Context.Lookup Γ x T -> - Context.Lookup (Γ,x:T) (x.succ) T.weaken -| tthere : - Context.Lookup Γ x T -> - Context.Lookup (Γ,X:B) x (T.tweaken) -| cthere : - Context.Lookup Γ x T -> - Context.Lookup (Γ,c:B) x (T.cweaken) -inductive Context.LookupT : Context n m k -> Fin m -> TBinding n m k -> Prop where -| here : Context.LookupT (Γ,X:T) 0 T.tweaken -| there : - Context.LookupT Γ X S -> - Context.LookupT (Γ,x:T) X S.weaken -| tthere : - Context.LookupT Γ X T -> - Context.LookupT (Γ,X:B) (X.succ) T.tweaken -| cthere : - Context.LookupT Γ X T -> - Context.LookupT (Γ,c:B) X T.cweaken -inductive Context.LookupC : Context n m k -> Fin k -> CBinding n k -> Prop where -| here : Context.LookupC (Γ,c:C) 0 C.cweaken -| there : - Context.LookupC Γ c C -> - Context.LookupC (Γ,x:T) c C.weaken -| tthere : - Context.LookupC Γ c C -> - Context.LookupC (Γ,X:B) c C -| cthere : - Context.LookupC Γ c C -> - Context.LookupC (Γ,c:B) (c.succ) C.cweaken - -end Capybara +import Capybara.Syntax.Context.Core +import Capybara.Syntax.Context.Properties diff --git a/Capybara/Syntax/Context/Core.lean b/Capybara/Syntax/Context/Core.lean new file mode 100644 index 00000000..fd0205f9 --- /dev/null +++ b/Capybara/Syntax/Context/Core.lean @@ -0,0 +1,123 @@ +import Mathlib.Data.Fin.Basic +import Capybara.Syntax.Type +namespace Capybara + +/-! +Kind of a capture set parameter. +-/ +inductive CKind : Nat -> Nat -> Type where +| Sep : SepDegree n k -> CKind n k +| Fresh : CKind n k + +/-! +Type binding and capture set binding. + +Type binding can be either a type parameter (abstract) or +a concrete type alias. Similarly, capture set binding can be +a capture set parameter (abstract) or a concrete capture set alias. +-/ +inductive TBinding : Nat -> Nat -> Nat -> Type where +| param : SType n m k -> TBinding n m k +| typealias : SType n m k -> TBinding n m k + +inductive CBinding : Nat -> Nat -> Type where +| param : CKind n k -> CBinding n k +| capturealias : CaptureSet n k -> CBinding n k + +notation:max "tparam" S => TBinding.param S +notation:max "talias" S => TBinding.typealias S +notation:max "cparam" k => CBinding.param k +notation:max "calias" C => CBinding.capturealias C + +/-! +Renaming functions for type and capture set binding. +-/ +def CKind.rename : CKind n k -> Renaming n m k n' m' k' -> CKind n' k' +| CKind.Sep D, ρ => CKind.Sep (D.rename ρ) +| CKind.Fresh, _ => CKind.Fresh +def TBinding.rename : TBinding n m k -> Renaming n m k n' m' k' -> TBinding n' m' k' +| TBinding.param T, ρ => TBinding.param (T.rename ρ) +| TBinding.typealias T, ρ => TBinding.typealias (T.rename ρ) +def CBinding.rename : CBinding n k -> Renaming n m k n' m' k' -> CBinding n' k' +| CBinding.param k, ρ => CBinding.param (k.rename ρ) +| CBinding.capturealias C, ρ => CBinding.capturealias (C.rename ρ) + +/-! +Weakening functions for type and capture set binding. +-/ +def TBinding.weaken (B : TBinding n m k) : TBinding (n+1) m k := + B.rename (Renaming.weaken) +def CKind.weaken (K : CKind n k) : CKind (n+1) k := + K.rename (Renaming.weaken (m:=0)) +def CBinding.weaken (B : CBinding n k) : CBinding (n+1) k := + B.rename (Renaming.weaken (m:=0)) +def TBinding.tweaken (B : TBinding n m k) : TBinding n (m+1) k := + B.rename (Renaming.tweaken) +def TBinding.cweaken (B : TBinding n m k) : TBinding n m (k+1) := + B.rename (Renaming.cweaken) +def CKind.cweaken (K : CKind n k) : CKind n (k+1) := + K.rename (Renaming.cweaken (m:=0)) +def CBinding.cweaken (B : CBinding n k) : CBinding n (k+1) := + B.rename (Renaming.cweaken (m:=0)) + +/-! +An indexed context. A `Context n m k` contains `n` term variables, +`m` type variables, and `k` capture set variables. +!-/ +inductive Context : Nat -> Nat -> Nat -> Type where +| empty : Context 0 0 0 +| cons : Context n m k -> CType n m k -> Context (n+1) m k +| tcons : Context n m k -> TBinding n m k -> Context n (m+1) k +| ccons : Context n m k -> CBinding n k -> Context n m (k+1) + +instance : EmptyCollection (Context 0 0 0) := + ⟨Context.empty⟩ + +theorem Context.empty_def : + ({} : Context 0 0 0) = Context.empty := rfl + +notation:20 Γ ",x:" T => Context.cons Γ T +notation:20 Γ ",X:" T => Context.tcons Γ T +notation:20 Γ ",c:" C => Context.ccons Γ C + +/-! +Context lookup. + +`Context.Lookup`, `Context.LookupT`, and `Context.LookupC` look up the three dimensions of a context, +respectively. +-/ +inductive Context.Lookup : Context n m k -> Fin n -> CType n m k -> Prop where +| here : Context.Lookup (Γ,x:T) 0 T.weaken +| there : + Context.Lookup Γ x T -> + Context.Lookup (Γ,x:T) (x.succ) T.weaken +| tthere : + Context.Lookup Γ x T -> + Context.Lookup (Γ,X:B) x (T.tweaken) +| cthere : + Context.Lookup Γ x T -> + Context.Lookup (Γ,c:B) x (T.cweaken) +inductive Context.LookupT : Context n m k -> Fin m -> TBinding n m k -> Prop where +| here : Context.LookupT (Γ,X:T) 0 T.tweaken +| there : + Context.LookupT Γ X S -> + Context.LookupT (Γ,x:T) X S.weaken +| tthere : + Context.LookupT Γ X T -> + Context.LookupT (Γ,X:B) (X.succ) T.tweaken +| cthere : + Context.LookupT Γ X T -> + Context.LookupT (Γ,c:B) X T.cweaken +inductive Context.LookupC : Context n m k -> Fin k -> CBinding n k -> Prop where +| here : Context.LookupC (Γ,c:C) 0 C.cweaken +| there : + Context.LookupC Γ c C -> + Context.LookupC (Γ,x:T) c C.weaken +| tthere : + Context.LookupC Γ c C -> + Context.LookupC (Γ,X:B) c C +| cthere : + Context.LookupC Γ c C -> + Context.LookupC (Γ,c:B) (c.succ) C.cweaken + +end Capybara diff --git a/Capybara/Syntax/Context/Properties.lean b/Capybara/Syntax/Context/Properties.lean new file mode 100644 index 00000000..721abd4e --- /dev/null +++ b/Capybara/Syntax/Context/Properties.lean @@ -0,0 +1,31 @@ +import Capybara.Syntax.Context.Core +namespace Capybara + +theorem TBinding.rename_id {B : TBinding n m k} : B.rename Renaming.id = B := by + cases B + case param => simp [TBinding.rename, SType.rename_id] + case typealias => simp [TBinding.rename, SType.rename_id] + +theorem TBinding.rename_weaken {B : TBinding n m k} : + (B.rename ρ).weaken = B.weaken.rename ρ.ext := by + cases B + case param => + simp [TBinding.weaken, TBinding.rename] + apply SType.rename_weaken + case typealias => + simp [TBinding.weaken, TBinding.rename] + apply SType.rename_weaken + +theorem CBinding.rename_weaken {B : CBinding n k} : + (B.rename ρ).weaken = B.weaken.rename ρ.ext := by + cases B + case param K => + simp [CBinding.weaken, CBinding.rename] + cases K + case Sep D => + cases D <;> simp [CKind.rename] <;> simp [SepDegree.rename] + apply CaptureSet.rename_weaken + case Fresh => + simp [CKind.rename] + +end Capybara diff --git a/Capybara/Syntax/Type/Properties.lean b/Capybara/Syntax/Type/Properties.lean index 3b5558d7..59d7280f 100644 --- a/Capybara/Syntax/Type/Properties.lean +++ b/Capybara/Syntax/Type/Properties.lean @@ -114,4 +114,8 @@ theorem CType.rename_weaken {T : CType n m k} : (T.rename ρ).weaken = T.weaken.rename ρ.ext := by simp [CType.weaken, CType.rename_comp, Renaming.comp_weaken] +theorem SType.rename_weaken {S : SType n m k} : + (S.rename ρ).weaken = S.weaken.rename ρ.ext := by + simp [SType.weaken, SType.rename_comp, Renaming.comp_weaken] + end Capybara From 2c64c87c40bd016329d13259b1e45d8ac7686f47 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 23 Jan 2025 14:21:21 +0800 Subject: [PATCH 59/84] proof(rebind): wip --- Capybara/Morphism/Core.lean | 29 ++++++++++++++++++++++ Capybara/Syntax/CaptureSet/Core.lean | 6 ++--- Capybara/Syntax/CaptureSet/Properties.lean | 23 ++++++++++------- Capybara/Syntax/Context/Core.lean | 12 ++++----- Capybara/Syntax/Context/Properties.lean | 14 ++++++++--- Capybara/Syntax/Term.lean | 4 +-- Capybara/Syntax/Type/Properties.lean | 6 ++--- Capybara/Syntax/Type/Renaming.lean | 6 ++--- 8 files changed, 71 insertions(+), 29 deletions(-) diff --git a/Capybara/Morphism/Core.lean b/Capybara/Morphism/Core.lean index 4157d66c..03c9245c 100644 --- a/Capybara/Morphism/Core.lean +++ b/Capybara/Morphism/Core.lean @@ -12,6 +12,7 @@ This module defines morphisms between contexts in the Capybara type system. - `n` term variables to `n'` term variables - `m` type variables to `m'` type variables - `k` capture set variables to `k'` capture set variables +- `CaptureRenaming n k n' k'`: A renaming morphism that maps between capture sets with only two dimensions: terms and captures. ## Implementation Notes @@ -65,6 +66,19 @@ structure Renaming (n m k n' m' k' : Nat) where tvar : FinFun m m' cvar : FinFun k k' +/-! +Capture renaming function. +-/ +structure CaptureRenaming (n k n' k' : Nat) where + var : FinFun n n' + cvar : FinFun k k' + +def Renaming.asCapt (ρ : Renaming n m k n' m' k') : CaptureRenaming n k n' k' := + { + var := ρ.var + cvar := ρ.cvar + } + /-! Extend a renaming function by one on the term variable dimension. -/ @@ -166,6 +180,12 @@ def Renaming.comp (ρ : Renaming n m k n' m' k') (ρ' : Renaming n' m' k' n'' m' cvar := ρ.cvar.comp ρ'.cvar } +def CaptureRenaming.comp (ρ : CaptureRenaming n k n' k') (ρ' : CaptureRenaming n' k' n'' k'') : CaptureRenaming n k n'' k'' := + { + var := ρ.var.comp ρ'.var + cvar := ρ.cvar.comp ρ'.cvar + } + /-! Basic properties of renamings. -/ @@ -239,4 +259,13 @@ theorem Renaming.comp_cweaken {ρ : Renaming n m k n' m' k'} : simp [Renaming.cweaken, Renaming.comp, Renaming.cext] simp [FinFun.comp_weaken, FinFun.comp_id, FinFun.id_comp] +theorem Renaming.comp_asCapt {ρ : Renaming n m k n' m' k'} {ρ' : Renaming n' m' k' n'' m'' k''} : + (ρ.comp ρ').asCapt = ρ.asCapt.comp ρ'.asCapt := by + simp [Renaming.asCapt, CaptureRenaming.comp, Renaming.comp] + +theorem Renaming.weaken_transportM {n m1 m2 k : Nat} : + (Renaming.weaken (n:=n) (m:=m1) (k:=k)).asCapt = + (Renaming.weaken (n:=n) (m:=m2) (k:=k)).asCapt := by + simp [Renaming.weaken, Renaming.asCapt] + end Capybara diff --git a/Capybara/Syntax/CaptureSet/Core.lean b/Capybara/Syntax/CaptureSet/Core.lean index 0a300d3f..c367787a 100644 --- a/Capybara/Syntax/CaptureSet/Core.lean +++ b/Capybara/Syntax/CaptureSet/Core.lean @@ -35,7 +35,7 @@ Renaming functions for capture sets. -/ def CaptureSet.rename (C : CaptureSet n k) - (ρ : Renaming n m k n' m' k') : + (ρ : CaptureRenaming n k n' k') : CaptureSet n' k' := match C with | empty => {} @@ -65,9 +65,9 @@ def CaptureSet.ro (C : CaptureSet n k) : CaptureSet n k := Weakening functions for capture sets. -/ def CaptureSet.weaken : CaptureSet n k -> CaptureSet (n+1) k := - fun C => C.rename (Renaming.weaken (m:=0)) + fun C => C.rename (Renaming.weaken (m:=0)).asCapt def CaptureSet.cweaken : CaptureSet n k -> CaptureSet n (k+1) := - fun C => C.rename (Renaming.cweaken (m:=0)) + fun C => C.rename (Renaming.cweaken (m:=0)).asCapt /-! Basic theorems. diff --git a/Capybara/Syntax/CaptureSet/Properties.lean b/Capybara/Syntax/CaptureSet/Properties.lean index f96c63ac..9a1abe63 100644 --- a/Capybara/Syntax/CaptureSet/Properties.lean +++ b/Capybara/Syntax/CaptureSet/Properties.lean @@ -8,27 +8,32 @@ namespace Capybara We can show that renaming by the identity renaming yields the same capture set. -/ @[simp] -theorem CaptureSet.rename_id {C : CaptureSet n k} : C.rename (Renaming.id (m:=m)) = C := by +theorem CaptureSet.rename_id {C : CaptureSet n k} : C.rename (Renaming.id (m:=m).asCapt) = C := by induction C <;> simp [CaptureSet.rename] case union ih1 ih2 => simp [ih1, ih2] - case singleton => simp [Renaming.id, FinFun.id] - case csingleton => simp [Renaming.id, FinFun.id] + case singleton => simp [Renaming.id, Renaming.asCapt, FinFun.id] + case csingleton => simp [Renaming.id, Renaming.asCapt, FinFun.id] /-! ## Composition of renamings In the following, we show that renaming composes. -/ -theorem CaptureSet.rename_comp {C : CaptureSet n k} : +theorem CaptureSet.rename_comp {ρ : CaptureRenaming n k n' k'} {ρ' : CaptureRenaming n' k' n'' k''} {C : CaptureSet n k} : (C.rename ρ).rename ρ' = C.rename (ρ.comp ρ') := by induction C <;> simp [CaptureSet.rename] case union ih1 ih2 => simp [ih1, ih2] - case singleton => simp [Renaming.comp, FinFun.comp] - case csingleton => simp [Renaming.comp, FinFun.comp] + case singleton => simp [CaptureRenaming.comp, FinFun.comp] + case csingleton => simp [CaptureRenaming.comp, FinFun.comp] -theorem CaptureSet.rename_weaken {C : CaptureSet n k} : - (C.rename ρ).weaken = C.weaken.rename ρ.ext := by +theorem CaptureSet.rename_weaken {C : CaptureSet n k} {ρ : Renaming n m k n' m' k'} : + (C.rename ρ.asCapt).weaken = C.weaken.rename ρ.ext.asCapt := by simp [CaptureSet.weaken] - sorry + simp [CaptureSet.rename_comp] + rw [Renaming.weaken_transportM (m1:=0) (m2:=m')] + rw [<-Renaming.comp_asCapt] + rw [Renaming.weaken_transportM (m1:=0) (m2:=m)] + rw [<-Renaming.comp_asCapt] + simp [Renaming.comp_weaken] end Capybara diff --git a/Capybara/Syntax/Context/Core.lean b/Capybara/Syntax/Context/Core.lean index fd0205f9..e3d3c488 100644 --- a/Capybara/Syntax/Context/Core.lean +++ b/Capybara/Syntax/Context/Core.lean @@ -32,13 +32,13 @@ notation:max "calias" C => CBinding.capturealias C /-! Renaming functions for type and capture set binding. -/ -def CKind.rename : CKind n k -> Renaming n m k n' m' k' -> CKind n' k' +def CKind.rename : CKind n k -> CaptureRenaming n k n' k' -> CKind n' k' | CKind.Sep D, ρ => CKind.Sep (D.rename ρ) | CKind.Fresh, _ => CKind.Fresh def TBinding.rename : TBinding n m k -> Renaming n m k n' m' k' -> TBinding n' m' k' | TBinding.param T, ρ => TBinding.param (T.rename ρ) | TBinding.typealias T, ρ => TBinding.typealias (T.rename ρ) -def CBinding.rename : CBinding n k -> Renaming n m k n' m' k' -> CBinding n' k' +def CBinding.rename : CBinding n k -> CaptureRenaming n k n' k' -> CBinding n' k' | CBinding.param k, ρ => CBinding.param (k.rename ρ) | CBinding.capturealias C, ρ => CBinding.capturealias (C.rename ρ) @@ -48,17 +48,17 @@ Weakening functions for type and capture set binding. def TBinding.weaken (B : TBinding n m k) : TBinding (n+1) m k := B.rename (Renaming.weaken) def CKind.weaken (K : CKind n k) : CKind (n+1) k := - K.rename (Renaming.weaken (m:=0)) + K.rename (Renaming.weaken (m:=0)).asCapt def CBinding.weaken (B : CBinding n k) : CBinding (n+1) k := - B.rename (Renaming.weaken (m:=0)) + B.rename (Renaming.weaken (m:=0)).asCapt def TBinding.tweaken (B : TBinding n m k) : TBinding n (m+1) k := B.rename (Renaming.tweaken) def TBinding.cweaken (B : TBinding n m k) : TBinding n m (k+1) := B.rename (Renaming.cweaken) def CKind.cweaken (K : CKind n k) : CKind n (k+1) := - K.rename (Renaming.cweaken (m:=0)) + K.rename (Renaming.cweaken (m:=0)).asCapt def CBinding.cweaken (B : CBinding n k) : CBinding n (k+1) := - B.rename (Renaming.cweaken (m:=0)) + B.rename (Renaming.cweaken (m:=0)).asCapt /-! An indexed context. A `Context n m k` contains `n` term variables, diff --git a/Capybara/Syntax/Context/Properties.lean b/Capybara/Syntax/Context/Properties.lean index 721abd4e..3f035902 100644 --- a/Capybara/Syntax/Context/Properties.lean +++ b/Capybara/Syntax/Context/Properties.lean @@ -16,16 +16,24 @@ theorem TBinding.rename_weaken {B : TBinding n m k} : simp [TBinding.weaken, TBinding.rename] apply SType.rename_weaken -theorem CBinding.rename_weaken {B : CBinding n k} : - (B.rename ρ).weaken = B.weaken.rename ρ.ext := by +theorem CBinding.rename_weaken {B : CBinding n k} {ρ : Renaming n m k n' m' k'} : + (B.rename ρ.asCapt).weaken = B.weaken.rename ρ.ext.asCapt := by cases B case param K => simp [CBinding.weaken, CBinding.rename] cases K case Sep D => - cases D <;> simp [CKind.rename] <;> simp [SepDegree.rename] + cases D; simp [CKind.rename]; simp [SepDegree.rename] apply CaptureSet.rename_weaken case Fresh => simp [CKind.rename] + case capturealias C => + simp [CBinding.weaken, CBinding.rename] + simp [CaptureSet.rename_comp] + rw [Renaming.weaken_transportM (m1:=0) (m2:=m')] + rw [<-Renaming.comp_asCapt] + rw [Renaming.weaken_transportM (m1:=0) (m2:=m)] + rw [<-Renaming.comp_asCapt] + simp [Renaming.comp_weaken] end Capybara diff --git a/Capybara/Syntax/Term.lean b/Capybara/Syntax/Term.lean index d9e7bb78..df20f325 100644 --- a/Capybara/Syntax/Term.lean +++ b/Capybara/Syntax/Term.lean @@ -53,7 +53,7 @@ def Term.rename | var x => var (ρ.var x) | lam t1 t2 => lam (t1.rename ρ) (t2.rename ρ.ext) | tlam t1 t2 => tlam (t1.rename ρ) (t2.rename ρ.text) - | clam D t => clam (D.rename ρ) (t.rename ρ.cext) + | clam D t => clam (D.rename ρ.asCapt) (t.rename ρ.cext) | flam T t => flam (T.rename ρ.cext) (t.rename ρ.cext.ext) | pack x y => pack (ρ.cvar x) (ρ.var y) | app x y => app (ρ.var x) (ρ.var y) @@ -62,7 +62,7 @@ def Term.rename | fapp x c y => fapp (ρ.var x) (ρ.cvar c) (ρ.var y) | letin t1 t2 => letin (t1.rename ρ) (t2.rename ρ.ext) | unpack t1 t2 => unpack (t1.rename ρ) (t2.rename ρ.cext.ext) - | calias C t => calias (C.rename ρ) (t.rename ρ.cext) + | calias C t => calias (C.rename ρ.asCapt) (t.rename ρ.cext) | talias T t => talias (T.rename ρ) (t.rename ρ.text) /-! diff --git a/Capybara/Syntax/Type/Properties.lean b/Capybara/Syntax/Type/Properties.lean index 59d7280f..70ef9ebd 100644 --- a/Capybara/Syntax/Type/Properties.lean +++ b/Capybara/Syntax/Type/Properties.lean @@ -10,7 +10,7 @@ namespace Capybara ## Renaming identity First, we show that renaming by the identity renaming yields the separation degree. -/ -theorem SepDegree.rename_id {D : SepDegree n k} : D.rename (Renaming.id (m:=m)) = D := by +theorem SepDegree.rename_id {D : SepDegree n k} : D.rename (Renaming.id (m:=m)).asCapt = D := by cases D; simp [SepDegree.rename] /-! @@ -83,7 +83,7 @@ theorem CType.rename_comp {C : CType n m k} : match C with | .capt m' C' S => by simp [CType.rename, SType.rename_comp] - simp [CaptureSet.rename_comp] + simp [CaptureSet.rename_comp, Renaming.comp_asCapt] theorem SType.rename_comp {S : SType n m k} : (S.rename ρ).rename ρ' = S.rename (ρ.comp ρ') := @@ -100,7 +100,7 @@ theorem SType.rename_comp {S : SType n m k} : simp [CType.rename_comp, EType.rename_comp, Renaming.comp_ext] | .carrow D T => by simp [SType.rename] - simp [EType.rename_comp, SepDegree.rename_comp, Renaming.comp_cext] + simp [EType.rename_comp, SepDegree.rename_comp, Renaming.comp_cext, Renaming.comp_asCapt] | .farrow C T => by simp [SType.rename] simp [CType.rename_comp, EType.rename_comp, Renaming.comp_cext, Renaming.comp_ext] diff --git a/Capybara/Syntax/Type/Renaming.lean b/Capybara/Syntax/Type/Renaming.lean index 030b71d1..08d5bf98 100644 --- a/Capybara/Syntax/Type/Renaming.lean +++ b/Capybara/Syntax/Type/Renaming.lean @@ -3,7 +3,7 @@ namespace Capybara def SepDegree.rename (D : SepDegree n k) - (ρ : Renaming n m k n' m' k') : + (ρ : CaptureRenaming n k n' k') : SepDegree n' k' := match D with | ⟨s, C⟩ => ⟨s, C.rename ρ⟩ @@ -23,14 +23,14 @@ def CType.rename (ρ : Renaming n m k n' m' k') : CType n' m' k' := match T with - | CType.capt C m S => CType.capt (C.rename ρ) m (S.rename ρ) + | CType.capt C m S => CType.capt (C.rename ρ.asCapt) m (S.rename ρ) def SType.rename (S : SType n m k) (ρ : Renaming n m k n' m' k') : SType n' m' k' := match S with | SType.top => SType.top | SType.tvar x => SType.tvar (ρ.tvar x) | SType.arrow T E => (x:T.rename ρ)->(E.rename ρ.ext) - | SType.carrow D E => [c:D.rename ρ]->(E.rename ρ.cext) + | SType.carrow D E => [c:D.rename ρ.asCapt]->(E.rename ρ.cext) | SType.farrow T E => [c:Fresh](x:T.rename ρ.cext)->(E.rename ρ.cext.ext) | SType.tarrow S T => [X<:S.rename ρ]->(T.rename ρ.text) From f4418282fc7e3d62d671988f7fdd18807aafd303 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 23 Jan 2025 14:23:20 +0800 Subject: [PATCH 60/84] proof(rebind): rebinding.ext --- Capybara/Morphism/Rebinding.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Capybara/Morphism/Rebinding.lean b/Capybara/Morphism/Rebinding.lean index 1e287016..51ed3c45 100644 --- a/Capybara/Morphism/Rebinding.lean +++ b/Capybara/Morphism/Rebinding.lean @@ -7,7 +7,7 @@ structure Rebinding (Γ : Context n m k) (Δ : Context n' m' k') where ρ : Renaming n m k n' m' k' var : ∀ {x T}, Γ.Lookup x T -> Δ.Lookup (ρ.var x) (T.rename ρ) tvar : ∀ {X S}, Γ.LookupT X S -> Δ.LookupT (ρ.tvar X) (S.rename ρ) - cvar : ∀ {c K}, Γ.LookupC c K -> Δ.LookupC (ρ.cvar c) (K.rename ρ) + cvar : ∀ {c K}, Γ.LookupC c K -> Δ.LookupC (ρ.cvar c) (K.rename ρ.asCapt) def Rebinding.ext (θ : Rebinding Γ Δ) : Rebinding (Γ,x:T) (Δ,x:T.rename θ.ρ) := by constructor @@ -35,6 +35,8 @@ def Rebinding.ext (θ : Rebinding Γ Δ) : Rebinding (Γ,x:T) (Δ,x:T.rename θ. intro c B hb cases hb case there hb => - sorry + simp [<-CBinding.rename_weaken] + constructor + apply θ.cvar; easy end Capybara From 0648efbf18c8213cbb8a908eb603ee2eb20760cd Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 23 Jan 2025 14:32:24 +0800 Subject: [PATCH 61/84] proof(rebind): rebinding.text --- Capybara/Morphism/Core.lean | 5 ++++ Capybara/Morphism/Rebinding.lean | 33 +++++++++++++++++++++++++ Capybara/Syntax/Context/Properties.lean | 10 ++++++++ Capybara/Syntax/Type/Properties.lean | 8 ++++++ 4 files changed, 56 insertions(+) diff --git a/Capybara/Morphism/Core.lean b/Capybara/Morphism/Core.lean index 03c9245c..eddeca89 100644 --- a/Capybara/Morphism/Core.lean +++ b/Capybara/Morphism/Core.lean @@ -268,4 +268,9 @@ theorem Renaming.weaken_transportM {n m1 m2 k : Nat} : (Renaming.weaken (n:=n) (m:=m2) (k:=k)).asCapt := by simp [Renaming.weaken, Renaming.asCapt] +@[simp] +theorem Renaming.text_asCapt {ρ : Renaming n m k n' m' k'} : + ρ.text.asCapt = ρ.asCapt := by + simp [text, asCapt] + end Capybara diff --git a/Capybara/Morphism/Rebinding.lean b/Capybara/Morphism/Rebinding.lean index 51ed3c45..2de5bb16 100644 --- a/Capybara/Morphism/Rebinding.lean +++ b/Capybara/Morphism/Rebinding.lean @@ -3,6 +3,11 @@ import Capybara.Syntax import Capybara.Morphism.Core namespace Capybara +/-! +# Rebinding + +A rebinding is a morphism from a source context `Γ` to a target context `Δ` that maps each binding in `Γ` to an equivalent one in `Δ`. +-/ structure Rebinding (Γ : Context n m k) (Δ : Context n' m' k') where ρ : Renaming n m k n' m' k' var : ∀ {x T}, Γ.Lookup x T -> Δ.Lookup (ρ.var x) (T.rename ρ) @@ -39,4 +44,32 @@ def Rebinding.ext (θ : Rebinding Γ Δ) : Rebinding (Γ,x:T) (Δ,x:T.rename θ. constructor apply θ.cvar; easy +def Rebinding.text (θ : Rebinding Γ Δ) : Rebinding (Γ,X:B) (Δ,X:B.rename θ.ρ) := by + constructor + case ρ => exact θ.ρ.text + case var => + intro x T hb + cases hb + case tthere hb => + simp [<-CType.rename_tweaken] + constructor + apply θ.var; easy + case tvar => + intro X B hb + cases hb + case here => + simp [<-TBinding.rename_tweaken] + constructor + case tthere hb => + simp [<-TBinding.rename_tweaken] + constructor + apply θ.tvar; easy + case cvar => + intro c B hb + cases hb + case tthere hb => + simp + constructor + apply θ.cvar; easy + end Capybara diff --git a/Capybara/Syntax/Context/Properties.lean b/Capybara/Syntax/Context/Properties.lean index 3f035902..57232e0b 100644 --- a/Capybara/Syntax/Context/Properties.lean +++ b/Capybara/Syntax/Context/Properties.lean @@ -16,6 +16,16 @@ theorem TBinding.rename_weaken {B : TBinding n m k} : simp [TBinding.weaken, TBinding.rename] apply SType.rename_weaken +theorem TBinding.rename_tweaken {B : TBinding n m k} : + (B.rename ρ).tweaken = B.tweaken.rename ρ.text := by + cases B + case param => + simp [TBinding.tweaken, TBinding.rename] + apply SType.rename_tweaken + case typealias => + simp [TBinding.tweaken, TBinding.rename] + apply SType.rename_tweaken + theorem CBinding.rename_weaken {B : CBinding n k} {ρ : Renaming n m k n' m' k'} : (B.rename ρ.asCapt).weaken = B.weaken.rename ρ.ext.asCapt := by cases B diff --git a/Capybara/Syntax/Type/Properties.lean b/Capybara/Syntax/Type/Properties.lean index 70ef9ebd..4ed9bca4 100644 --- a/Capybara/Syntax/Type/Properties.lean +++ b/Capybara/Syntax/Type/Properties.lean @@ -114,8 +114,16 @@ theorem CType.rename_weaken {T : CType n m k} : (T.rename ρ).weaken = T.weaken.rename ρ.ext := by simp [CType.weaken, CType.rename_comp, Renaming.comp_weaken] +theorem CType.rename_tweaken {T : CType n m k} : + (T.rename ρ).tweaken = T.tweaken.rename ρ.text := by + simp [CType.tweaken, CType.rename_comp, Renaming.comp_tweaken] + theorem SType.rename_weaken {S : SType n m k} : (S.rename ρ).weaken = S.weaken.rename ρ.ext := by simp [SType.weaken, SType.rename_comp, Renaming.comp_weaken] +theorem SType.rename_tweaken {S : SType n m k} : + (S.rename ρ).tweaken = S.tweaken.rename ρ.text := by + simp [SType.tweaken, SType.rename_comp, Renaming.comp_tweaken] + end Capybara From 8e781c11e8577c0ae9c15d3d889ec4d17b1bb160 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 23 Jan 2025 14:33:36 +0800 Subject: [PATCH 62/84] proof(rebind): doc --- Capybara/Morphism/Rebinding.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Capybara/Morphism/Rebinding.lean b/Capybara/Morphism/Rebinding.lean index 2de5bb16..d49539dc 100644 --- a/Capybara/Morphism/Rebinding.lean +++ b/Capybara/Morphism/Rebinding.lean @@ -6,6 +6,7 @@ namespace Capybara /-! # Rebinding +## Definition A rebinding is a morphism from a source context `Γ` to a target context `Δ` that maps each binding in `Γ` to an equivalent one in `Δ`. -/ structure Rebinding (Γ : Context n m k) (Δ : Context n' m' k') where @@ -14,6 +15,10 @@ structure Rebinding (Γ : Context n m k) (Δ : Context n' m' k') where tvar : ∀ {X S}, Γ.LookupT X S -> Δ.LookupT (ρ.tvar X) (S.rename ρ) cvar : ∀ {c K}, Γ.LookupC c K -> Δ.LookupC (ρ.cvar c) (K.rename ρ.asCapt) +/-! +## Extensions +The following methods lift rebindings to environments with more bindings. +-/ def Rebinding.ext (θ : Rebinding Γ Δ) : Rebinding (Γ,x:T) (Δ,x:T.rename θ.ρ) := by constructor case ρ => exact θ.ρ.ext From 9998d2a3aa1b1bcfe50ec0177f34752f176fd8d2 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 23 Jan 2025 14:42:21 +0800 Subject: [PATCH 63/84] proof(rebind): cext --- Capybara/Morphism/Core.lean | 5 ++++ Capybara/Morphism/Rebinding.lean | 28 ++++++++++++++++++++++ Capybara/Syntax/CaptureSet/Properties.lean | 9 +++++++ Capybara/Syntax/Context/Properties.lean | 25 +++++++++++++++++++ Capybara/Syntax/Type/Properties.lean | 8 +++++++ 5 files changed, 75 insertions(+) diff --git a/Capybara/Morphism/Core.lean b/Capybara/Morphism/Core.lean index eddeca89..3f397e69 100644 --- a/Capybara/Morphism/Core.lean +++ b/Capybara/Morphism/Core.lean @@ -268,6 +268,11 @@ theorem Renaming.weaken_transportM {n m1 m2 k : Nat} : (Renaming.weaken (n:=n) (m:=m2) (k:=k)).asCapt := by simp [Renaming.weaken, Renaming.asCapt] +theorem Renaming.cweaken_transportM {n m1 m2 k : Nat} : + (Renaming.cweaken (n:=n) (m:=m1) (k:=k)).asCapt = + (Renaming.cweaken (n:=n) (m:=m2) (k:=k)).asCapt := by + simp [Renaming.cweaken, Renaming.asCapt] + @[simp] theorem Renaming.text_asCapt {ρ : Renaming n m k n' m' k'} : ρ.text.asCapt = ρ.asCapt := by diff --git a/Capybara/Morphism/Rebinding.lean b/Capybara/Morphism/Rebinding.lean index d49539dc..4690f9f9 100644 --- a/Capybara/Morphism/Rebinding.lean +++ b/Capybara/Morphism/Rebinding.lean @@ -77,4 +77,32 @@ def Rebinding.text (θ : Rebinding Γ Δ) : Rebinding (Γ,X:B) (Δ,X:B.rename θ constructor apply θ.cvar; easy +def Rebinding.cext (θ : Rebinding Γ Δ) : Rebinding (Γ,c:K) (Δ,c:K.rename θ.ρ.asCapt) := by + constructor + case ρ => exact θ.ρ.cext + case var => + intro x T hb + cases hb + case cthere hb => + simp [<-CType.rename_cweaken] + constructor + apply θ.var; easy + case tvar => + intro X B hb + cases hb + case cthere hb => + simp [<-TBinding.rename_cweaken] + constructor + apply θ.tvar; easy + case cvar => + intro c K hb + cases hb + case here => + simp [<-CBinding.rename_cweaken] + constructor + case cthere hb => + simp [<-CBinding.rename_cweaken] + constructor + apply θ.cvar; easy + end Capybara diff --git a/Capybara/Syntax/CaptureSet/Properties.lean b/Capybara/Syntax/CaptureSet/Properties.lean index 9a1abe63..f423ab66 100644 --- a/Capybara/Syntax/CaptureSet/Properties.lean +++ b/Capybara/Syntax/CaptureSet/Properties.lean @@ -35,5 +35,14 @@ theorem CaptureSet.rename_weaken {C : CaptureSet n k} {ρ : Renaming n m k n' m' rw [<-Renaming.comp_asCapt] simp [Renaming.comp_weaken] +theorem CaptureSet.rename_cweaken {C : CaptureSet n k} {ρ : Renaming n m k n' m' k'} : + (C.rename ρ.asCapt).cweaken = C.cweaken.rename ρ.cext.asCapt := by + simp [CaptureSet.cweaken, CaptureSet.rename_comp] + rw [Renaming.cweaken_transportM (m1:=0) (m2:=m')] + rw [<-Renaming.comp_asCapt] + rw [Renaming.cweaken_transportM (m1:=0) (m2:=m)] + rw [<-Renaming.comp_asCapt] + simp [Renaming.comp_cweaken] + end Capybara diff --git a/Capybara/Syntax/Context/Properties.lean b/Capybara/Syntax/Context/Properties.lean index 57232e0b..d25094dd 100644 --- a/Capybara/Syntax/Context/Properties.lean +++ b/Capybara/Syntax/Context/Properties.lean @@ -26,6 +26,16 @@ theorem TBinding.rename_tweaken {B : TBinding n m k} : simp [TBinding.tweaken, TBinding.rename] apply SType.rename_tweaken +theorem TBinding.rename_cweaken {B : TBinding n m k} : + (B.rename ρ).cweaken = B.cweaken.rename ρ.cext := by + cases B + case param => + simp [TBinding.cweaken, TBinding.rename] + apply SType.rename_cweaken + case typealias => + simp [TBinding.cweaken, TBinding.rename] + apply SType.rename_cweaken + theorem CBinding.rename_weaken {B : CBinding n k} {ρ : Renaming n m k n' m' k'} : (B.rename ρ.asCapt).weaken = B.weaken.rename ρ.ext.asCapt := by cases B @@ -46,4 +56,19 @@ theorem CBinding.rename_weaken {B : CBinding n k} {ρ : Renaming n m k n' m' k'} rw [<-Renaming.comp_asCapt] simp [Renaming.comp_weaken] +theorem CBinding.rename_cweaken {B : CBinding n k} {ρ : Renaming n m k n' m' k'} : + (B.rename ρ.asCapt).cweaken = B.cweaken.rename ρ.cext.asCapt := by + cases B + case param K => + simp [CBinding.cweaken, CBinding.rename] + cases K + case Sep D => + cases D; simp [CKind.rename]; simp [SepDegree.rename] + apply CaptureSet.rename_cweaken + case Fresh => + simp [CKind.rename] + case capturealias C => + simp [CBinding.cweaken]; simp [CBinding.rename] + apply CaptureSet.rename_cweaken + end Capybara diff --git a/Capybara/Syntax/Type/Properties.lean b/Capybara/Syntax/Type/Properties.lean index 4ed9bca4..656c5c15 100644 --- a/Capybara/Syntax/Type/Properties.lean +++ b/Capybara/Syntax/Type/Properties.lean @@ -118,6 +118,10 @@ theorem CType.rename_tweaken {T : CType n m k} : (T.rename ρ).tweaken = T.tweaken.rename ρ.text := by simp [CType.tweaken, CType.rename_comp, Renaming.comp_tweaken] +theorem CType.rename_cweaken {T : CType n m k} : + (T.rename ρ).cweaken = T.cweaken.rename ρ.cext := by + simp [CType.cweaken, CType.rename_comp, Renaming.comp_cweaken] + theorem SType.rename_weaken {S : SType n m k} : (S.rename ρ).weaken = S.weaken.rename ρ.ext := by simp [SType.weaken, SType.rename_comp, Renaming.comp_weaken] @@ -126,4 +130,8 @@ theorem SType.rename_tweaken {S : SType n m k} : (S.rename ρ).tweaken = S.tweaken.rename ρ.text := by simp [SType.tweaken, SType.rename_comp, Renaming.comp_tweaken] +theorem SType.rename_cweaken {S : SType n m k} : + (S.rename ρ).cweaken = S.cweaken.rename ρ.cext := by + simp [SType.cweaken, SType.rename_comp, Renaming.comp_cweaken] + end Capybara From 43215889f85f1a9d7772905e28d2fa18db774ce1 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 23 Jan 2025 14:50:34 +0800 Subject: [PATCH 64/84] proof(rebind): subcapturing wip --- Capybara/Rebinding/Subcapturing.lean | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 Capybara/Rebinding/Subcapturing.lean diff --git a/Capybara/Rebinding/Subcapturing.lean b/Capybara/Rebinding/Subcapturing.lean new file mode 100644 index 00000000..ec3eb616 --- /dev/null +++ b/Capybara/Rebinding/Subcapturing.lean @@ -0,0 +1,19 @@ +import Capybara.StaticSemantics +import Capybara.Morphism.Rebinding +namespace Capybara + +theorem Subcapturing.rebind + (h : Γ ⊢c C1 <: C2) + (θ : Rebinding Γ Δ) : + Δ ⊢c (C1.rename θ.ρ.asCapt) <: (C2.rename θ.ρ.asCapt) := by + induction h + case subset => sorry + case trans ih1 ih2 => apply trans <;> aesop + case union ih1 ih2 => apply union <;> aesop + case mode => sorry + case var => sorry + case rovar => sorry + case cvar_l => sorry + case cvar_r => sorry + +end Capybara From 8ef1a0fbdcc788f2e8e411a15676fd54757c239a Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 23 Jan 2025 14:53:09 +0800 Subject: [PATCH 65/84] staging --- Capybara/Rebinding/Subcapturing.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Capybara/Rebinding/Subcapturing.lean b/Capybara/Rebinding/Subcapturing.lean index ec3eb616..fba81333 100644 --- a/Capybara/Rebinding/Subcapturing.lean +++ b/Capybara/Rebinding/Subcapturing.lean @@ -7,7 +7,7 @@ theorem Subcapturing.rebind (θ : Rebinding Γ Δ) : Δ ⊢c (C1.rename θ.ρ.asCapt) <: (C2.rename θ.ρ.asCapt) := by induction h - case subset => sorry + case subset hs => sorry case trans ih1 ih2 => apply trans <;> aesop case union ih1 ih2 => apply union <;> aesop case mode => sorry From 6cd584ed21504bf1bed44644011a88fe34820f1f Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 23 Jan 2025 17:14:40 +0800 Subject: [PATCH 66/84] proof: capture set properties --- Capybara/Syntax/CaptureSet/Properties.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Capybara/Syntax/CaptureSet/Properties.lean b/Capybara/Syntax/CaptureSet/Properties.lean index f423ab66..d92e790e 100644 --- a/Capybara/Syntax/CaptureSet/Properties.lean +++ b/Capybara/Syntax/CaptureSet/Properties.lean @@ -44,5 +44,12 @@ theorem CaptureSet.rename_cweaken {C : CaptureSet n k} {ρ : Renaming n m k n' m rw [<-Renaming.comp_asCapt] simp [Renaming.comp_cweaken] +theorem CaptureSet.rename_subset {C1 C2 : CaptureSet n k} {ρ : CaptureRenaming n k n' k'} (hs : C1 ⊆ C2) : + (C1.rename ρ) ⊆ (C2.rename ρ) := by + induction hs <;> try simp [CaptureSet.rename] <;> try (solve | constructor) + case refl => apply Subset.refl + case union_l ih1 ih2 => constructor <;> aesop + case union_rl => apply Subset.union_rl; aesop + case union_rr => apply Subset.union_rr; aesop end Capybara From 7654685ef2b3d52ebccfa141825bb76f959094fd Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Fri, 24 Jan 2025 17:38:33 +0800 Subject: [PATCH 67/84] I am so sorry --- Capless/Tactics.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Capless/Tactics.lean b/Capless/Tactics.lean index 3c8b95ac..3442051f 100644 --- a/Capless/Tactics.lean +++ b/Capless/Tactics.lean @@ -1,4 +1,5 @@ macro "easy" : tactic => `(tactic| assumption) +macro "sosorry" : tactic => `(tactic| all_goals sorry) macro "split_and" : tactic => `(tactic| repeat any_goals apply And.intro) macro "apply!" e:term : tactic => `(tactic| apply $e <;> easy) macro "apply?" e:term : tactic => `(tactic| apply $e <;> try easy) From 3f3c2770a5b3e43cfdbcf43f31e034899e9c7b52 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Fri, 24 Jan 2025 19:09:51 +0800 Subject: [PATCH 68/84] proof(rebind): subcapturing --- Capybara/Morphism/Core.lean | 5 +++ Capybara/Rebinding/Subcapturing.lean | 46 ++++++++++++++++++---- Capybara/Syntax/CaptureSet/Properties.lean | 11 ++++++ 3 files changed, 54 insertions(+), 8 deletions(-) diff --git a/Capybara/Morphism/Core.lean b/Capybara/Morphism/Core.lean index 3f397e69..421eac7a 100644 --- a/Capybara/Morphism/Core.lean +++ b/Capybara/Morphism/Core.lean @@ -278,4 +278,9 @@ theorem Renaming.text_asCapt {ρ : Renaming n m k n' m' k'} : ρ.text.asCapt = ρ.asCapt := by simp [text, asCapt] +@[simp] +theorem Renaming.asCapt_var {ρ : Renaming n m k n' m' k'} : + ρ.asCapt.var = ρ.var := by + simp [asCapt] + end Capybara diff --git a/Capybara/Rebinding/Subcapturing.lean b/Capybara/Rebinding/Subcapturing.lean index fba81333..020d1dbe 100644 --- a/Capybara/Rebinding/Subcapturing.lean +++ b/Capybara/Rebinding/Subcapturing.lean @@ -7,13 +7,43 @@ theorem Subcapturing.rebind (θ : Rebinding Γ Δ) : Δ ⊢c (C1.rename θ.ρ.asCapt) <: (C2.rename θ.ρ.asCapt) := by induction h - case subset hs => sorry - case trans ih1 ih2 => apply trans <;> aesop - case union ih1 ih2 => apply union <;> aesop - case mode => sorry - case var => sorry - case rovar => sorry - case cvar_l => sorry - case cvar_r => sorry + case subset hs => + apply Subcapturing.subset + apply CaptureSet.rename_subset hs + case trans ih1 ih2 => + apply Subcapturing.trans + · exact ih1 θ + · exact ih2 θ + case union ih1 ih2 => + apply Subcapturing.union + · exact ih1 θ + · exact ih2 θ + case mode h1 h2 => + simp [CaptureSet.qualified_rename] + apply mode; easy + case var hb => + simp [CaptureSet.rename] + simp [CaptureSet.qualified_rename] + apply var + have hb1 := θ.var hb + exact hb1 + case rovar hb => + simp [CaptureSet.rename] + simp [CaptureSet.qualified_rename] + apply rovar + have hb1 := θ.var hb + exact hb1 + case cvar_l hb => + simp [CaptureSet.rename] + simp [CaptureSet.qualified_rename] + apply cvar_l + have hb1 := θ.cvar hb + exact hb1 + case cvar_r hb => + simp [CaptureSet.rename] + simp [CaptureSet.qualified_rename] + apply cvar_r + have hb1 := θ.cvar hb + exact hb1 end Capybara diff --git a/Capybara/Syntax/CaptureSet/Properties.lean b/Capybara/Syntax/CaptureSet/Properties.lean index d92e790e..4998ed09 100644 --- a/Capybara/Syntax/CaptureSet/Properties.lean +++ b/Capybara/Syntax/CaptureSet/Properties.lean @@ -52,4 +52,15 @@ theorem CaptureSet.rename_subset {C1 C2 : CaptureSet n k} {ρ : CaptureRenaming case union_rl => apply Subset.union_rl; aesop case union_rr => apply Subset.union_rr; aesop +theorem CaptureSet.qualified_rename {C : CaptureSet n k} : + (C.qualified m).rename ρ = (C.rename ρ).qualified m := by + induction C <;> simp [CaptureSet.qualified, CaptureSet.rename] + case union ih1 ih2 => simp [ih1, ih2] + case singleton => + cases m <;> try simp [CaptureSet.qualified, CaptureSet.rename] + case M mu => cases mu <;> simp [CaptureSet.qualified, CaptureSet.rename] + case csingleton => + cases m <;> try simp [CaptureSet.qualified, CaptureSet.rename] + case M mu => cases mu <;> simp [CaptureSet.qualified, CaptureSet.rename] + end Capybara From 1011a2e61118aafc8396dcd21582bc4d47354782 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Fri, 24 Jan 2025 20:27:25 +0800 Subject: [PATCH 69/84] proof(rebind): subtyping --- Capybara/Rebinding/Subtyping.lean | 116 ++++++++++++++++++++++++++++++ 1 file changed, 116 insertions(+) create mode 100644 Capybara/Rebinding/Subtyping.lean diff --git a/Capybara/Rebinding/Subtyping.lean b/Capybara/Rebinding/Subtyping.lean new file mode 100644 index 00000000..05c8c10d --- /dev/null +++ b/Capybara/Rebinding/Subtyping.lean @@ -0,0 +1,116 @@ +import Capybara.StaticSemantics +import Capybara.Rebinding.Subcapturing +namespace Capybara + +private def motive_1 + (Γ : Context n m k) (S1 S2 : SType n m k) + (_ : SSubtyping Γ S1 S2) : Prop := + ∀ {n' m' k'} {Δ : Context n' m' k'} (θ : Rebinding Γ Δ), SSubtyping Δ (S1.rename θ.ρ) (S2.rename θ.ρ) + +private def motive_2 + (Γ : Context n m k) (T1 T2 : CType n m k) + (_ : CSubtyping Γ T1 T2) : Prop := + ∀ {n' m' k'} {Δ : Context n' m' k'} (θ : Rebinding Γ Δ), CSubtyping Δ (T1.rename θ.ρ) (T2.rename θ.ρ) + +private def motive_3 + (Γ : Context n m k) (E1 E2 : EType n m k) + (_ : ESubtyping Γ E1 E2) : Prop := + ∀ {n' m' k'} {Δ : Context n' m' k'} (θ : Rebinding Γ Δ), ESubtyping Δ (E1.rename θ.ρ) (E2.rename θ.ρ) + +syntax "unfold_all" : tactic + +macro_rules + | `(tactic| unfold_all) => `(tactic| try unfold motive_1 at *; try unfold motive_2 at *; try unfold motive_3 at *) + +theorem SSubtyping.rebind + (h : SSubtyping Γ S1 S2) + (θ : Rebinding Γ Δ) : + SSubtyping Δ (S1.rename θ.ρ) (S2.rename θ.ρ) := by + apply SSubtyping.rec + (motive_1:=motive_1) + (motive_2:=motive_2) + (motive_3:=motive_3) + (t:=h) + all_goals (unfold_all; repeat intro) + case top => constructor + case refl => apply SSubtyping.refl + case trans => + rename_i ih1 ih2 _ _ _ _ _ + apply trans <;> aesop + case tvar => + rename_i hb _ _ _ _ θ + apply tvar + have hb1 := θ.tvar hb + exact hb1 + case arrow T2 T1 _ _ _ _ ih1 ih2 _ _ _ _ θ => + simp [SType.rename] + apply arrow + { aesop } + { let θ' := θ.ext (T:=T2) + apply ih2 θ' } + case tarrow S2 S1 _ _ _ _ ih1 ih2 _ _ _ _ θ => + unfold motive_3 at ih2 + simp [SType.rename] + apply tarrow + { aesop } + { let θ' := θ.text (B:=tparam S2) + apply ih2 θ' } + case carrow K _ _ _ ih _ _ _ _ θ => + unfold motive_3 at ih + simp [SType.rename] + apply carrow + { let θ' := θ.cext (K:=cparam (CKind.Sep K)) + apply ih θ' } + case talias_l hb _ _ _ _ θ => + simp [SType.rename] + apply talias_l + have hb1 := θ.tvar hb + exact hb1 + case talias_r hb _ _ _ _ θ => + simp [SType.rename] + apply talias_r + have hb1 := θ.tvar hb + exact hb1 + case capt ih _ _ _ _ θ => + simp [CType.rename] + apply CSubtyping.capt + { aesop } + { apply Subcapturing.rebind; easy } + case type ih _ _ _ _ θ => + simp [EType.rename] + apply ESubtyping.type + { aesop } + case ex ih _ _ _ _ θ => + unfold motive_2 at ih + simp [EType.rename] + apply ESubtyping.ex + let θ' := θ.cext (K:=cparam CKind.Fresh) + apply ih θ' + +theorem CSubtyping.rebind + (h : CSubtyping Γ T1 T2) + (θ : Rebinding Γ Δ) : + CSubtyping Δ (T1.rename θ.ρ) (T2.rename θ.ρ) := by + cases h + case capt hs hc => + simp [CType.rename] + apply CSubtyping.capt + { apply SSubtyping.rebind; easy } + { apply Subcapturing.rebind; easy } + +theorem ESubtyping.rebind + (h : ESubtyping Γ E1 E2) + (θ : Rebinding Γ Δ) : + ESubtyping Δ (E1.rename θ.ρ) (E2.rename θ.ρ) := by + cases h + case type hc => + simp [EType.rename] + apply ESubtyping.type + apply CSubtyping.rebind; easy + case ex hc => + simp [EType.rename] + apply ESubtyping.ex + let θ' := θ.cext (K:=cparam CKind.Fresh) + apply CSubtyping.rebind hc θ' + +end Capybara From 955e83d79fd842ba00de196c05ae783a71a74a56 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Fri, 24 Jan 2025 20:38:22 +0800 Subject: [PATCH 70/84] proof(rebind): init typing --- Capybara/Rebinding/Typing.lean | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 Capybara/Rebinding/Typing.lean diff --git a/Capybara/Rebinding/Typing.lean b/Capybara/Rebinding/Typing.lean new file mode 100644 index 00000000..ac861e21 --- /dev/null +++ b/Capybara/Rebinding/Typing.lean @@ -0,0 +1,5 @@ +import Capybara.StaticSemantics +import Capybara.Rebinding.Subtyping +namespace Capybara + +end Capybara From 4437ef1ecd01d7e7a1a8a30bd4c4cd6b727eae5e Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sat, 25 Jan 2025 13:20:18 +0800 Subject: [PATCH 71/84] proof(rebind): typing scaffold --- Capybara/Rebinding/Typing.lean | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/Capybara/Rebinding/Typing.lean b/Capybara/Rebinding/Typing.lean index ac861e21..d50430a0 100644 --- a/Capybara/Rebinding/Typing.lean +++ b/Capybara/Rebinding/Typing.lean @@ -2,4 +2,36 @@ import Capybara.StaticSemantics import Capybara.Rebinding.Subtyping namespace Capybara +theorem Typed.rebind {Γ : Context n m k} {Δ : Context n' m' k'} + (h : Typed C Γ t E) + (θ : Rebinding Γ Δ) : + Typed (C.rename θ.ρ.asCapt) Δ (t.rename θ.ρ) (E.rename θ.ρ) := by + induction h generalizing n' m' k' Δ + case var => + sorry + case pack => + sorry + case subc => + sorry + case abs => + sorry + case tabs => + sorry + case cabs => + sorry + case fabs => + sorry + case app => + sorry + case tapp => + sorry + case capp => + sorry + case fapp => + sorry + case letin => + sorry + case unpack => + sorry + end Capybara From 44b1bbdbb7134d14e3c4434142cc88f6625ed77b Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Fri, 31 Jan 2025 08:50:26 +0100 Subject: [PATCH 72/84] So easy --- Capless/Tactics.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Capless/Tactics.lean b/Capless/Tactics.lean index 3442051f..6eb2b355 100644 --- a/Capless/Tactics.lean +++ b/Capless/Tactics.lean @@ -1,5 +1,6 @@ macro "easy" : tactic => `(tactic| assumption) macro "sosorry" : tactic => `(tactic| all_goals sorry) +macro "soeasy" : tactic => `(tactic| all_goals easy) macro "split_and" : tactic => `(tactic| repeat any_goals apply And.intro) macro "apply!" e:term : tactic => `(tactic| apply $e <;> easy) macro "apply?" e:term : tactic => `(tactic| apply $e <;> try easy) From bcf427fa9582f5b898786a7d3b06462dfbb5f512 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Fri, 31 Jan 2025 09:15:50 +0100 Subject: [PATCH 73/84] proof(rebind): typing, capture roots wip --- Capybara/Morphism/Core.lean | 16 ++++++++ Capybara/Rebinding/CaptureRoot.lean | 43 ++++++++++++++++++++++ Capybara/Rebinding/Kinding.lean | 5 +++ Capybara/Rebinding/Typing.lean | 19 ++++++++-- Capybara/Syntax/CaptureSet/Properties.lean | 4 ++ Capybara/Syntax/Type/Properties.lean | 5 +++ 6 files changed, 88 insertions(+), 4 deletions(-) create mode 100644 Capybara/Rebinding/CaptureRoot.lean create mode 100644 Capybara/Rebinding/Kinding.lean diff --git a/Capybara/Morphism/Core.lean b/Capybara/Morphism/Core.lean index 421eac7a..9a5984bd 100644 --- a/Capybara/Morphism/Core.lean +++ b/Capybara/Morphism/Core.lean @@ -199,6 +199,16 @@ theorem Renaming.ext_var_succ {ρ : Renaming n m k n' m' k'} {x : Fin n} : ρ.ex theorem FinFun.id_comp_id {n : Nat} : FinFun.comp (n:=n) FinFun.id FinFun.id = FinFun.id := by rfl +@[simp] +theorem FinFun.id_comp_left {f : FinFun n n'} : FinFun.comp (n:=n) FinFun.id f = f := by + funext x + simp [FinFun.comp, FinFun.id] + +@[simp] +theorem FinFun.id_comp_right {f : FinFun n n'} : FinFun.comp (n:=n) f FinFun.id = f := by + funext x + simp [FinFun.comp, FinFun.id] + theorem Renaming.id_comp_id {n m k : Nat} : Renaming.comp (n:=n) (m:=m) (k:=k) Renaming.id Renaming.id = Renaming.id := by rfl theorem FinFun.id_ext {n : Nat} : FinFun.ext (n:=n) FinFun.id = FinFun.id := by @@ -283,4 +293,10 @@ theorem Renaming.asCapt_var {ρ : Renaming n m k n' m' k'} : ρ.asCapt.var = ρ.var := by simp [asCapt] +theorem Renaming.copen_comp {ρ : Renaming n m k n' m' k'} : + (Renaming.copen c).comp ρ = (ρ.cext).comp (Renaming.copen (ρ.cvar c)) := by + simp [Renaming.copen, Renaming.cext, Renaming.comp] + funext x + cases x using Fin.cases <;> simp [FinFun.comp, FinFun.open, FinFun.ext] + end Capybara diff --git a/Capybara/Rebinding/CaptureRoot.lean b/Capybara/Rebinding/CaptureRoot.lean new file mode 100644 index 00000000..11e894d7 --- /dev/null +++ b/Capybara/Rebinding/CaptureRoot.lean @@ -0,0 +1,43 @@ +import Capybara.Morphism.Rebinding +import Capybara.StaticSemantics +namespace Capybara + +def CaptureRoot.rename (r : CaptureRoot k) (f : FinFun k k') : CaptureRoot k' := + match r with + | ⟨m,c⟩ => ⟨m,f c⟩ + +theorem ReachRoot.rename + (h : ReachRoot Γ C r) + (θ : Rebinding Γ Δ) : + ReachRoot Δ (C.rename θ.ρ.asCapt) (r.rename θ.ρ.cvar) := by + induction h + case union_l ih => + rw [CaptureSet.rename_union] + simp [CaptureRoot.rename] at * + apply union_l + easy + case union_r ih => + rw [CaptureSet.rename_union] + simp [CaptureRoot.rename] at * + apply union_r + easy + case var hb _ ih => + simp [CaptureSet.rename] + simp [CaptureRoot.rename] at * + apply var + { have hb' := θ.var hb; easy } + { repeat rw [<-CaptureSet.qualified_rename] + easy } + case cvar_alias hb _ ih => + simp [CaptureSet.rename] + simp [CaptureRoot.rename] at * + apply cvar_alias + { have hb' := θ.cvar hb; easy } + { repeat rw [<-CaptureSet.qualified_rename] + easy } + case cvar hb => + simp [CaptureSet.rename, ReachRoot.rename] + apply cvar + have hb' := θ.cvar hb; easy + +end Capybara diff --git a/Capybara/Rebinding/Kinding.lean b/Capybara/Rebinding/Kinding.lean new file mode 100644 index 00000000..96955b1b --- /dev/null +++ b/Capybara/Rebinding/Kinding.lean @@ -0,0 +1,5 @@ +import Capybara.Morphism.Rebinding +import Capybara.StaticSemantics +namespace Capybara + +end Capybara diff --git a/Capybara/Rebinding/Typing.lean b/Capybara/Rebinding/Typing.lean index d50430a0..553ca1bf 100644 --- a/Capybara/Rebinding/Typing.lean +++ b/Capybara/Rebinding/Typing.lean @@ -7,10 +7,21 @@ theorem Typed.rebind {Γ : Context n m k} {Δ : Context n' m' k'} (θ : Rebinding Γ Δ) : Typed (C.rename θ.ρ.asCapt) Δ (t.rename θ.ρ) (E.rename θ.ρ) := by induction h generalizing n' m' k' Δ - case var => - sorry - case pack => - sorry + case var hb hp => + simp [CaptureSet.rename, Term.rename] + simp [EType.rename, CType.rename, CaptureSet.rename] + apply var + have hb' := θ.var hb + soeasy + case pack hd hk ih => + simp [Term.rename, EType.rename] + apply pack + { have ih := ih θ + simp [Term.rename, EType.rename] at ih + simp [CType.copen_rename] at ih + easy } + { sorry } + { sorry } case subc => sorry case abs => diff --git a/Capybara/Syntax/CaptureSet/Properties.lean b/Capybara/Syntax/CaptureSet/Properties.lean index 4998ed09..e6b650e9 100644 --- a/Capybara/Syntax/CaptureSet/Properties.lean +++ b/Capybara/Syntax/CaptureSet/Properties.lean @@ -63,4 +63,8 @@ theorem CaptureSet.qualified_rename {C : CaptureSet n k} : cases m <;> try simp [CaptureSet.qualified, CaptureSet.rename] case M mu => cases mu <;> simp [CaptureSet.qualified, CaptureSet.rename] +theorem CaptureSet.rename_union {C1 C2 : CaptureSet n k} {ρ : CaptureRenaming n k n' k'} : + (C1 ∪ C2).rename ρ = (C1.rename ρ) ∪ (C2.rename ρ) := by + simp [CaptureSet.union, CaptureSet.rename] + end Capybara diff --git a/Capybara/Syntax/Type/Properties.lean b/Capybara/Syntax/Type/Properties.lean index 656c5c15..7a0242a6 100644 --- a/Capybara/Syntax/Type/Properties.lean +++ b/Capybara/Syntax/Type/Properties.lean @@ -1,6 +1,7 @@ import Capybara.Syntax.CaptureSet import Capybara.Syntax.Type.Renaming import Capybara.Syntax.Type.Weakening +import Capybara.Syntax.Type.Opening namespace Capybara @@ -134,4 +135,8 @@ theorem SType.rename_cweaken {S : SType n m k} : (S.rename ρ).cweaken = S.cweaken.rename ρ.cext := by simp [SType.cweaken, SType.rename_comp, Renaming.comp_cweaken] +theorem CType.copen_rename {T : CType n m (k+1)} : + (T.copen c).rename ρ = (T.rename ρ.cext).copen (ρ.cvar c) := by + simp [CType.copen, CType.rename_comp, Renaming.copen_comp] + end Capybara From 09a5d41d279bb7fd2e2cf26630cd53a4e43f4518 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sat, 1 Feb 2025 19:34:28 +0100 Subject: [PATCH 74/84] proof(rebind): separation, kinding wip --- Capybara/Rebinding/CaptureRoot.lean | 21 +++++++++++---- Capybara/Rebinding/Separation.lean | 33 +++++++++++++++++++++++ Capybara/StaticSemantics/CaptureRoot.lean | 11 ++++++-- Capybara/StaticSemantics/Separation.lean | 10 +++---- 4 files changed, 63 insertions(+), 12 deletions(-) create mode 100644 Capybara/Rebinding/Separation.lean diff --git a/Capybara/Rebinding/CaptureRoot.lean b/Capybara/Rebinding/CaptureRoot.lean index 11e894d7..75a2cdd7 100644 --- a/Capybara/Rebinding/CaptureRoot.lean +++ b/Capybara/Rebinding/CaptureRoot.lean @@ -2,11 +2,11 @@ import Capybara.Morphism.Rebinding import Capybara.StaticSemantics namespace Capybara -def CaptureRoot.rename (r : CaptureRoot k) (f : FinFun k k') : CaptureRoot k' := - match r with - | ⟨m,c⟩ => ⟨m,f c⟩ +/-! +This file proves that rebinding preserves capture root reachability. +-/ -theorem ReachRoot.rename +theorem ReachRoot.rebind (h : ReachRoot Γ C r) (θ : Rebinding Γ Δ) : ReachRoot Δ (C.rename θ.ρ.asCapt) (r.rename θ.ρ.cvar) := by @@ -36,8 +36,19 @@ theorem ReachRoot.rename { repeat rw [<-CaptureSet.qualified_rename] easy } case cvar hb => - simp [CaptureSet.rename, ReachRoot.rename] + simp [CaptureSet.rename] apply cvar have hb' := θ.cvar hb; easy +theorem RORoot.rebind + (h : RORoot Γ r) + (θ : Rebinding Γ Δ) : + RORoot Δ (r.rename θ.ρ.cvar) := by + cases h + case r_ro => + apply r_ro + case r_imm hc => + apply r_imm + have hc' := θ.cvar hc; easy + end Capybara diff --git a/Capybara/Rebinding/Separation.lean b/Capybara/Rebinding/Separation.lean new file mode 100644 index 00000000..f4db6b0f --- /dev/null +++ b/Capybara/Rebinding/Separation.lean @@ -0,0 +1,33 @@ +import Capybara.Morphism.Rebinding +import Capybara.StaticSemantics +import Capybara.Rebinding.CaptureRoot +namespace Capybara + +/-! +This file proves that rebinding preserves separation checking. +-/ + +theorem RootSeparation.rebind + (h : RootSeparation Γ r1 r2) + (θ : Rebinding Γ Δ) : + RootSeparation Δ (r1.rename θ.ρ.cvar) (r2.rename θ.ρ.cvar) := by + induction h + case s_symm ih => apply s_symm; easy + case s_ro => + apply s_ro <;> (apply RORoot.rebind; easy) + case s_rw ih => + simp [CaptureRoot.rename] at * + apply s_rw; easy + case s_sep hb hrea => + rw [CaptureRoot.rename] + apply s_sep + have hb' := θ.cvar hb; easy + apply ReachRoot.rebind hrea + case s_fresh hc1 hc2 hneq => + simp [CaptureRoot.rename] + apply s_fresh + { have hc1' := θ.cvar hc1; easy } + { have hc2' := θ.cvar hc2; easy } + sorry + +end Capybara diff --git a/Capybara/StaticSemantics/CaptureRoot.lean b/Capybara/StaticSemantics/CaptureRoot.lean index 9e82e05e..be149325 100644 --- a/Capybara/StaticSemantics/CaptureRoot.lean +++ b/Capybara/StaticSemantics/CaptureRoot.lean @@ -1,10 +1,17 @@ import Capybara.Syntax namespace Capybara +/-! +A capture root is described by an abstract capture parameter and an access mode. A capture root `m c` being reachable from a capture set `C` means that `C` could access `c` at mode `m`. +-/ structure CaptureRoot (k : Nat) : Type where m : Mode c : Fin k +def CaptureRoot.rename (r : CaptureRoot k) (f : FinFun k k') : CaptureRoot k' := + match r with + | ⟨m,c⟩ => ⟨m,f c⟩ + /-! `ReachRoot Γ C m c` means that the root `c` is reachable at access mode `m` from the capture set `C` under the context `Γ`. -/ @@ -28,9 +35,9 @@ inductive ReachRoot : Context n m k -> CaptureSet n k -> CaptureRoot k -> Prop w ReachRoot Γ ({c@mu:=c}) ⟨mu,c⟩ inductive RORoot : Context n m k -> CaptureRoot k -> Prop where -| ro : +| r_ro : RORoot Γ ⟨ro,c⟩ -| imm : +| r_imm : Context.LookupC Γ c (cparam (CKind.Sep ⟨SepMode.Imm, D⟩)) -> RORoot Γ ⟨Mode.M m,c⟩ diff --git a/Capybara/StaticSemantics/Separation.lean b/Capybara/StaticSemantics/Separation.lean index 1dfc03ae..59c44b02 100644 --- a/Capybara/StaticSemantics/Separation.lean +++ b/Capybara/StaticSemantics/Separation.lean @@ -6,21 +6,21 @@ Separation checking. -/ inductive RootSeparation : Context n m k -> CaptureRoot k -> CaptureRoot k -> Prop where -| symm : +| s_symm : RootSeparation Γ r1 r2 -> RootSeparation Γ r2 r1 -| ro : +| s_ro : RORoot Γ r1 -> RORoot Γ r2 -> RootSeparation Γ r1 r2 -| rw : +| s_rw : RootSeparation Γ ⟨ε,c1⟩ r2 -> RootSeparation Γ ⟨ro,c1⟩ r2 -| sep : +| s_sep : Context.LookupC Γ c (cparam (CKind.Sep ⟨s,D⟩)) -> ReachRoot Γ D r2 -> RootSeparation Γ ⟨ε,c⟩ r2 -| fresh : +| s_fresh : Context.LookupC Γ c1 (cparam CKind.Fresh) -> Context.LookupC Γ c2 (cparam CKind.Fresh) -> (c1 ≠ c2) -> From c640de4caa162a92a8b28812339474f745eca6f7 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sat, 1 Feb 2025 20:18:32 +0100 Subject: [PATCH 75/84] proof(rebind): root separation --- Capybara/Morphism/Rebinding.lean | 42 +++++++++++++++++++++++++ Capybara/Rebinding/Separation.lean | 2 +- Capybara/Syntax/Context/Properties.lean | 25 +++++++++++++++ 3 files changed, 68 insertions(+), 1 deletion(-) diff --git a/Capybara/Morphism/Rebinding.lean b/Capybara/Morphism/Rebinding.lean index 4690f9f9..06d8dee4 100644 --- a/Capybara/Morphism/Rebinding.lean +++ b/Capybara/Morphism/Rebinding.lean @@ -14,6 +14,12 @@ structure Rebinding (Γ : Context n m k) (Δ : Context n' m' k') where var : ∀ {x T}, Γ.Lookup x T -> Δ.Lookup (ρ.var x) (T.rename ρ) tvar : ∀ {X S}, Γ.LookupT X S -> Δ.LookupT (ρ.tvar X) (S.rename ρ) cvar : ∀ {c K}, Γ.LookupC c K -> Δ.LookupC (ρ.cvar c) (K.rename ρ.asCapt) + -- A rebinding is injective on fresh capture variables, as mapping two distinct + -- fresh capture variables to the same variable breaks the separation invariant. + -- This is needed to prove the `s_fresh` case of `RootSeparation.rebind`. + fresh_inj : ∀ {c1 c2}, + Γ.LookupC c1 (CBinding.param CKind.Fresh) -> Γ.LookupC c2 (CBinding.param CKind.Fresh) -> + (c1 ≠ c2) -> (ρ.cvar c1 ≠ ρ.cvar c2) /-! ## Extensions @@ -48,6 +54,11 @@ def Rebinding.ext (θ : Rebinding Γ Δ) : Rebinding (Γ,x:T) (Δ,x:T.rename θ. simp [<-CBinding.rename_weaken] constructor apply θ.cvar; easy + case fresh_inj => + intro c1 c2 hc1 hc2 hneq + have hc1' := Context.var_lookupc_fresh_inv hc1 + have hc2' := Context.var_lookupc_fresh_inv hc2 + apply θ.fresh_inj <;> aesop def Rebinding.text (θ : Rebinding Γ Δ) : Rebinding (Γ,X:B) (Δ,X:B.rename θ.ρ) := by constructor @@ -76,6 +87,11 @@ def Rebinding.text (θ : Rebinding Γ Δ) : Rebinding (Γ,X:B) (Δ,X:B.rename θ simp constructor apply θ.cvar; easy + case fresh_inj => + intro c1 c2 hc1 hc2 hneq + have hc1' := Context.tvar_lookupc_inv hc1 + have hc2' := Context.tvar_lookupc_inv hc2 + apply θ.fresh_inj <;> aesop def Rebinding.cext (θ : Rebinding Γ Δ) : Rebinding (Γ,c:K) (Δ,c:K.rename θ.ρ.asCapt) := by constructor @@ -104,5 +120,31 @@ def Rebinding.cext (θ : Rebinding Γ Δ) : Rebinding (Γ,c:K) (Δ,c:K.rename θ simp [<-CBinding.rename_cweaken] constructor apply θ.cvar; easy + case fresh_inj => + intro c1 c2 hc1 hc2 hneq + have h1 := Context.cvar_lookupc_inv hc1 + have h2 := Context.cvar_lookupc_inv hc2 + match h1, h2 with + | Or.inl ⟨h1,_⟩, Or.inl ⟨h2,_⟩ => aesop + | Or.inl ⟨h1,_⟩, Or.inr ⟨_, _, _, h2, _⟩ => + subst_vars + simp [Renaming.cext, FinFun.ext] + intro h; cases h + | Or.inr ⟨_, _, _, h1, _⟩, Or.inl ⟨h2,_⟩ => + subst_vars + simp [Renaming.cext, FinFun.ext] + intro h; cases h + | Or.inr ⟨c1, b1, hb1, h1, he1⟩, Or.inr ⟨c2, b2, hb2, h2, he2⟩ => + cases h1; cases h2 + cases b1 <;> try cases he1 + rename_i K; cases K <;> cases he1 + cases b2 <;> try cases he2 + rename_i K; cases K <;> cases he2 + simp [Renaming.cext, FinFun.ext] + intro h + apply θ.fresh_inj + exact hb1; exact hb2 + aesop + easy end Capybara diff --git a/Capybara/Rebinding/Separation.lean b/Capybara/Rebinding/Separation.lean index f4db6b0f..f3fe6c07 100644 --- a/Capybara/Rebinding/Separation.lean +++ b/Capybara/Rebinding/Separation.lean @@ -28,6 +28,6 @@ theorem RootSeparation.rebind apply s_fresh { have hc1' := θ.cvar hc1; easy } { have hc2' := θ.cvar hc2; easy } - sorry + apply θ.fresh_inj hc1 hc2 hneq end Capybara diff --git a/Capybara/Syntax/Context/Properties.lean b/Capybara/Syntax/Context/Properties.lean index d25094dd..6ddb1cc8 100644 --- a/Capybara/Syntax/Context/Properties.lean +++ b/Capybara/Syntax/Context/Properties.lean @@ -1,3 +1,4 @@ +import Capless.Tactics import Capybara.Syntax.Context.Core namespace Capybara @@ -71,4 +72,28 @@ theorem CBinding.rename_cweaken {B : CBinding n k} {ρ : Renaming n m k n' m' k' simp [CBinding.cweaken]; simp [CBinding.rename] apply CaptureSet.rename_cweaken +theorem Context.var_lookupc_inv {Γ : Context n m k} + (hb : (Γ,x:T).LookupC c B) : + ∃ B0, Γ.LookupC c B0 ∧ B = B0.weaken := by cases hb; aesop + +theorem Context.var_lookupc_fresh_inv {Γ : Context n m k} + (hb : (Γ,x:T).LookupC c (CBinding.param CKind.Fresh)) : + Γ.LookupC c (CBinding.param CKind.Fresh) := by + have ⟨B0, hb0, heq⟩ := Context.var_lookupc_inv hb + cases B0 <;> try cases heq + rename_i K; cases K <;> try cases heq + easy + +theorem Context.tvar_lookupc_inv {Γ : Context n m k} + (hb : (Γ,X:S).LookupC c B) : + Γ.LookupC c B := by cases hb; aesop + +theorem Context.cvar_lookupc_inv {Γ : Context n m k} + (hb : (Γ,c:K).LookupC c B) : + (c = 0 ∧ B = K.cweaken) ∨ + (∃ c0 B0, Γ.LookupC c0 B0 ∧ c = c0.succ ∧ B = B0.cweaken) := by + cases hb + case here => apply Or.inl; aesop + case cthere hb0 => apply Or.inr; aesop + end Capybara From c2d30ced0c1e86a465322b4cf3584f1b3455b890 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 2 Feb 2025 03:55:40 +0100 Subject: [PATCH 76/84] proof(rebind): separation wip --- Capybara/Rebinding/Separation.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Capybara/Rebinding/Separation.lean b/Capybara/Rebinding/Separation.lean index f3fe6c07..c18786fa 100644 --- a/Capybara/Rebinding/Separation.lean +++ b/Capybara/Rebinding/Separation.lean @@ -30,4 +30,11 @@ theorem RootSeparation.rebind { have hc2' := θ.cvar hc2; easy } apply θ.fresh_inj hc1 hc2 hneq +theorem Separation.rebind + (h : Separation Γ C1 C2) + (θ : Rebinding Γ Δ) : + Separation Δ (C1.rename θ.ρ.asCapt) (C2.rename θ.ρ.asCapt) := by + intro r1 r2 h1 h2 + sorry + end Capybara From f3434c1da9c1481c9bb84c0ba49b67bc474488d8 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 2 Feb 2025 10:56:49 +0100 Subject: [PATCH 77/84] proof(rebind): attempt --- Capybara/Rebinding/CaptureRoot.lean | 34 +++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/Capybara/Rebinding/CaptureRoot.lean b/Capybara/Rebinding/CaptureRoot.lean index 75a2cdd7..83916429 100644 --- a/Capybara/Rebinding/CaptureRoot.lean +++ b/Capybara/Rebinding/CaptureRoot.lean @@ -51,4 +51,38 @@ theorem RORoot.rebind apply r_imm have hc' := θ.cvar hc; easy +theorem ReachRoot.rebind_inv' + (θ : Rebinding Γ Δ) + (he : C0 = C.rename θ.ρ.asCapt) + (h : ReachRoot Δ C0 r) : + ∃ r0, ReachRoot Γ C r0 ∧ r0.rename θ.ρ.cvar = r := by + induction h generalizing C + case union_l ih => + cases C <;> simp [CaptureSet.rename] at he + case union D1 D2 => + have ⟨he, _⟩ := he + have ⟨r0, h0, h1⟩ := ih he + apply Exists.intro r0 + constructor + { apply union_l; easy } + { easy } + case union_r ih => + cases C <;> simp [CaptureSet.rename] at he + case union D1 D2 => + have ⟨_, he⟩ := he + have ⟨r0, h0, h1⟩ := ih he + apply Exists.intro r0 + constructor + { apply union_r; easy } + { easy } + case var => sorry + case cvar_alias => sorry + case cvar => sorry + +theorem ReachRoot.rebind_inv + (θ : Rebinding Γ Δ) + (h : ReachRoot Δ (C.rename θ.ρ.asCapt) r) : + ∃ r0, ReachRoot Γ C r0 ∧ r0.rename θ.ρ.cvar = r := sorry + + end Capybara From 2b9982fd800e4e5d049691319f30d7ee38d8dc3c Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 2 Feb 2025 11:23:17 +0100 Subject: [PATCH 78/84] proof(rebind): make "forall capture root" inductive --- Capybara/Rebinding/CaptureRoot.lean | 48 ++++++++--------------- Capybara/StaticSemantics/CaptureRoot.lean | 21 ++++++++++ 2 files changed, 37 insertions(+), 32 deletions(-) diff --git a/Capybara/Rebinding/CaptureRoot.lean b/Capybara/Rebinding/CaptureRoot.lean index 83916429..64188ec4 100644 --- a/Capybara/Rebinding/CaptureRoot.lean +++ b/Capybara/Rebinding/CaptureRoot.lean @@ -51,38 +51,22 @@ theorem RORoot.rebind apply r_imm have hc' := θ.cvar hc; easy -theorem ReachRoot.rebind_inv' +theorem ForallRoot.rebind {n m k n' m' k'} + {Γ : Context n m k} {Δ : Context n' m' k'} {C : CaptureSet n k} + (P : RootPred k) (Q : RootPred k') + (h : ForallRoot Γ C P) (θ : Rebinding Γ Δ) - (he : C0 = C.rename θ.ρ.asCapt) - (h : ReachRoot Δ C0 r) : - ∃ r0, ReachRoot Γ C r0 ∧ r0.rename θ.ρ.cvar = r := by - induction h generalizing C - case union_l ih => - cases C <;> simp [CaptureSet.rename] at he - case union D1 D2 => - have ⟨he, _⟩ := he - have ⟨r0, h0, h1⟩ := ih he - apply Exists.intro r0 - constructor - { apply union_l; easy } - { easy } - case union_r ih => - cases C <;> simp [CaptureSet.rename] at he - case union D1 D2 => - have ⟨_, he⟩ := he - have ⟨r0, h0, h1⟩ := ih he - apply Exists.intro r0 - constructor - { apply union_r; easy } - { easy } - case var => sorry - case cvar_alias => sorry - case cvar => sorry - -theorem ReachRoot.rebind_inv - (θ : Rebinding Γ Δ) - (h : ReachRoot Δ (C.rename θ.ρ.asCapt) r) : - ∃ r0, ReachRoot Γ C r0 ∧ r0.rename θ.ρ.cvar = r := sorry - + (transport : ∀r, P r -> Q (r.rename θ.ρ.cvar)) : + ForallRoot Δ (C.rename θ.ρ.asCapt) Q := by + induction h + case r_union ih1 ih2 => + rw [CaptureSet.rename_union] + apply r_union <;> aesop + case r_var => sorry + case r_cvar_alias => sorry + case r_cvar hc hp => + apply r_cvar + have hc' := θ.cvar hc; easy + have hp' := transport _ hp; easy end Capybara diff --git a/Capybara/StaticSemantics/CaptureRoot.lean b/Capybara/StaticSemantics/CaptureRoot.lean index be149325..44df99a0 100644 --- a/Capybara/StaticSemantics/CaptureRoot.lean +++ b/Capybara/StaticSemantics/CaptureRoot.lean @@ -41,4 +41,25 @@ inductive RORoot : Context n m k -> CaptureRoot k -> Prop where Context.LookupC Γ c (cparam (CKind.Sep ⟨SepMode.Imm, D⟩)) -> RORoot Γ ⟨Mode.M m,c⟩ +def RootPred (k : Nat) := CaptureRoot k -> Prop + +inductive ForallRoot : Context n m k -> CaptureSet n k -> RootPred k -> Prop where +| r_union : + ForallRoot Γ C1 P -> + ForallRoot Γ C2 P -> + ForallRoot Γ (C1 ∪ C2) P +| r_var : + Context.Lookup Γ x (S^[m]C) -> + ForallRoot Γ ((C.qualified (Mode.M m)).qualified mu) P -> + ForallRoot Γ ({x@mu:=x}) P +| r_cvar_alias : + Context.LookupC Γ c (calias C) -> + ForallRoot Γ (C.qualified mu) P -> + ForallRoot Γ ({c@mu:=c}) P +| r_cvar : + Context.LookupC Γ c (cparam K) -> + (P ⟨mu,c⟩) -> + ForallRoot Γ ({c@mu:=c}) P + + end Capybara From 27b4d8ca2b1301e356c6dce36558a2e03de8faf2 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 3 Feb 2025 10:21:29 +0100 Subject: [PATCH 79/84] proof(bind): "forall capture roots" --- Capybara/Rebinding/CaptureRoot.lean | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/Capybara/Rebinding/CaptureRoot.lean b/Capybara/Rebinding/CaptureRoot.lean index 64188ec4..c194e098 100644 --- a/Capybara/Rebinding/CaptureRoot.lean +++ b/Capybara/Rebinding/CaptureRoot.lean @@ -62,8 +62,18 @@ theorem ForallRoot.rebind {n m k n' m' k'} case r_union ih1 ih2 => rw [CaptureSet.rename_union] apply r_union <;> aesop - case r_var => sorry - case r_cvar_alias => sorry + case r_var hb _ ih => + simp [CaptureSet.rename] + apply r_var + { have hb' := θ.var hb; easy } + { repeat rw [<-CaptureSet.qualified_rename] + apply ih; easy } + case r_cvar_alias hb _ ih => + simp [CaptureSet.rename] + apply r_cvar_alias + { have hb' := θ.cvar hb; easy } + { repeat rw [<-CaptureSet.qualified_rename] + apply ih; easy } case r_cvar hc hp => apply r_cvar have hc' := θ.cvar hc; easy From 357ca7bbfb476cf6cad3844a50235cbd56fe8a76 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 3 Feb 2025 10:29:21 +0100 Subject: [PATCH 80/84] proof(rebind): separation --- Capybara/Rebinding/Separation.lean | 15 +++++++++++++-- Capybara/StaticSemantics/Separation.lean | 4 +++- 2 files changed, 16 insertions(+), 3 deletions(-) diff --git a/Capybara/Rebinding/Separation.lean b/Capybara/Rebinding/Separation.lean index c18786fa..9361c1e0 100644 --- a/Capybara/Rebinding/Separation.lean +++ b/Capybara/Rebinding/Separation.lean @@ -34,7 +34,18 @@ theorem Separation.rebind (h : Separation Γ C1 C2) (θ : Rebinding Γ Δ) : Separation Δ (C1.rename θ.ρ.asCapt) (C2.rename θ.ρ.asCapt) := by - intro r1 r2 h1 h2 - sorry + apply ForallRoot.rebind + (P := λ r1 => ForallRoot Γ C2 (λ r2 => RootSeparation Γ r1 r2)) + (Q := λ r1 => ForallRoot Δ (C2.rename θ.ρ.asCapt) (λ r2 => RootSeparation Δ r1 r2)) + (h := h) + (θ := θ) + intro r1 h' + apply ForallRoot.rebind + (P := λ r2 => RootSeparation Γ r1 r2) + (Q := λ r2 => RootSeparation Δ (r1.rename θ.ρ.cvar) r2) + (h := h') + (θ := θ) + intro r2 h'' + apply RootSeparation.rebind h'' end Capybara diff --git a/Capybara/StaticSemantics/Separation.lean b/Capybara/StaticSemantics/Separation.lean index 59c44b02..87e9a7b3 100644 --- a/Capybara/StaticSemantics/Separation.lean +++ b/Capybara/StaticSemantics/Separation.lean @@ -27,6 +27,8 @@ inductive RootSeparation : Context n m k -> CaptureRoot k -> CaptureRoot k -> Pr RootSeparation Γ ⟨μ1,c1⟩ ⟨μ2,c2⟩ def Separation (Γ : Context n m k) (C1 C2 : CaptureSet n k) : Prop := - ∀r1 r2, ReachRoot Γ C1 r1 -> ReachRoot Γ C2 r2 -> RootSeparation Γ r1 r2 + ForallRoot Γ C1 (λ r1 => + ForallRoot Γ C2 (λ r2 => + RootSeparation Γ r1 r2)) end Capybara From 60f3337ccfc96a75a8d4d6a1e3b1b9e524cb4806 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 3 Feb 2025 10:45:21 +0100 Subject: [PATCH 81/84] proof(rebind): kinding --- Capybara/Rebinding/CaptureRoot.lean | 48 +++++++++++++++++------ Capybara/Rebinding/Kinding.lean | 44 +++++++++++++++++++++ Capybara/StaticSemantics/CaptureRoot.lean | 27 +++++++++---- Capybara/StaticSemantics/Kinding.lean | 5 ++- 4 files changed, 103 insertions(+), 21 deletions(-) diff --git a/Capybara/Rebinding/CaptureRoot.lean b/Capybara/Rebinding/CaptureRoot.lean index c194e098..877323ed 100644 --- a/Capybara/Rebinding/CaptureRoot.lean +++ b/Capybara/Rebinding/CaptureRoot.lean @@ -3,9 +3,12 @@ import Capybara.StaticSemantics namespace Capybara /-! -This file proves that rebinding preserves capture root reachability. +This file proves that rebinding preserves judgements over capture roots. -/ +/-! +Rebinding preserves root reachability (deprecated) +-/ theorem ReachRoot.rebind (h : ReachRoot Γ C r) (θ : Rebinding Γ Δ) : @@ -40,17 +43,9 @@ theorem ReachRoot.rebind apply cvar have hb' := θ.cvar hb; easy -theorem RORoot.rebind - (h : RORoot Γ r) - (θ : Rebinding Γ Δ) : - RORoot Δ (r.rename θ.ρ.cvar) := by - cases h - case r_ro => - apply r_ro - case r_imm hc => - apply r_imm - have hc' := θ.cvar hc; easy - +/-! +Rebinding preserves the "forall roots" judgement. +-/ theorem ForallRoot.rebind {n m k n' m' k'} {Γ : Context n m k} {Δ : Context n' m' k'} {C : CaptureSet n k} (P : RootPred k) (Q : RootPred k') @@ -79,4 +74,33 @@ theorem ForallRoot.rebind {n m k n' m' k'} have hc' := θ.cvar hc; easy have hp' := transport _ hp; easy +/-! +The following three theorems show that rebinding preserves the kinding of capture roots. +-/ +theorem RORoot.rebind + (h : RORoot Γ r) + (θ : Rebinding Γ Δ) : + RORoot Δ (r.rename θ.ρ.cvar) := by + cases h + case r_ro => + apply r_ro + case r_imm hc => + apply r_imm + have hc' := θ.cvar hc; easy +theorem MutRoot.rebind + (h : MutRoot Γ r) + (θ : Rebinding Γ Δ) : + MutRoot Δ (r.rename θ.ρ.cvar) := by + cases h + case r_mut => + apply r_mut +theorem FreshRoot.rebind + (h : FreshRoot Γ r) + (θ : Rebinding Γ Δ) : + FreshRoot Δ (r.rename θ.ρ.cvar) := by + cases h + case r_fresh hc => + apply r_fresh + have hc' := θ.cvar hc; easy + end Capybara diff --git a/Capybara/Rebinding/Kinding.lean b/Capybara/Rebinding/Kinding.lean index 96955b1b..8679cb28 100644 --- a/Capybara/Rebinding/Kinding.lean +++ b/Capybara/Rebinding/Kinding.lean @@ -1,5 +1,49 @@ import Capybara.Morphism.Rebinding import Capybara.StaticSemantics +import Capybara.Rebinding.CaptureRoot +import Capybara.Rebinding.Separation namespace Capybara +/-! +Rebinding preserves the kinding of capture sets. +-/ +theorem Kinding.rebind + (h : Kinding Γ C K) + (θ : Rebinding Γ Δ) : + Kinding Δ (C.rename θ.ρ.asCapt) (K.rename θ.ρ.asCapt) := by + cases h + case fresh hk => + apply fresh + apply ForallRoot.rebind + (P := λ r => FreshRoot Γ r) + (Q := λ r => FreshRoot Δ r) + (θ := θ) + (h := hk) + intros r hf + apply hf.rebind + case sep_imm hs hk => + apply sep_imm + apply Separation.rebind + (h := hs) + (θ := θ) + apply ForallRoot.rebind + (P := λ r => RORoot Γ r) + (Q := λ r => RORoot Δ r) + (θ := θ) + (h := hk) + intros r hr + apply hr.rebind + case sep_mut hs hk => + apply sep_mut + apply Separation.rebind + (h := hs) + (θ := θ) + apply ForallRoot.rebind + (P := λ r => MutRoot Γ r) + (Q := λ r => MutRoot Δ r) + (θ := θ) + (h := hk) + intros r hr + apply hr.rebind + end Capybara diff --git a/Capybara/StaticSemantics/CaptureRoot.lean b/Capybara/StaticSemantics/CaptureRoot.lean index 44df99a0..709970b4 100644 --- a/Capybara/StaticSemantics/CaptureRoot.lean +++ b/Capybara/StaticSemantics/CaptureRoot.lean @@ -34,13 +34,6 @@ inductive ReachRoot : Context n m k -> CaptureSet n k -> CaptureRoot k -> Prop w Context.LookupC Γ c (cparam K) -> ReachRoot Γ ({c@mu:=c}) ⟨mu,c⟩ -inductive RORoot : Context n m k -> CaptureRoot k -> Prop where -| r_ro : - RORoot Γ ⟨ro,c⟩ -| r_imm : - Context.LookupC Γ c (cparam (CKind.Sep ⟨SepMode.Imm, D⟩)) -> - RORoot Γ ⟨Mode.M m,c⟩ - def RootPred (k : Nat) := CaptureRoot k -> Prop inductive ForallRoot : Context n m k -> CaptureSet n k -> RootPred k -> Prop where @@ -61,5 +54,25 @@ inductive ForallRoot : Context n m k -> CaptureSet n k -> RootPred k -> Prop whe (P ⟨mu,c⟩) -> ForallRoot Γ ({c@mu:=c}) P +/-! +The following judgements are predicates on the *kinds* of a capture root. +A capture root can be: +- read-only (`RORoot`), signifying a readonly access; +- mutable (`MutRoot`), signifying a read-write access; +- fresh (`FreshRoot`), signifying a read-write access to root that is known to be fresh. +-/ +inductive RORoot : Context n m k -> CaptureRoot k -> Prop where +| r_ro : + RORoot Γ ⟨ro,c⟩ +| r_imm : + Context.LookupC Γ c (cparam (CKind.Sep ⟨SepMode.Imm, D⟩)) -> + RORoot Γ ⟨Mode.M m,c⟩ +inductive MutRoot : Context n m k -> CaptureRoot k -> Prop where +| r_mut : + MutRoot Γ ⟨Mode.M m,c⟩ +inductive FreshRoot : Context n m k -> CaptureRoot k -> Prop where +| r_fresh : + Context.LookupC Γ c (cparam CKind.Fresh) -> + FreshRoot Γ ⟨Mode.M m,c⟩ end Capybara diff --git a/Capybara/StaticSemantics/Kinding.lean b/Capybara/StaticSemantics/Kinding.lean index 77fdef9b..596f7e05 100644 --- a/Capybara/StaticSemantics/Kinding.lean +++ b/Capybara/StaticSemantics/Kinding.lean @@ -5,14 +5,15 @@ namespace Capybara inductive Kinding : Context n m k -> CaptureSet n k -> CKind n k -> Prop where | fresh : - (∀c m, ReachRoot Γ C ⟨Mode.M m,c⟩ -> Context.LookupC Γ c (cparam CKind.Fresh)) -> + ForallRoot Γ C (λ r => FreshRoot Γ r) -> Kinding Γ C CKind.Fresh | sep_mut : Separation Γ C D -> + ForallRoot Γ C (λ r => MutRoot Γ r) -> Kinding Γ C (CKind.Sep ⟨SepMode.Mut, D⟩) | sep_imm : Separation Γ C D -> - (∀r, ReachRoot Γ C r -> RORoot Γ r) -> + ForallRoot Γ C (λ r => RORoot Γ r) -> Kinding Γ C (CKind.Sep ⟨SepMode.Imm, D⟩) end Capybara From effa18439efc2f3ef7c392d2815392a4efcd2ddb Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 3 Feb 2025 10:49:35 +0100 Subject: [PATCH 82/84] proof(def): reformulate chaining with ForallRoot --- Capybara/StaticSemantics/Chaining.lean | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/Capybara/StaticSemantics/Chaining.lean b/Capybara/StaticSemantics/Chaining.lean index b574bdf3..7bff4171 100644 --- a/Capybara/StaticSemantics/Chaining.lean +++ b/Capybara/StaticSemantics/Chaining.lean @@ -6,12 +6,30 @@ namespace Capybara Specifically, anything that has been dropped from `C1` cannot be mentioned by `C2` any more. -/ + +inductive RootChaining : Context n m k -> CaptureRoot k -> CaptureRoot k -> Prop +| c_rw : + RootChaining Γ ⟨Mode.M m1, c1⟩ r2 +| c_drop : + (c1 ≠ c2) -> + RootChaining Γ ⟨drop,c1⟩ ⟨m,c2⟩ + def Chaining (Γ : Context n m k) (C1 C2 : CaptureSet n k) : Prop := - ∀c, ReachRoot Γ C1 ⟨drop,c⟩ -> ∀m, ReachRoot Γ C2 ⟨m,c⟩ -> False + ForallRoot Γ C1 (λ r1 => + ForallRoot Γ C2 (λ r2 => + RootChaining Γ r1 r2)) + +inductive DroppedRootChaining : Context n m k -> CaptureRoot k -> CaptureRoot k -> Prop +| c_chain : + (c1 ≠ c2) -> + DroppedRootChaining Γ ⟨m1,c1⟩ ⟨m2,c2⟩ def DroppedChaining (Γ : Context n m k) (C1 C2 : CaptureSet n k) : Prop := - ∀μ c, ReachRoot Γ C1 ⟨μ,c⟩ -> ∀m, ReachRoot Γ C2 ⟨m,c⟩ -> False + ForallRoot Γ C1 (λ r1 => + ForallRoot Γ C2 (λ r2 => + DroppedRootChaining Γ r1 r2)) notation:50 Γ " ⊢ " C1 " >> " C2 => CaptureSet.Chaining Γ C1 C2 +notation:50 Γ " ⊢ " C1 " drop>> " C2 => CaptureSet.DroppedChaining Γ C1 C2 end Capybara From 30821411d116aceb4d2aed73a14f4d640afe5e7f Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 3 Feb 2025 13:12:24 +0100 Subject: [PATCH 83/84] proof(rebind): wip --- Capybara/StaticSemantics/Chaining.lean | 2 ++ Capybara/Syntax/Context/Properties.lean | 36 +++++++++++++++++++++++++ 2 files changed, 38 insertions(+) diff --git a/Capybara/StaticSemantics/Chaining.lean b/Capybara/StaticSemantics/Chaining.lean index 7bff4171..f38b38a8 100644 --- a/Capybara/StaticSemantics/Chaining.lean +++ b/Capybara/StaticSemantics/Chaining.lean @@ -11,6 +11,7 @@ inductive RootChaining : Context n m k -> CaptureRoot k -> CaptureRoot k -> Prop | c_rw : RootChaining Γ ⟨Mode.M m1, c1⟩ r2 | c_drop : + Γ.LookupC c1 (cparam CKind.Fresh) -> (c1 ≠ c2) -> RootChaining Γ ⟨drop,c1⟩ ⟨m,c2⟩ @@ -21,6 +22,7 @@ def Chaining (Γ : Context n m k) (C1 C2 : CaptureSet n k) : Prop := inductive DroppedRootChaining : Context n m k -> CaptureRoot k -> CaptureRoot k -> Prop | c_chain : + Γ.LookupC c1 (cparam CKind.Fresh) -> (c1 ≠ c2) -> DroppedRootChaining Γ ⟨m1,c1⟩ ⟨m2,c2⟩ diff --git a/Capybara/Syntax/Context/Properties.lean b/Capybara/Syntax/Context/Properties.lean index 6ddb1cc8..bf4b7dd9 100644 --- a/Capybara/Syntax/Context/Properties.lean +++ b/Capybara/Syntax/Context/Properties.lean @@ -96,4 +96,40 @@ theorem Context.cvar_lookupc_inv {Γ : Context n m k} case here => apply Or.inl; aesop case cthere hb0 => apply Or.inr; aesop +theorem Context.lookupc_complete {Γ : Context n m k} {c : Fin k} : + ∃ B, Γ.LookupC c B := by + induction Γ + case empty => apply Fin.elim0 c + case cons Γ0 P ih => + have ⟨B0,ih⟩ := ih (c:=c) + apply Exists.intro B0.weaken + constructor; easy + case tcons Γ0 P ih => + have ⟨B0,ih⟩ := ih (c:=c) + apply Exists.intro B0 + constructor; easy + case ccons Γ0 P ih => + cases c using Fin.cases + case zero => + apply Exists.intro P.cweaken + constructor + case succ c0 => + have ⟨B0,ih⟩ := ih (c:=c0) + apply Exists.intro B0.cweaken + constructor; easy + +theorem Context.lookupc_functional {Γ : Context n m k} {c : Fin k} + (h1 : Γ.LookupC c B1) (h2 : Γ.LookupC c B2) : B1 = B2 := by + induction h1 + case here => cases h2; rfl + case there ih => + cases h2; rename_i h2 + have ih := ih h2 + aesop + case tthere ih => + cases h2; rename_i h2 + have ih := ih h2 + aesop + case cthere ih => sorry + end Capybara From 9d436f9d3e9d6d1cfd1cfaa7bd369e526267cfbc Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 3 Feb 2025 13:12:33 +0100 Subject: [PATCH 84/84] proof(rebind): chaining --- Capybara/Rebinding/Chaining.lean | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 Capybara/Rebinding/Chaining.lean diff --git a/Capybara/Rebinding/Chaining.lean b/Capybara/Rebinding/Chaining.lean new file mode 100644 index 00000000..af4eb4d0 --- /dev/null +++ b/Capybara/Rebinding/Chaining.lean @@ -0,0 +1,27 @@ +import Capybara.Morphism.Rebinding +import Capybara.StaticSemantics +import Capybara.Rebinding.CaptureRoot +namespace Capybara + +theorem RootChaining.rebind + (h : RootChaining Γ r1 r2) + (θ : Rebinding Γ Δ) : + RootChaining Δ (r1.rename θ.ρ.cvar) (r2.rename θ.ρ.cvar) := by + cases h + case c_rw => apply c_rw + case c_drop hc => + apply c_drop + have hc' := θ.cvar hc + easy + sorry + +/-! +Rebinding preserves the chaining of capture sets. +-/ +theorem Chaining.rebind + (h : Chaining Γ C1 C2) + (θ : Rebinding Γ Δ) : + Chaining Δ (C1.rename θ.ρ.asCapt) (C2.rename θ.ρ.asCapt) := by + sorry + +end Capybara