CSE.v: 5 Admitted, regression from axiomatized cseExpr in GHC 9.10

[lastland]

Context

The CSE module verifies that Common Subexpression Elimination preserves well-scopedness — a key result from "Embracing a Mechanized Formalization Gap" (arxiv:1910.11724).

History

• Before PR Migrate hs-to-coq to GHC 9.10.3 and Coq 8.20 #209 (ghc8-coq810): cseExpr was a concrete Definition in lib/CSE.v (0 Axioms in the file). Proofs could unfold and compute with CSE functions. tryForCSE_simpl was Qed. WS_cseExpr was the only Admitted (1 Admitted total) — partially proved by core_induct with admit in 4 branches (App, Let/NonRec, Let/Rec, Case/lookup).
• PR Migrate hs-to-coq to GHC 9.10.3 and Coq 8.20 #209 (GHC 9.10): GHC 9.10's CSE module uses patterns hs-to-coq cannot translate (view patterns, complex mutual recursion, Data.Map.Strict with type annotations). The module is now axiomatize module-ed, making cseExpr/cseBind/try_for_cse all Axioms. 4 new unfolding lemmas added as Admitted placeholders, plus tryForCSE_simpl regressed from Qed to Admitted. WS_cseExpr remains Admitted (was partially proved, now has no proof body since it can't unfold anything).
• Theorem-level comparison:
  • Before: WS_cseExpr (1 Admitted, partially proved with 4 admits in branches)
  • After: cseExpr_App, cseExpr_Let, cseBind_NonRec (3 new Admitted), tryForCSE_simpl (Qed→Admitted regression), WS_cseExpr (still Admitted, but now fully blocked)
• Classification: Regression (1→5 Admitted). Paper-claims-audit marks claim G6 as "REGRESSED."

Current State

5 Admitted in examples/ghc/theories/CSE.v:

Lemma	Line	Description
cseExpr_App	47	Unfolding: cseExpr on App constructor
cseExpr_Let	53	Unfolding: cseExpr on Let constructor
cseBind_NonRec	63	Unfolding: cseBind on NonRec constructor
tryForCSE_simpl	179	Unfolding: tryForCSE (was Qed before GHC 9.10)
WS_cseExpr	187	Main theorem: well-scopedness preservation

Root Cause

lib/CSE.v now has 23+ axiomatized functions (was 0 Axioms before). GHC 9.10's CSE module uses view patterns and complex mutual recursion that hs-to-coq cannot translate.

Potential Solutions

1. De-axiomatize core functions: Write redefine edits producing concrete Coq definitions for cseExpr/cseBind/try_for_cse/cse_bind.
2. Partial de-axiomatization: Concrete definitions for just the core functions via midamble.
3. Improve hs-to-coq: Add view pattern support.
4. Accept as known limitation.

Acceptance Criteria

• Feasibility assessment for de-axiomatizing cseExpr/cseBind/try_for_cse
• If feasible: WS_cseExpr proved (restoring paper claim G6)
• Gap documented in paper-claims-audit.md

---

This issue was generated with the help of Claude Code. @lastland has checked these issues before posting.