Every coinduction proof must supply a

But in many other cases, proving the congruence property involves assuming that two terms are related by R and then showing that two other terms are related by R. In such cases, after applying quantifier and implication elimination, we will have assumed a ground equation

(*) t R t' = true ,which is often not directly usable for proving that the other two terms are related by R.

However, R is usually defined by some equations of the form

(+) (X) T0 R T0' = T1 == T1' and T2 == T2' and ....... ,where T0, T0' are terms of hidden sort, and the term pairs T1, T1', etc. each have the same visible sort. Then we can

t1 = t1' t2 = t2' ....... ,where the pairs t', t1' etc. are substitution instances of T', T1', etc. These consequences of (*) should be placed among the hypotheses of the proof, and are often essential for checking the congruence property.

This rule of inference, which we call **relation
expansion**, is actually a general result of equational logic,
not specific to hidden algebra. Its soundness is proved as
follows: an instance t R t' of T0 R T0' can only be true when each conjunct on the rightside of the
equation (+) is true; because each
conjunct relates two terms by ==, truth
of the conjunct implies that its two terms can be proved equal.

It is also possible that R has been defined recursively, so that there is a conjunct of the form Ti R Ti' on the rightside of (+). In this case, relation expansion of (*) produces an equation of the form

ti R ti' = true .

Kumo has a general inference rule that converts (some) first order formulae to equations that can be used as rewrite rules; this inference rule is general enough to include relation expansion as a special case.

[Next] [Prev] [Home] [BHome]

24 April 1998