Tej Chajed authored 4 years ago and Robbert Krebbers committed 4 years ago

Addresses #315 for several tactics (`wp_alloc`, `wp_load`, `wp_store`,
`wp_free`).

Add IdempP instances for min_nat and max_nat.

Move additional numbers related lemmas and instances into the numbers file.

This is more consistent with other tac_wp tactics for HeapLang and also
a tiny bit more efficient, which is good to embody in the basic tactics
so derived code follows the same patterns.

Fixes #325.

Also added a tests for the various `iSpecialize` error cases involving
the `[%]` and `[//]` specialization patterns.

Gregory Malecha authored 4 years ago and Robbert Krebbers committed 4 years ago

- it doesn't seem to conflict with anything in Ltac

Thanks to @tchajed for the initial version of this proof.