Relation Expansion
Every coinduction proof must supply a candidate relation R which must be shown to be a congruence, so that the desired equations can be shown behaviorally true by proving that their two sides are related by R. Sometimes the congruence property follows automatically because the relation and (constructor and selector) signatures involved are the default choices.

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 expand an instance t R t', as in (*), into a set of equations of the form:
      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