From ea0b55fa6a814a3bc69e052e61f9b4cf894d619e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 30 Nov 2021 12:28:19 -0500
Subject: [PATCH] simplify telescope-based notations
These type annotations are no longer needed once we have a bidirectionality hint
on tele_app.
---
iris/bi/lib/atomic.v | 85 ++++++++++++++-----------------------
iris/program_logic/atomic.v | 46 +++++++-------------
2 files changed, 48 insertions(+), 83 deletions(-)
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index aed9be0a8..c4d27aadf 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -95,21 +95,18 @@ Global Arguments atomic_acc {PROP _ TA TB} Eo Ei _ _ _ _ : simpl never.
Global Arguments atomic_update {PROP _ TA TB} Eo Ei _ _ _ : simpl never.
(** Notation: Atomic updates *)
+(* The way to read the [tele_app foo] here is that they convert the n-ary
+function [foo] into a unary function taking a telescope as the argument. *)
Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
(atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
(TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
Eo Ei
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, α%I) ..)
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn,
- tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
- (λ y1, .. (λ yn, β%I) .. )
+ (tele_app $ λ x1, .. (λ xn, α%I) ..)
+ (tele_app $ λ x1, .. (λ xn,
+ tele_app (λ y1, .. (λ yn, β%I) .. )
) .. )
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn,
- tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
- (λ y1, .. (λ yn, Φ%I) .. )
+ (tele_app $ λ x1, .. (λ xn,
+ tele_app (λ y1, .. (λ yn, Φ%I) .. )
) .. )
)
(at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
@@ -119,12 +116,9 @@ Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :
(atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
(TB:=TeleO)
Eo Ei
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, α%I) ..)
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, tele_app (TT:=TeleO) β%I) .. )
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
+ (tele_app $ λ x1, .. (λ xn, α%I) ..)
+ (tele_app $ λ x1, .. (λ xn, tele_app β%I) .. )
+ (tele_app $ λ x1, .. (λ xn, tele_app Φ%I) .. )
)
(at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder,
format "'[hv ' 'AU' '<<' '[' ∀ x1 .. xn , '/' α ']' '>>' '/' @ '[' Eo , '/' Ei ']' '/' '<<' '[' β , '/' COMM Φ ']' '>>' ']'") : bi_scope.
@@ -133,22 +127,19 @@ Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :
(atomic_update (TA:=TeleO)
(TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
Eo Ei
- (tele_app (TT:=TeleO) α%I)
- (tele_app (TT:=TeleO) $
- tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
- (λ y1, .. (λ yn, β%I) ..))
- (tele_app (TT:=TeleO) $
- tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
- (λ y1, .. (λ yn, Φ%I) ..))
+ (tele_app α%I)
+ (tele_app $ tele_app (λ y1, .. (λ yn, β%I) ..))
+ (tele_app $ tele_app (λ y1, .. (λ yn, Φ%I) ..))
)
(at level 20, Eo, Ei, α, β, Φ at level 200, y1 binder, yn binder,
format "'[hv ' 'AU' '<<' '[' α ']' '>>' '/' @ '[' Eo , '/' Ei ']' '/' '<<' '[' ∃ y1 .. yn , '/' β , '/' COMM Φ ']' '>>' ']'") : bi_scope.
Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
- (atomic_update (TA:=TeleO) (TB:=TeleO) Eo Ei
- (tele_app (TT:=TeleO) α%I)
- (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) β%I)
- (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
+ (atomic_update (TA:=TeleO) (TB:=TeleO)
+ Eo Ei
+ (tele_app α%I)
+ (tele_app $ tele_app β%I)
+ (tele_app $ tele_app Φ%I)
)
(at level 20, Eo, Ei, α, β, Φ at level 200,
format "'[hv ' 'AU' '<<' '[' α ']' '>>' '/' @ '[' Eo , '/' Ei ']' '/' '<<' '[' β , '/' COMM Φ ']' '>>' ']'") : bi_scope.
@@ -158,18 +149,13 @@ Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .
(atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
(TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
Eo Ei
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, α%I) ..)
+ (tele_app $ λ x1, .. (λ xn, α%I) ..)
P%I
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn,
- tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
- (λ y1, .. (λ yn, β%I) .. )
+ (tele_app $ λ x1, .. (λ xn,
+ tele_app (λ y1, .. (λ yn, β%I) .. )
) .. )
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn,
- tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
- (λ y1, .. (λ yn, Φ%I) .. )
+ (tele_app $ λ x1, .. (λ xn,
+ tele_app (λ y1, .. (λ yn, Φ%I) .. )
) .. )
)
(at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
@@ -179,13 +165,10 @@ Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'CO
(atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
(TB:=TeleO)
Eo Ei
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, α%I) ..)
+ (tele_app $ λ x1, .. (λ xn, α%I) ..)
P%I
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, tele_app (TT:=TeleO) β%I) .. )
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
+ (tele_app $ λ x1, .. (λ xn, tele_app β%I) .. )
+ (tele_app $ λ x1, .. (λ xn, tele_app Φ%I) .. )
)
(at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder,
format "'[hv ' 'AACC' '<<' '[' ∀ x1 .. xn , '/' α , '/' ABORT P ']' '>>' '/' @ '[' Eo , '/' Ei ']' '/' '<<' '[' β , '/' COMM Φ ']' '>>' ']'") : bi_scope.
@@ -194,14 +177,10 @@ Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'CO
(atomic_acc (TA:=TeleO)
(TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
Eo Ei
- (tele_app (TT:=TeleO) α%I)
+ (tele_app α%I)
P%I
- (tele_app (TT:=TeleO) $
- tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
- (λ y1, .. (λ yn, β%I) ..))
- (tele_app (TT:=TeleO) $
- tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
- (λ y1, .. (λ yn, Φ%I) ..))
+ (tele_app $ tele_app (λ y1, .. (λ yn, β%I) ..))
+ (tele_app $ tele_app (λ y1, .. (λ yn, Φ%I) ..))
)
(at level 20, Eo, Ei, α, P, β, Φ at level 200, y1 binder, yn binder,
format "'[hv ' 'AACC' '<<' '[' α , '/' ABORT P ']' '>>' '/' @ '[' Eo , '/' Ei ']' '/' '<<' '[' ∃ y1 .. yn , '/' β , '/' COMM Φ ']' '>>' ']'") : bi_scope.
@@ -210,10 +189,10 @@ Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
(atomic_acc (TA:=TeleO)
(TB:=TeleO)
Eo Ei
- (tele_app (TT:=TeleO) α%I)
+ (tele_app α%I)
P%I
- (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) β%I)
- (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
+ (tele_app $ tele_app β%I)
+ (tele_app $ tele_app Φ%I)
)
(at level 20, Eo, Ei, α, P, β, Φ at level 200,
format "'[hv ' 'AACC' '<<' '[' α , '/' ABORT P ']' '>>' '/' @ '[' Eo , '/' Ei ']' '/' '<<' '[' β , '/' COMM Φ ']' '>>' ']'") : bi_scope.
diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index 9d201ebd8..cc01c234c 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -23,22 +23,19 @@ Definition atomic_wp `{!irisGS Λ Σ} {TA TB : tele}
(* Note: To add a private postcondition, use
atomic_update α β Eo Ei (λ x y, POST x y -∗ Φ (f x y)) *)
+(* The way to read the [tele_app foo] here is that they convert the n-ary
+function [foo] into a unary function taking a telescope as the argument. *)
Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
(atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
(TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
e%E
E
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, α%I) ..)
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn,
- tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
- (λ y1, .. (λ yn, β%I) .. )
+ (tele_app $ λ x1, .. (λ xn, α%I) ..)
+ (tele_app $ λ x1, .. (λ xn,
+ tele_app (λ y1, .. (λ yn, β%I) .. )
) .. )
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn,
- tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
- (λ y1, .. (λ yn, v%V) .. )
+ (tele_app $ λ x1, .. (λ xn,
+ tele_app (λ y1, .. (λ yn, v%V) .. )
) .. )
)
(at level 20, E, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
@@ -50,16 +47,9 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
(TB:=TeleO)
e%E
E
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, α%I) ..)
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn,
- tele_app (TT:=TeleO) β%I
- ) .. )
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn,
- tele_app (TT:=TeleO) v%V
- ) .. )
+ (tele_app $ λ x1, .. (λ xn, α%I) ..)
+ (tele_app $ λ x1, .. (λ xn, tele_app β%I) .. )
+ (tele_app $ λ x1, .. (λ xn, tele_app v%V) .. )
)
(at level 20, E, α, β, v at level 200, x1 binder, xn binder,
format "'[hv' '<<<' '[' ∀ x1 .. xn , '/' α ']' '>>>' '/ ' e @ E '/' '<<<' '[' β , '/' 'RET' v ']' '>>>' ']'")
@@ -70,13 +60,9 @@ Notation "'<<<' α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
(TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
e%E
E
- (tele_app (TT:=TeleO) α%I)
- (tele_app (TT:=TeleO) $
- tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
- (λ y1, .. (λ yn, β%I) .. ))
- (tele_app (TT:=TeleO) $
- tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
- (λ y1, .. (λ yn, v%V) .. ))
+ (tele_app α%I)
+ (tele_app $ tele_app (λ y1, .. (λ yn, β%I) .. ))
+ (tele_app $ tele_app (λ y1, .. (λ yn, v%V) .. ))
)
(at level 20, E, α, β, v at level 200, y1 binder, yn binder,
format "'[hv' '<<<' '[' α ']' '>>>' '/ ' e @ E '/' '<<<' '[' ∃ y1 .. yn , '/' β , '/' 'RET' v ']' '>>>' ']'")
@@ -87,9 +73,9 @@ Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
(TB:=TeleO)
e%E
E
- (tele_app (TT:=TeleO) α%I)
- (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) β%I)
- (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) v%V)
+ (tele_app α%I)
+ (tele_app $ tele_app β%I)
+ (tele_app $ tele_app v%V)
)
(at level 20, E, α, β, v at level 200,
format "'[hv' '<<<' '[' α ']' '>>>' '/ ' e @ E '/' '<<<' '[' β , '/' 'RET' v ']' '>>>' ']'")
--
GitLab