# Simplifying dynamic clauses

### Summary

When writing proofs about relations that introduce hypotheses, it is sometimes necessary to introduce dynamic clauses for the proof along with the hypothetical variable, to encode informal reasoning "at the variable case". In some cases, this reasoning is somewhat complicated, and can be streamlined by a judicious choice of lemma, so that the dynamic clause, while still present, is of a much simpler form, and the complicated reasoning is pushed to the top-level, where it can be more easily encoded.

### Example

Suppose that we have lists of items, some of which may be colored red.

ERROR: option 'name' deprecated or invalidelt : type. cherry : elt. strawberry : elt. blueberry : elt. list : type. nil : list. cons : elt -> list -> list. is-red : elt -> type. is-red/cherry : is-red cherry. is-red/strawberry : is-red strawberry.

A property that a list may satisfy is that all of its elements are red, which is encoded as follows:

ERROR: option 'name' deprecated or invalidERROR: option 'include' deprecated or invalidall-red : list -> type. all-red/nil : all-red nil. all-red/cons : all-red (cons H L) <- all-red L <- is-red H.

We now define a nondeterministic function that take in a list, and outputs a list derived from the input by some combination of permutation, duplication, and dropping of its elements.

ERROR: option 'name' deprecated or invalidERROR: option 'include' deprecated or invalidmix : list -> list -> type. seed : elt -> type. mix/sow : (seed E -> mix L L') -> mix (cons E L) L'. mix/reap : mix nil L -> seed E -> mix nil (cons E L). mix/nil : mix nil nil.

The behavior of `mix` is as follows: it decomposes the input list, turning every element `E` in it into a hypothesis of type `seed E`. Once the input list is empty, it builds up a new list by consing on some number of elements to the empty list, but each element must have come from some `seed E`. Since there is no restriction on how many times a hypothesis is used, the resulting list may have many (or one, or no) copies of each element in the original list, and in any order. However, since the function `mix` cannot introduce elements *ex nihilo*, we can state and prove some properties of it. For instance, when applied to an all-red list, it must yield an all-red list.

mix-pres : mix L L' -> all-red L -> all-red L' -> type. %mode mix-pres +MIX +AR -AR'.

#### First proof

It can be proved in the following way:

ERROR: option 'name' deprecated or invalidERROR: option 'include' deprecated or invalid- : mix-pres (mix/sow ([s] MIX s)) (all-red/cons RH AR) AR' <- ({sd:seed E} {dynclause: {L: list} {Mix : mix nil L} {Ared:all-red nil} {Ared':all-red L} mix-pres (mix/reap Mix sd) Ared (all-red/cons RH Ared') <- mix-pres Mix Ared Ared'} mix-pres (MIX sd) AR AR'). - : mix-pres mix/nil all-red/nil all-red/nil.

In this proof of the theorem, the block of variables introduced includes a *dynamic clause* for the relation `mix-pres` that covers the variable case. It expresses the reasoning, "if the last rule used to derive `mix` was `mix-pres` applied to the seed `sd` just introduced, then appeal to the induction hypothesis on the smaller derivation of `mix`". Without this dynamic clause, coverage would fail, and the theorem would not go through.

%block b : some {E:elt} {RH:is-red E} block {sd:seed E} {dynclause: {L: list} {Mix : mix nil L} {Ared:all-red nil} {Ared':all-red L} mix-pres (mix/reap Mix sd) Ared (all-red/cons RH Ared') <- mix-pres Mix Ared Ared'}. %worlds (b) (mix-pres _ _ _). %total X (mix-pres X _ _).

Writing dynamic clauses like this can be annoying, because Twelf's type reconstruction cannot be used to elide implicit Πs. If we left a variable such as `Mix` implicitly quantified inside the dynamic clause, it would be quantified at the very outside, which would be incorrect. Moreover, some older versions of Twelf cannot check dynamic clauses that themselves have subgoals, as is the case here.

#### Second proof

We can instead prove the same theorem in a different way, which has the advantage of working in older verisons of Twelf, and allowing more leverage of type reconstruction in any event, simplifying the presentation.
The technique is to introduce another lemma that makes explicit the invariant represented by the worlds declaration for the main theorem. In this case, we know that for every `seed E` in the context, there is a derivation `RH` of type `is-red E`.

has-rh : seed E -> is-red E -> type. %mode has-rh +A -C.

The proof of this theorem conists of one dynamic clause, which has no subgoals, and no Π-quantification:

ERROR: option 'name' deprecated or invalidERROR: option 'include' deprecated or invalid%block b : some {E:elt} {RH:is-red E} block {sd:seed E} {clause: has-rh sd RH}. %worlds (b) (has-rh _ _). %total X (has-rh X _).

Having done that, the proof of the main theorem is simply

ERROR: option 'name' deprecated or invalidERROR: option 'include' deprecated or invalid- : mix-pres (mix/reap Mix SEED) Ared (all-red/cons RH Ared') <- has-rh SEED RH <- mix-pres Mix Ared Ared'. - : mix-pres (mix/sow ([s] MIX s)) (all-red/cons RH AR) AR' <- ({sd:seed E} {dynclause: has-rh sd RH} mix-pres(MIX sd) AR AR'). - : mix-pres mix/nil all-red/nil all-red/nil. %worlds (b) (mix-pres _ _ _). %total X (mix-pres X _ _).

Note how there is now an "explicit variable case", which covers any possible derivation `SEED` of `seed E`, and appeals to the above lemma `has-rh` in order to get the derivation of `is-red H`. The second case, which introduces a parametric `sd : seed E`, needs only supply the comparatively simple dynamic clause `{dynclause: has-rh sd RH}` to ensure the proof of `has-rh` goes through.

ERROR: option 'include' deprecated or invalidTwelf code of first proof

ERROR: option 'include' deprecated or invalidTwelf code of second proof

Read more Twelf tutorials and other Twelf documentation.