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

  • (no subject)

    Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

  • (no subject)

    Did some personal archaeology. Helped a little with laundry. Threw some chicken, onions, tomato, stock, peppers in the slow cooker and hopefully…

  • (no subject)

    Dinner with akiva and dannel at nuevo portal in carroll gardens. Ate a pile of chicken stew and rice and beans and maduros, good times. I do miss…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded