The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
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.
Concrete example:
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.