Next: Elimination Rule for Relations Up: New features in LEGO Versin 1.3 Previous: Assumption Tactic

LEGO Version 1.3: Configure Equality

Configure Equality sets up the equality to be used by Qrepl, Theorems, Inversion, Induction and qnify.

Its usage is

It will work with any propositional equality which is reflexive and substitutive.

The command first checks if the identifier eq_name_sym has been defined. If not, a proof of symmetry for eq_name is computed and called eq_name_sym. This done, it registers the name and the three theorems.

Note that if the symmetry proof is to be computed, the reflexivity and substitutivity proofs must already exist.

Note further that the appropriate Configure Equality command must be executed before any inductive declarations relying on it.

Configure Equality subsumes the previous Configure Qrepl command. (Indeed the former calls the latter.) Since Qrepl does not require equality to be reflexive (merely symmetric and substitutive), the old command is still available, enabling the use of Qrepl with partial equivalence relations.