Merge branch 'ci/cleanup_and_comments' into 'master'

Cleaned up codebase and updated README

See merge request !6

Makefile

@@ -100,7 +100,7 @@ supplements/builddep/%-builddep.opam: supplements/%.opam Makefile
 
 
 EXAMPLES_DIR := supplements/diaframe_heap_lang_examples
-BASE := diaframe_heap_lang/proof_automation.vo diaframe/lib/own_hints.vo diaframe/steps/local_post.vo
+BASE := diaframe_heap_lang/proof_automation.vo diaframe/lib/own_hints.vo
 TESTEXAMPLES := $(EXAMPLES_DIR)/comparison/spin_lock.vo $(EXAMPLES_DIR)/comparison/clh_lock.vo $(EXAMPLES_DIR)/comparison/arc.vo
 ACTRIS := $(patsubst %.v,%.vo,$(wildcard supplements/diaframe_actris/*.v))
 IRIS_EXAMPLES := $(patsubst %.v,%.vo,$(wildcard supplements/diaframe_iris_examples/*.v))
@@ -125,7 +125,7 @@ endif
 
 default: $(BASE)
 
-testexamples: $(BASE) $(TEST)
+testexamples: $(BASE) $(TESTEXAMPLES)
 
 actris: $(BASE) $(ACTRIS)
 

diaframe/env_utils.v

@@ -17,7 +17,7 @@ Definition envs_add_fresh {PROP} p (k : option ident) Q Δ :=
 
 (* Here envs_add_fresh : bool → option ident → PROP → envs PROP → option (envs PROP)
    and if (envs_add_fresh b mi P Δ) = Some Δ', then Δ' is equal to Δ with P as extra hypothesis.
-   if mi is None, the hypothesis with P is anonymous. If mi is Some i, the hypothesis has name i. 
+   if mi is None, the hypothesis P is anonymous. If mi is Some i, the hypothesis has name i.
 
    Below are lemmas which prove the required properties of envs_add_fresh
 *)

diaframe/hint_search/instances_base.v

@@ -32,7 +32,7 @@ Section biabd_instances.
   Proof. by rewrite /BiAbd /= !right_id. Qed.
 
   Global Instance bi_abd_empty_goal_from_emp p :
-    HINT □⟨p⟩ emp ✱ [- ; emp] ⊫ [@id PROP]; empty_goal ✱ [emp] | 50.
+    HINT □⟨p⟩ emp ✱ [- ; emp] ⊫ [@id PROP]; χ ✱ [emp] | 50.
   Proof. by rewrite /BiAbd /= empty_goal_eq bi.intuitionistically_if_elim. Qed.
 
 
@@ -50,7 +50,7 @@ Section biabd_instances.
     (TC∀.. (tt : TT), FromOr (tele_app P tt) (tele_app P1 tt) (tele_app P2 tt)) →
     SimplTeleEq TT teq →
     (TC∀.. (tt : TT), NormalizePropWrap (tele_app P tt) (tele_app P' tt)) →
-    BiAbd (TTl := TT) (TTr := TT) false empty_hyp_first P id P' (tele_map (tele_map (bi_pure)) (teq))%I | 40.
+    BiAbd (TTl := TT) (TTr := TT) false (ε₀)%I P id P' (tele_map (tele_map (bi_pure)) (teq))%I | 40.
   Proof.
     rewrite /NormalizePropWrap /NormalizeProp /BiAbd /SimplTeleEq /= empty_hyp_first_eq => _ /tforall_forall Hteq /tforall_forall HP.
     apply tforall_forall => ttl.
@@ -67,7 +67,7 @@ Section biabd_instances.
 
   Global Instance abd_if_bool_decide `{Decision φ} (L R : PROP) :
     (* cannot be a biabd, since the forall would not be introducable! *)
-    HINT1 empty_hyp_first ✱ [∀ (b : bool), (⌜b = true⌝ ∗ ⌜φ⌝ ∨ ⌜b = false⌝ ∗ ⌜¬φ⌝ )-∗ if b then L else R] 
+    HINT1 ε₀ ✱ [∀ (b : bool), (⌜b = true⌝ ∗ ⌜φ⌝ ∨ ⌜b = false⌝ ∗ ⌜¬φ⌝ )-∗ if b then L else R] 
         ⊫ [id]; if bool_decide φ then L else R.
   Proof.
     rewrite /Abduct /=.

diaframe/hint_search/lemmas_biabd.v

@@ -74,7 +74,7 @@ Section lemmas.
     (* S' := ∀.. tt1 : TT1, ∃.. ttl : tele_app TTl tt1, tele_app (tele_appd_dep S tt1) ttl *)
     TeleSummarize (tele_pointwise _ (flip (⊢@{PROP}))) (tele_curry T) T' →
     (* T' := λ tt2, ∃.. (tt : TeleConcatType TT1 TTl), tele_app (tele_curry T) tt *)
-    ModalityEC M →
+    ModalityStrongMono M →
     BiAbd (TTr := TT2) (TTl := [tele]) p P Q M S' T'.
   Proof.
     rewrite /IntoTExistExact /IntoTExist /BiAbd /= !bi_texist_exist => HP /tforall_forall HRS /tforall_forall HS /tforall_forall HT HM.
@@ -138,7 +138,7 @@ Section lemmas.
     apply H.
   Qed.
 
-(* IntoWand is too aggressive *)
+  (* IntoWand is too aggressive *)
   Lemma biabd_wand p P R V {TTl} {TTr} Q M S T :
     IntoWand2 p P R V →
     BiAbd (TTl := TTl) (TTr := TTr) false V Q M S T →
@@ -148,13 +148,13 @@ Section lemmas.
     by rewrite HPRV tele_map_app /= sep_comm -sep_assoc wand_elim_r sep_comm => ->.
   Qed.
 
-(* this is not strong enough: we want to condition here on M2
+  (* this is not strong enough: we want to condition here on M2
     if M2 commutes with later, then we want to add a later to S and T *)
   Lemma biabd_mod_intro_r p P {TTl TTr} φ Q MI Q' `(sel : TTr -t> A) M2 S T :
     (∀.. tt, TCAnd (FromModal (tele_app φ tt) MI (tele_app sel tt) (tele_app Q tt) (tele_app Q' tt)) (SolveSepSideCondition (tele_app φ tt))) →
     IntroducableModality MI →
     BiAbd (TTl := TTl) (TTr := TTr) p P Q' M2 S T →
-    ModalityEC M2 →
+    ModalityStrongMono M2 →
     BiAbd (TTl := TTl) (TTr := TTr) p P Q M2 S T.
   Proof.
     rewrite /BiAbd !tforall_forall => HQ HMI + HM2 ttl.
@@ -166,28 +166,28 @@ Section lemmas.
     apply HMI.
   Qed.
 
-(* for when P = |={⊤∖ ↑N, ⊤}=> P'*)
+  (* for when P = |={⊤∖ ↑N, ⊤}=> P'*)
   Lemma biabd_mod_intro_l p P M1 P' {TTl TTr} Q M2 S T M :
     IntoModal p P M1 P' →
-    ModalityEC M1 →
+    ModalityStrongMono M1 →
     BiAbd (TTl := TTl) (TTr := TTr) false P' Q M2 S T →
-    ModalityECCompat3 M M1 M2 → (* this (hopefully) normalizes M, so that we don't have M1 ∘ M2 *)
+    ModalityCompat3 M M1 M2 → (* this (hopefully) normalizes M, so that we don't have M1 ∘ M2 *)
     BiAbd (TTl := TTl) (TTr := TTr) p P Q M S T.
   Proof.
     rewrite /IntoModal /BiAbd /= !tforall_forall => HPP' HM HPS HM' ttl.
-    rewrite HPP' modality_ec_frame_l -HM'.
+    rewrite HPP' modality_strong_frame_l -HM'.
     by apply HM.
   Qed.
 
   Lemma biabd_sepl P P1 P2 {TTl TTr} Q M S T :
     IntoSepCareful P P1 P2 →
     BiAbd (TTl := TTl) (TTr := TTr) false P1 Q M S T →
-    ModalityEC M →
+    ModalityStrongMono M →
     BiAbd (TTl := TTl) (TTr := TTr) false P Q M S (tele_map (tele_map (bi_sep P2)) T).
   Proof.
     rewrite /BiAbd /IntoSepCareful !tforall_forall /= => HP + HM ttl.
     rewrite HP sep_comm sep_assoc (sep_comm (tele_app S _)) => ->.
-    rewrite modality_ec_frame_l.
+    rewrite modality_strong_frame_l.
     apply HM.
     iDestruct 1 as "[HQT HP]".
     iDestruct "HQT" as (tt) "[HQ HT]".
@@ -199,7 +199,7 @@ Section lemmas.
   Lemma biabd_sepr P P1 P2 {TTl TTr} Q M S T :
     IntoSepCareful P P1 P2 →
     BiAbd (TTl := TTl) (TTr := TTr) false P2 Q M S T →
-    ModalityEC M →
+    ModalityStrongMono M →
     BiAbd (TTl := TTl) (TTr := TTr) false P Q M S (tele_map (tele_map (bi_sep P1)) T).
   Proof.
     intros.

diaframe/hint_search/search_abd.v

@@ -11,53 +11,6 @@ Import bi.
 
 Set Universe Polymorphism.
 
-Section witness_postpone_optimization.
-  Context {PROP : bi}.
-  Implicit Types (M : PROP → PROP).
-
-  Lemma abd_forall_unif p P' `(P : A → PROP) {C : tele} TT Q M R (g : C -t> A) :
-    IntoForallCareful P' P →
-    (∀ (c : C), ∃ a' R',
-      Abduct (TT := TT) p (P a') Q M R' ∧
-      TCAnd (GatherEvarsEq a' (tele_app g c)) $ (* if g : C → A maybe the tactic can be simpler..? *)
-      TCEq R' (R c)
-    ) →
-    Abduct (TT := TT) p P' Q M (∃.. c, R c).
-  Proof.
-    rewrite /IntoForallCareful => HP Habd.
-    (* need to do some work before we can use abd_forall *)
-    rewrite /Abduct HP.
-    assert ((∃.. c, R c) ⊢ (∃.. c, tele_app (tele_bind R) c)) as ->.
-    { apply bi_texist_mono => tt. by rewrite tele_app_bind. }
-    eapply (abd_forall) => c.
-    destruct (Habd c) as [a' [R' [HPR [Ha' HR]]]].
-    revert Ha' HPR => /eq_from_gather_evars_eq ->.
-    rewrite /Abduct => <-.
-    apply bi.sep_mono_r. rewrite tele_app_bind HR //.
-  Qed.
-
-  Lemma abd_witness_unif {A : Type} {C : tele} {TTf : A → tele} (g : C -t> A) M R P (Q : TeleS TTf -t> PROP) p :
-    (∀ (c : C), ∃ a' R''',
-      Abduct (TT := TTf a') p P (Q a') M R''' ∧ (* R''': PROP! so stuff is not as difficult as in BiAbd *)
-      TCAnd (GatherEvarsEq a' (tele_app g c)) $
-      TCEq (R''') (R c)
-    ) →
-    ModalityMono M →
-    Abduct (TT := TeleS TTf) p P Q M (∃.. c, R c).
-  Proof.
-    move => HPR HM.
-    assert ((∃.. c, R c) ⊢ (∃.. c, tele_app (tele_bind R) c)) as ->.
-    { apply bi_texist_mono => tt. by rewrite tele_app_bind. }
-    eapply abd_goal_exist; last done.
-    move => c.
-    destruct (HPR c) as [a' [R' [HPR2 [Ha' ->]]]].
-    revert Ha' HPR2 => /eq_from_gather_evars_eq ->.
-    rewrite /Abduct => HPR2.
-    erewrite <-HPR2. rewrite tele_app_bind //.
-  Qed.
-
-End witness_postpone_optimization.
-
 Section witness_postpone_optimization.
   Context {PROP : bi}.
   Implicit Types (M : PROP → PROP).
@@ -134,7 +87,7 @@ Section stages_rec_mod.
       IntoModal p P M1 P' →
       SplitModality4 M Ml M1 M2 → (* it is valid and sometimes desired to keep a part of Ml around *)
       AbductModRec (TT := TTr) false P' Q M2 Mh S →
-      ModalityEC Mh →
+      ModalityStrongMono Mh →
       AbductModRec (TT := TTr) p P Q M Ml (Mh S).
     Proof.
       intros.

diaframe/hint_search/search_biabd.v

@@ -11,6 +11,8 @@ Import bi.
 
 Set Universe Polymorphism.
 
+(* This is some infrastructure to determine C, the telescope of generalizable evars *)
+
 Inductive TCEqFunApp {A} (x : A) : A → Prop := TCEqFunApp_refl : TCEqFunApp x x.
 Existing Class TCEqFunApp.
 
@@ -39,6 +41,7 @@ Section evar_retcon_optimization.
     (∀ (c : C), ∃ a' TTla S'' T'', (* S'' : TTla -t> PROP, T'' : TTla -t> TTr -t> PROP *)
       BiAbd (TTr := TTr) (TTl := TTla) p (P a') Q M S'' T'' ∧
       TCAnd (GatherEvarsEq a' (tele_app g c)) $ ∃ (HTTeq : TCEq TTla (TTl c)), 
+        (* yes, a lot of fun, we need eq_rect here *)
       TCAnd (TCEq (eq_rect TTla (λ T, T -t> PROP) S'' (TTl c) (TCEq_to_eq HTTeq)) (S c)) $ (* S : ∀ c, TTl c -t> PROP *)
       TCEq (eq_rect TTla (λ T, T -t> TTr -t> PROP) T'' (TTl c) (TCEq_to_eq HTTeq)) (T c)
     ) →
@@ -132,11 +135,7 @@ Section evar_retcon_optimization.
       TCAnd (TCEqFunApp (eq_rect TTl' (λ T, T -t> PROP) S'' (TTl a) (eq_from_eq_fun_app HTTeq)) (S a)) $
             (TCEqFunApp (eq_rect TTl' (λ T, T -t> TT2 -t> PROP) T'' (TTl a) (eq_from_eq_fun_app HTTeq)) (T a))
     ) →
-(*    TeleSummarize (⊢) (tele_bind (λ tt1, bi_texist $ tele_app $ tele_appd_dep S tt1)) S' →*)
-    (* S' := ∀.. tt1 : TT1, ∃.. ttl : tele_app TTl tt1, tele_app (tele_appd_dep S tt1) ttl *)
-(*    TeleSummarize (tele_pointwise _ (flip (⊢@{PROP}))) (tele_curry T) T' →*)
-    (* T' := λ tt2, ∃.. (tt : TeleConcatType TT1 TTl), tele_app (tele_curry T) tt *)
-    ModalityEC M →
+    ModalityStrongMono M →
     BiAbd (TTr := TT2) (TTl := [tele]) p P Q M (∀ a, ∃.. (ttl : TTl a), tele_app (S a) ttl)%I 
         (tele_bind (λ tt2, ∃ a, ∃.. (ttl : TTl a), tele_app (tele_app (T a) ttl) tt2))%I.
   Proof.
@@ -361,11 +360,11 @@ Section stages.
       move => ? HMs [[HP HMs']] HM1'. eapply unfoldhyp_from_base.
       - eapply biabd_mod_intro_l => //.
         * eapply HMs. 
-        * rewrite /ModalityECCompat3 => R //=.
+        * rewrite /ModalityCompat3 => R //=.
       - destruct HMs as [HMs1 HMs2 HMs3].
         destruct HMs' as [HMs1' HMs2' HMs3'].
         split.
-        * rewrite /ModalityECCompat3 => R //=.
+        * rewrite /ModalityCompat3 => R //=.
           rewrite -HMs1.
           apply HMs2, HMs3.
           rewrite -HMs1' -HM1' //=.

diaframe/lib/atomic.v

@@ -8,7 +8,7 @@ Import bi.
 
 Set Universe Polymorphism.
 
-(* hack to get around universe constraints *)
+(* 'hack' to get around universe constraints on the regular option type *)
 Inductive option2 (A : Type) :=
   | Some2 : A → option2 A
   | None2 : option2 A.
@@ -67,7 +67,7 @@ Section aupd_autom.
 
   (* when we need to prove an atomic update, we first run the greatest laterable fixpoint *)
   Global Instance abduct_aupd_as_gfp {TA TB : tele} Eo Ei (α : TA → PROP) (β Φ : TA → TB → PROP) :
-    HINT1 empty_hyp_last ✱ [greatest_laterable_fixpoint_wrt (λ Ψ, make_laterable $ atomic_acc' Eo Ei α Ψ β Φ) emp] ⊫ [id]; atomic_update Eo Ei α β Φ.
+    HINT1 ε₁ ✱ [greatest_laterable_fixpoint_wrt (λ Ψ, make_laterable $ atomic_acc' Eo Ei α Ψ β Φ) emp] ⊫ [id]; atomic_update Eo Ei α β Φ.
   Proof.
     rewrite /Abduct /= empty_hyp_last_eq left_id. rewrite <-atomic_update_to_gfp.
     rewrite greatest_laterable_fixpoint_wrt_eq.
@@ -82,7 +82,7 @@ Section aupd_autom.
   (* after running the fixpoint and introducing make_laterable, we proceed as follows: *)
   Global Instance atomic_acc_abd {TA TB : tele} Eo Ei' Ei (α : TA → PROP) P (β Φ : TA → TB → PROP) beq :
     SimplTeleEq TB beq →
-    HINT1 empty_hyp_first ✱ [
+    HINT1 ε₀ ✱ [
         |={Eo, Ei'}=> ∃.. x, α x ∗ (* A neat trick is that we need Ei ⊆ Ei', but we can actually defer that to below! *)
         (∀ (b : bool), ⌜b = true⌝ ∨ ⌜b = false⌝ -∗ ∀.. (my : if b then TB else [tele]),
           α x ∧ ⌜b = false⌝ ∨ (∃.. y : TB, β x y ∧ ⌜b = true⌝ ∧ ⌜match b, my with | true, y' => tele_app (tele_app beq y') y | false, _ => False end⌝) ={Ei',Eo}=∗ ⌜Ei ⊆ Ei'⌝ ∧ 

diaframe/lib/do_lob.v

@@ -5,6 +5,11 @@ From diaframe Require Import proofmode_base.
 Set Default Proof Using "Type*".
 
 
+(* Adds a do_löb constructor, and appropriate hints so that [do_löb TT args pre goal] 
+   will cause Löb induction to be done over (pre args -∗ goal args), while generalizing 
+   at least over (args : TT). It will generalize over more variables if they are detected
+   to be relevant *)
+
 Class AsFunOfOnly {A : Type} (a : A) {TT : tele} (tt : TT) (a' : TT -t> A) :=
   as_fun_of_only : tele_app a' tt = a.
 
@@ -123,13 +128,14 @@ Section do_lob_proofmode.
     AsSolveGoal M (do_löb TT args pre goal) (Transform $ do_löb TT args pre goal).
   Proof. unseal_diaframe; rewrite /AsSolveGoal. eauto. Qed.
 
+  (* TODO: this instance could maybe be dropped? *)
   Global Instance do_lob_re_intro_only p P TT (P' : TT -t> PROP) args pre goal : 
     VariablesOccurIn P args →
     AsFunOfOnly P args P' →
-    TransformHyp p P (do_löb TT args pre goal) 
-        (do_löb TT args 
+    TRANSFORM □⟨p⟩ P, do_löb TT args pre goal =[hyp]=> 
+        do_löb TT args 
             (tele_bind (λ tt, tele_app pre tt ∗ tele_app (tele_map (bi_intuitionistically_if p) P') tt))%I 
-         goal) | 20.
+         goal | 20.
   Proof.
     move => _ HP. rewrite /TransformHyp /=.
     assert (AsFunOfOnly (□?p P)%I args (tele_map (bi_intuitionistically_if p) P')).
@@ -141,12 +147,11 @@ Section do_lob_proofmode.
     VariablesOccurIn P tt1 →
     AsFunOfAmongOthers P tt1 tt2 P' →
     (TC∀.. (tt1 : TT1), AsFunOfOnly (tele_app goal tt1) tt2 (tele_app goal' tt1)) →
-    TransformHyp p P (do_löb TT1 tt1 pre goal)
-      (do_löb (TelePairType TT1 TT2) (tele_pair_arg tt1 tt2) 
+    TRANSFORM □⟨p⟩ P, do_löb TT1 tt1 pre goal =[hyp]=>
+      do_löb (TelePairType TT1 TT2) (tele_pair_arg tt1 tt2) 
             (tele_curry $ tele_dep_bind (λ tt1, tele_map (bi_sep (tele_app pre tt1)) $ 
                                                 as_dependent_fun _ _ (tele_map (λ f, tele_app f tt1) (tele_map (tele_map $ bi_intuitionistically_if p) P')) tt1))
-            (tele_curry $ tele_dep_bind (λ tt1, as_dependent_fun _ _  (tele_app goal' tt1) tt1))
-                    ) | 15.
+            (tele_curry $ tele_dep_bind (λ tt1, as_dependent_fun _ _  (tele_app goal' tt1) tt1)) | 15.
   Proof.
     move => _.
     rewrite /TransformHyp /TCTForall => HP Hgoal.
@@ -165,9 +170,9 @@ Section do_lob_proofmode.
 
   Global Instance run_do_lob_mod Δ (TT : tele) (args : TT) φ pre goal : 
     GatherPureOn args φ →
-    TransformCtx Δ (do_löb TT args pre goal)
+    TRANSFORM Δ, do_löb TT args pre goal =[ctx]=>
       ((□ ▷ (∀.. (tt : TT), tele_app pre tt ∗ [∗] (env_spatial Δ) ∗ <affine> ⌜tele_app φ tt⌝ -∗ tele_app goal tt)) -∗ 
-                         (∀.. (tt : TT), tele_app pre tt ∗ <affine> ⌜tele_app φ tt⌝ -∗ post_löb $ tele_app goal tt))%I.
+                         (∀.. (tt : TT), tele_app pre tt ∗ <affine> ⌜tele_app φ tt⌝ -∗ post_löb $ tele_app goal tt)).
   Proof.
     rewrite /TransformCtx. rewrite post_löb_eq.
     apply run_do_löb.
@@ -214,6 +219,9 @@ Ltac strip_known_fun_args :=
     enough (f = rhs_f) as H; [rewrite H; done | ]; strip_known_fun_args
   end.
 
+(* the NoLobGen class explicitly forbids do_löb from generalizing over certain variables.
+   For example, we dont want to generalize over the Σ in iProp Σ *)
+
 Class NoLobGen {A : Type} (a : A) := no_lob_gen : True.
 
 Global Instance dont_prop_gen (PROP : bi) : NoLobGen PROP := I.

diaframe/lib/frac_token.v

@@ -95,11 +95,11 @@ Section automation.
 
   Global Instance biabd_alloc_none q φ mq :
     CmraSubtract 1%Qp q φ mq →
-    HINT empty_hyp_last ✱ [⌜φ⌝] ⊫ [bupd] γ; no_tokens P γ q ✱ [default emp (q' ← mq; Some $ no_tokens P γ q')].
+    HINT ε₁ ✱ [- ; ⌜φ⌝] ⊫ [bupd] γ; no_tokens P γ q ✱ [default emp (q' ← mq; Some $ no_tokens P γ q')].
   Proof. apply: tokenizable.biabd_alloc_none. Qed.
 
   Global Instance biabd_alloc_some :
-    HINT empty_hyp_last ✱ [ - ; P 1] ⊫ [bupd] γ; token_counter P γ 1 ✱ [token P γ].
+    HINT ε₁ ✱ [ - ; P 1] ⊫ [bupd] γ; token_counter P γ 1 ✱ [token P γ].
   Proof. apply: tokenizable.biabd_alloc_some. Qed.
 
   Global Instance biabd_create_token γ p1 p2 :
@@ -231,7 +231,7 @@ Section token_counter_extra.
   Context {HP : Fractional P}.
 
   Global Instance biabd_alloc_multiple (p : positive) :
-    HINT empty_hyp_last ✱ [- ; P 1] ⊫ [bupd] γ; token_counter P γ p ✱ [token_iter P (Pos.to_nat p) γ] | 500.
+    HINT ε₁ ✱ [- ; P 1] ⊫ [bupd] γ; token_counter P γ p ✱ [token_iter P (Pos.to_nat p) γ] | 500.
   Proof.
     rewrite /BiAbd /= empty_hyp_last_eq left_id.
     rewrite -{1}(Pos2Nat.id p).

diaframe/lib/greatest_laterable_fixpoint.v

@@ -5,6 +5,10 @@ From diaframe Require Import proofmode_base.
 Set Default Proof Using "Type".
 
 
+(* Defines a 'greatest laterable fixpoint' and suitable hints.
+   Useful since "AU = greatest_laterable_fixpoint AACC" *)
+
+
 Global Instance unit_funs_ne {PROP : bi} (F : unit → PROP) : NonExpansive F.
 Proof. move => n1 [] [] //. Qed.
 
@@ -139,7 +143,7 @@ Section glp_lemmas.
   Global Instance transform_glfp_hyp F P R R' : 
     TCIf (Laterable P) False TCTrue →
     MakeSep R (▷ P) R' →
-    TransformHyp false P (greatest_laterable_fixpoint_wrt F R) (greatest_laterable_fixpoint_wrt F R').
+    TRANSFORM □⟨false⟩ P, greatest_laterable_fixpoint_wrt F R =[hyp]=> greatest_laterable_fixpoint_wrt F R'.
   Proof.
     rewrite /MakeSep => _ HPR.
     rewrite /TransformHyp /=. rewrite -HPR.
@@ -157,7 +161,7 @@ Section glp_lemmas.
 
   Global Instance glfp_introduce_no_spatial Δ F P :
     TCEq (env_spatial Δ) Enil →
-    TransformCtx Δ (greatest_laterable_fixpoint_wrt F P) (IntroduceHyp P (F P)) | 20.
+    TRANSFORM Δ, greatest_laterable_fixpoint_wrt F P =[ctx]=> IntroduceHyp P (F P) | 20.
   Proof.
     unseal_diaframe; rewrite /TransformCtx => HM.
     rewrite envs_entails_unseal. rewrite {2}env_spatial_is_nil_intuitionistically; last rewrite /env_spatial_is_nil HM //.
@@ -167,7 +171,7 @@ Section glp_lemmas.
   Global Instance glfp_introduce_all_laterable Δ F P :
     Laterable (PROP := PROP) emp →
     TCForall Laterable (env_spatial Δ) → 
-    TransformCtx Δ (greatest_laterable_fixpoint_wrt F P) (IntroduceHyp P (F ([∗] env_spatial Δ ∗ P)%I)) | 30.
+    TRANSFORM Δ, greatest_laterable_fixpoint_wrt F P =[ctx]=> IntroduceHyp P (F ([∗] env_spatial Δ ∗ P)%I) | 30.
   Proof.
     unseal_diaframe; rewrite /TransformCtx => Hemp HM.
     rewrite envs_entails_unseal of_envs_alt. revert HM.

diaframe/lib/int_as_nat_diff.v

@@ -20,7 +20,7 @@ Section nat_diff.
   Definition int_as_nat_diff (z : Z) (n1 n2 : nat) : PROP := ⌜int_as_nat_diff' z n1 n2⌝.
 
   Global Instance consume_nat_diff z n1 n2 : MergableConsume (int_as_nat_diff z n1 n2) (λ p Pin Pout,
-    TCAnd (TCEq Pin empty_hyp_first) $
+    TCAnd (TCEq Pin (ε₀)%I) $
           TCEq Pout ⌜z = (n1 - n2)%Z⌝%I).
   Proof.
     rewrite /MergableConsume /= => p Pin Pout [-> ->].
@@ -28,7 +28,7 @@ Section nat_diff.
   Qed.
 
   Global Instance nat_diff_unfold z n1 n2 : 
-    HINT empty_hyp_first ✱ [⌜int_as_nat_diff' z n1 n2⌝] ⊫ [id]; int_as_nat_diff z n1 n2 ✱ [True].
+    HINT ε₀ ✱ [- ; ⌜int_as_nat_diff' z n1 n2⌝] ⊫ [id]; int_as_nat_diff z n1 n2 ✱ [True].
   Proof. iStepsS. Qed.
 
   Global Instance nat_diff_timeless z n1 n2 : Timeless (int_as_nat_diff z n1 n2).

diaframe/lib/intuitionistically.v

@@ -16,7 +16,7 @@ Section intuitionistically.
 
   Global Instance intuitionistically_transform_ctx Δ P :
     TCEq (env_spatial Δ) Enil → 
-    TransformCtx Δ (□ P)%I P | 30.
+    TRANSFORM Δ , □ P =[ctx]=> P | 30.
   Proof.
     rewrite /TransformCtx => HM.
     rewrite envs_entails_unseal.
@@ -26,7 +26,7 @@ Section intuitionistically.
 
   Global Instance intuitionistically_intro_if (P : PROP) :
     Affine P → Persistent P →
-    HINT empty_hyp_first ✱ [- ; P] ⊫ [id] ; □ P ✱ [True].
+    HINT ε₀ ✱ [- ; P] ⊫ [id] ; □ P ✱ [True].
   Proof.
     move => HP1 HP2. iStepsS.
   Qed.

diaframe/lib/iris_hints.v

@@ -40,7 +40,7 @@ Section biabd_iris_instances.
   Global Arguments difference : simpl never. 
 
   Global Instance bi_abduct_inv P N E : 
-    HINT empty_hyp_last ✱ [▷ P] ⊫ [fupd E E]; inv N P ✱ [inv N P].
+    HINT ε₁ ✱ [- ; ▷ P] ⊫ [fupd E E]; inv N P ✱ [inv N P].
   Proof. 
     iStepS. rewrite inv_alloc. iStepsS.
   Qed.

diaframe/lib/laterable.v

@@ -2,6 +2,9 @@ From iris.bi Require Export bi telescopes lib.laterable.
 From iris.proofmode Require Import proofmode environments.
 From diaframe Require Import proofmode_base lib.intuitionistically.
 
+
+(* Adds support for goals of the form 'make_laterable G'. *)
+
 Section laterable_goal.
   Context {PROP : bi}.
   Implicit Type P : PROP.
@@ -13,7 +16,7 @@ Section laterable_goal.
 
   Global Instance make_laterable_re_intro P P' R :
     TCIf (Laterable P) False (IntoLaterable P P') →
-    TransformHyp false P (make_laterable R) (make_laterable $ IntroduceHyp P' R).
+    TRANSFORM □⟨false⟩ P, make_laterable R =[hyp]=> (make_laterable $ IntroduceHyp P' R).
   Proof.
     rewrite /TransformHyp. unseal_diaframe => /=.
     move => [Hl [] | HPQ].
@@ -33,7 +36,7 @@ Section laterable_goal.
   Global Instance make_laterable_introducable Δ P :
     Laterable (PROP := PROP) emp%I →
     TCForall Laterable (env_to_list $ env_spatial Δ) → 
-    TransformCtx Δ (make_laterable P) P | 30.
+    TRANSFORM Δ, make_laterable P =[ctx]=> P | 30.
   Proof.
     rewrite /TransformCtx => He HM.
     rewrite envs_entails_unseal => HΔ.
@@ -96,7 +99,7 @@ Section laterable_hyp.
   Lemma biabd_through_later_later_part (TT : tele) (P P' L : TT -t> PROP) teq :
     (TC∀.. (tt : TT), TCEq (tele_app P tt) (▷ later_part_of (tele_app L tt) (tele_app P' tt))%I) →
     SimplTeleEq TT teq →
-    BiAbd (TTl := TT) (TTr := TT) false empty_hyp_first P id (tele_bind (λ tt, later_later_part_of (tele_app L tt) (tele_app P' tt))) (tele_map (tele_map (bi_pure)) (teq))%I.
+    BiAbd (TTl := TT) (TTr := TT) false (ε₀)%I P id (tele_bind (λ tt, later_later_part_of (tele_app L tt) (tele_app P' tt))) (tele_map (tele_map (bi_pure)) (teq))%I.
   Proof.
     rewrite /BiAbd /SimplTeleEq /= => /tforall_forall HP /tforall_forall Hteq.
     apply tforall_forall => ttl.

diaframe/lib/own_hints.v

@@ -1969,7 +1969,7 @@ Section generic_instances.
   Global Instance mergable_drop_unit {A : ucmra} `{!inG Σ A} (a : A) γ :
     AsCmraUnit a →
     MergableConsume (own γ a) (PROP := iPropI Σ) (λ p Pin Pout,
-      TCAnd (TCEq Pin empty_hyp_first)
+      TCAnd (TCEq Pin (ε₀)%I)
             (TCEq Pout emp%I)) | 9. 
     (* this should trigger soon, so that we don't look for other stuff in our environment. if its ε, we won't learn anything *)
     (* TODO: are there units for which ✓ ε is non-trivial? if so, we need to change emp to ✓ ε *)
@@ -1980,7 +1980,7 @@ Section generic_instances.
 
   Global Instance unit_abduct2 {A : ucmra} `{inG Σ A} (x : A) γ :
     AsCmraUnit x →
-    HINT empty_hyp_last ✱ [- ; emp] ⊫ [bupd]; own γ x ✱ [emp] | 150.
+    HINT ε₁ ✱ [- ; emp] ⊫ [bupd]; own γ x ✱ [emp] | 150.
   Proof.
     move => ->. iStepS. rewrite right_id. iApply own_unit.
   Qed.
@@ -2047,7 +2047,7 @@ Section generic_instances.
 
   Global Instance biabd_cmra_subtract {A : cmra} `{!inG Σ A} (a b : A) γ φ mc p :
     CmraSubtract a b φ mc →
-    HINT □⟨p⟩ own γ a ✱ [⌜φ⌝] ⊫ [id]; own γ b ✱ [match mc with | Some c => own γ c | None => emp%I end] | 41.
+    HINT □⟨p⟩ own γ a ✱ [- ; ⌜φ⌝] ⊫ [id]; own γ b ✱ [match mc with | Some c => own γ c | None => emp%I end] | 41.
   Proof.
     rewrite /CmraSubtract => Hφ.
     iStepS.
@@ -2059,7 +2059,7 @@ Section generic_instances.
 
   Global Instance biabd_alloc_coalloc `{inG Σ A} a b :
     CoAllocate (A := A) a b →
-    HINT empty_hyp_last ✱ [⌜✓ a⌝] ⊫ [bupd] γ; own γ a ✱ [match b with | Some b => own γ b | _ => emp end].
+    HINT ε₁ ✱ [- ; ⌜✓ a⌝] ⊫ [bupd] γ; own γ a ✱ [match b with | Some b => own γ b | _ => emp end].
   Proof.
     case => Ha _. iStepS.
     iMod (own_alloc (a ⋅? b)) as (γ) "Hab". { apply Ha, H0. }

diaframe/lib/persistently.v

@@ -16,14 +16,14 @@ Section persistently.
 
 
   Global Instance persistently_transform_hyp P R : 
-    TransformHyp false P (<pers> R)%I (<pers> R)%I.
+    TRANSFORM □⟨false⟩ P, <pers> R =[hyp]=> <pers> R.
   Proof.
     rewrite /TransformHyp /=.
     iIntros "$". eauto.