From cc62f6c066bb6ee253e479a21d4ba3a7e883ccba Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Oct 2014 20:08:43 -0400
Subject: [PATCH] Stronger completeness proof for the executable semantics.

The proof now uses the stronger notion of memory permutation instead of a more
general memory refinement. We have also proven that memory permutations are
symmetric.
---
 theories/ars.v      |  2 ++
 theories/fin_maps.v | 19 ++++++++++++++-----
 2 files changed, 16 insertions(+), 5 deletions(-)

diff --git a/theories/ars.v b/theories/ars.v
index 43d18c23..679537ba 100644
--- a/theories/ars.v
+++ b/theories/ars.v
@@ -48,6 +48,8 @@ Section definitions.
     | ex_loop_do_step x y : R x y → ex_loop y → ex_loop x.
 End definitions.
 
+Hint Unfold nf red.
+
 (** * General theorems *)
 Section rtc.
   Context `{R : relation A}.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index a91b201f..f4b7567f 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -444,14 +444,23 @@ Lemma map_to_list_unique {A} (m : M A) i x y :
 Proof. rewrite !elem_of_map_to_list. congruence. Qed.
 Lemma NoDup_fst_map_to_list {A} (m : M A) : NoDup (fst <$> map_to_list m).
 Proof. eauto using NoDup_fmap_fst, map_to_list_unique, NoDup_map_to_list. Qed.
+Lemma elem_of_map_of_list_1_help {A} (l : list (K * A)) i x :
+  (i,x) ∈ l → (∀ y, (i,y) ∈ l → y = x) → map_of_list l !! i = Some x.
+Proof.
+  induction l as [|[j y] l IH]; csimpl; [by rewrite elem_of_nil|].
+  setoid_rewrite elem_of_cons.
+  intros [?|?] Hdup; simplify_equality; [by rewrite lookup_insert|].
+  destruct (decide (i = j)) as [->|].
+  * rewrite lookup_insert; f_equal; eauto.
+  * rewrite lookup_insert_ne by done; eauto.
+Qed.
 Lemma elem_of_map_of_list_1 {A} (l : list (K * A)) i x :
   NoDup (fst <$> l) → (i,x) ∈ l → map_of_list l !! i = Some x.
 Proof.
-  induction l as [|[j y] l IH]; csimpl; [by rewrite elem_of_nil|].
-  rewrite NoDup_cons, elem_of_cons, elem_of_list_fmap.
-  intros [Hl ?] [?|?]; simplify_equality; [by rewrite lookup_insert|].
-  destruct (decide (i = j)) as [->|]; [|rewrite lookup_insert_ne; auto].
-  destruct Hl. by exists (j,x).
+  intros ? Hx; apply elem_of_map_of_list_1_help; eauto using NoDup_fmap_fst.
+  intros y; revert Hx. rewrite !elem_of_list_lookup; intros [i' Hi'] [j' Hj'].
+  cut (i' = j'); [naive_solver|]. apply NoDup_lookup with (fst <$> l) i;
+    by rewrite ?list_lookup_fmap, ?Hi', ?Hj'.
 Qed.
 Lemma elem_of_map_of_list_2 {A} (l : list (K * A)) i x :
   map_of_list l !! i = Some x → (i,x) ∈ l.
-- 
GitLab