From 68209bad04731f114a2167f0074b81159a0276f3 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 21:51:44 +0000 Subject: [PATCH 1/2] proofs: make three modules pass the strict flag set MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes the repo-side sites the strict-flag survey found: - EchoExampleParser.parses-aux: the LP clause takes a variable depth but came after clauses that split on the depth, so --exact-split rejected it. Put it first, so the case tree splits on the token first. The function is unchanged. - EchoTropical._⊕_: the clause `m ⊕ zero = m` overlapped `zero ⊕ n`. It is now `suc m ⊕ zero = suc m`; the two agree at zero. - EchoBitNarrowingNumeric: stdlib's deprecated ≤-step, fatal under -W error, is replaced by m≤n⇒m≤1+n. Remaining strict failures, outside this repo: EchoCNOBridge and EchoThermodynamicsArbitrary import absolute-zero's CNO, which does not declare --cubical-compatible. That fix belongs in absolute-zero. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- proofs/agda/EchoBitNarrowingNumeric.agda | 4 ++-- proofs/agda/EchoExampleParser.agda | 5 ++++- proofs/agda/EchoTropical.agda | 2 +- 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/proofs/agda/EchoBitNarrowingNumeric.agda b/proofs/agda/EchoBitNarrowingNumeric.agda index 3d1621f..c193149 100644 --- a/proofs/agda/EchoBitNarrowingNumeric.agda +++ b/proofs/agda/EchoBitNarrowingNumeric.agda @@ -7,7 +7,7 @@ module EchoBitNarrowingNumeric where open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_; _^_; _<_; _≤_; z≤n; s≤s) -open import Data.Nat.Properties using (+-suc; +-identityʳ; *-assoc; ≤-step) +open import Data.Nat.Properties using (+-suc; +-identityʳ; *-assoc; m≤n⇒m≤1+n) open import Data.Vec.Base using (Vec; []; _∷_) open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans; subst; module ≡-Reasoning) @@ -48,7 +48,7 @@ private double-mono (s≤s p) = s≤s (s≤s (double-mono p)) join-bound : ∀ {m n} → m < n → ∀ b → joinBit m b < double n - join-bound (s≤s p) O = s≤s (≤-step (double-mono p)) + join-bound (s≤s p) O = s≤s (m≤n⇒m≤1+n (double-mono p)) join-bound (s≤s p) I = s≤s (s≤s (double-mono p)) -- The bit-vector reconstruction has the exact arithmetic shape of the API. diff --git a/proofs/agda/EchoExampleParser.agda b/proofs/agda/EchoExampleParser.agda index b1e6fba..dfd7c98 100644 --- a/proofs/agda/EchoExampleParser.agda +++ b/proofs/agda/EchoExampleParser.agda @@ -78,11 +78,14 @@ paren-pair = LP ∷ RP ∷ LP ∷ RP ∷ [] -- The auxiliary's signature `ℕ → List Token → Bool` mirrors a state -- machine. We pattern-match on the token first (Agda-friendly recursion -- shape) and on the depth only in the RP case (the abort condition). +-- The LP clause comes first so the case tree splits on the token +-- before the depth: every clause then holds definitionally, which +-- `--exact-split` requires. parses-aux : ℕ → List Token → Bool +parses-aux d (LP ∷ ts) = parses-aux (suc d) ts parses-aux zero [] = true parses-aux (suc _) [] = false -parses-aux d (LP ∷ ts) = parses-aux (suc d) ts parses-aux zero (RP ∷ _) = false parses-aux (suc d) (RP ∷ ts) = parses-aux d ts diff --git a/proofs/agda/EchoTropical.agda b/proofs/agda/EchoTropical.agda index 72fc148..fd89672 100644 --- a/proofs/agda/EchoTropical.agda +++ b/proofs/agda/EchoTropical.agda @@ -24,7 +24,7 @@ infixl 6 _⊕_ _⊕_ : ℕ → ℕ → ℕ zero ⊕ n = n -m ⊕ zero = m +suc m ⊕ zero = suc m suc m ⊕ suc n = suc (m ⊕ n) -- Basic tropical properties (simplified for bridge purposes) From 0584914a2568c4b63976659fa8646320d53caaec Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 22:16:03 +0000 Subject: [PATCH 2/2] proofs: split the second-token catch-all for --exact-split The strict re-sweep found one more site that the earlier parses-aux failure had masked: second-token's catch-all clause. List its two short-list cases explicitly. Behaviour is unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- proofs/agda/EchoExampleParser.agda | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/proofs/agda/EchoExampleParser.agda b/proofs/agda/EchoExampleParser.agda index dfd7c98..95fcc90 100644 --- a/proofs/agda/EchoExampleParser.agda +++ b/proofs/agda/EchoExampleParser.agda @@ -114,7 +114,8 @@ paren-nested≢paren-pair p = where second-token : List Token → Token second-token (_ ∷ t ∷ _) = t - second-token _ = LP -- default; never reached for these inputs + second-token [] = LP -- default; never reached for these inputs + second-token (_ ∷ []) = LP paren-empty≢paren-nested : paren-empty ≢ paren-nested paren-empty≢paren-nested p =