RFC / KEP-1: Taclet-generating transformers (lemmas instead of metaconstructs, built-in rules, etc.) - #3893

Draft

unp1 wants to merge 20 commits into

mainfrom

bubel/lemma-taclet-spike

Commits on Jul 5, 2026

Spike: taclet-generating transformers (lemma introduction rules)
unp1
committed
Lemma cleanup: lazy soundness POs off the search path, proof status tracking
unp1
committed
OneStepSimplifier: expose side-effect-free simplification core
unp1
committed
OSS as lemma generator: capture one-step-simplifications as provable taclets
unp1
committed
Add OSS lemma reuse measurement probe (runOssReuseProbe)
unp1
committed
Mode 2: a-posteriori lemma elaboration of finished proofs
unp1
committed
Transparent OSS: strategy option, CLI --save-transparent, GUI actions
unp1
committed
Missing Lemmas tab: load lemma soundness POs as side proofs from the GUI
unp1
committed
Fix transparent-mode automation on heap/SE proofs (SumAndMax runaway)
unp1
committed
Fix circular lemma soundness proof + duplicate GUI registration
unp1
committed
Redesign lemma dependency view: per-proof, grouped, batch-provable
unp1
committed
Fix lemma soundness PO generation for quantifiers; disable OSS in obligations
unp1
committed
Fix transparent-mode failures on contract PO proofs (BinarySearch)
unp1
committed
Transparent mode: no opaque OSS at all; ordinary rules handle the rest
unp1
committed
Transparent scheduling: lemma path wins the race; two determinism fixes
unp1
committed
Batch prove: keep closed obligations out of the task tree; refresh status
unp1
committed
Task tree: abandon all proofs of an environment at once
unp1
committed
Prove all lemmas: show a progress dialog with a cancel button
unp1
committed
Remove stray auto-generated files accidentally committed
unp1
committed
Undo determinism fix of previous commit for backwards compatibility
unp1
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

RFC / KEP-1: Taclet-generating transformers (lemmas instead of metaconstructs, built-in rules, etc.) - #3893

RFC / KEP-1: Taclet-generating transformers (lemmas instead of metaconstructs, built-in rules, etc.)#3893
unp1 wants to merge 20 commits into
mainfrom
bubel/lemma-taclet-spike

Commits on Jul 5, 2026

Spike: taclet-generating transformers (lemma introduction rules)

Lemma cleanup: lazy soundness POs off the search path, proof status tracking

OneStepSimplifier: expose side-effect-free simplification core

OSS as lemma generator: capture one-step-simplifications as provable taclets

Add OSS lemma reuse measurement probe (runOssReuseProbe)

Mode 2: a-posteriori lemma elaboration of finished proofs

Transparent OSS: strategy option, CLI --save-transparent, GUI actions

Missing Lemmas tab: load lemma soundness POs as side proofs from the GUI

Fix transparent-mode automation on heap/SE proofs (SumAndMax runaway)

Fix circular lemma soundness proof + duplicate GUI registration

Redesign lemma dependency view: per-proof, grouped, batch-provable

Fix lemma soundness PO generation for quantifiers; disable OSS in obligations

Fix transparent-mode failures on contract PO proofs (BinarySearch)

Transparent mode: no opaque OSS at all; ordinary rules handle the rest

Transparent scheduling: lemma path wins the race; two determinism fixes

Batch prove: keep closed obligations out of the task tree; refresh status

Task tree: abandon all proofs of an environment at once

Prove all lemmas: show a progress dialog with a cancel button

Remove stray auto-generated files accidentally committed

Undo determinism fix of previous commit for backwards compatibility