Reflexive tactics for algebra, revisited

Kazuhiko Sakaguchi

Computational reflection allows us to turn verified decision procedures into efficient automated reasoning tools in proof assistants. The typical applications of such methodology i…