metaprogramming-rosetta-stone
metaprogramming-rosetta-stone copied to clipboard
Published
20 hours ago •
coq-community
coq-community
A simplification tactic for Z-module equations, specific to Z
This PR implements the Z_zmodule_simplify tactic. For example, it turns a goal of the form
(x + y + - z + y)%Z = (x + - z + y + y')%Z
into
y = y'.
This kind of reflexive tactic leaving a proof obligation needs to simplify the obligation carefully. I'm not sure whether the current implementation is the best way to do so.
