From b78706e0cdd63825fb7d4c877d551e87c9fee007 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Tue, 18 Feb 2025 16:37:48 +0100
Subject: [PATCH] Set: move cartesian product to a separate file, and change
 notation for pairs

---
 List.lp | 16 ++++++++--------
 Prod.lp | 20 ++++++++++++++++++++
 Set.lp  | 19 -------------------
 3 files changed, 28 insertions(+), 27 deletions(-)
 create mode 100644 Prod.lp

diff --git a/List.lp b/List.lp
index ff4fdfc..b49a934 100644
--- a/List.lp
+++ b/List.lp
@@ -195,7 +195,7 @@ protected with nosimpl.
 */
 
 require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq
-  Stdlib.Nat Stdlib.Bool;
+  Stdlib.Nat Stdlib.Bool Stdlib.Prod;
 
 (a:Set) inductive 𝕃:TYPE ≔
 | □ : 𝕃 a // \Box
@@ -583,20 +583,20 @@ symbol zip [a b] : 𝕃 a → 𝕃 b → 𝕃 (a × b);
 rule zip □ □ ↪ □
 with zip □ _ ↪ □
 with zip _ □ ↪ □
-with zip ($x ⸬ $l) ($y ⸬ $m) ↪ $x & $y ⸬ zip $l $m;
+with zip ($x ⸬ $l) ($y ⸬ $m) ↪ ($x ‚ $y) ⸬ zip $l $m;
 
 symbol unzip1 [a b] : 𝕃 (a × b) → 𝕃 a;
 
 rule unzip1 □  ↪ □
-with unzip1 ($x & _ ⸬ $l) ↪ $x ⸬ unzip1 $l;
+with unzip1 (($x ‚ _ ) ⸬ $l) ↪ $x ⸬ unzip1 $l;
 
 symbol unzip2 [a b] : 𝕃 (a × b) → 𝕃 b;
 
 rule unzip2 □ ↪ □
-with unzip2 (_ & $y ⸬ $l) ↪ $y ⸬ unzip2 $l;
+with unzip2 ((_ ‚ $y) ⸬ $l) ↪ $y ⸬ unzip2 $l;
 
-assert ⊢ unzip1 ((3 & 5) ⸬ (6 & 4) ⸬ (7 & 2) ⸬ (8 & 1) ⸬ □) ≡ 3 ⸬ 6 ⸬ 7 ⸬ 8 ⸬ □;
-assert ⊢ unzip2 ((3 & 5) ⸬ (6 & 4) ⸬ (7 & 2) ⸬ (8 & 1) ⸬ □) ≡ 5 ⸬ 4 ⸬ 2 ⸬ 1 ⸬ □;
+assert ⊢ unzip1 ((3 ‚ 5) ⸬ (6 ‚ 4) ⸬ (7 ‚ 2) ⸬ (8 ‚ 1) ⸬ □) ≡ 3 ⸬ 6 ⸬ 7 ⸬ 8 ⸬ □;
+assert ⊢ unzip2 ((3 ‚ 5) ⸬ (6 ‚ 4) ⸬ (7 ‚ 2) ⸬ (8 ‚ 1) ⸬ □) ≡ 5 ⸬ 4 ⸬ 2 ⸬ 1 ⸬ □;
 
 symbol all2 [a b] : (τ a → τ b → 𝔹) → 𝕃 a → 𝕃 b → 𝔹;
 
@@ -687,12 +687,12 @@ begin
   apply @seq_ind2 a b (λ l1 l2, (zip (l1 ++ sa) (l2 ++ sb) = zip l1 l2 ++ zip sa sb)) _ _ la lb h {
     reflexivity;
   } {
-    assume l1 l2 e1 e2 h1 h2; simplify; apply feq (λ l, e1 & e2 ⸬ l) h2; 
+    assume l1 l2 e1 e2 h1 h2; simplify; apply feq (λ l, (e1 ‚ e2) ⸬ l) h2; 
   };
 end;
 
 opaque symbol nth_zip [a b] (x:τ a) (y:τ b) la lb i: π(size la = size lb) →
-  π(nth (x & y) (zip la lb) i = nth x la i & nth y lb i) ≔
+  π(nth (x ‚ y) (zip la lb) i = nth x la i ‚ nth y lb i) ≔
 begin
   assume a b x y; induction
   { assume lb i h;
diff --git a/Prod.lp b/Prod.lp
new file mode 100644
index 0000000..b97126b
--- /dev/null
+++ b/Prod.lp
@@ -0,0 +1,20 @@
+// Cartesian product
+
+require open Stdlib.Set;
+
+constant symbol × : Set → Set → Set; notation × infix right 10; // \times
+
+assert a b c ⊢ a × b × c ≡ a × (b × c);
+
+symbol ‚ [a b] : τ a → τ b → τ (a × b); notation ‚ infix right 30;
+
+assert a (x:τ a) b (y:τ b) c (z:τ c) ⊢ x ‚ y ‚ z : τ(a × b × c);
+assert x y z ⊢ x ‚ y ‚ z ≡ x ‚ (y ‚ z);
+
+symbol ₁ [a b] : τ(a × b) → τ a; notation ₁ postfix 10;
+
+rule ($x ‚ _)₁ ↪ $x;
+
+symbol ₂ [a b] : τ(a × b) → τ b; notation ₂ postfix 10;
+
+rule (_ ‚ $x)₂ ↪ $x;
diff --git a/Set.lp b/Set.lp
index 891ba8c..f484fdf 100644
--- a/Set.lp
+++ b/Set.lp
@@ -13,22 +13,3 @@ builtin "T" ≔ τ;
 // We assume that sets are non-empty
 
 symbol el a : τ a;
-
-// Cartesian product
-
-constant symbol × : Set → Set → Set; notation × infix right 10; // \times
-
-assert a b c ⊢ a × b × c ≡ a × (b × c);
-
-symbol & [a b] : τ a → τ b → τ (a × b); notation & infix right 30;
-
-assert a (x:τ a) b (y:τ b) c (z:τ c) ⊢ x & y & z : τ(a × b × c);
-assert x y z ⊢ x & y & z ≡ x & (y & z);
-
-symbol ₁ [a b] : τ(a × b) → τ a; notation ₁ postfix 10;
-
-rule ($x & _)₁ ↪ $x;
-
-symbol ₂ [a b] : τ(a × b) → τ b; notation ₂ postfix 10;
-
-rule (_ & $x)₂ ↪ $x;