Commit 3eb275ad authored by Ralf Jung's avatar Ralf Jung

add proof mode instances for array splitting

parent fd74b574
......@@ -155,6 +155,12 @@ Section tests.
by iApply "HΦ".
Qed.
Lemma test_array_app l vs1 vs2 :
l ↦∗ (vs1 ++ vs2) - l ↦∗ (vs1 ++ vs2).
Proof.
iIntros "[H1 H2]". iSplitL "H1"; done.
Qed.
End tests.
Section printing_tests.
......
......@@ -61,6 +61,25 @@ Proof.
rewrite drop_insert; last by lia. done.
Qed.
(** Proofmode instances *)
Global Instance into_sep_array_cons l vs v vs' :
IsCons vs v vs'
IntoSep (l ↦∗ vs) (l v) ((l + 1) ↦∗ vs').
Proof. rewrite /IsCons=>->. by rewrite /IntoSep array_cons. Qed.
Global Instance into_sep_array_app l vs vs1 vs2 :
IsApp vs vs1 vs2
IntoSep (l ↦∗ vs) (l ↦∗ vs1) ((l + length vs1) ↦∗ vs2).
Proof. rewrite /IsApp=>->. by rewrite /IntoSep array_app. Qed.
Global Instance from_sep_array_cons l vs v vs' :
IsCons vs v vs'
FromSep (l ↦∗ vs) (l v) ((l + 1) ↦∗ vs').
Proof. rewrite /IsCons=> ->. by rewrite /FromSep array_cons. Qed.
Global Instance from_sep_array_app l vs vs1 vs2 :
IsApp vs vs1 vs2
FromSep (l ↦∗ vs) (l ↦∗ vs1) ((l + length vs1) ↦∗ vs2).
Proof. rewrite /IsApp=> ->. by rewrite /FromSep array_app. Qed.
(** Allocation *)
Lemma mapsto_seq_array l v n :
([ list] i seq 0 n, (l + (i : nat)) v) -
......
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