Output factoring

When checking coverage of metatheorems, a common problem arises because the output coverage checker only considers each rule in isolation. The proof transformation technique for addressing this problem is known as output factoring.

The primary symptom of the problem is if STELF fails when checking an %total declaration and gives this sort of error:

Totality: Output of subgoal not covered
Output coverage error ...

Even and odd

In this section, we prove that every natural number is even or odd. First, we define the judgements:

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort odd {_ nat} %.
%sort even {_ nat} %.
%term z-e even z %.
%term s-o %pi (odd (s X)) %<- (even X) %.
%term s-e %pi (even (s X)) %<- (odd X) %.
%sort even_or_odd {_ nat} %.
%term eoo-e %pi (even_or_odd X) %<- (even X) %.
%term eoo-o %pi (even_or_odd X) %<- (odd X) %.

Incorrect proof

Next, we attempt the following theorem:

%sort always_even_or_odd {N nat} {_ even_or_odd N} %.
%mode always_even_or_odd %in %out %.
%term aeo_zero always_even_or_odd z (eoo-e z-e) %.
%term aeo_even
  %pi (always_even_or_odd (s X) (eoo-e (s-e Y)))
  %<- (always_even_or_odd X (eoo-o Y)) %.
%term aeo_odd
  %pi (always_even_or_odd (s X) (eoo-o (s-o Y)))
  %<- (always_even_or_odd X (eoo-e Y)) %.
%worlds () (always_even_or_odd D P) %.
%total D (always_even_or_odd D _) %.

Unfortunately, the totality check fails.

The line number in STELF’s error message points to the premise of aeo_even. The output of always_even_or_odd can be either eoo-o _ or eoo-e _, but this premise pattern-matches as if the output is always eoo-o _. The constant aeo_odd covers the alternative case when the output is eoo-e _.

Unfortunately, STELF’s output-coverage checker does not notice this sort of multiple-constant output coverage: the output-coverage checker only accepts a relation if each constant covers all outputs of its premises.

Correct proof

Nonetheless, we need to case-analyze this output in order to complete the proof. How can we do so? Well, STELF does not allow output coverage to be split across constants, but it certainly allows input coverage to be split across constants. Thus, we can solve the problem by turning an output-coverage checking problem into an input-coverage checking problem. We do this by writing an additional helper lemma.

Looking at what the two constants do with the output of the inductive call, we can see that in each case they turn a derivation of even_or_odd X into a derivation of even_or_odd (s X)—it’s just that they do it differently depending on what the output is. Thus, we factor this reasoning into a lemma:

%sort lemma {_ even_or_odd X} {_ even_or_odd (s X)} %.
%mode lemma %in %out %.
%term _ lemma (eoo-o Y) (eoo-e (s-e Y)) %.
%term _ lemma (eoo-e Y) (eoo-o (s-o Y)) %.
%worlds () (lemma _ _) %.
%total X (lemma X _) %.

Using this lemma, we complete the proof as follows:

%sort always_even_or_odd {N nat} {_ even_or_odd N} %.
%mode always_even_or_odd %in %out %.
%term aeo_zero always_even_or_odd z (eoo-e z-e) %.
%term aeo_succ %pi (always_even_or_odd (s X) D') %<- (always_even_or_odd X D) %<- (lemma D D') %.
%worlds () (always_even_or_odd D P) %.
%total D (always_even_or_odd D _) %.

Progress

Another example where output factoring comes up is the progress theorem for a programming language:

If $\mathsf{}e : \tau$ then $e \; \mathsf{value}$ or $e \mapsto e'$.

A typical case of progress makes an inductive call on a subderivation and then case-analyzes whether the result is a value or takes a step. This reasoning must be factored off into lemmas to avoid output coverage problems.

Using the simply typed λ-calculus defined in Representing the judgements of the STLC, we now show how output factoring is used to prove progress. For review, here is the LF signature for the STLC:

%% Syntax
%sort tp %.
%term unit tp %.
%term arrow %pi tp %-> tp %-> tp %.
%sort tm %.
%term empty tm %.
%term lam %pi tp %-> (%pi tm %-> tm) %-> tm %.
%term app %pi tm %-> tm %-> tm %.
%% Static Semantics
%sort of {_ tm} {_ tp} %.
%term of_empty of empty unit %.
%term of_lam %pi (of (lam T2 ([x] E x)) (arrow T2 T)) %<- ({x tm} {dx of x T2} of (E x) T) %.
%term of_app %pi (of (app E1 E2) T) %<- (of E2 T2) %<- (of E1 (arrow T2 T)) %.
%% Dynamic Semantics
%sort value {_ tm} %.
%term value_empty value empty %.
%term value_lam value (lam T2 ([x] E x)) %.
%sort step {_ tm} {_ tm} %.
%term step_app_1 %pi (step (app E1 E2) (app E1' E2)) %<- (step E1 E1') %.
%term step_app_2 %pi (step (app E1 E2) (app E1 E2')) %<- (step E2 E2') %<- (value E1) %.
%term step_app_beta %pi (step (app (lam T2 ([x] E x)) E2) (E E2)) %<- (value E2) %.

The result of progress is represented by the following sum type:

%sort val_or_step {_ tm} %.
%term vos_val %pi (val_or_step E) %<- (value E) %.
%term vos_step %pi (val_or_step E) %<- (step E E') %.

As discussed above, we first prove a factoring lemma that does all the work after the inductive call of the application case:

%sort progress/app {_ of E1 (arrow T2 T)} {_ val_or_step E1} {_ val_or_step E2} {_ val_or_step (app E1 E2)} %.
%mode progress/app %in %in %in %out %.
%term pa_step_1 progress/app _ (vos_step DstepE1) _ (vos_step (step_app_1 DstepE1)) %.
%term pa_val_1_step_2 progress/app _ (vos_val DvalE1) (vos_step DstepE2) (vos_step (step_app_2 DvalE1 DstepE2)) %.
%term pa_val_val progress/app (%the (of (lam T2' ([x] E x)) (arrow T2 T)) DofE1) (vos_val (%the (value (lam T2' ([x] E x))) DvalE1)) (vos_val DvalE2) (vos_step (step_app_beta DvalE2)) %.
%worlds () (progress/app _ _ _ _) %.
%total {} (progress/app _ _ _ _) %.

We give this lemma the typing derivation for E1 so that we can learn in the case pa_val_val that the E1 is a lam, which is necessary to apply step_app_beta. Note that there is no need for an explicit value inversion/canonical forms lemma: in the case pa_val_val, we simply assume that E1 is a lam, and the coverage checker justifies this assumption because it is both a value and has type arrow T2 T.

Using this lemma, the proof of progress is quite simple:

%sort progress {_ of E T} {_ val_or_step E} %.
%mode progress %in %out %.
%term prog_empty progress of_empty (vos_val value_empty) %.
%term prog_lam progress (of_lam ([x] [dx] DofE x dx)) (vos_val value_lam) %.
%term prog_app
  %pi (progress (of_app (%the (of E1 (arrow T2 T)) DofE1) (%the (of E2 T2) DofE2)) DvosApp)
  %<- (progress DofE1 (%the (val_or_step E1) DvosE1))
  %<- (progress DofE2 (%the (val_or_step E2) DvosE2))
  %<- (progress/app DofE1 DvosE1 DvosE2 DvosApp) %.
%worlds () (progress _ _) %.
%total D (progress D _) %.