Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Jonas Kastberg
iris
Commits
84fe6493
Commit
84fe6493
authored
Nov 22, 2017
by
Robbert Krebbers
Browse files
Bump stdpp.
parent
672d60be
Changes
4
Hide whitespace changes
Inline
Side-by-side
opam
View file @
84fe6493
...
...
@@ -12,5 +12,5 @@ remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { >= "8.6.1" & < "8.8~" }
"coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
"coq-stdpp" { (= "dev.2017-11-2
0.0
") | (= "dev") }
"coq-stdpp" { (= "dev.2017-11-2
2.1
") | (= "dev") }
]
theories/proofmode/coq_tactics.v
View file @
84fe6493
...
...
@@ -55,7 +55,7 @@ Definition envs_lookup_delete {M} (i : ident)
let
(
Γ
p
,
Γ
s
)
:
=
Δ
in
match
env_lookup_delete
i
Γ
p
with
|
Some
(
P
,
Γ
p'
)
=>
Some
(
true
,
P
,
Envs
Γ
p'
Γ
s
)
|
None
=>
'
(
P
,
Γ
s'
)
←
env_lookup_delete
i
Γ
s
;
Some
(
false
,
P
,
Envs
Γ
p
Γ
s'
)
|
None
=>
'
'
(
P
,
Γ
s'
)
←
env_lookup_delete
i
Γ
s
;
Some
(
false
,
P
,
Envs
Γ
p
Γ
s'
)
end
.
Fixpoint
envs_lookup_delete_list
{
M
}
(
js
:
list
ident
)
(
remove_persistent
:
bool
)
...
...
@@ -63,9 +63,9 @@ Fixpoint envs_lookup_delete_list {M} (js : list ident) (remove_persistent : bool
match
js
with
|
[]
=>
Some
(
true
,
[],
Δ
)
|
j
::
js
=>
'
(
p
,
P
,
Δ
'
)
←
envs_lookup_delete
j
Δ
;
let
Δ
'
:
=
if
p
then
(
if
remove_persistent
then
Δ
'
else
Δ
)
else
Δ
'
in
'
(
q
,
Hs
,
Δ
''
)
←
envs_lookup_delete_list
js
remove_persistent
Δ
'
;
'
'
(
p
,
P
,
Δ
'
)
←
envs_lookup_delete
j
Δ
;
let
Δ
'
:
=
if
p
:
bool
then
(
if
remove_persistent
then
Δ
'
else
Δ
)
else
Δ
'
in
'
'
(
q
,
Hs
,
Δ
''
)
←
envs_lookup_delete_list
js
remove_persistent
Δ
'
;
Some
(
p
&&
q
,
P
::
Hs
,
Δ
''
)
end
.
...
...
@@ -109,15 +109,15 @@ Fixpoint envs_split_go {M}
match
js
with
|
[]
=>
Some
(
Δ
1
,
Δ
2
)
|
j
::
js
=>
'
(
p
,
P
,
Δ
1
'
)
←
envs_lookup_delete
j
Δ
1
;
if
p
then
envs_split_go
js
Δ
1
Δ
2
else
'
'
(
p
,
P
,
Δ
1
'
)
←
envs_lookup_delete
j
Δ
1
;
if
p
:
bool
then
envs_split_go
js
Δ
1
Δ
2
else
envs_split_go
js
Δ
1
'
(
envs_snoc
Δ
2
false
j
P
)
end
.
(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
if [d = Left] then [result = (hyps named js, remaining hyps)] *)
Definition
envs_split
{
M
}
(
d
:
direction
)
(
js
:
list
ident
)
(
Δ
:
envs
M
)
:
option
(
envs
M
*
envs
M
)
:
=
'
(
Δ
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
).
(* Coq versions of the tactics *)
...
...
@@ -297,7 +297,7 @@ Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
Lemma
envs_lookup_envs_clear_spatial
Δ
j
:
envs_lookup
j
(
envs_clear_spatial
Δ
)
=
'
(
p
,
P
)
←
envs_lookup
j
Δ
;
if
p
then
Some
(
p
,
P
)
else
None
.
=
'
'
(
p
,
P
)
←
envs_lookup
j
Δ
;
if
p
:
bool
then
Some
(
p
,
P
)
else
None
.
Proof
.
rewrite
/
envs_lookup
/
envs_clear_spatial
.
destruct
Δ
as
[
Γ
p
Γ
s
]
;
simpl
;
destruct
(
Γ
p
!!
j
)
eqn
:
?
;
simplify_eq
/=
;
auto
.
...
...
@@ -640,7 +640,7 @@ Qed.
Lemma
tac_specialize_assert
Δ
Δ
'
Δ
1
Δ
2
'
j
q
neg
js
R
P1
P2
P1'
Q
:
envs_lookup_delete
j
Δ
=
Some
(
q
,
R
,
Δ
'
)
→
IntoWand
false
R
P1
P2
→
ElimModal
P1'
P1
Q
Q
→
(
'
(
Δ
1
,
Δ
2
)
←
envs_split
(
if
neg
is
true
then
Right
else
Left
)
js
Δ
'
;
(
'
'
(
Δ
1
,
Δ
2
)
←
envs_split
(
if
neg
is
true
then
Right
else
Left
)
js
Δ
'
;
Δ
2
'
←
envs_app
false
(
Esnoc
Enil
j
P2
)
Δ
2
;
Some
(
Δ
1
,
Δ
2
'
))
=
Some
(
Δ
1
,
Δ
2
'
)
→
(* does not preserve position of [j] *)
envs_entails
Δ
1
P1'
→
envs_entails
Δ
2
'
Q
→
envs_entails
Δ
Q
.
...
...
theories/proofmode/environments.v
View file @
84fe6493
...
...
@@ -17,11 +17,9 @@ Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
end
.
Module
env_notations
.
Notation
"y ≫= f"
:
=
(
match
y
with
Some
x
=>
f
x
|
None
=>
None
end
).
Notation
"x ← y ; z"
:
=
(
match
y
with
Some
x
=>
z
|
None
=>
None
end
).
Notation
"' ( x1 , x2 ) ← y ; z"
:
=
(
match
y
with
Some
(
x1
,
x2
)
=>
z
|
None
=>
None
end
).
Notation
"' ( x1 , x2 , x3 ) ← y ; z"
:
=
(
match
y
with
Some
(
x1
,
x2
,
x3
)
=>
z
|
None
=>
None
end
).
Notation
"' x1 .. xn ← y ; z"
:
=
(
y
≫
=
(
λ
x1
,
..
(
λ
xn
,
z
)
..
)).
Notation
"Γ !! j"
:
=
(
env_lookup
j
Γ
).
End
env_notations
.
Import
env_notations
.
...
...
@@ -68,7 +66,7 @@ Fixpoint env_lookup_delete {A} (i : ident) (Γ : env A) : option (A * env A) :=
|
Enil
=>
None
|
Esnoc
Γ
j
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
.
Inductive
env_Forall2
{
A
B
}
(
P
:
A
→
B
→
Prop
)
:
env
A
→
env
B
→
Prop
:
=
...
...
theories/proofmode/intro_patterns.v
View file @
84fe6493
...
...
@@ -39,9 +39,9 @@ Fixpoint close_list (k : stack)
|
SList
::
k
=>
Some
(
SPat
(
IList
(
ps
::
pss
))
::
k
)
|
SPat
pat
::
k
=>
close_list
k
(
pat
::
ps
)
pss
|
SAlwaysElim
::
k
=>
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close_list
k
(
IAlwaysElim
p
::
ps
)
pss
'
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close_list
k
(
IAlwaysElim
p
::
ps
)
pss
|
SModalElim
::
k
=>
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close_list
k
(
IModalElim
p
::
ps
)
pss
'
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close_list
k
(
IModalElim
p
::
ps
)
pss
|
SBar
::
k
=>
close_list
k
[]
(
ps
::
pss
)
|
_
=>
None
end
.
...
...
@@ -114,8 +114,8 @@ Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
match
k
with
|
[]
=>
Some
ps
|
SPat
pat
::
k
=>
close
k
(
pat
::
ps
)
|
SAlwaysElim
::
k
=>
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close
k
(
IAlwaysElim
p
::
ps
)
|
SModalElim
::
k
=>
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close
k
(
IModalElim
p
::
ps
)
|
SAlwaysElim
::
k
=>
'
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close
k
(
IAlwaysElim
p
::
ps
)
|
SModalElim
::
k
=>
'
'
(
p
,
ps
)
←
maybe2
(
::
)
ps
;
close
k
(
IModalElim
p
::
ps
)
|
_
=>
None
end
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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