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
a4363377
Commit
a4363377
authored
Nov 18, 2015
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
More setoid stuff on lists and maps.
parent
02030472
Changes
6
Hide whitespace changes
Inline
Side-by-side
Showing
6 changed files
with
95 additions
and
44 deletions
+95
-44
theories/collections.v
theories/collections.v
+16
-9
theories/fin_collections.v
theories/fin_collections.v
+4
-3
theories/fin_maps.v
theories/fin_maps.v
+17
-8
theories/list.v
theories/list.v
+30
-0
theories/option.v
theories/option.v
+7
-3
theories/orders.v
theories/orders.v
+21
-21
No files found.
theories/collections.v
View file @
a4363377
...
@@ -11,6 +11,8 @@ Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
...
@@ -11,6 +11,8 @@ Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
(** * Basic theorems *)
(** * Basic theorems *)
Section
simple_collection
.
Section
simple_collection
.
Context
`
{
SimpleCollection
A
C
}.
Context
`
{
SimpleCollection
A
C
}.
Implicit
Types
x
y
:
A
.
Implicit
Types
X
Y
:
C
.
Lemma
elem_of_empty
x
:
x
∈
∅
↔
False
.
Lemma
elem_of_empty
x
:
x
∈
∅
↔
False
.
Proof
.
split
.
apply
not_elem_of_empty
.
done
.
Qed
.
Proof
.
split
.
apply
not_elem_of_empty
.
done
.
Qed
.
...
@@ -47,9 +49,10 @@ Section simple_collection.
...
@@ -47,9 +49,10 @@ Section simple_collection.
*
intros
??.
rewrite
elem_of_singleton
.
by
intros
->.
*
intros
??.
rewrite
elem_of_singleton
.
by
intros
->.
*
intros
Ex
.
by
apply
(
Ex
x
),
elem_of_singleton
.
*
intros
Ex
.
by
apply
(
Ex
x
),
elem_of_singleton
.
Qed
.
Qed
.
Global
Instance
singleton_proper
:
Proper
((=)
==>
(
≡
))
singleton
.
Global
Instance
singleton_proper
:
Proper
((=)
==>
(
≡
))
(
singleton
(
B
:
=
C
))
.
Proof
.
by
repeat
intro
;
subst
.
Qed
.
Proof
.
by
repeat
intro
;
subst
.
Qed
.
Global
Instance
elem_of_proper
:
Proper
((=)
==>
(
≡
)
==>
iff
)
(
∈
)
|
5
.
Global
Instance
elem_of_proper
:
Proper
((=)
==>
(
≡
)
==>
iff
)
((
∈
)
:
A
→
C
→
Prop
)
|
5
.
Proof
.
intros
???
;
subst
.
firstorder
.
Qed
.
Proof
.
intros
???
;
subst
.
firstorder
.
Qed
.
Lemma
elem_of_union_list
Xs
x
:
x
∈
⋃
Xs
↔
∃
X
,
X
∈
Xs
∧
x
∈
X
.
Lemma
elem_of_union_list
Xs
x
:
x
∈
⋃
Xs
↔
∃
X
,
X
∈
Xs
∧
x
∈
X
.
Proof
.
Proof
.
...
@@ -59,7 +62,7 @@ Section simple_collection.
...
@@ -59,7 +62,7 @@ Section simple_collection.
*
intros
[
X
[]].
induction
1
;
simpl
;
[
by
apply
elem_of_union_l
|].
*
intros
[
X
[]].
induction
1
;
simpl
;
[
by
apply
elem_of_union_l
|].
intros
.
apply
elem_of_union_r
;
auto
.
intros
.
apply
elem_of_union_r
;
auto
.
Qed
.
Qed
.
Lemma
non_empty_singleton
x
:
{[
x
]}
≢
∅
.
Lemma
non_empty_singleton
x
:
(
{[
x
]}
:
C
)
≢
∅
.
Proof
.
intros
[
E
_
].
by
apply
(
elem_of_empty
x
),
E
,
elem_of_singleton
.
Qed
.
Proof
.
intros
[
E
_
].
by
apply
(
elem_of_empty
x
),
E
,
elem_of_singleton
.
Qed
.
Lemma
not_elem_of_singleton
x
y
:
x
∉
{[
y
]}
↔
x
≠
y
.
Lemma
not_elem_of_singleton
x
y
:
x
∉
{[
y
]}
↔
x
≠
y
.
Proof
.
by
rewrite
elem_of_singleton
.
Qed
.
Proof
.
by
rewrite
elem_of_singleton
.
Qed
.
...
@@ -266,19 +269,21 @@ Tactic Notation "esolve_elem_of" tactic3(tac) :=
...
@@ -266,19 +269,21 @@ Tactic Notation "esolve_elem_of" tactic3(tac) :=
unfold_elem_of
;
unfold_elem_of
;
naive_solver
tac
.
naive_solver
tac
.
Tactic
Notation
"esolve_elem_of"
:
=
esolve_elem_of
eauto
.
Tactic
Notation
"esolve_elem_of"
:
=
esolve_elem_of
eauto
.
(** * More theorems *)
(** * More theorems *)
Section
collection
.
Section
collection
.
Context
`
{
Collection
A
C
}.
Context
`
{
Collection
A
C
}.
Implicit
Types
X
Y
:
C
.
Global
Instance
:
Lattice
C
.
Global
Instance
:
Lattice
C
.
Proof
.
split
.
apply
_
.
firstorder
auto
.
solve_elem_of
.
Qed
.
Proof
.
split
.
apply
_
.
firstorder
auto
.
solve_elem_of
.
Qed
.
Global
Instance
difference_proper
:
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
(
∖
).
Global
Instance
difference_proper
:
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
(@
difference
C
_
).
Proof
.
Proof
.
intros
X1
X2
HX
Y1
Y2
HY
;
apply
elem_of_equiv
;
intros
x
.
intros
X1
X2
HX
Y1
Y2
HY
;
apply
elem_of_equiv
;
intros
x
.
by
rewrite
!
elem_of_difference
,
HX
,
HY
.
by
rewrite
!
elem_of_difference
,
HX
,
HY
.
Qed
.
Qed
.
Lemma
intersection_singletons
x
:
{[
x
]}
∩
{[
x
]}
≡
{[
x
]}.
Lemma
intersection_singletons
x
:
(
{[
x
]}
:
C
)
∩
{[
x
]}
≡
{[
x
]}.
Proof
.
esolve_elem_of
.
Qed
.
Proof
.
esolve_elem_of
.
Qed
.
Lemma
difference_twice
X
Y
:
(
X
∖
Y
)
∖
Y
≡
X
∖
Y
.
Lemma
difference_twice
X
Y
:
(
X
∖
Y
)
∖
Y
≡
X
∖
Y
.
Proof
.
esolve_elem_of
.
Qed
.
Proof
.
esolve_elem_of
.
Qed
.
...
@@ -475,10 +480,12 @@ Inductive Forall_fresh `{ElemOf A C} (X : C) : list A → Prop :=
...
@@ -475,10 +480,12 @@ Inductive Forall_fresh `{ElemOf A C} (X : C) : list A → Prop :=
Section
fresh
.
Section
fresh
.
Context
`
{
FreshSpec
A
C
}.
Context
`
{
FreshSpec
A
C
}.
Implicit
Types
X
Y
:
C
.
Global
Instance
fresh_proper
:
Proper
((
≡
)
==>
(=))
fresh
.
Global
Instance
fresh_proper
:
Proper
((
≡
)
==>
(=))
(
fresh
(
C
:
=
C
))
.
Proof
.
intros
???.
by
apply
fresh_proper_alt
,
elem_of_equiv
.
Qed
.
Proof
.
intros
???.
by
apply
fresh_proper_alt
,
elem_of_equiv
.
Qed
.
Global
Instance
fresh_list_proper
:
Proper
((=)
==>
(
≡
)
==>
(=))
fresh_list
.
Global
Instance
fresh_list_proper
:
Proper
((=)
==>
(
≡
)
==>
(=))
(
fresh_list
(
C
:
=
C
)).
Proof
.
Proof
.
intros
?
n
->.
induction
n
as
[|
n
IH
]
;
intros
??
E
;
f_equal'
;
[
by
rewrite
E
|].
intros
?
n
->.
induction
n
as
[|
n
IH
]
;
intros
??
E
;
f_equal'
;
[
by
rewrite
E
|].
apply
IH
.
by
rewrite
E
.
apply
IH
.
by
rewrite
E
.
...
@@ -539,7 +546,7 @@ Section collection_monad.
...
@@ -539,7 +546,7 @@ Section collection_monad.
Proof
.
esolve_elem_of
.
Qed
.
Proof
.
esolve_elem_of
.
Qed
.
Lemma
collection_guard_True
{
A
}
`
{
Decision
P
}
(
X
:
M
A
)
:
P
→
guard
P
;
X
≡
X
.
Lemma
collection_guard_True
{
A
}
`
{
Decision
P
}
(
X
:
M
A
)
:
P
→
guard
P
;
X
≡
X
.
Proof
.
esolve_elem_of
.
Qed
.
Proof
.
esolve_elem_of
.
Qed
.
Lemma
collection_fmap_compose
{
A
B
C
}
(
f
:
A
→
B
)
(
g
:
B
→
C
)
X
:
Lemma
collection_fmap_compose
{
A
B
C
}
(
f
:
A
→
B
)
(
g
:
B
→
C
)
(
X
:
M
A
)
:
g
∘
f
<$>
X
≡
g
<$>
(
f
<$>
X
).
g
∘
f
<$>
X
≡
g
<$>
(
f
<$>
X
).
Proof
.
esolve_elem_of
.
Qed
.
Proof
.
esolve_elem_of
.
Qed
.
Lemma
elem_of_fmap_1
{
A
B
}
(
f
:
A
→
B
)
(
X
:
M
A
)
(
y
:
B
)
:
Lemma
elem_of_fmap_1
{
A
B
}
(
f
:
A
→
B
)
(
X
:
M
A
)
(
y
:
B
)
:
...
...
theories/fin_collections.v
View file @
a4363377
...
@@ -12,15 +12,16 @@ Definition collection_fold `{Elements A C} {B}
...
@@ -12,15 +12,16 @@ Definition collection_fold `{Elements A C} {B}
Section
fin_collection
.
Section
fin_collection
.
Context
`
{
FinCollection
A
C
}.
Context
`
{
FinCollection
A
C
}.
Implicit
Types
X
Y
:
C
.
Global
Instance
elements_proper
:
Proper
((
≡
)
==>
(
≡
ₚ
))
elements
.
Global
Instance
elements_proper
:
Proper
((
≡
)
==>
(
≡
ₚ
))
(
elements
(
C
:
=
C
))
.
Proof
.
Proof
.
intros
??
E
.
apply
NoDup_Permutation
.
intros
??
E
.
apply
NoDup_Permutation
.
*
apply
NoDup_elements
.
*
apply
NoDup_elements
.
*
apply
NoDup_elements
.
*
apply
NoDup_elements
.
*
intros
.
by
rewrite
!
elem_of_elements
,
E
.
*
intros
.
by
rewrite
!
elem_of_elements
,
E
.
Qed
.
Qed
.
Global
Instance
collection_size_proper
:
Proper
((
≡
)
==>
(=))
size
.
Global
Instance
collection_size_proper
:
Proper
((
≡
)
==>
(=))
(@
size
C
_
)
.
Proof
.
intros
??
E
.
apply
Permutation_length
.
by
rewrite
E
.
Qed
.
Proof
.
intros
??
E
.
apply
Permutation_length
.
by
rewrite
E
.
Qed
.
Lemma
size_empty
:
size
(
∅
:
C
)
=
0
.
Lemma
size_empty
:
size
(
∅
:
C
)
=
0
.
Proof
.
Proof
.
...
@@ -148,7 +149,7 @@ Qed.
...
@@ -148,7 +149,7 @@ Qed.
Lemma
collection_fold_proper
{
B
}
(
R
:
relation
B
)
`
{!
Equivalence
R
}
Lemma
collection_fold_proper
{
B
}
(
R
:
relation
B
)
`
{!
Equivalence
R
}
(
f
:
A
→
B
→
B
)
(
b
:
B
)
`
{!
Proper
((=)
==>
R
==>
R
)
f
}
(
f
:
A
→
B
→
B
)
(
b
:
B
)
`
{!
Proper
((=)
==>
R
==>
R
)
f
}
(
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
)
(
collection_fold
f
b
).
Proper
((
≡
)
==>
R
)
(
collection_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
.
Global
Instance
set_Forall_dec
`
(
P
:
A
→
Prop
)
Global
Instance
set_Forall_dec
`
(
P
:
A
→
Prop
)
`
{
∀
x
,
Decision
(
P
x
)}
X
:
Decision
(
set_Forall
P
X
)
|
100
.
`
{
∀
x
,
Decision
(
P
x
)}
X
:
Decision
(
set_Forall
P
X
)
|
100
.
...
...
theories/fin_maps.v
View file @
a4363377
...
@@ -71,8 +71,8 @@ Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) :=
...
@@ -71,8 +71,8 @@ Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) :=
Instance
map_difference_with
`
{
Merge
M
}
{
A
}
:
DifferenceWith
A
(
M
A
)
:
=
Instance
map_difference_with
`
{
Merge
M
}
{
A
}
:
DifferenceWith
A
(
M
A
)
:
=
λ
f
,
merge
(
difference_with
f
).
λ
f
,
merge
(
difference_with
f
).
Instance
map_equiv
`
{
∀
A
,
Lookup
K
A
(
M
A
),
Equiv
A
}
:
Equiv
(
M
A
)
|
1
:
=
λ
m1
m2
,
Instance
map_equiv
`
{
∀
A
,
Lookup
K
A
(
M
A
),
Equiv
A
}
:
Equiv
(
M
A
)
|
1
8
:
=
∀
i
,
m1
!!
i
≡
m2
!!
i
.
λ
m1
m2
,
∀
i
,
m1
!!
i
≡
m2
!!
i
.
(** The relation [intersection_forall R] on finite maps describes that the
(** The relation [intersection_forall R] on finite maps describes that the
relation [R] holds for each pair in the intersection. *)
relation [R] holds for each pair in the intersection. *)
...
@@ -117,9 +117,8 @@ Context `{FinMap K M}.
...
@@ -117,9 +117,8 @@ Context `{FinMap K M}.
(** ** Setoids *)
(** ** Setoids *)
Section
setoid
.
Section
setoid
.
Context
`
{
Equiv
A
}.
Context
`
{
Equiv
A
}
`
{!
Equivalence
((
≡
)
:
relation
A
)}.
Global
Instance
map_equivalence
`
{!
Equivalence
((
≡
)
:
relation
A
)}
:
Global
Instance
map_equivalence
:
Equivalence
((
≡
)
:
relation
(
M
A
)).
Equivalence
((
≡
)
:
relation
(
M
A
)).
Proof
.
Proof
.
split
.
split
.
*
by
intros
m
i
.
*
by
intros
m
i
.
...
@@ -130,7 +129,7 @@ Section setoid.
...
@@ -130,7 +129,7 @@ Section setoid.
Proper
((
≡
)
==>
(
≡
))
(
lookup
(
M
:
=
M
A
)
i
).
Proper
((
≡
)
==>
(
≡
))
(
lookup
(
M
:
=
M
A
)
i
).
Proof
.
by
intros
m1
m2
Hm
.
Qed
.
Proof
.
by
intros
m1
m2
Hm
.
Qed
.
Global
Instance
partial_alter_proper
:
Global
Instance
partial_alter_proper
:
Proper
(((
≡
)
==>
(
≡
))
==>
(=)
==>
(
≡
)
==>
(
≡
))
partial_alter
.
Proper
(((
≡
)
==>
(
≡
))
==>
(=)
==>
(
≡
)
==>
(
≡
))
(
partial_alter
(
M
:
=
M
A
))
.
Proof
.
Proof
.
by
intros
f1
f2
Hf
i
?
<-
m1
m2
Hm
j
;
destruct
(
decide
(
i
=
j
))
as
[->|]
;
by
intros
f1
f2
Hf
i
?
<-
m1
m2
Hm
j
;
destruct
(
decide
(
i
=
j
))
as
[->|]
;
rewrite
?lookup_partial_alter
,
?lookup_partial_alter_ne
by
done
;
rewrite
?lookup_partial_alter
,
?lookup_partial_alter_ne
by
done
;
...
@@ -151,12 +150,12 @@ Section setoid.
...
@@ -151,12 +150,12 @@ Section setoid.
Lemma
merge_ext
f
g
Lemma
merge_ext
f
g
`
{!
PropHolds
(
f
None
None
=
None
),
!
PropHolds
(
g
None
None
=
None
)}
:
`
{!
PropHolds
(
f
None
None
=
None
),
!
PropHolds
(
g
None
None
=
None
)}
:
((
≡
)
==>
(
≡
)
==>
(
≡
))%
signature
f
g
→
((
≡
)
==>
(
≡
)
==>
(
≡
))%
signature
f
g
→
((
≡
)
==>
(
≡
)
==>
(
≡
))%
signature
(
merge
f
)
(
merge
g
).
((
≡
)
==>
(
≡
)
==>
(
≡
))%
signature
(
merge
(
M
:
=
M
)
f
)
(
merge
g
).
Proof
.
Proof
.
by
intros
Hf
??
Hm1
??
Hm2
i
;
rewrite
!
lookup_merge
by
done
;
apply
Hf
.
by
intros
Hf
??
Hm1
??
Hm2
i
;
rewrite
!
lookup_merge
by
done
;
apply
Hf
.
Qed
.
Qed
.
Global
Instance
union_with_proper
:
Global
Instance
union_with_proper
:
Proper
(((
≡
)
==>
(
≡
)
==>
(
≡
))
==>
(
≡
)
==>
(
≡
)
==>
(
≡
))
union_with
.
Proper
(((
≡
)
==>
(
≡
)
==>
(
≡
))
==>
(
≡
)
==>
(
≡
)
==>(
≡
))
(
union_with
(
M
:
=
M
A
))
.
Proof
.
Proof
.
intros
??
Hf
??
Hm1
??
Hm2
i
;
apply
(
merge_ext
_
_
)
;
auto
.
intros
??
Hf
??
Hm1
??
Hm2
i
;
apply
(
merge_ext
_
_
)
;
auto
.
by
do
2
destruct
1
;
first
[
apply
Hf
|
constructor
].
by
do
2
destruct
1
;
first
[
apply
Hf
|
constructor
].
...
@@ -167,6 +166,16 @@ Section setoid.
...
@@ -167,6 +166,16 @@ Section setoid.
*
by
intros
Hm
;
apply
map_eq
;
intros
i
;
unfold_leibniz
;
apply
lookup_proper
.
*
by
intros
Hm
;
apply
map_eq
;
intros
i
;
unfold_leibniz
;
apply
lookup_proper
.
*
by
intros
<-
;
intros
i
;
fold_leibniz
.
*
by
intros
<-
;
intros
i
;
fold_leibniz
.
Qed
.
Qed
.
Lemma
map_equiv_empty
(
m
:
M
A
)
:
m
≡
∅
↔
m
=
∅
.
Proof
.
split
;
[
intros
Hm
;
apply
map_eq
;
intros
i
|
by
intros
->].
by
rewrite
lookup_empty
,
<-
equiv_None
,
Hm
,
lookup_empty
.
Qed
.
Lemma
map_equiv_lookup
(
m1
m2
:
M
A
)
i
x
:
m1
≡
m2
→
m1
!!
i
=
Some
x
→
∃
y
,
m2
!!
i
=
Some
y
∧
x
≡
y
.
Proof
.
intros
Hm
?.
destruct
(
equiv_Some
(
m1
!!
i
)
(
m2
!!
i
)
x
)
as
(
y
&?&?)
;
eauto
.
Qed
.
End
setoid
.
End
setoid
.
(** ** General properties *)
(** ** General properties *)
...
...
theories/list.v
View file @
a4363377
...
@@ -35,6 +35,12 @@ Notation "( x ≢ₚ)" := (λ y, x ≢ₚ y) (only parsing) : C_scope.
...
@@ -35,6 +35,12 @@ Notation "( x ≢ₚ)" := (λ y, x ≢ₚ y) (only parsing) : C_scope.
Notation "(≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : C_scope.
Notation "(≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : C_scope.
(** * Definitions *)
(** * Definitions *)
(** Setoid equality lifted to lists *)
Inductive list_equiv `{Equiv A} : Equiv (list A) :=
| nil_equiv : [] ≡ []
| cons_equiv x y l k : x ≡ y → l ≡ k → x :: l ≡ y :: k.
Existing Instance list_equiv.
(** The operation [l !! i] gives the [i]th element of the list [l], or [None]
(** The operation [l !! i] gives the [i]th element of the list [l], or [None]
in case [i] is out of bounds. *)
in case [i] is out of bounds. *)
Instance list_lookup {A} : Lookup nat A (list A) :=
Instance list_lookup {A} : Lookup nat A (list A) :=
...
@@ -356,6 +362,30 @@ Context {A : Type}.
...
@@ -356,6 +362,30 @@ Context {A : Type}.
Implicit Types x y z : A.
Implicit Types x y z : A.
Implicit Types l k : list A.
Implicit Types l k : list A.
Section setoid.
Context `{Equiv A} `{!Equivalence ((≡) : relation A)}.
Global Instance map_equivalence : Equivalence ((≡) : relation (list A)).
Proof.
split.
* intros l; induction l; constructor; auto.
* induction 1; constructor; auto.
* intros l1 l2 l3 Hl; revert l3.
induction Hl; inversion_clear 1; constructor; try etransitivity; eauto.
Qed.
Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cons A).
Proof. by constructor. Qed.
Global Instance app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@app A).
Proof.
induction 1 as [|x y l k ?? IH]; intros ?? Htl; simpl; auto.
by apply cons_equiv, IH.
Qed.
Global Instance list_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (list A).
Proof.
intros l1 l2; split; [|by intros <-].
induction 1; f_equal; fold_leibniz; auto.
Qed.
End setoid.
Global Instance: Injective2 (=) (=) (=) (@cons A).
Global Instance: Injective2 (=) (=) (=) (@cons A).
Proof. by injection 1. Qed.
Proof. by injection 1. Qed.
Global Instance: ∀ k, Injective (=) (=) (k ++).
Global Instance: ∀ k, Injective (=) (=) (k ++).
...
...
theories/option.v
View file @
a4363377
...
@@ -89,10 +89,9 @@ Definition option_relation {A B} (R: A → B → Prop) (P: A → Prop) (Q: B →
...
@@ -89,10 +89,9 @@ Definition option_relation {A B} (R: A → B → Prop) (P: A → Prop) (Q: B →
(** Setoids *)
(** Setoids *)
Section
setoids
.
Section
setoids
.
Context
`
{
Equiv
A
}.
Context
`
{
Equiv
A
}
`
{!
Equivalence
((
≡
)
:
relation
A
)}
.
Global
Instance
option_equiv
:
Equiv
(
option
A
)
:
=
option_Forall2
(
≡
).
Global
Instance
option_equiv
:
Equiv
(
option
A
)
:
=
option_Forall2
(
≡
).
Global
Instance
option_equivalence
`
{!
Equivalence
((
≡
)
:
relation
A
)}
:
Global
Instance
option_equivalence
:
Equivalence
((
≡
)
:
relation
(
option
A
)).
Equivalence
((
≡
)
:
relation
(
option
A
)).
Proof
.
Proof
.
split
.
split
.
*
by
intros
[]
;
constructor
.
*
by
intros
[]
;
constructor
.
...
@@ -106,6 +105,11 @@ Section setoids.
...
@@ -106,6 +105,11 @@ Section setoids.
intros
x
y
;
split
;
[
destruct
1
;
fold_leibniz
;
congruence
|].
intros
x
y
;
split
;
[
destruct
1
;
fold_leibniz
;
congruence
|].
by
intros
<-
;
destruct
x
;
constructor
;
fold_leibniz
.
by
intros
<-
;
destruct
x
;
constructor
;
fold_leibniz
.
Qed
.
Qed
.
Lemma
equiv_None
(
mx
:
option
A
)
:
mx
≡
None
↔
mx
=
None
.
Proof
.
split
;
[
by
inversion_clear
1
|
by
intros
->].
Qed
.
Lemma
equiv_Some
(
mx
my
:
option
A
)
x
:
mx
≡
my
→
mx
=
Some
x
→
∃
y
,
my
=
Some
y
∧
x
≡
y
.
Proof
.
destruct
1
;
naive_solver
.
Qed
.
End
setoids
.
End
setoids
.
(** Equality on [option] is decidable. *)
(** Equality on [option] is decidable. *)
...
...
theories/orders.v
View file @
a4363377
...
@@ -309,7 +309,7 @@ End merge_sort_correct.
...
@@ -309,7 +309,7 @@ End merge_sort_correct.
(** We extend the canonical pre-order [⊆] to a partial order by defining setoid
(** We extend the canonical pre-order [⊆] to a partial order by defining setoid
equality as [λ X Y, X ⊆ Y ∧ Y ⊆ X]. We prove that this indeed gives rise to a
equality as [λ X Y, X ⊆ Y ∧ Y ⊆ X]. We prove that this indeed gives rise to a
setoid. *)
setoid. *)
Instance
preorder_equiv
`
{
SubsetEq
A
}
:
Equiv
A
:
=
λ
X
Y
,
X
⊆
Y
∧
Y
⊆
X
.
Instance
preorder_equiv
`
{
SubsetEq
A
}
:
Equiv
A
|
20
:
=
λ
X
Y
,
X
⊆
Y
∧
Y
⊆
X
.
Section
preorder
.
Section
preorder
.
Context
`
{
SubsetEq
A
,
!
PreOrder
(@
subseteq
A
_
)}.
Context
`
{
SubsetEq
A
,
!
PreOrder
(@
subseteq
A
_
)}.
...
@@ -321,13 +321,13 @@ Section preorder.
...
@@ -321,13 +321,13 @@ Section preorder.
*
by
intros
??
[??].
*
by
intros
??
[??].
*
by
intros
X
Y
Z
[??]
[??]
;
split
;
transitivity
Y
.
*
by
intros
X
Y
Z
[??]
[??]
;
split
;
transitivity
Y
.
Qed
.
Qed
.
Global
Instance
:
Proper
((
≡
)
==>
(
≡
)
==>
iff
)
(
⊆
).
Global
Instance
:
Proper
((
≡
)
==>
(
≡
)
==>
iff
)
(
(
⊆
)
:
relation
A
).
Proof
.
Proof
.
unfold
equiv
,
preorder_equiv
.
intros
X1
Y1
?
X2
Y2
?.
split
;
intro
.
unfold
equiv
,
preorder_equiv
.
intros
X1
Y1
?
X2
Y2
?.
split
;
intro
.
*
transitivity
X1
.
tauto
.
transitivity
X2
;
tauto
.
*
transitivity
X1
.
tauto
.
transitivity
X2
;
tauto
.
*
transitivity
Y1
.
tauto
.
transitivity
Y2
;
tauto
.
*
transitivity
Y1
.
tauto
.
transitivity
Y2
;
tauto
.
Qed
.
Qed
.
Lemma
subset_spec
X
Y
:
X
⊂
Y
↔
X
⊆
Y
∧
X
≢
Y
.
Lemma
subset_spec
(
X
Y
:
A
)
:
X
⊂
Y
↔
X
⊆
Y
∧
X
≢
Y
.
Proof
.
Proof
.
split
.
split
.
*
intros
[?
HYX
].
split
.
done
.
contradict
HYX
.
by
rewrite
<-
HYX
.
*
intros
[?
HYX
].
split
.
done
.
contradict
HYX
.
by
rewrite
<-
HYX
.
...
@@ -388,20 +388,20 @@ Section join_semi_lattice.
...
@@ -388,20 +388,20 @@ Section join_semi_lattice.
Proof
.
auto
.
Qed
.
Proof
.
auto
.
Qed
.
Lemma
union_empty
X
:
X
∪
∅
⊆
X
.
Lemma
union_empty
X
:
X
∪
∅
⊆
X
.
Proof
.
by
apply
union_least
.
Qed
.
Proof
.
by
apply
union_least
.
Qed
.
Global
Instance
union_proper
:
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
(
∪
).
Global
Instance
union_proper
:
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
(
@
union
A
_
).
Proof
.
Proof
.
unfold
equiv
,
preorder_equiv
.
unfold
equiv
,
preorder_equiv
.
split
;
apply
union_preserving
;
simpl
in
*
;
tauto
.
split
;
apply
union_preserving
;
simpl
in
*
;
tauto
.
Qed
.
Qed
.
Global
Instance
:
Idempotent
(
≡
)
(
∪
).
Global
Instance
:
Idempotent
(
(
≡
)
:
relation
A
)
(
∪
).
Proof
.
split
;
eauto
.
Qed
.
Proof
.
split
;
eauto
.
Qed
.
Global
Instance
:
LeftId
(
≡
)
∅
(
∪
).
Global
Instance
:
LeftId
(
(
≡
)
:
relation
A
)
∅
(
∪
).
Proof
.
split
;
eauto
.
Qed
.
Proof
.
split
;
eauto
.
Qed
.
Global
Instance
:
RightId
(
≡
)
∅
(
∪
).
Global
Instance
:
RightId
(
(
≡
)
:
relation
A
)
∅
(
∪
).
Proof
.
split
;
eauto
.
Qed
.
Proof
.
split
;
eauto
.
Qed
.
Global
Instance
:
Commutative
(
≡
)
(
∪
).
Global
Instance
:
Commutative
(
(
≡
)
:
relation
A
)
(
∪
).
Proof
.
split
;
auto
.
Qed
.
Proof
.
split
;
auto
.
Qed
.
Global
Instance
:
Associative
(
≡
)
(
∪
).
Global
Instance
:
Associative
(
(
≡
)
:
relation
A
)
(
∪
).
Proof
.
split
;
auto
.
Qed
.
Proof
.
split
;
auto
.
Qed
.
Lemma
subseteq_union
X
Y
:
X
⊆
Y
↔
X
∪
Y
≡
Y
.
Lemma
subseteq_union
X
Y
:
X
⊆
Y
↔
X
∪
Y
≡
Y
.
Proof
.
repeat
split
;
eauto
.
intros
HXY
.
rewrite
<-
HXY
.
auto
.
Qed
.
Proof
.
repeat
split
;
eauto
.
intros
HXY
.
rewrite
<-
HXY
.
auto
.
Qed
.
...
@@ -411,8 +411,8 @@ Section join_semi_lattice.
...
@@ -411,8 +411,8 @@ Section join_semi_lattice.
Proof
.
apply
subseteq_union
.
Qed
.
Proof
.
apply
subseteq_union
.
Qed
.
Lemma
equiv_empty
X
:
X
⊆
∅
→
X
≡
∅
.
Lemma
equiv_empty
X
:
X
⊆
∅
→
X
≡
∅
.
Proof
.
split
;
eauto
.
Qed
.
Proof
.
split
;
eauto
.
Qed
.
Global
Instance
union_list_proper
:
Proper
(
Forall2
(
≡
)
==>
(
≡
))
union_list
.
Global
Instance
union_list_proper
:
Proper
((
≡
)
==>
(
≡
))
(
union_list
(
A
:
=
A
))
.
Proof
.
induction
1
;
simpl
.
done
.
b
y
apply
union_proper
.
Qed
.
Proof
.
by
induction
1
;
simpl
;
tr
y
apply
union_proper
.
Qed
.
Lemma
union_list_nil
:
⋃
@
nil
A
=
∅
.
Lemma
union_list_nil
:
⋃
@
nil
A
=
∅
.
Proof
.
done
.
Qed
.
Proof
.
done
.
Qed
.
Lemma
union_list_cons
X
Xs
:
⋃
(
X
::
Xs
)
=
X
∪
⋃
Xs
.
Lemma
union_list_cons
X
Xs
:
⋃
(
X
::
Xs
)
=
X
∪
⋃
Xs
.
...
@@ -514,16 +514,16 @@ Section meet_semi_lattice.
...
@@ -514,16 +514,16 @@ Section meet_semi_lattice.
Lemma
intersection_preserving
X1
X2
Y1
Y2
:
Lemma
intersection_preserving
X1
X2
Y1
Y2
:
X1
⊆
X2
→
Y1
⊆
Y2
→
X1
∩
Y1
⊆
X2
∩
Y2
.
X1
⊆
X2
→
Y1
⊆
Y2
→
X1
∩
Y1
⊆
X2
∩
Y2
.
Proof
.
auto
.
Qed
.
Proof
.
auto
.
Qed
.
Global
Instance
:
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
(
∩
).
Global
Instance
:
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
(
@
intersection
A
_
).
Proof
.
Proof
.
unfold
equiv
,
preorder_equiv
.
split
;
unfold
equiv
,
preorder_equiv
.
split
;
apply
intersection_preserving
;
simpl
in
*
;
tauto
.
apply
intersection_preserving
;
simpl
in
*
;
tauto
.
Qed
.
Qed
.
Global
Instance
:
Idempotent
(
≡
)
(
∩
).
Global
Instance
:
Idempotent
(
(
≡
)
:
relation
A
)
(
∩
).
Proof
.
split
;
eauto
.
Qed
.
Proof
.
split
;
eauto
.
Qed
.
Global
Instance
:
Commutative
(
≡
)
(
∩
).
Global
Instance
:
Commutative
(
(
≡
)
:
relation
A
)
(
∩
).
Proof
.
split
;
auto
.
Qed
.
Proof
.
split
;
auto
.
Qed
.
Global
Instance
:
Associative
(
≡
)
(
∩
).
Global
Instance
:
Associative
(
(
≡
)
:
relation
A
)
(
∩
).
Proof
.
split
;
auto
.
Qed
.
Proof
.
split
;
auto
.
Qed
.
Lemma
subseteq_intersection
X
Y
:
X
⊆
Y
↔
X
∩
Y
≡
X
.
Lemma
subseteq_intersection
X
Y
:
X
⊆
Y
↔
X
∩
Y
≡
X
.
Proof
.
repeat
split
;
eauto
.
intros
HXY
.
rewrite
<-
HXY
.
auto
.
Qed
.
Proof
.
repeat
split
;
eauto
.
intros
HXY
.
rewrite
<-
HXY
.
auto
.
Qed
.
...
@@ -553,11 +553,11 @@ End meet_semi_lattice.
...
@@ -553,11 +553,11 @@ End meet_semi_lattice.
Section
lattice
.
Section
lattice
.
Context
`
{
Empty
A
,
Lattice
A
,
!
EmptySpec
A
}.
Context
`
{
Empty
A
,
Lattice
A
,
!
EmptySpec
A
}.
Global
Instance
:
LeftAbsorb
(
≡
)
∅
(
∩
).
Global
Instance
:
LeftAbsorb
(
(
≡
)
:
relation
A
)
∅
(
∩
).
Proof
.
split
.
by
apply
intersection_subseteq_l
.
by
apply
subseteq_empty
.
Qed
.
Proof
.
split
.
by
apply
intersection_subseteq_l
.
by
apply
subseteq_empty
.
Qed
.
Global
Instance
:
RightAbsorb
(
≡
)
∅
(
∩
).
Global
Instance
:
RightAbsorb
(
(
≡
)
:
relation
A
)
∅
(
∩
).
Proof
.
intros
?.
by
rewrite
(
commutative
_
),
(
left_absorb
_
_
).
Qed
.
Proof
.
intros
?.
by
rewrite
(
commutative
_
),
(
left_absorb
_
_
).
Qed
.
Global
Instance
:
LeftDistr
(
≡
)
(
∪
)
(
∩
).
Global
Instance
:
LeftDistr
(
(
≡
)
:
relation
A
)
(
∪
)
(
∩
).
Proof
.
Proof
.
intros
X
Y
Z
.
split
;
[|
apply
lattice_distr
].
intros
X
Y
Z
.
split
;
[|
apply
lattice_distr
].
apply
union_least
.
apply
union_least
.
...
@@ -566,9 +566,9 @@ Section lattice.
...
@@ -566,9 +566,9 @@ Section lattice.
*
apply
union_subseteq_r_transitive
,
intersection_subseteq_l
.
*
apply
union_subseteq_r_transitive
,
intersection_subseteq_l
.
*
apply
union_subseteq_r_transitive
,
intersection_subseteq_r
.
*
apply
union_subseteq_r_transitive
,
intersection_subseteq_r
.
Qed
.
Qed
.
Global
Instance
:
RightDistr
(
≡
)
(
∪
)
(
∩
).
Global
Instance
:
RightDistr
(
(
≡
)
:
relation
A
)
(
∪
)
(
∩
).
Proof
.
intros
X
Y
Z
.
by
rewrite
!(
commutative
_
_
Z
),
(
left_distr
_
_
).
Qed
.
Proof
.
intros
X
Y
Z
.
by
rewrite
!(
commutative
_
_
Z
),
(
left_distr
_
_
).
Qed
.
Global
Instance
:
LeftDistr
(
≡
)
(
∩
)
(
∪
).
Global
Instance
:
LeftDistr
(
(
≡
)
:
relation
A
)
(
∩
)
(
∪
).
Proof
.
Proof
.
intros
X
Y
Z
.
split
.
intros
X
Y
Z
.
split
.
*
rewrite
(
left_distr
(
∪
)
(
∩
)).
*
rewrite
(
left_distr
(
∪
)
(
∩
)).
...
@@ -582,7 +582,7 @@ Section lattice.
...
@@ -582,7 +582,7 @@ Section lattice.
+
apply
intersection_subseteq_r_transitive
,
union_subseteq_l
.
+
apply
intersection_subseteq_r_transitive
,
union_subseteq_l
.
+
apply
intersection_subseteq_r_transitive
,
union_subseteq_r
.
+
apply
intersection_subseteq_r_transitive
,
union_subseteq_r
.
Qed
.
Qed
.
Global
Instance
:
RightDistr
(
≡
)
(
∩
)
(
∪
).
Global
Instance
:
RightDistr
(
(
≡
)
:
relation
A
)
(
∩
)
(
∪
).
Proof
.
intros
X
Y
Z
.
by
rewrite
!(
commutative
_
_
Z
),
(
left_distr
_
_
).
Qed
.
Proof
.
intros
X
Y
Z
.
by
rewrite
!(
commutative
_
_
Z
),
(
left_distr
_
_
).
Qed
.
Section
leibniz
.
Section
leibniz
.
...
...
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