RelRST

RelRST  is a tactic that tries to solve goals by exploiting common properties of binary relations, including reflexivity, symmetry, transitivity, irreflexivity, antisymmetry, and linearity.

The heart of this tactic is a routine that builds a directed graph 

based on the binary relations in a sequent and finds shortest paths in the graph. Extensions to this routine to allow it to handle strict order relations and relations with differing strengths.

RelRST uses the the same database on relations and some of the same lemmas as the rewrite package. In addition, it relies on lemmas in the library of the following forms.

• Irreflexivity lemmas . These should have form

  

  and be named opid-of-<_irreflexivity.  

• Antisymmetry lemmas . These should have form

  

  and be named opid-of-_antisymmetry. 

• Complementing lemmas . These should have form

  

  and be named opid-of-_complement,   or

  

  and be named opid-of-<_complement. 

  

RelRST generalizes the Eq tactic in previous versions of Nuprl that only handled such reasoning with the equality relation of Nuprl 's type theory.

Here are a couple of examples of RelRST's use from a theory of divisibility  over the integers:

and

Here, I have elided hypotheses that were not required by RelRST to solve the goals. The relation is the associated relation and gcd(a;b) is a function that computes the greatest common divisor of a and b. The second example illustrates how RelRST is able to cope with relations of differing strengths.

Unlike Eq, RelRST doesn't involve any extensions being made to the primitive rule refiner.