From 9ba1b22eb33293f76b9a1bfddb160f45e2de20c9 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 30 Sep 2024 17:39:31 +0100 Subject: [PATCH 1/3] add OmniMap --- Capless/Basic.lean | 14 ++++++++++++++ Capless/CaptureSet.lean | 8 ++++++++ Capless/Term.lean | 17 +++++++++++++++++ Capless/Type/Renaming.lean | 19 +++++++++++++++++++ 4 files changed, 58 insertions(+) diff --git a/Capless/Basic.lean b/Capless/Basic.lean index 0e883dcf..b323d953 100644 --- a/Capless/Basic.lean +++ b/Capless/Basic.lean @@ -74,4 +74,18 @@ theorem FinFun.comp_succ {f : FinFun n n'}: Fin.succ ∘ f = (FinFun.ext f) ∘ case succ n => simp [FinFun.ext] +structure OmniMap (n m k n' m' k' : Nat) where + map : FinFun n n' + tmap : FinFun m m' + cmap : FinFun k k' + +def OmniMap.ext (f : OmniMap n m k n' m' k') : OmniMap (n+1) m k (n'+1) m' k' := + { map := f.map.ext, tmap := f.tmap, cmap := f.cmap } + +def OmniMap.text (f : OmniMap n m k n' m' k') : OmniMap n (m+1) k n' (m'+1) k' := + { map := f.map, tmap := f.tmap.ext, cmap := f.cmap } + +def OmniMap.cext (f : OmniMap n m k n' m' k') : OmniMap n m (k+1) n' m' (k'+1) := + { map := f.map, tmap := f.tmap, cmap := f.cmap.ext } + end Capless diff --git a/Capless/CaptureSet.lean b/Capless/CaptureSet.lean index 327647f3..a0125a06 100644 --- a/Capless/CaptureSet.lean +++ b/Capless/CaptureSet.lean @@ -62,6 +62,14 @@ def CaptureSet.crename (C : CaptureSet n k) (f : FinFun k k') : CaptureSet n k' | singleton x => {x=x} | csingleton c => {c=f c} +@[simp] +def CaptureSet.orename (C : CaptureSet n k) (f : OmniMap n m k n' m' k') : CaptureSet n' k' := + match C with + | empty => empty + | union C1 C2 => (C1.orename f) ∪ (C2.orename f) + | singleton x => {x=f.map x} + | csingleton c => {c=f.cmap c} + def CaptureSet.weaken (C : CaptureSet n k) : CaptureSet (n+1) k := C.rename FinFun.weaken diff --git a/Capless/Term.lean b/Capless/Term.lean index 455f0953..5f692260 100644 --- a/Capless/Term.lean +++ b/Capless/Term.lean @@ -86,6 +86,23 @@ def Term.crename (t : Term n m k) (f : FinFun k k') : Term n m k' := | Term.bindc c t => Term.bindc (c.crename f) (t.crename f.ext) | Term.unbox c x => Term.unbox (c.crename f) x +def Term.orename (t : Term n m k) (f : OmniMap n m k n' m' k') : Term n' m' k' := + match t with + | Term.var x => Term.var (f.map x) + | Term.lam E t => Term.lam (E.orename f) (t.orename f.ext) + | Term.tlam S t => Term.tlam (S.orename f) (t.orename f.text) + | Term.clam t => Term.clam (t.orename f.cext) + | Term.boxed x => Term.boxed (f.map x) + | Term.pack C x => Term.pack (C.orename f) (f.map x) + | Term.app x y => Term.app (f.map x) (f.map y) + | Term.tapp x X => Term.tapp (f.map x) (f.tmap X) + | Term.capp x c => Term.capp (f.map x) (f.cmap c) + | Term.letin t u => Term.letin (t.orename f) (u.orename f.ext) + | Term.letex t u => Term.letex (t.orename f) (u.orename f.ext.cext) + | Term.bindt S t => Term.bindt (S.orename f) (t.orename f.text) + | Term.bindc c t => Term.bindc (c.orename f) (t.orename f.cext) + | Term.unbox c x => Term.unbox (c.orename f) (f.map x) + theorem IsValue.rename_l' {t : Term n m k} {t0 : Term n' m k} (he : t0 = t.rename f) (hv : t0.IsValue) : diff --git a/Capless/Type/Renaming.lean b/Capless/Type/Renaming.lean index f8eaf393..e9305126 100644 --- a/Capless/Type/Renaming.lean +++ b/Capless/Type/Renaming.lean @@ -60,6 +60,25 @@ def SType.crename : SType n m k -> FinFun k k' -> SType n m k' end +mutual + +def EType.orename : EType n m k -> OmniMap n m k n' m' k' -> EType n' m' k' +| EType.ex T, f => EType.ex (T.orename f.cext) +| EType.type T, f => EType.type (T.orename f) + +def CType.orename : CType n m k -> OmniMap n m k n' m' k' -> CType n' m' k' +| CType.capt C S, f => CType.capt (C.orename f) (S.orename f) + +def SType.orename : SType n m k -> OmniMap n m k n' m' k' -> SType n' m' k' +| SType.top, _ => SType.top +| SType.tvar X, f => SType.tvar (f.tmap X) +| SType.forall E1 E2, f => SType.forall (E1.orename f) (E2.orename f.ext) +| SType.tforall S E, f => SType.tforall (S.orename f) (E.orename f.text) +| SType.cforall E, f => SType.cforall (E.orename f.cext) +| SType.box T, f => SType.box (T.orename f) + +end + def EType.weaken (E : EType n m k) : EType (n+1) m k := E.rename FinFun.weaken From 56ce515d67712092661a5ec092043665baeb7175 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 30 Sep 2024 17:42:21 +0100 Subject: [PATCH 2/3] add OmniSubst --- Capless/Subst/Basic.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/Capless/Subst/Basic.lean b/Capless/Subst/Basic.lean index a91f4929..fd078f5f 100644 --- a/Capless/Subst/Basic.lean +++ b/Capless/Subst/Basic.lean @@ -649,4 +649,17 @@ def CVarSubst.instantiate {Γ : Context n m k} : constructor trivial +structure OmniSubst + (Γ : Context n m k) + (f : OmniMap n m k n' m' k') + (Δ : Context n' m' k') where + map : ∀ x E, Γ.Bound x E -> Typed Δ (Term.var (f.map x)) (EType.type (E.orename f)) {x=f.map x} + tmap : ∀ X S, Γ.TBound X (TBinding.bound S) -> + SSubtyp Δ (SType.tvar (f.tmap X)) (S.orename f) + tmap_inst : ∀ X S, Γ.TBound X (TBinding.inst S) -> + Δ.TBound (f.tmap X) (TBinding.inst (S.orename f)) + cmap : ∀ c C, + Γ.CBound c (CBinding.inst C) -> + Δ.CBound (f.cmap c) (CBinding.inst (C.orename f)) + end Capless From dfdcfd4d7387e900a62327f0e48d25f71ca4e045 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 2 Oct 2024 01:22:07 +0200 Subject: [PATCH 3/3] proof sketch --- Capless/Subst/Basic.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/Capless/Subst/Basic.lean b/Capless/Subst/Basic.lean index fd078f5f..3434b984 100644 --- a/Capless/Subst/Basic.lean +++ b/Capless/Subst/Basic.lean @@ -662,4 +662,18 @@ structure OmniSubst Γ.CBound c (CBinding.inst C) -> Δ.CBound (f.cmap c) (CBinding.inst (C.orename f)) +def OmniSubst.ext {Γ : Context n m k} + (σ : OmniSubst Γ f Δ) + (T : CType n m k) : + OmniSubst (Γ.var T) f.ext (Δ.var (T.orename f)) := by + constructor + case map => + intro x E hb + cases hb + case here => sorry + case there_var => sorry + case tmap => sorry + case tmap_inst => sorry + case cmap => sorry + end Capless