Idris htSubst COMPLETE (all 15 cases) + substLemma0 — substitution layer of #108

proofs/STATUS.md

@@ -61,7 +61,7 @@ Last verified: 2026-06-14.
 | `progress` | Coq `solo-core/SoloCore` | **machine-checked** | `Theorem progress : Progress.` real `Qed`, axiom-free. Phase F1.3. CI: `proofs.yml` compiles it + asserts `Print Assumptions` closed. |
 | `progress` | Idris2 `solo-core/Soundness` | **locally-checked** | Hole-free total function (no `?todo_progress`); accepted by `idris2`, package built in CI (`proofs.yml`). Phase F1.3. **Re-proven over the SEPARATED context (`Tctx`/`Uvec`) + both products (`TWith`/`TTensor`, `LetPair`) in the 2026-06-15 F1.4 design migration** — closed-term inversions now massage only the usage vector (`uaddEmpty`/`uscaleEmpty`), since the shared type context stays `TEmpty` automatically; `:total progress` confirms totality. |
 | `preservation` | Coq `solo-core/SoloCore` | **machine-checked** | `Theorem preservation : Preservation.`, real `Qed`, axiom-free, via the open-context QTT substitution lemma `ht_subst`. Phase F1.4. CI: `proofs.yml` compiles it + asserts `Print Assumptions` closed (and likewise `affine_pres`). |
-| `preservation` | Idris2 `solo-core/Soundness` | **statement-only** | `?todo_preservation`, **now stated over the CORRECT design** (separated context + genuine products). The OLD Idris design (split-intro `Pair` + project-elim `Fst`/`Snd`) made the same-usage statement UNSOUND (issue #93); the 2026-06-15 migration makes it provable. Proof obligation = Phase F1.4 (Idris track), #108 — the QTT substitution lemma (`htSubst` + `subst2Lemma`) lands in a companion `Substitution.idr` and is wired in here once discharged. NOT described as proved. **Foundation landed (2026-06-15): `Substitution.idr` (in the ipkg, hole-free) carries the append-context algebra (`tappend`/`uappend` + injectivity/split/boundary lemmas) and the shape invariant (`shapeVar`/`shapeType`), all `idris2 --build`-checked. The shift/subst/preservation layers thread `g`/`t` RELEVANTLY around Idris's index erasure (ADR-003) — heavier than the Coq original; PENDING.** |
+| `preservation` | Idris2 `solo-core/Soundness` | **statement-only** | `?todo_preservation`, **now stated over the CORRECT design** (separated context + genuine products). The OLD Idris design (split-intro `Pair` + project-elim `Fst`/`Snd`) made the same-usage statement UNSOUND (issue #93); the 2026-06-15 migration makes it provable. Proof obligation = Phase F1.4 (Idris track), #108 — the QTT substitution lemma (`htSubst` + `subst2Lemma`) lands in a companion `Substitution.idr` and is wired in here once discharged. NOT described as proved. **Progress (2026-06-19): `Substitution.idr` (in the ipkg) now carries the append-context algebra, the shape invariant (`shapeVar`/`shapeType`), `hvShift`/`htShift` (term weakening, all 14 cases), the substitution accounting algebra (`qReassoc`/`vecReassoc`/`substReassocAdd`/`substReassocMult`/`usplit3`/`uaddSplitBoundary2`), `hvSubst`, the FULL `htSubst` (the QTT substitution lemma — all 15 cases, total, hole-free), and `substLemma0` (the `subst0` corollary). The `b`-index-erasure obstruction (ADR-003) is resolved by carrying `b` as an erased implicit in `hvSubst`/`htSubst`. `idris2 --build` exits 0; the ONLY remaining hole in the whole solo-core is `?todo_preservation`. REMAINING for `preservation`: `uaddAssoc` -> `subst2Lemma` (two-variable LetPair substitution) -> the `Step`-induction. PENDING (still NOT proved).** |
 | Small-step `step` | Coq `solo-core/SoloCore` | **definitions-only** | CBV left-to-right relation, all redex + congruence constructors. Committed in F1.1. |
 | Small-step `Step` | Idris2 `solo-core/Soundness` | **definitions-only** | CBV left-to-right relation, both products: additive `SFst`/`SSnd` fire on `With` values, multiplicative `SLetPair` fires on a `Tensor` value via `subst2`; plus the echo residue rules (`SWeaken`). Consumed by the verified `progress`. Migrated 2026-06-15. |
 | General core typing + substitution | Coq `coq/Typing.v` | **locally-checked** | Pre-existing: 9 `Qed`, 0 `Admitted`. Non-quantitative; substitution lemma proved. |

proofs/verification/idris/solo-core/Substitution.idr

@@ -779,7 +779,22 @@ htSubst (Lam q' tyL t1) i g a dg q di du u hlen (THLam bodyD) hu =
   let (dgr ** (hadd, hht)) =
         htSubst t1 (TSnoc i tyL) g a dg q (USnoc di q') du u (cong S hlen) bodyD hu
   in (dgr ** (hadd, THLam hht))
-htSubst (App t1 t2) i g a dg q di du u hlen (THApp d1 d2 q' h1 h2 prf) hu = ?htSubst_app
+htSubst (App t1 t2) i g a dg q di du u hlen (THApp d1 d2 q' h1 h2 prf) hu =
+  let (dg1 ** q1 ** di1 ** (Refl, l1)) = usplit3 d1 (tlen g) (tlen i)
+        (trans (shapeType (tappend (TSnoc g a) i) t1 h1) (tappendLen (TSnoc g a) i))
+      (dg2 ** q2 ** di2 ** (Refl, l2)) = usplit3 d2 (tlen g) (tlen i)
+        (trans (shapeType (tappend (TSnoc g a) i) t2 h2) (tappendLen (TSnoc g a) i))
+      (hGadd, hqeq, hIadd) =
+        uaddSplitBoundary2 dg1 q1 di1 (uscale q' dg2) (qMul q' q2) (uscale q' di2) dg q di
+          (trans l1 (sym (trans (uscaleLen q' di2) l2))) (trans hlen (sym l1))
+          (rewrite sym (uscaleUappend q' (USnoc dg2 q2) di2) in prf)
+      (dgr1 ** (hr1, hht1)) = htSubst t1 i g a dg1 q1 di1 du u l1 h1 hu
+      (dgr2 ** (hr2, hht2)) = htSubst t2 i g a dg2 q2 di2 du u l2 h2 hu
+      (dgr ** (hDgr, hcomb)) = substReassocAdd dg1 dgr1 dg2 dgr2 dg du q' q1 q2 hr1 hr2 hGadd
+  in (dgr ** (rewrite hqeq in hDgr,
+              THApp (uappend dgr1 di1) (uappend dgr2 di2) q' hht1 hht2
+                (rewrite uscaleUappend q' dgr2 di2 in
+                   uaddUappend di1 (uscale q' di2) di dgr1 (uscale q' dgr2) dgr hIadd hcomb)))
 htSubst (With t1 t2) i g a dg q di du u hlen (THWith h1 h2) hu =
   let (dgr1 ** (hr1, hht1)) = htSubst t1 i g a dg q di du u hlen h1 hu
       (dgr2 ** (hr2, hht2)) = htSubst t2 i g a dg q di du u hlen h2 hu
@@ -790,19 +805,95 @@ htSubst (Fst t1) i g a dg q di du u hlen (THFst h) hu =
 htSubst (Snd t1) i g a dg q di du u hlen (THSnd h) hu =
   let (dgr ** (hr, hht)) = htSubst t1 i g a dg q di du u hlen h hu
   in (dgr ** (hr, THSnd hht))
-htSubst (Tensor t1 t2) i g a dg q di du u hlen (THTensor d1 d2 h1 h2 prf) hu = ?htSubst_tensor
-htSubst (LetPair t1 t2) i g a dg q di du u hlen (THLetPair d1 d2 aa bb h1 hb prf) hu = ?htSubst_letpair
+htSubst (Tensor t1 t2) i g a dg q di du u hlen (THTensor d1 d2 h1 h2 prf) hu =
+  let (dg1 ** q1 ** di1 ** (Refl, l1)) = usplit3 d1 (tlen g) (tlen i)
+        (trans (shapeType (tappend (TSnoc g a) i) t1 h1) (tappendLen (TSnoc g a) i))
+      (dg2 ** q2 ** di2 ** (Refl, l2)) = usplit3 d2 (tlen g) (tlen i)
+        (trans (shapeType (tappend (TSnoc g a) i) t2 h2) (tappendLen (TSnoc g a) i))
+      (hGadd, hqeq, hIadd) = uaddSplitBoundary2 dg1 q1 di1 dg2 q2 di2 dg q di
+                               (trans l1 (sym l2)) (trans hlen (sym l1)) prf
+      (dgr1 ** (hr1, hht1)) = htSubst t1 i g a dg1 q1 di1 du u l1 h1 hu
+      (dgr2 ** (hr2, hht2)) = htSubst t2 i g a dg2 q2 di2 du u l2 h2 hu
+      (dgr ** (hDgr, hcomb)) = substReassocMult dg1 dgr1 dg2 dgr2 dg du q1 q2 hr1 hr2 hGadd
+  in (dgr ** (rewrite hqeq in hDgr,
+              THTensor (uappend dgr1 di1) (uappend dgr2 di2) hht1 hht2
+                (uaddUappend di1 di2 di dgr1 dgr2 dgr hIadd hcomb)))
+htSubst (LetPair t1 t2) i g a dg q di du u hlen (THLetPair d1 d2 aa bb h1 hb prf) hu =
+  let (dg1 ** q1 ** di1 ** (Refl, l1)) = usplit3 d1 (tlen g) (tlen i)
+        (trans (shapeType (tappend (TSnoc g a) i) t1 h1) (tappendLen (TSnoc g a) i))
+      (dg2 ** q2 ** di2 ** (Refl, l2)) = usplit3 d2 (tlen g) (tlen i)
+        (trans (predEq' (predEq'
+                 (shapeType (TSnoc (TSnoc (tappend (TSnoc g a) i) aa) bb) t2 hb)))
+               (tappendLen (TSnoc g a) i))
+      (hGadd, hqeq, hIadd) = uaddSplitBoundary2 dg1 q1 di1 dg2 q2 di2 dg q di
+                               (trans l1 (sym l2)) (trans hlen (sym l1)) prf
+      (dgr1 ** (hr1, hht1)) = htSubst t1 i g a dg1 q1 di1 du u l1 h1 hu
+      (dgr2 ** (hr2, hht2)) = htSubst t2 (TSnoc (TSnoc i aa) bb) g a dg2 q2
+                                (USnoc (USnoc di2 One) One) du u (cong S (cong S l2)) hb hu
+      (dgr ** (hDgr, hcomb)) = substReassocMult dg1 dgr1 dg2 dgr2 dg du q1 q2 hr1 hr2 hGadd
+  in (dgr ** (rewrite hqeq in hDgr,
+              THLetPair (uappend dgr1 di1) (uappend dgr2 di2) aa bb hht1 hht2
+                (uaddUappend di1 di2 di dgr1 dgr2 dgr hIadd hcomb)))
 htSubst (Inl b0 t1) i g a dg q di du u hlen (THInl h) hu =
   let (dgr ** (hr, hht)) = htSubst t1 i g a dg q di du u hlen h hu
   in (dgr ** (hr, THInl hht))
 htSubst (Inr a0 t1) i g a dg q di du u hlen (THInr h) hu =
   let (dgr ** (hr, hht)) = htSubst t1 i g a dg q di du u hlen h hu
   in (dgr ** (hr, THInr hht))
-htSubst (Case t1 tL tR) i g a dg q di du u hlen (THCase d1 d2 aa bb h hL hR prf) hu = ?htSubst_case
-htSubst (Let q' t1 t2) i g a dg q di du u hlen (THLet d1 d2 _ aa h1 h2 prf) hu = ?htSubst_let
+htSubst (Case t1 tL tR) i g a dg q di du u hlen (THCase d1 d2 aa bb h hL hR prf) hu =
+  let (dg1 ** q1 ** di1 ** (Refl, l1)) = usplit3 d1 (tlen g) (tlen i)
+        (trans (shapeType (tappend (TSnoc g a) i) t1 h) (tappendLen (TSnoc g a) i))
+      (dg2 ** q2 ** di2 ** (Refl, l2)) = usplit3 d2 (tlen g) (tlen i)
+        (trans (predEq' (shapeType (TSnoc (tappend (TSnoc g a) i) aa) tL hL))
+               (tappendLen (TSnoc g a) i))
+      (hGadd, hqeq, hIadd) = uaddSplitBoundary2 dg1 q1 di1 dg2 q2 di2 dg q di
+                               (trans l1 (sym l2)) (trans hlen (sym l1)) prf
+      (dgr1 ** (hr1, hht1))  = htSubst t1 i g a dg1 q1 di1 du u l1 h hu
+      (dgr2 ** (hr2, hhtL))  = htSubst tL (TSnoc i aa) g a dg2 q2 (USnoc di2 One) du u (cong S l2) hL hu
+      (dgr2' ** (hr2', hhtR)) = htSubst tR (TSnoc i bb) g a dg2 q2 (USnoc di2 One) du u (cong S l2) hR hu
+      (dgr ** (hDgr, hcomb)) = substReassocMult dg1 dgr1 dg2 dgr2 dg du q1 q2 hr1 hr2 hGadd
+  in (dgr ** (rewrite hqeq in hDgr,
+              THCase (uappend dgr1 di1) (uappend dgr2 di2) aa bb hht1 hhtL
+                (rewrite justInj' (trans (sym hr2) hr2') in hhtR)
+                (uaddUappend di1 di2 di dgr1 dgr2 dgr hIadd hcomb)))
+htSubst (Let q' t1 t2) i g a dg q di du u hlen (THLet d1 d2 _ aa h1 h2 prf) hu =
+  let (dg1 ** q1 ** di1 ** (Refl, l1)) = usplit3 d1 (tlen g) (tlen i)
+        (trans (shapeType (tappend (TSnoc g a) i) t1 h1) (tappendLen (TSnoc g a) i))
+      (dg2 ** q2 ** di2 ** (Refl, l2)) = usplit3 d2 (tlen g) (tlen i)
+        (trans (predEq' (shapeType (TSnoc (tappend (TSnoc g a) i) aa) t2 h2))
+               (tappendLen (TSnoc g a) i))
+      (hGadd, hqeq, hIadd) =
+        uaddSplitBoundary2 (uscale q' dg1) (qMul q' q1) (uscale q' di1) dg2 q2 di2 dg q di
+          (trans (uscaleLen q' di1) (trans l1 (sym l2)))
+          (trans hlen (sym (trans (uscaleLen q' di1) l1)))
+          (rewrite sym (uscaleUappend q' (USnoc dg1 q1) di1) in prf)
+      (dgr1 ** (hr1, hht1)) = htSubst t1 i g a dg1 q1 di1 du u l1 h1 hu
+      (dgr2 ** (hr2, hht2)) = htSubst t2 (TSnoc i aa) g a dg2 q2 (USnoc di2 q') du u (cong S l2) h2 hu
+      (dgr ** (hDgr, hcomb)) = substReassocAdd dg2 dgr2 dg1 dgr1 dg du q' q2 q1 hr2 hr1
+                                 (trans (uaddComm dg2 (uscale q' dg1)) hGadd)
+  in (dgr ** (rewrite hqeq in rewrite qAddComm (qMul q' q1) q2 in hDgr,
+              THLet (uappend dgr1 di1) (uappend dgr2 di2) q' aa hht1 hht2
+                (rewrite uscaleUappend q' dgr1 di1 in
+                   uaddUappend (uscale q' di1) di2 di (uscale q' dgr1) dgr2 dgr hIadd
+                     (trans (uaddComm (uscale q' dgr1) dgr2) hcomb))))
 htSubst (MkEcho m aE bE t1) i g a dg q di du u hlen (THEcho h) hu =
   let (dgr ** (hr, hht)) = htSubst t1 i g a dg q di du u hlen h hu
   in (dgr ** (hr, THEcho hht))
 htSubst (Weaken t1) i g a dg q di du u hlen (THWeaken h) hu =
   let (dgr ** (hr, hht)) = htSubst t1 i g a dg q di du u hlen h hu
   in (dgr ** (hr, THWeaken hht))
+
+------------------------------------------------------------
+-- 4c (cont). Operational corollaries of htSubst
+------------------------------------------------------------
+
+||| `subst0` corollary — `htSubst` at the empty prefix `I = TEmpty`: substitute
+||| the single top-of-context variable once. (Mirrors Coq `subst_lemma0`.)
+||| The reduction rules `S_App` / `S_CaseL` / `S_CaseR` / `S_Let` consume this.
+public export
+substLemma0 : (g : Tctx) -> (a : Ty) -> (dg : Uvec) -> (q : Q) -> (t : Tm)
+           -> (du : Uvec) -> (u : Tm)
+           -> Has (TSnoc g a) (USnoc dg q) t b
+           -> Has g du u a
+           -> (dgr : Uvec ** (uadd dg (uscale q du) = Just dgr, Has g dgr (subst0 u t) b))
+substLemma0 g a dg q t du u ht hu = htSubst t TEmpty g a dg q UEmpty du u Refl ht hu