Undesired simplification behaviour of big_sepM2
Iris version: dev.2019-11-22.2.a979391c
simpl unfolds the definition of big_sepM2 which makes it basically unusable.
Example:
From iris.program_logic Require Import weakestpre.
Example big_sepM2_simpl Σ (xs ys : gmap nat nat):
([∗ map] x;y ∈ xs;ys, ⌜x=y⌝ : iProp Σ)%I.
Proof. simpl. Abort.
(* => uPred_and ⌜∀ k : nat, is_Some (xs !! k) ↔ is_Some (ys !! k)⌝
([∗ map] xy ∈ map_zip xs ys, ⌜xy.1 = xy.2⌝%I) *)I am currently using the following workaround (big_sepM2 does not seem to have an Arguments command at the moment):
Arguments big_sepM2 {PROP K _ _ A B} _ !_ !_ /.
Example big_sepM2_simpl Σ (xs ys : gmap nat nat):
([∗ map] x;y ∈ xs;ys, ⌜x=y⌝ : iProp Σ)%I.
Proof. simpl. Abort.
(* => ([∗ map] x;y ∈ xs;ys, ⌜x = y⌝)%I *)