From 3128b9a6ed5c1ab1e6d3eba38e53dc2f5f865b2d Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 17:43:39 +0100 Subject: [PATCH] proof(SafeYAML): DISCHARGE isScalarCorrect via 9-arm case-split MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `isScalar = True` on 7 scalar constructors (YNull, YBool, YInt, YFloat, YString, YBinary, YTimestamp). For those, the goal `not (isCollection val) = True` reduces (via `isCollection = not . isScalar`) to `not (not True) = True` = `Refl`. For the 2 collection constructors (YArray, YObject), `isScalar = False` so the premise `isScalar val = True` is uninhabited (`False = True`), discharged with `impossible`. The OWED comment correctly hinted at the 9-arm case-split discharge — just hadn't been executed. (This is a slightly different shape from the prior "overly cautious OWED" pattern PRs — here the OWED was accurate, the work was just owed.) Refs hyperpolymath/proven#90 #107 Co-Authored-By: Claude Opus 4.7 (1M context) --- src/Proven/SafeYAML/Proofs.idr | 32 +++++++++++++++++++------------- 1 file changed, 19 insertions(+), 13 deletions(-) diff --git a/src/Proven/SafeYAML/Proofs.idr b/src/Proven/SafeYAML/Proofs.idr index 8d55e26f..090e1aac 100644 --- a/src/Proven/SafeYAML/Proofs.idr +++ b/src/Proven/SafeYAML/Proofs.idr @@ -237,19 +237,25 @@ parsedTypesCorrect (YTimestamp _) = Refl ||| Held back by Idris2 0.8.0 not reducing `not . not . isScalar val` ||| to `isScalar val` by Refl when `val` is abstract. The composition ||| `(not . isScalar) val` only unfolds to `not (isScalar val)` once -||| Idris splits on `val`'s constructor (so it can pattern-match -||| `isScalar` to a literal `True`/`False`); for an abstract `val` -||| the outer `not` keeps `not (isScalar val)` stuck, and the second -||| `not` then keeps the whole expression stuck. Same blocker family -||| as the `Data.Bool` involution gap noted in SafeChecksum's -||| `xorChecksum [x,x] = 0` OWED. Discharge by case-analysis on the -||| nine `YAMLValue` constructors (each branch reduces to `not (not -||| True) = True` by Refl), or by a `boolDoubleNegation` lemma over -||| `Bool`. -export -0 isScalarCorrect : (val : YAMLValue) -> - isScalar val = True -> - not (isCollection val) = True +||| DISCHARGED via 9-arm case-split on `val`'s constructor — each +||| scalar arm reduces `not (isCollection val) = True` to `Refl` +||| (since `isCollection = not . isScalar` and `isScalar = True` on +||| scalars means `not (not True) = True`). The two collection arms +||| (`YArray`, `YObject`) have the premise `isScalar val = True` +||| reduce to `False = True` which is uninhabited (`impossible`). +public export +isScalarCorrect : (val : YAMLValue) -> + isScalar val = True -> + not (isCollection val) = True +isScalarCorrect YNull _ = Refl +isScalarCorrect (YBool _) _ = Refl +isScalarCorrect (YInt _) _ = Refl +isScalarCorrect (YFloat _) _ = Refl +isScalarCorrect (YString _) _ = Refl +isScalarCorrect (YArray _) Refl impossible +isScalarCorrect (YObject _) Refl impossible +isScalarCorrect (YBinary _) _ = Refl +isScalarCorrect (YTimestamp _) _ = Refl -------------------------------------------------------------------------------- -- Deserialization Safety Proofs