pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-27 23:06:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising for next Wednesday's lecture

Browse source
This commit is contained in:
Adam Chlipala 2022-04-03 14:40:20 -04:00
parent 0e13a0a695
commit 092e3ccc1b
2 changed files with 17 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
SeparationLogic.v
View file

@ -908,7 +908,7 @@ Proof.
Qed. Qed.
(* Fancy theorem to help us rewrite within preconditions and postconditions *) (* 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). Proper (heq ==> eq ==> (eq ==> heq) ==> iff) (@hoare_triple A).
Proof. Proof.
Transparent himp. Transparent himp.
@ -1133,13 +1133,13 @@ Qed.
* memory. *) * memory. *)
Fixpoint linkedList (p : nat) (ls : list nat) := Fixpoint linkedList (p : nat) (ls : list nat) :=
match ls with match ls with
| nil => [| p = 0 |] | nil => [| p = 0 |]
(* An empty list is associated with a null pointer and no memory (* An empty list is associated with a null pointer and no memory
* contents. *) * contents. *)
| x :: ls' => [| p <> 0 |] | x :: ls' => [| p <> 0 |]
* exists p', p |--> [x; p'] * linkedList p' ls' * exists p', p |--> [x; p'] * linkedList p' ls'
(* A nonempty list is associated with a nonnull pointer and a two-cell (* A nonempty list is associated with a nonnull pointer and a two-cell
* struct, which points to a further list. *) * struct, which points to a further list. *)
end%sep. end%sep.
(* The definition of [linkedList] is recursive in the list. Let's also prove (* 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. *) * *list segments* that end with some pointer beside null. *)
Fixpoint linkedListSegment (p : nat) (ls : list nat) (q : nat) := Fixpoint linkedListSegment (p : nat) (ls : list nat) (q : nat) :=
match ls with match ls with
| nil => [| p = q |] | nil => [| p = q |]
| x :: ls' => [| p <> 0 |] * exists p', p |--> [x; p'] * linkedListSegment p' ls' q | x :: ls' => [| p <> 0 |] * exists p', p |--> [x; p'] * linkedListSegment p' ls' q
end%sep. end%sep.
(* Next, two [linkedListSegment] lemmas analogous to those for [linkedList] (* Next, two [linkedListSegment] lemmas analogous to those for [linkedList]

14
SeparationLogic_template.v
View file

@ -515,13 +515,13 @@ Admitted.
* memory. *) * memory. *)
Fixpoint linkedList (p : nat) (ls : list nat) := Fixpoint linkedList (p : nat) (ls : list nat) :=
match ls with match ls with
| nil => [| p = 0 |] | nil => [| p = 0 |]
(* An empty list is associated with a null pointer and no memory (* An empty list is associated with a null pointer and no memory
* contents. *) * contents. *)
| x :: ls' => [| p <> 0 |] | x :: ls' => [| p <> 0 |]
* exists p', p |--> [x; p'] * linkedList p' ls' * exists p', p |--> [x; p'] * linkedList p' ls'
(* A nonempty list is associated with a nonnull pointer and a two-cell (* A nonempty list is associated with a nonnull pointer and a two-cell
* struct, which points to a further list. *) * struct, which points to a further list. *)
end%sep. end%sep.
(* The definition of [linkedList] is recursive in the list. Let's also prove (* The definition of [linkedList] is recursive in the list. Let's also prove