Rewriting Induction for Existentially Quantified Equations in Logically Constrained Rewriting (Full Version)

TL;DR

This paper addresses proving inductive theorems for equations in logically constrained rewrite systems by extending the $RI$ framework to constrained $\exists$-equations. It defines constrained $\exists$-equations as $(\exists \boldmath{x}: \eta. s \approx t)[$\phi$] and shows how applying a constrained rewrite rule $\ell \to r [\varphi]$ at a position introduces existential quantification to the extra variables $\boldmath{z}$, yielding $(\exists \boldmath{x}, \boldmath{z}: \eta \land \varphi\gamma. s[r\gamma]_p \approx t)[$\phi$]. A central novelty is the Deletion rule, extended to accept $(\exists \boldmath{x}: \eta. s \approx t)[$\phi$] when $s = t$ or $\phi$ is unsatisfiable or when a theory-term equality is entailed by $\phi$ via $(\phi \Rightarrow (\exists \boldmath{x}. (\eta \land s=t)))$. The paper also introduces constrained $\exists$-terms and constrained rewriting for them, proving that the extended $RI$ is a conservative extension of the existing $RI$ for constrained equations, with the same termination guarantees under standard assumptions, and it enables reducing inequalities to equations within $RI$.

Abstract

Rewriting Induction (RI) is a principle to prove that an equation over terms is an inductive theorem of a rewrite system, i.e., that any ground instance of the equation is a theorem of the rewrite system. RI has been adapted to several kinds of rewrite systems, and RI for constrained rewrite systems has been extended to inequalities. In this paper, we extend RI for constrained equations to existentially quantified equations in logically constrained rewriting. To this end, we first extend constrained equations by introducing existential quantification to the equation part of constrained equations. Then, in applying a constrained rewrite rule to such extended constrained equations, we introduce existential quantification to extra variables of the applied rule. Finally, using the extended application of constrained rewrite rules, we extend RI for constrained equations to existentially quantified equations.