Usability issue
replace (rewriting a goal using an equality proof) is a fundamental Pie eliminator and one of the most common operations in equality-based proofs. It is not available as a tactic, so users must write a complete exact (replace ...) expression to use it, which defeats the purpose of the tactic system.
Context
Encountered when trying to rewrite a goal using an available equality hypothesis in tactic mode. The tactic palette offers no way to apply a replace-style rewrite, forcing the user to abandon the tactic UI and write the full term manually — including the motive, which is often complex.
Suggested improvement
Add a replace tactic with the signature (replace <equality-proof> <motive>) that rewrites the current goal using an equality proof. Where possible, the motive should be inferred from the goal to minimize required input.
Usability issue
replace(rewriting a goal using an equality proof) is a fundamental Pie eliminator and one of the most common operations in equality-based proofs. It is not available as a tactic, so users must write a completeexact (replace ...)expression to use it, which defeats the purpose of the tactic system.Context
Encountered when trying to rewrite a goal using an available equality hypothesis in tactic mode. The tactic palette offers no way to apply a
replace-style rewrite, forcing the user to abandon the tactic UI and write the full term manually — including the motive, which is often complex.Suggested improvement
Add a
replacetactic with the signature(replace <equality-proof> <motive>)that rewrites the current goal using an equality proof. Where possible, the motive should be inferred from the goal to minimize required input.