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
Simon Spies
stdpp
Commits
8d587626
Commit
8d587626
authored
Jun 20, 2018
by
Ralf Jung
Browse files
use lia instead of omega
parent
10636e80
Changes
5
Hide whitespace changes
Inline
Side-by-side
theories/collections.v
View file @
8d587626
...
...
@@ -1051,22 +1051,22 @@ Section seq_set.
x
∈
seq_set
(
C
:
=
C
)
start
len
↔
start
≤
x
<
start
+
len
.
Proof
.
revert
start
.
induction
len
as
[|
len
IH
]
;
intros
start
;
simpl
.
-
rewrite
elem_of_empty
.
omeg
a
.
-
rewrite
elem_of_union
,
elem_of_singleton
,
IH
.
omeg
a
.
-
rewrite
elem_of_empty
.
li
a
.
-
rewrite
elem_of_union
,
elem_of_singleton
,
IH
.
li
a
.
Qed
.
Lemma
seq_set_start_disjoint
start
len
:
{[
start
]}
##
seq_set
(
C
:
=
C
)
(
S
start
)
len
.
Proof
.
intros
x
.
rewrite
elem_of_singleton
,
elem_of_seq_set
.
omeg
a
.
Qed
.
Proof
.
intros
x
.
rewrite
elem_of_singleton
,
elem_of_seq_set
.
li
a
.
Qed
.
Lemma
seq_set_S_disjoint
start
len
:
{[
start
+
len
]}
##
seq_set
(
C
:
=
C
)
start
len
.
Proof
.
intros
x
.
rewrite
elem_of_singleton
,
elem_of_seq_set
.
omeg
a
.
Qed
.
Proof
.
intros
x
.
rewrite
elem_of_singleton
,
elem_of_seq_set
.
li
a
.
Qed
.
Lemma
seq_set_S_union
start
len
:
seq_set
start
(
S
len
)
≡
@{
C
}
{[
start
+
len
]}
∪
seq_set
start
len
.
Proof
.
intros
x
.
rewrite
elem_of_union
,
elem_of_singleton
,
!
elem_of_seq_set
.
omeg
a
.
intros
x
.
rewrite
elem_of_union
,
elem_of_singleton
,
!
elem_of_seq_set
.
li
a
.
Qed
.
Lemma
seq_set_S_union_L
`
{!
LeibnizEquiv
C
}
start
len
:
...
...
theories/gmultiset.v
View file @
8d587626
...
...
@@ -80,14 +80,14 @@ Lemma multiplicity_union X Y x :
multiplicity
x
(
X
∪
Y
)
=
multiplicity
x
X
+
multiplicity
x
Y
.
Proof
.
destruct
X
as
[
X
],
Y
as
[
Y
]
;
unfold
multiplicity
;
simpl
.
rewrite
lookup_union_with
.
destruct
(
X
!!
_
),
(
Y
!!
_
)
;
simpl
;
omeg
a
.
rewrite
lookup_union_with
.
destruct
(
X
!!
_
),
(
Y
!!
_
)
;
simpl
;
li
a
.
Qed
.
Lemma
multiplicity_difference
X
Y
x
:
multiplicity
x
(
X
∖
Y
)
=
multiplicity
x
X
-
multiplicity
x
Y
.
Proof
.
destruct
X
as
[
X
],
Y
as
[
Y
]
;
unfold
multiplicity
;
simpl
.
rewrite
lookup_difference_with
.
destruct
(
X
!!
_
),
(
Y
!!
_
)
;
simplify_option_eq
;
omeg
a
.
destruct
(
X
!!
_
),
(
Y
!!
_
)
;
simplify_option_eq
;
li
a
.
Qed
.
(* Collection *)
...
...
@@ -97,12 +97,12 @@ Proof. done. Qed.
Global
Instance
gmultiset_simple_collection
:
SimpleCollection
A
(
gmultiset
A
).
Proof
.
split
.
-
intros
x
.
rewrite
elem_of_multiplicity
,
multiplicity_empty
.
omeg
a
.
-
intros
x
.
rewrite
elem_of_multiplicity
,
multiplicity_empty
.
li
a
.
-
intros
x
y
.
destruct
(
decide
(
x
=
y
))
as
[->|].
+
rewrite
elem_of_multiplicity
,
multiplicity_singleton
.
split
;
auto
with
lia
.
+
rewrite
elem_of_multiplicity
,
multiplicity_singleton_ne
by
done
.
by
split
;
auto
with
lia
.
-
intros
X
Y
x
.
rewrite
!
elem_of_multiplicity
,
multiplicity_union
.
omeg
a
.
-
intros
X
Y
x
.
rewrite
!
elem_of_multiplicity
,
multiplicity_union
.
li
a
.
Qed
.
Global
Instance
gmultiset_elem_of_dec
:
RelDecision
(
∈
@{
gmultiset
A
}).
Proof
.
refine
(
λ
x
X
,
cast_if
(
decide
(
0
<
multiplicity
x
X
)))
;
done
.
Defined
.
...
...
@@ -110,11 +110,11 @@ Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
(* Algebraic laws *)
Global
Instance
gmultiset_comm
:
Comm
(=@{
gmultiset
A
})
(
∪
).
Proof
.
intros
X
Y
.
apply
gmultiset_eq
;
intros
x
.
rewrite
!
multiplicity_union
;
omeg
a
.
intros
X
Y
.
apply
gmultiset_eq
;
intros
x
.
rewrite
!
multiplicity_union
;
li
a
.
Qed
.
Global
Instance
gmultiset_assoc
:
Assoc
(=@{
gmultiset
A
})
(
∪
).
Proof
.
intros
X
Y
Z
.
apply
gmultiset_eq
;
intros
x
.
rewrite
!
multiplicity_union
;
omeg
a
.
intros
X
Y
Z
.
apply
gmultiset_eq
;
intros
x
.
rewrite
!
multiplicity_union
;
li
a
.
Qed
.
Global
Instance
gmultiset_left_id
:
LeftId
(=@{
gmultiset
A
})
∅
(
∪
).
Proof
.
...
...
@@ -127,7 +127,7 @@ Proof. intros X. by rewrite (comm_L (∪)), (left_id_L _ _). Qed.
Global
Instance
gmultiset_union_inj_1
X
:
Inj
(=)
(=)
(
X
∪
).
Proof
.
intros
Y1
Y2
.
rewrite
!
gmultiset_eq
.
intros
HX
x
;
generalize
(
HX
x
).
rewrite
!
multiplicity_union
.
omeg
a
.
rewrite
!
multiplicity_union
.
li
a
.
Qed
.
Global
Instance
gmultiset_union_inj_2
X
:
Inj
(=)
(=)
(
∪
X
).
Proof
.
intros
Y1
Y2
.
rewrite
<-!(
comm_L
_
X
).
apply
(
inj
_
).
Qed
.
...
...
@@ -185,15 +185,15 @@ Proof.
unfold
elem_of
at
2
,
gmultiset_elem_of
,
multiplicity
;
simpl
.
rewrite
elem_of_list_bind
.
split
.
-
intros
[[??]
[[<-
?]%
elem_of_replicate
->%
elem_of_map_to_list
]]
;
lia
.
-
intros
.
destruct
(
X
!!
x
)
as
[
n
|]
eqn
:
Hx
;
[|
omeg
a
].
-
intros
.
destruct
(
X
!!
x
)
as
[
n
|]
eqn
:
Hx
;
[|
li
a
].
exists
(
x
,
n
)
;
split
;
[|
by
apply
elem_of_map_to_list
].
apply
elem_of_replicate
;
auto
with
omeg
a
.
apply
elem_of_replicate
;
auto
with
li
a
.
Qed
.
Lemma
gmultiset_elem_of_dom
x
X
:
x
∈
dom
(
gset
A
)
X
↔
x
∈
X
.
Proof
.
unfold
dom
,
gmultiset_dom
,
elem_of
at
2
,
gmultiset_elem_of
,
multiplicity
.
destruct
X
as
[
X
]
;
simpl
;
rewrite
elem_of_dom
,
<-
not_eq_None_Some
.
destruct
(
X
!!
x
)
;
naive_solver
omeg
a
.
destruct
(
X
!!
x
)
;
naive_solver
li
a
.
Qed
.
(* Properties of the size operation *)
...
...
@@ -250,7 +250,7 @@ Lemma gmultiset_subseteq_alt X Y :
map_relation
(
≤
)
(
λ
_
,
False
)
(
λ
_
,
True
)
(
gmultiset_car
X
)
(
gmultiset_car
Y
).
Proof
.
apply
forall_proper
;
intros
x
.
unfold
multiplicity
.
destruct
(
gmultiset_car
X
!!
x
),
(
gmultiset_car
Y
!!
x
)
;
naive_solver
omeg
a
.
destruct
(
gmultiset_car
X
!!
x
),
(
gmultiset_car
Y
!!
x
)
;
naive_solver
li
a
.
Qed
.
Global
Instance
gmultiset_subseteq_dec
:
RelDecision
(
⊆
@{
gmultiset
A
}).
Proof
.
...
...
@@ -264,12 +264,12 @@ Proof. apply strict_include. Qed.
Hint
Resolve
gmultiset_subset_subseteq
.
Lemma
gmultiset_empty_subseteq
X
:
∅
⊆
X
.
Proof
.
intros
x
.
rewrite
multiplicity_empty
.
omeg
a
.
Qed
.
Proof
.
intros
x
.
rewrite
multiplicity_empty
.
li
a
.
Qed
.
Lemma
gmultiset_union_subseteq_l
X
Y
:
X
⊆
X
∪
Y
.
Proof
.
intros
x
.
rewrite
multiplicity_union
.
omeg
a
.
Qed
.
Proof
.
intros
x
.
rewrite
multiplicity_union
.
li
a
.
Qed
.
Lemma
gmultiset_union_subseteq_r
X
Y
:
Y
⊆
X
∪
Y
.
Proof
.
intros
x
.
rewrite
multiplicity_union
.
omeg
a
.
Qed
.
Proof
.
intros
x
.
rewrite
multiplicity_union
.
li
a
.
Qed
.
Lemma
gmultiset_union_mono
X1
X2
Y1
Y2
:
X1
⊆
X2
→
Y1
⊆
Y2
→
X1
∪
Y1
⊆
X2
∪
Y2
.
Proof
.
intros
??
x
.
rewrite
!
multiplicity_union
.
by
apply
Nat
.
add_le_mono
.
Qed
.
Lemma
gmultiset_union_mono_l
X
Y1
Y2
:
Y1
⊆
Y2
→
X
∪
Y1
⊆
X
∪
Y2
.
...
...
@@ -278,12 +278,12 @@ Lemma gmultiset_union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∪ Y ⊆ X2 ∪ Y.
Proof
.
intros
.
by
apply
gmultiset_union_mono
.
Qed
.
Lemma
gmultiset_subset
X
Y
:
X
⊆
Y
→
size
X
<
size
Y
→
X
⊂
Y
.
Proof
.
intros
.
apply
strict_spec_alt
;
split
;
naive_solver
auto
with
omeg
a
.
Qed
.
Proof
.
intros
.
apply
strict_spec_alt
;
split
;
naive_solver
auto
with
li
a
.
Qed
.
Lemma
gmultiset_union_subset_l
X
Y
:
Y
≠
∅
→
X
⊂
X
∪
Y
.
Proof
.
intros
HY
%
gmultiset_size_non_empty_iff
.
apply
gmultiset_subset
;
auto
using
gmultiset_union_subseteq_l
.
rewrite
gmultiset_size_union
;
omeg
a
.
rewrite
gmultiset_size_union
;
li
a
.
Qed
.
Lemma
gmultiset_union_subset_r
X
Y
:
X
≠
∅
→
Y
⊂
X
∪
Y
.
Proof
.
rewrite
(
comm_L
(
∪
)).
apply
gmultiset_union_subset_l
.
Qed
.
...
...
@@ -292,9 +292,9 @@ Lemma gmultiset_elem_of_singleton_subseteq x X : x ∈ X ↔ {[ x ]} ⊆ X.
Proof
.
rewrite
elem_of_multiplicity
.
split
.
-
intros
Hx
y
;
destruct
(
decide
(
x
=
y
))
as
[->|].
+
rewrite
multiplicity_singleton
;
omeg
a
.
+
rewrite
multiplicity_singleton_ne
by
done
;
omeg
a
.
-
intros
Hx
.
generalize
(
Hx
x
).
rewrite
multiplicity_singleton
.
omeg
a
.
+
rewrite
multiplicity_singleton
;
li
a
.
+
rewrite
multiplicity_singleton_ne
by
done
;
li
a
.
-
intros
Hx
.
generalize
(
Hx
x
).
rewrite
multiplicity_singleton
.
li
a
.
Qed
.
Lemma
gmultiset_elem_of_subseteq
X1
X2
x
:
x
∈
X1
→
X1
⊆
X2
→
x
∈
X2
.
...
...
@@ -303,7 +303,7 @@ Proof. rewrite !gmultiset_elem_of_singleton_subseteq. by intros ->. Qed.
Lemma
gmultiset_union_difference
X
Y
:
X
⊆
Y
→
Y
=
X
∪
Y
∖
X
.
Proof
.
intros
HXY
.
apply
gmultiset_eq
;
intros
x
;
specialize
(
HXY
x
).
rewrite
multiplicity_union
,
multiplicity_difference
;
omeg
a
.
rewrite
multiplicity_union
,
multiplicity_difference
;
li
a
.
Qed
.
Lemma
gmultiset_union_difference'
x
Y
:
x
∈
Y
→
Y
=
{[
x
]}
∪
Y
∖
{[
x
]}.
Proof
.
...
...
@@ -314,14 +314,14 @@ Qed.
Lemma
gmultiset_size_difference
X
Y
:
Y
⊆
X
→
size
(
X
∖
Y
)
=
size
X
-
size
Y
.
Proof
.
intros
HX
%
gmultiset_union_difference
.
rewrite
HX
at
2
;
rewrite
gmultiset_size_union
.
omeg
a
.
rewrite
HX
at
2
;
rewrite
gmultiset_size_union
.
li
a
.
Qed
.
Lemma
gmultiset_non_empty_difference
X
Y
:
X
⊂
Y
→
Y
∖
X
≠
∅
.
Proof
.
intros
[
_
HXY2
]
Hdiff
;
destruct
HXY2
;
intros
x
.
generalize
(
f_equal
(
multiplicity
x
)
Hdiff
).
rewrite
multiplicity_difference
,
multiplicity_empty
;
omeg
a
.
rewrite
multiplicity_difference
,
multiplicity_empty
;
li
a
.
Qed
.
Lemma
gmultiset_difference_subset
X
Y
:
X
≠
∅
→
X
⊆
Y
→
Y
∖
X
⊂
Y
.
...
...
theories/infinite.v
View file @
8d587626
...
...
@@ -52,15 +52,15 @@ Section Fresh.
revert
n
.
induction
s
as
[
s
IH
]
using
(
well_founded_ind
collection_wf
)
;
intros
n
.
setoid_rewrite
fresh_generic_fixpoint_unfold
;
unfold
fresh_generic_body
.
destruct
decide
as
[
Hcase
|
Hcase
]
;
[|
by
eauto
with
omeg
a
].
destruct
decide
as
[
Hcase
|
Hcase
]
;
[|
by
eauto
with
li
a
].
destruct
(
IH
_
(
subset_difference_elem_of
Hcase
)
(
S
n
))
as
(
m
&
Hmbound
&
Heqfix
&
Hnotin
&
Hinbelow
).
exists
m
;
repeat
split
;
auto
with
omeg
a
.
exists
m
;
repeat
split
;
auto
with
li
a
.
-
rewrite
not_elem_of_difference
,
elem_of_singleton
in
Hnotin
.
destruct
Hnotin
as
[?|?%
inject_injective
]
;
auto
with
omeg
a
.
destruct
Hnotin
as
[?|?%
inject_injective
]
;
auto
with
li
a
.
-
intros
i
Hibound
.
destruct
(
decide
(
i
=
n
))
as
[<-|
Hneq
]
;
[
by
auto
|].
assert
(
inject
i
∈
s
∖
{[
inject
n
]})
by
auto
with
omeg
a
.
assert
(
inject
i
∈
s
∖
{[
inject
n
]})
by
auto
with
li
a
.
set_solver
.
Qed
.
...
...
@@ -76,8 +76,8 @@ Section Fresh.
destruct
(
fresh_generic_fixpoint_spec
Y
0
)
as
(
mY
&
_
&
->
&
HnotinY
&
HbelowinY
).
destruct
(
Nat
.
lt_trichotomy
mX
mY
)
as
[
case
|[->|
case
]]
;
auto
.
+
contradict
HnotinX
.
rewrite
HeqXY
.
apply
HbelowinY
;
omeg
a
.
+
contradict
HnotinY
.
rewrite
<-
HeqXY
.
apply
HbelowinX
;
omeg
a
.
+
contradict
HnotinX
.
rewrite
HeqXY
.
apply
HbelowinY
;
li
a
.
+
contradict
HnotinY
.
rewrite
<-
HeqXY
.
apply
HbelowinX
;
li
a
.
-
intros
X
.
unfold
fresh
,
fresh_generic
.
destruct
(
fresh_generic_fixpoint_spec
X
0
)
as
(
m
&
_
&
->
&
HnotinX
&
HbelowinX
)
;
auto
.
...
...
theories/list.v
View file @
8d587626
...
...
@@ -1484,7 +1484,7 @@ Proof.
eapply
Permutation_cons
,
(
IH
_
g
).
+
rewrite
length_delete
by
(
rewrite
<-
Hl
;
eauto
)
;
simpl
in
*
;
lia
.
+
unfold
g
.
intros
i
j
Hg
.
repeat
destruct
(
lt_eq_lt_dec
_
_
)
as
[[?|?]|?]
;
simplify_eq
/=
;
try
omeg
a
.
repeat
destruct
(
lt_eq_lt_dec
_
_
)
as
[[?|?]|?]
;
simplify_eq
/=
;
try
li
a
.
apply
(
inj
S
),
(
inj
f
)
;
lia
.
+
intros
i
.
unfold
g
.
destruct
(
lt_eq_lt_dec
_
_
)
as
[[?|?]|?].
*
by
rewrite
lookup_delete_lt
,
<-
Hl
.
...
...
theories/nat_cancel.v
View file @
8d587626
...
...
@@ -78,25 +78,25 @@ Module nat_cancel.
Instance
nat_cancel_leaf_plus
m
m'
m''
n1
n2
n1'
n2'
n1'n2'
:
NatCancelR
m
n1
m'
n1'
→
NatCancelR
m'
n2
m''
n2'
→
MakeNatPlus
n1'
n2'
n1'n2'
→
NatCancelR
m
(
n1
+
n2
)
m''
n1'n2'
|
2
.
Proof
.
unfold
NatCancelR
,
NatCancelL
,
MakeNatPlus
.
omeg
a
.
Qed
.
Proof
.
unfold
NatCancelR
,
NatCancelL
,
MakeNatPlus
.
li
a
.
Qed
.
Instance
nat_cancel_leaf_S_here
m
n
m'
n'
:
NatCancelR
m
n
m'
n'
→
NatCancelR
(
S
m
)
(
S
n
)
m'
n'
|
3
.
Proof
.
unfold
NatCancelR
,
NatCancelL
.
omeg
a
.
Qed
.
Proof
.
unfold
NatCancelR
,
NatCancelL
.
li
a
.
Qed
.
Instance
nat_cancel_leaf_S_else
m
n
m'
n'
:
NatCancelR
m
n
m'
n'
→
NatCancelR
m
(
S
n
)
m'
(
S
n'
)
|
4
.
Proof
.
unfold
NatCancelR
,
NatCancelL
.
omeg
a
.
Qed
.
Proof
.
unfold
NatCancelR
,
NatCancelL
.
li
a
.
Qed
.
(** The instance [nat_cancel_S_both] is redundant, but may reduce proof search
quite a bit, e.g. when canceling constants in constants. *)
Instance
nat_cancel_S_both
m
n
m'
n'
:
NatCancelL
m
n
m'
n'
→
NatCancelL
(
S
m
)
(
S
n
)
m'
n'
|
1
.
Proof
.
unfold
NatCancelL
.
omeg
a
.
Qed
.
Proof
.
unfold
NatCancelL
.
li
a
.
Qed
.
Instance
nat_cancel_plus
m1
m2
m1'
m2'
m1'm2'
n
n'
n''
:
NatCancelL
m1
n
m1'
n'
→
NatCancelL
m2
n'
m2'
n''
→
MakeNatPlus
m1'
m2'
m1'm2'
→
NatCancelL
(
m1
+
m2
)
n
m1'm2'
n''
|
2
.
Proof
.
unfold
NatCancelL
,
MakeNatPlus
.
omeg
a
.
Qed
.
Proof
.
unfold
NatCancelL
,
MakeNatPlus
.
li
a
.
Qed
.
Instance
nat_cancel_S
m
m'
m''
Sm'
n
n'
n''
:
NatCancelL
m
n
m'
n'
→
NatCancelR
1
n'
m''
n''
→
MakeNatS
m''
m'
Sm'
→
NatCancelL
(
S
m
)
n
Sm'
n''
|
3
.
Proof
.
unfold
NatCancelR
,
NatCancelL
,
MakeNatS
.
omeg
a
.
Qed
.
Proof
.
unfold
NatCancelR
,
NatCancelL
,
MakeNatS
.
li
a
.
Qed
.
End
nat_cancel
.
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