From 20623c96a405d29e1eea85fdb77cccf30f57cb03 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 8 Aug 2017 10:18:51 +0200
Subject: [PATCH] Use notations.
---
theories/lifetime/lifetime_sig.v | 5 ++---
theories/lifetime/model/primitive.v | 5 ++---
2 files changed, 4 insertions(+), 6 deletions(-)
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 0492383b..58d85fb1 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -148,9 +148,8 @@ Module Type lifetime_sig.
↑lftN ⊆ E → κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
Parameter lft_incl_dead : ∀ E κ κ', ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
Parameter lft_incl_intro : ∀ κ κ',
- □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
- lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
- (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
+ □ ((∀ q, q.[κ] ={↑lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={↑lftN}=∗ q.[κ])) ∗
+ ([†κ'] ={↑lftN}=∗ [†κ])) -∗ κ ⊑ κ'.
End properties.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 5f77eea2..3751fa3e 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -330,9 +330,8 @@ Proof.
Qed.
Lemma lft_incl_intro κ κ' :
- □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
- lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
- (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
+ □ ((∀ q, q.[κ] ={↑lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={↑lftN}=∗ q.[κ])) ∗
+ ([†κ'] ={↑lftN}=∗ [†κ])) -∗ κ ⊑ κ'.
Proof. reflexivity. Qed.
Lemma lft_intersect_incl_l κ κ': (κ ⊓ κ' ⊑ κ)%I.
--
GitLab