From 5ae4adc9b5362db6292669b0ea36379d59f552ec Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 13 Mar 2019 14:37:24 +0100
Subject: [PATCH] better notation for lty2_prod and lty2_sum

---
 theories/examples/generative.v | 4 ++--
 theories/examples/symbol.v     | 4 ++--
 theories/lib/counter.v         | 2 +-
 theories/lib/list.v            | 4 +---
 theories/logic/compatibility.v | 2 +-
 theories/logic/model.v         | 3 ++-
 6 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/theories/examples/generative.v b/theories/examples/generative.v
index d064b77..8a1183b 100644
--- a/theories/examples/generative.v
+++ b/theories/examples/generative.v
@@ -41,7 +41,7 @@ Section namegen_refinement.
                         end)%I.
 
   Lemma nameGen_ref1 :
-    REL nameGen1 << nameGen2 : ∃ α, (() → α) × (α → α → lty2_bool).
+    REL nameGen1 << nameGen2 : ∃ α, (() → α) * (α → α → lty2_bool).
   Proof.
     unlock nameGen1 nameGen2.
     rel_alloc_r c as "Hc".
@@ -164,7 +164,7 @@ Section cell_refinement.
      ∗ cellInt R r1 r2 r3 l r)%I.
 
   Lemma cell2_cell1_refinement :
-    REL cell2 << cell1 : ∀ α, ∃ β, (α → β) × (β → α) × (β → α → ()).
+    REL cell2 << cell1 : ∀ α, ∃ β, (α → β) * (β → α) * (β → α → ()).
   Proof.
     unlock cell2 cell1.
     (* TODO: this uuugly *)
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 4f20284..802e198 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -15,8 +15,8 @@ From reloc.typing Require Import interp soundness.
 (** * Symbol table *)
 Definition lty_symbol `{relocG Σ} : lty2 Σ :=
   ∃ α, (α → α → lty2_bool)    (* equality check *)
-     × (lty2_int → α)          (* insert *)
-     × (α → lty2_int).         (* lookup *)
+     * (lty2_int → α)          (* insert *)
+     * (α → lty2_int).         (* lookup *)
 
 Definition eqKey : val := λ: "n" "m", "n" = "m".
 Definition symbol1 : val := λ: <>,
diff --git a/theories/lib/counter.v b/theories/lib/counter.v
index 7b7e231..e02c650 100644
--- a/theories/lib/counter.v
+++ b/theories/lib/counter.v
@@ -194,7 +194,7 @@ Section CG_Counter.
   Qed.
 
   Lemma FG_CG_counter_refinement :
-    REL FG_counter << CG_counter : (() → (() → lty2_int) × (() → lty2_int))%lty2.
+    REL FG_counter << CG_counter : () → (() → lty2_int) * (() → lty2_int).
   Proof.
     unfold FG_counter, CG_counter. unlock.
     iApply refines_arrow_val.
diff --git a/theories/lib/list.v b/theories/lib/list.v
index deed975..a6a7b47 100644
--- a/theories/lib/list.v
+++ b/theories/lib/list.v
@@ -14,10 +14,8 @@ Fixpoint is_list (hd : val) (xs : list val) : Prop :=
   | x :: xs => ∃ hd', hd = CONSV x hd' ∧ is_list hd' xs
   end.
 
-(* TODO: is it possible to do this without `Program Definition`? *)
-(* TODO: notation for lty_sum *)
 Program Definition lty_list `{relocG Σ} (A : lty2 Σ) : lty2 Σ :=
-  lty2_rec (λne B, lty2_sum () (A × B))%lty2.
+  lty2_rec (λne B, () + (A * B))%lty2.
 Next Obligation. solve_proper. Qed.
 
 Definition nth : val := rec: "nth" "l" "n" :=
diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 57e11a9..b34bfb6 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -22,7 +22,7 @@ Section compatibility.
   Lemma refines_pair e1 e2 e1' e2' A B :
     (REL e1 << e1' : A) -∗
     (REL e2 << e2' : B) -∗
-    REL (e1, e2) << (e1', e2') : A × B.
+    REL (e1, e2) << (e1', e2') : A * B.
   Proof.
     iIntros "IH1 IH2".
     rel_bind_ap e2 e2' "IH2" v2 v2' "Hvv2".
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 3f88adf..a46721f 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -142,7 +142,8 @@ End semtypes.
 (** Nice notations *)
 Notation "()" := lty2_unit : lty_scope.
 Infix "→" := lty2_arr : lty_scope.
-Infix "×" := lty2_prod (at level 80) : lty_scope.
+Infix "*" := lty2_prod : lty_scope.
+Infix "+" := lty2_sum : lty_scope.
 Notation "'ref' A" := (lty2_ref A) : lty_scope.
 Notation "∃ A1 .. An , C" :=
   (lty2_exists (λ A1, .. (lty2_exists (λ An, C%lty2)) ..)) : lty_scope.
-- 
GitLab