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
stdpp
Commits
7c3203e7
Commit
7c3203e7
authored
Jun 20, 2019
by
Ralf Jung
Browse files
make solve_ndisj more powerful
parent
3bf046f2
Changes
4
Hide whitespace changes
Inline
Side-by-side
tests/solve_ndisj.ref
View file @
7c3203e7
The command has indeed failed with message:
Ltac call to "solve_ndisj" failed.
No applicable tactic.
tests/solve_ndisj.v
View file @
7c3203e7
From
stdpp
Require
Import
namespaces
strings
.
Set
Ltac
Backtrace
.
Lemma
test1
(
N1
N2
:
namespace
)
:
N1
##
N2
→
↑
N1
⊆
@{
coPset
}
⊤
∖
↑
N2
.
Proof
.
solve_ndisj
.
Qed
.
...
...
@@ -20,9 +18,4 @@ Proof. solve_ndisj. Qed.
Lemma
test5
(
N1
N2
:
namespace
)
:
⊤
∖
↑
N1
∖
↑
N2
⊆
@{
coPset
}
⊤
∖
↑
N1
.@
"x"
∖
↑
N2
∖
↑
N1
.@
"y"
.
Proof
.
Fail
solve_ndisj
.
(* FIXME: it should be able to solve this. *)
apply
namespace_subseteq_difference
.
{
apply
ndot_preserve_disjoint_r
.
set_solver
.
}
solve_ndisj
.
Qed
.
Proof
.
solve_ndisj
.
Qed
.
theories/namespaces.v
View file @
7c3203e7
...
...
@@ -88,13 +88,15 @@ Hint Resolve namespace_subseteq_difference : ndisj.
Hint
Extern
0
(
_
##
_
)
=>
apply
ndot_ne_disjoint
;
congruence
:
ndisj
.
Hint
Resolve
ndot_preserve_disjoint_l
ndot_preserve_disjoint_r
:
ndisj
.
Hint
Resolve
nclose_subseteq'
ndisj_difference_l
:
ndisj
.
Hint
Resolve
namespace_subseteq_difference_l
|
100
:
ndisj
.
Hint
Resolve
(
empty_subseteq
(
A
:
=
positive
)
(
C
:
=
coPset
))
:
ndisj
.
Hint
Resolve
(
union_least
(
A
:
=
positive
)
(
C
:
=
coPset
))
:
ndisj
.
(* Fall-back rules that lose information (but let other rules above apply). *)
Hint
Resolve
namespace_subseteq_difference_l
|
100
:
ndisj
.
Hint
Resolve
(
disjoint_difference_l
(
A
:
=
positive
)
(
C
:
=
coPset
))
|
100
:
ndisj
.
Ltac
solve_ndisj
:
=
repeat
match
goal
with
|
H
:
_
∪
_
⊆
_
|-
_
=>
apply
union_subseteq
in
H
as
[??]
end
;
solve
[
eauto
1
0
with
ndisj
].
solve
[
eauto
1
2
with
ndisj
].
Hint
Extern
1000
=>
solve_ndisj
:
solve_ndisj
.
theories/sets.v
View file @
7c3203e7
...
...
@@ -656,6 +656,10 @@ Section set.
(** Disjointness *)
Lemma
disjoint_intersection
X
Y
:
X
##
Y
↔
X
∩
Y
≡
∅
.
Proof
.
set_solver
.
Qed
.
Lemma
disjoint_difference_l
X
Y1
Y2
:
Y1
##
X
→
Y1
∖
Y2
##
X
.
Proof
.
set_solver
.
Qed
.
Lemma
disjoint_difference_r
X
Y1
Y2
:
X
##
Y1
→
X
##
Y1
∖
Y2
.
Proof
.
set_solver
.
Qed
.
Section
leibniz
.
Context
`
{!
LeibnizEquiv
C
}.
...
...
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