From bdfa43b9d7f168b90814794a5582aeae76f9662b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 1 Jun 2019 15:18:24 +0200
Subject: [PATCH] show that there are infinitely many locations

---
 theories/heap_lang/locations.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/theories/heap_lang/locations.v b/theories/heap_lang/locations.v
index e10269515..53ca9e056 100644
--- a/theories/heap_lang/locations.v
+++ b/theories/heap_lang/locations.v
@@ -11,6 +11,20 @@ Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
 Instance loc_countable : Countable loc.
 Proof. by apply (inj_countable' loc_car (λ i, {| loc_car := i |})); intros []. Qed.
 
+Program Definition loc_infinite : Infinite loc := {|
+  infinite_fresh l := {| loc_car := infinite_fresh (loc_car <$> l) |}
+|}.
+Next Obligation.
+  intros xs Hfresh. unfold fresh in Hfresh.
+  eapply (infinite_is_fresh (loc_car <$> xs)).
+  eapply elem_of_list_fmap. eexists. split; last done.
+  reflexivity.
+Qed.
+Next Obligation.
+  intros xs ys Hperm. unfold fresh. f_equal.
+  eapply infinite_fresh_Permutation. rewrite Hperm //.
+Qed.
+
 Definition loc_add (l : loc) (off : Z) : loc :=
   {| loc_car := loc_car l + off|}.
 
-- 
GitLab