Skip to content

Commit f742e62

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
proof(SafeCSV): DISCHARGE filterTrueIdentity + mapFieldsIdentity, fix 3 broken proofs, wire module into proven.ipkg (proven#90 #107 #119)
Three coordinated changes to `Proven.SafeCSV.Proofs`: 1. **DISCHARGE filterTrueIdentity + mapFieldsIdentity** by induction. - `filterTrueIdentity` (3 lines): the `(x :: xs)` case reduces by beta-reduction of the constant-True lambda inside the `if`-arm, then `cong (x ::)` on the recursive call. The OWED comment claimed the lambda doesn't unfold inside `if`, but empirical test (`/tmp/charrefl/src/TestCsv.idr`) shows it does. - `mapFieldsIdentity` (8 lines): add helper `mapIdHelper : (xs : List a) -> map id xs = xs` (3 lines, induction on `xs`), then compose at the outer + inner list levels via `trans` / `cong`. Idris2 0.8.0's `Data.List` doesn't ship `mapId` as a Refl-reducible lemma, so the helper lives here. 2. **Convert 3 broken `= Refl` proofs to OWED stubs** with an accurate blocker explanation. The pre-existing `defaultDelimiterIsComma` / `defaultQuoteIsDoubleQuote` / `defaultEscapeMatchesQuote` had `= Refl` bodies that DO NOT type-check on Idris2 0.8.0 — `defaultOptions.delimiter` does not reduce to `','` even though `defaultOptions = MkCSVOptions ',' '"' '"' "\r\n"` and `(MkCSVOptions ',' '"' '"' "\r\n").delimiter = ','` is Refl. The blocker is record-field projection through a `public export` top-level constant — same family as the SafeFile pre-#136 bug, but here the LHS is a top-level constant with no argument to attach a visibility-bumped function to. Also added 3 *constructor-form* witnesses (`defaultDelimiterIsCommaCtor` etc.) that DO type-check by Refl. Callers with flexibility should prefer the `*Ctor` form. 3. **Wire `Proven.SafeCSV.Proofs` into `proven.ipkg`** so CI now validates the module. Previously the module was orphan — file existed but wasn't built. That orphan status had concealed the 3 broken-proof errors. With this change, breakage will be caught at PR time going forward. Net effect: 2 new DISCHARGES + 3 hidden-broken-proofs converted to honest OWED + 3 new constructor-form witnesses + CI now validates the file (was: false-green by omission). Empirical reduction map ref: `reference_idris2_0_8_0_reduction_map.md`. Zero `believe_me`/`postulate`/`idris_crash`. Refs proven#90 (Phase 3 OWED triage), proven#107 (overly-cautious OWED meta-issue), proven#119 (paths-forward proposal). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 477172b commit f742e62

2 files changed

Lines changed: 92 additions & 34 deletions

File tree

‎proven.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -212,6 +212,7 @@ modules = Proven
212212
, Proven.SafeTensor
213213
-- Data formats
214214
, Proven.SafeCSV
215+
, Proven.SafeCSV.Proofs
215216
, Proven.SafeDigest
216217
, Proven.SafeDigest.Proofs
217218
, Proven.SafeRegistry

‎src/Proven/SafeCSV/Proofs.idr‎

Lines changed: 91 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -90,31 +90,39 @@ makeRectangularEmpty = Refl
9090
-- Filter and Map Properties
9191
--------------------------------------------------------------------------------
9292

93-
||| OWED: `filterRows (\_ => True) csv = csv`. By the definition
94-
||| `filterRows = filter`, this is the well-known `filterTrue`
95-
||| identity for `Data.List.filter`. Held back by Idris2 0.8.0 not
96-
||| reducing `filter (\_ => True) (x :: xs)` to `x :: filter (\_ => True) xs`
97-
||| by `Refl` alone — `filter`'s with-block branch on the predicate's
98-
||| result does not unfold under an opaque lambda, so the inductive
99-
||| step is not Refl-discharable and the stdlib does not expose a
100-
||| `filterTrueId` lemma. Discharge once `Data.List` ships the lemma
101-
||| or once the predicate's constant return is exposed reductively.
102-
public export
103-
0 filterTrueIdentity : (csv : CSV) -> filterRows (\_ => True) csv = csv
104-
105-
||| OWED: `mapFields id csv = csv`. By the definition
106-
||| `mapFields f = map (map f)`, this composes the standard `mapId`
107-
||| lemma (`map id xs = xs`) at the outer and inner list levels.
108-
||| Held back by Idris2 0.8.0 not exposing `Data.List.mapId` as a
109-
||| `Refl`-reducible identity — the proof requires induction on the
110-
||| outer list and a second induction on each `Row`, neither of which
111-
||| is available without an explicit recursive body, and the stdlib
112-
||| does not ship the lemma. Discharge once `Data.List` ships
113-
||| `mapId` (or by adding a local recursive `mapIdList` helper plus
114-
||| `cong (:: _)` traversal — kept as OWED here pending the estate
115-
||| convention on whether to inline the helper).
116-
public export
117-
0 mapFieldsIdentity : (csv : CSV) -> mapFields id csv = csv
93+
||| DISCHARGED: `filterRows (\_ => True) csv = csv`. By the definition
94+
||| `filterRows = filter`, the `(x :: xs)` case reduces to
95+
||| `if (\_ => True) x then x :: filter ... xs else filter ... xs`,
96+
||| then to `if True then x :: ... else ...`, then to `x :: ...`.
97+
||| Inductive step closed by `cong (x ::)` applied to the recursive
98+
||| call. The OWED comment claimed the lambda doesn't unfold inside
99+
||| `if`, but empirically (Idris2 0.8.0, `/tmp/charrefl` harness) it
100+
||| does — the cons-arm reduces by Refl after lambda beta-reduction.
101+
public export
102+
filterTrueIdentity : (csv : CSV) -> filterRows (\_ => True) csv = csv
103+
filterTrueIdentity [] = Refl
104+
filterTrueIdentity (x :: xs) = cong (x ::) (filterTrueIdentity xs)
105+
106+
||| Helper: `map id xs = xs` for any `List`. Used to discharge
107+
||| `mapFieldsIdentity` below at both the outer (rows) and inner
108+
||| (fields) list levels. Idris2 0.8.0's `Data.List` does not ship
109+
||| this as a `Refl`-reducible lemma, so it lives here.
110+
mapIdHelper : (xs : List a) -> map Prelude.id xs = xs
111+
mapIdHelper [] = Refl
112+
mapIdHelper (x :: xs) = cong (x ::) (mapIdHelper xs)
113+
114+
||| DISCHARGED: `mapFields id csv = csv`. By the definition
115+
||| `mapFields f = map (map f)`, the `(x :: xs)` case reduces to
116+
||| `map id x :: map (map id) xs`. Outer cons rewritten via
117+
||| `mapIdHelper x` on the head (giving `x ::`), then inductive
118+
||| step on the tail via `mapFieldsIdentity xs`. Composed with
119+
||| `trans` to match `(map id x) :: (map (map id) xs) = x :: xs`.
120+
public export
121+
mapFieldsIdentity : (csv : CSV) -> mapFields Prelude.id csv = csv
122+
mapFieldsIdentity [] = Refl
123+
mapFieldsIdentity (x :: xs) =
124+
trans (cong (:: map (map Prelude.id) xs) (mapIdHelper x))
125+
(cong (x ::) (mapFieldsIdentity xs))
118126

119127
||| column from empty CSV is always empty.
120128
public export
@@ -128,19 +136,68 @@ columnByNameFromEmpty _ = Refl
128136

129137
--------------------------------------------------------------------------------
130138
-- Default Options Properties
139+
--
140+
-- The three claims below state that `defaultOptions` has comma /
141+
-- double-quote / matching-escape. Operationally true by the
142+
-- `defaultOptions = MkCSVOptions ',' '"' '"' "\r\n"` body in
143+
-- `Proven.SafeCSV`, BUT Idris2 0.8.0 does NOT reduce a `public
144+
-- export` top-level definition through `.fieldName` projection at
145+
-- type-check time — `defaultOptions.delimiter` does not normalise to
146+
-- `(MkCSVOptions ',' '"' '"' "\r\n").delimiter` by Refl alone, even
147+
-- though `(MkCSVOptions ',' '"' '"' "\r\n").delimiter = ','` IS
148+
-- Refl-discharable. Empirically verified at `/tmp/charrefl/src/
149+
-- TestRecField.idr`. Same blocker family as the pre-fix SafeFile
150+
-- `updateAfterRead`/`updateAfterWrite` issue (proven#136 fix
151+
-- inlined the constructor on a function with an argument; here the
152+
-- record field is a top-level constant with no argument to attach a
153+
-- visibility-bumped function to).
154+
--
155+
-- Discharge once Idris2 fixes the projection-through-top-level-def
156+
-- reduction, OR by re-stating each lemma at the constructor form
157+
-- `(MkCSVOptions ',' '"' '"' "\r\n").delimiter = ','` and leaving
158+
-- the abstract `defaultOptions.delimiter = ','` form as a bridge
159+
-- once a `defaultOptionsIsCtor` lemma is admitted (which itself
160+
-- requires the same reduction we're missing).
161+
--
162+
-- Stated as OWED postulates parallel to SafeBuffer's I6/I7 pattern.
131163
--------------------------------------------------------------------------------
132164

133-
||| Default delimiter is comma.
165+
||| OWED: Default delimiter is comma.
134166
public export
135-
defaultDelimiterIsComma : defaultOptions.delimiter = ','
136-
defaultDelimiterIsComma = Refl
167+
0 defaultDelimiterIsComma : defaultOptions.delimiter = ','
137168

138-
||| Default quote character is double-quote.
169+
||| OWED: Default quote character is double-quote.
139170
public export
140-
defaultQuoteIsDoubleQuote : defaultOptions.quote = '"'
141-
defaultQuoteIsDoubleQuote = Refl
171+
0 defaultQuoteIsDoubleQuote : defaultOptions.quote = '"'
142172

143-
||| Default escape character matches quote character (RFC 4180).
173+
||| OWED: Default escape character matches quote character (RFC 4180).
144174
public export
145-
defaultEscapeMatchesQuote : defaultOptions.escape = defaultOptions.quote
146-
defaultEscapeMatchesQuote = Refl
175+
0 defaultEscapeMatchesQuote : defaultOptions.escape = defaultOptions.quote
176+
177+
--------------------------------------------------------------------------------
178+
-- Constructor-form witnesses of the same facts
179+
--
180+
-- These three are the same theorems as the OWED above but stated at
181+
-- the explicit-constructor LHS, so the `.fieldName` projection
182+
-- reduces by Refl. They are the proof-debt-free witnesses callers
183+
-- should prefer when they have flexibility in how to reference the
184+
-- default options shape.
185+
--------------------------------------------------------------------------------
186+
187+
||| Constructor-form: the explicit `MkCSVOptions ',' '"' '"' "\r\n"`
188+
||| (which `defaultOptions` is judgmentally equal to at runtime) has
189+
||| delimiter `','`.
190+
public export
191+
defaultDelimiterIsCommaCtor : (MkCSVOptions ',' '"' '"' "\r\n").delimiter = ','
192+
defaultDelimiterIsCommaCtor = Refl
193+
194+
||| Constructor-form: quote character is `'"'`.
195+
public export
196+
defaultQuoteIsDoubleQuoteCtor : (MkCSVOptions ',' '"' '"' "\r\n").quote = '"'
197+
defaultQuoteIsDoubleQuoteCtor = Refl
198+
199+
||| Constructor-form: escape matches quote.
200+
public export
201+
defaultEscapeMatchesQuoteCtor :
202+
(MkCSVOptions ',' '"' '"' "\r\n").escape = (MkCSVOptions ',' '"' '"' "\r\n").quote
203+
defaultEscapeMatchesQuoteCtor = Refl

0 commit comments

Comments
 (0)