Commit 9578026e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Strong framing.

parent bb16bae7
......@@ -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.
......@@ -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.
......
......@@ -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
......
......@@ -6,7 +6,7 @@ Inductive sel_pat :=
| SelPure
| SelPersistent
| SelSpatial
| SelName : string sel_pat.
| SelName : bool string sel_pat.
Fixpoint sel_pat_pure (ps : list sel_pat) : bool :=
match ps with
......@@ -19,7 +19,8 @@ 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)
......@@ -31,7 +32,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
......
......@@ -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)
......
......@@ -80,7 +80,7 @@ Ltac iElaborateSelPat pat tac :=
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"
......@@ -180,11 +180,14 @@ Local Ltac iFramePure t :=
[apply _ || fail "iFrame: cannot frame" φ
|iFrameFinish].
Local Ltac iFrameHyp H :=
Local Ltac iFrameHyp strong H :=
eapply tac_frame with _ H _ _ _;
[env_cbv; reflexivity || fail "iFrame:" H "not found"
|let R := match goal with |- Frame ?R _ _ => R end in
apply _ || fail "iFrame: cannot frame" R
lazymatch strong with
| false => apply _
| true => typeclasses eauto with typeclass_instances strong_frame
end || fail "iFrame: cannot frame" R
|iFrameFinish].
Local Ltac iFrameAnyPure :=
......@@ -192,7 +195,7 @@ Local Ltac iFrameAnyPure :=
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
......@@ -200,7 +203,7 @@ Local Ltac iFrameAnyPersistent :=
Local Ltac iFrameAnySpatial :=
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 true H; go Hs end in
match goal with
| |- of_envs ?Δ _ =>
let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
......@@ -236,7 +239,7 @@ Tactic Notation "iFrame" constr(Hs) :=
| SelPure :: ?Hs => iFrameAnyPure; go Hs
| SelPersistent :: ?Hs => iFrameAnyPersistent; go Hs
| SelSpatial :: ?Hs => iFrameAnySpatial; go Hs
| SelName ?H :: ?Hs => iFrameHyp H; 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 +325,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 +677,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 +699,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 +826,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 +1256,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 _;
......
......@@ -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)) =>
......
......@@ -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 R : uPred M) :
P - Q - R - (P Q R False).
Proof.
iIntros "^$ HQ HR {^$HR}".
iAssert (Q False)%I with "[^$HQ]" as "[HQ|[]]".
iFrame "^HQ".
Qed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment