Commit faba7343 authored by Simon Friis Vindum's avatar Simon Friis Vindum Committed by Robbert Krebbers
Browse files

Fix various things

parent 17033126
...@@ -9,7 +9,9 @@ ...@@ -9,7 +9,9 @@
-Q iris/program_logic iris.program_logic -Q iris/program_logic iris.program_logic
-Q iris_heap_lang iris.heap_lang -Q iris_heap_lang iris.heap_lang
# We sometimes want to locally override notation, and there is no good way to do that with scopes. # We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden -arg -w -arg -notation-overridden
# Coq emits warnings when a custom entry is reimported, this is too noisy.
-arg -w -arg -custom-entry-overriden
# Cannot use non-canonical projections as it causes massive unification failures # Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294). # (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection -arg -w -arg -redundant-canonical-projection
......
...@@ -32,6 +32,12 @@ Inductive dfrac := ...@@ -32,6 +32,12 @@ Inductive dfrac :=
| DfracDiscarded : dfrac | DfracDiscarded : dfrac
| DfracBoth : Qp dfrac. | DfracBoth : Qp dfrac.
Declare Custom Entry dfrac.
Notation "{ dq }" := (dq) (in custom dfrac at level 1, dq constr).
Notation "□" := DfracDiscarded (in custom dfrac).
Notation "{# q }" := (DfracOwn q) (in custom dfrac at level 1, q constr).
Notation "" := (DfracOwn 1) (in custom dfrac).
Section dfrac. Section dfrac.
Canonical Structure dfracO := leibnizO dfrac. Canonical Structure dfracO := leibnizO dfrac.
......
...@@ -123,12 +123,6 @@ Section definitions. ...@@ -123,12 +123,6 @@ Section definitions.
End definitions. End definitions.
Arguments meta {L _ _ V Σ _ A _ _} l N x. Arguments meta {L _ _ V Σ _ A _ _} l N x.
Declare Custom Entry dfrac.
Notation "{ dq }" := (dq) (in custom dfrac at level 1, dq constr).
Notation "□" := DfracDiscarded (in custom dfrac).
Notation "{# q }" := (DfracOwn q) (in custom dfrac at level 1, q constr).
Notation "" := (DfracOwn 1) (in custom dfrac).
Local Notation "l ↦ dq v" := (mapsto l dq v) Local Notation "l ↦ dq v" := (mapsto l dq v)
(at level 20, dq custom dfrac at level 1, format "l ↦ dq v") : bi_scope. (at level 20, dq custom dfrac at level 1, format "l ↦ dq v") : bi_scope.
......
...@@ -47,7 +47,7 @@ Arguments atomic_heap _ {_}. ...@@ -47,7 +47,7 @@ Arguments atomic_heap _ {_}.
(** Notation for heap primitives, in a module so you can import it separately. *) (** Notation for heap primitives, in a module so you can import it separately. *)
Module notation. Module notation.
otation "l ↦ dq v" := (mapsto l dq v) Notation "l ↦ dq v" := (mapsto l dq v)
(at level 20, dq custom dfrac at level 1, format "l ↦ dq v") : bi_scope. (at level 20, dq custom dfrac at level 1, format "l ↦ dq v") : bi_scope.
Notation "'ref' e" := (alloc e) : expr_scope. Notation "'ref' e" := (alloc e) : expr_scope.
......
...@@ -111,8 +111,8 @@ Section increment. ...@@ -111,8 +111,8 @@ Section increment.
(* TODO: Generalize to q and 1-q, based on some theory for a "maybe-mapsto" (* TODO: Generalize to q and 1-q, based on some theory for a "maybe-mapsto"
connective that works on [option Qp] (the type of 1-q). *) connective that works on [option Qp] (the type of 1-q). *)
Lemma weak_incr_spec (l: loc) (v : Z) : Lemma weak_incr_spec (l: loc) (v : Z) :
l {#(1/2)} #v - l {#1/2} #v -
<<< (v' : Z), l {#(1/2)} #v' >>> <<< (v' : Z), l {#1/2} #v' >>>
weak_incr #l @ weak_incr #l @
<<< v = v' l #(v + 1), RET #v >>>. <<< v = v' l #(v + 1), RET #v >>>.
Proof. Proof.
......
...@@ -28,8 +28,6 @@ Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := { ...@@ -28,8 +28,6 @@ Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
(** Since we use an [option val] instance of [gen_heap], we need to overwrite (** Since we use an [option val] instance of [gen_heap], we need to overwrite
the notations. That also helps for scopes and coercions. *) the notations. That also helps for scopes and coercions. *)
Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn 1) (Some v%V))
(at level 20) : bi_scope.
Notation "l ↦ dq v" := (mapsto (L:=loc) (V:=option val) l dq (Some v%V)) Notation "l ↦ dq v" := (mapsto (L:=loc) (V:=option val) l dq (Some v%V))
(at level 20, dq custom dfrac at level 1, format "l ↦ dq v") : bi_scope. (at level 20, dq custom dfrac at level 1, format "l ↦ dq v") : bi_scope.
...@@ -277,7 +275,7 @@ Qed. ...@@ -277,7 +275,7 @@ Qed.
(** We need to adjust the [gen_heap] and [gen_inv_heap] lemmas because of our (** We need to adjust the [gen_heap] and [gen_inv_heap] lemmas because of our
value type being [option val]. *) value type being [option val]. *)
Lemma mapsto_valid l dq v : l {dq} v - ⌜✓ dq%Qp. Lemma mapsto_valid l dq v : l {dq} v - ⌜✓ dq.
Proof. apply mapsto_valid. Qed. Proof. apply mapsto_valid. Qed.
Lemma mapsto_valid_2 l dq1 dq2 v1 v2 : Lemma mapsto_valid_2 l dq1 dq2 v1 v2 :
l {dq1} v1 - l {dq2} v2 - ⌜✓ (dq1 dq2) v1 = v2. l {dq1} v1 - l {dq2} v2 - ⌜✓ (dq1 dq2) v1 = v2.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment