# Respects lemma

*You should read the tutorial on representing equality of LF terms as a type family before reading this one.*

At a high level, a **respects lemma** shows that a type family or term constructor "respects" some relations on its arguments. Specifically, we use the term *respects lemma* to refer to:

- a lemma proving that the indices to a type family "respect" some relations on those indices, in the sense that inhabitation of the type family is preserved by replacing related indices.
- a
**compatibility lemma**for a term constructor`f`, which states that if some relations hold for some arguments, then a relation holds for`f`applied to those arguments.

Often, the relations in question are equality of LF terms.

## Example: Proving that a type family respects equality

It is often necessary to prove a respects lemma showing that a type family respects equality of its indices.
For example, we can define the standard equality relation `bin-eq` for binary numbers, the standard `and` relation on binary numbers, and then prove a *respects lemma* that `and` respects equality:

bin : type. e : bin. 1 : bin -> bin. 0 : bin -> bin. bin-eq : bin -> bin -> type. bin-eq/ : bin-eq N N. % note: not defined unless the numbers are the same length and : bin -> bin -> bin -> type. %mode and +N1 +N2 -N3. and/e : and e e e. and/00 : and (0 M) (0 N) (0 P) <- and M N P. and/01 : and (0 M) (1 N) (0 P) <- and M N P. and/10 : and (1 M) (0 N) (0 P) <- and M N P. and/11 : and (1 M) (1 N) (1 P) <- and M N P. %{ The respects lemma: the and relation respects equality }% and-resp : bin-eq M M' -> bin-eq N N' -> bin-eq O O' -> and M N O -> and M' N' O' -> type. %mode and-resp +EQM +EQN +EQO +A -A'. - : and-resp bin-eq/ bin-eq/ bin-eq/ A A. %worlds () (and-resp _ _ _ _ _). %total {} (and-resp _ _ _ _ _).

The theorem `and-resp` states that if M and M' are equal, and N and N' are equal, and O and O' are equal, and M & N = O, then M' & N' = O'. The proof is trivial: since the only way to conclude `bin-eq` is using `bin-eq/` where both binary numbers must be identical, the same derivation of `and` that we got as input works for the output.

If `bin-eq` were some other equivalence relation (*e.g.*, ignoring leading zeros), the respects lemma would require a more sophisticated proof (e.g., an inductive argument over the derivation of the equality).

Although we proved that `and` respects equality in all three arguments, we can easily use this lemma even when we only have an equality derivation for one pair of arguments, as long as the other two pairs of arguments are already syntactically equal. For example, we can prove:

and-first-resp : bin-eq M M' -> and M N O -> and M' N O -> type. %mode and-first-resp +EQ +A -A'. - : and-first-resp EQ A A' <- and-resp EQ bin-eq/ bin-eq/ A A'. %worlds () (and-first-resp _ _ _). %total D (and-first-resp D _ _).

(This theorem is trivial and could have been proven directly, but it illustrates the point.) When we invoke the `and-resp` lemma as a subgoal, we pass along the equality derivation for the first two arguments, and pass along the constant `bin-eq/` for the others, which are known to be identical. Therefore, it suffices to define the more general respects lemmas and then invoke them in specialized ways, if necessary.

This article or section needs an example where a respects lemma is needed. |

## Example: proving compatibility lemmas

Another kind of respects lemma is a **compatibility lemma**, which states that a relation is respected by the application of term constructors. (This is also called a **congruence lemma** when the relation in question is an equivalence relation.) For example, we can prove compatibility lemmas about the constructors `1` and `0`:

1-compat : bin-eq M M' -> bin-eq (1 M) (1 M') -> type. %mode 1-compat +EQ -EQ'. - : 1-compat bin-eq/ bin-eq/. 0-compat : bin-eq M M' -> bin-eq (0 M) (0 M') -> type. %mode 0-compat +EQ -EQ'. - : 0-compat bin-eq/ bin-eq/. %worlds () (1-compat _ _) (0-compat _ _). %total (D E) (1-compat D _) (0-compat E _).

We might use these compatibility lemmas in proving some theorems about binary numbers. For instance, we might want to prove that `not` is its own inverse:

not : bin -> bin -> type. %mode not +B -B'. not/e : not e e. not/1 : not (1 B) (0 B') <- not B B'. not/0 : not (0 B) (1 B') <- not B B'. notnot : not A B -> not B C -> bin-eq A C -> type. %mode notnot +N +N' -EQ. notnot/e : notnot not/e not/e bin-eq/. notnot/1 : notnot (not/1 N1) (not/0 N2) EQ' <- notnot N1 N2 (EQ : bin-eq A' C') <- 1-compat EQ (EQ' : bin-eq (1 A') (1 C')). notnot/0 : notnot (not/0 N1) (not/1 N2) EQ' <- notnot N1 N2 (EQ : bin-eq A' C') <- 0-compat EQ (EQ' : bin-eq (0 A') (0 C')). %worlds () (notnot _ _ _). %total D (notnot D _ _).

In the inductive cases of `notnot`, we have a derivation `EQ` that two smaller numbers are equal, and need to use this derivation to prove that if we apply the `1` constructor (for each) to each of the terms, they are still equal.

### Generalized compatibility lemmas

Compatibility lemmas can be generalized somewhat so that we needn't prove so many. Instead of defining the `0-compat` and `1-compat` cases separately, we can abstract over the constructor as an LF function:

f-compat : {EQ : bin-eq M M'} {F : bin -> bin} {EQ' : bin-eq (F M) (F M')} type. %mode f-compat +EQ +F -EQ'. - : f-compat bin-eq/ _ bin-eq/. %worlds () (f-compat _ _ _). %total D (f-compat D _ _).

Here, we instead prove that if `M` and `M'` are equal, then `F M` and `F M'` are equal for any `F`. Now we can prove the `notnot` theorem again using only this generalized compatibility lemma:

notnot : not A B -> not B C -> bin-eq A C -> type. %mode notnot +N +N' -EQ. notnot/e : notnot not/e not/e bin-eq/. notnot/1 : notnot (not/1 N1) (not/0 N2) EQ' <- notnot N1 N2 EQ <- f-compat EQ 1 EQ'. notnot/0 : notnot (not/0 N1) (not/1 N2) EQ' <- notnot N1 N2 EQ <- f-compat EQ 0 EQ'. %worlds () (notnot _ _ _). %total D (notnot D _ _).

Here we pass in the constructors `1 : bin -> bin` and `0 : bin -> bin` as `F`. The functions could arbitrary complex, like `[b] 0 (1 (1 b))`.

This generalization technique usually only works when equality is defined as Twelf identity, because of the arbitrariness of the function passed in. When it can be used, it can substantially reduce the number of compatibility lemmas that one needs to state.

This article or section needs a description of some more advanced/tasteless generalization tricks. |

All code from this tutorial. Twelf's output from this tutorial.

Read more Twelf tutorials and other Twelf documentation.