From 7af01091126372b50c0c1b6cd4c3201b5c6d5e81 Mon Sep 17 00:00:00 2001
From: Johannes Hostert <jhostert@ethz.ch>
Date: Sat, 2 Dec 2023 02:53:24 +0100
Subject: [PATCH] Refactor proofs of {impl,wand}_timeless

---
 iris/bi/derived_laws_later.v | 30 ++++++++++++++++++++----------
 1 file changed, 20 insertions(+), 10 deletions(-)

diff --git a/iris/bi/derived_laws_later.v b/iris/bi/derived_laws_later.v
index d89ef8243..3c15d3a7b 100644
--- a/iris/bi/derived_laws_later.v
+++ b/iris/bi/derived_laws_later.v
@@ -337,6 +337,21 @@ Proof. rewrite /bi_except_0; apply _. Qed.
 Global Instance Timeless_proper : Proper ((≡) ==> iff) (@Timeless PROP).
 Proof. solve_proper. Qed.
 
+(* To prove a timeless proposition Q, we can additionally assume
+   that we are at step-index 0 (hypothesis â–· False).
+   In fact, this can also serve as a definition of timelessness. *)
+Lemma timeless_alt `{!BiLöb PROP} Q :
+  Timeless Q ↔ ∀ P, (▷ False ∧ P ⊢ Q) → (P ⊢ Q).
+Proof.
+  split; rewrite /Timeless => H.
+  * intros P Hpr.
+    rewrite -(löb Q). apply impl_intro_l.
+    rewrite H /bi_except_0 and_or_r. apply or_elim; auto.
+  * rewrite later_false_em.
+    apply or_mono; first done.
+    apply H, impl_elim_r.
+Qed.
+
 Global Instance pure_timeless φ : Timeless (PROP:=PROP) ⌜φ⌝.
 Proof.
   rewrite /Timeless /bi_except_0 pure_alt later_exist_false.
@@ -352,11 +367,8 @@ Proof. intros; rewrite /Timeless except_0_or later_or; auto. Qed.
 
 Global Instance impl_timeless `{!BiLöb PROP} P Q : Timeless Q → Timeless (P → Q).
 Proof.
-  rewrite /Timeless=> HQ. rewrite later_false_em.
-  apply or_mono, impl_intro_l; first done.
-  rewrite -{2}(löb Q). apply impl_intro_l.
-  rewrite HQ /bi_except_0 !and_or_r. apply or_elim; last auto.
-  by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
+  rewrite !timeless_alt=> HQ R HR. apply impl_intro_l, HQ.
+  rewrite assoc -(comm _ P) -assoc. by apply impl_elim_r'.
 Qed.
 Global Instance sep_timeless P Q: Timeless P → Timeless Q → Timeless (P ∗ Q).
 Proof.
@@ -365,11 +377,9 @@ Qed.
 
 Global Instance wand_timeless `{!BiLöb PROP} P Q : Timeless Q → Timeless (P -∗ Q).
 Proof.
-  rewrite /Timeless=> HQ. rewrite later_false_em.
-  apply or_mono, wand_intro_l; first done.
-  rewrite -{2}(löb Q); apply impl_intro_l.
-  rewrite HQ /bi_except_0 !and_or_r. apply or_elim; last auto.
-  by rewrite (comm _ P) persistent_and_sep_assoc impl_elim_r wand_elim_l.
+  rewrite !timeless_alt=> HQ R HR. apply wand_intro_l, HQ.
+  rewrite persistent_and_affinely_sep_l assoc -(comm _ P) -assoc.
+  rewrite -persistent_and_affinely_sep_l. by apply wand_elim_r'.
 Qed.
 Global Instance forall_timeless {A} (Ψ : A → PROP) :
   (∀ x, Timeless (Ψ x)) → Timeless (∀ x, Ψ x).
-- 
GitLab