Subject: Tactics

Keywords: ::tactic

Title: RelRST (using reflexive, symmetric, transitive relations)

--------------------------------------------------
 If a user defined relation ⌜relname(...; x; y)⌝ is an equivalence relation
then the tactic RelRST can prove that a conclusion ⌜relname(...; a; b)⌝ follows
from hypotheses of that form. To make this work, three lemmas must be
added :  relname_weakening, relname_inversion, and relname_transitivity.
It is crucial that these lemmas are named exactly like this.
Then an update like geo-eq update that contains
 rrrs_add (ioid obid) [relname,`equal`];;
is added to the library.
After that, RelRST should work provided it can find the three lemmas for
relname with the right names and with the right form (search for examples
of other _weakening, _inversion, and _transitivity lemmas).⋅
--------------------------------------------------

Authors: MARK:t

⋅

Home