Eliminating pure underneath an exists*

[nikswamy]

The checker eagerly eliminates pure _ in the vprop context, but only if the pure _ is not hidden beneath a binder. This leads to surprises, explaining the two surprises I commented on in PR #135

For example, test_elim_pure below fails, since Some?.v x is checked in a typing environment (the gamma part) that doesn't include Some? x.

fn test_elim_pure (x:option bool)
requires exists* q. q ** pure (Some? x)
ensures emp
{
    let v = Some?.v x;
    admit()
}

However, just asserting even a trivial pure causes the checker to open the existential and eliminate the pure _ and put its payload in gamma, allowing this to check.

fn test_elim_pure2 (x:option bool)
requires exists* q. q ** pure (Some? x)
ensures emp
{
    assert pure (True); //trivial to just open the exists
    let v = Some?.v x;
    admit()
}

Should we eagerly eliminate pure even when under a binder?

[nikswamy]

Part of what added to my confusion was that if you do:

fn test_elim_pure (x:option bool)
requires exists* q. q ** pure (Some? x)
ensures emp
{
    show_proof_state();
    let v = Some?.v x;
    admit()
}

then you see the proof state after the exists has been opened and the pure eliminated, in an attempt to prove the unprovable precondition of show_proof_state. Maybe show_proof_state should be a primitive directive that just prints the state and exits, without triggering and proof steps.