Skip to content

Stronger Persistent/Affine/Timeless results for big ops.

Robbert Krebbers requested to merge robbert/big_op_closed into master

Currently we have instances like the following for Persistent/Affine/Timeless for all big ops:

  Global Instance big_sepL_persistent Φ l :
    (∀ k x, Persistent (Φ k x)) → Persistent ([∗ list] k↦x ∈ l, Φ k x).

This MR adds stronger versions where the premise only needs to be proven for elements that are actually in the list/map/set:

Lemma big_sepL_persistent Φ l :
  (∀ k x, l !! k = Some x → Persistent (Φ k x)) →
  Persistent ([∗ list] k↦x ∈ l, Φ k x).

The stronger version is a lemma, since l !! k = Some x is useless for TC search. The instance is still there, but with a ' in its name.

To prove these lemmas, I added generic lemmas to prove closedness of big ops under a property. For example:

Lemma big_opL_closed (P : M → Prop) f l :
  P monoid_unit →
  (∀ x y, P x → P y → P (x `o` y)) →
  (∀ k x, l !! k = Some x → P (f k x)) →
  P ([^o list] k↦x ∈ l, f k x).

This lemma builds on !938 (merged)

Merge request reports