From 7fc43dd6355d74a9f1ff3ac319de504179619c46 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 15:06:16 +0100 Subject: [PATCH] hygiene: per-lemma Smoke pins for EchoApprox via concrete instance module MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes a silent violation of the CLAUDE.md "Working rules" invariant ("Every headline theorem must be pinned in Smoke.agda via using clause") for parameterised modules. EchoApprox.Approx lemmas could not be named in Smoke.agda until some PseudoMetric was supplied; PR #70 (Lane C of the multi-lane swarm) added the retract-direction lemmas but, following existing convention, left them unpinned for the same reason. This PR closes the gap with the smallest, most honest possible instance. Instance chosen: the trivial / collapse-to-strict pseudometric on the unit carrier ⊤. * Tol := ⊤, zero := tt, _+_ := λ _ _ → tt * _≤_ := λ _ _ → ⊤ * dist := λ _ _ → tt on B := ⊤ Every order / monotonicity / triangle obligation discharges to tt. Every approximate echo collapses to Σ A (λ _ → ⊤), so each pinned lemma is a proof-of-life sanity check that the parameterised module's term is well-typed at *some* instance — exactly the hygiene contract the invariant asks for. No new mathematical content. When a genuine metric instance lands in the repo, the per-lemma pins can be re-pointed at it. Headlines now pinned in Smoke.agda (9 names): * approx-EchoR (= EchoR) * approx-intro (= echo-approx-intro) * approx-strict→approx (= echo-strict→approx) * approx-relax (= echo-approx-relax) * approx-NonExpansive (= NonExpansive) * approx-compose (= echo-approx-compose) * approx-comp-sound (= echo-approx-comp-sound) * approx-comp-retract-to (= echo-approx-comp-retract-to) * approx-comp-retract-A (= echo-approx-comp-retract-A) Plus the instance constructors trivialTolerance, trivialPseudoMetric. Build verified in parent session (sandbox quirk denied positional- argument agda invocations in this worktree): $ LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda exit: 0 $ LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/Smoke.agda exit: 0 --safe --without-K invariants intact. No postulates, no funext, no path algebra — every field is tt or refl. Refs PR #70 (Lane C surfaced the gap). Refs CLAUDE.md "Working rules" invariant. Co-Authored-By: Claude Opus 4.7 (1M context) --- proofs/agda/All.agda | 1 + proofs/agda/EchoApproxInstance.agda | 98 +++++++++++++++++++++++++++++ proofs/agda/Smoke.agda | 17 +++++ 3 files changed, 116 insertions(+) create mode 100644 proofs/agda/EchoApproxInstance.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index f048444..aa23afb 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -18,6 +18,7 @@ open import EchoIntegration open import EchoCNOBridge open import EchoApprox +open import EchoApproxInstance open import EchoIndexed open import EchoDecidable open import EchoAccess diff --git a/proofs/agda/EchoApproxInstance.agda b/proofs/agda/EchoApproxInstance.agda new file mode 100644 index 0000000..9922ea0 --- /dev/null +++ b/proofs/agda/EchoApproxInstance.agda @@ -0,0 +1,98 @@ +{-# OPTIONS --safe --without-K #-} + +-- A concrete `Tolerance` + `PseudoMetric` instance for `EchoApprox.Approx`, +-- whose sole purpose is to give `Smoke.agda` a typeable identifier per +-- headline lemma of the parameterised `EchoApprox.Approx` module. +-- +-- Repo invariant (`CLAUDE.md`, "Working rules"): +-- +-- "Every headline theorem must be pinned in `Smoke.agda` via +-- `using` clause." +-- +-- Lemmas living inside the parameterised submodule `EchoApprox.Approx` +-- cannot be named in `Smoke.agda` until *some* `PseudoMetric` is +-- supplied, so the invariant is silently violated for every +-- `echo-approx-*` and `echo-strict→approx` lemma. This module closes +-- that gap. +-- +-- Design call: the trivial / collapse-to-strict pseudometric on `⊤`. +-- +-- * `Tol` := `⊤`, `zero` := `tt`, `_+_` := `λ _ _ → tt` +-- * `_≤_` := `λ _ _ → ⊤` +-- * `dist` := `λ _ _ → tt` on the carrier `B := ⊤` +-- +-- Every order / monotonicity / triangle obligation discharges to `tt`. +-- Every approximate echo `EchoR ε f y = Σ A (λ x → dist (f x) y ≤ ε)` +-- collapses to `Σ A (λ _ → ⊤)`, so each pinned lemma here is a trivial +-- sanity check that the parameterised module's term is well-typed at +-- *some* instance. That is exactly the hygiene contract the invariant +-- asks for — proof-of-life, not new content. +-- +-- We choose `A := ⊤` and `B := ⊤` so each pinned name resolves to a +-- single top-level identifier with no remaining type parameters, which +-- lets `Smoke.agda` enumerate them in a `using` clause one-for-one. +-- +-- A non-trivial pseudometric (e.g. the discrete metric over `Bool`) +-- would also work, but adds nothing the trivial one does not give for +-- the purposes of `Smoke.agda` pinning. When a genuine metric instance +-- lands in the repo, the per-lemma pins below can be re-pointed at it. + +module EchoApproxInstance where + +open import Level using (Level) +open import Data.Unit.Base using (⊤; tt) +open import Relation.Binary.PropositionalEquality using (refl) + +open import EchoApprox using (Tolerance; PseudoMetric; module Approx) + +---------------------------------------------------------------------- +-- The trivial tolerance carrier +---------------------------------------------------------------------- + +-- All fields are tt / Unit; every law obligation is met by `tt`. +trivialTolerance : Tolerance Level.zero +trivialTolerance = record + { Tol = ⊤ + ; zero = tt + ; _+_ = λ _ _ → tt + ; _≤_ = λ _ _ → ⊤ + ; ≤-refl = tt + ; ≤-trans = λ _ _ → tt + ; +-mono-≤ = λ _ _ → tt + } + +---------------------------------------------------------------------- +-- The trivial pseudometric on the carrier `⊤` +---------------------------------------------------------------------- + +-- Distance is constantly `tt`; self-distance is `refl`; triangle is `tt`. +trivialPseudoMetric : PseudoMetric ⊤ trivialTolerance +trivialPseudoMetric = record + { dist = λ _ _ → tt + ; dist-self = λ _ → refl + ; dist-tri = λ _ _ _ → tt + } + +---------------------------------------------------------------------- +-- Per-lemma proof-of-life pins for `Approx` at the trivial instance. +-- +-- Top-level identifiers, one per `EchoApprox.Approx` headline, with +-- `A := ⊤` and `B := ⊤` so each is a closed term that `Smoke.agda` +-- can enumerate in a `using` clause. Definitions use `=` (no explicit +-- type signature) so the original term's type is inferred — which is +-- exactly the typeability check the hygiene invariant asks for. +---------------------------------------------------------------------- + +private + open module ApproxT⊤ = + Approx {A = ⊤} {B = ⊤} {T = trivialTolerance} trivialPseudoMetric + +approx-EchoR = EchoR +approx-intro = echo-approx-intro +approx-strict→approx = echo-strict→approx +approx-relax = echo-approx-relax +approx-NonExpansive = NonExpansive +approx-compose = echo-approx-compose +approx-comp-sound = echo-approx-comp-sound +approx-comp-retract-to = echo-approx-comp-retract-to +approx-comp-retract-A = echo-approx-comp-retract-A diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 88eb2d1..17a5e5c 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -75,6 +75,23 @@ open import EchoApprox using ; module Approx ) +-- Per-lemma pins for the parameterised EchoApprox via EchoApproxInstance +-- (hygiene; closes the CLAUDE.md "Working rules" invariant gap for +-- parameterised modules — see follow-up to PR #70). +open import EchoApproxInstance using + ( trivialTolerance + ; trivialPseudoMetric + ; approx-EchoR + ; approx-intro + ; approx-strict→approx + ; approx-relax + ; approx-NonExpansive + ; approx-compose + ; approx-comp-sound + ; approx-comp-retract-to + ; approx-comp-retract-A + ) + open import EchoIndexed using ( Echoᵢ ; echoᵢ-intro