From 3eb275ad344924d5cc223cfddfdd7e034d25895c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 7 Aug 2019 18:01:15 +0200
Subject: [PATCH] add proof mode instances for array splitting

---
 tests/heap_lang.v          |  6 ++++++
 theories/heap_lang/array.v | 19 +++++++++++++++++++
 2 files changed, 25 insertions(+)

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 4f55ecbdd..9d7f906bb 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -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.
diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index d046a9932..c7dee7696 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -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) -∗
-- 
GitLab