Skip to content

Omni substitution theorems #10

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Linyxus wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Omni substitution theorems #10

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
9ba1b22
add OmniMap
Linyxus Sep 30, 2024
56ce515
add OmniSubst
Linyxus Sep 30, 2024
dfdcfd4
proof sketch
Linyxus Oct 1, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 14 additions & 0 deletions Capless/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
8 changes: 8 additions & 0 deletions Capless/CaptureSet.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
27 changes: 27 additions & 0 deletions Capless/Subst/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -649,4 +649,31 @@ 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))

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
17 changes: 17 additions & 0 deletions Capless/Term.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) :
Expand Down
19 changes: 19 additions & 0 deletions Capless/Type/Renaming.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down