Commit ddf8ef49 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 66c3aff9
......@@ -101,9 +101,9 @@ Proof.
- by trans (big_op xs2).
Qed.
Lemma big_op_contains xs ys : xs `contains` ys [] xs [] ys.
Lemma big_op_submseteq xs ys : xs + ys [] xs [] ys.
Proof.
intros [xs' ->]%contains_Permutation.
intros [xs' ->]%submseteq_Permutation.
rewrite big_op_app; apply cmra_included_l.
Qed.
......@@ -158,9 +158,9 @@ Section list.
Lemma big_opL_permutation (f : A M) l1 l2 :
l1 ≡ₚ l2 ([ list] x l1, f x) ([ list] x l2, f x).
Proof. intros Hl. by rewrite /big_opL !imap_const Hl. Qed.
Lemma big_opL_contains (f : A M) l1 l2 :
l1 `contains` l2 ([ list] x l1, f x) ([ list] x l2, f x).
Proof. intros Hl. apply big_op_contains. rewrite !imap_const. by rewrite ->Hl. Qed.
Lemma big_opL_submseteq (f : A M) l1 l2 :
l1 + l2 ([ list] x l1, f x) ([ list] x l2, f x).
Proof. intros Hl. apply big_op_submseteq. rewrite !imap_const. by rewrite ->Hl. Qed.
Global Instance big_opL_ne l n :
Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
......@@ -230,7 +230,7 @@ Section gmap.
([ map] k x m1, f k x) [ map] k x m2, g k x.
Proof.
intros Hm Hf. trans ([ map] kx m2, f k x).
- by apply big_op_contains, fmap_contains, map_to_list_contains.
- by apply big_op_submseteq, fmap_submseteq, map_to_list_submseteq.
- apply big_opM_forall; apply _ || auto.
Qed.
Lemma big_opM_ext f g m :
......@@ -345,7 +345,7 @@ Section gset.
([ set] x X, f x) [ set] x Y, g x.
Proof.
intros HX Hf. trans ([ set] x Y, f x).
- by apply big_op_contains, fmap_contains, elements_contains.
- by apply big_op_submseteq, fmap_submseteq, elements_submseteq.
- apply big_opS_forall; apply _ || auto.
Qed.
Lemma big_opS_ext f g X :
......@@ -446,7 +446,7 @@ Section gmultiset.
([ mset] x X, f x) [ mset] x Y, g x.
Proof.
intros HX Hf. trans ([ mset] x Y, f x).
- by apply big_op_contains, fmap_contains, gmultiset_elements_contains.
- by apply big_op_submseteq, fmap_submseteq, gmultiset_elements_submseteq.
- apply big_opMS_forall; apply _ || auto.
Qed.
Lemma big_opMS_ext f g X :
......
......@@ -29,9 +29,9 @@ Module ra_reflection. Section ra_reflection.
by rewrite fmap_app IH1 IH2 big_op_app.
Qed.
Lemma flatten_correct Σ e1 e2 :
flatten e1 `contains` flatten e2 eval Σ e1 eval Σ e2.
flatten e1 + flatten e2 eval Σ e1 eval Σ e2.
Proof.
by intros He; rewrite !eval_flatten; apply big_op_contains; rewrite ->He.
by intros He; rewrite !eval_flatten; apply big_op_submseteq; rewrite ->He.
Qed.
Class Quote (Σ1 Σ2 : list A) (l : A) (e : expr) := {}.
......
......@@ -133,8 +133,8 @@ Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Lemma big_sep_app Ps Qs : [] (Ps ++ Qs) ⊣⊢ [] Ps [] Qs.
Proof. by rewrite big_op_app. Qed.
Lemma big_sep_contains Ps Qs : Qs `contains` Ps [] Ps [] Qs.
Proof. intros. apply uPred_included. by apply: big_op_contains. Qed.
Lemma big_sep_submseteq Ps Qs : Qs + Ps [] Ps [] Qs.
Proof. intros. apply uPred_included. by apply: big_op_submseteq. Qed.
Lemma big_sep_elem_of Ps P : P Ps [] Ps P.
Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
Lemma big_sep_elem_of_acc Ps P : P Ps [] Ps P (P - [] Ps).
......@@ -220,9 +220,9 @@ Section list.
( k y, l !! k = Some y Φ k y ⊣⊢ Ψ k y)
([ list] k y l, Φ k y) ⊣⊢ ([ list] k y l, Ψ k y).
Proof. apply big_opL_proper. Qed.
Lemma big_sepL_contains (Φ : A uPred M) l1 l2 :
l1 `contains` l2 ([ list] y l2, Φ y) [ list] y l1, Φ y.
Proof. intros ?. apply uPred_included. by apply: big_opL_contains. Qed.
Lemma big_sepL_submseteq (Φ : A uPred M) l1 l2 :
l1 + l2 ([ list] y l2, Φ y) [ list] y l1, Φ y.
Proof. intros ?. apply uPred_included. by apply: big_opL_submseteq. Qed.
Global Instance big_sepL_mono' l :
Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
......@@ -353,8 +353,8 @@ Section gmap.
([ map] k x m1, Φ k x) [ map] k x m2, Ψ k x.
Proof.
intros Hm HΦ. trans ([ map] kx m2, Φ k x)%I.
- apply uPred_included. apply: big_op_contains.
by apply fmap_contains, map_to_list_contains.
- apply uPred_included. apply: big_op_submseteq.
by apply fmap_submseteq, map_to_list_submseteq.
- apply big_opM_forall; apply _ || auto.
Qed.
Lemma big_sepM_proper Φ Ψ m :
......@@ -517,8 +517,8 @@ Section gset.
([ set] x X, Φ x) [ set] x Y, Ψ x.
Proof.
intros HX HΦ. trans ([ set] x Y, Φ x)%I.
- apply uPred_included. apply: big_op_contains.
by apply fmap_contains, elements_contains.
- apply uPred_included. apply: big_op_submseteq.
by apply fmap_submseteq, elements_submseteq.
- apply big_opS_forall; apply _ || auto.
Qed.
Lemma big_sepS_proper Φ Ψ X :
......@@ -666,8 +666,8 @@ Section gmultiset.
([ mset] x X, Φ x) [ mset] x Y, Ψ x.
Proof.
intros HX HΦ. trans ([ mset] x Y, Φ x)%I.
- apply uPred_included. apply: big_op_contains.
by apply fmap_contains, gmultiset_elements_contains.
- apply uPred_included. apply: big_op_submseteq.
by apply fmap_submseteq, gmultiset_elements_submseteq.
- apply big_opMS_forall; apply _ || auto.
Qed.
Lemma big_sepMS_proper Φ Ψ X :
......
......@@ -30,9 +30,9 @@ Module uPred_reflection. Section uPred_reflection.
rewrite /= ?right_id ?fmap_app ?big_sep_app ?IH1 ?IH2 //.
Qed.
Lemma flatten_entails Σ e1 e2 :
flatten e2 `contains` flatten e1 eval Σ e1 eval Σ e2.
flatten e2 + flatten e1 eval Σ e1 eval Σ e2.
Proof.
intros. rewrite !eval_flatten. by apply big_sep_contains, fmap_contains.
intros. rewrite !eval_flatten. by apply big_sep_submseteq, fmap_submseteq.
Qed.
Lemma flatten_equiv Σ e1 e2 :
flatten e2 ≡ₚ flatten e1 eval Σ e1 ⊣⊢ eval Σ e2.
......
......@@ -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.