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
911412f9
Commit
911412f9
authored
May 25, 2019
by
Robbert Krebbers
Browse files
Port `tac_assumption`.
parent
1945565f
Changes
2
Hide whitespace changes
Inline
Side-by-side
theories/proofmode/coq_tactics.v
View file @
911412f9
...
...
@@ -61,17 +61,17 @@ Proof. intros H. induction H; simpl; apply _. Qed.
Lemma
tac_emp_intro
Δ
:
AffineEnv
(
env_spatial
Δ
)
→
envs_entails
Δ
emp
.
Proof
.
intros
.
by
rewrite
envs_entails_eq
(
affine
(
of_envs
Δ
)).
Qed
.
(* TODO: convert to not take Δ' *)
Lemma
tac_assumption
Δ
Δ
'
i
p
P
Q
:
envs_lookup_delete
true
i
Δ
=
Some
(
p
,
P
,
Δ
'
)
→
Lemma
tac_assumption
Δ
i
p
P
Q
:
envs_lookup
i
Δ
=
Some
(
p
,
P
)
→
FromAssumption
p
P
Q
→
(
if
env_spatial_is_nil
Δ
'
then
TCTrue
(
let
Δ
'
:
=
envs_delete
true
i
p
Δ
in
if
env_spatial_is_nil
Δ
'
then
TCTrue
else
TCOr
(
Absorbing
Q
)
(
AffineEnv
(
env_spatial
Δ
'
)))
→
envs_entails
Δ
Q
.
Proof
.
intros
??
H
.
rewrite
envs_entails_eq
envs_lookup_
delete_
sound
//.
destruct
(
env_spatial_is_nil
Δ
'
)
eqn
:
?.
-
by
rewrite
(
env_spatial_is_nil_intuitionistically
Δ
'
)
//
sep_elim_l
.
intros
??
H
.
rewrite
envs_entails_eq
envs_lookup_sound
//.
simpl
in
*.
destruct
(
env_spatial_is_nil
_
)
eqn
:
?.
-
by
rewrite
(
env_spatial_is_nil_intuitionistically
_
)
//
sep_elim_l
.
-
rewrite
from_assumption
.
destruct
H
;
by
rewrite
sep_elim_l
.
Qed
.
...
...
theories/proofmode/ltac_tactics.v
View file @
911412f9
...
...
@@ -228,7 +228,7 @@ Ltac, but it may be possible in Ltac2. *)
(** * Assumptions *)
Tactic
Notation
"iExact"
constr
(
H
)
:
=
eapply
tac_assumption
with
_
H
_
_;
(* (i:=H) *)
eapply
tac_assumption
with
H
_
_;
(* (i:=H) *)
[
pm_reflexivity
||
let
H
:
=
pretty_ident
H
in
fail
"iExact:"
H
"not found"
...
...
@@ -262,7 +262,7 @@ Tactic Notation "iAssumption" :=
lazymatch
Γ
with
|
Esnoc
?
Γ
?j
?P
=>
first
[
pose
proof
(
_
:
FromAssumption
p
P
Q
)
as
Hass
;
eapply
(
tac_assumption
_
_
j
p
P
)
;
eapply
(
tac_assumption
_
j
p
P
)
;
[
pm_reflexivity
|
apply
Hass
|
pm_reduce
;
iSolveTC
||
...
...
@@ -1051,7 +1051,7 @@ premises [n], the tactic will have the following behavior:
actual error. *)
Local
Ltac
iApplyHypExact
H
:
=
first
[
eapply
tac_assumption
with
_
H
_
_;
(* (i:=H) *)
[
eapply
tac_assumption
with
H
_
_;
(* (i:=H) *)
[
pm_reflexivity
||
fail
1
|
iSolveTC
||
fail
1
|
pm_reduce
;
iSolveTC
]
...
...
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