Jason (jcreed) wrote,

Found a stupid place in a stupid simple theorem where I can't remember how the induction measure is supposed to get smaller. This is almost certainly not be a bug in my system, since the gap in my proof applies just as well to basic LF, leading me to believe it's just me being dumb.


Oh, yeah, it seems I already dealt with this a while ago when I was trying to do proof irrelevance in canonical style. It's a terribly finicky issue with substitution being partial. I can prove [M/x][N/y]P = [[M/x]N/y][M/x]P if both sides are defined, (and y not free in M) but this isn't strong enough; for armed with that only it seems I need to invoke the induction hypotheses twice on the same thing, which potentially gets inductively bigger after the first hit. So I need some lemma that says conclusively that things are defined, not merely use definedness as a premise, and ugh, to really be thorough I will probably have to adapt this bullshit huge technical lemma from the irrelevant-canonical notes.

I shouldn't complain too much, though. I'd be worse off if I hadn't written them in the first place.


Eh. Went over the proof over dinner, seems to be fine, and moreover all the particulars seem familiar now that I see them again. It still is such a technical lemma that I fail to have any good intuition for why it should be true, though.
Tags: 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