From ebdd150d3f8d53597650d2f2712ad524ec5c07ce Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 14 Mar 2019 19:09:05 +0100
Subject: [PATCH] make use of `map_seq`

---
 theories/logic/adequacy.v |  1 +
 theories/logic/spec_ra.v  | 17 +++++------------
 2 files changed, 6 insertions(+), 12 deletions(-)

diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index 865f180..5ead070 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -47,6 +47,7 @@ Proof.
     iSpecialize ("Hrel" with "Hcfg").
     iApply ("Hrel" $! 0%nat []).
     rewrite tpool_mapsto_eq /tpool_mapsto_def. iFrame.
+    by rewrite /to_tpool /= insert_empty map_fmap_singleton //.
   - iIntros (v).
     iDestruct 1 as (v') "[Hj Hinterp]".
     rewrite HA.
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 573eff2..2d72003 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -21,12 +21,7 @@ Class relocG Σ := RelocG {
   relocG_cfgG :> cfgSG Σ;
 }.
 
-Fixpoint to_tpool_go (i : nat) (tp : list expr) : tpoolUR :=
-  match tp with
-  | [] => ∅
-  | e :: tp => <[i:=Excl e]>(to_tpool_go (S i) tp)
-  end.
-Definition to_tpool : list expr → tpoolUR := to_tpool_go 0.
+Definition to_tpool (tp : list expr) : tpoolUR := Excl <$> (map_seq 0 tp).
 
 Section definitionsS.
   Context `{cfgSG Σ, invG Σ}.
@@ -75,16 +70,14 @@ Section conversions.
   Lemma to_tpool_valid es : ✓ to_tpool es.
   Proof.
     rewrite /to_tpool. move: 0.
-    induction es as [|e es]=> n /= //. by apply insert_valid.
+    induction es as [|e es]=> n /= //.
+    rewrite fmap_insert. by apply insert_valid.
   Qed.
 
   Lemma tpool_lookup tp j : to_tpool tp !! j = Excl <$> tp !! j.
   Proof.
-    cut (∀ i, to_tpool_go i tp !! (i + j) = Excl <$> tp !! j).
-    { intros help. apply (help 0%nat). }
-    revert j. induction tp as [|e tp IH]=> //= -[|j] i /=.
-    - by rewrite Nat.add_0_r lookup_insert.
-    - by rewrite -Nat.add_succ_comm lookup_insert_ne; last lia.
+    unfold to_tpool. rewrite lookup_fmap.
+    by rewrite lookup_map_seq_0.
   Qed.
   Lemma tpool_lookup_Some tp j e : to_tpool tp !! j = Excl' e → tp !! j = Some e.
   Proof. rewrite tpool_lookup fmap_Some. naive_solver. Qed.
-- 
GitLab