Commit 0158faa7 authored by Robbert Krebbers's avatar Robbert Krebbers

Renaming in prelude/list.

Rename:

- prefix_of -> prefix and suffix_of -> suffix because that saves keystrokes
  in lemma names. However, keep the infix notations with l1 `prefix_of` l2 and
  l1 `suffix_of` l2 because those are easier to read.
- change the notation l1 `sublist` l2 into l1 `sublist_of` l2 to be consistent.
- rename contains -> submseteq and use the notation ⊆+
parent 808b681c
......@@ -69,9 +69,9 @@ Proof.
apply Permutation_singleton. by rewrite <-(right_id () {[x]}),
elements_union_singleton, elements_empty by set_solver.
Qed.
Lemma elements_contains X Y : X Y elements X `contains` elements Y.
Lemma elements_submseteq X Y : X Y elements X + elements Y.
Proof.
intros; apply NoDup_contains; auto using NoDup_elements.
intros; apply NoDup_submseteq; auto using NoDup_elements.
intros x. rewrite !elem_of_elements; auto.
Qed.
......
......@@ -699,10 +699,10 @@ Proof.
by rewrite map_to_list_insert, map_to_list_empty by auto using lookup_empty.
Qed.
Lemma map_to_list_contains {A} (m1 m2 : M A) :
m1 m2 map_to_list m1 `contains` map_to_list m2.
Lemma map_to_list_submseteq {A} (m1 m2 : M A) :
m1 m2 map_to_list m1 + map_to_list m2.
Proof.
intros; apply NoDup_contains; auto using NoDup_map_to_list.
intros; apply NoDup_submseteq; auto using NoDup_map_to_list.
intros [i x]. rewrite !elem_of_map_to_list; eauto using lookup_weaken.
Qed.
Lemma map_to_list_fmap {A B} (f : A B) m :
......
......@@ -107,17 +107,17 @@ Proof.
unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|].
constructor; exact x.
Qed.
Lemma finite_inj_contains `{finA: Finite A} `{finB: Finite B} (f: A B)
`{!Inj (=) (=) f} : f <$> enum A `contains` enum B.
Lemma finite_inj_submseteq `{finA: Finite A} `{finB: Finite B} (f: A B)
`{!Inj (=) (=) f} : f <$> enum A + enum B.
Proof.
intros. destruct finA, finB. apply NoDup_contains; auto using NoDup_fmap_2.
intros. destruct finA, finB. apply NoDup_submseteq; auto using NoDup_fmap_2.
Qed.
Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A B)
`{!Inj (=) (=) f} : card A = card B f <$> enum A enum B.
Proof.
intros. apply contains_Permutation_length_eq.
intros. apply submseteq_Permutation_length_eq.
- by rewrite fmap_length.
- by apply finite_inj_contains.
- by apply finite_inj_submseteq.
Qed.
Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A B)
`{!Inj (=) (=) f} : card A = card B Surj (=) f.
......@@ -144,7 +144,7 @@ Proof.
destruct (finite_surj A B) as (g&?); auto with lia.
destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
- intros [f ?]. unfold card. rewrite <-(fmap_length f).
by apply contains_length, (finite_inj_contains f).
by apply submseteq_length, (finite_inj_submseteq f).
Qed.
Lemma finite_bijective A `{Finite A} B `{Finite B} :
card A = card B f : A B, Inj (=) (=) f Surj (=) f.
......
......@@ -345,14 +345,14 @@ Proof.
Qed.
(* Mononicity *)
Lemma gmultiset_elements_contains X Y : X Y elements X `contains` elements Y.
Lemma gmultiset_elements_submseteq X Y : X Y elements X + elements Y.
Proof.
intros ->%gmultiset_union_difference. rewrite gmultiset_elements_union.
by apply contains_inserts_r.
by apply submseteq_inserts_r.
Qed.
Lemma gmultiset_subseteq_size X Y : X Y size X size Y.
Proof. intros. by apply contains_length, gmultiset_elements_contains. Qed.
Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed.
Lemma gmultiset_subset_size X Y : X Y size X < size Y.
Proof.
......
......@@ -236,19 +236,19 @@ Fixpoint interleave {A} (x : A) (l : list A) : list (list A) :=
Fixpoint permutations {A} (l : list A) : list (list A) :=
match l with [] => [[]] | x :: l => permutations l ≫= interleave x end.
(** The predicate [suffix_of] holds if the first list is a suffix of the second.
The predicate [prefix_of] holds if the first list is a prefix of the second. *)
Definition suffix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1.
Definition prefix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = l1 ++ k.
Infix "`suffix_of`" := suffix_of (at level 70) : C_scope.
Infix "`prefix_of`" := prefix_of (at level 70) : C_scope.
(** The predicate [suffix] holds if the first list is a suffix of the second.
The predicate [prefix] holds if the first list is a prefix of the second. *)
Definition suffix {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1.
Definition prefix {A} : relation (list A) := λ l1 l2, ∃ k, l2 = l1 ++ k.
Infix "`suffix_of`" := suffix (at level 70) : C_scope.
Infix "`prefix_of`" := prefix (at level 70) : C_scope.
Hint Extern 0 (_ `prefix_of` _) => reflexivity.
Hint Extern 0 (_ `suffix_of` _) => reflexivity.
Section prefix_suffix_ops.
Context `{EqDecision A}.
Definition max_prefix_of : list A → list A → list A * list A * list A :=
Definition max_prefix : list A → list A → list A * list A * list A :=
fix go l1 l2 :=
match l1, l2 with
| [], l2 => ([], l2, [])
......@@ -257,12 +257,12 @@ Section prefix_suffix_ops.
if decide_rel (=) x1 x2
then prod_map id (x1 ::) (go l1 l2) else (x1 :: l1, x2 :: l2, [])
end.
Definition max_suffix_of (l1 l2 : list A) : list A * list A * list A :=
match max_prefix_of (reverse l1) (reverse l2) with
Definition max_suffix (l1 l2 : list A) : list A * list A * list A :=
match max_prefix (reverse l1) (reverse l2) with
| (k1, k2, k3) => (reverse k1, reverse k2, reverse k3)
end.
Definition strip_prefix (l1 l2 : list A) := (max_prefix_of l1 l2).1.2.
Definition strip_suffix (l1 l2 : list A) := (max_suffix_of l1 l2).1.2.
Definition strip_prefix (l1 l2 : list A) := (max_prefix l1 l2).1.2.
Definition strip_suffix (l1 l2 : list A) := (max_suffix l1 l2).1.2.
End prefix_suffix_ops.
(** A list [l1] is a sublist of [l2] if [l2] is obtained by removing elements
......@@ -271,19 +271,19 @@ Inductive sublist {A} : relation (list A) :=
| sublist_nil : sublist [] []
| sublist_skip x l1 l2 : sublist l1 l2 → sublist (x :: l1) (x :: l2)
| sublist_cons x l1 l2 : sublist l1 l2 → sublist l1 (x :: l2).
Infix "`sublist`" := sublist (at level 70) : C_scope.
Hint Extern 0 (_ `sublist` _) => reflexivity.
Infix "`sublist_of`" := sublist (at level 70) : C_scope.
Hint Extern 0 (_ `sublist_of` _) => reflexivity.
(** A list [l2] contains a list [l1] if [l2] is obtained by removing elements
(** A list [l2] submseteq a list [l1] if [l2] is obtained by removing elements
from [l1] while possiblity changing the order. *)
Inductive contains {A} : relation (list A) :=
| contains_nil : contains [] []
| contains_skip x l1 l2 : contains l1 l2 → contains (x :: l1) (x :: l2)
| contains_swap x y l : contains (y :: x :: l) (x :: y :: l)
| contains_cons x l1 l2 : contains l1 l2 → contains l1 (x :: l2)
| contains_trans l1 l2 l3 : contains l1 l2 → contains l2 l3 → contains l1 l3.
Infix "`contains`" := contains (at level 70) : C_scope.
Hint Extern 0 (_ `contains` _) => reflexivity.
Inductive submseteq {A} : relation (list A) :=
| submseteq_nil : submseteq [] []
| submseteq_skip x l1 l2 : submseteq l1 l2 → submseteq (x :: l1) (x :: l2)
| submseteq_swap x y l : submseteq (y :: x :: l) (x :: y :: l)
| submseteq_cons x l1 l2 : submseteq l1 l2 → submseteq l1 (x :: l2)
| submseteq_trans l1 l2 l3 : submseteq l1 l2 → submseteq l2 l3 → submseteq l1 l3.
Infix "⊆+" := submseteq (at level 70) : C_scope.
Hint Extern 0 (_ ⊆+ _) => reflexivity.
(** Removes [x] from the list [l]. The function returns a [Some] when the
+removal succeeds and [None] when [x] is not in [l]. *)
......@@ -351,7 +351,7 @@ Section list_set.
End list_set.
(** * Basic tactics on lists *)
(** The tactic [discriminate_list] discharges a goal if it contains
(** The tactic [discriminate_list] discharges a goal if it submseteq
a list equality involving [(::)] and [(++)] of two lists that have a different
length as one of its hypotheses. *)
Tactic Notation "discriminate_list" hyp(H) :=
......@@ -1426,120 +1426,120 @@ Qed.
Lemma elem_of_Permutation l x : x ∈ l → ∃ k, l ≡ₚ x :: k.
Proof. intros [i ?]%elem_of_list_lookup. eauto using delete_Permutation. Qed.
(** ** Properties of the [prefix_of] and [suffix_of] predicates *)
Global Instance: PreOrder (@prefix_of A).
(** ** Properties of the [prefix] and [suffix] predicates *)
Global Instance: PreOrder (@prefix A).
Proof.
split.
- intros ?. eexists []. by rewrite (right_id_L [] (++)).
- intros ???[k1->] [k2->]. exists (k1 ++ k2). by rewrite (assoc_L (++)).
Qed.
Lemma prefix_of_nil l : [] `prefix_of` l.
Lemma prefix_nil l : [] `prefix_of` l.
Proof. by exists l. Qed.
Lemma prefix_of_nil_not x l : ¬x :: l `prefix_of` [].
Lemma prefix_nil_not x l : ¬x :: l `prefix_of` [].
Proof. by intros [k ?]. Qed.
Lemma prefix_of_cons x l1 l2 : l1 `prefix_of` l2 → x :: l1 `prefix_of` x :: l2.
Lemma prefix_cons x l1 l2 : l1 `prefix_of` l2 → x :: l1 `prefix_of` x :: l2.
Proof. intros [k ->]. by exists k. Qed.
Lemma prefix_of_cons_alt x y l1 l2 :
Lemma prefix_cons_alt x y l1 l2 :
x = y → l1 `prefix_of` l2 → x :: l1 `prefix_of` y :: l2.
Proof. intros ->. apply prefix_of_cons. Qed.
Lemma prefix_of_cons_inv_1 x y l1 l2 : x :: l1 `prefix_of` y :: l2 → x = y.
Proof. intros ->. apply prefix_cons. Qed.
Lemma prefix_cons_inv_1 x y l1 l2 : x :: l1 `prefix_of` y :: l2 → x = y.
Proof. by intros [k ?]; simplify_eq/=. Qed.
Lemma prefix_of_cons_inv_2 x y l1 l2 :
Lemma prefix_cons_inv_2 x y l1 l2 :
x :: l1 `prefix_of` y :: l2 → l1 `prefix_of` l2.
Proof. intros [k ?]; simplify_eq/=. by exists k. Qed.
Lemma prefix_of_app k l1 l2 : l1 `prefix_of` l2 → k ++ l1 `prefix_of` k ++ l2.
Lemma prefix_app k l1 l2 : l1 `prefix_of` l2 → k ++ l1 `prefix_of` k ++ l2.
Proof. intros [k' ->]. exists k'. by rewrite (assoc_L (++)). Qed.
Lemma prefix_of_app_alt k1 k2 l1 l2 :
Lemma prefix_app_alt k1 k2 l1 l2 :
k1 = k2 → l1 `prefix_of` l2 → k1 ++ l1 `prefix_of` k2 ++ l2.
Proof. intros ->. apply prefix_of_app. Qed.
Lemma prefix_of_app_l l1 l2 l3 : l1 ++ l3 `prefix_of` l2 → l1 `prefix_of` l2.
Proof. intros ->. apply prefix_app. Qed.
Lemma prefix_app_l l1 l2 l3 : l1 ++ l3 `prefix_of` l2 → l1 `prefix_of` l2.
Proof. intros [k ->]. exists (l3 ++ k). by rewrite (assoc_L (++)). Qed.
Lemma prefix_of_app_r l1 l2 l3 : l1 `prefix_of` l2 → l1 `prefix_of` l2 ++ l3.
Lemma prefix_app_r l1 l2 l3 : l1 `prefix_of` l2 → l1 `prefix_of` l2 ++ l3.
Proof. intros [k ->]. exists (k ++ l3). by rewrite (assoc_L (++)). Qed.
Lemma prefix_of_length l1 l2 : l1 `prefix_of` l2 → length l1 ≤ length l2.
Lemma prefix_length l1 l2 : l1 `prefix_of` l2 → length l1 ≤ length l2.
Proof. intros [? ->]. rewrite app_length. lia. Qed.
Lemma prefix_of_snoc_not l x : ¬l ++ [x] `prefix_of` l.
Lemma prefix_snoc_not l x : ¬l ++ [x] `prefix_of` l.
Proof. intros [??]. discriminate_list. Qed.
Global Instance: PreOrder (@suffix_of A).
Global Instance: PreOrder (@suffix A).
Proof.
split.
- intros ?. by eexists [].
- intros ???[k1->] [k2->]. exists (k2 ++ k1). by rewrite (assoc_L (++)).
Qed.
Global Instance prefix_of_dec `{!EqDecision A} : ∀ l1 l2,
Global Instance prefix_dec `{!EqDecision A} : ∀ l1 l2,
Decision (l1 `prefix_of` l2) := fix go l1 l2 :=
match l1, l2 return { l1 `prefix_of` l2 } + { ¬l1 `prefix_of` l2 } with
| [], _ => left (prefix_of_nil _)
| _, [] => right (prefix_of_nil_not _ _)
| [], _ => left (prefix_nil _)
| _, [] => right (prefix_nil_not _ _)
| x :: l1, y :: l2 =>
match decide_rel (=) x y with
| left Hxy =>
match go l1 l2 with
| left Hl1l2 => left (prefix_of_cons_alt _ _ _ _ Hxy Hl1l2)
| right Hl1l2 => right (Hl1l2 ∘ prefix_of_cons_inv_2 _ _ _ _)
| left Hl1l2 => left (prefix_cons_alt _ _ _ _ Hxy Hl1l2)
| right Hl1l2 => right (Hl1l2 ∘ prefix_cons_inv_2 _ _ _ _)
end
| right Hxy => right (Hxy ∘ prefix_of_cons_inv_1 _ _ _ _)
| right Hxy => right (Hxy ∘ prefix_cons_inv_1 _ _ _ _)
end
end.
Section prefix_ops.
Context `{!EqDecision A}.
Lemma max_prefix_of_fst l1 l2 :
l1 = (max_prefix_of l1 l2).2 ++ (max_prefix_of l1 l2).1.1.
Lemma max_prefix_fst l1 l2 :
l1 = (max_prefix l1 l2).2 ++ (max_prefix l1 l2).1.1.
Proof.
revert l2. induction l1; intros [|??]; simpl;
repeat case_decide; f_equal/=; auto.
Qed.
Lemma max_prefix_of_fst_alt l1 l2 k1 k2 k3 :
max_prefix_of l1 l2 = (k1, k2, k3) → l1 = k3 ++ k1.
Lemma max_prefix_fst_alt l1 l2 k1 k2 k3 :
max_prefix l1 l2 = (k1, k2, k3) → l1 = k3 ++ k1.
Proof.
intros. pose proof (max_prefix_of_fst l1 l2).
by destruct (max_prefix_of l1 l2) as [[]?]; simplify_eq.
intros. pose proof (max_prefix_fst l1 l2).
by destruct (max_prefix l1 l2) as [[]?]; simplify_eq.
Qed.
Lemma max_prefix_of_fst_prefix l1 l2 : (max_prefix_of l1 l2).2 `prefix_of` l1.
Proof. eexists. apply max_prefix_of_fst. Qed.
Lemma max_prefix_of_fst_prefix_alt l1 l2 k1 k2 k3 :
max_prefix_of l1 l2 = (k1, k2, k3) → k3 `prefix_of` l1.
Proof. eexists. eauto using max_prefix_of_fst_alt. Qed.
Lemma max_prefix_of_snd l1 l2 :
l2 = (max_prefix_of l1 l2).2 ++ (max_prefix_of l1 l2).1.2.
Lemma max_prefix_fst_prefix l1 l2 : (max_prefix l1 l2).2 `prefix_of` l1.
Proof. eexists. apply max_prefix_fst. Qed.
Lemma max_prefix_fst_prefix_alt l1 l2 k1 k2 k3 :
max_prefix l1 l2 = (k1, k2, k3) → k3 `prefix_of` l1.
Proof. eexists. eauto using max_prefix_fst_alt. Qed.
Lemma max_prefix_snd l1 l2 :
l2 = (max_prefix l1 l2).2 ++ (max_prefix l1 l2).1.2.
Proof.
revert l2. induction l1; intros [|??]; simpl;
repeat case_decide; f_equal/=; auto.
Qed.
Lemma max_prefix_of_snd_alt l1 l2 k1 k2 k3 :
max_prefix_of l1 l2 = (k1, k2, k3) → l2 = k3 ++ k2.
Lemma max_prefix_snd_alt l1 l2 k1 k2 k3 :
max_prefix l1 l2 = (k1, k2, k3) → l2 = k3 ++ k2.
Proof.
intro. pose proof (max_prefix_of_snd l1 l2).
by destruct (max_prefix_of l1 l2) as [[]?]; simplify_eq.
intro. pose proof (max_prefix_snd l1 l2).
by destruct (max_prefix l1 l2) as [[]?]; simplify_eq.
Qed.
Lemma max_prefix_of_snd_prefix l1 l2 : (max_prefix_of l1 l2).2 `prefix_of` l2.
Proof. eexists. apply max_prefix_of_snd. Qed.
Lemma max_prefix_of_snd_prefix_alt l1 l2 k1 k2 k3 :
max_prefix_of l1 l2 = (k1,k2,k3) → k3 `prefix_of` l2.
Proof. eexists. eauto using max_prefix_of_snd_alt. Qed.
Lemma max_prefix_of_max l1 l2 k :
k `prefix_of` l1 → k `prefix_of` l2 → k `prefix_of` (max_prefix_of l1 l2).2.
Lemma max_prefix_snd_prefix l1 l2 : (max_prefix l1 l2).2 `prefix_of` l2.
Proof. eexists. apply max_prefix_snd. Qed.
Lemma max_prefix_snd_prefix_alt l1 l2 k1 k2 k3 :
max_prefix l1 l2 = (k1,k2,k3) → k3 `prefix_of` l2.
Proof. eexists. eauto using max_prefix_snd_alt. Qed.
Lemma max_prefix_max l1 l2 k :
k `prefix_of` l1 → k `prefix_of` l2 → k `prefix_of` (max_prefix l1 l2).2.
Proof.
intros [l1' ->] [l2' ->]. by induction k; simpl; repeat case_decide;
simpl; auto using prefix_of_nil, prefix_of_cons.
simpl; auto using prefix_nil, prefix_cons.
Qed.
Lemma max_prefix_of_max_alt l1 l2 k1 k2 k3 k :
max_prefix_of l1 l2 = (k1,k2,k3) →
Lemma max_prefix_max_alt l1 l2 k1 k2 k3 k :
max_prefix l1 l2 = (k1,k2,k3) →
k `prefix_of` l1 → k `prefix_of` l2 → k `prefix_of` k3.
Proof.
intro. pose proof (max_prefix_of_max l1 l2 k).
by destruct (max_prefix_of l1 l2) as [[]?]; simplify_eq.
intro. pose proof (max_prefix_max l1 l2 k).
by destruct (max_prefix l1 l2) as [[]?]; simplify_eq.
Qed.
Lemma max_prefix_of_max_snoc l1 l2 k1 k2 k3 x1 x2 :
max_prefix_of l1 l2 = (x1 :: k1, x2 :: k2, k3) → x1 ≠ x2.
Lemma max_prefix_max_snoc l1 l2 k1 k2 k3 x1 x2 :
max_prefix l1 l2 = (x1 :: k1, x2 :: k2, k3) → x1 ≠ x2.
Proof.
intros Hl ->. destruct (prefix_of_snoc_not k3 x2).
eapply max_prefix_of_max_alt; eauto.
- rewrite (max_prefix_of_fst_alt _ _ _ _ _ Hl).
apply prefix_of_app, prefix_of_cons, prefix_of_nil.
- rewrite (max_prefix_of_snd_alt _ _ _ _ _ Hl).
apply prefix_of_app, prefix_of_cons, prefix_of_nil.
intros Hl ->. destruct (prefix_snoc_not k3 x2).
eapply max_prefix_max_alt; eauto.
- rewrite (max_prefix_fst_alt _ _ _ _ _ Hl).
apply prefix_app, prefix_cons, prefix_nil.
- rewrite (max_prefix_snd_alt _ _ _ _ _ Hl).
apply prefix_app, prefix_cons, prefix_nil.
Qed.
End prefix_ops.
......@@ -1553,147 +1553,147 @@ Qed.
Lemma suffix_prefix_reverse l1 l2 :
l1 `suffix_of` l2 ↔ reverse l1 `prefix_of` reverse l2.
Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.
Lemma suffix_of_nil l : [] `suffix_of` l.
Lemma suffix_nil l : [] `suffix_of` l.
Proof. exists l. by rewrite (right_id_L [] (++)). Qed.
Lemma suffix_of_nil_inv l : l `suffix_of` [] → l = [].
Lemma suffix_nil_inv l : l `suffix_of` [] → l = [].
Proof. by intros [[|?] ?]; simplify_list_eq. Qed.
Lemma suffix_of_cons_nil_inv x l : ¬x :: l `suffix_of` [].
Lemma suffix_cons_nil_inv x l : ¬x :: l `suffix_of` [].
Proof. by intros [[] ?]. Qed.
Lemma suffix_of_snoc l1 l2 x :
Lemma suffix_snoc l1 l2 x :
l1 `suffix_of` l2 → l1 ++ [x] `suffix_of` l2 ++ [x].
Proof. intros [k ->]. exists k. by rewrite (assoc_L (++)). Qed.
Lemma suffix_of_snoc_alt x y l1 l2 :
Lemma suffix_snoc_alt x y l1 l2 :
x = y → l1 `suffix_of` l2 → l1 ++ [x] `suffix_of` l2 ++ [y].
Proof. intros ->. apply suffix_of_snoc. Qed.
Lemma suffix_of_app l1 l2 k : l1 `suffix_of` l2 → l1 ++ k `suffix_of` l2 ++ k.
Proof. intros ->. apply suffix_snoc. Qed.
Lemma suffix_app l1 l2 k : l1 `suffix_of` l2 → l1 ++ k `suffix_of` l2 ++ k.
Proof. intros [k' ->]. exists k'. by rewrite (assoc_L (++)). Qed.
Lemma suffix_of_app_alt l1 l2 k1 k2 :
Lemma suffix_app_alt l1 l2 k1 k2 :
k1 = k2 → l1 `suffix_of` l2 → l1 ++ k1 `suffix_of` l2 ++ k2.
Proof. intros ->. apply suffix_of_app. Qed.
Lemma suffix_of_snoc_inv_1 x y l1 l2 :
Proof. intros ->. apply suffix_app. Qed.
Lemma suffix_snoc_inv_1 x y l1 l2 :
l1 ++ [x] `suffix_of` l2 ++ [y] → x = y.
Proof. intros [k' E]. rewrite (assoc_L (++)) in E. by simplify_list_eq. Qed.
Lemma suffix_of_snoc_inv_2 x y l1 l2 :
Lemma suffix_snoc_inv_2 x y l1 l2 :
l1 ++ [x] `suffix_of` l2 ++ [y] → l1 `suffix_of` l2.
Proof.
intros [k' E]. exists k'. rewrite (assoc_L (++)) in E. by simplify_list_eq.
Qed.
Lemma suffix_of_app_inv l1 l2 k :
Lemma suffix_app_inv l1 l2 k :
l1 ++ k `suffix_of` l2 ++ k → l1 `suffix_of` l2.
Proof.
intros [k' E]. exists k'. rewrite (assoc_L (++)) in E. by simplify_list_eq.
Qed.
Lemma suffix_of_cons_l l1 l2 x : x :: l1 `suffix_of` l2 → l1 `suffix_of` l2.
Lemma suffix_cons_l l1 l2 x : x :: l1 `suffix_of` l2 → l1 `suffix_of` l2.
Proof. intros [k ->]. exists (k ++ [x]). by rewrite <-(assoc_L (++)). Qed.
Lemma suffix_of_app_l l1 l2 l3 : l3 ++ l1 `suffix_of` l2 → l1 `suffix_of` l2.
Lemma suffix_app_l l1 l2 l3 : l3 ++ l1 `suffix_of` l2 → l1 `suffix_of` l2.
Proof. intros [k ->]. exists (k ++ l3). by rewrite <-(assoc_L (++)). Qed.
Lemma suffix_of_cons_r l1 l2 x : l1 `suffix_of` l2 → l1 `suffix_of` x :: l2.
Lemma suffix_cons_r l1 l2 x : l1 `suffix_of` l2 → l1 `suffix_of` x :: l2.
Proof. intros [k ->]. by exists (x :: k). Qed.
Lemma suffix_of_app_r l1 l2 l3 : l1 `suffix_of` l2 → l1 `suffix_of` l3 ++ l2.
Lemma suffix_app_r l1 l2 l3 : l1 `suffix_of` l2 → l1 `suffix_of` l3 ++ l2.
Proof. intros [k ->]. exists (l3 ++ k). by rewrite (assoc_L (++)). Qed.
Lemma suffix_of_cons_inv l1 l2 x y :
Lemma suffix_cons_inv l1 l2 x y :
x :: l1 `suffix_of` y :: l2 → x :: l1 = y :: l2 ∨ x :: l1 `suffix_of` l2.
Proof.
intros [[|? k] E]; [by left|]. right. simplify_eq/=. by apply suffix_of_app_r.
intros [[|? k] E]; [by left|]. right. simplify_eq/=. by apply suffix_app_r.
Qed.
Lemma suffix_of_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2.
Lemma suffix_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2.
Proof. intros [? ->]. rewrite app_length. lia. Qed.
Lemma suffix_of_cons_not x l : ¬x :: l `suffix_of` l.
Lemma suffix_cons_not x l : ¬x :: l `suffix_of` l.
Proof. intros [??]. discriminate_list. Qed.
Global Instance suffix_of_dec `{!EqDecision A} l1 l2 :
Global Instance suffix_dec `{!EqDecision A} l1 l2 :
Decision (l1 `suffix_of` l2).
Proof.
refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
refine (cast_if (decide_rel prefix (reverse l1) (reverse l2)));
abstract (by rewrite suffix_prefix_reverse).
Defined.
Section max_suffix_of.
Section max_suffix.
Context `{!EqDecision A}.
Lemma max_suffix_of_fst l1 l2 :
l1 = (max_suffix_of l1 l2).1.1 ++ (max_suffix_of l1 l2).2.
Lemma max_suffix_fst l1 l2 :
l1 = (max_suffix l1 l2).1.1 ++ (max_suffix l1 l2).2.
Proof.
rewrite <-(reverse_involutive l1) at 1.
rewrite (max_prefix_of_fst (reverse l1) (reverse l2)). unfold max_suffix_of.
destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
rewrite (max_prefix_fst (reverse l1) (reverse l2)). unfold max_suffix.
destruct (max_prefix (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
by rewrite reverse_app.
Qed.
Lemma max_suffix_of_fst_alt l1 l2 k1 k2 k3 :
max_suffix_of l1 l2 = (k1, k2, k3) → l1 = k1 ++ k3.
Lemma max_suffix_fst_alt l1 l2 k1 k2 k3 :
max_suffix l1 l2 = (k1, k2, k3) → l1 = k1 ++ k3.
Proof.
intro. pose proof (max_suffix_of_fst l1 l2).
by destruct (max_suffix_of l1 l2) as [[]?]; simplify_eq.
intro. pose proof (max_suffix_fst l1 l2).
by destruct (max_suffix l1 l2) as [[]?]; simplify_eq.
Qed.
Lemma max_suffix_of_fst_suffix l1 l2 : (max_suffix_of l1 l2).2 `suffix_of` l1.
Proof. eexists. apply max_suffix_of_fst. Qed.
Lemma max_suffix_of_fst_suffix_alt l1 l2 k1 k2 k3 :
max_suffix_of l1 l2 = (k1, k2, k3) → k3 `suffix_of` l1.
Proof. eexists. eauto using max_suffix_of_fst_alt. Qed.
Lemma max_suffix_of_snd l1 l2 :
l2 = (max_suffix_of l1 l2).1.2 ++ (max_suffix_of l1 l2).2.
Lemma max_suffix_fst_suffix l1 l2 : (max_suffix l1 l2).2 `suffix_of` l1.
Proof. eexists. apply max_suffix_fst. Qed.
Lemma max_suffix_fst_suffix_alt l1 l2 k1 k2 k3 :
max_suffix l1 l2 = (k1, k2, k3) → k3 `suffix_of` l1.
Proof. eexists. eauto using max_suffix_fst_alt. Qed.
Lemma max_suffix_snd l1 l2 :
l2 = (max_suffix l1 l2).1.2 ++ (max_suffix l1 l2).2.
Proof.
rewrite <-(reverse_involutive l2) at 1.
rewrite (max_prefix_of_snd (reverse l1) (reverse l2)). unfold max_suffix_of.
destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
rewrite (max_prefix_snd (reverse l1) (reverse l2)). unfold max_suffix.
destruct (max_prefix (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
by rewrite reverse_app.
Qed.
Lemma max_suffix_of_snd_alt l1 l2 k1 k2 k3 :
max_suffix_of l1 l2 = (k1,k2,k3) → l2 = k2 ++ k3.
Lemma max_suffix_snd_alt l1 l2 k1 k2 k3 :
max_suffix l1 l2 = (k1,k2,k3) → l2 = k2 ++ k3.
Proof.
intro. pose proof (max_suffix_of_snd l1 l2).
by destruct (max_suffix_of l1 l2) as [[]?]; simplify_eq.
intro. pose proof (max_suffix_snd l1 l2).
by destruct (max_suffix l1 l2) as [[]?]; simplify_eq.
Qed.
Lemma max_suffix_of_snd_suffix l1 l2 : (max_suffix_of l1 l2).2 `suffix_of` l2.
Proof. eexists. apply max_suffix_of_snd. Qed.
Lemma max_suffix_of_snd_suffix_alt l1 l2 k1 k2 k3 :
max_suffix_of l1 l2 = (k1,k2,k3) → k3 `suffix_of` l2.
Proof. eexists. eauto using max_suffix_of_snd_alt. Qed.
Lemma max_suffix_of_max l1 l2 k :
k `suffix_of` l1 → k `suffix_of` l2 → k `suffix_of` (max_suffix_of l1 l2).2.
Lemma max_suffix_snd_suffix l1 l2 : (max_suffix l1 l2).2 `suffix_of` l2.
Proof. eexists. apply max_suffix_snd. Qed.
Lemma max_suffix_snd_suffix_alt l1 l2 k1 k2 k3 :
max_suffix l1 l2 = (k1,k2,k3) → k3 `suffix_of` l2.
Proof. eexists. eauto using max_suffix_snd_alt. Qed.
Lemma max_suffix_max l1 l2 k :
k `suffix_of` l1 → k `suffix_of` l2 → k `suffix_of` (max_suffix l1 l2).2.
Proof.
generalize (max_prefix_of_max (reverse l1) (reverse l2)).
rewrite !suffix_prefix_reverse. unfold max_suffix_of.
destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
generalize (max_prefix_max (reverse l1) (reverse l2)).
rewrite !suffix_prefix_reverse. unfold max_suffix.
destruct (max_prefix (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
rewrite reverse_involutive. auto.
Qed.
Lemma max_suffix_of_max_alt l1 l2 k1 k2 k3 k :
max_suffix_of l1 l2 = (k1, k2, k3) →
Lemma max_suffix_max_alt l1 l2 k1 k2 k3 k :
max_suffix l1 l2 = (k1, k2, k3) →
k `suffix_of` l1 → k `suffix_of` l2 → k `suffix_of` k3.
Proof.
intro. pose proof (max_suffix_of_max l1 l2 k).
by destruct (max_suffix_of l1 l2) as [[]?]; simplify_eq.
intro. pose proof (max_suffix_max l1 l2 k).
by destruct (max_suffix l1 l2) as [[]?]; simplify_eq.
Qed.
Lemma max_suffix_of_max_snoc l1 l2 k1 k2 k3 x1 x2 :
max_suffix_of l1 l2 = (k1 ++ [x1], k2 ++ [x2], k3) → x1 ≠ x2.
Lemma max_suffix_max_snoc l1 l2 k1 k2 k3 x1 x2 :
max_suffix l1 l2 = (k1 ++ [x1], k2 ++ [x2], k3) → x1 ≠ x2.
Proof.
intros Hl ->. destruct (suffix_of_cons_not x2 k3).
eapply max_suffix_of_max_alt; eauto.
- rewrite (max_suffix_of_fst_alt _ _ _ _ _ Hl).
by apply (suffix_of_app [x2]), suffix_of_app_r.
- rewrite (max_suffix_of_snd_alt _ _ _ _ _ Hl).
by apply (suffix_of_app [x2]), suffix_of_app_r.
intros Hl ->. destruct (suffix_cons_not x2 k3).
eapply max_suffix_max_alt; eauto.
- rewrite (max_suffix_fst_alt _ _ _ _ _ Hl).
by apply (suffix_app [x2]), suffix_app_r.
- rewrite (max_suffix_snd_alt _ _ _ _ _ Hl).
by apply (suffix_app [x2]), suffix_app_r.
Qed.
End max_suffix_of.
End max_suffix.
(** ** Properties of the [sublist] predicate *)
Lemma sublist_length l1 l2 : l1 `sublist` l2 → length l1 ≤ length l2.
Lemma sublist_length l1 l2 : l1 `sublist_of` l2 → length l1 ≤ length l2.
Proof. induction 1; simpl; auto with arith. Qed.
Lemma sublist_nil_l l : [] `sublist` l.
Lemma sublist_nil_l l : [] `sublist_of` l.
Proof. induction l; try constructor; auto. Qed.
Lemma sublist_nil_r l : l `sublist` [] ↔ l = [].
Lemma sublist_nil_r l : l `sublist_of` [] ↔ l = [].
Proof. split. by inversion 1. intros ->. constructor. Qed.
Lemma sublist_app l1 l2 k1 k2 :
l1 `sublist` l2 → k1 `sublist` k2 → l1 ++ k1 `sublist` l2 ++ k2.
l1 `sublist_of` l2 → k1 `sublist_of` k2 → l1 ++ k1 `sublist_of` l2 ++ k2.
Proof. induction 1; simpl; try constructor; auto. Qed.
Lemma sublist_inserts_l k l1 l2 : l1 `sublist` l2 → l1 `sublist` k ++ l2.
Lemma sublist_inserts_l k l1 l2 : l1 `sublist_of` l2 → l1 `sublist_of` k ++ l2.
Proof. induction k; try constructor; auto. Qed.
Lemma sublist_inserts_r k l1 l2 : l1 `sublist` l2 → l1 `sublist` l2 ++ k.
Lemma sublist_inserts_r k l1 l2 : l1 `sublist_of` l2 → l1 `sublist_of` l2 ++ k.
Proof. induction 1; simpl; try constructor; auto using sublist_nil_l. Qed.
Lemma sublist_cons_r x l k :
l `sublist` x :: k ↔ l `sublist` k ∨ ∃ l', l = x :: l' ∧ l' `sublist` k.
l `sublist_of` x :: k ↔ l `sublist_of` k ∨ ∃ l', l = x :: l' ∧ l' `sublist_of` k.
Proof. split. inversion 1; eauto. intros [?|(?&->&?)]; constructor; auto. Qed.
Lemma sublist_cons_l x l k :
x :: l `sublist` k ↔ ∃ k1 k2, k = k1 ++ x :: k2 ∧ l `sublist` k2.
x :: l `sublist_of` k ↔ ∃ k1 k2, k = k1 ++ x :: k2 ∧ l `sublist_of` k2.
Proof.
split.
- intros Hlk. induction k as [|y k IH]; inversion Hlk.
......@@ -1702,8 +1702,8 @@ Proof.
- intros (k1&k2&->&?). by apply sublist_inserts_l, sublist_skip.
Qed.
Lemma sublist_app_r l k1 k2 :
l `sublist` k1 ++ k2 ↔
∃ l1 l2, l = l1 ++ l2 ∧ l1 `sublist` k1 ∧ l2 `sublist` k2.
l `sublist_of` k1 ++ k2 ↔
∃ l1 l2, l = l1 ++ l2 ∧ l1 `sublist_of` k1 ∧ l2 `sublist_of` k2.
Proof.
split.
- revert l k2. induction k1 as [|y k1 IH]; intros l k2; simpl.
......@@ -1716,8 +1716,8 @@ Proof.
- intros (?&?&?&?&?); subst. auto using sublist_app.
Qed.
Lemma sublist_app_l l1 l2 k :
l1 ++ l2 `sublist` k ↔
∃ k1 k2, k = k1 ++ k2 ∧ l1 `sublist` k1 ∧ l2 `sublist` k2.
l1 ++ l2 `sublist_of` k ↔
∃ k1 k2, k = k1 ++ k2 ∧ l1 `sublist_of` k1 ∧ l2 `sublist_of` k2.
Proof.
split.
- revert l2 k. induction l1 as [|x l1 IH]; intros l2 k; simpl.
......@@ -1728,14 +1728,14 @@ Proof.
auto using sublist_inserts_l, sublist_skip.
- intros (?&?&?&?&?); subst. auto using sublist_app.
Qed.
Lemma sublist_app_inv_l k l1 l2 : k ++ l1 `sublist` k ++ l2 → l1 `sublist` l2.
Lemma sublist_app_inv_l k l1 l2 : k ++ l1 `sublist_of` k ++ l2 → l1 `sublist_of` l2.
Proof.
induction k as [|y k IH]; simpl; [done |].
rewrite sublist_cons_r. intros [Hl12|(?&?&?)]; [|simplify_eq; eauto].
rewrite sublist_cons_l in Hl12. destruct Hl12 as (k1&k2&Hk&?).
apply IH. rewrite Hk. eauto using sublist_inserts_l, sublist_cons.
Qed.
Lemma sublist_app_inv_r k l1 l2 : l1 ++ k `sublist` l2 ++ k → l1 `sublist` l2.
Lemma sublist_app_inv_r k l1 l2 : l1 ++ k `sublist_of` l2 ++ k → l1 `sublist_of` l2.
Proof.
revert l1 l2. induction k as [|y k IH]; intros l1 l2.
{ by rewrite !(right_id_L [] (++)). }
......@@ -1760,18 +1760,18 @@ Proof.
induction Hl12; f_equal/=; auto with arith.
apply sublist_length in Hl12. lia.
Qed.
Lemma sublist_take l i : take i l `sublist` l.
Lemma sublist_take l i : take i l `sublist_of` l.
Proof. rewrite <-(take_drop i l) at 2. by apply sublist_inserts_r. Qed.
Lemma sublist_drop l i : drop i l `sublist` l.
Lemma sublist_drop l i : drop i l `sublist_of` l.
Proof. rewrite <-(take_drop i l) at 2. by apply sublist_inserts_l. Qed.
Lemma sublist_delete l i : delete i l `sublist` l.
Lemma sublist_delete l i : delete i l `sublist_of` l.
Proof. revert i. by induction l; intros [|?]; simpl; constructor. Qed.
Lemma sublist_foldr_delete l is : foldr delete l is `sublist` l.
Lemma sublist_foldr_delete l is : foldr delete l is `sublist_of` l.
Proof.
induction is as [|i is IH]; simpl; [done |].
trans (foldr delete l is); auto using sublist_delete.
Qed.
Lemma sublist_alt l1 l2 : l1 `sublist` l2 ↔ ∃ is, l1 = foldr delete l2 is.
Lemma sublist_alt l1 l2 : l1 `sublist_of` l2 ↔ ∃ is, l1 = foldr delete l2 is.
Proof.
split; [|intros [is ->]; apply sublist_foldr_delete].
intros Hl12. cut (∀ k, ∃ is, k ++ l1 = foldr delete (k ++ l2) is).
......@@ -1784,7 +1784,7 @@ Proof.
rewrite fold_right_app. simpl. by rewrite delete_middle.
Qed.
Lemma Permutation_sublist l1 l2 l3 :
l1 ≡ₚ l2 → l2 `sublist` l3 → ∃ l4, l1 `sublist` l4 ∧ l4 ≡ₚ l3.
l1 ≡ₚ l2 → l2 `sublist_of` l3 → ∃ l4, l1 `sublist_of` l4 ∧ l4 ≡ₚ l3.
Proof.
intros Hl1l2. revert l3.
induction Hl1l2 as [|x l1 l2 ? IH|x y l1|l1 l1' l2 ? IH1 ? IH2].
......@@ -1802,7 +1802,7 @@ Proof.
split. done. etrans; eauto.
Qed.
Lemma sublist_Permutation l1 l2 l3 :