add first draft of an explanation of the substitutions

Author: meditans

UnderstandingSubstitutions.agda

@@ -0,0 +1,135 @@
+module UnderstandingSubstitutions where
+
+open import Study
+open HSub
+
+-- Here I will do a personal rewrite of Conor's hereditary substitution, to
+-- understand it better.
+
+--------------------------------------------------------------------------------
+-- Weakening substitutions
+--------------------------------------------------------------------------------
+-- Crucially, φ indicates which iz of the jz occur in the source term. So the
+-- point here is that all the variables in iz are added to the passive variables
+-- while the active variables remain the same, and passive and active are
+-- similarly extended. Also the partition is updated to note that all the iz
+-- have gone in the passive variables. The other significant change is that all
+-- the images have been thinned to account for the fact that they are throwing
+-- away the things in jz (that they don't need).
+wkHSub' : ∀ {I}{D : I → Desc I}{src trg bnd iz jz}
+        → HSub D src trg bnd
+        → iz <= jz
+        → HSub D (src ++ iz) (trg ++ jz) bnd
+wkHSub' {iz = iz} {jz = jz} h φ =
+  record
+    { pass    = pass h ++ iz
+    ; act     = act h
+    ; passive = passive h <++= oi {kz = iz}
+    ; active  = active  h <++= oe {kz = iz}
+    ; parti   = bindPassive iz
+    ; passTrg = passTrg h <++= φ
+    ; actBnd  = actBnd h
+    ; images  = all (thin/ (oi <++= oe {kz = jz})) (images h)
+    }
+  where
+    -- bindPassive extends the partition with a cs' for each variable in iz
+    -- (because they are active)
+    bindPassive : forall iz -> Cover ff (passive h <++= oi {kz = iz}) (active h <++= oe {kz = iz})
+    bindPassive B0       = parti h
+    bindPassive (iz - _) = bindPassive iz cs'
+
+--------------------------------------------------------------------------------
+-- Whittling them down
+--------------------------------------------------------------------------------
+mutual
+  -- The type of this is fairly straightforward, and the implementation
+  -- essentially uses selPart'
+  selHSub' :  forall {I}{D : I -> Desc I}{src src' trg bnd}
+           -> src <= src' -> HSub D src' trg bnd -> HSub D src trg bnd
+  selHSub' ψ s with selPart' ψ (parti s)
+  selHSub' ψ s | iz , jz , th , ph , ps0 , ps1 , c
+    = record
+        { pass    = iz
+        ; act     = jz
+        ; passive = th
+        ; active  = ph
+        ; parti   = c
+        ; passTrg = ps0 <&= passTrg s
+        ; actBnd  = ps1 <&= actBnd s
+        ; images  = ps1 <?= images s
+        }
+
+  -- A bit difficult to read here because Sg is the paper's internal notation
+  -- for Σ, but the gist of it is that if I give you a kz <= kz' and a
+  -- partitioning of kz' in th' and ph', then I can give you a partitioning of
+  -- kz, just "reading" the corresponding choices in kz'. This function, in
+  -- retrospective, is obvious.
+  selPart' : forall {K}{iz' jz' kz kz' : Bwd K}{th' : iz' <= kz'}{ph' : jz' <= kz'}
+             (ps : kz <= kz')
+             -> Cover ff th' ph'
+             -> Sg _ \ iz
+             -> Sg _ \ jz
+             -> Sg (iz <= kz) \ th
+             -> Sg (jz <= kz) \ ph
+             -> Sg (iz <= iz') \ ps0
+             -> Sg (jz <= jz') \ ps1
+             -> Cover ff th ph
+           -- ps o' means that the new element is not in kz, the cover specifies where it was in kz'
+  selPart' (ps o') (c' c's) = let ! ! ! ! ps0 , ps1 , c = selPart' ps c' in ! ! ! ! ps0 , ps1 o' , c
+  selPart' (ps o') (c' cs') = let ! ! ! ! ps0 , ps1 , c = selPart' ps c' in ! ! ! ! ps0 o' , ps1 , c
+  selPart' (ps o') (_css {both = ()} _)
+  selPart' (ps os) (c' c's) = let ! ! ! ! ps0 , ps1 , c = selPart' ps c' in ! ! ! ! ps0 , ps1 os , c c's
+  selPart' (ps os) (c' cs') = let ! ! ! ! ps0 , ps1 , c = selPart' ps c' in ! ! ! ! ps0 os , ps1 , c cs'
+  selPart' (ps os) (_css {both = ()} _)
+  selPart' oz czz = ! ! ! ! oz , oz , czz
+
+--------------------------------------------------------------------------------
+-- allLeft
+--------------------------------------------------------------------------------
+-- If the right part of a partition is empty, then the left must be full. The
+-- proof is simple induction.
+allLeft' : forall {K}{iz kz : Bwd K}{ov}{th : iz <= kz}{ph : B0 <= kz} -> Cover ov th ph -> iz == kz
+allLeft' czz                        = refl
+allLeft' (c cs') rewrite allLeft' c = refl
+
+--------------------------------------------------------------------------------
+-- The main functions
+--------------------------------------------------------------------------------
+
+-- hSub is the main operation on terms: given a substitution between contexts,
+-- and a term, it applies the substitution. Let's notice here that the term uses
+-- all his variables in a relevant way, while the resulting term may not use all
+-- of them.
+hSub'    : forall {I D src trg bnd}{i : I}
+         -> HSub D src trg bnd -> TmR D i src -> TmR D i / trg
+-- This function is used to apply a substitution to a description in the
+-- co-de-Bruijn syntax.
+hSubs'   : forall {I D src trg bnd}(S : Desc I)
+         -> HSub D src trg bnd -> [! S !! TmR D !]R src -> [! S !! TmR D !]R / trg
+-- This is the lifted version of the preceding function: the source term doesn't
+-- need to use all the variables in src.
+hSubs/'  : forall {I D src trg bnd}(S : Desc I)
+         -> HSub D src trg bnd -> [! S !! TmR D !]R / src -> [! S !! TmR D !]R / trg
+-- This is to substitute the variable hereditarily: it is the part that
+-- explicitly involves the spine construction
+hered'   : forall {I D jz trg bnd}{i : I}
+         -> (jz !- TmR D i) / trg -> B0 - (jz => i) <= bnd -> [! SpD jz !! TmR D !]R / trg -> TmR D i / trg
+
+-- We can have two constructs here: a syntax construct or a variable. In the
+-- first case, we will continue substituting into the structure. In the second
+-- case, we have to understand whether the variable we're talking about is
+-- passive or active, so we pattern match on selHSub', with a first argument,
+-- th, which has been refined enough to admit only one variable (the other
+-- argument is of course the substitution). We also compute the substitution in
+-- the spine, via hSubs/'. Next, if the variable is passive, we just return the
+-- variable with the new computed interpretation of the spine, while if the
+-- variable is active, we substitute hereditarily using the image.
+hSub' {D = D}{i = i} h [ ts ] = map/ [_] (hSubs' (D i) h ts)
+hSub' h (# {jz} (pair (only ^ th) ts _)) with selHSub' th h | hSubs/' (SpD jz) h ts
+... | record { parti = _css {both = ()} _ }                        | ts'
+... | record { parti = czz cs' ; passTrg = ph }                    | ts' = map/ # (vaR ph ,R ts')
+... | record { parti = czz c's ; actBnd = th' ; images = B0 - im } | ts' = hered im th' ts'
+
+hSubs'   = {!!}
+hSubs/'  = {!!}
+hered'   = {!!}