Jason (jcreed) wrote,

The twelf road is bumpy today. I stated at least one lemma that turned out to be false, and now I'm struggling with how to actually convince twelf of something very simple and almost assuredly true. It comes out of the wash as a coverage error; I'm doing a lambda case of a type preservation theorem of sorts, and there's some fiddly little thing about the worlds (in the object logic "modal world" not the metalogic "regular world" sense) lining up right around the binders. Grr.

Here's the problem, essentially:
tm : type.
w : type.
hyp : tm -> w -> type.
good : type.

fact : ({x}{a} hyp x a -> good)
	 -> ({a:w} good).

easy : ({x}{a} hyp x a -> good)
	 -> {{a:w} good)
	 -> type.
hard :     ({x}{a} hyp x a -> {y} hyp y (Q a) -> good)
	-> (   {a}            {y} hyp y (Q a) -> good)
	-> type.

"easy" should be easy to prove, by using "fact". For "hard", however, I want to hypothesize y : tm and pf : hyp y (Q a) and then appeal to "easy" as a lemma, but I don't have access to a! If I try

hard_proof : hard HYP1 HYP2
             <- ({y}{pf:hyp y _} easy ([x][a][h] HYP1 x a h y pf) ([a] HYP2 a y pf)).

then the underscore is reconstructed as merely a first-order Q, without any dependencies, of course, on the a that isn't even in its scope.
Tags: angst, work

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded