|
| 1 | +-- SPDX-License-Identifier: MPL-2.0 |
| 2 | +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | +-- |
| 4 | +-- The QTT substitution lemma + preservation for the my-lang Solo core |
| 5 | +-- (Idris2 twin of the F1.4 section of SoloCore.v). Phase F1.4, Idris track. |
| 6 | +-- |
| 7 | +-- This is the proof of `preservation` (Soundness.idr states it as the hole |
| 8 | +-- `?todo_preservation`). It rests on the standard open-context substitution |
| 9 | +-- lemma `htSubst`: substitution under binders shifts the substituted |
| 10 | +-- variable's index, so the lemma is generalised over a type-context prefix |
| 11 | +-- `I` (the binders crossed so far). The reduction rules only ever do |
| 12 | +-- `subst0` (one variable) and `subst2` (two), but the under-binder induction |
| 13 | +-- needs the general form. |
| 14 | +-- |
| 15 | +-- Layers (mirroring the Coq twin): |
| 16 | +-- 4a append-context algebra (tappend/uappend + injectivity/split) [VERIFIED] |
| 17 | +-- 4b shape + shift (shapeType [VERIFIED]; hvShift/htShift/ |
| 18 | +-- htShift0/weakeningAppend — PENDING) |
| 19 | +-- 4c substitution core (reassoc algebra, hvSubst, htSubst, |
| 20 | +-- substLemma0, subst2Lemma — PENDING) |
| 21 | +-- 4d preservation (consumes 4c; congruences recurse on Step |
| 22 | +-- — PENDING; Soundness.preservation stays |
| 23 | +-- the honest hole until 4d lands) |
| 24 | +-- |
| 25 | +-- STATUS (Idris track, #108): this module is HOLE-FREE for the layers it |
| 26 | +-- currently contains (4a + the shape invariant). It does NOT yet prove |
| 27 | +-- preservation. The remaining layers each thread the type context (and term) |
| 28 | +-- RELEVANTLY because Idris erases the indices of `Has`/`HasVar` (ADR-003) — |
| 29 | +-- the same wall the `progress` proof navigated with explicit-term recursion. |
| 30 | +-- That makes the Idris port heavier than the Coq original (whose `Prop` |
| 31 | +-- indices erase without blocking the proofs), but the technique is settled |
| 32 | +-- (see `shapeType`/`shapeVar` below): pass `g`/`t` explicitly, recurse on the |
| 33 | +-- non-binding premise so erased branch-binder types are never demanded. |
| 34 | + |
| 35 | +module Substitution |
| 36 | + |
| 37 | +import Quantity |
| 38 | +import EchoMode |
| 39 | +import Syntax |
| 40 | +import Context |
| 41 | +import Typing |
| 42 | +import Soundness |
| 43 | +import Data.Nat |
| 44 | + |
| 45 | +%default total |
| 46 | + |
| 47 | +------------------------------------------------------------ |
| 48 | +-- local disjointness / injectivity helpers |
| 49 | +------------------------------------------------------------ |
| 50 | +-- (Context.idr's equivalents are not exported; restate locally.) |
| 51 | + |
| 52 | +justInj' : Just x = Just y -> x = y |
| 53 | +justInj' Refl = Refl |
| 54 | + |
| 55 | +nothingNotJust' : Nothing = Just x -> Void |
| 56 | +nothingNotJust' Refl impossible |
| 57 | + |
| 58 | +usnocNotUEmpty' : USnoc d q = UEmpty -> Void |
| 59 | +usnocNotUEmpty' Refl impossible |
| 60 | + |
| 61 | +predEq' : S n = S m -> n = m |
| 62 | +predEq' Refl = Refl |
| 63 | + |
| 64 | +sNotZ' : S n = Z -> Void |
| 65 | +sNotZ' Refl impossible |
| 66 | + |
| 67 | +zNotS' : Z = S n -> Void |
| 68 | +zNotS' Refl impossible |
| 69 | + |
| 70 | +------------------------------------------------------------ |
| 71 | +-- 4a. Append-context algebra |
| 72 | +------------------------------------------------------------ |
| 73 | + |
| 74 | +||| Append type contexts: `tappend G I` places `I`'s binders on top of `G`. |
| 75 | +public export |
| 76 | +tappend : Tctx -> Tctx -> Tctx |
| 77 | +tappend g TEmpty = g |
| 78 | +tappend g (TSnoc i a) = TSnoc (tappend g i) a |
| 79 | + |
| 80 | +||| Append usage vectors, shape-matched to `tappend`. |
| 81 | +public export |
| 82 | +uappend : Uvec -> Uvec -> Uvec |
| 83 | +uappend d UEmpty = d |
| 84 | +uappend d (USnoc e q) = USnoc (uappend d e) q |
| 85 | + |
| 86 | +public export |
| 87 | +tappendLen : (g, i : Tctx) -> tlen (tappend g i) = tlen g + tlen i |
| 88 | +tappendLen g TEmpty = rewrite plusZeroRightNeutral (tlen g) in Refl |
| 89 | +tappendLen g (TSnoc i a) = |
| 90 | + rewrite tappendLen g i in rewrite plusSuccRightSucc (tlen g) (tlen i) in Refl |
| 91 | + |
| 92 | +public export |
| 93 | +uappendLen : (d, e : Uvec) -> ulen (uappend d e) = ulen d + ulen e |
| 94 | +uappendLen d UEmpty = rewrite plusZeroRightNeutral (ulen d) in Refl |
| 95 | +uappendLen d (USnoc e q) = |
| 96 | + rewrite uappendLen d e in rewrite plusSuccRightSucc (ulen d) (ulen e) in Refl |
| 97 | + |
| 98 | +public export |
| 99 | +uzeroTappend : (g, i : Tctx) -> uzero (tappend g i) = uappend (uzero g) (uzero i) |
| 100 | +uzeroTappend g TEmpty = Refl |
| 101 | +uzeroTappend g (TSnoc i a) = rewrite uzeroTappend g i in Refl |
| 102 | + |
| 103 | +public export |
| 104 | +uscaleUappend : (q : Q) -> (d, e : Uvec) |
| 105 | + -> uscale q (uappend d e) = uappend (uscale q d) (uscale q e) |
| 106 | +uscaleUappend q d UEmpty = Refl |
| 107 | +uscaleUappend q d (USnoc e qe) = rewrite uscaleUappend q d e in Refl |
| 108 | + |
| 109 | +||| Add appended vectors componentwise (forward direction). |
| 110 | +public export |
| 111 | +uaddUappend : (ai, bi, ci, ag, bg, cg : Uvec) |
| 112 | + -> uadd ai bi = Just ci -> uadd ag bg = Just cg |
| 113 | + -> uadd (uappend ag ai) (uappend bg bi) = Just (uappend cg ci) |
| 114 | +uaddUappend UEmpty UEmpty ci ag bg cg hi hg = |
| 115 | + rewrite sym (justInj' hi) in hg |
| 116 | +uaddUappend UEmpty (USnoc _ _) _ _ _ _ hi _ = void (nothingNotJust' hi) |
| 117 | +uaddUappend (USnoc _ _) UEmpty _ _ _ _ hi _ = void (nothingNotJust' hi) |
| 118 | +uaddUappend (USnoc ai qa) (USnoc bi qb) ci ag bg cg hi hg with (uadd ai bi) proof p |
| 119 | + uaddUappend (USnoc ai qa) (USnoc bi qb) ci ag bg cg hi hg | Nothing = |
| 120 | + void (nothingNotJust' hi) |
| 121 | + uaddUappend (USnoc ai qa) (USnoc bi qb) ci ag bg cg hi hg | Just cii = |
| 122 | + rewrite uaddUappend ai bi cii ag bg cg p hg in |
| 123 | + rewrite sym (justInj' hi) in Refl |
| 124 | + |
| 125 | +usnocInj : USnoc x p = USnoc y q -> (x = y, p = q) |
| 126 | +usnocInj Refl = (Refl, Refl) |
| 127 | + |
| 128 | +||| uappend injectivity, given the low parts have matching length. |
| 129 | +public export |
| 130 | +uappendInj : (e, f, d1, d2 : Uvec) -> ulen e = ulen f |
| 131 | + -> uappend d1 e = uappend d2 f -> (d1 = d2, e = f) |
| 132 | +uappendInj UEmpty UEmpty d1 d2 _ heq = (heq, Refl) |
| 133 | +uappendInj UEmpty (USnoc _ _) _ _ hlen _ = void (zNotS' hlen) |
| 134 | +uappendInj (USnoc _ _) UEmpty _ _ hlen _ = void (sNotZ' hlen) |
| 135 | +uappendInj (USnoc e qe) (USnoc f qf) d1 d2 hlen heq = |
| 136 | + let (hbody, hq) = usnocInj heq |
| 137 | + (hd, he) = uappendInj e f d1 d2 (predEq' hlen) hbody |
| 138 | + in (hd, rewrite he in rewrite hq in Refl) |
| 139 | + |
| 140 | +||| Split a usage vector by a target low-length `m`. |
| 141 | +public export |
| 142 | +uappendSplit : (m : Nat) -> (d : Uvec) -> LTE m (ulen d) |
| 143 | + -> (dhi : Uvec ** dlo : Uvec ** (d = uappend dhi dlo, ulen dlo = m)) |
| 144 | +uappendSplit Z d _ = (d ** UEmpty ** (Refl, Refl)) |
| 145 | +uappendSplit (S m) UEmpty lte = absurd lte |
| 146 | +uappendSplit (S m) (USnoc d q) lte = |
| 147 | + let (dhi ** dlo ** (heq, hlen)) = uappendSplit m d (fromLteSucc lte) in |
| 148 | + (dhi ** USnoc dlo q ** (rewrite heq in Refl, cong S hlen)) |
| 149 | + |
| 150 | +||| Inverse of `uaddUappend`: a sum of appends (with matching low-lengths) |
| 151 | +||| splits back into a sum of the highs and a sum of the lows. |
| 152 | +public export |
| 153 | +uaddUappendInv : (ai, bi, ag, bg, c : Uvec) -> ulen ai = ulen bi |
| 154 | + -> uadd (uappend ag ai) (uappend bg bi) = Just c |
| 155 | + -> (cg : Uvec ** ci : Uvec ** |
| 156 | + (c = uappend cg ci, uadd ag bg = Just cg, uadd ai bi = Just ci)) |
| 157 | +uaddUappendInv UEmpty UEmpty ag bg c _ h = (c ** UEmpty ** (Refl, h, Refl)) |
| 158 | +uaddUappendInv UEmpty (USnoc _ _) _ _ _ hlen _ = void (zNotS' hlen) |
| 159 | +uaddUappendInv (USnoc _ _) UEmpty _ _ _ hlen _ = void (sNotZ' hlen) |
| 160 | +uaddUappendInv (USnoc ai qa) (USnoc bi qb) ag bg c hlen h |
| 161 | + with (uadd (uappend ag ai) (uappend bg bi)) proof p |
| 162 | + uaddUappendInv (USnoc ai qa) (USnoc bi qb) ag bg c hlen h | Nothing = |
| 163 | + void (nothingNotJust' h) |
| 164 | + uaddUappendInv (USnoc ai qa) (USnoc bi qb) ag bg c hlen h | Just d = |
| 165 | + let (cg ** ci ** (heq, hg, hi)) = uaddUappendInv ai bi ag bg d (predEq' hlen) p in |
| 166 | + (cg ** USnoc ci (qAdd qa qb) ** |
| 167 | + (rewrite sym (justInj' h) in rewrite heq in Refl, |
| 168 | + hg, |
| 169 | + rewrite hi in Refl)) |
| 170 | + |
| 171 | +||| Split a sum-of-appends at the boundary (low parts matched by length). |
| 172 | +public export |
| 173 | +uaddSplitBoundary : (dg1, di1, dg2, di2, dg, di : Uvec) |
| 174 | + -> ulen di1 = ulen di2 -> ulen di = ulen di1 |
| 175 | + -> uadd (uappend dg1 di1) (uappend dg2 di2) = Just (uappend dg di) |
| 176 | + -> (uadd dg1 dg2 = Just dg, uadd di1 di2 = Just di) |
| 177 | +uaddSplitBoundary dg1 di1 dg2 di2 dg di h12 hd heq = |
| 178 | + let (cg ** ci ** (hap, hg, hi)) = |
| 179 | + uaddUappendInv di1 di2 dg1 dg2 (uappend dg di) h12 heq |
| 180 | + (hdg, hdi) = uappendInj di ci dg cg |
| 181 | + (rewrite hd in sym (uaddLen di1 di2 ci hi)) hap |
| 182 | + in (rewrite hdg in hg, rewrite hdi in hi) |
| 183 | + |
| 184 | +------------------------------------------------------------ |
| 185 | +-- 4b. Shape invariant + shift / weakening |
| 186 | +------------------------------------------------------------ |
| 187 | + |
| 188 | +-- The type context `g` (and, for `shapeType`, the term `t`) are passed |
| 189 | +-- EXPLICITLY/relevantly: Idris erases the indices of `HasVar`/`Has`, so the |
| 190 | +-- `THUnit` case (which needs `uzeroLen g`) and the binder cases (which need |
| 191 | +-- the Lam annotation for the extended context) cannot recover them from the |
| 192 | +-- erased derivation. The term drives the recursion; for every BINDING rule |
| 193 | +-- except `THLam` we recurse only on the non-binding premise, so the erased |
| 194 | +-- branch-binder types are never needed. |
| 195 | + |
| 196 | +||| A variable lookup's usage has the same length as its type context. |
| 197 | +public export |
| 198 | +shapeVar : (g : Tctx) -> HasVar g d n a -> ulen d = tlen g |
| 199 | +shapeVar (TSnoc g a) HVHere = cong S (uzeroLen g) |
| 200 | +shapeVar (TSnoc g b) (HVThere hv) = cong S (shapeVar g hv) |
| 201 | + |
| 202 | +||| Every derivation's usage has the length of its type context. The |
| 203 | +||| separated-context invariant that the split/scale algebra relies on. |
| 204 | +public export |
| 205 | +shapeType : (g : Tctx) -> (t : Tm) -> Has g d t a -> ulen d = tlen g |
| 206 | +shapeType g (Var n) (THVar hv) = shapeVar g hv |
| 207 | +shapeType g UnitT THUnit = uzeroLen g |
| 208 | +shapeType g (Lam q a body) (THLam bodyD) = predEq' (shapeType (TSnoc g a) body bodyD) |
| 209 | +shapeType g (App t1 t2) (THApp d1 d2 q h1 h2 prf) = trans (uaddLen d1 (uscale q d2) _ prf) (shapeType g t1 h1) |
| 210 | +shapeType g (With t1 t2) (THWith h1 h2) = shapeType g t1 h1 |
| 211 | +shapeType g (Fst t1) (THFst h) = shapeType g t1 h |
| 212 | +shapeType g (Snd t1) (THSnd h) = shapeType g t1 h |
| 213 | +shapeType g (Tensor t1 t2) (THTensor d1 d2 h1 h2 prf) = trans (uaddLen d1 d2 _ prf) (shapeType g t1 h1) |
| 214 | +shapeType g (LetPair t1 t2)(THLetPair d1 d2 h1 hb prf)= trans (uaddLen d1 d2 _ prf) (shapeType g t1 h1) |
| 215 | +shapeType g (Inl b t1) (THInl h) = shapeType g t1 h |
| 216 | +shapeType g (Inr a t1) (THInr h) = shapeType g t1 h |
| 217 | +shapeType g (Case t tL tR) (THCase d1 d2 h hL hR prf) = trans (uaddLen d1 d2 _ prf) (shapeType g t h) |
| 218 | +shapeType g (Let q t1 t2) (THLet d1 d2 _ h1 h2 prf) = |
| 219 | + trans (uaddLen (uscale q d1) d2 _ prf) (trans (uscaleLen q d1) (shapeType g t1 h1)) |
| 220 | +shapeType g (MkEcho m a b t1) (THEcho h) = shapeType g t1 h |
| 221 | +shapeType g (Weaken t1) (THWeaken h) = shapeType g t1 h |
0 commit comments