.gitlab-ci.yml

@@ -23,6 +23,7 @@ iris-coq8.6:
   - master
   - ci
   - timing
+  - strong_frame
   artifacts:
     paths:
     - build-time.txt

theories/proofmode/class_instances.v

@@ -520,9 +520,15 @@ Global Instance make_or_true_r P : MakeOr P True True.
 Proof. by rewrite /MakeOr right_absorb. Qed.
 Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
 Proof. done. Qed.
-Global Instance frame_or R P1 P2 Q1 Q2 Q :
-  Frame R P1 Q1 → Frame R P2 Q2 → MakeOr Q1 Q2 Q → Frame R (P1 ∨ P2) Q.
-Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
+
+Global Instance frame_or_l R P1 P2 Q1 Q2 Q :
+  Frame R P1 Q1 → MaybeFrame R P2 Q2 → MakeOr Q1 Q2 Q → Frame R (P1 ∨ P2) Q.
+Proof. rewrite /Frame /MaybeFrame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
+Lemma frame_or_r R P1 P2 Q2 Q :
+  Frame R P2 Q2 → MakeOr P1 Q2 Q → Frame R (P1 ∨ P2) Q.
+Proof.
+  rewrite /Frame /MaybeFrame /MakeOr => <- <-. by rewrite sep_or_l sep_elim_r.
+Qed.
 
 Global Instance frame_wand R P1 P2 Q2 :
   Frame R P2 Q2 → Frame R (P1 -∗ P2) (P1 -∗ Q2).
@@ -717,4 +723,6 @@ Proof.
 Qed.
 End classes.
 
+Hint Resolve frame_or_r : strong_frame.
+
 Hint Mode ProgIntoLaterN + - ! - : typeclass_instances.

theories/proofmode/classes.v

@@ -72,6 +72,16 @@ Class Frame {M} (R P Q : uPred M) := frame : R ∗ Q ⊢ P.
 Arguments frame {_} _ _ _ {_}.
 Hint Mode Frame + ! ! - : typeclass_instances.
 
+Class MaybeFrame {M} (R P Q : uPred M) := maybe_frame : R ∗ Q ⊢ P.
+Arguments maybe_frame {_} _ _ _ {_}.
+Hint Mode MaybeFrame + ! ! - : typeclass_instances.
+
+Instance maybe_frame_frame {M} (R P Q : uPred M) : Frame R P Q → MaybeFrame R P Q.
+Proof. done. Qed.
+Lemma maybe_frame_default {M} (R P : uPred M) : MaybeFrame R P P.
+Proof. apply sep_elim_r. Qed.
+Hint Resolve maybe_frame_default : strong_frame.
+
 Class FromOr {M} (P Q1 Q2 : uPred M) := from_or : Q1 ∨ Q2 ⊢ P.
 Arguments from_or {_} _ _ _ {_}.
 Hint Mode FromOr + ! - - : typeclass_instances.

theories/proofmode/intro_patterns.v

@@ -6,7 +6,7 @@ Inductive intro_pat :=
   | IName : string → intro_pat
   | IAnom : intro_pat
   | IDrop : intro_pat
-  | IFrame : intro_pat
+  | IFrame : bool → intro_pat
   | IList : list (list intro_pat) → intro_pat
   | IPureElim : intro_pat
   | IAlwaysElim : intro_pat → intro_pat
@@ -18,7 +18,7 @@ Inductive intro_pat :=
   | IForall : intro_pat
   | IAll : intro_pat
   | IClear : string → intro_pat
-  | IClearFrame : string → intro_pat.
+  | IClearFrame : bool → string → intro_pat.
 
 Module intro_pat.
 Inductive stack_item :=
@@ -73,7 +73,8 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | TName "_" :: ts => parse_go ts (SPat IDrop :: k)
   | TName s :: ts => parse_go ts (SPat (IName s) :: k)
   | TAnom :: ts => parse_go ts (SPat IAnom :: k)
-  | TFrame :: ts => parse_go ts (SPat IFrame :: k)
+  | THat :: TFrame :: ts => parse_go ts (SPat (IFrame true) :: k)
+  | TFrame :: ts => parse_go ts (SPat (IFrame false) :: k)
   | TBracketL :: ts => parse_go ts (SList :: k)
   | TBar :: ts => parse_go ts (SBar :: k)
   | TBracketR :: ts => close_list k [] [] ≫= parse_go ts
@@ -94,7 +95,8 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   end
 with parse_clear (ts : list token) (k : stack) : option stack :=
   match ts with
-  | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame s) :: k)
+  | THat :: TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame true s) :: k)
+  | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame false s) :: k)
   | TName s :: ts => parse_clear ts (SPat (IClear s) :: k)
   | TBraceR :: ts => parse_go ts k
   | _ => None

theories/proofmode/sel_patterns.v

@@ -5,8 +5,8 @@ Set Default Proof Using "Type".
 Inductive sel_pat :=
   | SelPure
   | SelPersistent
-  | SelSpatial
-  | SelName : string → sel_pat.
+  | SelSpatial : bool → sel_pat
+  | SelName : bool → string → sel_pat.
 
 Fixpoint sel_pat_pure (ps : list sel_pat) : bool :=
   match ps with
@@ -19,10 +19,12 @@ Module sel_pat.
 Fixpoint parse_go (ts : list token) (k : list sel_pat) : option (list sel_pat) :=
   match ts with
   | [] => Some (reverse k)
-  | TName s :: ts => parse_go ts (SelName s :: k)
+  | THat :: TName s :: ts => parse_go ts (SelName true s :: k)
+  | TName s :: ts => parse_go ts (SelName false s :: k)
   | TPure :: ts => parse_go ts (SelPure :: k)
   | TAlways :: ts => parse_go ts (SelPersistent :: k)
-  | TSep :: ts => parse_go ts (SelSpatial :: k)
+  | THat :: TSep :: ts => parse_go ts (SelSpatial true :: k)
+  | TSep :: ts => parse_go ts (SelSpatial false :: k)
   | _ => None
   end.
 Definition parse (s : string) : option (list sel_pat) :=
@@ -31,7 +33,8 @@ Definition parse (s : string) : option (list sel_pat) :=
 Ltac parse s :=
   lazymatch type of s with
   | list sel_pat => s
-  | list string => eval vm_compute in (SelName <$> s)
+  | list string => eval vm_compute in (SelName false <$> s)
+  | list (bool * string) => eval vm_compute in (curry SelName <$> s)
   | string =>
      lazymatch eval vm_compute in (parse s) with
      | Some ?pats => pats | _ => fail "invalid sel_pat" s

theories/proofmode/spec_patterns.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 Record spec_goal := SpecGoal {
   spec_goal_modal : bool;
   spec_goal_negate : bool;
-  spec_goal_frame : list string;
+  spec_goal_frame : list (bool * string);
   spec_goal_hyps : list string
 }.
 
@@ -46,9 +46,12 @@ with parse_goal (ts : list token) (g : spec_goal)
   | TName s :: ts =>
      parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
        (spec_goal_frame g) (s :: spec_goal_hyps g)) k
+  | THat :: TFrame :: TName s :: ts =>
+     parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
+       ((true,s) :: spec_goal_frame g) (spec_goal_hyps g)) k
   | TFrame :: TName s :: ts =>
      parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
-       (s :: spec_goal_frame g) (spec_goal_hyps g)) k
+       ((false,s) :: spec_goal_frame g) (spec_goal_hyps g)) k
   | TBracketR :: ts =>
      parse_go ts (SGoal (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
        (reverse (spec_goal_frame g)) (reverse (spec_goal_hyps g))) :: k)

theories/proofmode/tactics.v

@@ -76,11 +76,11 @@ Ltac iElaborateSelPat pat tac :=
        let Hs' := eval env_cbv in (env_dom (env_persistent Δ)) in
        let Δ' := eval env_cbv in (envs_clear_persistent Δ) in
        go pat Δ' ((ESelName true <$> Hs') ++ Hs)
-    | SelSpatial :: ?pat =>
+    | SelSpatial _ :: ?pat =>
        let Hs' := eval env_cbv in (env_dom (env_spatial Δ)) in
        let Δ' := eval env_cbv in (envs_clear_spatial Δ) in
        go pat Δ' ((ESelName false <$> Hs') ++ Hs)
-    | SelName ?H :: ?pat =>
+    | SelName _ ?H :: ?pat =>
        lazymatch eval env_cbv in (envs_lookup_delete H Δ) with
        | Some (?p,_,?Δ') => go pat Δ' (ESelName p H :: Hs)
        | None => fail "iElaborateSelPat:" H "not found"
@@ -177,36 +177,45 @@ Local Ltac iFrameFinish :=
 Local Ltac iFramePure t :=
   let φ := type of t in
   eapply (tac_frame_pure _ _ _ _ t);
-    [apply _ || fail "iFrame: cannot frame" φ
+    [typeclasses eauto with typeclass_instances strong_frame
+     || fail "iFrame: cannot frame" φ
     |iFrameFinish].
 
-Local Ltac iFrameHyp H :=
-  eapply tac_frame with _ H _ _ _;
-    [env_cbv; reflexivity || fail "iFrame:" H "not found"
+Local Ltac iFrameHyp strong H :=
+  (* Create an evar so we can remember whether the hypothesis is persistent. If
+  it is, we won't drop the hypothesis anyway, so we can use strong framing
+  safely. *)
+  let q := fresh in evar (q : bool);
+  eapply tac_frame with _ H q _ _;
+    [env_cbv; apply: reflexivity (* reflexivity fails because of the evar *)
+      || fail "iFrame:" H "not found"
     |let R := match goal with |- Frame ?R _ _ => R end in
-     apply _ || fail "iFrame: cannot frame" R
-    |iFrameFinish].
+     lazymatch eval compute in (q || strong) with
+     | false => apply _
+     | true => typeclasses eauto with typeclass_instances strong_frame
+     end || fail "iFrame: cannot frame" R
+    |unfold q; clear q; iFrameFinish].
 
 Local Ltac iFrameAnyPure :=
   repeat match goal with H : _ |- _ => iFramePure H end.
 
 Local Ltac iFrameAnyPersistent :=
   let rec go Hs :=
-    match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
+    match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp false H; go Hs end in
   match goal with
   | |- of_envs ?Δ ⊢ _ =>
      let Hs := eval cbv in (env_dom (env_persistent Δ)) in go Hs
   end.
 
-Local Ltac iFrameAnySpatial :=
+Local Ltac iFrameAnySpatial strong :=
   let rec go Hs :=
-    match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp H; go Hs end in
+    match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp strong H; go Hs end in
   match goal with
   | |- of_envs ?Δ ⊢ _ =>
      let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
   end.
 
-Tactic Notation "iFrame" := iFrameAnySpatial.
+Tactic Notation "iFrame" := iFrameAnySpatial false.
 
 Tactic Notation "iFrame" "(" constr(t1) ")" :=
   iFramePure t1.
@@ -235,8 +244,8 @@ Tactic Notation "iFrame" constr(Hs) :=
     | [] => idtac
     | SelPure :: ?Hs => iFrameAnyPure; go Hs
     | SelPersistent :: ?Hs => iFrameAnyPersistent; go Hs
-    | SelSpatial :: ?Hs => iFrameAnySpatial; go Hs
-    | SelName ?H :: ?Hs => iFrameHyp H; go Hs
+    | SelSpatial ?b :: ?Hs => iFrameAnySpatial b; go Hs
+    | SelName ?b ?H :: ?Hs => iFrameHyp b H; go Hs
     end
   in let Hs := sel_pat.parse Hs in go Hs.
 Tactic Notation "iFrame" "(" constr(t1) ")" constr(Hs) :=
@@ -322,7 +331,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
          |(*goal*)
          |go H1 pats]
     | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs) :: ?pats =>
-       let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
+       let Hs' := eval cbv in (if lr then Hs else (snd <$> Hs_frame) ++ Hs) in
        eapply tac_specialize_assert with _ _ _ H1 _ lr Hs' _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
@@ -674,7 +683,7 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
     lazymatch pat with
     | IAnom => idtac
     | IDrop => iClear Hz
-    | IFrame => iFrame Hz
+    | IFrame ?b => iFrameHyp b Hz
     | IName ?y => iRename Hz into y
     | IList [[]] => iExFalso; iExact Hz
     | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as true Hz; go Hz pat1
@@ -696,7 +705,7 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
       end
     | ISimpl :: ?pats => simpl; find_pat found pats
     | IClear ?H :: ?pats => iClear H; find_pat found pats
-    | IClearFrame ?H :: ?pats => iFrame H; find_pat found pats
+    | IClearFrame ?b ?H :: ?pats => iFrameHyp b H; find_pat found pats
     | ?pat :: ?pats =>
        lazymatch found with
        | false => go H pat; find_pat true pats
@@ -823,7 +832,7 @@ Tactic Notation "iIntros" constr(pat) :=
     (* Clearing and simplifying introduction patterns *)
     | ISimpl :: ?pats => simpl; go pats
     | IClear ?H :: ?pats => iClear H; go pats
-    | IClearFrame ?H :: ?pats => iFrame H; go pats
+    | IClearFrame ?b ?H :: ?pats => iFrameHyp b H; go pats
     (* Introduction + destruct *)
     | IAlwaysElim ?pat :: ?pats =>
        let H := iFresh in iIntro #H; iDestructHyp H as pat; go pats
@@ -1253,7 +1262,7 @@ Tactic Notation "iAssertCore" open_constr(Q)
        |apply _ || fail "iAssert:" Q "not persistent"
        |tac H]
   | [SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs)] =>
-     let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
+     let Hs' := eval cbv in (if lr then Hs else (snd <$> Hs_frame) ++ Hs) in
      match eval cbv in (p && negb m) with
      | false =>
        eapply tac_assert with _ _ _ lr Hs' H Q _;

theories/proofmode/tokens.v

@@ -23,7 +23,8 @@ Inductive token :=
   | TForall : token
   | TAll : token
   | TMinus : token
-  | TSep : token.
+  | TSep : token
+  | THat : token.
 
 Fixpoint cons_name (kn : string) (k : list token) : list token :=
   match kn with "" => k | _ => TName (string_rev kn) :: k end.
@@ -50,6 +51,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String "*" (String "*" s) => tokenize_go s (TAll :: cons_name kn k) ""
   | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
   | String "-" s => tokenize_go s (TMinus :: cons_name kn k) ""
+  | String "^" s => tokenize_go s (THat :: cons_name kn k) ""
   | String (Ascii.Ascii false true false false false true true true) (* unicode ∗ *)
       (String (Ascii.Ascii false false false true false false false true)
       (String (Ascii.Ascii true true true false true false false true) s)) =>

theories/tests/proofmode.v

@@ -146,3 +146,11 @@ Proof. eauto with iFrame. Qed.
 Lemma demo_17 (M : ucmraT) (P Q R : uPred M) `{!PersistentP R} :
   P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
 Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.
+
+Lemma demo_18 (M : ucmraT) (P Q Q2 R : uPred M) `{!PersistentP Q2}:
+  P -∗ Q -∗ Q2 -∗ R -∗ (P ∗ Q ∗ Q2 ∨ R ∗ False).
+Proof.
+  iIntros "^$ HQ1 #HQ2 HR {^$HR}".
+  iAssert (Q ∨ False)%I with "[^$HQ1]" as "[HQ1|[]]".
+  iFrame "^HQ1 HQ2".
+Qed.