From 5644d68f4f15012ace5d956314cc68ad8b8b982a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 29 Jan 2015 11:32:41 +0100
Subject: [PATCH] mem_force no longer flattens the entire subobject for
 "unsigned char" addresses.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The operation "mem_force Γ m a" used to apply the identify function to
pricisely the object "a", even in case "a" is an "unsigned char" address
refering to an individual byte. This caused the ctree substructure of the
entire subobject to disappear and had the undesired effect that:

  mem_force Γ a m ⊑{Γ,true@Γm} m

failed to hold (i.e. unused reads cannot be removed).
---
 theories/list.v | 2 ++
 theories/nmap.v | 1 +
 2 files changed, 3 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index d0c27ab3..73991db9 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -473,6 +473,8 @@ Proof.
   intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
   rewrite Hi at 1. by apply alter_app_r.
 Qed.
+Lemma list_alter_id f l i : (∀ x, f x = x) → alter f i l = l.
+Proof. intros ?. revert i. induction l; intros [|?]; f_equal'; auto. Qed.
 Lemma list_alter_ext f g l k i :
   (∀ x, l !! i = Some x → f x = g x) → l = k → alter f i l = alter g i k.
 Proof. intros H ->. revert i H. induction k; intros [|?] ?; f_equal'; auto. Qed.
diff --git a/theories/nmap.v b/theories/nmap.v
index 5f78de7a..b66ed43b 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -21,6 +21,7 @@ Proof.
   end; abstract congruence.
 Defined.
 Instance Nempty {A} : Empty (Nmap A) := NMap None ∅.
+Global Opaque Nempty.
 Instance Nlookup {A} : Lookup N A (Nmap A) := λ i t,
   match i with
   | N0 => Nmap_0 t
-- 
GitLab