Fix bugs from listTovect about pumpkin-pi HOT 7 OPEN

Details: What happens is that one function (app, the way it is generated from the preprocessed version) gets lifted incorrectly, and then all of the other proofs that reference it fail. This is because the rules I have to deal with non-primitive projections in the code assume everything is fully eta-expanded, but there's a place the code isn't eta-expanding where it should be, so they don't run and app doesn't deal with non-primitive projections. Then later on proofs about app fail because projections aren't primitive.

from pumpkin-pi.

Partially fixed in a branch. The code needs to be smart enough to:

1. Fully eta expand in certain places (still breaking)
2. Repack all applications that result in the goal type

Fixing the second of these fixed 27/31 errors. Need to check performance and so on, and see if I can get the remaining 4. I'm not sure where the best place to repack is, generally. Non-primitive projections are annoying.

from pumpkin-pi.

2 more, so only 2 left.

These two were interesting. The SECTION/RETRACTION rules actually need to recurse too. We can think of these as recursing after vs. recursing before, I guess, but in terms of implementation there is no difference.

from pumpkin-pi.

To understand this, note that your eliminator might produce, say, a list of lists. And then in your lifted motive you'll end up with a forgotten sigT (vector (list A)). That's a nice start, but you want to make sure you lift the inner (list A) too.

from pumpkin-pi.

I set a one-day timeout for myself on this with respect to the camera ready, so unfortunately I'm going to call it with those last 2 failing cases still there. 2 is a lot better than 31. If I fix these after the camera ready and it turns out they are interesting like the last one, I'll post an errata on my website. My suspicion though is that these two are implementation errors, since they seem to revolve around mistakes in lazy eta expansion.

from pumpkin-pi.

The remaining 2 seem to be thanks to DEVOID not understand how to lift the implicit identity function when you have a hypothesis of type (list T * list T). Thus definitional equalities are not preserved in that case. This seems to happen with partition, so that lifted proofs about partition sometimes do not type check.

from pumpkin-pi.

Should check with renewed understanding of the limitations of matching and so on

from pumpkin-pi.