We introduce REST, a rewrite technique for SMT-based verifiers that supports user-defined terminating functions. Our technique builds upon proof-by-logical evaluation (PLE) that decidably encodes user-defined functions as SMT equalities. REST extends PLE to automatically instantiate provably correct rewrite rules. It uses size-change termination to ensure that rewriting does not diverge, preserving predictable verification.

We implement REST in Liquid Haskell and use it to automate proof generation. The automation provided by REST sets the ground for further proof tactic development: we used metaprogramming to implement a structural induction tactic. Our evaluation of REST and the induction tactic combined concludes that

1. they are not subsumed by existing rewriting techniques,
2. they can automate existing proof benchmarks, and
3. having the expected verification slowdown cost, they greatly ease Liquid Haskell proof development.