Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Lennard Gäher
Iris
Commits
4973d0b3
Commit
4973d0b3
authored
Dec 23, 2020
by
Robbert Krebbers
Browse files
Remove old `Hint Extern` hack for `impl_persistent` that seems no longer needed.
parent
58c1caae
Changes
3
Hide whitespace changes
Inline
Sidebyside
iris/bi/plainly.v
View file @
4973d0b3
...
@@ 362,8 +362,7 @@ Proof. intros; destruct p; simpl; apply _. Qed.
...
@@ 362,8 +362,7 @@ Proof. intros; destruct p; simpl; apply _. Qed.
Lemma
plain_persistent
P
:
Plain
P
→
Persistent
P
.
Lemma
plain_persistent
P
:
Plain
P
→
Persistent
P
.
Proof
.
intros
.
by
rewrite
/
Persistent

plainly_elim_persistently
.
Qed
.
Proof
.
intros
.
by
rewrite
/
Persistent

plainly_elim_persistently
.
Qed
.
(* Not an instance, see the bottom of this file *)
Global
Instance
impl_persistent
P
Q
:
Lemma
impl_persistent
P
Q
:
Absorbing
P
→
Plain
P
→
Persistent
Q
→
Persistent
(
P
→
Q
).
Absorbing
P
→
Plain
P
→
Persistent
Q
→
Persistent
(
P
→
Q
).
Proof
.
Proof
.
intros
.
by
rewrite
/
Persistent
{
2
}(
plain
P
)

persistently_impl_plainly
intros
.
by
rewrite
/
Persistent
{
2
}(
plain
P
)

persistently_impl_plainly
...
@@ 645,10 +644,3 @@ To avoid that, we declare it using a [Hint Immediate], so that it will
...
@@ 645,10 +644,3 @@ To avoid that, we declare it using a [Hint Immediate], so that it will
only be used at the leaves of the proof search tree, i.e. when the
only be used at the leaves of the proof search tree, i.e. when the
premise of the hint can be derived from just the current context. *)
premise of the hint can be derived from just the current context. *)
Global
Hint
Immediate
plain_persistent
:
typeclass_instances
.
Global
Hint
Immediate
plain_persistent
:
typeclass_instances
.
(* Not defined using an ordinary [Instance] because the default
[class_apply @impl_persistent] shelves the [BiPlainly] premise, making proof
search for the other premises fail. See the proof of [coreP_persistent] for an
example where it would fail with a regular [Instance].*)
Global
Hint
Extern
4
(
Persistent
_
)
=>
notypeclasses
refine
(
impl_persistent
_
_
_
_
_
)
:
typeclass_instances
.
tests/bi.ref
0 → 100644
View file @
4973d0b3
tests/bi.v
0 → 100644
View file @
4973d0b3
From
iris
.
bi
Require
Import
bi
plainly
.
(** See https://gitlab.mpisws.org/iris/iris//merge_requests/610 *)
Lemma
test_impl_persistent_1
`
{!
BiPlainly
PROP
}
:
Persistent
(
PROP
:
=
PROP
)
(
True
→
True
).
Proof
.
apply
_
.
Qed
.
Lemma
test_impl_persistent_2
`
{!
BiPlainly
PROP
}
:
Persistent
(
PROP
:
=
PROP
)
(
True
→
True
→
True
).
Proof
.
apply
_
.
Qed
.
Write
Preview
Supports
Markdown
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