From 3aa5cd2d1b5f4bdc51acb065c88480fceef06111 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thibaut=20P=C3=A9rami?= <thibaut.perami@cl.cam.ac.uk>
Date: Wed, 18 Oct 2023 11:41:37 +0100
Subject: [PATCH] Allow patterns and type annotations in propset notation

---
 CHANGELOG.md      |  2 ++
 stdpp/propset.v   |  7 ++++++-
 tests/propset.ref |  0
 tests/propset.v   | 20 ++++++++++++++++++++
 4 files changed, 28 insertions(+), 1 deletion(-)
 create mode 100644 tests/propset.ref
 create mode 100644 tests/propset.v

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a604255c..9fbaaccf 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -28,6 +28,8 @@ Coq 8.19 is newly supported by this version of std++.
   to refer to a hypothesis on the goal (`inv 1`).
 - Add `prod_swap : A * B → B * A` and some basic theory about it.
 - Add lemma `join_app`.
+- Allow patterns and type annotations in propset notation, e.g.
+  `{[ (x, y) : nat * nat | x = y ]}`
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/stdpp/propset.v b/stdpp/propset.v
index 1ed3af52..7a220edc 100644
--- a/stdpp/propset.v
+++ b/stdpp/propset.v
@@ -6,8 +6,13 @@ Record propset (A : Type) : Type := PropSet { propset_car : A → Prop }.
 Add Printing Constructor propset.
 Global Arguments PropSet {_} _ : assert.
 Global Arguments propset_car {_} _ _ : assert.
+(** Here we are using the notation "at level 200 as pattern" because we want to
+    be compatible with all the rules that start with [ {[ TERM ] such as
+    records, singletons, and map singletons. See
+    https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#binders-bound-in-the-notation-and-parsed-as-terms
+    and https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/533#note_98003 *)
 Notation "{[ x | P ]}" := (PropSet (λ x, P))
-  (at level 1, format "{[  x  |  P  ]}") : stdpp_scope.
+  (at level 1, x at level 200 as pattern, format "{[  x  |  P  ]}") : stdpp_scope.
 
 Global Instance propset_elem_of {A} : ElemOf A (propset A) := λ x X, propset_car X x.
 
diff --git a/tests/propset.ref b/tests/propset.ref
new file mode 100644
index 00000000..e69de29b
diff --git a/tests/propset.v b/tests/propset.v
new file mode 100644
index 00000000..6d356cbc
--- /dev/null
+++ b/tests/propset.v
@@ -0,0 +1,20 @@
+From stdpp Require Import propset.
+
+Lemma diagonal : {[ (a,b) : nat * nat | a = b ]} ≡ (λ x, (x,x)) <$> ⊤.
+Proof. set_unfold. intros []. naive_solver. Qed.
+
+Lemma diagonal2 : {[ (a,b) | a =@{nat} b ]} ≡ {[ x | x.1 = x.2 ]}.
+Proof. set_unfold. intros []. naive_solver. Qed.
+
+Lemma firstis42 : {[ (x, _) : nat * nat | x = 42 ]} ≡ (42,.) <$> ⊤.
+Proof. set_unfold. intros []. naive_solver. Qed.
+
+Inductive foo := Foo (n : nat).
+
+Definition set_of_positive_foos : {[ Foo x | x ≠ 0 ]} ≡ Foo <$> (Pos.to_nat <$> ⊤).
+Proof.
+  set_unfold. intros [[]]; naive_solver by (rewrite SuccNat2Pos.id_succ || lia).
+Qed.
+
+Lemma simple_pattern_does_not_match : {[ x : nat | x = x]} = PropSet (λ x, x = x).
+Proof. exact eq_refl. Qed.
-- 
GitLab