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.

%sort elt %.
%term cherry elt %.
%term strawberry elt %.
%term blueberry elt %.
%sort list %.
%term nil list %.
%term cons %pi elt %-> list %-> list %.
%sort is-red {_ elt} %.
%term is-red/cherry is-red cherry %.
%term 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:

%sort all-red {_ list} %.
%term all-red/nil all-red nil %.
%term all-red/cons %pi (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.

%sort mix {_ list} {_ list} %.
%sort seed {_ elt} %.
%term mix/sow %pi (%pi (seed E) %-> (mix L L')) %-> (mix (cons E L) L') %.
%term mix/reap %pi (mix nil L) %-> (seed E) %-> (mix nil (cons E L)) %.
%term 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 <I>ex nihilo</I>, 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.

%sort mix-pres {_ mix L L'} {_ all-red L} {_ all-red L'} %.
%mode mix-pres %in %in %out %.

First proof

The proof of this theorem can be completed in the following way:

- : 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.

%block complicated_block : 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 (complicated_block) (mix-pres _ _ _).
%total X (mix-pres X _ _).

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.

Writing dynamic clauses like this can be annoying, because STELF’s type reconstruction cannot be used to elide implicit $\Pi$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.

Second proof

We can instead prove the same theorem in a different way, which has the advantage of working in older verisons of STELF, 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.

%sort has-rh {_ seed E} {_ is-red E} %.
%mode has-rh %in %out %.

We can prove the has-rh theorem in a %world that is much simpler than the complicated world used before:

%block simpler_block [E elt] [RH is-red E] {sd seed E} {clause has-rh sd RH}%.
%worlds (simpler_block) (has-rh _ _) %.
%total X (has-rh X _) %.

The proof of the main theorem can be stated more simply in this less complicated world:

%term _
  %pi (mix-pres (mix/reap Mix SEED) Ared (all-red/cons RH Ared'))
  %<- (has-rh SEED RH)
  %<- (mix-pres Mix Ared Ared') %.
%term _
  %pi (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') %.
%term _ mix-pres mix/nil all-red/nil all-red/nil %.
%worlds (simpler_block) (mix-pres _ _ _) %.
%total X (mix-pres X _ _) %.