Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Joshua Yanovski
iris-coq
Commits
3d46bb4d
Commit
3d46bb4d
authored
Jan 22, 2017
by
Robbert Krebbers
Browse files
Declare [Hint Mode] instances for proof mode.
This fixes issue #62.
parent
e2b1c91c
Changes
5
Hide whitespace changes
Inline
Side-by-side
theories/base_logic/lib/fancy_updates.v
View file @
3d46bb4d
...
...
@@ -155,8 +155,10 @@ Section proofmode_classes.
Proof
.
rewrite
/
FromAssumption
=>->
.
apply
bupd_fupd
.
Qed
.
Global
Instance
into_wand_fupd
E1
E2
R
P
Q
:
IntoWand
R
P
Q
→
IntoWand
R
(
|={
E1
,
E2
}=>
P
)
(
|={
E1
,
E2
}=>
Q
)
|
100.
Proof
.
rewrite
/
IntoWand
=>->
.
apply
wand_intro_l
.
by
rewrite
fupd_wand_r
.
Qed
.
IntoWand
R
P
Q
→
IntoWand
'
R
(
|={
E1
,
E2
}=>
P
)
(
|={
E1
,
E2
}=>
Q
)
|
100.
Proof
.
rewrite
/
IntoWand
'
/
IntoWand
=>->
.
apply
wand_intro_l
.
by
rewrite
fupd_wand_r
.
Qed
.
Global
Instance
from_sep_fupd
E
P
Q1
Q2
:
FromSep
P
Q1
Q2
→
FromSep
(
|={
E
}=>
P
)
(
|={
E
}=>
Q1
)
(
|={
E
}=>
Q2
).
...
...
@@ -179,8 +181,8 @@ Section proofmode_classes.
Global
Instance
is_except_0_fupd
E1
E2
P
:
IsExcept0
(
|={
E1
,
E2
}=>
P
).
Proof
.
by
rewrite
/
IsExcept0
except_0_fupd
.
Qed
.
Global
Instance
into
_modal_fupd
E
P
:
Into
Modal
P
(
|={
E
}=>
P
).
Proof
.
rewrite
/
Into
Modal
.
apply
fupd_intro
.
Qed
.
Global
Instance
from
_modal_fupd
E
P
:
From
Modal
(
|={
E
}=>
P
)
P
.
Proof
.
rewrite
/
From
Modal
.
apply
fupd_intro
.
Qed
.
(
*
Put
a
lower
priority
compared
to
[
elim_modal_fupd_fupd
],
so
that
it
is
not
taken
when
the
first
parameter
is
not
specified
(
in
...
...
theories/proofmode/class_instances.v
View file @
3d46bb4d
...
...
@@ -219,15 +219,22 @@ Proof. apply and_elim_r', impl_wand. Qed.
Global
Instance
into_wand_always
R
P
Q
:
IntoWand
R
P
Q
→
IntoWand
(
□
R
)
P
Q
.
Proof
.
rewrite
/
IntoWand
=>
->
.
apply
always_elim
.
Qed
.
Global
Instance
into_wand_later
(
R1
R2
P
Q
:
uPred
M
)
:
IntoLaterN
1
R1
R2
→
IntoWand
R2
P
Q
→
IntoWand
R1
(
▷
P
)
(
▷
Q
)
|
99.
Proof
.
rewrite
/
IntoLaterN
/
IntoWand
=>
->
->
.
by
rewrite
-
later_wand
.
Qed
.
IntoLaterN
1
R1
R2
→
IntoWand
R2
P
Q
→
IntoWand
'
R1
(
▷
P
)
(
▷
Q
)
|
99.
Proof
.
rewrite
/
IntoLaterN
/
IntoWand
'
/
IntoWand
=>
->
->
.
by
rewrite
-
later_wand
.
Qed
.
Global
Instance
into_wand_laterN
n
(
R1
R2
P
Q
:
uPred
M
)
:
IntoLaterN
n
R1
R2
→
IntoWand
R2
P
Q
→
IntoWand
R1
(
▷
^
n
P
)
(
▷
^
n
Q
)
|
100.
Proof
.
rewrite
/
IntoLaterN
/
IntoWand
=>
->
->
.
by
rewrite
-
laterN_wand
.
Qed
.
IntoLaterN
n
R1
R2
→
IntoWand
R2
P
Q
→
IntoWand
'
R1
(
▷
^
n
P
)
(
▷
^
n
Q
)
|
100.
Proof
.
rewrite
/
IntoLaterN
/
IntoWand
'
/
IntoWand
=>
->
->
.
by
rewrite
-
laterN_wand
.
Qed
.
Global
Instance
into_wand_bupd
R
P
Q
:
IntoWand
R
P
Q
→
IntoWand
R
(
|==>
P
)
(
|==>
Q
)
|
98.
Proof
.
rewrite
/
IntoWand
=>->
.
apply
wand_intro_l
.
by
rewrite
bupd_wand_r
.
Qed
.
IntoWand
R
P
Q
→
IntoWand
'
R
(
|==>
P
)
(
|==>
Q
)
|
98.
Proof
.
rewrite
/
IntoWand
'
/
IntoWand
=>
->
.
apply
wand_intro_l
.
by
rewrite
bupd_wand_r
.
Qed
.
(
*
FromAnd
*
)
Global
Instance
from_and_and
P1
P2
:
FromAnd
(
P1
∧
P2
)
P1
P2
.
...
...
@@ -564,12 +571,12 @@ Global Instance into_exist_laterN {A} n P (Φ : A → uPred M) :
IntoExist
P
Φ
→
Inhabited
A
→
IntoExist
(
▷
^
n
P
)
(
λ
a
,
▷
^
n
(
Φ
a
))
%
I
.
Proof
.
rewrite
/
IntoExist
=>
HP
?
.
by
rewrite
HP
laterN_exist
.
Qed
.
(
*
Into
Modal
*
)
Global
Instance
into
_modal_later
P
:
Into
Modal
P
(
▷
P
).
(
*
From
Modal
*
)
Global
Instance
from
_modal_later
P
:
From
Modal
(
▷
P
)
P
.
Proof
.
apply
later_intro
.
Qed
.
Global
Instance
into
_modal_bupd
P
:
Into
Modal
P
(
|==>
P
).
Global
Instance
from
_modal_bupd
P
:
From
Modal
(
|==>
P
)
P
.
Proof
.
apply
bupd_intro
.
Qed
.
Global
Instance
into
_modal_except_0
P
:
Into
Modal
P
(
◇
P
).
Global
Instance
from
_modal_except_0
P
:
From
Modal
(
◇
P
)
P
.
Proof
.
apply
except_0_intro
.
Qed
.
(
*
ElimModal
*
)
...
...
theories/proofmode/classes.v
View file @
3d46bb4d
...
...
@@ -2,77 +2,102 @@ From iris.base_logic Require Export base_logic.
Set
Default
Proof
Using
"Type"
.
Import
uPred
.
Section
classes
.
Context
{
M
:
ucmraT
}
.
Implicit
Types
P
Q
:
uPred
M
.
Class
FromAssumption
(
p
:
bool
)
(
P
Q
:
uPred
M
)
:=
from_assumption
:
□
?
p
P
⊢
Q
.
Global
Arguments
from_assumption
_
_
_
{
_
}
.
Class
IntoPure
(
P
:
uPred
M
)
(
φ
:
Prop
)
:=
into_pure
:
P
⊢
⌜φ⌝
.
Global
Arguments
into_pure
:
clear
implicits
.
Class
FromPure
(
P
:
uPred
M
)
(
φ
:
Prop
)
:=
from_pure
:
⌜φ⌝
⊢
P
.
Global
Arguments
from_pure
:
clear
implicits
.
Class
IntoPersistentP
(
P
Q
:
uPred
M
)
:=
into_persistentP
:
P
⊢
□
Q
.
Global
Arguments
into_persistentP
:
clear
implicits
.
Class
IntoLaterN
(
n
:
nat
)
(
P
Q
:
uPred
M
)
:=
into_laterN
:
P
⊢
▷
^
n
Q
.
Global
Arguments
into_laterN
_
_
_
{
_
}
.
Class
FromLaterN
(
n
:
nat
)
(
P
Q
:
uPred
M
)
:=
from_laterN
:
▷
^
n
Q
⊢
P
.
Global
Arguments
from_laterN
_
_
_
{
_
}
.
Class
IntoWand
(
R
P
Q
:
uPred
M
)
:=
into_wand
:
R
⊢
P
-
∗
Q
.
Global
Arguments
into_wand
:
clear
implicits
.
Class
FromAnd
(
P
Q1
Q2
:
uPred
M
)
:=
from_and
:
Q1
∧
Q2
⊢
P
.
Global
Arguments
from_and
:
clear
implicits
.
Class
FromSep
(
P
Q1
Q2
:
uPred
M
)
:=
from_sep
:
Q1
∗
Q2
⊢
P
.
Global
Arguments
from_sep
:
clear
implicits
.
Class
IntoAnd
(
p
:
bool
)
(
P
Q1
Q2
:
uPred
M
)
:=
Class
FromAssumption
{
M
}
(
p
:
bool
)
(
P
Q
:
uPred
M
)
:=
from_assumption
:
□
?
p
P
⊢
Q
.
Arguments
from_assumption
{
_
}
_
_
_
{
_
}
.
Hint
Mode
FromAssumption
+
+
!
-
:
typeclass_instances
.
Class
IntoPure
{
M
}
(
P
:
uPred
M
)
(
φ
:
Prop
)
:=
into_pure
:
P
⊢
⌜φ⌝
.
Arguments
into_pure
{
_
}
_
_
{
_
}
.
Hint
Mode
IntoPure
+
!
-
:
typeclass_instances
.
Class
FromPure
{
M
}
(
P
:
uPred
M
)
(
φ
:
Prop
)
:=
from_pure
:
⌜φ⌝
⊢
P
.
Arguments
from_pure
{
_
}
_
_
{
_
}
.
Hint
Mode
FromPure
+
!
-
:
typeclass_instances
.
Class
IntoPersistentP
{
M
}
(
P
Q
:
uPred
M
)
:=
into_persistentP
:
P
⊢
□
Q
.
Arguments
into_persistentP
{
_
}
_
_
{
_
}
.
Hint
Mode
IntoPersistentP
+
!
-
:
typeclass_instances
.
Class
IntoLaterN
{
M
}
(
n
:
nat
)
(
P
Q
:
uPred
M
)
:=
into_laterN
:
P
⊢
▷
^
n
Q
.
Arguments
into_laterN
{
_
}
_
_
_
{
_
}
.
Hint
Mode
IntoLaterN
+
-
!
-
:
typeclass_instances
.
Class
FromLaterN
{
M
}
(
n
:
nat
)
(
P
Q
:
uPred
M
)
:=
from_laterN
:
▷
^
n
Q
⊢
P
.
Arguments
from_laterN
{
_
}
_
_
_
{
_
}
.
Hint
Mode
FromLaterN
+
-
!
-
:
typeclass_instances
.
Class
IntoWand
{
M
}
(
R
P
Q
:
uPred
M
)
:=
into_wand
:
R
⊢
P
-
∗
Q
.
Arguments
into_wand
{
_
}
_
_
_
{
_
}
.
Hint
Mode
IntoWand
+
!
-
-
:
typeclass_instances
.
Class
IntoWand
'
{
M
}
(
R
P
Q
:
uPred
M
)
:=
into_wand
'
:>
IntoWand
R
P
Q
.
Arguments
into_wand
'
{
_
}
_
_
_
{
_
}
.
Hint
Mode
IntoWand
'
+
!
!
-
:
typeclass_instances
.
Hint
Mode
IntoWand
'
+
!
-
!
:
typeclass_instances
.
Class
FromAnd
{
M
}
(
P
Q1
Q2
:
uPred
M
)
:=
from_and
:
Q1
∧
Q2
⊢
P
.
Arguments
from_and
{
_
}
_
_
_
{
_
}
.
Hint
Mode
FromAnd
+
!
-
-
:
typeclass_instances
.
Class
FromSep
{
M
}
(
P
Q1
Q2
:
uPred
M
)
:=
from_sep
:
Q1
∗
Q2
⊢
P
.
Arguments
from_sep
{
_
}
_
_
_
{
_
}
.
Hint
Mode
FromSep
+
!
-
-
:
typeclass_instances
.
Hint
Mode
FromSep
+
-
!
!
:
typeclass_instances
.
(
*
For
iCombine
*
)
Class
IntoAnd
{
M
}
(
p
:
bool
)
(
P
Q1
Q2
:
uPred
M
)
:=
into_and
:
P
⊢
if
p
then
Q1
∧
Q2
else
Q1
∗
Q2
.
Global
Arguments
into_and
:
clear
implicits
.
Lemma
mk_into_and_sep
p
P
Q1
Q2
:
(
P
⊢
Q1
∗
Q2
)
→
IntoAnd
p
P
Q1
Q2
.
Arguments
into_and
{
_
}
_
_
_
_
{
_
}
.
Hint
Mode
IntoAnd
+
+
!
-
-
:
typeclass_instances
.
Lemma
mk_into_and_sep
{
M
}
p
(
P
Q1
Q2
:
uPred
M
)
:
(
P
⊢
Q1
∗
Q2
)
→
IntoAnd
p
P
Q1
Q2
.
Proof
.
rewrite
/
IntoAnd
=>->
.
destruct
p
;
auto
using
sep_and
.
Qed
.
Class
FromOp
{
A
:
cmraT
}
(
a
b1
b2
:
A
)
:=
from_op
:
b1
⋅
b2
≡
a
.
Global
Arguments
from_op
{
_
}
_
_
_
{
_
}
.
Arguments
from_op
{
_
}
_
_
_
{
_
}
.
Hint
Mode
FromOp
+
!
-
-
:
typeclass_instances
.
Hint
Mode
FromOp
+
-
!
!
:
typeclass_instances
.
(
*
For
iCombine
*
)
Class
IntoOp
{
A
:
cmraT
}
(
a
b1
b2
:
A
)
:=
into_op
:
a
≡
b1
⋅
b2
.
Global
Arguments
into_op
{
_
}
_
_
_
{
_
}
.
Arguments
into_op
{
_
}
_
_
_
{
_
}
.
(
*
No
[
Hint
Mode
]
since
we
want
to
turn
[
?
x
]
into
[
?
x1
⋅
?
x2
],
for
example
when
having
[
H
:
own
?
x
].
*
)
Class
Frame
(
R
P
Q
:
uPred
M
)
:=
frame
:
R
∗
Q
⊢
P
.
Global
Arguments
frame
:
clear
implicits
.
Class
Frame
{
M
}
(
R
P
Q
:
uPred
M
)
:=
frame
:
R
∗
Q
⊢
P
.
Arguments
frame
{
_
}
_
_
_
{
_
}
.
Hint
Mode
Frame
+
!
!
-
:
typeclass_instances
.
Class
FromOr
(
P
Q1
Q2
:
uPred
M
)
:=
from_or
:
Q1
∨
Q2
⊢
P
.
Global
Arguments
from_or
:
clear
implicits
.
Class
FromOr
{
M
}
(
P
Q1
Q2
:
uPred
M
)
:=
from_or
:
Q1
∨
Q2
⊢
P
.
Arguments
from_or
{
_
}
_
_
_
{
_
}
.
Hint
Mode
FromOr
+
!
-
-
:
typeclass_instances
.
Class
IntoOr
P
Q1
Q2
:=
into_or
:
P
⊢
Q1
∨
Q2
.
Global
Arguments
into_or
:
clear
implicits
.
Class
IntoOr
{
M
}
(
P
Q1
Q2
:
uPred
M
)
:=
into_or
:
P
⊢
Q1
∨
Q2
.
Arguments
into_or
{
_
}
_
_
_
{
_
}
.
Hint
Mode
IntoOr
+
!
-
-
:
typeclass_instances
.
Class
FromExist
{
A
}
(
P
:
uPred
M
)
(
Φ
:
A
→
uPred
M
)
:=
Class
FromExist
{
M
A
}
(
P
:
uPred
M
)
(
Φ
:
A
→
uPred
M
)
:=
from_exist
:
(
∃
x
,
Φ
x
)
⊢
P
.
Global
Arguments
from_exist
{
_
}
_
_
{
_
}
.
Arguments
from_exist
{
_
_
}
_
_
{
_
}
.
Hint
Mode
FromExist
+
-
!
-
:
typeclass_instances
.
Class
IntoExist
{
A
}
(
P
:
uPred
M
)
(
Φ
:
A
→
uPred
M
)
:=
Class
IntoExist
{
M
A
}
(
P
:
uPred
M
)
(
Φ
:
A
→
uPred
M
)
:=
into_exist
:
P
⊢
∃
x
,
Φ
x
.
Global
Arguments
into_exist
{
_
}
_
_
{
_
}
.
Arguments
into_exist
{
_
_
}
_
_
{
_
}
.
Hint
Mode
IntoExist
+
-
!
-
:
typeclass_instances
.
Class
IntoModal
(
P
Q
:
uPred
M
)
:=
into_modal
:
P
⊢
Q
.
Global
Arguments
into_modal
:
clear
implicits
.
Class
FromModal
{
M
}
(
P
Q
:
uPred
M
)
:=
from_modal
:
Q
⊢
P
.
Arguments
from_modal
{
_
}
_
_
{
_
}
.
Hint
Mode
FromModal
+
!
-
:
typeclass_instances
.
Class
ElimModal
(
P
P
'
:
uPred
M
)
(
Q
Q
'
:
uPred
M
)
:=
Class
ElimModal
{
M
}
(
P
P
'
:
uPred
M
)
(
Q
Q
'
:
uPred
M
)
:=
elim_modal
:
P
∗
(
P
'
-
∗
Q
'
)
⊢
Q
.
Global
Arguments
elim_modal
_
_
_
_
{
_
}
.
Arguments
elim_modal
{
_
}
_
_
_
_
{
_
}
.
Hint
Mode
ElimModal
+
!
-
!
-
:
typeclass_instances
.
Hint
Mode
ElimModal
+
-
!
-
!
:
typeclass_instances
.
Lemma
elim_modal_dummy
P
Q
:
ElimModal
P
P
Q
Q
.
Lemma
elim_modal_dummy
{
M
}
(
P
Q
:
uPred
M
)
:
ElimModal
P
P
Q
Q
.
Proof
.
by
rewrite
/
ElimModal
wand_elim_r
.
Qed
.
Class
IsExcept0
(
Q
:
uPred
M
)
:=
is_except_0
:
◇
Q
⊢
Q
.
Global
Arguments
is_except_0
:
clear
implicits
.
End
class
es
.
Class
IsExcept0
{
M
}
(
Q
:
uPred
M
)
:=
is_except_0
:
◇
Q
⊢
Q
.
Arguments
is_except_0
{
_
}
_
{
_
}
.
Hint
Mode
IsExcept0
+
!
:
typeclass_instanc
es
.
theories/proofmode/coq_tactics.v
View file @
3d46bb4d
...
...
@@ -832,8 +832,8 @@ Proof.
Qed
.
(
**
*
Modalities
*
)
Lemma
tac_modal_intro
Δ
P
Q
:
Into
Modal
Q
P
→
(
Δ
⊢
Q
)
→
Δ
⊢
P
.
Proof
.
rewrite
/
Into
Modal
.
by
intros
<-
->
.
Qed
.
Lemma
tac_modal_intro
Δ
P
Q
:
From
Modal
P
Q
→
(
Δ
⊢
Q
)
→
Δ
⊢
P
.
Proof
.
rewrite
/
From
Modal
.
by
intros
<-
->
.
Qed
.
Lemma
tac_modal_elim
Δ
Δ'
i
p
P
'
P
Q
Q
'
:
envs_lookup
i
Δ
=
Some
(
p
,
P
)
→
...
...
@@ -845,3 +845,5 @@ Proof.
rewrite
right_id
H
Δ
always_if_elim
.
by
apply
elim_modal
.
Qed
.
End
tactics
.
Hint
Mode
ForallSpecialize
+
-
-
!
-
:
typeclass_instances
.
theories/proofmode/tactics.v
View file @
3d46bb4d
...
...
@@ -642,7 +642,7 @@ Tactic Notation "iNext":= iNext _.
Tactic
Notation
"iModIntro"
:=
iStartProof
;
eapply
tac_modal_intro
;
[
let
P
:=
match
goal
with
|-
Into
Modal
_
?
P
=>
P
end
in
[
let
P
:=
match
goal
with
|-
From
Modal
?
P
_
=>
P
end
in
apply
_
||
fail
"iModIntro:"
P
"not a modality"
|
].
Tactic
Notation
"iModCore"
constr
(
H
)
:=
...
...
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