This file collects general purpose definitions and theorems on lists that
are not in the Coq standard library.
Require Import Permutation.
Require Export base decidable option numbers.
Arguments length {
_}
_.
Arguments cons {
_}
_ _.
Arguments app {
_}
_ _.
Arguments Permutation {
_}
_ _.
Arguments Forall_cons {
_}
_ _ _ _ _.
Notation Forall_nil_2 :=
Forall_nil.
Notation Forall_cons_2 :=
Forall_cons.
Notation tail :=
tl.
Notation take :=
firstn.
Notation drop :=
skipn.
Notation take_drop :=
firstn_skipn.
Arguments take {
_} !
_ !
_ /.
Arguments drop {
_} !
_ !
_ /.
Notation "(::)" :=
cons (
only parsing) :
C_scope.
Notation "(
x ::)" := (
cons x) (
only parsing) :
C_scope.
Notation "(::
l )" := (λ
x,
cons x l) (
only parsing) :
C_scope.
Notation "(++)" :=
app (
only parsing) :
C_scope.
Notation "(
l ++)" := (
app l) (
only parsing) :
C_scope.
Notation "(++
k )" := (λ
l,
app l k) (
only parsing) :
C_scope.
General definitions
Looking up, updating, and deleting elements of a list.
Instance list_lookup {
A} :
Lookup nat A (
list A) :=
fix go (
i :
nat) (
l :
list A) {
struct l} :
option A :=
match l with
| [] =>
None
|
x ::
l =>
match i with
| 0 =>
Some x
|
S i => @
lookup _ _ _ go i l
end
end.
Instance list_alter {
A} (
f :
A →
A) :
AlterD nat A (
list A)
f :=
fix go (
i :
nat) (
l :
list A) {
struct l} :=
match l with
| [] => []
|
x ::
l =>
match i with
| 0 =>
f x ::
l
|
S i =>
x :: @
alter _ _ _ f go i l
end
end.
Instance list_delete {
A} :
Delete nat (
list A) :=
fix go (
i :
nat) (
l :
list A) {
struct l} :
list A :=
match l with
| [] => []
|
x ::
l =>
match i with
| 0 =>
l
|
S i =>
x :: @
delete _ _ go i l
end
end.
Instance list_insert {
A} :
Insert nat A (
list A) := λ
i x,
alter (λ
_,
x)
i.
The function option_list converts an element of the option type into
a list.
Definition option_list {
A} :
option A →
list A :=
option_rect _ (λ
x, [
x]) [].
The function filter P l returns the list of elements of l that
satisfies P. The order remains unchanged.
Instance list_filter {
A} :
Filter A (
list A) :=
fix go P _ l :=
match l with
| [] => []
|
x ::
l =>
if decide (
P x)
then x :: @
filter _ _ (@
go)
_ _ l
else @
filter _ _ (@
go)
_ _ l
end.
The function replicate n x generates a list with length n of elements
with value x.
Fixpoint replicate {
A} (
n :
nat) (
x :
A) :
list A :=
match n with
| 0 => []
|
S n =>
x ::
replicate n x
end.
The function reverse l returns the elements of l in reverse order.
Definition reverse {
A} (
l :
list A) :
list A :=
rev_append l [].
The function resize n y l takes the first n elements of l in case
length l ≤ n, and otherwise appends elements with value x to l to obtain
a list of length n.
Fixpoint resize {
A} (
n :
nat) (
y :
A) (
l :
list A) :
list A :=
match l with
| [] =>
replicate n y
|
x ::
l =>
match n with
| 0 => []
|
S n =>
x ::
resize n y l
end
end.
Arguments resize {
_} !
_ _ !
_.
The predicate prefix_of holds if the first list is a prefix of the second.
The predicate suffix_of holds if the first list is a suffix of the second.
Definition prefix_of {
A} (
l1 l2 :
list A) :
Prop := ∃
k,
l2 =
l1 ++
k.
Definition suffix_of {
A} (
l1 l2 :
list A) :
Prop := ∃
k,
l2 =
k ++
l1.
Tactics on lists
Lemma cons_inv {
A} (
l1 l2 :
list A)
x1 x2 :
x1 ::
l1 =
x2 ::
l2 →
x1 =
x2 ∧
l1 =
l2.
Proof.
by injection 1. Qed.
The tactic discriminate_list_equality discharges goals containing
invalid list equalities as an assumption.
Tactic Notation "
discriminate_list_equality"
hyp(
H) :=
apply (
f_equal length)
in H;
repeat (
simpl in H ||
rewrite app_length in H);
exfalso;
lia.
Tactic Notation "
discriminate_list_equality" :=
repeat_on_hyps (
fun H =>
discriminate_list_equality H).
The tactic simplify_list_equality simplifies assumptions involving
equalities on lists.
Ltac simplify_list_equality :=
repeat
match goal with
|
H :
_ ::
_ =
_ ::
_ |-
_ =>
apply cons_inv in H;
destruct H
|
H :
_ ++
_ =
_ ++
_ |-
_ =>
first
[
apply app_inj_tail in H;
destruct H
|
apply app_inv_head in H
|
apply app_inv_tail in H ]
|
H : [?
x] !! ?
i =
Some ?
y |-
_ =>
destruct i; [
change (
Some x =
Some y)
in H|
discriminate]
|
_ =>
progress simplify_equality
|
H :
_ |-
_ =>
discriminate_list_equality H
end.
General theorems
Section general_properties.
Context {
A :
Type}.
Global Instance: ∀
x :
A,
Injective (=) (=) (
x ::).
Proof.
by injection 1. Qed.
Global Instance: ∀
l :
list A,
Injective (=) (=) (::
l).
Proof.
by injection 1. Qed.
Global Instance: ∀
k :
list A,
Injective (=) (=) (
k ++).
Proof.
intros ???. apply app_inv_head. Qed.
Global Instance: ∀
k :
list A,
Injective (=) (=) (++
k).
Proof.
intros ???. apply app_inv_tail. Qed.
Lemma app_inj (
l1 k1 l2 k2 :
list A) :
length l1 =
length k1 →
l1 ++
l2 =
k1 ++
k2 →
l1 =
k1 ∧
l2 =
k2.
Proof.
revert k1. induction l1; intros [|??]; naive_solver. Qed.
Lemma list_eq (
l1 l2 :
list A) : (∀
i,
l1 !!
i =
l2 !!
i) →
l1 =
l2.
Proof.
revert l2. induction l1; intros [|??] H.
* done.
* discriminate (H 0).
* discriminate (H 0).
* f_equal; [by injection (H 0) |].
apply IHl1. intro. apply (H (S _)).
Qed.
Lemma list_eq_nil (
l :
list A) : (∀
i,
l !!
i =
None) →
l =
nil.
Proof.
intros. by apply list_eq. Qed.
Global Instance list_eq_dec {
dec : ∀
x y :
A,
Decision (
x =
y)} : ∀
l k,
Decision (
l =
k) :=
list_eq_dec dec.
Definition list_singleton_dec (
l :
list A) : {
x |
l = [
x] } + {
length l ≠ 1 }.
Proof.
by refine (
match l with
| [x] => inleft (x ↾ _)
| _ => inright _
end).
Defined.
Lemma nil_or_length_pos (
l :
list A) :
l = [] ∨
length l ≠ 0.
Proof.
destruct l; simpl; auto with lia. Qed.
Lemma nil_length (
l :
list A) :
length l = 0 →
l = [].
Proof.
by destruct l. Qed.
Lemma lookup_nil i : @
nil A !!
i =
None.
Proof.
by destruct i. Qed.
Lemma lookup_tail (
l :
list A)
i :
tail l !!
i =
l !!
S i.
Proof.
by destruct l. Qed.
Lemma lookup_lt_length (
l :
list A)
i :
is_Some (
l !!
i) ↔
i <
length l.
Proof.
revert i. induction l.
* split; by inversion 1.
* intros [|?]; simpl.
+ split; eauto with arith.
+ by rewrite <-NPeano.Nat.succ_lt_mono.
Qed.
Lemma lookup_lt_length_1 (
l :
list A)
i :
is_Some (
l !!
i) →
i <
length l.
Proof.
apply lookup_lt_length. Qed.
Lemma lookup_lt_length_alt (
l :
list A)
i x :
l !!
i =
Some x →
i <
length l.
Proof.
intros Hl. by rewrite <-lookup_lt_length, Hl. Qed.
Lemma lookup_lt_length_2 (
l :
list A)
i :
i <
length l →
is_Some (
l !!
i).
Proof.
apply lookup_lt_length. Qed.
Lemma lookup_ge_length (
l :
list A)
i :
l !!
i =
None ↔
length l ≤
i.
Proof.
rewrite eq_None_not_Some, lookup_lt_length. lia. Qed.
Lemma lookup_ge_length_1 (
l :
list A)
i :
l !!
i =
None →
length l ≤
i.
Proof.
by rewrite lookup_ge_length. Qed.
Lemma lookup_ge_length_2 (
l :
list A)
i :
length l ≤
i →
l !!
i =
None.
Proof.
by rewrite lookup_ge_length. Qed.
Lemma list_eq_length_eq (
l1 l2 :
list A) :
length l2 =
length l1 →
(∀
i x y,
l1 !!
i =
Some x →
l2 !!
i =
Some y →
x =
y) →
l1 =
l2.
Proof.
intros Hlength Hlookup. apply list_eq. intros i.
destruct (l2 !! i) as [x|] eqn:E.
* feed inversion (lookup_lt_length_2 l1 i) as [y].
{ pose proof (lookup_lt_length_alt l2 i x E). lia. }
f_equal. eauto.
* rewrite lookup_ge_length in E |- *. lia.
Qed.
Lemma lookup_app_l (
l1 l2 :
list A)
i :
i <
length l1 →
(
l1 ++
l2) !!
i =
l1 !!
i.
Proof.
revert i. induction l1; intros [|?]; simpl; auto with lia. Qed.
Lemma lookup_app_l_Some (
l1 l2 :
list A)
i x :
l1 !!
i =
Some x →
(
l1 ++
l2) !!
i =
Some x.
Proof.
intros. rewrite lookup_app_l; eauto using lookup_lt_length_alt. Qed.
Lemma lookup_app_r (
l1 l2 :
list A)
i :
(
l1 ++
l2) !! (
length l1 +
i) =
l2 !!
i.
Proof.
revert i.
induction l1; intros [|i]; simpl in *; simplify_equality; auto.
Qed.
Lemma lookup_app_r_alt (
l1 l2 :
list A)
i :
length l1 ≤
i →
(
l1 ++
l2) !!
i =
l2 !! (
i -
length l1).
Proof.
intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
rewrite Hi at 1. by apply lookup_app_r.
Qed.
Lemma lookup_app_r_Some (
l1 l2 :
list A)
i x :
l2 !!
i =
Some x →
(
l1 ++
l2) !! (
length l1 +
i) =
Some x.
Proof.
by rewrite lookup_app_r. Qed.
Lemma lookup_app_r_Some_alt (
l1 l2 :
list A)
i x :
length l1 ≤
i →
l2 !! (
i -
length l1) =
Some x →
(
l1 ++
l2) !!
i =
Some x.
Proof.
intro. by rewrite lookup_app_r_alt. Qed.
Lemma lookup_app_inv (
l1 l2 :
list A)
i x :
(
l1 ++
l2) !!
i =
Some x →
l1 !!
i =
Some x ∨
l2 !! (
i -
length l1) =
Some x.
Proof.
revert i.
induction l1; intros [|i] ?; simpl in *; simplify_equality; auto.
Qed.
Lemma list_lookup_middle (
l1 l2 :
list A) (
x :
A) :
(
l1 ++
x ::
l2) !!
length l1 =
Some x.
Proof.
by induction l1; simpl. Qed.
Lemma alter_length (
f :
A →
A)
l i :
length (
alter f i l) =
length l.
Proof.
revert i. induction l; intros [|?]; simpl; auto with lia. Qed.
Lemma insert_length (
l :
list A)
i x :
length (<[
i:=
x]>
l) =
length l.
Proof.
apply alter_length. Qed.
Lemma list_lookup_alter (
f :
A →
A)
l i :
alter f i l !!
i =
f <$>
l !!
i.
Proof.
revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed.
Lemma list_lookup_alter_ne (
f :
A →
A)
l i j :
i ≠
j →
alter f i l !!
j =
l !!
j.
Proof.
revert i j. induction l; [done|].
intros [|i] [|j] ?; try done. apply (IHl i). congruence.
Qed.
Lemma list_lookup_insert (
l :
list A)
i x :
i <
length l →
<[
i:=
x]>
l !!
i =
Some x.
Proof.
intros Hi. unfold insert, list_insert.
rewrite list_lookup_alter.
by feed inversion (lookup_lt_length_2 l i).
Qed.
Lemma list_lookup_insert_ne (
l :
list A)
i j x :
i ≠
j → <[
i:=
x]>
l !!
j =
l !!
j.
Proof.
apply list_lookup_alter_ne. Qed.
Lemma list_lookup_other (
l :
list A)
i x :
length l ≠ 1 →
l !!
i =
Some x →
∃
j y,
j ≠
i ∧
l !!
j =
Some y.
Proof.
intros Hl Hi.
destruct i; destruct l as [|x0 [|x1 l]]; simpl in *; simplify_equality.
* by exists 1 x1.
* by exists 0 x0.
Qed.
Lemma alter_app_l (
f :
A →
A) (
l1 l2 :
list A)
i :
i <
length l1 →
alter f i (
l1 ++
l2) =
alter f i l1 ++
l2.
Proof.
revert i.
induction l1; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma alter_app_r (
f :
A →
A) (
l1 l2 :
list A)
i :
alter f (
length l1 +
i) (
l1 ++
l2) =
l1 ++
alter f i l2.
Proof.
revert i.
induction l1; intros [|?]; simpl in *; f_equal; auto.
Qed.
Lemma alter_app_r_alt (
f :
A →
A) (
l1 l2 :
list A)
i :
length l1 ≤
i →
alter f i (
l1 ++
l2) =
l1 ++
alter f (
i -
length l1)
l2.
Proof.
intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
rewrite Hi at 1. by apply alter_app_r.
Qed.
Lemma insert_app_l (
l1 l2 :
list A)
i x :
i <
length l1 →
<[
i:=
x]>(
l1 ++
l2) = <[
i:=
x]>
l1 ++
l2.
Proof.
apply alter_app_l. Qed.
Lemma insert_app_r (
l1 l2 :
list A)
i x :
<[
length l1 +
i:=
x]>(
l1 ++
l2) =
l1 ++ <[
i:=
x]>
l2.
Proof.
apply alter_app_r. Qed.
Lemma insert_app_r_alt (
l1 l2 :
list A)
i x :
length l1 ≤
i →
<[
i:=
x]>(
l1 ++
l2) =
l1 ++ <[
i -
length l1:=
x]>
l2.
Proof.
apply alter_app_r_alt. Qed.
Lemma insert_consecutive_length (
l :
list A)
i k :
length (
insert_consecutive i k l) =
length l.
Proof.
revert i. by induction k; intros; simpl; rewrite ?insert_length. Qed.
Lemma not_elem_of_nil (
x :
A) :
x ∉ [].
Proof.
by inversion 1. Qed.
Lemma elem_of_nil (
x :
A) :
x ∈ [] ↔
False.
Proof.
intuition. by destruct (not_elem_of_nil x). Qed.
Lemma elem_of_nil_inv (
l :
list A) : (∀
x,
x ∉
l) →
l = [].
Proof.
destruct l. done. by edestruct 1; constructor. Qed.
Lemma elem_of_cons (
l :
list A)
x y :
x ∈
y ::
l ↔
x =
y ∨
x ∈
l.
Proof.
split.
* inversion 1; subst. by left. by right.
* intros [?|?]; subst. by left. by right.
Qed.
Lemma not_elem_of_cons (
l :
list A)
x y :
x ∉
y ::
l ↔
x ≠
y ∧
x ∉
l.
Proof.
rewrite elem_of_cons. tauto. Qed.
Lemma elem_of_app (
l1 l2 :
list A)
x :
x ∈
l1 ++
l2 ↔
x ∈
l1 ∨
x ∈
l2.
Proof.
induction l1.
* split; [by right|]. intros [Hx|]; [|done].
by destruct (elem_of_nil x).
* simpl. rewrite !elem_of_cons, IHl1. tauto.
Qed.
Lemma not_elem_of_app (
l1 l2 :
list A)
x :
x ∉
l1 ++
l2 ↔
x ∉
l1 ∧
x ∉
l2.
Proof.
rewrite elem_of_app. tauto. Qed.
Lemma elem_of_list_singleton (
x y :
A) :
x ∈ [
y] ↔
x =
y.
Proof.
rewrite elem_of_cons, elem_of_nil. tauto. Qed.
Global Instance elem_of_list_permutation_proper (
x :
A) :
Proper (
Permutation ==>
iff) (
x ∈).
Proof.
induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
Lemma elem_of_list_split (
l :
list A)
x :
x ∈
l → ∃
l1 l2,
l =
l1 ++
x ::
l2.
Proof.
induction 1 as [x l|x y l ? [l1 [l2 ?]]].
* by eexists [], l.
* subst. by exists (y :: l1) l2.
Qed.
Global Instance elem_of_list_dec {
dec : ∀
x y :
A,
Decision (
x =
y)} :
∀ (
x :
A)
l,
Decision (
x ∈
l).
Proof.
intros x. refine (
fix go l :=
match l return Decision (x ∈ l) with
| [] => right (not_elem_of_nil _)
| y :: l => cast_if_or (decide_rel (=) x y) (go l)
end); clear go dec; subst; try (by constructor); by inversion 1.
Defined.
Lemma elem_of_list_lookup_1 (
l :
list A)
x :
x ∈
l → ∃
i,
l !!
i =
Some x.
Proof.
induction 1 as [|???? IH].
* by exists 0.
* destruct IH as [i ?]; auto. by exists (S i).
Qed.
Lemma elem_of_list_lookup_2 (
l :
list A)
i x :
l !!
i =
Some x →
x ∈
l.
Proof.
revert i. induction l; intros [|i] ?;
simpl; simplify_equality; constructor; eauto.
Qed.
Lemma elem_of_list_lookup (
l :
list A)
x :
x ∈
l ↔ ∃
i,
l !!
i =
Some x.
Proof.
firstorder eauto using
elem_of_list_lookup_1, elem_of_list_lookup_2.
Qed.
Lemma NoDup_nil :
NoDup (@
nil A) ↔
True.
Proof.
split; constructor. Qed.
Lemma NoDup_cons (
x :
A)
l :
NoDup (
x ::
l) ↔
x ∉
l ∧
NoDup l.
Proof.
split. by inversion 1. intros [??]. by constructor. Qed.
Lemma NoDup_cons_11 (
x :
A)
l :
NoDup (
x ::
l) →
x ∉
l.
Proof.
rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_cons_12 (
x :
A)
l :
NoDup (
x ::
l) →
NoDup l.
Proof.
rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_singleton (
x :
A) :
NoDup [
x].
Proof.
constructor. apply not_elem_of_nil. constructor. Qed.
Lemma NoDup_app (
l k :
list A) :
NoDup (
l ++
k) ↔
NoDup l ∧ (∀
x,
x ∈
l →
x ∉
k) ∧
NoDup k.
Proof.
induction l; simpl.
* rewrite NoDup_nil.
setoid_rewrite elem_of_nil. naive_solver.
* rewrite !NoDup_cons.
setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app.
naive_solver.
Qed.
Global Instance NoDup_proper:
Proper (
Permutation ==>
iff) (@
NoDup A).
Proof.
induction 1 as [|x l k Hlk IH | |].
* by rewrite !NoDup_nil.
* by rewrite !NoDup_cons, IH, Hlk.
* rewrite !NoDup_cons, !elem_of_cons. intuition.
* intuition.
Qed.
Lemma NoDup_Permutation (
l k :
list A) :
NoDup l →
NoDup k → (∀
x,
x ∈
l ↔
x ∈
k) →
Permutation l k.
Proof.
intros Hl. revert k. induction Hl as [|x l Hin ? IH].
* intros k _ Hk.
rewrite (elem_of_nil_inv k); [done |].
intros x. rewrite <-Hk, elem_of_nil. intros [].
* intros k Hk Hlk.
destruct (elem_of_list_split k x) as [l1 [l2 ?]]; subst.
{ rewrite <-Hlk. by constructor. }
rewrite <-Permutation_middle, NoDup_cons in Hk.
destruct Hk as [??].
apply Permutation_cons_app, IH; [done |].
intros y. specialize (Hlk y).
rewrite <-Permutation_middle, !elem_of_cons in Hlk.
naive_solver.
Qed.
Global Instance NoDup_dec {
dec : ∀
x y :
A,
Decision (
x =
y)} :
∀ (
l :
list A),
Decision (
NoDup l) :=
fix NoDup_dec l :=
match l return Decision (
NoDup l)
with
| [] =>
left NoDup_nil_2
|
x ::
l =>
match decide_rel (∈)
x l with
|
left Hin =>
right (λ
H,
NoDup_cons_11 _ _ H Hin)
|
right Hin =>
match NoDup_dec l with
|
left H =>
left (
NoDup_cons_2 _ _ Hin H)
|
right H =>
right (
H ∘
NoDup_cons_12 _ _)
end
end
end.
Section remove_dups.
Context `{!∀
x y :
A,
Decision (
x =
y)}.
Fixpoint remove_dups (
l :
list A) :
list A :=
match l with
| [] => []
|
x ::
l =>
if decide_rel (∈)
x l then remove_dups l else x ::
remove_dups l
end.
Lemma elem_of_remove_dups l x :
x ∈
remove_dups l ↔
x ∈
l.
Proof.
split; induction l; simpl; repeat case_decide;
rewrite ?elem_of_cons; intuition (simplify_equality; auto).
Qed.
Lemma remove_dups_nodup l :
NoDup (
remove_dups l).
Proof.
induction l; simpl; repeat case_decide; try constructor; auto.
by rewrite elem_of_remove_dups.
Qed.
End remove_dups.
Lemma elem_of_list_filter `{∀
x :
A,
Decision (
P x)}
l x :
x ∈
filter P l ↔
P x ∧
x ∈
l.
Proof.
unfold filter. induction l; simpl; repeat case_decide;
rewrite ?elem_of_nil, ?elem_of_cons; naive_solver.
Qed.
Lemma filter_nodup P `{∀
x :
A,
Decision (
P x)}
l :
NoDup l →
NoDup (
filter P l).
Proof.
unfold filter. induction 1; simpl; repeat case_decide;
rewrite ?NoDup_nil, ?NoDup_cons, ?elem_of_list_filter; tauto.
Qed.
Lemma reverse_nil :
reverse [] = @
nil A.
Proof.
done. Qed.
Lemma reverse_cons (
l :
list A)
x :
reverse (
x ::
l) =
reverse l ++ [
x].
Proof.
unfold reverse. by rewrite <-!rev_alt. Qed.
Lemma reverse_snoc (
l :
list A)
x :
reverse (
l ++ [
x]) =
x ::
reverse l.
Proof.
unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
Lemma reverse_app (
l1 l2 :
list A) :
reverse (
l1 ++
l2) =
reverse l2 ++
reverse l1.
Proof.
unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
Lemma reverse_length (
l :
list A) :
length (
reverse l) =
length l.
Proof.
unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
Lemma reverse_involutive (
l :
list A) :
reverse (
reverse l) =
l.
Proof.
unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed.
Lemma take_nil n :
take n (@
nil A) = [].
Proof.
by destruct n. Qed.
Lemma take_app (
l k :
list A) :
take (
length l) (
l ++
k) =
l.
Proof.
induction l; simpl; f_equal; auto. Qed.
Lemma take_app_alt (
l k :
list A)
n :
n =
length l →
take n (
l ++
k) =
l.
Proof.
intros Hn. by rewrite Hn, take_app. Qed.
Lemma take_app_le (
l k :
list A)
n :
n ≤
length l →
take n (
l ++
k) =
take n l.
Proof.
revert n;
induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma take_app_ge (
l k :
list A)
n :
length l ≤
n →
take n (
l ++
k) =
l ++
take (
n -
length l)
k.
Proof.
revert n;
induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma take_ge (
l :
list A)
n :
length l ≤
n →
take n l =
l.
Proof.
revert n.
induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma take_take (
l :
list A)
n m :
take n (
take m l) =
take (
min n m)
l.
Proof.
revert n m. induction l; intros [|?] [|?]; simpl; f_equal; auto. Qed.
Lemma take_idempotent (
l :
list A)
n :
take n (
take n l) =
take n l.
Proof.
by rewrite take_take, Min.min_idempotent. Qed.
Lemma take_length (
l :
list A)
n :
length (
take n l) =
min n (
length l).
Proof.
revert n. induction l; intros [|?]; simpl; f_equal; done. Qed.
Lemma take_length_alt (
l :
list A)
n :
n ≤
length l →
length (
take n l) =
n.
Proof.
rewrite take_length. apply Min.min_l. Qed.
Lemma lookup_take (
l :
list A)
n i :
i <
n →
take n l !!
i =
l !!
i.
Proof.
revert n i. induction l; intros [|n] i ?; trivial.
* auto with lia.
* destruct i; simpl; auto with arith.
Qed.
Lemma lookup_take_ge (
l :
list A)
n i :
n ≤
i →
take n l !!
i =
None.
Proof.
revert n i.
induction l; intros [|?] [|?] ?; simpl; auto with lia.
Qed.
Lemma take_alter (
f :
A →
A)
l n i :
n ≤
i →
take n (
alter f i l) =
take n l.
Proof.
intros. apply list_eq. intros j. destruct (le_lt_dec n j).
* by rewrite !lookup_take_ge.
* by rewrite !lookup_take, !list_lookup_alter_ne by lia.
Qed.
Lemma take_insert (
l :
list A)
n i x :
n ≤
i →
take n (<[
i:=
x]>
l) =
take n l.
Proof take_alter _ _ _ _.
Lemma drop_nil n :
drop n (@
nil A) = [].
Proof.
by destruct n. Qed.
Lemma drop_app (
l k :
list A) :
drop (
length l) (
l ++
k) =
k.
Proof.
induction l; simpl; f_equal; auto. Qed.
Lemma drop_app_alt (
l k :
list A)
n :
n =
length l →
drop n (
l ++
k) =
k.
Proof.
intros Hn. by rewrite Hn, drop_app. Qed.
Lemma drop_length (
l :
list A)
n :
length (
drop n l) =
length l -
n.
Proof.
revert n. by induction l; intros [|i]; simpl; f_equal.
Qed.
Lemma drop_all (
l :
list A) :
drop (
length l)
l = [].
Proof.
induction l; simpl; auto. Qed.
Lemma drop_all_alt (
l :
list A)
n :
n =
length l →
drop n l = [].
Proof.
intros. subst. by rewrite drop_all. Qed.
Lemma lookup_drop (
l :
list A)
n i :
drop n l !!
i =
l !! (
n +
i).
Proof.
revert n i. induction l; intros [|i] ?; simpl; auto. Qed.
Lemma drop_alter (
f :
A →
A)
l n i :
i <
n →
drop n (
alter f i l) =
drop n l.
Proof.
intros. apply list_eq. intros j.
by rewrite !lookup_drop, !list_lookup_alter_ne by lia.
Qed.
Lemma drop_insert (
l :
list A)
n i x :
i <
n →
drop n (<[
i:=
x]>
l) =
drop n l.
Proof drop_alter _ _ _ _.
Lemma replicate_length n (
x :
A) :
length (
replicate n x) =
n.
Proof.
induction n; simpl; auto. Qed.
Lemma lookup_replicate n (
x :
A)
i :
i <
n →
replicate n x !!
i =
Some x.
Proof.
revert i.
induction n; intros [|?]; naive_solver auto with lia.
Qed.
Lemma lookup_replicate_inv n (
x y :
A)
i :
replicate n x !!
i =
Some y →
y =
x ∧
i <
n.
Proof.
revert i.
induction n; intros [|?]; naive_solver auto with lia.
Qed.
Lemma replicate_plus n m (
x :
A) :
replicate (
n +
m)
x =
replicate n x ++
replicate m x.
Proof.
induction n; simpl; f_equal; auto. Qed.
Lemma take_replicate n m (
x :
A) :
take n (
replicate m x) =
replicate (
min n m)
x.
Proof.
revert m. by induction n; intros [|?]; simpl; f_equal. Qed.
Lemma take_replicate_plus n m (
x :
A) :
take n (
replicate (
n +
m)
x) =
replicate n x.
Proof.
by rewrite take_replicate, min_l by lia. Qed.
Lemma drop_replicate n m (
x :
A) :
drop n (
replicate m x) =
replicate (
m -
n)
x.
Proof.
revert m. by induction n; intros [|?]; simpl; f_equal. Qed.
Lemma drop_replicate_plus n m (
x :
A) :
drop n (
replicate (
n +
m)
x) =
replicate m x.
Proof.
rewrite drop_replicate. f_equal. lia. Qed.
Lemma resize_spec (
l :
list A)
n x :
resize n x l =
take n l ++
replicate (
n -
length l)
x.
Proof.
revert n.
induction l; intros [|?]; simpl; f_equal; auto.
Qed.
Lemma resize_0 (
l :
list A)
x :
resize 0
x l = [].
Proof.
by destruct l. Qed.
Lemma resize_nil n (
x :
A) :
resize n x [] =
replicate n x.
Proof.
rewrite resize_spec. rewrite take_nil. simpl. f_equal. lia. Qed.
Lemma resize_ge (
l :
list A)
n x :
length l ≤
n →
resize n x l =
l ++
replicate (
n -
length l)
x.
Proof.
intros. by rewrite resize_spec, take_ge. Qed.
Lemma resize_le (
l :
list A)
n x :
n ≤
length l →
resize n x l =
take n l.
Proof.
intros. rewrite resize_spec, (proj2 (NPeano.Nat.sub_0_le _ _)) by done.
simpl. by rewrite app_nil_r.
Qed.
Lemma resize_all (
l :
list A)
x :
resize (
length l)
x l =
l.
Proof.
intros. by rewrite resize_le, take_ge. Qed.
Lemma resize_all_alt (
l :
list A)
n x :
n =
length l →
resize n x l =
l.
Proof.
intros. subst. by rewrite resize_all. Qed.
Lemma resize_plus (
l :
list A)
n m x :
resize (
n +
m)
x l =
resize n x l ++
resize m x (
drop n l).
Proof.
revert n m.
induction l; intros [|?] [|?]; simpl; f_equal; auto.
* by rewrite plus_0_r, app_nil_r.
* by rewrite replicate_plus.
Qed.
Lemma resize_plus_eq (
l :
list A)
n m x :
length l =
n →
resize (
n +
m)
x l =
l ++
replicate m x.
Proof.
intros. subst.
by rewrite resize_plus, resize_all, drop_all, resize_nil.
Qed.
Lemma resize_app_le (
l1 l2 :
list A)
n x :
n ≤
length l1 →
resize n x (
l1 ++
l2) =
resize n x l1.
Proof.
intros.
by rewrite !resize_le, take_app_le by (rewrite ?app_length; lia).
Qed.
Lemma resize_app_ge (
l1 l2 :
list A)
n x :
length l1 ≤
n →
resize n x (
l1 ++
l2) =
l1 ++
resize (
n -
length l1)
x l2.
Proof.
intros.
rewrite !resize_spec, take_app_ge, app_assoc by done.
do 2 f_equal. rewrite app_length. lia.
Qed.
Lemma resize_length (
l :
list A)
n x :
length (
resize n x l) =
n.
Proof.
rewrite resize_spec, app_length, replicate_length, take_length. lia.
Qed.
Lemma resize_replicate (
x :
A)
n m :
resize n x (
replicate m x) =
replicate n x.
Proof.
revert m. induction n; intros [|?]; simpl; f_equal; auto. Qed.
Lemma resize_resize (
l :
list A)
n m x :
n ≤
m →
resize n x (
resize m x l) =
resize n x l.
Proof.
revert n m. induction l; simpl.
* intros. by rewrite !resize_nil, resize_replicate.
* intros [|?] [|?] ?; simpl; f_equal; auto with lia.
Qed.
Lemma resize_idempotent (
l :
list A)
n x :
resize n x (
resize n x l) =
resize n x l.
Proof.
by rewrite resize_resize. Qed.
Lemma resize_take_le (
l :
list A)
n m x :
n ≤
m →
resize n x (
take m l) =
resize n x l.
Proof.
revert n m.
induction l; intros [|?] [|?] ?; simpl; f_equal; auto with lia.
Qed.
Lemma resize_take_eq (
l :
list A)
n x :
resize n x (
take n l) =
resize n x l.
Proof.
by rewrite resize_take_le. Qed.
Lemma take_resize (
l :
list A)
n m x :
take n (
resize m x l) =
resize (
min n m)
x l.
Proof.
revert n m.
induction l; intros [|?] [|?]; simpl; f_equal; auto using take_replicate.
Qed.
Lemma take_resize_le (
l :
list A)
n m x :
n ≤
m →
take n (
resize m x l) =
resize n x l.
Proof.
intros. by rewrite take_resize, Min.min_l. Qed.
Lemma take_resize_eq (
l :
list A)
n x :
take n (
resize n x l) =
resize n x l.
Proof.
intros. by rewrite take_resize, Min.min_l. Qed.
Lemma take_length_resize (
l :
list A)
n x :
length l ≤
n →
take (
length l) (
resize n x l) =
l.
Proof.
intros. by rewrite take_resize_le, resize_all. Qed.
Lemma take_length_resize_alt (
l :
list A)
n m x :
m =
length l →
m ≤
n →
take m (
resize n x l) =
l.
Proof.
intros. subst. by apply take_length_resize. Qed.
Lemma take_resize_plus (
l :
list A)
n m x :
take n (
resize (
n +
m)
x l) =
resize n x l.
Proof.
by rewrite take_resize, min_l by lia. Qed.
Lemma drop_resize_le (
l :
list A)
n m x :
n ≤
m →
drop n (
resize m x l) =
resize (
m -
n)
x (
drop n l).
Proof.
revert n m. induction l; simpl.
* intros. by rewrite drop_nil, !resize_nil, drop_replicate.
* intros [|?] [|?] ?; simpl; try case_match; auto with lia.
Qed.
Lemma drop_resize_plus (
l :
list A)
n m x :
drop n (
resize (
n +
m)
x l) =
resize m x (
drop n l).
Proof.
rewrite drop_resize_le by lia. f_equal. lia. Qed.
Section Forall_Exists.
Context (
P :
A →
Prop).
Lemma Forall_forall l :
Forall P l ↔ ∀
x,
x ∈
l →
P x.
Proof.
split.
* induction 1; inversion 1; subst; auto.
* intros Hin. induction l; constructor.
+ apply Hin. constructor.
+ apply IHl. intros ??. apply Hin. by constructor.
Qed.
Lemma Forall_nil :
Forall P [] ↔
True.
Proof.
done. Qed.
Lemma Forall_cons_1 x l :
Forall P (
x ::
l) →
P x ∧
Forall P l.
Proof.
by inversion 1. Qed.
Lemma Forall_cons x l :
Forall P (
x ::
l) ↔
P x ∧
Forall P l.
Proof.
split. by inversion 1. intros [??]. by constructor. Qed.
Lemma Forall_singleton x :
Forall P [
x] ↔
P x.
Proof.
rewrite Forall_cons, Forall_nil; tauto. Qed.
Lemma Forall_app l1 l2 :
Forall P (
l1 ++
l2) ↔
Forall P l1 ∧
Forall P l2.
Proof.
split.
* induction l1; inversion 1; intuition.
* intros [H ?]. induction H; simpl; intuition.
Qed.
Lemma Forall_true l : (∀
x,
P x) →
Forall P l.
Proof.
induction l; auto. Qed.
Lemma Forall_impl l (
Q :
A →
Prop) :
Forall P l → (∀
x,
P x →
Q x) →
Forall Q l.
Proof.
intros H ?. induction H; auto. Defined.
Lemma Forall_delete l i :
Forall P l →
Forall P (
delete i l).
Proof.
intros H. revert i.
by induction H; intros [|i]; try constructor.
Qed.
Lemma Forall_lookup l :
Forall P l ↔ ∀
i x,
l !!
i =
Some x →
P x.
Proof.
rewrite Forall_forall.
setoid_rewrite elem_of_list_lookup.
naive_solver.
Qed.
Lemma Forall_lookup_1 l i x :
Forall P l →
l !!
i =
Some x →
P x.
Proof.
rewrite Forall_lookup. eauto. Qed.
Lemma Forall_alter f l i :
Forall P l →
(∀
x,
l !!
i =
Some x →
P x →
P (
f x)) →
Forall P (
alter f i l).
Proof.
intros Hl. revert i.
induction Hl; simpl; intros [|i]; constructor; auto.
Qed.
Lemma Forall_replicate n x :
P x →
Forall P (
replicate n x).
Proof.
induction n; simpl; constructor; auto. Qed.
Lemma Forall_replicate_eq n (
x :
A) :
Forall (=
x) (
replicate n x).
Proof.
induction n; simpl; constructor; auto. Qed.
Lemma Exists_exists l :
Exists P l ↔ ∃
x,
x ∈
l ∧
P x.
Proof.
split.
* induction 1 as [x|y ?? IH].
+ exists x. split. constructor. done.
+ destruct IH as [x [??]]. exists x. split. by constructor. done.
* intros [x [Hin ?]]. induction l.
+ by destruct (not_elem_of_nil x).
+ inversion Hin; subst. by left. right; auto.
Qed.
Lemma Exists_inv x l :
Exists P (
x ::
l) →
P x ∨
Exists P l.
Proof.
inversion 1; intuition trivial. Qed.
Lemma Exists_app l1 l2 :
Exists P (
l1 ++
l2) ↔
Exists P l1 ∨
Exists P l2.
Proof.
split.
* induction l1; inversion 1; intuition.
* intros [H|H].
+ induction H; simpl; intuition.
+ induction l1; simpl; intuition.
Qed.
Lemma Exists_not_Forall l :
Exists (
not ∘
P)
l → ¬
Forall P l.
Proof.
induction 1; inversion_clear 1; contradiction. Qed.
Lemma Forall_not_Exists l :
Forall (
not ∘
P)
l → ¬
Exists P l.
Proof.
induction 1; inversion_clear 1; contradiction. Qed.
Context {
dec : ∀
x,
Decision (
P x)}.
Fixpoint Forall_Exists_dec l : {
Forall P l} + {
Exists (
not ∘
P)
l}.
Proof.
refine (
match l with
| [] => left _
| x :: l => cast_if_and (dec x) (Forall_Exists_dec l)
end); clear Forall_Exists_dec; abstract intuition.
Defined.
Lemma not_Forall_Exists l : ¬
Forall P l →
Exists (
not ∘
P)
l.
Proof.
intro. destruct (Forall_Exists_dec l); intuition. Qed.
Global Instance Forall_dec l :
Decision (
Forall P l) :=
match Forall_Exists_dec l with
|
left H =>
left H
|
right H =>
right (
Exists_not_Forall _ H)
end.
Fixpoint Exists_Forall_dec l : {
Exists P l} + {
Forall (
not ∘
P)
l}.
Proof.
refine (
match l with
| [] => right _
| x :: l => cast_if_or (dec x) (Exists_Forall_dec l)
end); clear Exists_Forall_dec; abstract intuition.
Defined.
Lemma not_Exists_Forall l : ¬
Exists P l →
Forall (
not ∘
P)
l.
Proof.
intro. destruct (Exists_Forall_dec l); intuition. Qed.
Global Instance Exists_dec l :
Decision (
Exists P l) :=
match Exists_Forall_dec l with
|
left H =>
left H
|
right H =>
right (
Forall_not_Exists _ H)
end.
End Forall_Exists.
End general_properties.
Section Forall2.
Context {
A B} (
P :
A →
B →
Prop).
Lemma Forall2_nil_inv_l k :
Forall2 P []
k →
k = [].
Proof.
by inversion 1. Qed.
Lemma Forall2_nil_inv_r k :
Forall2 P k [] →
k = [].
Proof.
by inversion 1. Qed.
Lemma Forall2_cons_inv l1 l2 x1 x2 :
Forall2 P (
x1 ::
l1) (
x2 ::
l2) →
P x1 x2 ∧
Forall2 P l1 l2.
Proof.
by inversion 1. Qed.
Lemma Forall2_cons_inv_l l1 k x1 :
Forall2 P (
x1 ::
l1)
k → ∃
x2 l2,
P x1 x2 ∧
Forall2 P l1 l2 ∧
k =
x2 ::
l2.
Proof.
inversion 1; subst; eauto. Qed.
Lemma Forall2_cons_inv_r k l2 x2 :
Forall2 P k (
x2 ::
l2) → ∃
x1 l1,
P x1 x2 ∧
Forall2 P l1 l2 ∧
k =
x1 ::
l1.
Proof.
inversion 1; subst; eauto. Qed.
Lemma Forall2_cons_nil_inv l1 x1 :
Forall2 P (
x1 ::
l1) [] →
False.
Proof.
by inversion 1. Qed.
Lemma Forall2_nil_cons_inv l2 x2 :
Forall2 P [] (
x2 ::
l2) →
False.
Proof.
by inversion 1. Qed.
Lemma Forall2_flip l1 l2 :
Forall2 P l1 l2 ↔
Forall2 (
flip P)
l2 l1.
Proof.
split; induction 1; constructor; auto. Qed.
Lemma Forall2_length l1 l2 :
Forall2 P l1 l2 →
length l1 =
length l2.
Proof.
induction 1; simpl; auto. Qed.
Lemma Forall2_impl (
Q :
A →
B →
Prop)
l1 l2 :
Forall2 P l1 l2 → (∀
x y,
P x y →
Q x y) →
Forall2 Q l1 l2.
Proof.
intros H ?. induction H; auto. Defined.
Lemma Forall2_unique l k1 k2 :
Forall2 P l k1 →
Forall2 P l k2 →
(∀
x y1 y2,
P x y1 →
P x y2 →
y1 =
y2) →
k1 =
k2.
Proof.
intros H. revert k2.
induction H; inversion_clear 1; intros; f_equal; eauto.
Qed.
Lemma Forall2_Forall_l (
Q :
A →
Prop)
l k :
Forall2 P l k →
Forall (λ
y, ∀
x,
P x y →
Q x)
k →
Forall Q l.
Proof.
induction 1; inversion_clear 1; eauto. Qed.
Lemma Forall2_Forall_r (
Q :
B →
Prop)
l k :
Forall2 P l k →
Forall (λ
x, ∀
y,
P x y →
Q y)
l →
Forall Q k.
Proof.
induction 1; inversion_clear 1; eauto. Qed.
Lemma Forall2_lookup l1 l2 i x y :
Forall2 P l1 l2 →
l1 !!
i =
Some x →
l2 !!
i =
Some y →
P x y.
Proof.
intros H. revert i. induction H.
* discriminate.
* intros [|?] ??; simpl in *; simplify_equality; eauto.
Qed.
Lemma Forall2_lookup_l l1 l2 i x :
Forall2 P l1 l2 →
l1 !!
i =
Some x → ∃
y,
l2 !!
i =
Some y ∧
P x y.
Proof.
intros H. revert i. induction H.
* discriminate.
* intros [|?] ?; simpl in *; simplify_equality; eauto.
Qed.
Lemma Forall2_lookup_r l1 l2 i y :
Forall2 P l1 l2 →
l2 !!
i =
Some y → ∃
x,
l1 !!
i =
Some x ∧
P x y.
Proof.
intros H. revert i. induction H.
* discriminate.
* intros [|?] ?; simpl in *; simplify_equality; eauto.
Qed.
Lemma Forall2_alter_l f l1 l2 i :
Forall2 P l1 l2 →
(∀
x1 x2,
l1 !!
i =
Some x1 →
l2 !!
i =
Some x2 →
P x1 x2 →
P (
f x1)
x2) →
Forall2 P (
alter f i l1)
l2.
Proof.
intros Hl. revert i.
induction Hl; simpl; intros [|i]; constructor; auto.
Qed.
Lemma Forall2_alter_r f l1 l2 i :
Forall2 P l1 l2 →
(∀
x1 x2,
l1 !!
i =
Some x1 →
l2 !!
i =
Some x2 →
P x1 x2 →
P x1 (
f x2)) →
Forall2 P l1 (
alter f i l2).
Proof.
intros Hl. revert i.
induction Hl; simpl; intros [|i]; constructor; auto.
Qed.
Lemma Forall2_alter f g l1 l2 i :
Forall2 P l1 l2 →
(∀
x1 x2,
l1 !!
i =
Some x1 →
l2 !!
i =
Some x2 →
P x1 x2 →
P (
f x1) (
g x2)) →
Forall2 P (
alter f i l1) (
alter g i l2).
Proof.
intros Hl. revert i.
induction Hl; simpl; intros [|i]; constructor; auto.
Qed.
Lemma Forall2_replicate_l l n x :
Forall (
P x)
l →
length l =
n →
Forall2 P (
replicate n x)
l.
Proof.
intros Hl. revert n.
induction Hl; intros [|?] ?; simplify_equality; constructor; auto.
Qed.
Lemma Forall2_replicate_r l n x :
Forall (
flip P x)
l →
length l =
n →
Forall2 P l (
replicate n x).
Proof.
intros Hl. revert n.
induction Hl; intros [|?] ?; simplify_equality; constructor; auto.
Qed.
Lemma Forall2_replicate n x1 x2 :
P x1 x2 →
Forall2 P (
replicate n x1) (
replicate n x2).
Proof.
induction n; simpl; constructor; auto. Qed.
Lemma Forall2_take l1 l2 n :
Forall2 P l1 l2 →
Forall2 P (
take n l1) (
take n l2).
Proof.
intros Hl1l2. revert n.
induction Hl1l2; intros [|?]; simpl; auto.
Qed.
Lemma Forall2_drop l1 l2 n :
Forall2 P l1 l2 →
Forall2 P (
drop n l1) (
drop n l2).
Proof.
intros Hl1l2. revert n.
induction Hl1l2; intros [|?]; simpl; auto.
Qed.
Lemma Forall2_resize l1 l2 x1 x2 n :
P x1 x2 →
Forall2 P l1 l2 →
Forall2 P (
resize n x1 l1) (
resize n x2 l2).
Proof.
intros. rewrite !resize_spec, (Forall2_length l1 l2) by done.
auto using Forall2_app, Forall2_take, Forall2_replicate.
Qed.
Lemma Forall2_resize_ge_l l1 l2 x1 x2 n m :
(∀
x,
P x x2) →
n ≤
m →
Forall2 P (
resize n x1 l1)
l2 →
Forall2 P (
resize m x1 l1) (
resize m x2 l2).
Proof.
intros. assert (n = length l2).
{ by rewrite <-(Forall2_length (resize n x1 l1) l2), resize_length. }
rewrite (le_plus_minus n m) by done. subst.
rewrite !resize_plus, resize_all, drop_all, resize_nil.
apply Forall2_app; [done |].
apply Forall2_replicate_r; [| by rewrite resize_length].
by apply Forall_true.
Qed.
Lemma Forall2_resize_ge_r l1 l2 x1 x2 n m :
(∀
x3,
P x1 x3) →
n ≤
m →
Forall2 P l1 (
resize n x2 l2) →
Forall2 P (
resize m x1 l1) (
resize m x2 l2).
Proof.
intros. assert (n = length l1).
{ by rewrite (Forall2_length l1 (resize n x2 l2)), resize_length. }
rewrite (le_plus_minus n m) by done. subst.
rewrite !resize_plus, resize_all, drop_all, resize_nil.
apply Forall2_app; [done |].
apply Forall2_replicate_l; [| by rewrite resize_length].
by apply Forall_true.
Qed.
Lemma Forall2_trans {
C} (
Q :
B →
C →
Prop) (
R :
A →
C →
Prop)
l1 l2 l3 :
(∀
x1 x2 x3,
P x1 x2 →
Q x2 x3 →
R x1 x3) →
Forall2 P l1 l2 →
Forall2 Q l2 l3 →
Forall2 R l1 l3.
Proof.
intros ? Hl1l2. revert l3.
induction Hl1l2; inversion_clear 1; eauto.
Qed.
Lemma Forall2_Forall (
Q :
A →
A →
Prop)
l :
Forall (λ
x,
Q x x)
l →
Forall2 Q l l.
Proof.
induction 1; constructor; auto. Qed.
Global Instance Forall2_dec `{∀
x1 x2,
Decision (
P x1 x2)} :
∀
l1 l2,
Decision (
Forall2 P l1 l2).
Proof.
refine (
fix go l1 l2 : Decision (Forall2 P l1 l2) :=
match l1, l2 with
| [], [] => left _
| x1 :: l1, x2 :: l2 => cast_if_and (decide (P x1 x2)) (go l1 l2)
| _, _ => right _
end); clear go; abstract first [by constructor | by inversion 1].
Defined.
End Forall2.
Section Forall2_order.
Context {
A} (
R :
relation A).
Global Instance:
PreOrder R →
PreOrder (
Forall2 R).
Proof.
split.
* intros l. induction l; by constructor.
* intros ???. apply Forall2_trans. apply transitivity.
Qed.
Global Instance:
AntiSymmetric R →
AntiSymmetric (
Forall2 R).
Proof.
induction 2; inversion_clear 1; f_equal; auto. Qed.
End Forall2_order.
Ltac decompose_elem_of_list :=
repeat
match goal with
|
H : ?
x ∈ [] |-
_ =>
by destruct (
not_elem_of_nil x)
|
H :
_ ∈
_ ::
_ |-
_ =>
apply elem_of_cons in H;
destruct H
|
H :
_ ∈
_ ++
_ |-
_ =>
apply elem_of_app in H;
destruct H
end.
Ltac decompose_Forall :=
repeat
match goal with
|
H :
Forall _ [] |-
_ =>
clear H
|
H :
Forall _ (
_ ::
_) |-
_ =>
rewrite Forall_cons in H;
destruct H
|
H :
Forall _ (
_ ++
_) |-
_ =>
rewrite Forall_app in H;
destruct H
|
H :
Forall2 _ [] [] |-
_ =>
clear H
|
H :
Forall2 _ (
_ ::
_) [] |-
_ =>
destruct (
Forall2_cons_nil_inv _ _ _ H)
|
H :
Forall2 _ [] (
_ ::
_) |-
_ =>
destruct (
Forall2_nil_cons_inv _ _ _ H)
|
H :
Forall2 _ [] ?
l |-
_ =>
apply Forall2_nil_inv_l in H;
subst l
|
H :
Forall2 _ ?
l [] |-
_ =>
apply Forall2_nil_inv_r in H;
subst l
|
H :
Forall2 _ (
_ ::
_) (
_ ::
_) |-
_ =>
apply Forall2_cons_inv in H;
destruct H
|
H :
Forall2 _ (
_ ::
_) ?
l |-
_ =>
apply Forall2_cons_inv_l in H;
destruct H as (? & ? & ? & ? & ?);
subst l
|
H :
Forall2 _ ?
l (
_ ::
_) |-
_ =>
apply Forall2_cons_inv_r in H;
destruct H as (? & ? & ? & ? & ?);
subst l
end.
Theorems on the prefix and suffix predicates
Section prefix_postfix.
Context {
A :
Type}.
Global Instance:
PreOrder (@
prefix_of A).
Proof.
split.
* intros ?. eexists []. by rewrite app_nil_r.
* intros ??? [k1 ?] [k2 ?].
exists (k1 ++ k2). subst. by rewrite app_assoc.
Qed.
Lemma prefix_of_nil (
l :
list A) :
prefix_of []
l.
Proof.
by exists l. Qed.
Lemma prefix_of_nil_not x (
l :
list A) : ¬
prefix_of (
x ::
l) [].
Proof.
by intros [k E]. Qed.
Lemma prefix_of_cons x y (
l1 l2 :
list A) :
x =
y →
prefix_of l1 l2 →
prefix_of (
x ::
l1) (
y ::
l2).
Proof.
intros ? [k E]. exists k. by subst. Qed.
Lemma prefix_of_cons_inv_1 x y (
l1 l2 :
list A) :
prefix_of (
x ::
l1) (
y ::
l2) →
x =
y.
Proof.
intros [k E]. by injection E. Qed.
Lemma prefix_of_cons_inv_2 x y (
l1 l2 :
list A) :
prefix_of (
x ::
l1) (
y ::
l2) →
prefix_of l1 l2.
Proof.
intros [k E]. exists k. by injection E. Qed.
Lemma prefix_of_app_l (
l1 l2 l3 :
list A) :
prefix_of (
l1 ++
l3)
l2 →
prefix_of l1 l2.
Proof.
intros [k ?]. red. exists (l3 ++ k). subst. by rewrite <-app_assoc. Qed.
Lemma prefix_of_app_r (
l1 l2 l3 :
list A) :
prefix_of l1 l2 →
prefix_of l1 (
l2 ++
l3).
Proof.
intros [k ?]. exists (k ++ l3). subst. by rewrite app_assoc. Qed.
Global Instance:
PreOrder (@
suffix_of A).
Proof.
split.
* intros ?. by eexists [].
* intros ??? [k1 ?] [k2 ?].
exists (k2 ++ k1). subst. by rewrite app_assoc.
Qed.
Lemma prefix_suffix_reverse (
l1 l2 :
list A) :
prefix_of l1 l2 ↔
suffix_of (
reverse l1) (
reverse l2).
Proof.
split; intros [k E]; exists (reverse k).
* by rewrite E, reverse_app.
* by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
Qed.
Lemma suffix_prefix_reverse (
l1 l2 :
list A) :
suffix_of l1 l2 ↔
prefix_of (
reverse l1) (
reverse l2).
Proof.
by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.
Lemma suffix_of_nil (
l :
list A) :
suffix_of []
l.
Proof.
exists l. by rewrite app_nil_r. Qed.
Lemma suffix_of_nil_inv (
l :
list A) :
suffix_of l [] →
l = [].
Proof.
by intros [[|?] ?]; simplify_list_equality. Qed.
Lemma suffix_of_cons_nil_inv x (
l :
list A) : ¬
suffix_of (
x ::
l) [].
Proof.
by intros [[] ?]. Qed.
Lemma suffix_of_app (
l1 l2 k :
list A) :
suffix_of l1 l2 →
suffix_of (
l1 ++
k) (
l2 ++
k).
Proof.
intros [k' E]. exists k'. subst. by rewrite app_assoc. Qed.
Lemma suffix_of_snoc_inv_1 x y (
l1 l2 :
list A) :
suffix_of (
l1 ++ [
x]) (
l2 ++ [
y]) →
x =
y.
Proof.
rewrite suffix_prefix_reverse, !reverse_snoc.
by apply prefix_of_cons_inv_1.
Qed.
Lemma suffix_of_snoc_inv_2 x y (
l1 l2 :
list A) :
suffix_of (
l1 ++ [
x]) (
l2 ++ [
y]) →
suffix_of l1 l2.
Proof.
rewrite !suffix_prefix_reverse, !reverse_snoc.
by apply prefix_of_cons_inv_2.
Qed.
Lemma suffix_of_cons_l (
l1 l2 :
list A)
x :
suffix_of (
x ::
l1)
l2 →
suffix_of l1 l2.
Proof.
intros [k ?]. exists (k ++ [x]). subst. by rewrite <-app_assoc. Qed.
Lemma suffix_of_app_l (
l1 l2 l3 :
list A) :
suffix_of (
l3 ++
l1)
l2 →
suffix_of l1 l2.
Proof.
intros [k ?]. exists (k ++ l3). subst. by rewrite <-app_assoc. Qed.
Lemma suffix_of_cons_r (
l1 l2 :
list A)
x :
suffix_of l1 l2 →
suffix_of l1 (
x ::
l2).
Proof.
intros [k ?]. exists (x :: k). by subst. Qed.
Lemma suffix_of_app_r (
l1 l2 l3 :
list A) :
suffix_of l1 l2 →
suffix_of l1 (
l3 ++
l2).
Proof.
intros [k ?]. exists (l3 ++ k). subst. by rewrite app_assoc. Qed.
Lemma suffix_of_cons_inv (
l1 l2 :
list A)
x y :
suffix_of (
x ::
l1) (
y ::
l2) →
x ::
l1 =
y ::
l2 ∨
suffix_of (
x ::
l1)
l2.
Proof.
intros [[|? k] E].
* by left.
* right. simplify_equality. by apply suffix_of_app_r.
Qed.
Lemma suffix_of_cons_not x (
l :
list A) : ¬
suffix_of (
x ::
l)
l.
Proof.
intros [??]. discriminate_list_equality. Qed.
Context `{∀
x y :
A,
Decision (
x =
y)}.
Fixpoint strip_prefix (
l1 l2 :
list A) :
list A * (
list A *
list A) :=
match l1,
l2 with
| [],
l2 => ([], ([],
l2))
|
l1, [] => ([], (
l1, []))
|
x ::
l1,
y ::
l2 =>
if decide_rel (=)
x y
then fst_map (
x ::) (
strip_prefix l1 l2)
else ([], (
x ::
l1,
y ::
l2))
end.
Global Instance prefix_of_dec: ∀
l1 l2 :
list A,
Decision (
prefix_of l1 l2) :=
fix go l1 l2 :=
match l1,
l2 return {
prefix_of l1 l2 } + { ¬
prefix_of l1 l2 }
with
| [],
_ =>
left (
prefix_of_nil _)
|
_, [] =>
right (
prefix_of_nil_not _ _)
|
x ::
l1,
y ::
l2 =>
match decide_rel (=)
x y with
|
left Exy =>
match go l1 l2 with
|
left Hl1l2 =>
left (
prefix_of_cons _ _ _ _ Exy Hl1l2)
|
right Hl1l2 =>
right (
Hl1l2 ∘
prefix_of_cons_inv_2 _ _ _ _)
end
|
right Exy =>
right (
Exy ∘
prefix_of_cons_inv_1 _ _ _ _)
end
end.
Global Instance suffix_of_dec (
l1 l2 :
list A) :
Decision (
suffix_of l1 l2).
Proof.
refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
abstract (by rewrite suffix_prefix_reverse).
Defined.
End prefix_postfix.
The simplify_suffix_of tactic removes suffix_of hypotheses that are
tautologies, and simplifies suffix_of hypotheses involving (::) and
(++).
Ltac simplify_suffix_of :=
repeat
match goal with
|
H :
suffix_of (
_ ::
_)
_ |-
_ =>
destruct (
suffix_of_cons_not _ _ H)
|
H :
suffix_of (
_ ::
_) [] |-
_ =>
apply suffix_of_nil_inv in H
|
H :
suffix_of (
_ ::
_) (
_ ::
_) |-
_ =>
destruct (
suffix_of_cons_inv _ _ _ _ H);
clear H
|
H :
suffix_of ?
x ?
x |-
_ =>
clear H
|
H :
suffix_of ?
x (
_ :: ?
x) |-
_ =>
clear H
|
H :
suffix_of ?
x (
_ ++ ?
x) |-
_ =>
clear H
|
_ =>
progress simplify_equality
end.
The solve_suffix_of tactic tries to solve goals involving suffix_of. It
uses simplify_suffix_of to simplify hypotheses and tries to solve suffix_of
conclusions. This tactic either fails or proves the goal.
Ltac solve_suffix_of :=
solve [
intuition (
repeat
match goal with
|
_ =>
done
|
_ =>
progress simplify_suffix_of
| |-
suffix_of []
_ =>
apply suffix_of_nil
| |-
suffix_of _ _ =>
reflexivity
| |-
suffix_of _ (
_ ::
_) =>
apply suffix_of_cons_r
| |-
suffix_of _ (
_ ++
_) =>
apply suffix_of_app_r
|
H :
suffix_of _ _ →
False |-
_ =>
destruct H
end)].
Hint Extern 0 (
PropHolds (
suffix_of _ _)) =>
unfold PropHolds;
solve_suffix_of :
typeclass_instances.
Folding lists
Notation foldr :=
fold_right.
Notation foldr_app :=
fold_right_app.
Lemma foldr_permutation {
A B} (
R :
relation B)
`{!
Equivalence R}
(
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))) :
Proper (
Permutation ==>
R) (
foldr f b).
Proof.
induction 1; simpl.
* done.
* by f_equiv.
* apply Hf.
* etransitivity; eauto.
Qed.
We redefine foldl with the arguments in the same order as in Haskell.
Definition foldl {
A B} (
f :
A →
B →
A) :
A →
list B →
A :=
fix go a l :=
match l with
| [] =>
a
|
x ::
l =>
go (
f a x)
l
end.
Lemma foldl_app {
A B} (
f :
A →
B →
A) (
l k :
list B) (
a :
A) :
foldl f a (
l ++
k) =
foldl f (
foldl f a l)
k.
Proof.
revert a. induction l; simpl; auto. Qed.
Monadic operations
Instance list_ret:
MRet list := λ
A x,
x :: @
nil A.
Instance list_fmap {
A B} (
f :
A →
B) :
FMapD list f :=
fix go (
l :
list A) :=
match l with
| [] => []
|
x ::
l =>
f x :: @
fmap _ _ _ f go l
end.
Instance list_bind {
A B} (
f :
A →
list B) :
MBindD list f :=
fix go (
l :
list A) :=
match l with
| [] => []
|
x ::
l =>
f x ++ @
mbind _ _ _ f go l
end.
Instance list_join:
MJoin list :=
fix go A (
ls :
list (
list A)) :
list A :=
match ls with
| [] => []
|
l ::
ls =>
l ++ @
mjoin _ go _ ls
end.
Definition mapM `{!
MBind M} `{!
MRet M} {
A B}
(
f :
A →
M B) :
list A →
M (
list B) :=
fix go l :=
match l with
| [] =>
mret []
|
x ::
l =>
y ←
f x;
k ←
go l;
mret (
y ::
k)
end.
Section list_fmap.
Context {
A B :
Type} (
f :
A →
B).
Lemma list_fmap_compose {
C} (
g :
B →
C)
l :
g ∘
f <$>
l =
g <$>
f <$>
l.
Proof.
induction l; simpl; f_equal; auto. Qed.
Lemma list_fmap_ext (
g :
A →
B) (
l :
list A) :
(∀
x,
f x =
g x) →
fmap f l =
fmap g l.
Proof.
intro. induction l; simpl; f_equal; auto. Qed.
Lemma list_fmap_ext_alt (
g :
A →
B) (
l :
list A) :
Forall (λ
x,
f x =
g x)
l ↔
fmap f l =
fmap g l.
Proof.
split.
* induction 1; simpl; f_equal; auto.
* induction l; simpl; constructor; simplify_equality; auto.
Qed.
Global Instance:
Injective (=) (=)
f →
Injective (=) (=) (
fmap f).
Proof.
intros ? l1. induction l1 as [|x l1 IH].
* by intros [|??].
* intros [|??]; simpl; intros; f_equal; simplify_equality; auto.
Qed.
Lemma fmap_app l1 l2 :
f <$>
l1 ++
l2 = (
f <$>
l1) ++ (
f <$>
l2).
Proof.
induction l1; simpl; by f_equal. Qed.
Lemma fmap_cons_inv y l k :
f <$>
l =
y ::
k → ∃
x l',
y =
f x ∧
l =
x ::
l'.
Proof.
intros. destruct l; simpl; simplify_equality; eauto. Qed.
Lemma fmap_app_inv l k1 k2 :
f <$>
l =
k1 ++
k2 → ∃
l1 l2,
k1 =
f <$>
l1 ∧
k2 =
f <$>
l2 ∧
l =
l1 ++
l2.
Proof.
revert l. induction k1 as [|y k1 IH]; simpl.
* intros l ?. by eexists [], l.
* intros [|x l] ?; simpl; simplify_equality.
destruct (IH l) as [l1 [l2 [? [??]]]]; subst; [done |].
by exists (x :: l1) l2.
Qed.
Lemma fmap_length l :
length (
f <$>
l) =
length l.
Proof.
induction l; simpl; by f_equal. Qed.
Lemma fmap_reverse l :
f <$>
reverse l =
reverse (
f <$>
l).
Proof.
induction l; simpl; [done |].
by rewrite !reverse_cons, fmap_app, IHl.
Qed.
Lemma fmap_replicate n x :
f <$>
replicate n x =
replicate n (
f x).
Proof.
induction n; simpl; f_equal; auto. Qed.
Lemma list_lookup_fmap l i : (
f <$>
l) !!
i =
f <$> (
l !!
i).
Proof.
revert i. induction l; by intros [|]. Qed.
Lemma list_lookup_fmap_inv l i x :
(
f <$>
l) !!
i =
Some x → ∃
y,
x =
f y ∧
l !!
i =
Some y.
Proof.
intros Hi. rewrite list_lookup_fmap in Hi.
destruct (l !! i) eqn:?; simplify_equality; eauto.
Qed.
Lemma list_alter_fmap (
g :
A →
A) (
h :
B →
B)
l i :
Forall (λ
x,
f (
g x) =
h (
f x))
l →
f <$>
alter g i l =
alter h i (
f <$>
l).
Proof.
intros Hl. revert i.
induction Hl; intros [|i]; simpl; f_equal; auto.
Qed.
Lemma elem_of_list_fmap_1 l x :
x ∈
l →
f x ∈
f <$>
l.
Proof.
induction 1; simpl; rewrite elem_of_cons; intuition. Qed.
Lemma elem_of_list_fmap_1_alt l x y :
x ∈
l →
y =
f x →
y ∈
f <$>
l.
Proof.
intros. subst. by apply elem_of_list_fmap_1. Qed.
Lemma elem_of_list_fmap_2 l x :
x ∈
f <$>
l → ∃
y,
x =
f y ∧
y ∈
l.
Proof.
induction l as [|y l IH]; simpl; intros; decompose_elem_of_list.
+ exists y. split; [done | by left].
+ destruct IH as [z [??]]. done. exists z. split; [done | by right].
Qed.
Lemma elem_of_list_fmap l x :
x ∈
f <$>
l ↔ ∃
y,
x =
f y ∧
y ∈
l.
Proof.
firstorder eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2.
Qed.
Lemma NoDup_fmap_1 (
l :
list A) :
NoDup (
f <$>
l) →
NoDup l.
Proof.
induction l; simpl; inversion_clear 1; constructor; auto.
rewrite elem_of_list_fmap in *. naive_solver.
Qed.
Lemma NoDup_fmap_2 `{!
Injective (=) (=)
f} (
l :
list A) :
NoDup l →
NoDup (
f <$>
l).
Proof.
induction 1; simpl; constructor; trivial.
rewrite elem_of_list_fmap. intros [y [Hxy ?]].
apply (injective f) in Hxy. by subst.
Qed.
Lemma NoDup_fmap `{!
Injective (=) (=)
f} (
l :
list A) :
NoDup (
f <$>
l) ↔
NoDup l.
Proof.
split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.
Global Instance fmap_Permutation_proper:
Proper (
Permutation ==>
Permutation) (
fmap f).
Proof.
induction 1; simpl; econstructor; eauto. Qed.
Lemma Forall_fmap (
l :
list A) (
P :
B →
Prop) :
Forall P (
f <$>
l) ↔
Forall (
P ∘
f)
l.
Proof.
split; induction l; inversion_clear 1; constructor; auto.
Qed.
Lemma Forall2_fmap_l {
C} (
P :
B →
C →
Prop)
l1 l2 :
Forall2 P (
f <$>
l1)
l2 ↔
Forall2 (
P ∘
f)
l1 l2.
Proof.
split; revert l2; induction l1; inversion_clear 1; constructor; auto.
Qed.
Lemma Forall2_fmap_r {
C} (
P :
C →
B →
Prop)
l1 l2 :
Forall2 P l1 (
f <$>
l2) ↔
Forall2 (λ
x,
P x ∘
f)
l1 l2.
Proof.
split; revert l1; induction l2; inversion_clear 1; constructor; auto.
Qed.
Lemma Forall2_fmap_1 {
C D} (
g :
C →
D) (
P :
B →
D →
Prop)
l1 l2 :
Forall2 P (
f <$>
l1) (
g <$>
l2) →
Forall2 (λ
x1 x2,
P (
f x1) (
g x2))
l1 l2.
Proof.
revert l2; induction l1; intros [|??]; inversion_clear 1; auto. Qed.
Lemma Forall2_fmap_2 {
C D} (
g :
C →
D) (
P :
B →
D →
Prop)
l1 l2 :
Forall2 (λ
x1 x2,
P (
f x1) (
g x2))
l1 l2 →
Forall2 P (
f <$>
l1) (
g <$>
l2).
Proof.
induction 1; simpl; auto. Qed.
Lemma Forall2_fmap {
C D} (
g :
C →
D) (
P :
B →
D →
Prop)
l1 l2 :
Forall2 P (
f <$>
l1) (
g <$>
l2) ↔
Forall2 (λ
x1 x2,
P (
f x1) (
g x2))
l1 l2.
Proof.
split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed.
Lemma mapM_fmap_Some (
g :
B →
option A) (
l :
list A) :
(∀
x,
g (
f x) =
Some x) →
mapM g (
f <$>
l) =
Some l.
Proof.
intros. by induction l; simpl; simplify_option_equality. Qed.
Lemma mapM_fmap_Some_inv (
g :
B →
option A) (
l :
list A) (
k :
list B) :
(∀
x y,
g y =
Some x →
y =
f x) →
mapM g k =
Some l →
k =
f <$>
l.
Proof.
intros Hgf. revert l; induction k as [|y k]; intros [|x l] ?;
simplify_option_equality; f_equiv; eauto.
Qed.
Lemma mapM_Some (
g :
B →
option A)
l k :
Forall2 (λ
x y,
g x =
Some y)
l k →
mapM g l =
Some k.
Proof.
by induction 1; simplify_option_equality. Qed.
Lemma Forall2_impl_mapM (
P :
B →
A →
Prop) (
g :
B →
option A)
l k :
Forall (λ
x, ∀
y,
g x =
Some y →
P x y)
l →
mapM g l =
Some k →
Forall2 P l k.
Proof.
intros Hl. revert k. induction Hl; intros [|??] ?;
simplify_option_equality; eauto.
Qed.
End list_fmap.
Lemma NoDup_fmap_fst {
A B} (
l :
list (
A *
B)) :
(∀
x y1 y2, (
x,
y1) ∈
l → (
x,
y2) ∈
l →
y1 =
y2) →
NoDup l →
NoDup (
fst <$>
l).
Proof.
intros Hunique.
induction 1 as [|[x1 y1] l Hin Hnodup IH]; simpl; constructor.
* rewrite elem_of_list_fmap.
intros [[x2 y2] [??]]; simpl in *; subst. destruct Hin.
rewrite (Hunique x2 y1 y2); rewrite ?elem_of_cons; auto.
* apply IH. intros.
eapply Hunique; rewrite ?elem_of_cons; eauto.
Qed.
Section list_bind.
Context {
A B :
Type} (
f :
A →
list B).
Lemma bind_app (
l1 l2 :
list A) :
(
l1 ++
l2) ≫=
f = (
l1 ≫=
f) ++ (
l2 ≫=
f).
Proof.
induction l1; simpl; [done|].
by rewrite <-app_assoc, IHl1.
Qed.
Lemma elem_of_list_bind (
x :
B) (
l :
list A) :
x ∈
l ≫=
f ↔ ∃
y,
x ∈
f y ∧
y ∈
l.
Proof.
split.
* induction l as [|y l IH]; simpl; intros; decompose_elem_of_list.
+ exists y. split; [done | by left].
+ destruct IH as [z [??]]. done.
exists z. split; [done | by right].
* intros [y [Hx Hy]].
induction Hy; simpl; rewrite elem_of_app; intuition.
Qed.
Lemma Forall2_bind {
C D} (
g :
C →
list D) (
P :
B →
D →
Prop)
l1 l2 :
Forall2 (λ
x1 x2,
Forall2 P (
f x1) (
g x2))
l1 l2 →
Forall2 P (
l1 ≫=
f) (
l2 ≫=
g).
Proof.
induction 1; simpl; auto using Forall2_app. Qed.
End list_bind.
Section list_ret_join.
Context {
A :
Type}.
Lemma list_join_bind (
ls :
list (
list A)) :
mjoin ls =
ls ≫=
id.
Proof.
induction ls; simpl; f_equal; auto. Qed.
Lemma elem_of_list_ret (
x y :
A) :
x ∈ @
mret list _ A y ↔
x =
y.
Proof.
apply elem_of_list_singleton. Qed.
Lemma elem_of_list_join (
x :
A) (
ls :
list (
list A)) :
x ∈
mjoin ls ↔ ∃
l,
x ∈
l ∧
l ∈
ls.
Proof.
by rewrite list_join_bind, elem_of_list_bind. Qed.
Lemma join_nil (
ls :
list (
list A)) :
mjoin ls = [] ↔
Forall (= [])
ls.
Proof.
split.
* by induction ls as [|[|??] ?]; constructor; auto.
* by induction 1 as [|[|??] ?].
Qed.
Lemma join_nil_1 (
ls :
list (
list A)) :
mjoin ls = [] →
Forall (= [])
ls.
Proof.
by rewrite join_nil. Qed.
Lemma join_nil_2 (
ls :
list (
list A)) :
Forall (= [])
ls →
mjoin ls = [].
Proof.
by rewrite join_nil. Qed.
Lemma join_length (
ls :
list (
list A)) :
length (
mjoin ls) =
foldr (
plus ∘
length) 0
ls.
Proof.
by induction ls; simpl; rewrite ?app_length; f_equal. Qed.
Lemma join_length_same (
ls :
list (
list A))
n :
Forall (λ
l,
length l =
n)
ls →
length (
mjoin ls) =
length ls *
n.
Proof.
rewrite join_length. by induction 1; simpl; f_equal. Qed.
Lemma lookup_join_same_length (
ls :
list (
list A))
n i :
n ≠ 0 →
Forall (λ
l,
length l =
n)
ls →
mjoin ls !!
i =
ls !! (
i `
div`
n) ≫= (!! (
i `
mod`
n)).
Proof.
intros Hn Hls. revert i.
induction Hls as [|l ls ? Hls IH]; simpl; [done |]. intros i.
destruct (decide (i < n)) as [Hin|Hin].
* rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
simpl. rewrite lookup_app_l; auto with lia.
* replace i with ((i - n) + 1 * n) by lia.
rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
replace (i - n + 1 * n) with i by lia.
rewrite (plus_comm _ 1), lookup_app_r_alt, IH by lia.
by subst.
Qed.
Lemma alter_join_same_length f (
ls :
list (
list A))
n i :
n ≠ 0 →
Forall (λ
l,
length l =
n)
ls →
alter f i (
mjoin ls) =
mjoin (
alter (
alter f (
i `
mod`
n)) (
i `
div`
n)
ls).
Proof.
intros Hn Hls. revert i.
induction Hls as [|l ls ? Hls IH]; simpl; [done |]. intros i.
destruct (decide (i < n)) as [Hin|Hin].
* rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
simpl. rewrite alter_app_l; auto with lia.
* replace i with ((i - n) + 1 * n) by lia.
rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
replace (i - n + 1 * n) with i by lia.
rewrite (plus_comm _ 1), alter_app_r_alt, IH by lia.
by subst.
Qed.
Lemma insert_join_same_length (
ls :
list (
list A))
n i x :
n ≠ 0 →
Forall (λ
l,
length l =
n)
ls →
<[
i:=
x]>(
mjoin ls) =
mjoin (
alter <[
i `
mod`
n:=
x]> (
i `
div`
n)
ls).
Proof.
apply alter_join_same_length. Qed.
Lemma Forall2_join {
B} (
P :
A →
B →
Prop)
ls1 ls2 :
Forall2 (
Forall2 P)
ls1 ls2 →
Forall2 P (
mjoin ls1) (
mjoin ls2).
Proof.
induction 1; simpl; auto using Forall2_app. Qed.
End list_ret_join.
Ltac simplify_list_fmap_equality :=
repeat
match goal with
|
_ =>
progress simplify_equality
|
H :
_ <$>
_ =
_ ::
_ |-
_ =>
apply fmap_cons_inv in H;
destruct H as [? [? [??]]]
|
H :
_ ::
_ =
_ <$>
_ |-
_ =>
symmetry in H
|
H :
_ <$>
_ =
_ ++
_ |-
_ =>
apply fmap_app_inv in H;
destruct H as [? [? [? [??]]]]
|
H :
_ ++
_ =
_ <$>
_ |-
_ =>
symmetry in H
end.
Indexed folds and maps
We define stronger variants of map and fold that also take the index of the
element into account.
Definition imap_go {
A B} (
f :
nat →
A →
B) :
nat →
list A →
list B :=
fix go (
n :
nat) (
l :
list A) :=
match l with
| [] => []
|
x ::
l =>
f n x ::
go (
S n)
l
end.
Definition imap {
A B} (
f :
nat →
A →
B) :
list A →
list B :=
imap_go f 0.
Definition ifoldr {
A B} (
f :
nat →
B →
A →
A)
(
a :
nat →
A) :
nat →
list B →
A :=
fix go (
n :
nat) (
l :
list B) :
A :=
match l with
|
nil =>
a n
|
b ::
l =>
f n b (
go (
S n)
l)
end.
Lemma ifoldr_app {
A B} (
f :
nat →
B →
A →
A) (
a :
nat →
A)
(
l1 l2 :
list B)
n :
ifoldr f a n (
l1 ++
l2) =
ifoldr f (λ
n,
ifoldr f a n l2)
n l1.
Proof.
revert n a. induction l1 as [| b l1 IH ]; intros; simpl; f_equal; auto.
Qed.
Lists of the same length
The same_length view allows convenient induction over two lists with the
same length.
Section same_length.
Context {
A B :
Type}.
Inductive same_length :
list A →
list B →
Prop :=
|
same_length_nil :
same_length [] []
|
same_length_cons x y l k :
same_length l k →
same_length (
x ::
l) (
y ::
k).
Lemma same_length_length_1 l k :
same_length l k →
length l =
length k.
Proof.
induction 1; simpl; auto. Qed.
Lemma same_length_length_2 l k :
length l =
length k →
same_length l k.
Proof.
revert k. induction l; intros [|??]; try discriminate;
constructor; auto with arith.
Qed.
Lemma same_length_length l k :
same_length l k ↔
length l =
length k.
Proof.
split; auto using same_length_length_1, same_length_length_2. Qed.
Lemma same_length_lookup l k i :
same_length l k →
is_Some (
l !!
i) →
is_Some (
k !!
i).
Proof.
rewrite same_length_length.
setoid_rewrite lookup_lt_length.
intros E. by rewrite E.
Qed.
Lemma Forall2_same_length (
P :
A →
B →
Prop)
l1 l2 :
Forall2 P l1 l2 →
same_length l1 l2.
Proof.
intro. eapply same_length_length, Forall2_length; eauto. Qed.
Lemma Forall2_app_inv (
P :
A →
B →
Prop)
l1 l2 k1 k2 :
same_length l1 k1 →
Forall2 P (
l1 ++
l2) (
k1 ++
k2) →
Forall2 P l2 k2.
Proof.
induction 1. done. inversion 1; subst; auto. Qed.
Lemma same_length_Forall2 l1 l2 :
same_length l1 l2 ↔
Forall2 (λ
_ _,
True)
l1 l2.
Proof.
split; induction 1; constructor; auto. Qed.
Lemma same_length_take l1 l2 n :
same_length l1 l2 →
same_length (
take n l1) (
take n l2).
Proof.
rewrite !same_length_Forall2. apply Forall2_take. Qed.
Lemma same_length_drop l1 l2 n :
same_length l1 l2 →
same_length (
drop n l1) (
drop n l2).
Proof.
rewrite !same_length_Forall2. apply Forall2_drop. Qed.
Lemma same_length_resize l1 l2 x1 x2 n :
same_length (
resize n x1 l1) (
resize n x2 l2).
Proof.
apply same_length_length. by rewrite !resize_length. Qed.
End same_length.
Instance: ∀
A,
Reflexive (@
same_length A A).
Proof.
intros A l. induction l; constructor; auto. Qed.
Zipping lists
Definition zip_with {
A B C} (
f :
A →
B →
C) :
list A →
list B →
list C :=
fix go l1 l2 :=
match l1,
l2 with
|
x1 ::
l1,
x2 ::
l2 =>
f x1 x2 ::
go l1 l2
|
_ ,
_ => []
end.
Section zip_with.
Context {
A B C :
Type} (
f :
A →
B →
C).
Lemma zip_with_length l1 l2 :
length l1 ≤
length l2 →
length (
zip_with f l1 l2) =
length l1.
Proof.
revert l2.
induction l1; intros [|??]; simpl; auto with lia.
Qed.
Lemma zip_with_fmap_fst_le (
g :
C →
A)
l1 l2 :
(∀
x y,
g (
f x y) =
x) →
length l1 ≤
length l2 →
g <$>
zip_with f l1 l2 =
l1.
Proof.
revert l2.
induction l1; intros [|??] ??; simpl in *; f_equal; auto with lia.
Qed.
Lemma zip_with_fmap_snd_le (
g :
C →
B)
l1 l2 :
(∀
x y,
g (
f x y) =
y) →
length l2 ≤
length l1 →
g <$>
zip_with f l1 l2 =
l2.
Proof.
revert l1.
induction l2; intros [|??] ??; simpl in *; f_equal; auto with lia.
Qed.
Lemma zip_with_fmap_fst (
g :
C →
A)
l1 l2 :
(∀
x y,
g (
f x y) =
x) →
same_length l1 l2 →
g <$>
zip_with f l1 l2 =
l1.
Proof.
induction 2; simpl; f_equal; auto. Qed.
Lemma zip_with_fmap_snd (
g :
C →
B)
l1 l2 :
(∀
x y,
g (
f x y) =
y) →
same_length l1 l2 →
g <$>
zip_with f l1 l2 =
l2.
Proof.
induction 2; simpl; f_equal; auto. Qed.
Lemma Forall_zip_with_fst (
P :
A →
Prop) (
Q :
C →
Prop)
l1 l2 :
Forall P l1 →
Forall (λ
y, ∀
x,
P x →
Q (
f x y))
l2 →
Forall Q (
zip_with f l1 l2).
Proof.
intros Hl1. revert l2.
induction Hl1; destruct 1; simpl in *; auto.
Qed.
Lemma Forall_zip_with_snd (
P :
B →
Prop) (
Q :
C →
Prop)
l1 l2 :
Forall (λ
x, ∀
y,
P y →
Q (
f x y))
l1 →
Forall P l2 →
Forall Q (
zip_with f l1 l2).
Proof.
intros Hl1. revert l2.
induction Hl1; destruct 1; simpl in *; auto.
Qed.
End zip_with.
Notation zip := (
zip_with pair).
Section zip.
Context {
A B :
Type}.
Lemma zip_length (
l1 :
list A) (
l2 :
list B) :
length l1 ≤
length l2 →
length (
zip l1 l2) =
length l1.
Proof.
by apply zip_with_length. Qed.
Lemma zip_fmap_fst_le (
l1 :
list A) (
l2 :
list B) :
length l1 ≤
length l2 →
fst <$>
zip l1 l2 =
l1.
Proof.
by apply zip_with_fmap_fst_le. Qed.
Lemma zip_fmap_snd (
l1 :
list A) (
l2 :
list B) :
length l2 ≤
length l1 →
snd <$>
zip l1 l2 =
l2.
Proof.
by apply zip_with_fmap_snd_le. Qed.
Lemma zip_fst (
l1 :
list A) (
l2 :
list B) :
same_length l1 l2 →
fst <$>
zip l1 l2 =
l1.
Proof.
by apply zip_with_fmap_fst. Qed.
Lemma zip_snd (
l1 :
list A) (
l2 :
list B) :
same_length l1 l2 →
snd <$>
zip l1 l2 =
l2.
Proof.
by apply zip_with_fmap_snd. Qed.
End zip.
Definition zipped_map {
A B} (
f :
list A →
list A →
A →
B) :
list A →
list A →
list B :=
fix go l k :=
match k with
| [] => []
|
x ::
k =>
f l k x ::
go (
x ::
l)
k
end.
Lemma elem_of_zipped_map {
A B} (
f :
list A →
list A →
A →
B)
l k x :
x ∈
zipped_map f l k ↔
∃
k'
k''
y,
k =
k' ++ [
y] ++
k'' ∧
x =
f (
reverse k' ++
l)
k''
y.
Proof.
split.
* revert l. induction k as [|z k IH]; simpl;
intros l ?; decompose_elem_of_list.
+ by eexists [], k, z.
+ destruct (IH (z :: l)) as [k' [k'' [y [??]]]]; [done |]; subst.
eexists (z :: k'), k'', y. split; [done |].
by rewrite reverse_cons, <-app_assoc.
* intros [k' [k'' [y [??]]]]; subst.
revert l. induction k' as [|z k' IH]; intros l.
+ by left.
+ right. by rewrite reverse_cons, <-!app_assoc.
Qed.
Section zipped_list_ind.
Context {
A} (
P :
list A →
list A →
Prop).
Context (
Pnil : ∀
l,
P l []).
Context (
Pcons : ∀
l k x,
P (
x ::
l)
k →
P l (
x ::
k)).
Fixpoint zipped_list_ind l k :
P l k :=
match k with
| [] =>
Pnil _
|
x ::
k =>
Pcons _ _ _ (
zipped_list_ind (
x ::
l)
k)
end.
End zipped_list_ind.
Inductive zipped_Forall {
A} (
P :
list A →
list A →
A →
Prop) :
list A →
list A →
Prop :=
|
zipped_Forall_nil l :
zipped_Forall P l []
|
zipped_Forall_cons l k x :
P l k x →
zipped_Forall P (
x ::
l)
k →
zipped_Forall P l (
x ::
k).
Arguments zipped_Forall_nil {
_ _}
_.
Arguments zipped_Forall_cons {
_ _}
_ _ _ _ _.
Lemma zipped_Forall_app {
A} (
P :
list A →
list A →
A →
Prop)
l k k' :
zipped_Forall P l (
k ++
k') →
zipped_Forall P (
reverse k ++
l)
k'.
Proof.
revert l. induction k as [|x k IH]; simpl; [done |].
inversion_clear 1. rewrite reverse_cons, <-app_assoc.
by apply IH.
Qed.
Permutations
Fixpoint interleave {
A} (
x :
A) (
l :
list A) :
list (
list A) :=
match l with
| [] => [ [
x] ]
|
y ::
l => (
x ::
y ::
l) :: ((
y ::) <$>
interleave x l)
end.
Fixpoint permutations {
A} (
l :
list A) :
list (
list A) :=
match l with
| [] => [ [] ]
|
x ::
l =>
permutations l ≫=
interleave x
end.
Section permutations.
Context {
A :
Type}.
Lemma interleave_cons (
x :
A) (
l :
list A) :
x ::
l ∈
interleave x l.
Proof.
destruct l; simpl; rewrite elem_of_cons; auto. Qed.
Lemma interleave_Permutation (
x :
A) (
l l' :
list A) :
l' ∈
interleave x l →
Permutation l' (
x ::
l).
Proof.
revert l'. induction l as [|y l IH]; intros l'; simpl.
* rewrite elem_of_list_singleton. intros. by subst.
* rewrite elem_of_cons, elem_of_list_fmap.
intros [?|[? [? H]]]; subst.
+ by constructor.
+ rewrite (IH _ H). constructor.
Qed.
Lemma permutations_refl (
l :
list A) :
l ∈
permutations l.
Proof.
induction l; simpl.
* by apply elem_of_list_singleton.
* apply elem_of_list_bind. eauto using interleave_cons.
Qed.
Lemma permutations_skip (
x :
A) (
l l' :
list A) :
l ∈
permutations l' →
x ::
l ∈
permutations (
x ::
l').
Proof.
intros Hl. simpl. apply elem_of_list_bind.
eauto using interleave_cons.
Qed.
Lemma permutations_swap (
x y :
A) (
l :
list A) :
y ::
x ::
l ∈
permutations (
x ::
y ::
l).
Proof.
simpl. apply elem_of_list_bind.
exists (y :: l). split; simpl.
* destruct l; simpl; rewrite !elem_of_cons; auto.
* apply elem_of_list_bind. simpl.
eauto using interleave_cons, permutations_refl.
Qed.
Lemma permutations_nil (
l :
list A) :
l ∈
permutations [] ↔
l = [].
Proof.
simpl. by rewrite elem_of_list_singleton. Qed.
Lemma interleave_interleave_toggle (
x1 x2 :
A) (
l1 l2 l3 :
list A) :
l1 ∈
interleave x1 l2 →
l2 ∈
interleave x2 l3 → ∃
l4,
l1 ∈
interleave x2 l4 ∧
l4 ∈
interleave x1 l3.
Proof.
revert l1 l2. induction l3 as [|y l3 IH]; intros l1 l2; simpl.
{ intros Hl1 Hl2.
rewrite elem_of_list_singleton in Hl2. subst. simpl in Hl1.
rewrite elem_of_cons, elem_of_list_singleton in Hl1.
exists [x1]. simpl.
rewrite elem_of_cons, !elem_of_list_singleton. tauto. }
rewrite elem_of_cons, elem_of_list_fmap.
intros Hl1 [? | [l2' [??]]]; subst; simpl in *.
* rewrite !elem_of_cons, elem_of_list_fmap in Hl1.
destruct Hl1 as [? | [? | [l4 [??]]]]; subst.
+ exists (x1 :: y :: l3). simpl. rewrite !elem_of_cons. tauto.
+ exists (x1 :: y :: l3). simpl. rewrite !elem_of_cons. tauto.
+ exists l4. simpl. rewrite elem_of_cons. auto using interleave_cons.
* rewrite elem_of_cons, elem_of_list_fmap in Hl1.
destruct Hl1 as [? | [l1' [??]]]; subst.
+ exists (x1 :: y :: l3). simpl.
rewrite !elem_of_cons, !elem_of_list_fmap.
split; [| by auto]. right. right. exists (y :: l2').
rewrite elem_of_list_fmap. naive_solver.
+ destruct (IH l1' l2') as [l4 [??]]; auto.
exists (y :: l4). simpl.
rewrite !elem_of_cons, !elem_of_list_fmap. naive_solver.
Qed.
Lemma permutations_interleave_toggle (
x :
A) (
l1 l2 l3 :
list A) :
l1 ∈
permutations l2 →
l2 ∈
interleave x l3 → ∃
l4,
l1 ∈
interleave x l4 ∧
l4 ∈
permutations l3.
Proof.
revert l1 l2. induction l3 as [|y l3 IH]; intros l1 l2; simpl.
{ intros Hl1 Hl2. eexists []. simpl.
split; [| by rewrite elem_of_list_singleton].
rewrite elem_of_list_singleton in Hl2.
by rewrite Hl2 in Hl1. }
rewrite elem_of_cons, elem_of_list_fmap.
intros Hl1 [? | [l2' [? Hl2']]]; subst; simpl in *.
* rewrite elem_of_list_bind in Hl1.
destruct Hl1 as [l1' [??]]. by exists l1'.
* rewrite elem_of_list_bind in Hl1.
setoid_rewrite elem_of_list_bind.
destruct Hl1 as [l1' [??]].
destruct (IH l1' l2') as [l1'' [??]]; auto.
destruct (interleave_interleave_toggle y x l1 l1' l1'') as [? [??]]; eauto.
Qed.
Lemma permutations_trans (
l1 l2 l3 :
list A) :
l1 ∈
permutations l2 →
l2 ∈
permutations l3 →
l1 ∈
permutations l3.
Proof.
revert l1 l2. induction l3 as [|x l3 IH]; intros l1 l2; simpl.
* intros Hl1 Hl2. rewrite elem_of_list_singleton in Hl2.
by rewrite Hl2 in Hl1.
* rewrite !elem_of_list_bind. intros Hl1 [l2' [Hl2 Hl2']].
destruct (permutations_interleave_toggle x l1 l2 l2') as [? [??]]; eauto.
Qed.
Lemma permutations_Permutation (
l l' :
list A) :
l' ∈
permutations l ↔
Permutation l l'.
Proof.
split.
* revert l'. induction l; simpl; intros l''.
+ rewrite elem_of_list_singleton.
intros. subst. constructor.
+ rewrite elem_of_list_bind. intros [l' [Hl'' ?]].
rewrite (interleave_Permutation _ _ _ Hl'').
constructor; auto.
* induction 1; eauto using permutations_refl,
permutations_skip, permutations_swap, permutations_trans.
Qed.
Global Instance Permutation_dec `{∀
x y :
A,
Decision (
x =
y)}
(
l1 l2 :
list A) :
Decision (
Permutation l1 l2).
Proof.
refine (cast_if (decide (l2 ∈ permutations l1)));
by rewrite <-permutations_Permutation.
Defined.
End permutations.
Set operations on lists
Section list_set_operations.
Context {
A} {
dec : ∀
x y :
A,
Decision (
x =
y)}.
Fixpoint list_difference (
l k :
list A) :
list A :=
match l with
| [] => []
|
x ::
l =>
if decide_rel (∈)
x k
then list_difference l k
else x ::
list_difference l k
end.
Lemma elem_of_list_difference l k x :
x ∈
list_difference l k ↔
x ∈
l ∧
x ∉
k.
Proof.
split; induction l; simpl; try case_decide;
rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence.
Qed.
Lemma list_difference_nodup l k :
NoDup l →
NoDup (
list_difference l k).
Proof.
induction 1; simpl; try case_decide.
* constructor.
* done.
* constructor. rewrite elem_of_list_difference; intuition. done.
Qed.
Fixpoint list_intersection (
l k :
list A) :
list A :=
match l with
| [] => []
|
x ::
l =>
if decide_rel (∈)
x k
then x ::
list_intersection l k
else list_intersection l k
end.
Lemma elem_of_list_intersection l k x :
x ∈
list_intersection l k ↔
x ∈
l ∧
x ∈
k.
Proof.
split; induction l; simpl; repeat case_decide;
rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence.
Qed.
Lemma list_intersection_nodup l k :
NoDup l →
NoDup (
list_intersection l k).
Proof.
induction 1; simpl; try case_decide.
* constructor.
* constructor. rewrite elem_of_list_intersection; intuition. done.
* done.
Qed.
Definition list_intersection_with (
f :
A →
A →
option A) :
list A →
list A →
list A :=
fix go l k :=
match l with
| [] => []
|
x ::
l =>
foldr (λ
y,
match f x y with None =>
id |
Some z => (
z ::)
end) (
go l k)
k
end.
Lemma elem_of_list_intersection_with f l k x :
x ∈
list_intersection_with f l k ↔ ∃
x1 x2,
x1 ∈
l ∧
x2 ∈
k ∧
f x1 x2 =
Some x.
Proof.
split.
* induction l as [|x1 l IH]; simpl.
+ by rewrite elem_of_nil.
+ intros Hx. setoid_rewrite elem_of_cons.
cut ((∃ x2, x2 ∈ k ∧ f x1 x2 = Some x)
∨ x ∈ list_intersection_with f l k).
{ naive_solver. }
clear IH. revert Hx. generalize (list_intersection_with f l k).
induction k; simpl; [by auto|].
case_match; setoid_rewrite elem_of_cons; naive_solver.
* intros (x1 & x2 & Hx1 & Hx2 & Hx).
induction Hx1 as [x1 | x1 ? l ? IH]; simpl.
+ generalize (list_intersection_with f l k).
induction Hx2; simpl; [by rewrite Hx; left |].
case_match; simpl; try setoid_rewrite elem_of_cons; auto.
+ generalize (IH Hx). clear Hx IH Hx2.
generalize (list_intersection_with f l k).
induction k; simpl; intros; [done |].
case_match; simpl; rewrite ?elem_of_cons; auto.
Qed.
End list_set_operations.