From 9723ef2364e50314eb269a4499cccc3a2fa3fdc6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thibaut=20P=C3=A9rami?= <thibaut.perami@cl.cam.ac.uk>
Date: Tue, 8 Oct 2024 16:46:21 +0100
Subject: [PATCH] Redefine list_cprod and remove notation
---
stdpp/base.v | 5 +----
stdpp/boolset.v | 4 ++--
stdpp/gmap.v | 4 ++--
stdpp/list.v | 19 ++++++++++++++-----
stdpp/sets.v | 6 +++---
5 files changed, 22 insertions(+), 16 deletions(-)
diff --git a/stdpp/base.v b/stdpp/base.v
index 3488b6fd..395df7cb 100644
--- a/stdpp/base.v
+++ b/stdpp/base.v
@@ -1053,10 +1053,7 @@ Notation "(∖*)" := (zip_with (∖)) (only parsing) : stdpp_scope.
Class CProd A B C := cprod : A → B → C.
Global Hint Mode CProd ! ! - : typeclass_instances.
Global Instance: Params (@cprod) 4 := {}.
-Infix "×" := cprod (at level 37, left associativity) : stdpp_scope.
-Notation "(×)" := cprod (only parsing) : stdpp_scope.
-Notation "( x ×.)" := (cprod x) (only parsing) : stdpp_scope.
-Notation "(.× x )" := (λ y, cprod y x) (only parsing) : stdpp_scope.
+(* TODO choose a notation *)
Class Singleton A B := singleton: A → B.
Global Hint Mode Singleton - ! : typeclass_instances.
diff --git a/stdpp/boolset.v b/stdpp/boolset.v
index d7ae716e..cf5f7c54 100644
--- a/stdpp/boolset.v
+++ b/stdpp/boolset.v
@@ -36,7 +36,7 @@ Global Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
Lemma elem_of_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) (x : A * B) :
- x ∈ X1 × X2 ↔ x.1 ∈ X1 ∧ x.2 ∈ X2.
+ x ∈ cprod X1 X2 ↔ x.1 ∈ X1 ∧ x.2 ∈ X2.
Proof.
destruct X1, X2.
unfold cprod, boolset_cprod, elem_of, boolset_elem_of.
@@ -46,7 +46,7 @@ Qed.
Global Instance set_unfold_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) x P Q :
SetUnfoldElemOf x.1 X1 P → SetUnfoldElemOf x.2 X2 Q →
- SetUnfoldElemOf x (X1 × X2) (P ∧ Q).
+ SetUnfoldElemOf x (cprod X1 X2) (P ∧ Q).
Proof.
intros ??; constructor.
by rewrite elem_of_boolset_cprod, (set_unfold_elem_of x.1 X1 P),
diff --git a/stdpp/gmap.v b/stdpp/gmap.v
index ea12bae1..ed811569 100644
--- a/stdpp/gmap.v
+++ b/stdpp/gmap.v
@@ -830,12 +830,12 @@ Section gset_cprod.
λ X Y, set_bind (λ e1, set_map (e1,.) Y) X.
Lemma elem_of_gset_cprod (X : gset A) (Y : gset B) x :
- x ∈ X × Y ↔ x.1 ∈ X ∧ x.2 ∈ Y.
+ x ∈ cprod X Y ↔ x.1 ∈ X ∧ x.2 ∈ Y.
Proof. unfold cprod, gset_cprod. destruct x. set_solver. Qed.
Global Instance set_unfold_gset_cprod (X : gset A) (Y : gset B) x (P : Prop) Q :
SetUnfoldElemOf x.1 X P → SetUnfoldElemOf x.2 Y Q →
- SetUnfoldElemOf x (X × Y) (P ∧ Q).
+ SetUnfoldElemOf x (cprod X Y) (P ∧ Q).
Proof using.
intros ??; constructor.
by rewrite elem_of_gset_cprod, (set_unfold_elem_of x.1 X P),
diff --git a/stdpp/list.v b/stdpp/list.v
index acf4f7b8..82caddb4 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -68,9 +68,6 @@ Inductive list_equiv `{Equiv A} : Equiv (list A) :=
| cons_equiv x y l k : x ≡ y → l ≡ k → x :: l ≡ y :: k.
Global Existing Instance list_equiv.
-(** The operation [l × l'] gives the Cartesian product of both lists *)
-Global Instance list_cprod {A B} : CProd (list A) (list B) (list (A * B)) :=
- @list_prod A B.
(** The operation [l !! i] gives the [i]th element of the list [l], or [None]
in case [i] is out of bounds. *)
@@ -228,6 +225,10 @@ Global Instance list_join: MJoin list :=
fix go A (ls : list (list A)) : list A :=
match ls with [] => [] | l :: ls => l ++ @mjoin _ go _ ls end.
+(** The operation [cprod l l'] gives the Cartesian product of both lists *)
+Global Instance list_cprod {A B} : CProd (list A) (list B) (list (A * B)) :=
+ λ l k, x ← l; (x,.) <$> k.
+
Definition mapM `{MBind M, MRet M} {A B} (f : A → M B) : list A → M (list B) :=
fix go l :=
match l with [] => mret [] | x :: l => y ← f x; k ← go l; mret (y :: k) end.
@@ -950,10 +951,18 @@ Proof.
split; auto using elem_of_reverse_2.
intros. rewrite <-(reverse_involutive l). by apply elem_of_reverse_2.
Qed.
+Lemma list_cprod_list_prod {B} l1 (l2 : list B) :
+ cprod l1 l2 = list_prod l1 l2.
+Proof.
+ induction l1.
+ - by unfold cprod, list_cprod.
+ - unfold cprod, list_cprod in *. simpl.
+ by setoid_rewrite IHl1.
+Qed.
Lemma elem_of_list_cprod {B} l1 (l2 : list B) (x : A * B) :
- x ∈ l1 × l2 ↔ x.1 ∈ l1 ∧ x.2 ∈ l2.
+ x ∈ cprod l1 l2 ↔ x.1 ∈ l1 ∧ x.2 ∈ l2.
Proof.
- unfold cprod, list_cprod.
+ rewrite list_cprod_list_prod.
setoid_rewrite elem_of_list_In.
destruct x.
apply in_prod_iff.
diff --git a/stdpp/sets.v b/stdpp/sets.v
index f4d77b53..69486858 100644
--- a/stdpp/sets.v
+++ b/stdpp/sets.v
@@ -289,7 +289,7 @@ Section set_unfold_list.
Qed.
Global Instance set_unfold_list_cprod {B} (x : A * B) l (k : list B) P Q :
SetUnfoldElemOf x.1 l P → SetUnfoldElemOf x.2 k Q →
- SetUnfoldElemOf x (l × k) (P ∧ Q).
+ SetUnfoldElemOf x (cprod l k) (P ∧ Q).
Proof.
intros ??; constructor.
by rewrite elem_of_list_cprod, (set_unfold_elem_of x.1 l P),
@@ -1118,7 +1118,7 @@ Section set_monad.
Global Instance monadset_cprod {A B} :
CProd (M A) (M B) (M (A * B)) := λ X Y, x ← X; fmap (x,.) Y.
Lemma elem_of_monadset_cprod {A B} (X : M A) (Y : M B) (x : A * B) :
- x ∈ X × Y ↔ x.1 ∈ X ∧ x.2 ∈ Y.
+ x ∈ cprod X Y ↔ x.1 ∈ X ∧ x.2 ∈ Y.
Proof.
unfold cprod, monadset_cprod.
setoid_rewrite elem_of_bind.
@@ -1129,7 +1129,7 @@ Section set_monad.
Global Instance set_unfold_monadset_cprod {A B} (X : M A) (Y : M B) P Q x :
SetUnfoldElemOf x.1 X P →
SetUnfoldElemOf x.2 Y Q →
- SetUnfoldElemOf x (X × Y) (P ∧ Q).
+ SetUnfoldElemOf x (cprod X Y) (P ∧ Q).
Proof.
constructor.
by rewrite elem_of_monadset_cprod, (set_unfold_elem_of x.1 X P),
--
GitLab