Using wp_ tactics without making every tiny step a function is super slow solely because Coq has to keep proving this Closed obligation
Which would be fine, except that there is no good way right now to prove closed-ness under a binder without knowing string literals for the variable names.
Definition big_blob_of_code x := (* huge blob of code here *)%E. Definition foo: val := (λ: [ "x"; "y" ], big_blob_of_code "x" + big_blob_code "y").
I don't want big_blob_of_code to be a function (because it isn't in the source code, and I'd like to actually verify foo as written rather than some other thing). However, Coq takes far too long to execute
wp_rec on my
foo-like thing, and it only gets worse the more times it is called. It also requires an irritating number of rewrites. There may be some ways around this if you happen to have some closed values somewhere up the stack and use
Notation for previous ones, with a typeclass instance for
Closed for those functions, but even that is highly annoying, and proving
Closed for any of the lower-level functions doesn't really work because of the way
solve_closed is defined (and according to Janno, probably just can't work at all).
I don't really care what solution this has, just that there is one.