A semi-reflexive tactic for (sub-)equational reasoning

We propose a simple theory of monotone functions that is the basis for the implementation of a tactic that generalises one step conditional rewriting by ``propagating'' constraints of the form x R y$ where the relation R can be weaker than an equivalence relation. The constraints can be propagated only in goals whose conclusion is a syntactic composition of n-ary functions that are monotone in each argument. The tactic has been implemented in the Coq system as a semi-reflexive tactic, which represents a novelty and an improvement over an earlier similar development for NuPRL. A few interesting applications of the tactic are: reasoning in type theory about equivalence classes (by performing rewriting in well-defined goals); reasoning about reductions and properties preserved by reductions; reasoning about partial functions over equivalence classes (by performing rewriting in PERs); propagating inequalities by replacing a term with a smaller (greater) one in a given monotone context.