Add array_copy to heap_lang

Closes #293

See merge request iris/iris!379

Tej Chajed authored 5 years ago and Ralf Jung committed 5 years ago

Add array_copy_to (copy in-place to destination array) and array_clone
(copy to a freshly allocated array). The heap_lang spec and proof for
array_copy_to are inspired by
https://gitlab.mpi-sws.org/iris/lambda-rust/blob/3b4ae69fa3be1344245245bf05e5e80e790e064d/theories/lang/lib/memcpy.v.

Fixes #293.

Derive WP lifting and array rules from TWP rules

See merge request iris/iris!383

- Export `total_weakestpre` in `lifting` already, like we do for `weakestpre`.
- Do not export modules that are already exported by exported modules.

Fix wp_alloc when applying twp_allocN

See merge request iris/iris!382

Add ownership fraction to array assertion

See merge request iris/iris!380

say things about modalities

See merge request iris/iris!377

Add introduction pattern `-# pat` to move a hypothesis to the spatial context

Closes #213

See merge request iris/iris!370

It was already marked as deprecated in `doc/proof_mode.md`.

- Rename `IPureElim` -> `iPure`, `IAlwaysElim` -> `IIntuitionistic`
- Drop `IAlwaysIntro` (it's just `IModalIntro`).

Remove useless implicit annotation on binder

See merge request iris/iris!376

Tej Chajed authored 5 years ago and Ralf Jung committed 5 years ago

Fixes a new warning on Coq 8.12+alpha when implicit annotations are used
in positions where they are ignored.

Adding a constructor for reflexive transitive closures into bi's

See merge request iris/iris!375