Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
stdpp
Commits
812f01bf
Commit
812f01bf
authored
Apr 19, 2019
by
Dan Frumin
Committed by
Robbert Krebbers
Apr 19, 2019
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
gmultiset lemmas
parent
d98ab4e4
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
64 additions
and
4 deletions
+64
-4
theories/fin_sets.v
theories/fin_sets.v
+24
-0
theories/gmultiset.v
theories/gmultiset.v
+30
-4
theories/list.v
theories/list.v
+10
-0
No files found.
theories/fin_sets.v
View file @
812f01bf
...
@@ -101,6 +101,14 @@ Proof.
...
@@ -101,6 +101,14 @@ Proof.
apply
Permutation_singleton
.
by
rewrite
<-(
right_id
∅
(
∪
)
{[
x
]}),
apply
Permutation_singleton
.
by
rewrite
<-(
right_id
∅
(
∪
)
{[
x
]}),
elements_union_singleton
,
elements_empty
by
set_solver
.
elements_union_singleton
,
elements_empty
by
set_solver
.
Qed
.
Qed
.
Lemma
elements_disj_union
(
X
Y
:
C
)
:
X
##
Y
→
elements
(
X
∪
Y
)
≡
ₚ
elements
X
++
elements
Y
.
Proof
.
intros
HXY
.
apply
NoDup_Permutation
.
-
apply
NoDup_elements
.
-
apply
NoDup_app
.
set_solver
by
eauto
using
NoDup_elements
.
-
set_solver
.
Qed
.
Lemma
elements_submseteq
X
Y
:
X
⊆
Y
→
elements
X
⊆
+
elements
Y
.
Lemma
elements_submseteq
X
Y
:
X
⊆
Y
→
elements
X
⊆
+
elements
Y
.
Proof
.
Proof
.
intros
;
apply
NoDup_submseteq
;
eauto
using
NoDup_elements
.
intros
;
apply
NoDup_submseteq
;
eauto
using
NoDup_elements
.
...
@@ -222,6 +230,22 @@ Lemma set_fold_proper {B} (R : relation B) `{!Equivalence R}
...
@@ -222,6 +230,22 @@ Lemma set_fold_proper {B} (R : relation B) `{!Equivalence R}
Proper
((
≡
)
==>
R
)
(
set_fold
f
b
:
C
→
B
).
Proper
((
≡
)
==>
R
)
(
set_fold
f
b
:
C
→
B
).
Proof
.
intros
??
E
.
apply
(
foldr_permutation
R
f
b
)
;
auto
.
by
rewrite
E
.
Qed
.
Proof
.
intros
??
E
.
apply
(
foldr_permutation
R
f
b
)
;
auto
.
by
rewrite
E
.
Qed
.
Lemma
set_fold_empty
{
B
}
(
f
:
A
→
B
→
B
)
(
b
:
B
)
:
set_fold
f
b
(
∅
:
C
)
=
b
.
Proof
.
by
unfold
set_fold
;
simpl
;
rewrite
elements_empty
.
Qed
.
Lemma
set_fold_singleton
{
B
}
(
f
:
A
→
B
→
B
)
(
b
:
B
)
(
a
:
A
)
:
set_fold
f
b
({[
a
]}
:
C
)
=
f
a
b
.
Proof
.
by
unfold
set_fold
;
simpl
;
rewrite
elements_singleton
.
Qed
.
Lemma
set_fold_disj_union
(
f
:
A
→
A
→
A
)
(
b
:
A
)
X
Y
:
Comm
(=)
f
→
Assoc
(=)
f
→
X
##
Y
→
set_fold
f
b
(
X
∪
Y
)
=
set_fold
f
(
set_fold
f
b
X
)
Y
.
Proof
.
intros
Hcomm
Hassoc
Hdisj
.
unfold
set_fold
;
simpl
.
by
rewrite
elements_disj_union
,
<-
foldr_app
,
(
comm
(++)).
Qed
.
(** * Minimal elements *)
(** * Minimal elements *)
Lemma
minimal_exists
R
`
{!
Transitive
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
.
X
≢
∅
→
∃
x
,
x
∈
X
∧
minimal
R
x
X
.
...
...
theories/gmultiset.v
View file @
812f01bf
...
@@ -330,7 +330,23 @@ Proof.
...
@@ -330,7 +330,23 @@ Proof.
destruct
(
X
!!
x
)
;
naive_solver
lia
.
destruct
(
X
!!
x
)
;
naive_solver
lia
.
Qed
.
Qed
.
(* Properties of the size operation *)
(** Properties of the set_fold operation *)
Lemma
gmultiset_set_fold_empty
{
B
}
(
f
:
A
→
B
→
B
)
(
b
:
B
)
:
set_fold
f
b
(
∅
:
gmultiset
A
)
=
b
.
Proof
.
by
unfold
set_fold
;
simpl
;
rewrite
gmultiset_elements_empty
.
Qed
.
Lemma
gmultiset_set_fold_singleton
{
B
}
(
f
:
A
→
B
→
B
)
(
b
:
B
)
(
a
:
A
)
:
set_fold
f
b
({[
a
]}
:
gmultiset
A
)
=
f
a
b
.
Proof
.
by
unfold
set_fold
;
simpl
;
rewrite
gmultiset_elements_singleton
.
Qed
.
Lemma
gmultiset_set_fold_disj_union
(
f
:
A
→
A
→
A
)
(
b
:
A
)
X
Y
:
Comm
(=)
f
→
Assoc
(=)
f
→
set_fold
f
b
(
X
⊎
Y
)
=
set_fold
f
(
set_fold
f
b
X
)
Y
.
Proof
.
intros
Hcomm
Hassoc
.
unfold
set_fold
;
simpl
.
by
rewrite
gmultiset_elements_disj_union
,
<-
foldr_app
,
(
comm
(++)).
Qed
.
(** Properties of the size operation *)
Lemma
gmultiset_size_empty
:
size
(
∅
:
gmultiset
A
)
=
0
.
Lemma
gmultiset_size_empty
:
size
(
∅
:
gmultiset
A
)
=
0
.
Proof
.
done
.
Qed
.
Proof
.
done
.
Qed
.
Lemma
gmultiset_size_empty_inv
X
:
size
X
=
0
→
X
=
∅
.
Lemma
gmultiset_size_empty_inv
X
:
size
X
=
0
→
X
=
∅
.
...
@@ -370,7 +386,7 @@ Proof.
...
@@ -370,7 +386,7 @@ Proof.
by
rewrite
gmultiset_elements_disj_union
,
app_length
.
by
rewrite
gmultiset_elements_disj_union
,
app_length
.
Qed
.
Qed
.
(* Order stuff *)
(*
*
Order stuff *)
Global
Instance
gmultiset_po
:
PartialOrder
(
⊆
@{
gmultiset
A
}).
Global
Instance
gmultiset_po
:
PartialOrder
(
⊆
@{
gmultiset
A
}).
Proof
.
Proof
.
split
;
[
split
|].
split
;
[
split
|].
...
@@ -464,6 +480,13 @@ Proof.
...
@@ -464,6 +480,13 @@ Proof.
rewrite
HX
at
2
;
rewrite
gmultiset_size_disj_union
.
lia
.
rewrite
HX
at
2
;
rewrite
gmultiset_size_disj_union
.
lia
.
Qed
.
Qed
.
Lemma
gmultiset_empty_difference
X
Y
:
Y
⊆
X
→
Y
∖
X
=
∅
.
Proof
.
intros
HYX
.
unfold_leibniz
.
intros
x
.
rewrite
multiplicity_difference
,
multiplicity_empty
.
specialize
(
HYX
x
).
lia
.
Qed
.
Lemma
gmultiset_non_empty_difference
X
Y
:
X
⊂
Y
→
Y
∖
X
≠
∅
.
Lemma
gmultiset_non_empty_difference
X
Y
:
X
⊂
Y
→
Y
∖
X
≠
∅
.
Proof
.
Proof
.
intros
[
_
HXY2
]
Hdiff
;
destruct
HXY2
;
intros
x
.
intros
[
_
HXY2
]
Hdiff
;
destruct
HXY2
;
intros
x
.
...
@@ -471,13 +494,16 @@ Proof.
...
@@ -471,13 +494,16 @@ Proof.
rewrite
multiplicity_difference
,
multiplicity_empty
;
lia
.
rewrite
multiplicity_difference
,
multiplicity_empty
;
lia
.
Qed
.
Qed
.
Lemma
gmultiset_difference_diag
X
:
X
∖
X
=
∅
.
Proof
.
by
apply
gmultiset_empty_difference
.
Qed
.
Lemma
gmultiset_difference_subset
X
Y
:
X
≠
∅
→
X
⊆
Y
→
Y
∖
X
⊂
Y
.
Lemma
gmultiset_difference_subset
X
Y
:
X
≠
∅
→
X
⊆
Y
→
Y
∖
X
⊂
Y
.
Proof
.
Proof
.
intros
.
eapply
strict_transitive_l
;
[
by
apply
gmultiset_union_subset_r
|].
intros
.
eapply
strict_transitive_l
;
[
by
apply
gmultiset_union_subset_r
|].
by
rewrite
<-(
gmultiset_disj_union_difference
X
Y
).
by
rewrite
<-(
gmultiset_disj_union_difference
X
Y
).
Qed
.
Qed
.
(* Mononicity *)
(*
*
Mononicity *)
Lemma
gmultiset_elements_submseteq
X
Y
:
X
⊆
Y
→
elements
X
⊆
+
elements
Y
.
Lemma
gmultiset_elements_submseteq
X
Y
:
X
⊆
Y
→
elements
X
⊆
+
elements
Y
.
Proof
.
Proof
.
intros
->%
gmultiset_disj_union_difference
.
rewrite
gmultiset_elements_disj_union
.
intros
->%
gmultiset_disj_union_difference
.
rewrite
gmultiset_elements_disj_union
.
...
@@ -495,7 +521,7 @@ Proof.
...
@@ -495,7 +521,7 @@ Proof.
gmultiset_size_disj_union
by
auto
.
lia
.
gmultiset_size_disj_union
by
auto
.
lia
.
Qed
.
Qed
.
(* Well-foundedness *)
(*
*
Well-foundedness *)
Lemma
gmultiset_wf
:
wf
(
⊂
@{
gmultiset
A
}).
Lemma
gmultiset_wf
:
wf
(
⊂
@{
gmultiset
A
}).
Proof
.
Proof
.
apply
(
wf_projected
(<)
size
)
;
auto
using
gmultiset_subset_size
,
lt_wf
.
apply
(
wf_projected
(<)
size
)
;
auto
using
gmultiset_subset_size
,
lt_wf
.
...
...
theories/list.v
View file @
812f01bf
...
@@ -3446,6 +3446,16 @@ Lemma foldr_permutation_proper {A B} (R : relation B) `{!PreOrder R}
...
@@ -3446,6 +3446,16 @@ Lemma foldr_permutation_proper {A B} (R : relation B) `{!PreOrder R}
(Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
(Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
Proper ((≡ₚ) ==> R) (foldr f b).
Proper ((≡ₚ) ==> R) (foldr f b).
Proof. intros l1 l2 Hl. apply foldr_permutation; auto. Qed.
Proof. intros l1 l2 Hl. apply foldr_permutation; auto. Qed.
Instance foldr_permutation_proper' {A} (R : relation A) `{!PreOrder R}
(f : A → A → A) (a : A) `{!∀ a, Proper (R ==> R) (f a), !Assoc R f, !Comm R f} :
Proper ((≡ₚ) ==> R) (foldr f a).
Proof.
apply (foldr_permutation_proper R f); [solve_proper|].
assert (Proper (R ==> R ==> R) f).
{ intros a1 a2 Ha b1 b2 Hb. by rewrite Hb, (comm f a1), Ha, (comm f). }
intros a1 a2 b.
by rewrite (assoc f), (comm f _ b), (assoc f), (comm f b), (comm f _ a2).
Qed.
(** ** Properties of the [zip_with] and [zip] functions *)
(** ** Properties of the [zip_with] and [zip] functions *)
Section zip_with.
Section zip_with.
...
...
Write
Preview
Markdown
is supported
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