Commit 9e8004f8 authored by Ralf Jung's avatar Ralf Jung

prepare for having fractional arrays in the future

parent 3eb275ad
......@@ -86,6 +86,16 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
--------------------------------------∗
WP "x" {{ _, True }}
The command has indeed failed with message:
In nested Ltac calls to "iIntros (constr)", "iIntros_go",
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
"iAndDestruct (constr) as (constr) (constr)", last call failed.
Tactic failure: iAndDestruct: cannot destruct (l ↦∗ (vs1 ++ vs2))%I.
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: (l ↦∗ (vs1 ++ vs2))%I not a separating conjunction.
1 subgoal
Σ : gFunctors
......
......@@ -158,7 +158,10 @@ Section tests.
Lemma test_array_app l vs1 vs2 :
l ↦∗ (vs1 ++ vs2) - l ↦∗ (vs1 ++ vs2).
Proof.
iIntros "[H1 H2]". iSplitL "H1"; done.
Fail iIntros "[H1 H2]". (* this should, one day, split at the fraction. *)
iIntros "H". iDestruct (array_app with "H") as "[H1 H2]".
Fail iSplitL "H1".
iApply array_app. iSplitL "H1"; done.
Qed.
End tests.
......
......@@ -61,24 +61,8 @@ 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.
(** No [FromSep] or [IntoSep] instances to remain forwards compatible with a
fractional array assertion, that will split the fraction, not the list. *)
(** Allocation *)
Lemma mapsto_seq_array l v n :
......@@ -240,3 +224,5 @@ Proof.
Qed.
End lifting.
Typeclasses Opaque array.
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