Commit 75ad3b2e authored by Robbert Krebbers's avatar Robbert Krebbers

Support for framing pure hypotheses.

This closes issue 32.
parent 6f8c17a5
Pipeline #2713 passed with stage
in 9 minutes and 21 seconds
......@@ -81,11 +81,16 @@ Elimination of logical connectives
Separating logic specific tactics
---------------------------------
- `iFrame "H0 ... Hn"` : cancel the hypotheses `H0 ... Hn` in the goal. The
symbol `★` can be used to frame as much of the spatial context as possible,
and the symbol `#` can be used to repeatedly frame as much of the persistent
context as possible. When without arguments, it attempts to frame all spatial
hypotheses.
- `iFrame (t1 .. tn) "H0 ... Hn"` : cancel the Coq terms (or Coq hypotheses)
`t1 ... tn` and Iris hypotheses `H0 ... Hn` in the goal. Apart from
hypotheses, the following symbols can be used:
+ `%` : repeatedly frame hypotheses from the Coq context.
+ `#` : repeatedly frame hypotheses from the persistent context.
+ `★` : frame as much of the spatial context as possible.
Notice that framing spatial hypotheses makes them disappear, but framing Coq
or persistent hypotheses does not make them disappear.
- `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into
`H : P1 ★ P2`.
......
......@@ -219,6 +219,8 @@ Qed.
(* Frame *)
Global Instance frame_here R : Frame R R True.
Proof. by rewrite /Frame right_id. Qed.
Global Instance frame_here_pure φ Q : FromPure Q φ Frame ( φ) Q True.
Proof. rewrite /FromPure /Frame=> ->. by rewrite right_id. Qed.
Class MakeSep (P Q PQ : uPred M) := make_sep : P Q ⊣⊢ PQ.
Global Instance make_sep_true_l P : MakeSep True P P.
......
......@@ -685,6 +685,10 @@ Proof.
Qed.
(** * Framing *)
Lemma tac_frame_pure Δ (φ : Prop) P Q :
φ Frame ( φ) P Q (Δ Q) Δ P.
Proof. intros ?? ->. by rewrite -(frame ( φ) P) pure_equiv // left_id. Qed.
Lemma tac_frame Δ Δ' i p R P Q :
envs_lookup_delete i Δ = Some (p, R, Δ') Frame R P Q
((if p then Δ else Δ') Q) Δ P.
......
......@@ -430,6 +430,11 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
|env_cbv; reflexivity || fail "iCombine:" H "not fresh"|].
(** Framing *)
Local Ltac iFramePure t :=
let φ := type of t in
eapply (tac_frame_pure _ _ _ _ t);
[apply _ || fail "iFrame: cannot frame" φ|].
Local Ltac iFrameHyp H :=
eapply tac_frame with _ H _ _ _;
[env_cbv; reflexivity || fail "iFrame:" H "not found"
......@@ -437,7 +442,10 @@ Local Ltac iFrameHyp H :=
apply _ || fail "iFrame: cannot frame" R
|lazy iota beta].
Local Ltac iFramePersistent :=
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 goal with
......@@ -445,7 +453,7 @@ Local Ltac iFramePersistent :=
let Hs := eval cbv in (env_dom (env_persistent Δ)) in go Hs
end.
Local Ltac iFrameSpatial :=
Local Ltac iFrameAnySpatial :=
let rec go Hs :=
match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp H; go Hs end in
match goal with
......@@ -453,17 +461,60 @@ Local Ltac iFrameSpatial :=
let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
end.
Tactic Notation "iFrame" := iFrameAnySpatial.
Tactic Notation "iFrame" "(" constr(t1) ")" :=
iFramePure t1.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) ")" :=
iFramePure t1; iFrame ( t2 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) ")" :=
iFramePure t1; iFrame ( t2 t3 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4) ")" :=
iFramePure t1; iFrame ( t2 t3 t4 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
constr(t5) ")" :=
iFramePure t1; iFrame ( t2 t3 t4 t5 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
constr(t5) constr(t6) ")" :=
iFramePure t1; iFrame ( t2 t3 t4 t5 t6 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
constr(t5) constr(t6) constr(t7) ")" :=
iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
constr(t5) constr(t6) constr(t7) constr(t8)")" :=
iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ).
Tactic Notation "iFrame" constr(Hs) :=
let rec go Hs :=
match Hs with
| [] => idtac
| "#" :: ?Hs => iFramePersistent; go Hs
| "★" :: ?Hs => iFrameSpatial; go Hs
| "%" :: ?Hs => iFrameAnyPure; go Hs
| "#" :: ?Hs => iFrameAnyPersistent; go Hs
| "★" :: ?Hs => iFrameAnySpatial; go Hs
| ?H :: ?Hs => iFrameHyp H; go Hs
end
in let Hs := words Hs in go Hs.
Tactic Notation "iFrame" := iFrameSpatial.
Tactic Notation "iFrame" "(" constr(t1) ")" constr(Hs) :=
iFramePure t1; iFrame Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) ")" constr(Hs) :=
iFramePure t1; iFrame ( t2 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) ")" constr(Hs) :=
iFramePure t1; iFrame ( t2 t3 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4) ")"
constr(Hs) :=
iFramePure t1; iFrame ( t2 t3 t4 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
constr(t5) ")" constr(Hs) :=
iFramePure t1; iFrame ( t2 t3 t4 t5 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
constr(t5) constr(t6) ")" constr(Hs) :=
iFramePure t1; iFrame ( t2 t3 t4 t5 t6 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
constr(t5) constr(t6) constr(t7) ")" constr(Hs) :=
iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
constr(t5) constr(t6) constr(t7) constr(t8)")" constr(Hs) :=
iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ) Hs.
(** * Existential *)
Tactic Notation "iExists" uconstr(x1) :=
......
......@@ -100,3 +100,7 @@ Section iris.
- done.
Qed.
End iris.
Lemma demo_9 (M : ucmraT) (x y z : M) :
x (y z) ( x x y z : uPred M).
Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed.
Markdown is supported
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