From 12f8178f526aa74ccc41481410b75bb2a8f58d4e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 24 Sep 2017 22:46:00 +0200
Subject: [PATCH] Steps are preserved by permutations.

---
 opam                              |  2 +-
 opam.pins                         |  2 +-
 theories/program_logic/language.v | 10 ++++++++++
 3 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/opam b/opam
index 74cfc66fd..042694642 100644
--- a/opam
+++ b/opam
@@ -12,5 +12,5 @@ remove: ["sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris'"]
 depends: [
   "coq" { >= "8.6.1" & < "8.8~" }
   "coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2017-09-21.2") | (= "dev") }
+  "coq-stdpp" { (= "dev.2017-09-24.0") | (= "dev") }
 ]
diff --git a/opam.pins b/opam.pins
index 7034b4457..6bdd007ff 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 2f9f3d3f28aa568f5cbee1be5699f163800491c0
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 4ea9c34a9c58a13aae97b4cc7f75fc862bdfcc7c
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index a4e9cf079..6dc76129c 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -83,4 +83,14 @@ Section language.
   Lemma irreducible_fill `{LanguageCtx Λ K} e σ :
     to_val e = None → irreducible e σ → irreducible (K e) σ.
   Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
+
+  Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 :
+    t1 ≡ₚ t1' → step (t1,σ1) (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ step (t1',σ1) (t2',σ2).
+  Proof.
+    intros Ht [e1 σ1' e2 σ2' efs tl tr ?? Hstep]; simplify_eq/=.
+    move: Ht; rewrite -Permutation_middle (symmetry_iff (≡ₚ)).
+    intros (tl'&tr'&->&Ht)%Permutation_cons_inv.
+    exists (tl' ++ e2 :: tr' ++ efs); split; [|by econstructor].
+    by rewrite -!Permutation_middle !assoc_L Ht.
+  Qed.
 End language.
-- 
GitLab