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
Iris
Fairis
Commits
dafb6fa6
Commit
dafb6fa6
authored
Jun 16, 2018
by
Ralf Jung
Browse files
bump Iris; fix build
parent
39843c62
Pipeline
#10763
passed with stage
in 11 minutes and 29 seconds
Changes
10
Pipelines
28
Hide whitespace changes
Inline
Side-by-side
opam
View file @
dafb6fa6
...
...
@@ -6,5 +6,5 @@ install: [make "install"]
remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"]
depends: [
"coq" { (>= "8.7.2") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-06-
0
5.
5.4946e270
") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-06-
1
5.
3.d88d654b
") | (= "dev") }
]
theories/algebra/base_logic.v
View file @
dafb6fa6
...
...
@@ -15,4 +15,4 @@ Hint Resolve sep_mono : I. (* sep_elim_l' sep_elim_r' *)
Hint
Immediate
True_intro
False_elim
:
I
.
Hint
Immediate
iff_refl
internal_eq_refl
:
I
.
(
*
Setup
of
the
proof
mode
*
)
Hint
Extern
1
(
coq_tactics
.
envs_entails
_
(
|==>
_
))
=>
iModIntro
.
\ No newline at end of file
Hint
Extern
1
(
environments
.
envs_entails
_
(
|==>
_
))
=>
iModIntro
.
theories/chan2heap/simple_reln.v
View file @
dafb6fa6
...
...
@@ -33,7 +33,7 @@ Section lr.
Local
Notation
cvalC
:=
(
leibnizC
(
chan_lang
.
val
)).
Import
uPred
coq_tactics
.
Import
uPred
proofmode
.
coq_tactics
proofmode
.
reduction
.
(
*
Notation
ownT
:=
(
λ
i
ec
K
,
ownT
i
ec
K
(
dK
ec
)).
*
)
...
...
@@ -395,7 +395,7 @@ Section lr.
|
_
=>
eapply
tac_refine_bind
with
_
j
_
_
_
K
;
first
(
fast_by
iAssumptionCore
);
[
env_cbv
;
reflexivity
|
]
[
pm_
reflexivity
|
]
end
.
Tactic
Notation
"refine_unbind"
constr
(
K
)
"at"
constr
(
j
)
:=
...
...
@@ -403,7 +403,7 @@ Section lr.
|
_
=>
eapply
tac_refine_unbind
with
_
j
_
_
_
K
;
first
(
fast_by
iAssumptionCore
);
[
env_cbv
;
reflexivity
|
]
[
pm_
reflexivity
|
]
end
.
Tactic
Notation
"refine_unbind"
constr
(
K
)
constr
(
K
'
)
"at"
constr
(
j
)
:=
...
...
@@ -411,7 +411,7 @@ Section lr.
|
_
=>
eapply
tac_refine_unbind
with
_
j
_
_
K
K
'
;
first
(
fast_by
iAssumptionCore
);
[
env_cbv
;
reflexivity
|
]
[
pm_
reflexivity
|
]
end
.
Tactic
Notation
"refine_unbind"
constr
(
K
)
:=
...
...
@@ -419,7 +419,7 @@ Tactic Notation "refine_unbind" constr(K) :=
|
_
=>
eapply
tac_refine_unbind
with
_
_
_
_
_
K
;
first
(
fast_by
iAssumptionCore
);
[
env_cbv
;
reflexivity
|
]
[
pm_
reflexivity
|
]
end
.
Tactic
Notation
"refine_focus"
open_constr
(
efoc
)
:=
...
...
theories/chan_lang/refine_heap_proofmode.v
View file @
dafb6fa6
From
fri
.
algebra
Require
Export
base_logic
.
From
iris
.
proofmode
Require
Import
tactics
coq_tactics
.
From
iris
.
proofmode
Require
Import
tactics
coq_tactics
reduction
.
From
fri
.
chan_lang
Require
Export
tactics
refine_heap
notation
.
Import
uPred
.
...
...
@@ -587,14 +587,14 @@ Tactic Notation "refine_bind" constr(K) "at" constr(j) :=
|
_
=>
eapply
(
tac_refine_bind
_
_
_
j
_
_
_
K
);
first
(
fast_by
iAssumptionCore
);
[
env_cbv
;
reflexivity
|
]
[
pm_
reflexivity
|
]
end
.
Tactic
Notation
"refine_bind"
constr
(
K
)
:=
lazymatch
eval
hnf
in
K
with
|
_
=>
eapply
(
tac_refine_bind
_
_
_
_
_
_
_
K
);
first
(
fast_by
iAssumptionCore
);
[
env_cbv
;
reflexivity
|
]
[
pm_
reflexivity
|
]
end
.
Tactic
Notation
"refine_unbind"
constr
(
K
)
"at"
constr
(
j
)
:=
...
...
@@ -602,7 +602,7 @@ Tactic Notation "refine_unbind" constr(K) "at" constr(j) :=
|
_
=>
eapply
(
tac_refine_unbind
_
_
_
j
_
_
_
K
);
first
(
fast_by
iAssumptionCore
);
[
env_cbv
;
reflexivity
|
]
[
pm_
reflexivity
|
]
end
.
Tactic
Notation
"refine_unbind"
constr
(
K
)
constr
(
K
'
)
"at"
constr
(
j
)
:=
...
...
@@ -610,7 +610,7 @@ Tactic Notation "refine_unbind" constr(K) constr(K') "at" constr(j) :=
|
_
=>
eapply
(
tac_refine_unbind
_
_
_
j
_
_
K
K
'
);
first
(
fast_by
iAssumptionCore
);
[
env_cbv
;
reflexivity
|
]
[
pm_
reflexivity
|
]
end
.
Tactic
Notation
"refine_unbind"
constr
(
K
)
:=
...
...
@@ -618,7 +618,7 @@ Tactic Notation "refine_unbind" constr(K) :=
|
_
=>
eapply
(
tac_refine_unbind
_
_
_
_
_
_
_
K
);
first
(
fast_by
iAssumptionCore
);
[
env_cbv
;
reflexivity
|
]
[
pm_
reflexivity
|
]
end
.
Lemma
envs_entails_of_envs_refl
{
PROP
:
bi
}
Δ
:
...
...
@@ -638,11 +638,11 @@ Tactic Notation "refine_alloc" constr(dnew) ident(l) "as" constr(H) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_alloc: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_alloc: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
first
[
intros
l
|
fail
1
"refine_alloc:"
l
"not fresh"
];
eexists
;
split
;
[
env_cbv
;
reflexivity
||
fail
"refine_allc:"
H
"not fresh"
[
pm_
reflexivity
||
fail
"refine_allc:"
H
"not fresh"
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]]
|
_
=>
fail
"refine_alloc: no ownT found"
end
.
...
...
@@ -662,11 +662,11 @@ Tactic Notation "refine_recv" constr(dnew) :=
end
)
|
fail
1
"refine_recv: cannot find 'Load' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
env_cbv
;
eauto
|
pm_reduce
;
eauto
|
case
cleft
;
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_recv: no ownT found"
end
.
...
...
@@ -682,11 +682,11 @@ Tactic Notation "refine_recv_miss" constr(dnew) :=
end
)
|
fail
1
"refine_recv: cannot find 'Load' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
env_cbv
;
eauto
|
pm_reduce
;
eauto
|
case
cleft
;
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_recv: no ownT found"
end
.
...
...
@@ -703,11 +703,11 @@ Tactic Notation "refine_send" constr(dnew) :=
|
fail
1
"refine_send: cannot find 'Send' in "
e0
];
[
try
omega
|
try
omega
|
wp_done
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
env_cbv
;
eauto
|
pm_reduce
;
eauto
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_send: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_send: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_send: no ownT found"
end
.
...
...
@@ -724,11 +724,11 @@ Tactic Notation "refine_select" constr(dnew) :=
|
fail
1
"refine_select: cannot find 'Select' in "
e0
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
env_cbv
;
eauto
|
pm_reduce
;
eauto
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_select: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_select: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_select: no ownT found"
end
.
...
...
@@ -745,11 +745,11 @@ Tactic Notation "refine_rcase_left" constr(dnew) :=
end
)
|
fail
1
"refine_recv: cannot find 'Load' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
env_cbv
;
eauto
|
pm_reduce
;
eauto
|
case
cleft
;
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_recv: no ownT found"
end
.
...
...
@@ -766,11 +766,11 @@ Tactic Notation "refine_rcase_right" constr(dnew) :=
end
)
|
fail
1
"refine_recv: cannot find 'Load' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
env_cbv
;
eauto
|
pm_reduce
;
eauto
|
case
cleft
;
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_recv: no ownT found"
end
.
...
...
@@ -787,11 +787,11 @@ Tactic Notation "refine_rcase_miss" constr(dnew) :=
end
)
|
fail
1
"refine_recv: cannot find 'Load' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
env_cbv
;
eauto
|
pm_reduce
;
eauto
|
case
cleft
;
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_recv: no ownT found"
end
.
...
...
@@ -813,12 +813,12 @@ Tactic Notation "refine_rec" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_lam: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
wp_done
|
wp_done
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
;
simpl_subst
]
end
)
|
fail
1
"refine_lam: cannot find 'App' in "
e
]
...
...
@@ -838,12 +838,12 @@ Tactic Notation "refine_lam" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_lam: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
wp_done
|
wp_done
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
;
simpl_subst
]
end
)
|
fail
1
"refine_lam: cannot find 'App' in "
e
]
...
...
@@ -869,13 +869,13 @@ Tactic Notation "refine_letp" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_alloc: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
wp_done
|
wp_done
|
wp_done
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
;
simpl_subst
]
end
)
|
fail
1
"refine_rec: cannot find 'App' in "
e
]
...
...
@@ -889,9 +889,9 @@ Tactic Notation "refine_delay" constr(dnew) :=
[
try
omega
|
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
eauto
|
pm_reduce
;
eauto
|
]
|
_
=>
fail
"refine_focus: could not find ownT"
end
.
...
...
@@ -920,10 +920,10 @@ Tactic Notation "refine_op" constr(dnew) :=
|
fail
1
"refine_op: cannot find 'BinOp' or 'UnOp' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_cas_suc: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_cas_suc: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
rewrite
/=
?
to_of_val
;
fast_done
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_op: no ownT found"
end
.
...
...
@@ -942,11 +942,11 @@ Tactic Notation "refine_fork" constr(dnew) ident(t) "as" constr(H) :=
|
fail
1
"refine_fork: cannot find 'Fork' in "
e0
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_fork: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_fork: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
first
[
intros
t
|
fail
1
"refine_fork:"
t
"not fresh"
];
eexists
;
split
;
[
env_cbv
;
reflexivity
||
fail
"refine_fork:"
H
"not fresh"
[
pm_
reflexivity
||
fail
"refine_fork:"
H
"not fresh"
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
;
rewrite
/
fresh_delay
/=
?
to_of_val
]]
|
_
=>
fail
"refine_fork: no ownT found"
end
.
...
...
@@ -959,7 +959,7 @@ Ltac refine_stopped :=
|
|-
context
[
Esnoc
_
_
(
ownT
?
i
?
e
?
K
?
d0
)]
=>
eapply
tac_refine_stopped
with
_
i
e
_
;
[
wp_done
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_stopped: non-affine ctxt"
]
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_stopped: non-affine ctxt"
]
end
.
Tactic
Notation
"refine_if_true"
constr
(
dnew
)
:=
...
...
@@ -974,9 +974,9 @@ Tactic Notation "refine_if_true" constr(dnew) :=
|
fail
1
"refine_if_true: cannot find 'If' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_if_true: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_if_true: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_if_true: no ownT found"
end
.
...
...
@@ -993,9 +993,9 @@ Tactic Notation "refine_if_false" constr(dnew) :=
|
fail
1
"refine_if_false: cannot find 'If' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_if_true: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_if_true: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_if_false: no ownT found"
end
.
...
...
theories/heap_lang/proofmode.v
View file @
dafb6fa6
From
fri
.
algebra
Require
Export
base_logic
.
From
iris
.
proofmode
Require
Import
tactics
coq_tactics
.
From
iris
.
proofmode
Require
Import
tactics
coq_tactics
reduction
.
From
fri
.
heap_lang
Require
Export
wp_tactics
heap
notation
.
Import
uPred
.
...
...
@@ -159,7 +159,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
|
apply
_
|
first
[
intros
l
|
fail
1
"wp_alloc:"
l
"not fresh"
];
eexists
;
split
;
[
env_cbv
;
reflexivity
||
fail
"wp_alloc:"
H
"not fresh"
[
pm_
reflexivity
||
fail
"wp_alloc:"
H
"not fresh"
|
wp_finish
]]
|
_
=>
fail
"wp_alloc: not a 'wp'"
end
.
...
...
@@ -199,7 +199,7 @@ Tactic Notation "wp_store" :=
|
apply
_
|
let
l
:=
match
goal
with
|-
_
=
Some
(
_
,
(
?
l
↦
{
_
}
_
)
%
I
)
=>
l
end
in
iAssumptionCore
||
fail
"wp_store: cannot find"
l
"↦ ?"
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
wp_finish
]
|
_
=>
fail
"wp_store: not a 'wp'"
end
.
...
...
@@ -244,7 +244,7 @@ Tactic Notation "wp_cas_suc" :=
|
let
l
:=
match
goal
with
|-
_
=
Some
(
_
,
(
?
l
↦
{
_
}
_
)
%
I
)
=>
l
end
in
iAssumptionCore
||
fail
"wp_cas_suc: cannot find"
l
"↦ ?"
|
try
congruence
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
wp_finish
]
|
_
=>
fail
"wp_cas_suc: not a 'wp'"
end
.
...
...
@@ -264,7 +264,7 @@ Tactic Notation "wp_swap" :=
|
apply
_
|
let
l
:=
match
goal
with
|-
_
=
Some
(
_
,
(
?
l
↦
{
_
}
_
)
%
I
)
=>
l
end
in
iAssumptionCore
||
fail
"wp_store: cannot find"
l
"↦ ?"
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
wp_finish
]
|
_
=>
fail
"wp_store: not a 'wp'"
end
.
...
...
@@ -282,7 +282,7 @@ Tactic Notation "wp_fai" :=
|
apply
_
|
let
l
:=
match
goal
with
|-
_
=
Some
(
_
,
(
?
l
↦
{
_
}
_
)
%
I
)
=>
l
end
in
iAssumptionCore
||
fail
"wp_store: cannot find"
l
"↦ ?"
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
wp_finish
]
|
_
=>
fail
"wp_store: not a 'wp'"
end
.
\ No newline at end of file
end
.
theories/heap_lang/refine_proofmode.v
View file @
dafb6fa6
From
fri
.
algebra
Require
Export
base_logic
.
From
iris
.
proofmode
Require
Export
tactics
coq_tactics
.
From
iris
.
proofmode
Require
Export
tactics
coq_tactics
reduction
.
From
fri
.
heap_lang
Require
Export
wp_tactics
heap
refine_heap
notation
proofmode
.
Import
uPred
.
...
...
@@ -463,14 +463,14 @@ Tactic Notation "refine_bind" constr(K) "at" constr(j) :=
|
_
=>
eapply
(
tac_refine_bind
_
_
_
j
_
_
_
K
);
first
(
fast_by
iAssumptionCore
);
[
env_cbv
;
reflexivity
|
]
[
pm_
reflexivity
|
]
end
.
Tactic
Notation
"refine_bind"
constr
(
K
)
:=
lazymatch
eval
hnf
in
K
with
|
_
=>
eapply
(
tac_refine_bind
_
_
_
_
_
_
_
K
);
first
(
fast_by
iAssumptionCore
);
[
env_cbv
;
reflexivity
|
]
[
pm_
reflexivity
|
]
end
.
Tactic
Notation
"refine_unbind"
constr
(
K
)
"at"
constr
(
j
)
:=
...
...
@@ -478,7 +478,7 @@ Tactic Notation "refine_unbind" constr(K) "at" constr(j) :=
|
_
=>
eapply
(
tac_refine_unbind
_
_
_
j
_
_
_
K
);
first
(
fast_by
iAssumptionCore
);
[
env_cbv
;
reflexivity
|
]
[
pm_
reflexivity
|
]
end
.
Tactic
Notation
"refine_unbind"
constr
(
K
)
constr
(
K
'
)
"at"
constr
(
j
)
:=
...
...
@@ -486,7 +486,7 @@ Tactic Notation "refine_unbind" constr(K) constr(K') "at" constr(j) :=
|
_
=>
eapply
(
tac_refine_unbind
_
_
_
j
_
_
K
K
'
);
first
(
fast_by
iAssumptionCore
);
[
env_cbv
;
reflexivity
|
]
[
pm_
reflexivity
|
]
end
.
Tactic
Notation
"refine_unbind"
constr
(
K
)
:=
...
...
@@ -494,7 +494,7 @@ Tactic Notation "refine_unbind" constr(K) :=
|
_
=>
eapply
(
tac_refine_unbind
_
_
_
_
_
_
_
K
);
first
(
fast_by
iAssumptionCore
);
[
env_cbv
;
reflexivity
|
]
[
pm_
reflexivity
|
]
end
.
Tactic
Notation
"refine_alloc"
constr
(
dnew
)
ident
(
l
)
"as"
constr
(
H
)
:=
...
...
@@ -511,11 +511,11 @@ Tactic Notation "refine_alloc" constr(dnew) ident(l) "as" constr(H) :=
|
wp_done
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_alloc: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_alloc: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
first
[
intros
l
|
fail
1
"refine_alloc:"
l
"not fresh"
];
eexists
;
split
;
[
env_cbv
;
reflexivity
||
fail
"refine_allc:"
H
"not fresh"
[
pm_
reflexivity
||
fail
"refine_allc:"
H
"not fresh"
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]]
|
_
=>
fail
"refine_alloc: no ownT found"
end
.
...
...
@@ -537,9 +537,9 @@ Tactic Notation "refine_load" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_load: no ownT found"
end
.
...
...
@@ -558,9 +558,9 @@ Tactic Notation "refine_store" constr(dnew) :=
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_store: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_store: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_store: no ownT found"
end
.
...
...
@@ -584,9 +584,9 @@ Tactic Notation "refine_cas_fail" constr(dnew) :=
|
iAssumptionCore
|
iAssumptionCore
|
try
congruence
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_cas_fail: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_cas_fail: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_cas_fail: no ownT found"
end
.
...
...
@@ -610,9 +610,9 @@ Tactic Notation "refine_cas_suc" constr(dnew) :=
|
iAssumptionCore
|
iAssumptionCore
|
try
congruence
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_cas_suc: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_cas_suc: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_cas_suc: no ownT found"
end
.
...
...
@@ -631,9 +631,9 @@ Tactic Notation "refine_swap" constr(dnew) :=
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_swap: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_swap: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_store: no ownT found"
end
.
...
...
@@ -652,9 +652,9 @@ Tactic Notation "refine_fai" constr(dnew) :=
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_fai: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_fai: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_store: no ownT found"
end
.
...
...
@@ -676,12 +676,12 @@ Tactic Notation "refine_rec" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_rec: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
wp_done
|
fast_done
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
;
simpl_subst
]
end
)
|
fail
1
"refine_rec: cannot find 'App' in "
e
]
...
...
@@ -700,12 +700,12 @@ Tactic Notation "refine_lam" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_rec: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
wp_done
|
wp_done
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
;
simpl_subst
]
end
)
|
fail
1
"refine_lam: cannot find 'App' in "
e
]
...
...
@@ -722,9 +722,9 @@ Tactic Notation "refine_delay" constr(dnew) :=
[
try
omega
|
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_delay: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_delay: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
eauto
|
pm_reduce
;
eauto
|
]
|
_
=>
fail
"refine_focus: could not find ownT"
end
.
...
...
@@ -752,10 +752,10 @@ Tactic Notation "refine_op" constr(dnew) :=
|
fail
1
"refine_op: cannot find 'BinOp' or 'UnOp' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_op: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_op: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
wp_done
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_op: no ownT found"
end
.
...
...
@@ -776,11 +776,11 @@ Tactic Notation "refine_proj" constr(dnew) :=
|
fail
1
"refine_proj: cannot find 'Fst' or 'Snd' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_proj: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_proj: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
wp_done
|
wp_done
|
env_cbv
;
reflexivity
|
pm_
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
|
_
=>
fail
"refine_proj: no ownT found"
end
.
...
...
@@ -798,11 +798,11 @@ Tactic Notation "refine_fork" constr(dnew) ident(t) "as" constr(H) :=
|
fail
1
"refine_fork: cannot find 'Fork' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_fork: non-affine ctxt"
|
pm_reduce
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_fork: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
first
[
intros
t
|
fail
1
"refine_fork:"
t
"not fresh"
];
eexists
;
split
;
[
env_cbv
;
reflexivity
||
fail
"refine_fork:"
H
"not fresh"
[
pm_
reflexivity
||
fail
"refine_fork:"
H
"not fresh"
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]]