Unfolding terms created with `assert` in Coq

Question

The proof in question can be found here. At the current state, I would like to unfold eqvid and eqvneg in hypothesis eqveq, in order to simplify the projection and obtain a contradictory equality between two different functions. However, these two terms were synthesized as subgoals using the assert tactic, and it seems that the current environment bears no memory of the values of the terms. I know that I could write the two terms manually, but that would be quite cumbersome in my opinion. Is there a more elegant way to recover the definitions generated in solving the subgoals?

Answer 1

Incant:

unshelve epose (eqvid := _ : isequiv bool bool).

pose/set are transparent while assert is not. The _ becomes a new existential variable (or unification variable in more standard parlance). A normal pose would fail because it can't solve for the variable, but epose skips the check. Existential variables aren't usually attacked by tactics directly (they are solved for by unification), so they are automatically shelved, but unshelve takes all the evars made by the tactic it controls and turns them into goals.

Replace the asserts with this (you could make a custom notation if you wanted) and

apply (f_equal (fun f => f false)) in eqveq.
discriminate.

finishes your proof.

Note that the proof state gets rapidly unreadable if you do this. A trick to avoid that is to have

Definition hidden {A} {x : A} : A := x.

And use

unshelve epose (eqvid := hidden : isequiv bool bool).

instead. Then the hypotheses will not show the messy term until you reveal it.