Output factoring

From The Twelf Project
Jump to: navigation, search

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

nat : type.
z : nat.
s : nat -> nat.

odd : nat -> type.
even : nat -> type. 

z-e : even z.
s-o : odd (s X) <- even X.
s-e : even (s X) <- odd X.

even_or_odd : nat -> type. 

eoo-e : even_or_odd X <- even X.
eoo-o : even_or_odd X <- odd X.

Incorrect proof

Next, we attempt the following theorem:

always_even_or_odd : {N:nat} even_or_odd N -> type.
%mode always_even_or_odd +D -P.   

aeo_zero : always_even_or_odd z (eoo-e z-e). 

aeo_even : always_even_or_odd (s X) (eoo-e (s-e Y))
	    <- always_even_or_odd X (eoo-o Y).

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

Unfortunately, totality check fails:

%total D (always_even_or_odd D _).
See Twelf's output

The line number in Twelf'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, Twelf'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, Twelf 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:

lemma : even_or_odd X -> even_or_odd (s X) -> type.
%mode lemma +X -Y. 
- : lemma (eoo-o Y) (eoo-e (s-e Y)).
- : lemma (eoo-e Y) (eoo-o (s-o Y)).
%worlds () (lemma _ _). 
%total X (lemma X _).

Using this lemma, we complete the proof as follows:

always_even_or_odd : {N:nat} even_or_odd N -> type.
%mode always_even_or_odd +D -P.   

aeo_zero : always_even_or_odd z (eoo-e z-e). 

aeo_succ : 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 _).
See Twelf's output

Progress

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

If then or .

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 in the tutorial Proving metatheorems with Twelf, we now show how output factoring is used to prove progress. For review, here is the LF signature for the STLC:

%% Syntax
tp    : type.

unit  : tp.
arrow : tp -> tp -> tp.

tm    : type.
empty : tm.
lam   : tp -> (tm -> tm) -> tm.
app   : tm -> tm -> tm.

%% Static Semantics 

of       : tm -> tp -> type.
of_empty : of empty unit.
of_lam   : of (lam T2 ([x] (E x))) (arrow T2 T)
            <- ({x:tm} {dx : of x T2} of (E x) T).
of_app   : of (app E1 E2) T
            <- of E2 T2
            <- of E1 (arrow T2 T).

%% Dynamic Semantics

value       : tm -> type.
value_empty : value empty.
value_lam   : value (lam T2 ([x] E x)).
             
step          : tm -> tm -> type.
step_app_1    : step (app E1 E2) (app E1' E2)
                 <- step E1 E1'.
step_app_2    : step (app E1 E2) (app E1 E2')
                 <- step E2 E2'
                 <- value E1.

step_app_beta : step (app (lam T2 ([x] E x)) E2) (E E2)
                 <- value E2.

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

val_or_step : tm -> type.
vos_val : val_or_step E
           <- value E.
vos_step : 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:

progress/app : of E1 (arrow T2 T)
                -> val_or_step E1
                -> val_or_step E2
                -> val_or_step (app E1 E2)
                -> type.
%mode progress/app +DofE1 +DvosE1 +DvosE2 -DvosApp.

pa_step_1 : progress/app 
             _
             (vos_step DstepE1)
             _
             (vos_step (step_app_1 DstepE1)).

pa_val_1_step_2 : progress/app
                   _
                   (vos_val DvalE1)
                   (vos_step DstepE2)
                   (vos_step (step_app_2 DvalE1 DstepE2)).

pa_val_val : progress/app
              (DofE1 : of (lam T2' ([x] E x)) (arrow T2 T))
              (vos_val 
                 (DvalE1 : value (lam T2' ([x] E x))))
              (vos_val DvalE2)
              (vos_step (step_app_beta DvalE2)).
              
%worlds () (progress/app _ _ _ _).
%total {} (progress/app _ _ _ _).
See Twelf's output

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:

progress : of E T -> val_or_step E -> type. 
%mode progress +Dof -Dvos.

prog_empty : progress of_empty (vos_val value_empty).

prog_lam : progress (of_lam ([x] [dx] DofE x dx)) (vos_val value_lam).

prog_app : progress (of_app (DofE1 : of E1 (arrow T2 T)) 
                            (DofE2 : of E2 T2))
            DvosApp
            <- progress DofE1 (DvosE1 : val_or_step E1)
            <- progress DofE2 (DvosE2 : val_or_step E2)
            <- progress/app DofE1 DvosE1 DvosE2 DvosApp.

%worlds () (progress _ _).             
%total D (progress D _).
See Twelf's output

Read more Twelf tutorials and other Twelf documentation.