Commit fb763c47 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'fractional_big_sepL2' into 'master'

Prove missing fractional_big_sepL2

See merge request iris/iris!737
parents 12925885 3162a652
......@@ -74,6 +74,7 @@ Coq 8.11 is no longer supported in this version of Iris.
only printed, not parsed): added a `,` before `ABORT`, for consistency with `COMM`.
* Add the lemmas `big_sepM_impl_strong` and `big_sepM_impl_dom_subseteq` that
generalize the existing `big_sepM_impl` lemma. (by Simon Friis Vindum)
* Add new instance `fractional_big_sepL2`. (by Paolo G. Giarrusso, BedRock Systems)
**Changes in `proofmode`:**
......
......@@ -77,13 +77,18 @@ Section fractional.
rewrite !assoc. f_equiv. by rewrite comm.
Qed.
Global Instance fractional_big_sepL {A} l Ψ :
( k (x : A), Fractional (Ψ k x))
Global Instance fractional_big_sepL {A} (l : list A) Ψ :
( k x, Fractional (Ψ k x))
Fractional (PROP:=PROP) (λ q, [ list] kx l, Ψ k x q)%I.
Proof. intros ? q q'. rewrite -big_sepL_sep. by setoid_rewrite fractional. Qed.
Global Instance fractional_big_sepL2 {A B} (l1 : list A) (l2 : list B) Ψ :
( k x1 x2, Fractional (Ψ k x1 x2))
Fractional (PROP:=PROP) (λ q, [ list] kx1; x2 l1; l2, Ψ k x1 x2 q)%I.
Proof. intros ? q q'. rewrite -big_sepL2_sep. by setoid_rewrite fractional. Qed.
Global Instance fractional_big_sepM `{Countable K} {A} (m : gmap K A) Ψ :
( k (x : A), Fractional (Ψ k x))
( k x, Fractional (Ψ k x))
Fractional (PROP:=PROP) (λ q, [ map] kx m, Ψ k x q)%I.
Proof. intros ? q q'. rewrite -big_sepM_sep. by setoid_rewrite fractional. Qed.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment