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

When running `iDestruct "H" as (?) "H"`, use the name of the binder in
"H". For example, if "H" has type `∃ y, Φ y`,  we now use `y` as the
name of the variable after freshening. Previously the name was always
the equivalent of running `fresh H`.

The implementation achieves this by forwarding the desired identifier
name through the `IntoExist` typeclass. Identifiers are serialized in
Gallina by using them as the name of a function of type `ident_name :=
unit -> unit`.

- all ascii notation is marked "only parsing" so this PR shouldn't
  change anything for anyone using only unicode notation.
- the algorithm for creating an ascii notation is pretty simple.
  - \ast -> *
  - \triangleright -> |>
  - \vee -> \/
  - \wedge -> /\
  - \forall -> forall
  - \exists -> exists
  - \ast -> **

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.

The unbounded fractional authoritative camera is a version of the fractional
authoritative camera that can be used with fractions `> 1`.

Most of the reasoning principles for this version of the fractional
authoritative cameras are the same as for the original version. There are two
difference:

- We get the additional rule that can be used to allocate a "surplus", i.e.
  if we have the authoritative element we can always increase its fraction
  and allocate a new fragment.

      ✓ (a ⋅ b) → ●U{p} a ~~> ●U{p + q} (a ⋅ b) ⋅ ◯U{q} b

- At the cost of that, we no longer have the `◯U{1} a` is an exclusive
  fragmental element (cf. `frac_auth_frag_validN_op_1_l`).