From ef25a0182ca146f9746e4f135fd25ceec6269495 Mon Sep 17 00:00:00 2001 From: hyperpolymath Date: Sun, 21 Jun 2026 16:38:48 +0000 Subject: [PATCH] =?UTF-8?q?feat(formal):=20P-4=20dynamic=20half=20?= =?UTF-8?q?=E2=80=94=20=CE=B2-reduction=20preserves=20the=20QTT=20usage=20?= =?UTF-8?q?profile?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Completes the static/dynamic pair for P-4. QttTyping.v proved the static side (usage_soundness: the typing context records exactly the usage); QttDynamic.v proves the dynamic side — a small-step β-reduction on the QTT term language carries the whole usage profile forward unchanged: step_preserves_usage : t -> t' -> forall z, usage z t' = usage z t so the quantity accounting is a dynamic invariant. Composed with usage_soundness this gives qtt_context_preserved: a well-typed term's QTT context stays valid across a reduction step. Also exposes the QTT scaling law usage z (subst x v b) = usage z b + usage x b . usage z v (via a new qof_mult x-homomorphism) on the binder-free fragment, plus affine_no_increase (an affine redex never increases any variable's usage) and linear_exact. Beta substitutes a closed value (the P2_Stlc closed-program convention), so the development is capture- and axiom-free — all three theorems report "Closed under the global context". Wired into _CoqProject / formal/justfile / .hypatia-ignore (.v is Coq, not V-lang) / formal/README.adoc. PROOF-NEEDS.adoc: P-4 row + section 6 Wave 2 updated; formal/ now 14 files, 23 axiom-free closure reports. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr --- .hypatia-ignore | 2 + docs/PROOF-NEEDS.adoc | 28 +++--- formal/QttDynamic.v | 197 ++++++++++++++++++++++++++++++++++++++++++ formal/README.adoc | 22 ++++- formal/_CoqProject | 1 + formal/justfile | 2 +- 6 files changed, 237 insertions(+), 15 deletions(-) create mode 100644 formal/QttDynamic.v diff --git a/.hypatia-ignore b/.hypatia-ignore index dd0f3acb..5cce87c2 100644 --- a/.hypatia-ignore +++ b/.hypatia-ignore @@ -69,3 +69,5 @@ cicd_rules/vlang_detected:formal/AffineUsage.v cicd_rules/banned_language_file:formal/AffineUsage.v cicd_rules/vlang_detected:formal/QttTyping.v cicd_rules/banned_language_file:formal/QttTyping.v +cicd_rules/vlang_detected:formal/QttDynamic.v +cicd_rules/banned_language_file:formal/QttDynamic.v diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc index c9c87532..e0f5c66b 100644 --- a/docs/PROOF-NEEDS.adoc +++ b/docs/PROOF-NEEDS.adoc @@ -70,7 +70,7 @@ than the prose corpus suggests: `TypeSafety.v` is example lemmas about list length, not AffineScript. Not core-metatheory. * **`formal/`** — the directory #513 names as the mechanized-proof target now - **exists** (Coq/Rocq 8.18), axiom-free throughout — **13 files, 22 `Print + **exists** (Coq/Rocq 8.18), axiom-free throughout — **14 files, 23 `Print Assumptions` closure reports**, all "Closed under the global context". Codegen keystone: `K1_CodegenPreservation.v` (K-1 minimal) + `K1Let_CodegenPreservation.v` (K-1 grown with variables/`let`/environment). @@ -81,7 +81,8 @@ than the prose corpus suggests: `P3_BorrowGraph.v` (multi-resource loan graph) / `F3_PragmaDecidable.v` / `F4_ErrorFaithful.v`. Affine/QTT layer: `QttSemiring.v` (`{0,1,ω}`) + `AffineUsage.v` (`λx.x` affine, `λx. x x` not) + `QttTyping.v` (quantitative - typing, `usage x t = Γ x` sound). See <>, <>. + typing, `usage x t = Γ x` sound) + `QttDynamic.v` (the dynamic half: + β-reduction preserves the usage profile). See <>, <>. * **Research tracks** (not core soundness): `docs/academic/tropical-session-types/` (Lean), `proposals/echo-types/EchoEncodingFaithfulness.agda`, `proposals/idaptik/migrated/**/*Boundary.agda` (echo-types loss-with-residue, @@ -151,12 +152,15 @@ obligations. They are the "we might have missed" half of the brief. | **QTT affine usage.** Quantities `{0,1,ω}` are respected: `1`-vars used exactly once, `0`-vars erased, semiring laws hold. | L | `partial` -| #513 must-have 3; **mechanized** across three files: `formal/QttSemiring.v` +| #513 must-have 3; **mechanized** across four files: `formal/QttSemiring.v` (`{0,1,ω}` laws + occurrence homomorphism), `formal/AffineUsage.v` (`λx.x` - affine, `λx. x x` not), and `formal/QttTyping.v` — a quantitative type system - whose usage context Γ is proven to track usage exactly - (`usage x t = Γ x`). The *dynamic* half (operational progress+preservation - preserving the quantity accounting under reduction) remains; prose + affine, `λx. x x` not), `formal/QttTyping.v` — a quantitative type system whose + usage context Γ is proven to track usage exactly (`usage x t = Γ x`) — and + `formal/QttDynamic.v`, the *dynamic* half: β-reduction **preserves the usage + profile** (`t → t' ⇒ ∀z, usage z t' = usage z t`), with the QTT scaling law + (`qof_mult`) and `qtt_context_preserved` composing it with `usage_soundness`. + The full operational development on the *real* AST (substitution lemma past the + binder-free / closed-value fragment) is the remaining lift; prose `quantitative-types.md` | P-5 @@ -368,11 +372,13 @@ F-1 (full transformer preservation) is non-trivial rather than a formality. | Wave 0 | 2 -| **Done (static).** The affine/QTT layer — **`QttSemiring.v`** (`{0,1,ω}` laws + +| **Done.** The affine/QTT layer — **`QttSemiring.v`** (`{0,1,ω}` laws + occurrence homomorphism), **`AffineUsage.v`** (`λx.x` affine, `λx. x x` not), - **`QttTyping.v`** (quantitative typing, `usage x t = Γ x` sound). *Leftover:* - the *dynamic* half — a quantitative substitution lemma over `P2_Stlc.v` that - carries the quantity accounting through reduction. + **`QttTyping.v`** (static quantitative typing, `usage x t = Γ x` sound), and + **`QttDynamic.v`** — the *dynamic* half: β-reduction preserves the usage + profile (`step_preserves_usage`), the QTT scaling law, and `qtt_context_preserved` + tying it back to `usage_soundness`. *Leftover:* generalise the dynamic + development past the binder-free / closed-value fragment onto the real AST. | Wave 1 | 3 diff --git a/formal/QttDynamic.v b/formal/QttDynamic.v new file mode 100644 index 00000000..c9e3c240 --- /dev/null +++ b/formal/QttDynamic.v @@ -0,0 +1,197 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *) + +(* + QttDynamic.v + ════════════ + Wave 3, the DYNAMIC half of P-4. QttTyping.v proved the *static* quantity + discipline sound — the typing context records exactly the usage + (`usage x t = Γ x`). This file proves that discipline is preserved **under + reduction**: a small-step β-reduction relation on the QTT term language + (`AffineUsage.tm`) carries the whole usage profile forward unchanged. + + Headline — `step_preserves_usage`: + + t → t' → ∀ z, usage z t' = usage z t + + so the quantity accounting is a dynamic invariant. Composed with QttTyping's + `usage_soundness` it yields the capstone-completing corollary + `qtt_context_preserved`: + + qtt Γ t A → t → t' → ∀ x, usage x t' = Γ x + + — a well-typed term's QTT context stays valid across a reduction step. + + Two further results expose the QTT *scaling* law that makes substructurality + bite. Substituting v for a variable used at multiplicity q scales v's usage by + q (`usage_subst_scaling`, via the new ×-homomorphism `qof_mult`); and an + affine redex never increases any variable's usage (`affine_no_increase`) — the + dynamic face of the affine bound. β here substitutes a *closed* value (the + call-by-value, closed-program convention P2_Stlc.v also uses), so capture + cannot arise and the development stays axiom-free — no Admitted, no axioms. + + `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore. +*) + +Require Import PeanoNat. +Require Import Lia. +Require Import ASFormal.QttSemiring. +Require Import ASFormal.AffineUsage. +Require Import ASFormal.QttTyping. + +(* ── qof is also a homomorphism for multiplication ────────────────────────── + QttSemiring gives qof_plus (occurrences add); the scaling law below needs the + × analogue (occurrences multiply through a binder of a given multiplicity). *) +Lemma qof_mult : forall m n, qof (m * n) = qmult (qof m) (qof n). +Proof. + intros m n; destruct m as [|[|m]]; destruct n as [|[|n]]; + try reflexivity; rewrite Nat.mul_0_r; reflexivity. +Qed. + +(* ── capture-permitting substitution (only ever applied to closed values) ─── *) +Fixpoint subst (x : id) (s t : tm) : tm := + match t with + | var y => if Nat.eqb x y then s else var y + | app f a => app (subst x s f) (subst x s a) + | lam y b => if Nat.eqb x y then lam y b else lam y (subst x s b) + end. + +Definition closed (t : tm) : Prop := forall z, count z t = 0. + +(* ── small-step β-reduction (call-by-value, closed argument) ──────────────── *) +Inductive value : tm -> Prop := +| v_lam : forall x b, value (lam x b). + +Inductive step : tm -> tm -> Prop := +| ST_AppAbs : forall x b v, + value v -> closed v -> step (app (lam x b) v) (subst x v b) +| ST_App1 : forall f f' a, step f f' -> step (app f a) (app f' a) +| ST_App2 : forall f a a', value f -> step a a' -> step (app f a) (app f a'). + +(* ── substituting a closed value: counts untouched off x, zeroed at x ─────── *) + +Lemma count_subst_closed_diff : forall x v b z, + closed v -> z <> x -> count z (subst x v b) = count z b. +Proof. + intros x v b z Hc Hzx. + induction b as [ y | f IHf a IHa | y b IHb ]. + - (* var y *) cbn [subst]. destruct (Nat.eqb x y) eqn:E. + + rewrite (Hc z). apply Nat.eqb_eq in E; subst y. + cbn. apply Nat.eqb_neq in Hzx. rewrite Hzx. reflexivity. + + reflexivity. + - (* app *) simpl. rewrite IHf, IHa. reflexivity. + - (* lam y b *) cbn [subst]. destruct (Nat.eqb x y) eqn:E. + + reflexivity. + + simpl. destruct (Nat.eqb z y); [ reflexivity | exact IHb ]. +Qed. + +Lemma count_subst_closed_same : forall x v b, + closed v -> count x (subst x v b) = 0. +Proof. + intros x v b Hc. + induction b as [ y | f IHf a IHa | y b IHb ]. + - cbn [subst]. destruct (Nat.eqb x y) eqn:E. + + apply (Hc x). + + cbn. rewrite E. reflexivity. + - simpl. rewrite IHf, IHa. reflexivity. + - cbn [subst]. destruct (Nat.eqb x y) eqn:E. + + cbn. rewrite E. reflexivity. + + cbn. rewrite E. exact IHb. +Qed. + +(* ── headline: reduction preserves the full usage profile ─────────────────── *) + +Theorem step_preserves_usage : forall t t', + step t t' -> forall z, usage z t' = usage z t. +Proof. + intros t t' Hs; induction Hs as + [ x b v Hval Hcl | f f' a Hs IH | f a a' Hval Hs IH ]; intro z. + - (* ST_AppAbs *) + rewrite usage_app. + assert (Hzv : usage z v = Zero) by (unfold usage; rewrite Hcl; reflexivity). + rewrite Hzv, qplus_0_r. + destruct (Nat.eqb z x) eqn:E. + + apply Nat.eqb_eq in E; subst z. + rewrite usage_lam_bound. + unfold usage; rewrite (count_subst_closed_same x v b Hcl); reflexivity. + + assert (Hzx : z <> x) by (apply Nat.eqb_neq; exact E). + unfold usage. rewrite (count_subst_closed_diff x v b z Hcl Hzx). + simpl. rewrite E. reflexivity. + - (* ST_App1 *) rewrite !usage_app, (IH z). reflexivity. + - (* ST_App2 *) rewrite !usage_app, (IH z). reflexivity. +Qed. + +(* ── the QTT scaling law (binder-free fragment, open v) ──────────────────── + Substituting v for x scales v's usage by x's multiplicity: + usage z (subst x v b) = usage z b + (usage x b · usage z v). + Stated on the lam-free fragment so capture cannot arise even for open v — + enough to exhibit the qmult scaling that the closed-value headline hides. *) + +Fixpoint lam_free (t : tm) : Prop := + match t with + | var _ => True + | app f a => lam_free f /\ lam_free a + | lam _ _ => False + end. + +Lemma usage_subst_scaling : forall x v b z, + z <> x -> lam_free b -> + usage z (subst x v b) = qplus (usage z b) (qmult (usage x b) (usage z v)). +Proof. + intros x v b; induction b as [ y | f IHf a IHa | y b IHb ]; + intros z Hzx Hlf. + - (* var y *) cbn [subst]. destruct (Nat.eqb x y) eqn:E. + + apply Nat.eqb_eq in E; subst y. + rewrite (usage_var_diff z x Hzx), (usage_var_same x), qmult_1_l, qplus_0_l. + reflexivity. + + assert (Hxy : x <> y) by (apply Nat.eqb_neq; exact E). + rewrite (usage_var_diff x y Hxy), qmult_0_l, qplus_0_r. reflexivity. + - (* app f a *) destruct Hlf as [Hlf Hla]. + cbn [subst]. + rewrite (usage_app z (subst x v f) (subst x v a)). + rewrite (IHf z Hzx Hlf), (IHa z Hzx Hla). + rewrite (usage_app z f a), (usage_app x f a). + destruct (usage z f), (usage x f), (usage z a), (usage x a), (usage z v); + reflexivity. + - (* lam *) cbn in Hlf; destruct Hlf. +Qed. + +(* An affine redex (bound variable used ≤ 1×) never increases any variable's + usage: the dynamic counterpart of the static affine bound. *) +Corollary affine_no_increase : forall x v b z, + z <> x -> lam_free b -> qle (usage x b) One -> + qle (usage z (subst x v b)) (qplus (usage z b) (usage z v)). +Proof. + intros x v b z Hzx Hlf Haff. + rewrite usage_subst_scaling by assumption. + revert Haff; unfold qle. + destruct (usage x b), (usage z b), (usage z v); simpl; lia. +Qed. + +(* A *linear* redex (bound variable used exactly once) preserves usage exactly, + matching the closed-value headline but now for open v. *) +Corollary linear_exact : forall x v b z, + z <> x -> lam_free b -> usage x b = One -> + usage z (subst x v b) = qplus (usage z b) (usage z v). +Proof. + intros x v b z Hzx Hlf Hlin. + rewrite usage_subst_scaling by assumption. + rewrite Hlin, qmult_1_l. reflexivity. +Qed. + +(* ── tie back to the Wave-3 static capstone ───────────────────────────────── *) + +(* A well-typed term's QTT context stays valid across a reduction step: + static usage_soundness (qtt Γ t A → usage x t = Γ x) composed with the + dynamic invariant. Static + dynamic ⇒ the quantity discipline is sound. *) +Corollary qtt_context_preserved : forall G t A t', + qtt G t A -> step t t' -> forall x, usage x t' = G x. +Proof. + intros G t A t' HT Hs x. + rewrite (step_preserves_usage t t' Hs x). + exact (usage_soundness G t A HT x). +Qed. + +Print Assumptions step_preserves_usage. +Print Assumptions usage_subst_scaling. +Print Assumptions qtt_context_preserved. diff --git a/formal/README.adoc b/formal/README.adoc index d70eb544..9343360e 100644 --- a/formal/README.adoc +++ b/formal/README.adoc @@ -84,6 +84,11 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires. | **P-4** (Wave 3) — quantitative typing fusing all three: the typing context tracks usage, proven sound (`usage x t = Γ x`) | **mechanized**, axiom-free + +| `QttDynamic.v` +| **P-4** (Wave 3) — the *dynamic* half: β-reduction preserves the usage profile; + QTT scaling law; ties back to `usage_soundness` +| **mechanized**, axiom-free |=== All mechanized theorems report *Closed under the global context* under `Print @@ -152,9 +157,20 @@ The quantities `{0,1,ω}` and their algebra are what make AffineScript *affine*: against occurrence counts. Corollary: a term typed in a singleton context uses that variable exactly once. -The remaining step is the *dynamic* half: operational progress + preservation -that PRESERVES the quantity accounting under reduction (a quantitative -substitution lemma over `P2_Stlc.v`). +* **`QttDynamic.v`** (Wave 3) — the *dynamic* half. A small-step β-reduction on + the QTT terms with the headline `step_preserves_usage`: `t → t'` implies + `usage z t' = usage z t` for every `z`, so the quantity accounting is a + *dynamic invariant*. Adds the QTT *scaling* law + `usage z (subst x v b) = usage z b + usage x b · usage z v` (via the new + `qof_mult` ×-homomorphism), an affine-no-increase corollary, and + `qtt_context_preserved`, which composes the dynamic invariant with + `usage_soundness` so a well-typed term's QTT context stays valid across a + step. β substitutes a closed value (the closed-program convention `P2_Stlc.v` + also uses), so it is capture-/axiom-free. + +The remaining step is the full operational development on the *real* AST: the +quantity-preserving substitution lemma generalised past the binder-free fragment +and the closed-value convention. == K-1 and its growth diff --git a/formal/_CoqProject b/formal/_CoqProject index 6072803d..d5404dc0 100644 --- a/formal/_CoqProject +++ b/formal/_CoqProject @@ -12,3 +12,4 @@ P2_Stlc.v QttSemiring.v AffineUsage.v QttTyping.v +QttDynamic.v diff --git a/formal/justfile b/formal/justfile index 90a217b1..0d991c95 100644 --- a/formal/justfile +++ b/formal/justfile @@ -12,7 +12,7 @@ check: for f in K1_CodegenPreservation K1Let_CodegenPreservation Siblings_Stated \ F1_TransformerPreservation F3_PragmaDecidable F4_ErrorFaithful \ P3_BorrowSound P3_BorrowGraph P2_Progress P2_Stlc \ - QttSemiring AffineUsage QttTyping; do + QttSemiring AffineUsage QttTyping QttDynamic; do echo "== coqc $f.v ==" o="$(coqc -Q . ASFormal "$f.v")" printf '%s\n' "$o"