From 092e3ccc1bfc0a997f0399fdfa24cce5a892ac8d Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 3 Apr 2022 14:40:20 -0400
Subject: [PATCH] Revising for next Wednesday's lecture

---
 SeparationLogic.v          | 20 ++++++++++----------
 SeparationLogic_template.v | 14 +++++++-------
 2 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/SeparationLogic.v b/SeparationLogic.v
index e059a86..5bf7ac7 100644
--- a/SeparationLogic.v
+++ b/SeparationLogic.v
@@ -908,7 +908,7 @@ Proof.
 Qed.
 
 (* Fancy theorem to help us rewrite within preconditions and postconditions *)
-Instance hoare_triple_morphism : forall A,
+Global Instance hoare_triple_morphism : forall A,
   Proper (heq ==> eq ==> (eq ==> heq) ==> iff) (@hoare_triple A).
 Proof.
   Transparent himp.
@@ -1133,13 +1133,13 @@ Qed.
  * memory. *)
 Fixpoint linkedList (p : nat) (ls : list nat) :=
   match ls with
-    | nil => [| p = 0 |]
-      (* An empty list is associated with a null pointer and no memory
-       * contents. *)
-    | x :: ls' => [| p <> 0 |]
-                  * exists p', p |--> [x; p'] * linkedList p' ls'
-      (* A nonempty list is associated with a nonnull pointer and a two-cell
-       * struct, which points to a further list. *)
+  | nil => [| p = 0 |]
+    (* An empty list is associated with a null pointer and no memory
+     * contents. *)
+  | x :: ls' => [| p <> 0 |]
+                * exists p', p |--> [x; p'] * linkedList p' ls'
+    (* A nonempty list is associated with a nonnull pointer and a two-cell
+     * struct, which points to a further list. *)
   end%sep.
 
 (* The definition of [linkedList] is recursive in the list.  Let's also prove
@@ -1266,8 +1266,8 @@ Qed.
  * *list segments* that end with some pointer beside null. *)
 Fixpoint linkedListSegment (p : nat) (ls : list nat) (q : nat) :=
   match ls with
-    | nil => [| p = q |]
-    | x :: ls' => [| p <> 0 |] * exists p', p |--> [x; p'] * linkedListSegment p' ls' q
+  | nil => [| p = q |]
+  | x :: ls' => [| p <> 0 |] * exists p', p |--> [x; p'] * linkedListSegment p' ls' q
   end%sep.
 
 (* Next, two [linkedListSegment] lemmas analogous to those for [linkedList]
diff --git a/SeparationLogic_template.v b/SeparationLogic_template.v
index 5006301..3134f7c 100644
--- a/SeparationLogic_template.v
+++ b/SeparationLogic_template.v
@@ -515,13 +515,13 @@ Admitted.
  * memory. *)
 Fixpoint linkedList (p : nat) (ls : list nat) :=
   match ls with
-    | nil => [| p = 0 |]
-      (* An empty list is associated with a null pointer and no memory
-       * contents. *)
-    | x :: ls' => [| p <> 0 |]
-                  * exists p', p |--> [x; p'] * linkedList p' ls'
-      (* A nonempty list is associated with a nonnull pointer and a two-cell
-       * struct, which points to a further list. *)
+  | nil => [| p = 0 |]
+    (* An empty list is associated with a null pointer and no memory
+     * contents. *)
+  | x :: ls' => [| p <> 0 |]
+                * exists p', p |--> [x; p'] * linkedList p' ls'
+    (* A nonempty list is associated with a nonnull pointer and a two-cell
+     * struct, which points to a further list. *)
   end%sep.
 
 (* The definition of [linkedList] is recursive in the list.  Let's also prove