Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
I
Iris
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
95
Issues
95
List
Boards
Labels
Milestones
Merge Requests
10
Merge Requests
10
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Iris
Iris
Commits
613c7a7d
Commit
613c7a7d
authored
Nov 08, 2019
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Simplify `iIntoEmpValid`.
parent
83b31bbd
Changes
6
Hide whitespace changes
Inline
Sidebyside
Showing
6 changed files
with
48 additions
and
69 deletions
+48
69
tests/proofmode.ref
tests/proofmode.ref
+5
5
theories/base_logic/lib/boxes.v
theories/base_logic/lib/boxes.v
+4
4
theories/base_logic/lib/saved_prop.v
theories/base_logic/lib/saved_prop.v
+3
2
theories/bi/lib/fixpoint.v
theories/bi/lib/fixpoint.v
+1
1
theories/proofmode/coq_tactics.v
theories/proofmode/coq_tactics.v
+15
4
theories/proofmode/ltac_tactics.v
theories/proofmode/ltac_tactics.v
+20
53
No files found.
tests/proofmode.ref
View file @
613c7a7d
...
...
@@ 578,13 +578,13 @@ Tactic failure: iStartProof: not a BI assertion.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (
constr) as (tactic3)" and
"
<iris.proofmode.ltac_tactics.iIntoEmpValid>
", last call failed.
Tactic failure: iPoseProof: not a BI assertion.
"iPoseProofCoreLem (
open_constr) as (tactic3)" and
"
iIntoEmpValid
", last call failed.
Tactic failure: iPoseProof:
(0 = 0)
not a BI assertion.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to
"iPoseProofCoreLem (
open_
constr) as (tactic3)", "tac" (bound to
fun Htmp => spec_tac Htmp; [ ..  tac Htmp ]), "tac" (bound to
fun Htmp => spec_tac Htmp; [ ..  tac Htmp ]), "tac" (bound to
fun H => iDestructHyp H as pat), "iDestructHyp (constr) as (constr)",
...
...
@@ 604,7 +604,7 @@ Tactic failure: iPoseProof: "Hx" not found.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to
"iPoseProofCoreLem (
open_
constr) as (tactic3)", "tac" (bound to
fun Htmp => spec_tac Htmp; [ ..  tac Htmp ]), "tac" (bound to
fun Htmp => spec_tac Htmp; [ ..  tac Htmp ]), "spec_tac" (bound to
fun Htmp =>
...
...
theories/base_logic/lib/boxes.v
View file @
613c7a7d
...
...
@@ 271,7 +271,7 @@ Proof.
iExists
γ
1
,
γ
2
.
iIntros
"{$% $#} !>"
.
iSplit
;
last
iSplit
;
try
iPureIntro
.
{
by
eapply
lookup_insert_None
.
}
{
by
apply
(
lookup_insert_None
(
delete
γ
f
)
γ
1
γ
2
true
).
}
iNext
.
iApply
(
internal_eq_rewrite_contractive
_
_
(
λ
P
,
_
)
with
"[Heq] Hbox"
).
iNext
.
iApply
(
internal_eq_rewrite_contractive
_
_
(
box
_
_
)
with
"[Heq] Hbox"
).
iNext
.
iRewrite
"Heq"
.
iPureIntro
.
by
rewrite
assoc
(
comm
_
Q2
).

iMod
(
slice_delete_empty
with
"Hslice Hbox"
)
as
(
P'
)
"[Heq Hbox]"
;
try
done
.
iMod
(
slice_insert_empty
with
"Hbox"
)
as
(
γ
1
?)
"[#Hslice1 Hbox]"
.
...
...
@@ 279,7 +279,7 @@ Proof.
iExists
γ
1
,
γ
2
.
iIntros
"{$% $#} !>"
.
iSplit
;
last
iSplit
;
try
iPureIntro
.
{
by
eapply
lookup_insert_None
.
}
{
by
apply
(
lookup_insert_None
(
delete
γ
f
)
γ
1
γ
2
false
).
}
iNext
.
iApply
(
internal_eq_rewrite_contractive
_
_
(
λ
P
,
_
)
with
"[Heq] Hbox"
).
iNext
.
iApply
(
internal_eq_rewrite_contractive
_
_
(
box
_
_
)
with
"[Heq] Hbox"
).
iNext
.
iRewrite
"Heq"
.
iPureIntro
.
by
rewrite
assoc
(
comm
_
Q2
).
Qed
.
...
...
@@ 296,14 +296,14 @@ Proof.
iMod
(
slice_insert_full
_
_
_
_
(
Q1
∗
Q2
)%
I
with
"[$HQ1 $HQ2] Hbox"
)
as
(
γ
?)
"[#Hslice Hbox]"
;
first
done
.
iExists
γ
.
iIntros
"{$% $#} !>"
.
iNext
.
iApply
(
internal_eq_rewrite_contractive
_
_
(
λ
P
,
_
)
with
"[Heq1 Heq2] Hbox"
).
iApply
(
internal_eq_rewrite_contractive
_
_
(
box
_
_
)
with
"[Heq1 Heq2] Hbox"
).
iNext
.
iRewrite
"Heq1"
.
iRewrite
"Heq2"
.
by
rewrite
assoc
.

iMod
(
slice_delete_empty
with
"Hslice1 Hbox"
)
as
(
P1
)
"(Heq1 & Hbox)"
;
try
done
.
iMod
(
slice_delete_empty
with
"Hslice2 Hbox"
)
as
(
P2
)
"(Heq2 & Hbox)"
;
first
done
.
{
by
simplify_map_eq
.
}
iMod
(
slice_insert_empty
with
"Hbox"
)
as
(
γ
?)
"[#Hslice Hbox]"
.
iExists
γ
.
iIntros
"{$% $#} !>"
.
iNext
.
iApply
(
internal_eq_rewrite_contractive
_
_
(
λ
P
,
_
)
with
"[Heq1 Heq2] Hbox"
).
iApply
(
internal_eq_rewrite_contractive
_
_
(
box
_
_
)
with
"[Heq1 Heq2] Hbox"
).
iNext
.
iRewrite
"Heq1"
.
iRewrite
"Heq2"
.
by
rewrite
assoc
.
Qed
.
End
box
.
...
...
theories/base_logic/lib/saved_prop.v
View file @
613c7a7d
...
...
@@ 95,7 +95,8 @@ Proof. iApply saved_anything_alloc. Qed.
Lemma
saved_prop_agree
`
{!
savedPropG
Σ
}
γ
P
Q
:
saved_prop_own
γ
P

∗
saved_prop_own
γ
Q

∗
▷
(
P
≡
Q
).
Proof
.
iIntros
"HP HQ"
.
iApply
later_equivI
.
iApply
(
saved_anything_agree
with
"HP HQ"
).
iIntros
"HP HQ"
.
iApply
later_equivI
.
iApply
(
saved_anything_agree
(
F
:
=
▶
∙
)
with
"HP HQ"
).
Qed
.
(* Saved predicates. *)
...
...
@@ 129,6 +130,6 @@ Lemma saved_pred_agree `{!savedPredG Σ A} γ Φ Ψ x :
saved_pred_own
γ
Φ

∗
saved_pred_own
γ
Ψ

∗
▷
(
Φ
x
≡
Ψ
x
).
Proof
.
unfold
saved_pred_own
.
iIntros
"#HΦ #HΨ /="
.
iApply
later_equivI
.
iDestruct
(
saved_anything_agree
with
"HΦ HΨ"
)
as
"Heq"
.
iDestruct
(
saved_anything_agree
(
F
:
=
A

d
>
▶
∙
)
with
"HΦ HΨ"
)
as
"Heq"
.
by
iDestruct
(
discrete_fun_equivI
with
"Heq"
)
as
"?"
.
Qed
.
theories/bi/lib/fixpoint.v
View file @
613c7a7d
...
...
@@ 108,7 +108,7 @@ Section greatest.
F
(
bi_greatest_fixpoint
F
)
x
⊢
bi_greatest_fixpoint
F
x
.
Proof
.
iIntros
"HF"
.
iExists
(
OfeMor
(
F
(
bi_greatest_fixpoint
F
))).
iSplit
;
last
done
.
iIntros
"!#"
(
y
)
"Hy"
.
iApply
(
bi_mono_pred
with
"[#] Hy"
).
iSplit
;
last
done
.
iIntros
"!#"
(
y
)
"Hy
/=
"
.
iApply
(
bi_mono_pred
with
"[#] Hy"
).
iIntros
"!#"
(
z
)
"?"
.
by
iApply
greatest_fixpoint_unfold_1
.
Qed
.
...
...
theories/proofmode/coq_tactics.v
View file @
613c7a7d
...
...
@@ 452,8 +452,19 @@ Proof.
by
rewrite
(
entails_wand
P
)
//
intuitionistically_emp
emp_wand
.
Qed
.
Lemma
tac_pose_proof
Δ
j
P
Q
:
P
→
Definition
IntoEmpValid
(
φ
:
Type
)
(
P
:
PROP
)
:
=
φ
→
bi_emp_valid
P
.
Lemma
into_emp_valid_here
φ
P
:
AsEmpValid
φ
P
→
IntoEmpValid
φ
P
.
Proof
.
by
intros
[??].
Qed
.
Lemma
into_emp_valid_impl
(
φ
ψ
:
Type
)
P
:
φ
→
IntoEmpValid
ψ
P
→
IntoEmpValid
(
φ
→
ψ
)
P
.
Proof
.
rewrite
/
IntoEmpValid
;
auto
.
Qed
.
Lemma
into_emp_valid_forall
{
A
}
(
φ
:
A
→
Type
)
P
x
:
IntoEmpValid
(
φ
x
)
P
→
IntoEmpValid
(
∀
x
:
A
,
φ
x
)
P
.
Proof
.
rewrite
/
IntoEmpValid
;
auto
.
Qed
.
Lemma
tac_pose_proof
Δ
j
(
φ
:
Prop
)
P
Q
:
φ
→
IntoEmpValid
φ
P
→
match
envs_app
true
(
Esnoc
Enil
j
P
)
Δ
with

None
=>
False

Some
Δ
'
=>
envs_entails
Δ
'
Q
...
...
@@ 461,8 +472,8 @@ Lemma tac_pose_proof Δ j P Q :
envs_entails
Δ
Q
.
Proof
.
destruct
(
envs_app
_
_
_
)
as
[
Δ
'
]
eqn
:
?
;
last
done
.
rewrite
envs_entails_eq
=>
HP
?
.
rewrite
envs_app_singleton_sound
//=.
by
rewrite

HP
/=
intuitionistically_emp
emp_wand
.
rewrite
envs_entails_eq
=>
?
HP
<
.
rewrite
envs_app_singleton_sound
//=.
by
rewrite

HP
/
/
=
intuitionistically_emp
emp_wand
.
Qed
.
Lemma
tac_pose_proof_hyp
Δ
i
j
Q
:
...
...
theories/proofmode/ltac_tactics.v
View file @
613c7a7d
...
...
@@ 720,58 +720,9 @@ Notation "( H $! x1 .. xn 'with' pat )" :=
(
ITrm
H
(
hcons
x1
..
(
hcons
xn
hnil
)
..)
pat
)
(
at
level
0
,
x1
,
xn
at
level
9
).
Notation
"( H 'with' pat )"
:
=
(
ITrm
H
hnil
pat
)
(
at
level
0
).
(* The tactic [iIntoEmpValid] tactic solves a goal [bi_emp_valid ?Q]. The
argument [t] must be a Coq term whose type is of the following shape:
[∀ (x_1 : A_1) .. (x_n : A_n), φ]
for which we have an instance [AsEmpValid φ ?Q].
Examples of such [φ]s are
 [bi_emp_valid P], in which case [Q] is unified with [P].
 [P1 ⊢ P2], in which case [Q] is unified with [P1 ∗ P2].
 [P1 ⊣⊢ P2], in which case [Q] is unified with [P1 ↔ P2].
The tactic instantiates each dependent argument [x_i : A_i] with an evar and
generates a goal [A_i] for each nondependent argument [x_i : A_i].
For example, if the initial goal is [bi_emp_valid ?Q] and [t] has type
[∀ x, P x → R x], then it generates an evar [?x] for [x], a subgoal [P ?x],
and unifies [?Q] with [R x]. *)
Local
Ltac
iIntoEmpValid
t
:
=
let
go_specialize
t
tT
:
=
lazymatch
tT
with
(* We do not use hnf of tT, because, if
entailment is not opaque, then it would
unfold it. *)

?P
→
?Q
=>
let
H
:
=
fresh
in
assert
P
as
H
;
[
iIntoEmpValid
uconstr
:
(
t
H
)
;
clear
H
]

∀
_
:
?T
,
_
=>
(* Put [T] inside an [id] to avoid TC inference from being invoked. *)
(* This is a workarround for Coq bug #6583. *)
let
e
:
=
fresh
in
evar
(
e
:
id
T
)
;
let
e'
:
=
eval
unfold
e
in
e
in
clear
e
;
iIntoEmpValid
(
t
e'
)
end
in
(* We try two reduction tactics for the type of t before trying to
specialize it. We first try the head normal form in order to
unfold all the definition that could hide an entailment. Then,
we try the much weaker [eval cbv zeta], because entailment is
not necessarilly opaque, and could be unfolded by [hnf].
However, for calling type class search, we only use [cbv zeta]
in order to make sure we do not unfold [bi_emp_valid]. *)
let
tT
:
=
type
of
t
in
first
[
let
tT'
:
=
eval
hnf
in
tT
in
go_specialize
t
tT'

let
tT'
:
=
eval
cbv
zeta
in
tT
in
go_specialize
t
tT'

let
tT'
:
=
eval
cbv
zeta
in
tT
in
notypeclasses
refine
(
as_emp_valid_1
tT
_
_
)
;
[
iSolveTC

fail
1
"iPoseProof: not a BI assertion"

exact
t
]].
Tactic
Notation
"iPoseProofCoreHyp"
constr
(
H
)
"as"
constr
(
Hnew
)
:
=
let
Δ
:
=
iGetCtx
in
eapply
tac_pose_proof_hyp
with
H
Hnew
;
notypeclasses
refine
(
tac_pose_proof_hyp
_
H
Hnew
_
_
)
;
pm_reduce
;
lazymatch
goal
with


False
=>
...
...
@@ 787,10 +738,26 @@ Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=

_
=>
idtac
end
.
Tactic
Notation
"iPoseProofCoreLem"
constr
(
lem
)
"as"
tactic3
(
tac
)
:
=
Ltac
iIntoEmpValid_go
:
=
first
[
(* Case [φ → ψ] *)
notypeclasses
refine
(
into_emp_valid_impl
_
_
_
_
_
)
;
[
(*goal for [φ] *)

iIntoEmpValid_go
]

(* Case [∀ x : A, φ] *)
notypeclasses
refine
(
into_emp_valid_forall
_
_
_
_
)
;
iIntoEmpValid_go

(* Case [P ⊢ Q], [P ⊣⊢ Q], [bi_emp_valid P] *)
notypeclasses
refine
(
into_emp_valid_here
_
_
_
)].
(** Factor out the base case of the loop to avoid needless backtracking *)
Ltac
iIntoEmpValid
:
=
iIntoEmpValid_go
;
[..
(* goals for premises *)

iSolveTC

let
φ
:
=
lazymatch
goal
with

AsEmpValid
?
φ
_
=>
φ
end
in
fail
"iPoseProof:"
φ
"not a BI assertion"
].
Tactic
Notation
"iPoseProofCoreLem"
open_constr
(
lem
)
"as"
tactic3
(
tac
)
:
=
let
Hnew
:
=
iFresh
in
eapply
tac_pose_proof
with
Hnew
_;
(* (j:=H) *)
[
iIntoEmpValid
lem
notypeclasses
refine
(
tac_pose_proof
_
Hnew
_
_
_
lem
_
_
)
;
[
iIntoEmpValid

pm_reduce
;
lazymatch
goal
with


False
=>
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment