Manipulating proof witnesses as inputs

From The Twelf Project
Jump to: navigation, search

Christopher asks...

There are things which I can express as a sequence of two "%solve" commands that I can't express in one: e.g.

%solve A : foo.
%solve B : bar A.

I'd like to be able to write a type quux which combines the two searches, like:

quux : { A : foo } bar A -> type.
%mode quux -A -B.
quux_con : { A : foo } { B : foo A } quux A B
% or maybe if there was syntax like
% quux_con2 : quux A B <- A : foo <- B : foo A

Response

I believe what you want to do is doable - you were on the right track with introducing A as an explicit parameter here. However, I would caution you against what you're suggesting, because - as far as I know, what you're asking requires essentially duplicating your entire program as effectiveness lemmas.

I had trouble working out what the meaning of the example was based on abstract examples, so included the natural numbers with plus. We also encode the metatheorem for the commutivity of plus, but we're not interested in the fact that it is a metatheorem here - plus here is our analog for foo above, and so plus-comm is our bar.

plus-comm : plus A B C -> plus B A C -> type.
%mode plus-comm +A -B.

plus-comm/z : plus-comm plus/z (D: plus N z N)
               <- plus-zero N D.
plus-comm/s : plus-comm (plus/s D1) D2
               <- plus-comm D1 D3
               <- plus-succ D3 D2.

If you want to see the code leading up to that point, you can see it here.

Now, in our example, we have a new version of the first code example:

ERROR: option 'noinclude' deprecated or invalid
%solve derivA : plus (s (s z)) (s z) _.
%solve derivB : plus-comm derivA C.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%solve plus (s (s z)) (s z) X1. OK derivA : plus (s (s z)) (s z) (s (s (s z))) = plus/s (plus/s plus/z). %solve plus-comm derivA C. OK derivB : plus-comm derivA (plus/s plus/z) = plus-comm/s (plus-succ/s plus-succ/z) (plus-comm/s (plus-succ/s plus-succ/z) (plus-comm/z (plus-zero/s plus-zero/z))).

%% OK %%

As far as I can tell, the equivalent of your relation above in my example is one that takes two natural numbers A and B and produces

  • The natural number C that is the sum of A and B
  • A derivation D of plus A B C
  • A derivation of the commuted sum D', i.e. plus B A C
  • A derivation of plus-comm D D' of that

This is realized in the following relation:

twoplus : {A}{B}{C}{D: plus A B C}{D': plus B A C} plus-comm D D' -> type.
%mode twoplus +A +B -C -D -D' -D''.

Lots of effectiveness lemmas

In order to get what we want, we are going to have to encode a bunch of effectiveness lemmas—not having written them those may have been what was giving you trouble before. In your example you seem to indicate that the relations you were working with were not necessarily total relations from inputs to outputs - if that is the case, then you will define what could more accurately be called effectiveness relations. What effectiveness lemmas/relations do is express how to build a proof witness given certain inputs - in some sense making the proof search process explicit rather than letting %solve handle it.

Our effectivness lemma for plus looks like this. Pay careful attention to what is an input and what is an output.

can-plus : {A}{B}{C} plus A B C -> type.
%mode can-plus +A +B -C -D.

can-plus/z : can-plus z B B plus/z.

can-plus/s : can-plus (s A) B (s C) (plus/s D)
              <- can-plus A B C D.

%worlds () (can-plus _ _ _ _).
%total T (can-plus T _ _ _).

The totality checks on these and the other effectiveness lemmas are just a sanity check here - this technique would work even if you were working with relations which were not total. As before, I will skip over the effectivenes lemmas for plus-zero and plus-succ and skip to the proof for

can-plus-comm : {D: plus A B C}{D': plus B A C} plus-comm D D' -> type.
%mode can-plus-comm +D -D' -DC.

can-plus-comm/z : can-plus-comm plus/z (D: plus N z N) (plus-comm/z DZ)
		   <- can-plus-zero N D (DZ: plus-zero N D).

can-plus-succ/s : can-plus-comm (plus/s D) D'' (plus-comm/s DS DC)
		   <- can-plus-comm D D' DC
		   <- can-plus-succ D' D'' DS.

%worlds () (can-plus-comm _ _ _).
%total T (can-plus-comm T _ _).

To see all of the code with effectiveness lemmas included, click here.

Putting together the twoplus relation

Now that we have all the effectiveness lemmas we could ever need or want, it is relatively simple to define twoplus. Furthermore, because we established totality of plus and plus-comm, it is simple to establish totality of twoplus.

twoplus : {A}{B}{C}{D: plus A B C}{D': plus B A C} plus-comm D D' -> type.
%mode twoplus +A +B -C -D -D' -D''.

twoplus/i : twoplus A B C D D' DC
             <- can-plus A B C D
	     <- can-plus-comm D D' DC.

%worlds () (twoplus _ _ _ _ _ _).
%total {} (twoplus _ _ _ _ _ _).

You can see all the code or see Twelf's response to checking it.

Side note about %define

As a side note, look at Twelf's output when we solved %solve B : plus-comm A C. It didn't allow us to see the type of C, and it didn't allow us to use C later in the program. We can bind outputs of functions and use them later in the signature by using %define, as the following example shows:

%solve deriv1 : plus (s (s z)) (s z) _.
%define deriv2 = C 
%solve deriv3 : plus-comm deriv1 C.

test = plus/s deriv2.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%solve plus (s (s z)) (s z) X1. OK deriv1 : plus (s (s z)) (s z) (s (s (s z))) = plus/s (plus/s plus/z). %solve plus-comm deriv1 C. OK deriv2 : plus (s z) (s (s z)) (s (s (s z))) = plus/s plus/z. deriv3 : plus-comm deriv1 (plus/s plus/z) = plus-comm/s (plus-succ/s plus-succ/z) (plus-comm/s (plus-succ/s plus-succ/z) (plus-comm/z (plus-zero/s plus-zero/z))). test : plus (s (s z)) (s (s z)) (s (s (s (s z)))) = plus/s deriv2.

%% OK %%