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
Tej Chajed
stdpp
Commits
2d56770b
Commit
2d56770b
authored
Nov 21, 2016
by
Robbert Krebbers
Browse files
More generic definition of minimal that also for for anti-symmetric relations.
parent
8db5c86f
Changes
2
Hide whitespace changes
Inline
Side-by-side
theories/collections.v
View file @
2d56770b
...
...
@@ -996,7 +996,7 @@ End seq_set.
(** Mimimal elements *)
Definition
minimal
`
{
ElemOf
A
C
}
(
R
:
relation
A
)
(
x
:
A
)
(
X
:
C
)
:
Prop
:
=
∀
y
,
y
∈
X
→
R
y
x
→
y
=
x
.
∀
y
,
y
∈
X
→
R
y
x
→
R
x
y
.
Instance
:
Params
(@
minimal
)
5
.
Section
minimal
.
...
...
@@ -1004,6 +1004,20 @@ Section minimal.
Global
Instance
minimal_proper
x
:
Proper
(@
equiv
C
_
==>
iff
)
(
minimal
R
x
).
Proof
.
intros
X
X'
y
;
unfold
minimal
;
set_solver
.
Qed
.
Lemma
minimal_anti_symm
`
{!
AntiSymm
(=)
R
}
x
X
:
minimal
R
x
X
↔
∀
y
,
y
∈
X
→
R
y
x
→
x
=
y
.
Proof
.
unfold
minimal
;
split
;
[|
naive_solver
].
intros
Hmin
y
??.
apply
(
anti_symm
_
)
;
auto
.
Qed
.
Lemma
minimal_strict
`
{!
StrictOrder
R
}
x
X
:
minimal
R
x
X
↔
∀
y
,
y
∈
X
→
¬
R
y
x
.
Proof
.
unfold
minimal
;
split
;
[|
naive_solver
].
intros
Hmin
y
??.
destruct
(
irreflexivity
R
x
)
;
trans
y
;
auto
.
Qed
.
Lemma
empty_minimal
x
:
minimal
R
x
∅
.
Proof
.
unfold
minimal
;
set_solver
.
Qed
.
Lemma
singleton_minimal
x
:
minimal
R
x
{[
x
]}.
...
...
@@ -1016,11 +1030,10 @@ Section minimal.
Lemma
minimal_subseteq
X
Y
x
:
minimal
R
x
X
→
Y
⊆
X
→
minimal
R
x
Y
.
Proof
.
unfold
minimal
;
set_solver
.
Qed
.
Lemma
minimal_weaken
`
{!
StrictOrder
R
}
X
x
x'
:
Lemma
minimal_weaken
`
{!
Transitive
R
}
X
x
x'
:
minimal
R
x
X
→
R
x'
x
→
minimal
R
x'
X
.
Proof
.
intros
Hmin
?
y
??.
assert
(
y
=
x
)
as
->
by
(
apply
(
Hmin
y
)
;
[
done
|
by
trans
x'
]).
destruct
(
irreflexivity
R
x
).
by
trans
x'
.
intros
Hmin
?
y
??.
trans
x
;
[
done
|].
by
eapply
(
Hmin
y
),
transitivity
.
Qed
.
End
minimal
.
theories/fin_collections.v
View file @
2d56770b
...
...
@@ -189,7 +189,7 @@ Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
Proof
.
intros
??
E
.
apply
(
foldr_permutation
R
f
b
)
;
auto
.
by
rewrite
E
.
Qed
.
(** * Minimal elements *)
Lemma
minimal_exists
`
{!
StrictOrder
R
,
∀
x
y
,
Decision
(
R
x
y
)}
(
X
:
C
)
:
Lemma
minimal_exists
R
`
{!
Transitive
R
,
∀
x
y
,
Decision
(
R
x
y
)}
(
X
:
C
)
:
X
≢
∅
→
∃
x
,
x
∈
X
∧
minimal
R
x
X
.
Proof
.
pattern
X
;
apply
collection_ind
;
clear
X
.
...
...
@@ -205,10 +205,10 @@ Proof.
exists
x
;
split
;
[
set_solver
|].
rewrite
HX
,
(
right_id
_
(
∪
)).
apply
singleton_minimal
.
Qed
.
Lemma
minimal_exists_L
`
{!
LeibnizEquiv
C
,
!
StrictOrder
R
,
∀
x
y
,
Decision
(
R
x
y
)}
(
X
:
C
)
:
Lemma
minimal_exists_L
R
`
{!
LeibnizEquiv
C
,
!
Transitive
R
,
∀
x
y
,
Decision
(
R
x
y
)}
(
X
:
C
)
:
X
≠
∅
→
∃
x
,
x
∈
X
∧
minimal
R
x
X
.
Proof
.
unfold_leibniz
.
apply
minimal_exists
.
Qed
.
Proof
.
unfold_leibniz
.
apply
(
minimal_exists
R
)
.
Qed
.
(** * Filter *)
Lemma
elem_of_filter
(
P
:
A
→
Prop
)
`
{!
∀
x
,
Decision
(
P
x
)}
X
x
:
...
...
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