From 039c000a1180317f183b6e7373c60ca4643ead56 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 21:51:45 +0000 Subject: [PATCH] proofs: make three modules pass --exact-split MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes the sites the strict-flag survey found: - Kripke.Residual.Is: list all nine constructor pairs instead of ending in a catch-all. The values are unchanged. - EchoBridge.≤G-trans: put the top≤ clause first, so the case tree splits on the second argument before the first. - ProofTransportExample.checkPayload: put the ImpossibleClaim clause first, for the same reason. Each function computes the same values on constructor arguments; the changes only make every clause hold definitionally. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- src/EpistemicTypes/EchoBridge.agda | 2 +- src/EpistemicTypes/Kripke/Residual.agda | 8 +++++++- src/EpistemicTypes/ProofTransportExample.agda | 2 +- 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/EpistemicTypes/EchoBridge.agda b/src/EpistemicTypes/EchoBridge.agda index a2b51b2..045369f 100644 --- a/src/EpistemicTypes/EchoBridge.agda +++ b/src/EpistemicTypes/EchoBridge.agda @@ -165,8 +165,8 @@ data _≤G_ : Grade -> Grade -> Set where top≤ : {g : Grade} -> g ≤G infinity ≤G-trans : {a b c : Grade} -> a ≤G b -> b ≤G c -> a ≤G c +≤G-trans _ top≤ = top≤ ≤G-trans (finite≤ p) (finite≤ q) = finite≤ (≤ℕ-trans p q) -≤G-trans p top≤ = top≤ ≤G-plus : (a b : Grade) -> a ≤G gradePlus a b ≤G-plus (finite a) (finite b) = finite≤ (≤ℕ-plus a b) diff --git a/src/EpistemicTypes/Kripke/Residual.agda b/src/EpistemicTypes/Kripke/Residual.agda index 22596ca..78fb4a2 100644 --- a/src/EpistemicTypes/Kripke/Residual.agda +++ b/src/EpistemicTypes/Kripke/Residual.agda @@ -45,8 +45,14 @@ E _ = ⊤ -- "Thing x is here": true only at world x. Is : W → W → Set Is a a = ⊤ +Is a b = ⊥ +Is a c = ⊥ +Is b a = ⊥ Is b b = ⊤ -Is _ _ = ⊥ +Is b c = ⊥ +Is c a = ⊥ +Is c b = ⊥ +Is c c = ⊥ Present : W → Set Present w = Σ W (λ x → Is x w) diff --git a/src/EpistemicTypes/ProofTransportExample.agda b/src/EpistemicTypes/ProofTransportExample.agda index 728af25..d480aad 100644 --- a/src/EpistemicTypes/ProofTransportExample.agda +++ b/src/EpistemicTypes/ProofTransportExample.agda @@ -28,9 +28,9 @@ Payload _ _ = Bool open import EpistemicTypes.ProofTransport Agent Claim Artifact Meaning Payload checkPayload : (a : Artifact) -> (c : Claim) -> Payload a c -> Bool +checkPayload _ ImpossibleClaim _ = false checkPayload true ArtifactIsTrue p = p checkPayload false ArtifactIsTrue _ = false -checkPayload _ ImpossibleClaim _ = false checkPayloadSound : (holder : Agent) (a : Artifact) (c : Claim) (p : Payload a c) ->