Commit 982a55c7 authored by Robbert Krebbers's avatar Robbert Krebbers

Proof mode class instances for `big_sepL2`.

All those for `big_sepL` that hold.
parent 76812039
......@@ -548,6 +548,28 @@ Global Instance from_and_big_sepL_app_persistent {A} (Φ : nat → A → PROP) l
([ list] k y l1, Φ k y) ([ list] k y l2, Φ (length l1 + k) y).
Proof. rewrite /IsApp=> -> ?. by rewrite /FromAnd big_sepL_app persistent_and_sep_1. Qed.
Global Instance from_and_big_sepL2_cons_persistent {A B}
(Φ : nat A B PROP) l1 x1 l1' l2 x2 l2' :
IsCons l1 x1 l1' IsCons l2 x2 l2'
Persistent (Φ 0 x1 x2)
FromAnd ([ list] k y1;y2 l1;l2, Φ k y1 y2)
(Φ 0 x1 x2) ([ list] k y1;y2 l1';l2', Φ (S k) y1 y2).
Proof.
rewrite /IsCons=> -> -> ?.
by rewrite /FromAnd big_sepL2_cons persistent_and_sep_1.
Qed.
Global Instance from_and_big_sepL2_app_persistent {A B}
(Φ : nat A B PROP) l1 l1' l1'' l2 l2' l2'' :
IsApp l1 l1' l1'' IsApp l2 l2' l2''
( k y1 y2, Persistent (Φ k y1 y2))
FromAnd ([ list] k y1;y2 l1;l2, Φ k y1 y2)
([ list] k y1;y2 l1';l2', Φ k y1 y2)
([ list] k y1;y2 l1'';l2'', Φ (length l1' + k) y1 y2).
Proof.
rewrite /IsApp=> -> -> ?. rewrite /FromAnd persistent_and_sep_1.
apply wand_elim_l', big_sepL2_app.
Qed.
(** FromSep *)
Global Instance from_sep_sep P1 P2 : FromSep (P1 P2) P1 P2 | 100.
Proof. by rewrite /FromSep. Qed.
......@@ -587,6 +609,20 @@ Global Instance from_sep_big_sepL_app {A} (Φ : nat → A → PROP) l l1 l2 :
([ list] k y l1, Φ k y) ([ list] k y l2, Φ (length l1 + k) y).
Proof. rewrite /IsApp=> ->. by rewrite /FromSep big_opL_app. Qed.
Global Instance from_sep_big_sepL2_cons {A B} (Φ : nat A B PROP)
l1 x1 l1' l2 x2 l2' :
IsCons l1 x1 l1' IsCons l2 x2 l2'
FromSep ([ list] k y1;y2 l1;l2, Φ k y1 y2)
(Φ 0 x1 x2) ([ list] k y1;y2 l1';l2', Φ (S k) y1 y2).
Proof. rewrite /IsCons=> -> ->. by rewrite /FromSep big_sepL2_cons. Qed.
Global Instance from_sep_big_sepL2_app {A B} (Φ : nat A B PROP)
l1 l1' l1'' l2 l2' l2'' :
IsApp l1 l1' l1'' IsApp l2 l2' l2''
FromSep ([ list] k y1;y2 l1;l2, Φ k y1 y2)
([ list] k y1;y2 l1';l2', Φ k y1 y2)
([ list] k y1;y2 l1'';l2'', Φ (length l1' + k) y1 y2).
Proof. rewrite /IsApp=>-> ->. apply wand_elim_l', big_sepL2_app. Qed.
Global Instance from_sep_bupd `{BiBUpd PROP} P Q1 Q2 :
FromSep P Q1 Q2 FromSep (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
......@@ -728,6 +764,14 @@ Global Instance into_sep_big_sepL_app {A} (Φ : nat → A → PROP) l l1 l2 :
([ list] k y l1, Φ k y) ([ list] k y l2, Φ (length l1 + k) y).
Proof. rewrite /IsApp=>->. by rewrite /IntoSep big_sepL_app. Qed.
(* No instance for app, since that only works when the LHSs have the same length *)
Global Instance into_sep_big_sepL2_cons {A B}
(Φ : nat A B PROP) l1 x1 l1' l2 x2 l2' :
IsCons l1 x1 l1' IsCons l2 x2 l2'
IntoSep ([ list] k y1;y2 l1;l2, Φ k y1 y2)
(Φ 0 x1 x2) ([ list] k y1;y2 l1';l2', Φ (S k) y1 y2).
Proof. rewrite /IsCons=>-> ->. by rewrite /IntoSep big_sepL2_cons. Qed.
(** FromOr *)
Global Instance from_or_or P1 P2 : FromOr (P1 P2) P1 P2.
Proof. by rewrite /FromOr. Qed.
......
......@@ -606,6 +606,14 @@ Proof.
rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
rewrite big_opL_commute. by apply big_sepL_mono.
Qed.
Global Instance into_laterN_big_sepL2 n {A B} (Φ Ψ : nat A B PROP) l1 l2 :
( x1 x2 k, IntoLaterN false n (Φ k x1 x2) (Ψ k x1 x2))
IntoLaterN false n ([ list] k y1;y2 l1;l2, Φ k y1 y2)
([ list] k y1;y2 l1;l2, Ψ k y1 y2).
Proof.
rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
rewrite -big_sepL2_laterN_2. by apply big_sepL2_mono.
Qed.
Global Instance into_laterN_big_sepM n `{Countable K} {A}
(Φ Ψ : K A PROP) (m : gmap K A) :
( x k, IntoLaterN false n (Φ k x) (Ψ k x))
......
......@@ -89,7 +89,21 @@ Global Instance frame_big_sepL_app {A} p (Φ : nat → A → PROP) R Q l l1 l2 :
Frame p R (([ list] k y l1, Φ k y)
[ list] k y l2, Φ (length l1 + k) y) Q
Frame p R ([ list] k y l, Φ k y) Q.
Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
Proof. rewrite /IsApp=>->. by rewrite /Frame big_sepL_app. Qed.
Global Instance frame_big_sepL2_cons {A B} p (Φ : nat A B PROP)
R Q l1 x1 l1' l2 x2 l2' :
IsCons l1 x1 l1' IsCons l2 x2 l2'
Frame p R (Φ 0 x1 x2 [ list] k y1;y2 l1';l2', Φ (S k) y1 y2) Q
Frame p R ([ list] k y1;y2 l1;l2, Φ k y1 y2) Q.
Proof. rewrite /IsCons=>-> ->. by rewrite /Frame big_sepL2_cons. Qed.
Global Instance frame_big_sepL2_app {A B} p (Φ : nat A B PROP)
R Q l1 l1' l1'' l2 l2' l2'' :
IsApp l1 l1' l1'' IsApp l2 l2' l2''
Frame p R (([ list] k y1;y2 l1';l2', Φ k y1 y2)
[ list] k y1;y2 l1'';l2'', Φ (length l1' + k) y1 y2) Q
Frame p R ([ list] k y1;y2 l1;l2, Φ k y1 y2) Q.
Proof. rewrite /IsApp /Frame=>-> -> ->. apply wand_elim_l', big_sepL2_app. Qed.
Global Instance make_and_true_l P : KnownLMakeAnd True P P.
Proof. apply left_id, _. Qed.
......
......@@ -2091,6 +2091,8 @@ Hint Extern 0 (envs_entails _ (_ ≡ _)) =>
rewrite envs_entails_eq; apply bi.internal_eq_refl.
Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
rewrite envs_entails_eq; apply big_sepL_nil'.
Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
rewrite envs_entails_eq; apply big_sepL2_nil'.
Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
rewrite envs_entails_eq; apply big_sepM_empty'.
Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
......
Markdown is supported
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