Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Rice Wine
Iris
Commits
f56551e7
Commit
f56551e7
authored
Jul 05, 2018
by
Robbert Krebbers
Browse files
More consistent names for modality actions.
parent
7265d257
Changes
2
Hide whitespace changes
Inline
Sidebyside
theories/proofmode/coq_tactics.v
View file @
f56551e7
...
...
@@ 1068,7 +1068,7 @@ Inputs:
Outputs:
 [Γout] : the resulting environment. *)
Inductive
IntoModalPersistentEnv
{
PROP2
}
:
∀
{
PROP1
}
(
M
:
modality
PROP1
PROP2
)
(
Γ
in
:
env
PROP2
)
(
Γ
out
:
env
PROP1
),
modality_
intro_spec
PROP1
PROP2
→
Prop
:
=
(
Γ
in
:
env
PROP2
)
(
Γ
out
:
env
PROP1
),
modality_
action
PROP1
PROP2
→
Prop
:
=

MIEnvIsEmpty_persistent
{
PROP1
}
(
M
:
modality
PROP1
PROP2
)
:
IntoModalPersistentEnv
M
Enil
Enil
MIEnvIsEmpty

MIEnvForall_persistent
(
M
:
modality
PROP2
PROP2
)
(
C
:
PROP2
→
Prop
)
Γ
:
...
...
@@ 1100,7 +1100,7 @@ Outputs:
 [Γout] : the resulting environment.
 [filtered] : a Boolean indicating if nonaffine hypotheses have been cleared. *)
Inductive
IntoModalSpatialEnv
{
PROP2
}
:
∀
{
PROP1
}
(
M
:
modality
PROP1
PROP2
)
(
Γ
in
:
env
PROP2
)
(
Γ
out
:
env
PROP1
),
modality_
intro_spec
PROP1
PROP2
→
bool
→
Prop
:
=
(
Γ
in
:
env
PROP2
)
(
Γ
out
:
env
PROP1
),
modality_
action
PROP1
PROP2
→
bool
→
Prop
:
=

MIEnvIsEmpty_spatial
{
PROP1
}
(
M
:
modality
PROP1
PROP2
)
:
IntoModalSpatialEnv
M
Enil
Enil
MIEnvIsEmpty
false

MIEnvForall_spatial
(
M
:
modality
PROP2
PROP2
)
(
C
:
PROP2
→
Prop
)
Γ
:
...
...
@@ 1183,8 +1183,8 @@ Section tac_modal_intro.
(** The actual introduction tactic *)
Lemma
tac_modal_intro
{
A
}
(
sel
:
A
)
Γ
p
Γ
s
n
Γ
p'
Γ
s'
Q
Q'
fi
:
FromModal
M
sel
Q'
Q
→
IntoModalPersistentEnv
M
Γ
p
Γ
p'
(
modality_intuitionistic_
spec
M
)
→
IntoModalSpatialEnv
M
Γ
s
Γ
s'
(
modality_spatial_
spec
M
)
fi
→
IntoModalPersistentEnv
M
Γ
p
Γ
p'
(
modality_intuitionistic_
action
M
)
→
IntoModalSpatialEnv
M
Γ
s
Γ
s'
(
modality_spatial_
action
M
)
fi
→
(
if
fi
then
Absorbing
Q'
else
TCTrue
)
→
envs_entails
(
Envs
Γ
p'
Γ
s'
n
)
Q
→
envs_entails
(
Envs
Γ
p
Γ
s
n
)
Q'
.
Proof
.
...
...
@@ 1199,7 +1199,7 @@ Section tac_modal_intro.
{
destruct
H
Γ
s
as
[
??????
[]
]
;
eauto
.
}
naive_solver
.
}
assert
(
□
[
∧
]
Γ
p
⊢
M
(
□
[
∧
]
Γ
p'
))%
I
as
HMp
.
{
remember
(
modality_intuitionistic_
spec
M
).
{
remember
(
modality_intuitionistic_
action
M
).
destruct
H
Γ
p
as
[?
M
C
Γ
p
?%
TCForall_Forall
?
M
C
Γ
p
Γ
p'
[]?
M
Γ
p

M
Γ
p
]
;
simpl
.

rewrite
{
1
}
intuitionistically_elim_emp
(
modality_emp
M
)
intuitionistically_True_emp
//.
...
...
@@ 1210,7 +1210,7 @@ Section tac_modal_intro.
intuitionistically_True_emp
.

eauto
using
modality_intuitionistic_id
.
}
move
:
HQ'
;
rewrite

HQ
pure_True
//
left_id
HMp
=>
HQ'
{
HQ
Hwf
HMp
}.
remember
(
modality_spatial_
spec
M
).
remember
(
modality_spatial_
action
M
).
destruct
H
Γ
s
as
[?
M
C
Γ
s
?%
TCForall_Forall
?
M
C
Γ
s
Γ
s'
fi
[]?
M
Γ
s

M
Γ
s
]
;
simpl
.

by
rewrite

HQ'
/=
!
right_id
.

rewrite

HQ'
{
1
}(
modality_spatial_forall_big_sep
_
_
Γ
s
)
//.
...
...
theories/proofmode/modalities.v
View file @
f56551e7
...
...
@@ 21,12 +21,12 @@ spatial context what action should be performed upon introducing the modality:
Formally, these actions correspond to the following inductive type: *)
Inductive
modality_
intro_spec
(
PROP1
:
bi
)
:
bi
→
Type
:
=

MIEnvIsEmpty
{
PROP2
:
bi
}
:
modality_
intro_spec
PROP1
PROP2

MIEnvForall
(
C
:
PROP1
→
Prop
)
:
modality_
intro_spec
PROP1
PROP1

MIEnvTransform
{
PROP2
:
bi
}
(
C
:
PROP2
→
PROP1
→
Prop
)
:
modality_
intro_spec
PROP1
PROP2

MIEnvClear
{
PROP2
}
:
modality_
intro_spec
PROP1
PROP2

MIEnvId
:
modality_
intro_spec
PROP1
PROP1
.
Inductive
modality_
action
(
PROP1
:
bi
)
:
bi
→
Type
:
=

MIEnvIsEmpty
{
PROP2
:
bi
}
:
modality_
action
PROP1
PROP2

MIEnvForall
(
C
:
PROP1
→
Prop
)
:
modality_
action
PROP1
PROP1

MIEnvTransform
{
PROP2
:
bi
}
(
C
:
PROP2
→
PROP1
→
Prop
)
:
modality_
action
PROP1
PROP2

MIEnvClear
{
PROP2
}
:
modality_
action
PROP1
PROP2

MIEnvId
:
modality_
action
PROP1
PROP1
.
Arguments
MIEnvIsEmpty
{
_
_
}.
Arguments
MIEnvForall
{
_
}
_
.
Arguments
MIEnvTransform
{
_
_
}
_
.
...
...
@@ 35,8 +35,8 @@ Arguments MIEnvId {_}.
Notation
MIEnvFilter
C
:
=
(
MIEnvTransform
(
TCDiag
C
)).
Definition
modality_int
ro_spec_intuitionisti
c
{
PROP1
PROP2
}
(
s
:
modality_
intro_spec
PROP1
PROP2
)
:
(
PROP1
→
PROP2
)
→
Prop
:
=
Definition
modality_int
uitionistic_action_spe
c
{
PROP1
PROP2
}
(
s
:
modality_
action
PROP1
PROP2
)
:
(
PROP1
→
PROP2
)
→
Prop
:
=
match
s
with

MIEnvIsEmpty
=>
λ
M
,
True

MIEnvForall
C
=>
λ
M
,
...
...
@@ 49,8 +49,8 @@ Definition modality_intro_spec_intuitionistic {PROP1 PROP2}

MIEnvId
=>
λ
M
,
∀
P
,
□
P
⊢
M
(
□
P
)
end
.
Definition
modality_
intro_spec_spatial
{
PROP1
PROP2
}
(
s
:
modality_
intro_spec
PROP1
PROP2
)
:
(
PROP1
→
PROP2
)
→
Prop
:
=
Definition
modality_
spatial_action_spec
{
PROP1
PROP2
}
(
s
:
modality_
action
PROP1
PROP2
)
:
(
PROP1
→
PROP2
)
→
Prop
:
=
match
s
with

MIEnvIsEmpty
=>
λ
M
,
True

MIEnvForall
C
=>
λ
M
,
∀
P
,
C
P
→
P
⊢
M
P
...
...
@@ 62,9 +62,9 @@ Definition modality_intro_spec_spatial {PROP1 PROP2}
(* A modality is then a record packing together the modality with the laws it
should satisfy to justify the given actions for both contexts: *)
Record
modality_mixin
{
PROP1
PROP2
:
bi
}
(
M
:
PROP1
→
PROP2
)
(
pspec
sspec
:
modality_
intro_spec
PROP1
PROP2
)
:
=
{
modality_mixin_intuitionistic
:
modality_int
ro_spec_intuitionistic
pspec
M
;
modality_mixin_spatial
:
modality_
intro_spec_spatial
sspec
M
;
(
iaction
saction
:
modality_
action
PROP1
PROP2
)
:
=
{
modality_mixin_intuitionistic
:
modality_int
uitionistic_action_spec
iaction
M
;
modality_mixin_spatial
:
modality_
spatial_action_spec
saction
M
;
modality_mixin_emp
:
emp
⊢
M
emp
;
modality_mixin_mono
P
Q
:
(
P
⊢
Q
)
→
M
P
⊢
M
Q
;
modality_mixin_sep
P
Q
:
M
P
∗
M
Q
⊢
M
(
P
∗
Q
)
...
...
@@ 72,29 +72,29 @@ Record modality_mixin {PROP1 PROP2 : bi} (M : PROP1 → PROP2)
Record
modality
(
PROP1
PROP2
:
bi
)
:
=
Modality
{
modality_car
:
>
PROP1
→
PROP2
;
modality_intuitionistic_
spec
:
modality_
intro_spec
PROP1
PROP2
;
modality_spatial_
spec
:
modality_
intro_spec
PROP1
PROP2
;
modality_intuitionistic_
action
:
modality_
action
PROP1
PROP2
;
modality_spatial_
action
:
modality_
action
PROP1
PROP2
;
modality_mixin_of
:
modality_mixin
modality_car
modality_intuitionistic_
spec
modality_spatial_
spec
modality_mixin
modality_car
modality_intuitionistic_
action
modality_spatial_
action
}.
Arguments
Modality
{
_
_
}
_
{
_
_
}
_
.
Arguments
modality_intuitionistic_
spec
{
_
_
}
_
.
Arguments
modality_spatial_
spec
{
_
_
}
_
.
Arguments
modality_intuitionistic_
action
{
_
_
}
_
.
Arguments
modality_spatial_
action
{
_
_
}
_
.
Section
modality
.
Context
{
PROP1
PROP2
}
(
M
:
modality
PROP1
PROP2
).
Lemma
modality_intuitionistic_transform
C
P
Q
:
modality_intuitionistic_
spec
M
=
MIEnvTransform
C
→
C
P
Q
→
□
P
⊢
M
(
□
Q
).
modality_intuitionistic_
action
M
=
MIEnvTransform
C
→
C
P
Q
→
□
P
⊢
M
(
□
Q
).
Proof
.
destruct
M
as
[???
[]]
;
naive_solver
.
Qed
.
Lemma
modality_and_transform
C
P
Q
:
modality_intuitionistic_
spec
M
=
MIEnvTransform
C
→
M
P
∧
M
Q
⊢
M
(
P
∧
Q
).
modality_intuitionistic_
action
M
=
MIEnvTransform
C
→
M
P
∧
M
Q
⊢
M
(
P
∧
Q
).
Proof
.
destruct
M
as
[???
[]]
;
naive_solver
.
Qed
.
Lemma
modality_spatial_transform
C
P
Q
:
modality_spatial_
spec
M
=
MIEnvTransform
C
→
C
P
Q
→
P
⊢
M
Q
.
modality_spatial_
action
M
=
MIEnvTransform
C
→
C
P
Q
→
P
⊢
M
Q
.
Proof
.
destruct
M
as
[???
[]]
;
naive_solver
.
Qed
.
Lemma
modality_spatial_clear
P
:
modality_spatial_
spec
M
=
MIEnvClear
→
Absorbing
(
M
P
).
modality_spatial_
action
M
=
MIEnvClear
→
Absorbing
(
M
P
).
Proof
.
destruct
M
as
[???
[]]
;
naive_solver
.
Qed
.
Lemma
modality_emp
:
emp
⊢
M
emp
.
...
...
@@ 115,23 +115,23 @@ Section modality1.
Context
{
PROP
}
(
M
:
modality
PROP
PROP
).
Lemma
modality_intuitionistic_forall
C
P
:
modality_intuitionistic_
spec
M
=
MIEnvForall
C
→
C
P
→
□
P
⊢
M
(
□
P
).
modality_intuitionistic_
action
M
=
MIEnvForall
C
→
C
P
→
□
P
⊢
M
(
□
P
).
Proof
.
destruct
M
as
[???
[]]
;
naive_solver
.
Qed
.
Lemma
modality_and_forall
C
P
Q
:
modality_intuitionistic_
spec
M
=
MIEnvForall
C
→
M
P
∧
M
Q
⊢
M
(
P
∧
Q
).
modality_intuitionistic_
action
M
=
MIEnvForall
C
→
M
P
∧
M
Q
⊢
M
(
P
∧
Q
).
Proof
.
destruct
M
as
[???
[]]
;
naive_solver
.
Qed
.
Lemma
modality_intuitionistic_id
P
:
modality_intuitionistic_
spec
M
=
MIEnvId
→
□
P
⊢
M
(
□
P
).
modality_intuitionistic_
action
M
=
MIEnvId
→
□
P
⊢
M
(
□
P
).
Proof
.
destruct
M
as
[???
[]]
;
naive_solver
.
Qed
.
Lemma
modality_spatial_forall
C
P
:
modality_spatial_
spec
M
=
MIEnvForall
C
→
C
P
→
P
⊢
M
P
.
modality_spatial_
action
M
=
MIEnvForall
C
→
C
P
→
P
⊢
M
P
.
Proof
.
destruct
M
as
[???
[]]
;
naive_solver
.
Qed
.
Lemma
modality_spatial_id
P
:
modality_spatial_
spec
M
=
MIEnvId
→
P
⊢
M
P
.
modality_spatial_
action
M
=
MIEnvId
→
P
⊢
M
P
.
Proof
.
destruct
M
as
[???
[]]
;
naive_solver
.
Qed
.
Lemma
modality_intuitionistic_forall_big_and
C
Ps
:
modality_intuitionistic_
spec
M
=
MIEnvForall
C
→
modality_intuitionistic_
action
M
=
MIEnvForall
C
→
Forall
C
Ps
→
□
[
∧
]
Ps
⊢
M
(
□
[
∧
]
Ps
).
Proof
.
induction
2
as
[
P
Ps
?
_
IH
]
;
simpl
.
...
...
@@ 140,7 +140,7 @@ Section modality1.
by
rewrite
{
1
}(
modality_intuitionistic_forall
_
P
).
Qed
.
Lemma
modality_spatial_forall_big_sep
C
Ps
:
modality_spatial_
spec
M
=
MIEnvForall
C
→
modality_spatial_
action
M
=
MIEnvForall
C
→
Forall
C
Ps
→
[
∗
]
Ps
⊢
M
([
∗
]
Ps
).
Proof
.
induction
2
as
[
P
Ps
?
_
IH
]
;
simpl
.
...
...
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