Skip to content
BANG

Reusable proof assets (generated inventory)

The single source of truth is the Lean source; this page is a pure derivation. What exists, where it lives, and what to reach for before hand-rolling. Companion analysis: just clones (tools/clone-report.py) ranks duplication for future extraction candidates; the triage of the current families lives in docs/notes/clone-triage.md.

Custom tactics / attributes

None. There are no macro/elab/syntax tactic definitions and no registered attributes in Bang/. Reuse today = the simp sets below + template lemmas by convention (see the design notes for each spine, e.g. krelS_state_reinstall as the D5 template). The tactics-survey's @[bang_grind]/aesop recommendations remain unimplemented — see docs/notes/clone-triage.md for why the top clone families are not tactic-shaped.

@[simp] sets by module (105 lemmas)

Calling simp in a module's proofs implicitly uses these; when writing new proofs in a module, check its set before re-proving a rewrite.

Bang/Meta/LR.lean (42)

  • reshape_nil (LR.lean:260)
  • reshape_cons (LR.lean:262)
  • renameK_cons (LR.lean:509)
  • renameK_nil (LR.lean:552)
  • renameV_vunit (LR.lean:557)
  • renameV_vint (LR.lean:558)
  • renameV_vvar (LR.lean:560)
  • renameV_vcap (LR.lean:562)
  • renameV_vthunk (LR.lean:564)
  • renameV_inl (LR.lean:566)
  • renameV_inr (LR.lean:568)
  • renameV_pair (LR.lean:570)
  • renameV_fold (LR.lean:572)
  • renameC_ret (LR.lean:575)
  • renameC_letC (LR.lean:577)
  • renameC_force (LR.lean:579)
  • renameC_lam (LR.lean:581)
  • renameC_app (LR.lean:583)
  • renameC_perform (LR.lean:585)
  • renameC_handle (LR.lean:587)
  • renameC_case (LR.lean:589)
  • renameC_split (LR.lean:591)
  • renameC_unfold (LR.lean:593)
  • renameC_binop (LR.lean:595)
  • renameV_boolVal (LR.lean:597)
  • renameC_oom (LR.lean:599)
  • renameC_wrong (LR.lean:600)
  • renameH_state (LR.lean:603)
  • renameH_throws (LR.lean:605)
  • renameH_transaction (LR.lean:607)
  • renameH_custom (LR.lean:609)
  • renameF_letF (LR.lean:612)
  • renameF_appF (LR.lean:613)
  • renameF_handleF (LR.lean:614)
  • renameH_label (LR.lean:618)
  • handlesOp_renameH (LR.lean:622)
  • tvarIdx_renameV (LR.lean:769)
  • krelS_nil (LR.lean:1492)
  • krelS_letF (LR.lean:1498)
  • krelS_appF (LR.lean:1506)
  • krelS_handleF (LR.lean:1537)
  • EnvRelK_nil_iff (LR.lean:1860)

Bang/Backend/EnvMachine.lean (27)

  • substEnv_nil (EnvMachine.lean:493)
  • substEnv_cons (EnvMachine.lean:494)
  • substEnvV_nil (EnvMachine.lean:574)
  • substEnv_ret (EnvMachine.lean:576)
  • substEnv_force (EnvMachine.lean:582)
  • substEnv_app (EnvMachine.lean:588)
  • substEnv_unfold (EnvMachine.lean:594)
  • substEnv_binop (EnvMachine.lean:600)
  • substEnv_perform (EnvMachine.lean:606)
  • substEnv_handle (EnvMachine.lean:622)
  • substEnvH_state (EnvMachine.lean:630)
  • substEnvH_transaction (EnvMachine.lean:635)
  • substEnvH_custom (EnvMachine.lean:640)
  • substEnvH_throws (EnvMachine.lean:646)
  • substEnvH_label (EnvMachine.lean:652)
  • substEnv_letC (EnvMachine.lean:660)
  • substEnv_lam (EnvMachine.lean:668)
  • substEnv_case (EnvMachine.lean:676)
  • substEnv_split (EnvMachine.lean:685)
  • substEnvV_vthunk (EnvMachine.lean:1373)
  • substEnvV_vunit (EnvMachine.lean:1380)
  • substEnvV_vint (EnvMachine.lean:1384)
  • substEnvV_vcap (EnvMachine.lean:1388)
  • substEnvV_inl (EnvMachine.lean:1393)
  • substEnvV_inr (EnvMachine.lean:1398)
  • substEnvV_pair (EnvMachine.lean:1403)
  • substEnvV_fold (EnvMachine.lean:1408)

Bang/Core/Semantics/Subst.lean (20)

  • closeC_nil (Subst.lean:297)
  • closeV_nil (Subst.lean:298)
  • shiftN_zero (Subst.lean:306)
  • closeCUnderBinders_nil (Subst.lean:323)
  • closeC_ret (Subst.lean:331)
  • closeC_force (Subst.lean:337)
  • closeC_app (Subst.lean:343)
  • closeC_perform (Subst.lean:349)
  • closeC_unfold (Subst.lean:355)
  • closeC_handleThrows (Subst.lean:365)
  • closeC_handleState (Subst.lean:378)
  • closeC_handleTransaction (Subst.lean:392)
  • closeC_handleCustom (Subst.lean:404)
  • closeV_vunit (Subst.lean:413)
  • closeV_vint (Subst.lean:418)
  • closeV_vthunk (Subst.lean:598)
  • closeV_inl (Subst.lean:604)
  • closeV_inr (Subst.lean:610)
  • closeV_pair (Subst.lean:616)
  • closeV_fold (Subst.lean:622)

Bang/Core/Soundness.lean (12)

  • hsmul_eq_smul (Soundness.lean:36)
  • hadd_eq_add (Soundness.lean:39)
  • add_nil_left (Soundness.lean:53)
  • add_nil_right (Soundness.lean:56)
  • add_cons (Soundness.lean:60)
  • smul_nil (Soundness.lean:63)
  • smul_cons (Soundness.lean:66)
  • smul_length (Soundness.lean:69)
  • add_length (Soundness.lean:73)
  • zeros_length (Soundness.lean:77)
  • basis_length (Soundness.lean:81)
  • smul_zeros (Soundness.lean:98)

Bang/Core/Semantics/Dispatch.lean (4)

  • handlerCount_letF (Dispatch.lean:208)
  • handlerCount_appF (Dispatch.lean:210)
  • handlerCount_handleF (Dispatch.lean:212)
  • handlesOp_substFrom (Dispatch.lean:262)