Replace the bespoke TreeMap traversal/find proof with one private fold-model lemma and use simp_to_model for the Const.get? representation bridge.

TreeMap list-model reduction

Reduce mergeWith to its ordered associative-list fold, prove the fold lookup equation by induction, and invoke simp_to_model for the TreeMap-to-model lookup obligation.

Hypothesis: A private fold-model lemma plus simp_to_model can replace most bespoke issue-127 proof machinery while preserving both public mergeWith lookup theorem signatures and the full Iris build.

Test: Compile Iris/Std/HeapInstances.lean, run the complete default lake build, and independently compare theorem headers and compile generic downstream consumers.

Kernel and build evidence establishes correctness and signature preservation for the current patch, but source inspection and a controlled failure show that the strongest robustness claim is not yet satisfied.

• The modified Iris/Std/HeapInstances.lean compiles on pinned Lean 4.32.0.
• The complete default Iris and IrisTest build succeeds with 259 jobs.
• Both public getElem?_mergeWith' theorem headers are byte-normalized-equivalent to the repository baseline.
• No axiom, sorry, or admit was introduced.
• The pinned released simp_to_model tactic lacks native Const.mergeWith model support.

• env LEAN_NUM_THREADS=1 lake env lean Iris/Std/HeapInstances.lean returned 0 in experiment 20260723-044741-e67162.
• env LEAN_NUM_THREADS=1 lake build completed successfully with 259 jobs; hash-recorded cached replay 20260723-051842-1376cc returned 0.
• Independent experiment 20260723-051852-d6e5d6 returned 0 and emitted passed=true.
• git diff --check returned 0; target diff is 41 insertions and 119 deletions.

• source/iris-lean/Iris/.proof-experiments/20260723-044132-a4007c: inherited unreleased-theorem route failed with unknown identifier and WF obligations.
• source/iris-lean/Iris/.proof-experiments/20260723-044741-e67162: focused target file compiled in 3.294 seconds.
• source/iris-lean/Iris/.proof-experiments/20260723-051842-1376cc: full-build replay returned 0 after the cold 259-job build completed.
• source/iris-lean/Iris/.proof-experiments/20260723-051852-d6e5d6: independent checker returned 0 with passed=true.

scripts/check_issue_127.py, using checks/Issue127.lean as a separate downstream encoding; it compares both theorem headers to git HEAD, rejects proof escapes, checks tactic and helper removal, and compiles generic consumers.

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome

no_progress

Public classification

no_progress

• Verified data-structure model lemmas -> move proof complexity from concrete tree traversal to an associative-list invariant -> reduced the target proof by 78 net lines, but native mergeWith automation remains absent.

• The current target file elaborates successfully on Lean 4.32.0.
  Experiment 20260723-044741-e67162 returncode 0 · Iris/Iris/Std/HeapInstances.lean at SHA-256 9ae351dd350ca086c02d01bfcc50e001547a0d90be56ec14b859a069976af7d7 · computed
• The complete default project build succeeds.
  Cold build completed 259 jobs; experiment 20260723-051842-1376cc replay returncode 0 · Pinned Iris and IrisTest targets in lakefile.toml · computed
• The public TreeMap and ExtTreeMap theorem signatures remain usable.
  Experiment 20260723-051852-d6e5d6 passed normalized header comparison and downstream compilation · Both getElem?_mergeWith' declarations · computed

• Use Std.Internal.List.Const.getValue?_mergeWith directly with simp_to_model on the pinned project.
  Installed Lean 4.32.0 toolchain used by current iris-lean · The identifier exists only in inherited uncommitted Lean-source modifications and is unknown to the installed library. · Experiment 20260723-044132-a4007c · A released/pinned Lean toolchain exports the theorem and corresponding mergeWith model conversion.
• Treat a 6144 MB run_experiment lake-build failure as a code regression.
  This host and wrapper resource limit · It failed before compilation with failed to create thread; the same build completed with normal resources and replayed under 16384 MB. · Experiments 20260723-044808-9be589 and 20260723-051842-1376cc · A Lean diagnostic appears under sufficient memory rather than a runtime thread-creation abort.

• Upstream Const.mergeWith support for simp_to_model
  It directly removes the only remaining implementation-level proof and matches the issue's robustness objective. · Build the smallest Std patch adding a mergeWith toListModel theorem and tactic mapping, then test a two-line Iris proof. · high · open
• Check a newer official Lean release for mergeWith model support
  A released implementation may supersede the local upstream prototype and avoid maintaining a custom lemma. · Search official Lean tags after v4.32.0 for Const.mergeWith in the simp_to_model modify map and compile a minimal fixture. · normal · open

Objective: Make the public TreeMap proof a direct simp_to_model proof with no private implementation-level fold invariant.

First action: Inspect official Lean branches/tags for post-v4.32 Const.mergeWith model support; if absent, isolate the inherited three-file Std prototype into the smallest independently compiling upstream patch.

Stop condition: Either the direct Iris proof compiles and all verification checks pass, or an authoritative maintainer confirms that a private model lemma is the intended acceptance boundary.

• Add or locate a released Std list-model theorem and simp_to_model mapping for Const.mergeWith.
• Replace Const.get?_foldl_merge and the explicit mergeWith! unfolding with a direct simp_to_model proof.
• Rerun the focused experiment, cold full build, and independent checker before candidate promotion.

• https://github.com/leanprover-community/iris-lean/issues/127 ↗

GPT-5.6 Sol principal designed and audited the patch; the GPT-5.6 Terra source delegate timed out and supplied no usable evidence. Lean 4.32.0 and Lake 5.0.0 checked the formal artifacts. Python 3.12.3 ran the deterministic experiment harness and independent checker. Git and ripgrep were used for source and diff audits. No CAS, external solver, or unverified LLM result was used as decisive evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

3153.8s

Review state

evidence invalid or incomplete; not durable progress

Attempt ID

iris-lean-127-simp-to-model-20260723-052301-5a467e

No human review recorded.