Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Iris
Commits
3012972e
Commit
3012972e
authored
Jul 15, 2020
by
Robbert Krebbers
1
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Bump std++ (pattern matching bind).
parent
07ff13e0
Pipeline
#31484
canceled with stage
in 16 minutes and 31 seconds
Changes
4
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
16 additions
and
16 deletions
+16
-16
opam
opam
+1
-1
theories/proofmode/coq_tactics.v
theories/proofmode/coq_tactics.v
+2
-2
theories/proofmode/environments.v
theories/proofmode/environments.v
+8
-8
theories/proofmode/intro_patterns.v
theories/proofmode/intro_patterns.v
+5
-5
No files found.
opam
View file @
3012972e
...
@@ -11,7 +11,7 @@ synopsis: "This is the Coq development of the Iris Project"
...
@@ -11,7 +11,7 @@ synopsis: "This is the Coq development of the Iris Project"
depends: [
depends: [
"coq" { (>= "8.9.1" & < "8.13~") | (= "dev") }
"coq" { (>= "8.9.1" & < "8.13~") | (= "dev") }
"coq-stdpp" { (= "dev.2020-07-
02
.1.
c8129a37
") | (= "dev") }
"coq-stdpp" { (= "dev.2020-07-
15
.1.
92dc4869
") | (= "dev") }
]
]
build: [make "-j%{jobs}%"]
build: [make "-j%{jobs}%"]
...
...
theories/proofmode/coq_tactics.v
View file @
3012972e
...
@@ -322,8 +322,8 @@ Lemma tac_specialize_assert Δ j (q am neg : bool) js R P1 P2 P1' Q :
...
@@ -322,8 +322,8 @@ Lemma tac_specialize_assert Δ j (q am neg : bool) js R P1 P2 P1' Q :
IntoWand
q
false
R
P1
P2
→
IntoWand
q
false
R
P1
P2
→
(
if
am
then
AddModal
P1'
P1
Q
else
TCEq
P1'
P1
)
→
(
if
am
then
AddModal
P1'
P1
Q
else
TCEq
P1'
P1
)
→
match
match
'
'
(
Δ
1
,
Δ
2
)
←
envs_split
(
if
neg
is
true
then
Right
else
Left
)
'
(
Δ
1
,
Δ
2
)
←
envs_split
(
if
neg
is
true
then
Right
else
Left
)
js
(
envs_delete
true
j
q
Δ
)
;
js
(
envs_delete
true
j
q
Δ
)
;
Δ
2
'
←
envs_app
(
negb
am
&&&
q
&&&
env_spatial_is_nil
Δ
1
)
(
Esnoc
Enil
j
P2
)
Δ
2
;
Δ
2
'
←
envs_app
(
negb
am
&&&
q
&&&
env_spatial_is_nil
Δ
1
)
(
Esnoc
Enil
j
P2
)
Δ
2
;
Some
(
Δ
1
,
Δ
2
'
)
(* does not preserve position of [j] *)
Some
(
Δ
1
,
Δ
2
'
)
(* does not preserve position of [j] *)
with
with
...
...
theories/proofmode/environments.v
View file @
3012972e
...
@@ -22,7 +22,7 @@ Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
...
@@ -22,7 +22,7 @@ Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
Module
env_notations
.
Module
env_notations
.
Notation
"y ≫= f"
:
=
(
pm_option_bind
f
y
).
Notation
"y ≫= f"
:
=
(
pm_option_bind
f
y
).
Notation
"x ← y ; z"
:
=
(
y
≫
=
λ
x
,
z
).
Notation
"x ← y ; z"
:
=
(
y
≫
=
λ
x
,
z
).
Notation
"' x1
.. xn
← y ; z"
:
=
(
y
≫
=
(
λ
x1
,
..
(
λ
xn
,
z
)
..
)).
Notation
"' x1 ← y ; z"
:
=
(
y
≫
=
(
λ
x1
,
z
)).
Notation
"Γ !! j"
:
=
(
env_lookup
j
Γ
).
Notation
"Γ !! j"
:
=
(
env_lookup
j
Γ
).
End
env_notations
.
End
env_notations
.
Import
env_notations
.
Import
env_notations
.
...
@@ -71,7 +71,7 @@ Fixpoint env_lookup_delete {A} (i : ident) (Γ : env A) : option (A * env A) :=
...
@@ -71,7 +71,7 @@ Fixpoint env_lookup_delete {A} (i : ident) (Γ : env A) : option (A * env A) :=
|
Enil
=>
None
|
Enil
=>
None
|
Esnoc
Γ
j
x
=>
|
Esnoc
Γ
j
x
=>
if
ident_beq
i
j
then
Some
(
x
,
Γ
)
if
ident_beq
i
j
then
Some
(
x
,
Γ
)
else
'
'
(
y
,
Γ
'
)
←
env_lookup_delete
i
Γ
;
Some
(
y
,
Esnoc
Γ
'
j
x
)
else
'
(
y
,
Γ
'
)
←
env_lookup_delete
i
Γ
;
Some
(
y
,
Esnoc
Γ
'
j
x
)
end
.
end
.
Inductive
env_Forall2
{
A
B
}
(
P
:
A
→
B
→
Prop
)
:
env
A
→
env
B
→
Prop
:
=
Inductive
env_Forall2
{
A
B
}
(
P
:
A
→
B
→
Prop
)
:
env
A
→
env
B
→
Prop
:
=
...
@@ -296,7 +296,7 @@ Definition envs_lookup_delete {PROP} (remove_intuitionistic : bool)
...
@@ -296,7 +296,7 @@ Definition envs_lookup_delete {PROP} (remove_intuitionistic : bool)
let
(
Γ
p
,
Γ
s
,
n
)
:
=
Δ
in
let
(
Γ
p
,
Γ
s
,
n
)
:
=
Δ
in
match
env_lookup_delete
i
Γ
p
with
match
env_lookup_delete
i
Γ
p
with
|
Some
(
P
,
Γ
p'
)
=>
Some
(
true
,
P
,
Envs
(
if
remove_intuitionistic
then
Γ
p'
else
Γ
p
)
Γ
s
n
)
|
Some
(
P
,
Γ
p'
)
=>
Some
(
true
,
P
,
Envs
(
if
remove_intuitionistic
then
Γ
p'
else
Γ
p
)
Γ
s
n
)
|
None
=>
'
'
(
P
,
Γ
s'
)
←
env_lookup_delete
i
Γ
s
;
Some
(
false
,
P
,
Envs
Γ
p
Γ
s'
n
)
|
None
=>
'
(
P
,
Γ
s'
)
←
env_lookup_delete
i
Γ
s
;
Some
(
false
,
P
,
Envs
Γ
p
Γ
s'
n
)
end
.
end
.
Fixpoint
envs_lookup_delete_list
{
PROP
}
(
remove_intuitionistic
:
bool
)
Fixpoint
envs_lookup_delete_list
{
PROP
}
(
remove_intuitionistic
:
bool
)
...
@@ -304,8 +304,8 @@ Fixpoint envs_lookup_delete_list {PROP} (remove_intuitionistic : bool)
...
@@ -304,8 +304,8 @@ Fixpoint envs_lookup_delete_list {PROP} (remove_intuitionistic : bool)
match
js
with
match
js
with
|
[]
=>
Some
(
true
,
[],
Δ
)
|
[]
=>
Some
(
true
,
[],
Δ
)
|
j
::
js
=>
|
j
::
js
=>
'
'
(
p
,
P
,
Δ
'
)
←
envs_lookup_delete
remove_intuitionistic
j
Δ
;
'
(
p
,
P
,
Δ
'
)
←
envs_lookup_delete
remove_intuitionistic
j
Δ
;
'
'
(
q
,
Ps
,
Δ
''
)
←
envs_lookup_delete_list
remove_intuitionistic
js
Δ
'
;
'
(
q
,
Ps
,
Δ
''
)
←
envs_lookup_delete_list
remove_intuitionistic
js
Δ
'
;
Some
((
p
:
bool
)
&&&
q
,
P
::
Ps
,
Δ
''
)
Some
((
p
:
bool
)
&&&
q
,
P
::
Ps
,
Δ
''
)
end
.
end
.
...
@@ -352,7 +352,7 @@ Fixpoint envs_split_go {PROP}
...
@@ -352,7 +352,7 @@ Fixpoint envs_split_go {PROP}
match
js
with
match
js
with
|
[]
=>
Some
(
Δ
1
,
Δ
2
)
|
[]
=>
Some
(
Δ
1
,
Δ
2
)
|
j
::
js
=>
|
j
::
js
=>
'
'
(
p
,
P
,
Δ
1
'
)
←
envs_lookup_delete
true
j
Δ
1
;
'
(
p
,
P
,
Δ
1
'
)
←
envs_lookup_delete
true
j
Δ
1
;
if
p
:
bool
then
envs_split_go
js
Δ
1
Δ
2
else
if
p
:
bool
then
envs_split_go
js
Δ
1
Δ
2
else
envs_split_go
js
Δ
1
'
(
envs_snoc
Δ
2
false
j
P
)
envs_split_go
js
Δ
1
'
(
envs_snoc
Δ
2
false
j
P
)
end
.
end
.
...
@@ -360,7 +360,7 @@ Fixpoint envs_split_go {PROP}
...
@@ -360,7 +360,7 @@ Fixpoint envs_split_go {PROP}
if [d = Left] then [result = (hyps named js, remaining hyps)] *)
if [d = Left] then [result = (hyps named js, remaining hyps)] *)
Definition
envs_split
{
PROP
}
(
d
:
direction
)
Definition
envs_split
{
PROP
}
(
d
:
direction
)
(
js
:
list
ident
)
(
Δ
:
envs
PROP
)
:
option
(
envs
PROP
*
envs
PROP
)
:
=
(
js
:
list
ident
)
(
Δ
:
envs
PROP
)
:
option
(
envs
PROP
*
envs
PROP
)
:
=
'
'
(
Δ
1
,
Δ
2
)
←
envs_split_go
js
Δ
(
envs_clear_spatial
Δ
)
;
'
(
Δ
1
,
Δ
2
)
←
envs_split_go
js
Δ
(
envs_clear_spatial
Δ
)
;
if
d
is
Right
then
Some
(
Δ
1
,
Δ
2
)
else
Some
(
Δ
2
,
Δ
1
).
if
d
is
Right
then
Some
(
Δ
1
,
Δ
2
)
else
Some
(
Δ
2
,
Δ
1
).
Fixpoint
env_to_prop_go
{
PROP
:
bi
}
(
acc
:
PROP
)
(
Γ
:
env
PROP
)
:
PROP
:
=
Fixpoint
env_to_prop_go
{
PROP
:
bi
}
(
acc
:
PROP
)
(
Γ
:
env
PROP
)
:
PROP
:
=
...
@@ -688,7 +688,7 @@ Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Q
...
@@ -688,7 +688,7 @@ Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Q
Lemma
envs_lookup_envs_clear_spatial
Δ
j
:
Lemma
envs_lookup_envs_clear_spatial
Δ
j
:
envs_lookup
j
(
envs_clear_spatial
Δ
)
envs_lookup
j
(
envs_clear_spatial
Δ
)
=
'
'
(
p
,
P
)
←
envs_lookup
j
Δ
;
if
p
:
bool
then
Some
(
p
,
P
)
else
None
.
=
'
(
p
,
P
)
←
envs_lookup
j
Δ
;
if
p
:
bool
then
Some
(
p
,
P
)
else
None
.
Proof
.
Proof
.
rewrite
/
envs_lookup
/
envs_clear_spatial
.
rewrite
/
envs_lookup
/
envs_clear_spatial
.
destruct
Δ
as
[
Γ
p
Γ
s
]
;
simpl
;
destruct
(
Γ
p
!!
j
)
eqn
:
?
;
simplify_eq
/=
;
auto
.
destruct
Δ
as
[
Γ
p
Γ
s
]
;
simpl
;
destruct
(
Γ
p
!!
j
)
eqn
:
?
;
simplify_eq
/=
;
auto
.
...
...
theories/proofmode/intro_patterns.v
View file @
3012972e
...
@@ -44,9 +44,9 @@ Fixpoint close_list (k : stack)
...
@@ -44,9 +44,9 @@ Fixpoint close_list (k : stack)
|
StList
::
k
=>
Some
(
StPat
(
IList
(
ps
::
pss
))
::
k
)
|
StList
::
k
=>
Some
(
StPat
(
IList
(
ps
::
pss
))
::
k
)
|
StPat
pat
::
k
=>
close_list
k
(
pat
::
ps
)
pss
|
StPat
pat
::
k
=>
close_list
k
(
pat
::
ps
)
pss
|
StIntuitionistic
::
k
=>
|
StIntuitionistic
::
k
=>
'
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close_list
k
(
IIntuitionistic
p
::
ps
)
pss
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close_list
k
(
IIntuitionistic
p
::
ps
)
pss
|
StModalElim
::
k
=>
|
StModalElim
::
k
=>
'
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close_list
k
(
IModalElim
p
::
ps
)
pss
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close_list
k
(
IModalElim
p
::
ps
)
pss
|
StBar
::
k
=>
close_list
k
[]
(
ps
::
pss
)
|
StBar
::
k
=>
close_list
k
[]
(
ps
::
pss
)
|
_
=>
None
|
_
=>
None
end
.
end
.
...
@@ -121,9 +121,9 @@ Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
...
@@ -121,9 +121,9 @@ Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
match
k
with
match
k
with
|
[]
=>
Some
ps
|
[]
=>
Some
ps
|
StPat
pat
::
k
=>
close
k
(
pat
::
ps
)
|
StPat
pat
::
k
=>
close
k
(
pat
::
ps
)
|
StIntuitionistic
::
k
=>
'
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close
k
(
IIntuitionistic
p
::
ps
)
|
StIntuitionistic
::
k
=>
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close
k
(
IIntuitionistic
p
::
ps
)
|
StSpatial
::
k
=>
'
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close
k
(
ISpatial
p
::
ps
)
|
StSpatial
::
k
=>
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close
k
(
ISpatial
p
::
ps
)
|
StModalElim
::
k
=>
'
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close
k
(
IModalElim
p
::
ps
)
|
StModalElim
::
k
=>
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close
k
(
IModalElim
p
::
ps
)
|
_
=>
None
|
_
=>
None
end
.
end
.
...
...
Robbert Krebbers
@robbertkrebbers
mentioned in merge request
stdpp!169 (merged)
·
Jul 15, 2020
mentioned in merge request
stdpp!169 (merged)
mentioned in merge request stdpp!169
Toggle commit list
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