Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Jonas Kastberg
stdpp
Commits
0e155310
Commit
0e155310
authored
Jan 14, 2022
by
Robbert Krebbers
Browse files
Move `reverse` lemmas above `elem_of` ones.
parent
74d21e01
Changes
1
Hide whitespace changes
Inline
Sidebyside
theories/list.v
View file @
0e155310
...
...
@@ 846,6 +846,47 @@ Proof.
rewrite
list_inserts_cons
.
simpl
.
by
rewrite
IH
.
Qed
.
(** ** Properties of the [reverse] function *)
Lemma
reverse_nil
:
reverse
[]
=@{
list
A
}
[].
Proof
.
done
.
Qed
.
Lemma
reverse_singleton
x
:
reverse
[
x
]
=
[
x
].
Proof
.
done
.
Qed
.
Lemma
reverse_cons
l
x
:
reverse
(
x
::
l
)
=
reverse
l
++
[
x
].
Proof
.
unfold
reverse
.
by
rewrite
<!
rev_alt
.
Qed
.
Lemma
reverse_snoc
l
x
:
reverse
(
l
++
[
x
])
=
x
::
reverse
l
.
Proof
.
unfold
reverse
.
by
rewrite
<!
rev_alt
,
rev_unit
.
Qed
.
Lemma
reverse_app
l1
l2
:
reverse
(
l1
++
l2
)
=
reverse
l2
++
reverse
l1
.
Proof
.
unfold
reverse
.
rewrite
<!
rev_alt
.
apply
rev_app_distr
.
Qed
.
Lemma
reverse_length
l
:
length
(
reverse
l
)
=
length
l
.
Proof
.
unfold
reverse
.
rewrite
<!
rev_alt
.
apply
rev_length
.
Qed
.
Lemma
reverse_involutive
l
:
reverse
(
reverse
l
)
=
l
.
Proof
.
unfold
reverse
.
rewrite
<!
rev_alt
.
apply
rev_involutive
.
Qed
.
Lemma
reverse_lookup
l
i
:
i
<
length
l
→
reverse
l
!!
i
=
l
!!
(
length
l

S
i
).
Proof
.
revert
i
.
induction
l
as
[
x
l
IH
]
;
simpl
;
intros
i
Hi
;
[
done
].
rewrite
reverse_cons
.
destruct
(
decide
(
i
=
length
l
))
;
subst
.
+
by
rewrite
list_lookup_middle
,
Nat
.
sub_diag
by
by
rewrite
reverse_length
.
+
rewrite
lookup_app_l
by
(
rewrite
reverse_length
;
lia
).
rewrite
IH
by
lia
.
by
assert
(
length
l

i
=
S
(
length
l

S
i
))
as
>
by
lia
.
Qed
.
Lemma
reverse_lookup_Some
l
i
x
:
reverse
l
!!
i
=
Some
x
↔
l
!!
(
length
l

S
i
)
=
Some
x
∧
i
<
length
l
.
Proof
.
split
.

destruct
(
decide
(
i
<
length
l
))
;
[
by
rewrite
reverse_lookup
].
rewrite
lookup_ge_None_2
;
[
done
].
rewrite
reverse_length
.
lia
.

intros
[??].
by
rewrite
reverse_lookup
.
Qed
.
Global
Instance
:
Inj
(=)
(=)
(@
reverse
A
).
Proof
.
intros
l1
l2
Hl
.
by
rewrite
<(
reverse_involutive
l1
),
<(
reverse_involutive
l2
),
Hl
.
Qed
.
(** ** Properties of the [elem_of] predicate *)
Lemma
not_elem_of_nil
x
:
x
∉
[].
Proof
.
by
inversion
1
.
Qed
.
...
...
@@ 869,6 +910,17 @@ Lemma not_elem_of_app l1 l2 x : x ∉ l1 ++ l2 ↔ x ∉ l1 ∧ x ∉ l2.
Proof
.
rewrite
elem_of_app
.
tauto
.
Qed
.
Lemma
elem_of_list_singleton
x
y
:
x
∈
[
y
]
↔
x
=
y
.
Proof
.
rewrite
elem_of_cons
,
elem_of_nil
.
tauto
.
Qed
.
Lemma
elem_of_reverse_2
x
l
:
x
∈
l
→
x
∈
reverse
l
.
Proof
.
induction
1
;
rewrite
reverse_cons
,
elem_of_app
,
?elem_of_list_singleton
;
intuition
.
Qed
.
Lemma
elem_of_reverse
x
l
:
x
∈
reverse
l
↔
x
∈
l
.
Proof
.
split
;
auto
using
elem_of_reverse_2
.
intros
.
rewrite
<(
reverse_involutive
l
).
by
apply
elem_of_reverse_2
.
Qed
.
Lemma
elem_of_list_lookup_1
l
x
:
x
∈
l
→
∃
i
,
l
!!
i
=
Some
x
.
Proof
.
induction
1
as
[????
IH
]
;
[
by
exists
0
].
...
...
@@ 1064,57 +1116,6 @@ Section list_set.
Qed
.
End
list_set
.
(** ** Properties of the [reverse] function *)
Lemma
reverse_nil
:
reverse
[]
=@{
list
A
}
[].
Proof
.
done
.
Qed
.
Lemma
reverse_singleton
x
:
reverse
[
x
]
=
[
x
].
Proof
.
done
.
Qed
.
Lemma
reverse_cons
l
x
:
reverse
(
x
::
l
)
=
reverse
l
++
[
x
].
Proof
.
unfold
reverse
.
by
rewrite
<!
rev_alt
.
Qed
.
Lemma
reverse_snoc
l
x
:
reverse
(
l
++
[
x
])
=
x
::
reverse
l
.
Proof
.
unfold
reverse
.
by
rewrite
<!
rev_alt
,
rev_unit
.
Qed
.
Lemma
reverse_app
l1
l2
:
reverse
(
l1
++
l2
)
=
reverse
l2
++
reverse
l1
.
Proof
.
unfold
reverse
.
rewrite
<!
rev_alt
.
apply
rev_app_distr
.
Qed
.
Lemma
reverse_length
l
:
length
(
reverse
l
)
=
length
l
.
Proof
.
unfold
reverse
.
rewrite
<!
rev_alt
.
apply
rev_length
.
Qed
.
Lemma
reverse_involutive
l
:
reverse
(
reverse
l
)
=
l
.
Proof
.
unfold
reverse
.
rewrite
<!
rev_alt
.
apply
rev_involutive
.
Qed
.
Lemma
reverse_lookup
l
i
:
i
<
length
l
→
reverse
l
!!
i
=
l
!!
(
length
l

S
i
).
Proof
.
revert
i
.
induction
l
as
[
x
l
IH
]
;
simpl
;
intros
i
Hi
;
[
done
].
rewrite
reverse_cons
.
destruct
(
decide
(
i
=
length
l
))
;
subst
.
+
by
rewrite
list_lookup_middle
,
Nat
.
sub_diag
by
by
rewrite
reverse_length
.
+
rewrite
lookup_app_l
by
(
rewrite
reverse_length
;
lia
).
rewrite
IH
by
lia
.
by
assert
(
length
l

i
=
S
(
length
l

S
i
))
as
>
by
lia
.
Qed
.
Lemma
reverse_lookup_Some
l
i
x
:
reverse
l
!!
i
=
Some
x
↔
l
!!
(
length
l

S
i
)
=
Some
x
∧
i
<
length
l
.
Proof
.
split
.

destruct
(
decide
(
i
<
length
l
))
;
[
by
rewrite
reverse_lookup
].
rewrite
lookup_ge_None_2
;
[
done
].
rewrite
reverse_length
.
lia
.

intros
[??].
by
rewrite
reverse_lookup
.
Qed
.
Lemma
elem_of_reverse_2
x
l
:
x
∈
l
→
x
∈
reverse
l
.
Proof
.
induction
1
;
rewrite
reverse_cons
,
elem_of_app
,
?elem_of_list_singleton
;
intuition
.
Qed
.
Lemma
elem_of_reverse
x
l
:
x
∈
reverse
l
↔
x
∈
l
.
Proof
.
split
;
auto
using
elem_of_reverse_2
.
intros
.
rewrite
<(
reverse_involutive
l
).
by
apply
elem_of_reverse_2
.
Qed
.
Global
Instance
:
Inj
(=)
(=)
(@
reverse
A
).
Proof
.
intros
l1
l2
Hl
.
by
rewrite
<(
reverse_involutive
l1
),
<(
reverse_involutive
l2
),
Hl
.
Qed
.
(** ** Properties of the [last] function *)
Lemma
last_nil
:
last
[]
=@{
option
A
}
None
.
Proof
.
done
.
Qed
.
...
...
Write
Preview
Supports
Markdown
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