cleanup and doc-writing

_CoqProject

@@ -9,7 +9,7 @@ src/guarding/own_and_own_sep.v
 src/guarding/factoring_props.v
 src/guarding/guard.v
 src/guarding/tactics.v
-src/guarding/guard_later.v
+src/guarding/guard_later_pers.v
 
 src/guarding/storage_protocol/inved.v
 src/guarding/storage_protocol/protocol.v

src/examples/counting.v

@@ -17,7 +17,6 @@ From iris Require Import options.
 From iris.algebra Require Import auth.
 
 Require Import guarding.guard.
-Require Import guarding.guard_later.
 
 Require Import guarding.storage_protocol.protocol.
 Require Import guarding.storage_protocol.inved.

src/examples/forever.v

@@ -16,7 +16,6 @@ From lang Require Import lang.
 From iris Require Import options.
 
 Require Import guarding.guard.
-Require Import guarding.guard_later.
 Require Import examples.misc_tactics.
 Require Import guarding.storage_protocol.protocol.
 Require Import guarding.storage_protocol.inved.

src/examples/fractional.v

@@ -23,7 +23,6 @@ From lang Require Import lang.
 From iris Require Import options.
 
 Require Import guarding.guard.
-Require Import guarding.guard_later.
 Require Import guarding.storage_protocol.protocol.
 Require Import guarding.storage_protocol.inved.
 From iris.algebra Require Import auth.

src/examples/hash_table.v

@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Import invariants.
 From lang Require Import lang simp adequacy primitive_laws.
 
 Require Import guarding.guard.
-Require Import guarding.guard_later.
+Require Import guarding.guard_later_pers.
 Require Import guarding.lib.rwlock.
 
 From lang Require Import heap_ra.

src/examples/main.v

@@ -6,14 +6,14 @@ From iris.program_logic Require Import ectx_lifting.
 From iris Require Import options.
 
 Require Import guarding.guard.
+Require Import guarding.guard_later_pers.
 Require Import guarding.lib.rwlock.
 
 From lang Require Import lang simp adequacy primitive_laws.
 From lang Require Import heap_ra.
 
 From examples Require Import forever.
 From examples Require Import hash_table.
-From guarding Require Import guard_later.
 From examples Require Import seqs.
 From examples Require Import hash_table_logic.
 From examples Require Import hash_table_raw.

src/examples/rwlock.v

@@ -16,7 +16,7 @@ From lang Require Import heap_ra.
 From iris Require Import options.
 
 Require Import guarding.guard.
-Require Import guarding.guard_later.
+Require Import guarding.guard_later_pers.
 Require Import guarding.lib.rwlock.
 Require Import examples.misc_tactics.
 

src/guarding/factoring_props.v

@@ -1,81 +1,57 @@
-From iris.algebra Require Export cmra updates.
-From iris.algebra Require Import proofmode_classes.
-From iris.algebra Require Import auth.
-From iris.algebra Require Import functions.
-From iris.algebra Require Import gmap.
 From iris.prelude Require Import options.
-
+From iris.algebra Require Import cmra updates proofmode_classes auth functions gmap.
 From iris.base_logic Require Import upred.
-From iris.base_logic.lib Require Export own iprop.
-From iris.proofmode Require Import base.
-From iris.proofmode Require Import ltac_tactics.
-From iris.proofmode Require Import tactics.
-From iris.proofmode Require Import coq_tactics.
-
-From iris.base_logic.lib Require Export invariants.
-
-From iris.base_logic.lib Require Export fancy_updates.
-From iris.base_logic.lib Require Export fancy_updates_from_vs.
-
-From iris.bi Require Import derived_laws_later.
-
-From iris.proofmode Require Import coq_tactics reduction.
-From iris.proofmode Require Export tactics.
-From iris.program_logic Require Import atomic.
-From iris.prelude Require Import options.
-
-From iris.base_logic.lib Require Export wsat.
-
-From iris.bi Require Import derived_laws.
-
+From iris.base_logic.lib Require Import own iprop.
+From iris.base_logic.lib Require Import fancy_updates fancy_updates_from_vs.
+From iris.proofmode Require Import base ltac_tactics tactics coq_tactics reduction.
+From iris.bi Require Import derived_laws_later derived_laws.
 Require Import guarding.internal.factoring_upred.
 
 (**
-In general, it does *not* hold that:
-
+In general, it does _not_ hold that:
+<<
     (P ⊢ Q) → (P &&{_}&&> Q)
-    
+>>
 (See Appendix 1.4; https://arxiv.org/pdf/2309.04851 for a counter-example.)
 
 This does hold if we can "factor" P as Q ∗ R.
-
+<<
     (Q ∗ R) &&{_}&&> Q.
-    
+>>
 For this reason, it is useful to identify propositions that Q that are _always_
 factor-out-able in this sense. This is true for propositions like `own γ x`.
 That is, we have:
 
-    If `P ⊢ own γ x` then there is `Q` such that `P ⊣⊢ own γ x ∗ Q`
-    
-(Specifically, we can take `Q` to be `own γ x -∗ P`.)
+    If [`P ⊢ own γ x`] then there exists [Q] such that [P ⊣⊢ own γ x ∗ Q]
 
-This lets us prove:
+(Specifically, we can take [Q] to be [own γ x -∗ P].)
 
+This lets us prove:
+<<
     (P ⊢ own γ x) → P &&{_}&&> own γ x
-
+>>
 Now, I don't know if this particular rule is very useful, but this factorizability property
-*is* crucial for stating and proving Leaf's (∧)-related rules.
+_is_ crucial for stating and proving Leaf's (∧)-related rules.
 
 Unfortunately, I don't have a clean description of the class of propositions Q that
 meet this factorizability property, let alone one that also handles all the fiddly
-details with ◇ and ▷ that we need. I do know that all propositions of the form
-`uPred_ownM x` work for everything we need (thus any proposition of the form
-`own γ x` and ∗-conjunctions thereof). So that's what we classify here.
+details with [◇] and [▷] that we need. I do know that all propositions of the form
+[uPred_ownM x] work for everything we need (thus any proposition of the form
+[own γ x] and [∗]-conjunctions thereof). So that's what we classify here.
 
 This definitely isn't the complete set -- we should probably extend it to include
 persistent propositions at the very least.
 It would be nice to have a clean definition like:
-
+<<
     Definition can_always_factor_out Q := ∀ P , (P -∗ Q) ∗ P ⊢ Q ∗ (Q -∗ P).
-
+>>
 But from a definition like this, I haven't been able to answer basic questions, like
 whether this is true:
-
+<<
     can_always_factor_out P →
     can_always_factor_out Q →
     can_always_factor_out (P ∗ Q)
-    
-If you know a proof or counterexample to this, do let me know!
+>>   
 *)
 
 Section Factoring.

src/guarding/guard.v

@@ -1,14 +1,8 @@
-From iris.algebra Require Export cmra.
-From iris.algebra Require Import functions.
-From iris.algebra Require Import gmap.
 From iris.prelude Require Import options.
-
+From iris.algebra Require Import gmap auth.
 From iris.base_logic Require Import upred.
-From iris.base_logic.lib Require Export own iprop.
-From iris.base_logic.lib Require Export wsat invariants.
-
-From iris.algebra Require Import auth.
-
+From iris.base_logic.lib Require Export own iprop wsat invariants.
+From iris.base_logic.lib Require Import fancy_updates fancy_updates_from_vs.
 From iris.proofmode Require Export tactics.
 Require Import guarding.factoring_props.
 
@@ -1325,7 +1319,7 @@ Proof.
   iMod "b". iModIntro. iFrame.
 Qed.
 
-Definition lguards_include_pers (P X Q : iProp Σ) F n
+Lemma lguards_include_pers (P X Q : iProp Σ) F n
     (pers: Persistent P) :
   P ∗ (X &&{ F; n }&&> Q) ⊢ (X &&{ F; n }&&> (Q ∗ P)).
 Proof.
@@ -1339,7 +1333,7 @@ Qed.
 
 (* Guard-Pers *)
 
-Definition guards_include_pers (P X Q : iProp Σ) F
+Lemma guards_include_pers (P X Q : iProp Σ) F
     (pers: Persistent P) :
   P ∗ (X &&{ F }&&> Q) ⊢ (X &&{ F }&&> (Q ∗ P)).
 Proof.
@@ -1366,7 +1360,7 @@ Proof.
   iDestruct (lguards_weaken_rhs_r with "g") as "g". iFrame "g".
 Qed.
 
-Definition lguards_impl_point (P Q S : iProp Σ) F n
+Lemma lguards_impl_point (P Q S : iProp Σ) F n
     (point: point_prop S)
     (qrx: (Q ⊢ S))
     : (
@@ -1383,7 +1377,7 @@ Qed.
 
 (* Guard-Implies *)
 
-Definition guards_impl_point (P Q S : iProp Σ) F
+Lemma guards_impl_point (P Q S : iProp Σ) F
     (point: point_prop S)
     (qrx: (Q ⊢ S))
     : (
@@ -1395,7 +1389,7 @@ Proof.
   apply lguards_impl_point; trivial.
 Qed.
 
-Definition lguards_and_point (P Q R S : iProp Σ) F n
+Lemma lguards_and_point (P Q R S : iProp Σ) F n
     (point: point_prop S)
     (qrx: (Q ∧ R ⊢ S))
     : (
@@ -1419,7 +1413,7 @@ Qed.
 
 (* Guard-And *)
 
-Definition guards_and_point (P Q R S : iProp Σ) F
+Lemma guards_and_point (P Q R S : iProp Σ) F
     (point: point_prop S)
     (qrx: (Q ∧ R ⊢ S))
     : (
@@ -1431,7 +1425,7 @@ Proof.
   apply lguards_and_point; trivial.
 Qed.
 
-Definition guards_and (P Q R : iProp Σ) {A} `{ing : inG Σ A} γ (x: A) F
+Lemma guards_and (P Q R : iProp Σ) {A} `{ing : inG Σ A} γ (x: A) F
     (qrx: (Q ∧ R ⊢ own γ x))
     : (
       (P &&{F}&&> Q) ∗ (P &&{F}&&> R)
@@ -1601,4 +1595,3 @@ Notation "P &&{ E }&&> Q" := (guards P Q E)
 
 Notation "P &&{ E ; n }&&> Q" := (lguards P Q E n)
   (at level 99, E at level 50, Q at level 200).
-

src/guarding/guard_later.v → src/guarding/guard_later_pers.v

@@ -1,18 +1,19 @@
 From iris.algebra Require Export cmra.
-From iris.algebra Require Import functions.
-From iris.algebra Require Import gmap.
-From iris.prelude Require Import options.
-
 From iris.base_logic Require Import upred.
-From iris.base_logic.lib Require Export own iprop.
-From iris.base_logic.lib Require Export wsat invariants.
-
-From iris.algebra Require Import auth.
-
+From iris.base_logic.lib Require Export own iprop wsat invariants.
 From iris.proofmode Require Export tactics.
 Require Import guarding.guard.
 
-Section GuardLater.
+(** Say you have [P &&{E}&&> (▷ Q)] and you want to eliminate the [▷].
+If [Q] is timeless, you can do this with [guards_remove_later].
+
+What if [Q] is the conjunction of a timeless part and a persistent part?
+Persistent props can be moved in and out of guards easily.
+Thus you can eliminate the [▷] by moving the persistent part out,
+eliminating the later, then moving the persistent part back in.
+This file contains some type classes to automate this. *)
+
+Section GuardLaterPers.
 
 Class LaterGuardExtractable {Σ: gFunctors} (P : iProp Σ) := {
   extract_pers : iProp Σ;
@@ -75,7 +76,7 @@ Context `{!invGS Σ}.
 
 (* Later-Pers-Guard *)
 
-Definition extract_later1 (X T P : iProp Σ) E F
+Lemma extract_later1 (X T P : iProp Σ) E F
     (pers: Persistent P)
     (tl: Timeless T)
     (su: F ⊆ E)
@@ -99,7 +100,7 @@ Proof.
   iFrame "p". iFrame "g4".
 Qed.
 
-Definition extract_later (X S : iProp Σ) E F
+Lemma extract_later (X S : iProp Σ) E F
     (ex: LaterGuardExtractable S)
     (su: F ⊆ E)
     : ⊢ (X ∗ (X &&{F}&&> ▷ S)) ={E}=∗
@@ -111,5 +112,4 @@ Proof.
   - apply lg_timeless.
 Qed.
 
-
-End GuardLater.
+End GuardLaterPers.