From c641e267241dd43949985dc0af1697a66f77b25a Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 13:49:21 +0000 Subject: [PATCH 1/3] =?UTF-8?q?proof(solo-core/idris):=20htSubst=20COMPLET?= =?UTF-8?q?E=20=E2=80=94=20all=205=20usage-splitting=20cases=20(toward=20#?= =?UTF-8?q?108)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The QTT substitution lemma htSubst is now fully proved (all 15 cases, total, hole-free) on the Idris track, mirroring Coq ht_subst. The 5 usage-splitting cases land via the accounting algebra: - Tensor / LetPair / Case : usplit3 (USnoc-boundary split) x2 -> uaddSplitBoundary2 -> recurse -> substReassocMult -> uaddUappend - App / Let : the q-scaled variants via substReassocAdd + uscaleUappend (Let also needs uaddComm/qAddComm for the d1-scaled shape) - binder cases (LetPair/Case/Let) recurse with the prefix I extended and the body usage reshaped (USnoc..); Case unifies the two branch residuals (justInj' on the shared d2 split). Build green 8/8; the ONLY remaining hole in the whole solo-core is ?todo_preservation. Next: substLemma0 + subst2Lemma (corollaries) then the Step-induction closes preservation. --- .../idris/solo-core/Substitution.idr | 86 +++++++++++++++++-- 1 file changed, 81 insertions(+), 5 deletions(-) diff --git a/proofs/verification/idris/solo-core/Substitution.idr b/proofs/verification/idris/solo-core/Substitution.idr index c684860..b4b738a 100644 --- a/proofs/verification/idris/solo-core/Substitution.idr +++ b/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,16 +805,77 @@ 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)) From 9c574690e2df7abdbb93072cf0b97ab07ef7a7a2 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 13:54:20 +0000 Subject: [PATCH 2/3] =?UTF-8?q?proof(solo-core/idris):=20substLemma0=20?= =?UTF-8?q?=E2=80=94=20subst0=20corollary=20of=20htSubst=20(toward=20#108)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit substLemma0 = htSubst at the empty prefix (I = TEmpty): substitute the single top-of-context variable once, the workhorse the reduction rules S_App / S_CaseL / S_CaseR / S_Let consume. One-liner over the now-complete htSubst; build green. Layer 4c (the QTT substitution lemma) is now: htSubst COMPLETE (15/15) + substLemma0. Remaining for preservation (4d): uaddAssoc -> subst2Lemma (the two-variable LetPair substitution), then the Step-induction. --- .../verification/idris/solo-core/Substitution.idr | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/proofs/verification/idris/solo-core/Substitution.idr b/proofs/verification/idris/solo-core/Substitution.idr index b4b738a..a41b392 100644 --- a/proofs/verification/idris/solo-core/Substitution.idr +++ b/proofs/verification/idris/solo-core/Substitution.idr @@ -882,3 +882,18 @@ htSubst (MkEcho m aE bE t1) i g a dg q di du u hlen (THEcho h) hu = 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 From 25a4f8b8915754efa0ecb47aff0d23b5b319ee93 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 13:55:05 +0000 Subject: [PATCH 3/3] =?UTF-8?q?docs(proofs):=20update=20STATUS=20registry?= =?UTF-8?q?=20=E2=80=94=20htSubst=20complete=20+=20substLemma0=20(Idris=20?= =?UTF-8?q?#108)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Idris preservation row: foundation -> htSubst COMPLETE (15/15, b-erasure resolved) + substLemma0; only ?todo_preservation remains; subst2Lemma (via uaddAssoc) + the Step-induction are the documented remainder. --- proofs/STATUS.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/STATUS.md b/proofs/STATUS.md index c3687f7..f434066 100644 --- a/proofs/STATUS.md +++ b/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. |