Commit 487cdead authored by Robbert Krebbers's avatar Robbert Krebbers

Some minor cleanup, and more lemmas on prefix/postfixes of lists.

parent a89a1e98
...@@ -290,7 +290,7 @@ Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : C_scope. ...@@ -290,7 +290,7 @@ Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : C_scope.
Notation "x ← y ; z" := (y = (λ x : _, z)) Notation "x ← y ; z" := (y = (λ x : _, z))
(at level 65, only parsing, next at level 35, right associativity) : C_scope. (at level 65, only parsing, next at level 35, right associativity) : C_scope.
Infix "<$>" := fmap (at level 65, right associativity) : C_scope. Infix "<$>" := fmap (at level 60, right associativity) : C_scope.
Class MGuard (M : Type Type) := Class MGuard (M : Type Type) :=
mguard: P {dec : Decision P} {A}, M A M A. mguard: P {dec : Decision P} {A}, M A M A.
...@@ -425,6 +425,10 @@ Arguments left_absorb {_ _} _ _ {_} _. ...@@ -425,6 +425,10 @@ Arguments left_absorb {_ _} _ _ {_} _.
Arguments right_absorb {_ _} _ _ {_} _. Arguments right_absorb {_ _} _ _ {_} _.
Arguments anti_symmetric {_} _ {_} _ _ _ _. Arguments anti_symmetric {_} _ {_} _ _ _ _.
Instance: Commutative () (@eq A).
Proof. red. intuition. Qed.
Instance: Commutative () (λ x y, @eq A y x).
Proof. red. intuition. Qed.
Instance: Commutative () (). Instance: Commutative () ().
Proof. red. intuition. Qed. Proof. red. intuition. Qed.
Instance: Commutative () (). Instance: Commutative () ().
...@@ -672,13 +676,11 @@ Section prod_relation. ...@@ -672,13 +676,11 @@ Section prod_relation.
End prod_relation. End prod_relation.
(** ** Other *) (** ** Other *)
Definition lift_relation {A B} (R : relation A) Definition proj_relation {A B} (R : relation A)
(f : B A) : relation B := λ x y, R (f x) (f y). (f : B A) : relation B := λ x y, R (f x) (f y).
Definition lift_relation_equivalence {A B} (R : relation A) (f : B A) : Definition proj_relation_equivalence {A B} (R : relation A) (f : B A) :
Equivalence R Equivalence (lift_relation R f). Equivalence R Equivalence (proj_relation R f).
Proof. unfold lift_relation. firstorder auto. Qed. Proof. unfold proj_relation. firstorder auto. Qed.
Hint Extern 0 (Equivalence (lift_relation _ _)) =>
eapply @lift_relation_equivalence : typeclass_instances.
Instance: A B (x : B), Commutative (=) (λ _ _ : A, x). Instance: A B (x : B), Commutative (=) (λ _ _ : A, x).
Proof. red. trivial. Qed. Proof. red. trivial. Qed.
......
...@@ -46,6 +46,17 @@ Ltac solve_decision := intros; first ...@@ -46,6 +46,17 @@ Ltac solve_decision := intros; first
[ solve_trivial_decision [ solve_trivial_decision
| unfold Decision; decide equality; solve_trivial_decision ]. | unfold Decision; decide equality; solve_trivial_decision ].
(** The following combinators are useful to create Decision proofs in
combination with the [refine] tactic. *)
Notation cast_if S := (if S then left _ else right _).
Notation cast_if_and S1 S2 := (if S1 then cast_if S2 else right _).
Notation cast_if_and3 S1 S2 S3 := (if S1 then cast_if_and S2 S3 else right _).
Notation cast_if_and4 S1 S2 S3 S4 :=
(if S1 then cast_if_and3 S2 S3 S4 else right _).
Notation cast_if_or S1 S2 := (if S1 then left _ else cast_if S2).
Notation cast_if_not_or S1 S2 := (if S1 then cast_if S2 else left _).
Notation cast_if_not S := (if S then right _ else left _).
(** We can convert decidable propositions to booleans. *) (** We can convert decidable propositions to booleans. *)
Definition bool_decide (P : Prop) {dec : Decision P} : bool := Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
if dec then true else false. if dec then true else false.
...@@ -66,8 +77,7 @@ Definition proj2_dsig `{∀ x : A, Decision (P x)} (x : dsig P) : P (`x) := ...@@ -66,8 +77,7 @@ Definition proj2_dsig `{∀ x : A, Decision (P x)} (x : dsig P) : P (`x) :=
bool_decide_unpack _ (proj2_sig x). bool_decide_unpack _ (proj2_sig x).
Definition dexist `{ x : A, Decision (P x)} (x : A) (p : P x) : dsig P := Definition dexist `{ x : A, Decision (P x)} (x : A) (p : P x) : dsig P :=
xbool_decide_pack _ p. xbool_decide_pack _ p.
Lemma dsig_eq `(P : A Prop) `{ x, Decision (P x)}
Lemma dsig_eq {A} (P : A Prop) {dec : x, Decision (P x)}
(x y : dsig P) : x = y `x = `y. (x y : dsig P) : x = y `x = `y.
Proof. Proof.
split. split.
...@@ -78,16 +88,13 @@ Proof. ...@@ -78,16 +88,13 @@ Proof.
+ by intros [] []. + by intros [] [].
+ done. + done.
Qed. Qed.
Lemma dexists_proj1 `(P : A Prop) `{ x, Decision (P x)} (x : dsig P) p :
dexist (`x) p = x.
Proof. by apply dsig_eq. Qed.
(** The following combinators are useful to create Decision proofs in Global Instance dsig_eq_dec `(P : A Prop) `{ x, Decision (P x)}
combination with the [refine] tactic. *) `{ x y : A, Decision (x = y)} (x y : dsig P) : Decision (x = y).
Notation cast_if S := (if S then left _ else right _). Proof. refine (cast_if (decide (`x = `y))); by rewrite dsig_eq. Defined.
Notation cast_if_and S1 S2 := (if S1 then cast_if S2 else right _).
Notation cast_if_and3 S1 S2 S3 := (if S1 then cast_if_and S2 S3 else right _).
Notation cast_if_and4 S1 S2 S3 S4 :=
(if S1 then cast_if_and3 S2 S3 S4 else right _).
Notation cast_if_or S1 S2 := (if S1 then left _ else cast_if S2).
Notation cast_if_not S := (if S then right _ else left _).
(** * Instances of Decision *) (** * Instances of Decision *)
(** Instances of [Decision] for operators of propositional logic. *) (** Instances of [Decision] for operators of propositional logic. *)
......
...@@ -105,10 +105,26 @@ Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A := ...@@ -105,10 +105,26 @@ Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
end. end.
Arguments resize {_} !_ _ !_. 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.
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 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. Definition suffix_of {A} (l1 l2 : list A) : Prop := k, l2 = k ++ l1.
Definition prefix_of {A} (l1 l2 : list A) : Prop := k, l2 = l1 ++ k.
Definition max_prefix_of `{ x y : A, Decision (x = y)} :
list A list A list A * list A * list A :=
fix go l1 l2 :=
match l1, l2 with
| [], l2 => ([], l2, [])
| l1, [] => (l1, [], [])
| x1 :: l1, x2 :: l2 =>
if decide_rel (=) x1 x2
then snd_map (x1 ::) (go l1 l2)
else (x1 :: l1, x2 :: l2, [])
end.
Definition max_suffix_of `{ x y : A, Decision (x = y)} (l1 l2 : list A) :
list A * list A * list A :=
match max_prefix_of (reverse l1) (reverse l2) with
| (k1, k2, k3) => (reverse k1, reverse k2, reverse k3)
end.
(** * Tactics on lists *) (** * Tactics on lists *)
Lemma cons_inv {A} (l1 l2 : list A) x1 x2 : Lemma cons_inv {A} (l1 l2 : list A) x1 x2 :
...@@ -122,7 +138,7 @@ Tactic Notation "discriminate_list_equality" hyp(H) := ...@@ -122,7 +138,7 @@ Tactic Notation "discriminate_list_equality" hyp(H) :=
repeat (simpl in H || rewrite app_length in H); repeat (simpl in H || rewrite app_length in H);
exfalso; lia. exfalso; lia.
Tactic Notation "discriminate_list_equality" := Tactic Notation "discriminate_list_equality" :=
repeat_on_hyps (fun H => discriminate_list_equality H). solve [repeat_on_hyps (fun H => discriminate_list_equality H)].
(** The tactic [simplify_list_equality] simplifies assumptions involving (** The tactic [simplify_list_equality] simplifies assumptions involving
equalities on lists. *) equalities on lists. *)
...@@ -153,6 +169,12 @@ Global Instance: ∀ k : list A, Injective (=) (=) (k ++). ...@@ -153,6 +169,12 @@ Global Instance: ∀ k : list A, Injective (=) (=) (k ++).
Proof. intros ???. apply app_inv_head. Qed. Proof. intros ???. apply app_inv_head. Qed.
Global Instance: k : list A, Injective (=) (=) (++ k). Global Instance: k : list A, Injective (=) (=) (++ k).
Proof. intros ???. apply app_inv_tail. Qed. Proof. intros ???. apply app_inv_tail. Qed.
Global Instance: Associative (=) (@app A).
Proof. intros ???. apply app_assoc. Qed.
Global Instance: LeftId (=) [] (@app A).
Proof. done. Qed.
Global Instance: RightId (=) [] (@app A).
Proof. intro. apply app_nil_r. Qed.
Lemma app_inj (l1 k1 l2 k2 : list A) : Lemma app_inj (l1 k1 l2 k2 : list A) :
length l1 = length k1 length l1 = length k1
...@@ -532,6 +554,8 @@ Qed. ...@@ -532,6 +554,8 @@ Qed.
Lemma reverse_nil : reverse [] = @nil A. Lemma reverse_nil : reverse [] = @nil A.
Proof. done. Qed. Proof. done. Qed.
Lemma reverse_singleton (x : A) : reverse [x] = [x].
Proof. done. Qed.
Lemma reverse_cons (l : list A) x : reverse (x :: l) = reverse l ++ [x]. Lemma reverse_cons (l : list A) x : reverse (x :: l) = reverse l ++ [x].
Proof. unfold reverse. by rewrite <-!rev_alt. Qed. Proof. unfold reverse. by rewrite <-!rev_alt. Qed.
Lemma reverse_snoc (l : list A) x : reverse (l ++ [x]) = x :: reverse l. Lemma reverse_snoc (l : list A) x : reverse (l ++ [x]) = x :: reverse l.
...@@ -704,7 +728,7 @@ Lemma resize_le (l : list A) n x : ...@@ -704,7 +728,7 @@ Lemma resize_le (l : list A) n x :
resize n x l = take n l. resize n x l = take n l.
Proof. Proof.
intros. rewrite resize_spec, (proj2 (NPeano.Nat.sub_0_le _ _)) by done. intros. rewrite resize_spec, (proj2 (NPeano.Nat.sub_0_le _ _)) by done.
simpl. by rewrite app_nil_r. simpl. by rewrite (right_id [] (++)).
Qed. Qed.
Lemma resize_all (l : list A) x : Lemma resize_all (l : list A) x :
...@@ -720,7 +744,7 @@ Lemma resize_plus (l : list A) n m x : ...@@ -720,7 +744,7 @@ Lemma resize_plus (l : list A) n m x :
Proof. Proof.
revert n m. revert n m.
induction l; intros [|?] [|?]; simpl; f_equal; auto. induction l; intros [|?] [|?]; simpl; f_equal; auto.
* by rewrite plus_0_r, app_nil_r. * by rewrite plus_0_r, (right_id [] (++)).
* by rewrite replicate_plus. * by rewrite replicate_plus.
Qed. Qed.
Lemma resize_plus_eq (l : list A) n m x : Lemma resize_plus_eq (l : list A) n m x :
...@@ -743,7 +767,7 @@ Lemma resize_app_ge (l1 l2 : list A) n x : ...@@ -743,7 +767,7 @@ Lemma resize_app_ge (l1 l2 : list A) n x :
resize n x (l1 ++ l2) = l1 ++ resize (n - length l1) x l2. resize n x (l1 ++ l2) = l1 ++ resize (n - length l1) x l2.
Proof. Proof.
intros. intros.
rewrite !resize_spec, take_app_ge, app_assoc by done. rewrite !resize_spec, take_app_ge, (associative (++)) by done.
do 2 f_equal. rewrite app_length. lia. do 2 f_equal. rewrite app_length. lia.
Qed. Qed.
...@@ -1205,18 +1229,21 @@ Section prefix_postfix. ...@@ -1205,18 +1229,21 @@ Section prefix_postfix.
Global Instance: PreOrder (@prefix_of A). Global Instance: PreOrder (@prefix_of A).
Proof. Proof.
split. split.
* intros ?. eexists []. by rewrite app_nil_r. * intros ?. eexists []. by rewrite (right_id [] (++)).
* intros ??? [k1 ?] [k2 ?]. * intros ??? [k1 ?] [k2 ?].
exists (k1 ++ k2). subst. by rewrite app_assoc. exists (k1 ++ k2). subst. by rewrite (associative (++)).
Qed. Qed.
Lemma prefix_of_nil (l : list A) : prefix_of [] l. Lemma prefix_of_nil (l : list A) : prefix_of [] l.
Proof. by exists l. Qed. Proof. by exists l. Qed.
Lemma prefix_of_nil_not x (l : list A) : ¬prefix_of (x :: l) []. Lemma prefix_of_nil_not x (l : list A) : ¬prefix_of (x :: l) [].
Proof. by intros [k E]. Qed. Proof. by intros [k E]. Qed.
Lemma prefix_of_cons x y (l1 l2 : list A) : Lemma prefix_of_cons x (l1 l2 : list A) :
prefix_of l1 l2 prefix_of (x :: l1) (x :: l2).
Proof. intros [k E]. exists k. by subst. Qed.
Lemma prefix_of_cons_alt x y (l1 l2 : list A) :
x = y prefix_of l1 l2 prefix_of (x :: l1) (y :: l2). x = y prefix_of l1 l2 prefix_of (x :: l1) (y :: l2).
Proof. intros ? [k E]. exists k. by subst. Qed. Proof. intro. subst. apply prefix_of_cons. Qed.
Lemma prefix_of_cons_inv_1 x y (l1 l2 : list A) : Lemma prefix_of_cons_inv_1 x y (l1 l2 : list A) :
prefix_of (x :: l1) (y :: l2) x = y. prefix_of (x :: l1) (y :: l2) x = y.
Proof. intros [k E]. by injection E. Qed. Proof. intros [k E]. by injection E. Qed.
...@@ -1224,20 +1251,128 @@ Section prefix_postfix. ...@@ -1224,20 +1251,128 @@ Section prefix_postfix.
prefix_of (x :: l1) (y :: l2) prefix_of l1 l2. prefix_of (x :: l1) (y :: l2) prefix_of l1 l2.
Proof. intros [k E]. exists k. by injection E. Qed. Proof. intros [k E]. exists k. by injection E. Qed.
Lemma prefix_of_app k (l1 l2 : list A) :
prefix_of l1 l2 prefix_of (k ++ l1) (k ++ l2).
Proof. intros [k' ?]. subst. exists k'. by rewrite (associative (++)). Qed.
Lemma prefix_of_app_alt k1 k2 (l1 l2 : list A) :
k1 = k2 prefix_of l1 l2 prefix_of (k1 ++ l1) (k2 ++ l2).
Proof. intro. subst. apply prefix_of_app. Qed.
Lemma prefix_of_app_l (l1 l2 l3 : list A) : Lemma prefix_of_app_l (l1 l2 l3 : list A) :
prefix_of (l1 ++ l3) l2 prefix_of l1 l2. prefix_of (l1 ++ l3) l2 prefix_of l1 l2.
Proof. intros [k ?]. red. exists (l3 ++ k). subst. by rewrite <-app_assoc. Qed. Proof.
intros [k ?]. red. exists (l3 ++ k). subst.
by rewrite <-(associative (++)).
Qed.
Lemma prefix_of_app_r (l1 l2 l3 : list A) : Lemma prefix_of_app_r (l1 l2 l3 : list A) :
prefix_of l1 l2 prefix_of l1 (l2 ++ l3). prefix_of l1 l2 prefix_of l1 (l2 ++ l3).
Proof. intros [k ?]. exists (k ++ l3). subst. by rewrite app_assoc. Qed. Proof.
intros [k ?]. exists (k ++ l3). subst.
by rewrite (associative (++)).
Qed.
Lemma prefix_of_length (l1 l2 : list A) :
prefix_of l1 l2 length l1 length l2.
Proof. intros [??]. subst. rewrite app_length. lia. Qed.
Lemma prefix_of_snoc_not (l : list A) x : ¬prefix_of (l ++ [x]) l.
Proof. intros [??]. discriminate_list_equality. Qed.
Global Instance: PreOrder (@suffix_of A). Global Instance: PreOrder (@suffix_of A).
Proof. Proof.
split. split.
* intros ?. by eexists []. * intros ?. by eexists [].
* intros ??? [k1 ?] [k2 ?]. * intros ??? [k1 ?] [k2 ?].
exists (k2 ++ k1). subst. by rewrite app_assoc. exists (k2 ++ k1). subst. by rewrite (associative (++)).
Qed.
Global Instance prefix_of_dec `{ x y : A, Decision (x = y)} :
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_alt _ _ _ _ Exy Hl1l2)
| right Hl1l2 => right (Hl1l2 prefix_of_cons_inv_2 _ _ _ _)
end
| right Exy => right (Exy prefix_of_cons_inv_1 _ _ _ _)
end
end.
Section max_prefix_of.
Context `{ x y : A, Decision (x = y)}.
Lemma max_prefix_of_fst (l1 l2 : list A) :
l1 = snd (max_prefix_of l1 l2) ++ fst (fst (max_prefix_of l1 l2)).
Proof.
revert l2. induction l1; intros [|??]; simpl;
repeat case_decide; simpl; f_equal; auto.
Qed.
Lemma max_prefix_of_fst_alt (l1 l2 : list A) k1 k2 k3 :
max_prefix_of l1 l2 = (k1,k2,k3) l1 = k3 ++ k1.
Proof.
intro. pose proof (max_prefix_of_fst l1 l2).
by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
Qed.
Lemma max_prefix_of_fst_prefix (l1 l2 : list A) :
prefix_of (snd (max_prefix_of l1 l2)) l1.
Proof. eexists. apply max_prefix_of_fst. Qed.
Lemma max_prefix_of_fst_prefix_alt (l1 l2 : list A) k1 k2 k3 :
max_prefix_of l1 l2 = (k1,k2,k3) prefix_of k3 l1.
Proof. eexists. eauto using max_prefix_of_fst_alt. Qed.
Lemma max_prefix_of_snd (l1 l2 : list A) :
l2 = snd (max_prefix_of l1 l2) ++ snd (fst (max_prefix_of l1 l2)).
Proof.
revert l2. induction l1; intros [|??]; simpl;
repeat case_decide; simpl; f_equal; auto.
Qed.
Lemma max_prefix_of_snd_alt (l1 l2 : list A) k1 k2 k3 :
max_prefix_of 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_equality.
Qed. Qed.
Lemma max_prefix_of_snd_prefix (l1 l2 : list A) :
prefix_of (snd (max_prefix_of l1 l2)) l2.
Proof. eexists. apply max_prefix_of_snd. Qed.
Lemma max_prefix_of_snd_prefix_alt (l1 l2 : list A) k1 k2 k3 :
max_prefix_of l1 l2 = (k1,k2,k3) prefix_of k3 l2.
Proof. eexists. eauto using max_prefix_of_snd_alt. Qed.
Lemma max_prefix_of_max (l1 l2 : list A) k :
prefix_of k l1
prefix_of k l2
prefix_of k (snd (max_prefix_of l1 l2)).
Proof.
intros [l1' ?] [l2' ?]. subst.
by induction k; simpl; repeat case_decide; simpl;
auto using prefix_of_nil, prefix_of_cons.
Qed.
Lemma max_prefix_of_max_alt (l1 l2 : list A) k1 k2 k3 k :
max_prefix_of l1 l2 = (k1,k2,k3)
prefix_of k l1
prefix_of k l2
prefix_of k k3.
Proof.
intro. pose proof (max_prefix_of_max l1 l2 k).
by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
Qed.
Lemma max_prefix_of_max_snoc (l1 l2 : list A) k1 k2 k3 x1 x2 :
max_prefix_of l1 l2 = (x1 :: k1, x2 :: k2, k3)
x1 x2.
Proof.
intros Hl ?. subst. 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.
Qed.
End max_prefix_of.
Lemma prefix_suffix_reverse (l1 l2 : list A) : Lemma prefix_suffix_reverse (l1 l2 : list A) :
prefix_of l1 l2 suffix_of (reverse l1) (reverse l2). prefix_of l1 l2 suffix_of (reverse l1) (reverse l2).
...@@ -1251,15 +1386,24 @@ Section prefix_postfix. ...@@ -1251,15 +1386,24 @@ Section prefix_postfix.
Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed. Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.
Lemma suffix_of_nil (l : list A) : suffix_of [] l. Lemma suffix_of_nil (l : list A) : suffix_of [] l.
Proof. exists l. by rewrite app_nil_r. Qed. Proof. exists l. by rewrite (right_id [] (++)). Qed.
Lemma suffix_of_nil_inv (l : list A) : suffix_of l [] l = []. Lemma suffix_of_nil_inv (l : list A) : suffix_of l [] l = [].
Proof. by intros [[|?] ?]; simplify_list_equality. Qed. Proof. by intros [[|?] ?]; simplify_list_equality. Qed.
Lemma suffix_of_cons_nil_inv x (l : list A) : ¬suffix_of (x :: l) []. Lemma suffix_of_cons_nil_inv x (l : list A) : ¬suffix_of (x :: l) [].
Proof. by intros [[] ?]. Qed. Proof. by intros [[] ?]. Qed.
Lemma suffix_of_snoc (l1 l2 : list A) x :
suffix_of l1 l2 suffix_of (l1 ++ [x]) (l2 ++ [x]).
Proof. intros [k E]. exists k. subst. by rewrite (associative (++)). Qed.
Lemma suffix_of_snoc_alt x y (l1 l2 : list A) :
x = y suffix_of l1 l2 suffix_of (l1 ++ [x]) (l2 ++ [y]).
Proof. intro. subst. apply suffix_of_snoc. Qed.
Lemma suffix_of_app (l1 l2 k : list A) : Lemma suffix_of_app (l1 l2 k : list A) :
suffix_of l1 l2 suffix_of (l1 ++ k) (l2 ++ k). suffix_of l1 l2 suffix_of (l1 ++ k) (l2 ++ k).
Proof. intros [k' E]. exists k'. subst. by rewrite app_assoc. Qed. Proof. intros [k' E]. exists k'. subst. by rewrite (associative (++)). Qed.
Lemma suffix_of_app_alt (l1 l2 k1 k2 : list A) :
k1 = k2 suffix_of l1 l2 suffix_of (l1 ++ k1) (l2 ++ k2).
Proof. intro. subst. apply suffix_of_app. Qed.
Lemma suffix_of_snoc_inv_1 x y (l1 l2 : list A) : Lemma suffix_of_snoc_inv_1 x y (l1 l2 : list A) :
suffix_of (l1 ++ [x]) (l2 ++ [y]) x = y. suffix_of (l1 ++ [x]) (l2 ++ [y]) x = y.
...@@ -1276,17 +1420,25 @@ Section prefix_postfix. ...@@ -1276,17 +1420,25 @@ Section prefix_postfix.
Lemma suffix_of_cons_l (l1 l2 : list A) x : Lemma suffix_of_cons_l (l1 l2 : list A) x :
suffix_of (x :: l1) l2 suffix_of l1 l2. suffix_of (x :: l1) l2 suffix_of l1 l2.
Proof. intros [k ?]. exists (k ++ [x]). subst. by rewrite <-app_assoc. Qed. Proof.
intros [k ?]. exists (k ++ [x]). subst.
by rewrite <-(associative (++)).
Qed.
Lemma suffix_of_app_l (l1 l2 l3 : list A) : Lemma suffix_of_app_l (l1 l2 l3 : list A) :
suffix_of (l3 ++ l1) l2 suffix_of l1 l2. suffix_of (l3 ++ l1) l2 suffix_of l1 l2.
Proof. intros [k ?]. exists (k ++ l3). subst. by rewrite <-app_assoc. Qed. Proof.
intros [k ?]. exists (k ++ l3). subst.
by rewrite <-(associative (++)).
Qed.
Lemma suffix_of_cons_r (l1 l2 : list A) x : Lemma suffix_of_cons_r (l1 l2 : list A) x :
suffix_of l1 l2 suffix_of l1 (x :: l2). suffix_of l1 l2 suffix_of l1 (x :: l2).
Proof. intros [k ?]. exists (x :: k). by subst. Qed. Proof. intros [k ?]. exists (x :: k). by subst. Qed.
Lemma suffix_of_app_r (l1 l2 l3 : list A) : Lemma suffix_of_app_r (l1 l2 l3 : list A) :
suffix_of l1 l2 suffix_of l1 (l3 ++ l2). suffix_of l1 l2 suffix_of l1 (l3 ++ l2).
Proof. intros [k ?]. exists (l3 ++ k). subst. by rewrite app_assoc. Qed. Proof.
intros [k ?]. exists (l3 ++ k). subst.
by rewrite (associative (++)).
Qed.
Lemma suffix_of_cons_inv (l1 l2 : list A) x y : Lemma suffix_of_cons_inv (l1 l2 : list A) x y :
suffix_of (x :: l1) (y :: l2) suffix_of (x :: l1) (y :: l2)
...@@ -1297,44 +1449,98 @@ Section prefix_postfix. ...@@ -1297,44 +1449,98 @@ Section prefix_postfix.
* right. simplify_equality. by apply suffix_of_app_r. * right. simplify_equality. by apply suffix_of_app_r.
Qed. Qed.
Lemma suffix_of_length (l1 l2 : list A) :
suffix_of l1 l2 length l1 length l2.
Proof. intros [??]. subst. rewrite app_length. lia. Qed.
Lemma suffix_of_cons_not x (l : list A) : ¬suffix_of (x :: l) l. Lemma suffix_of_cons_not x (l : list A) : ¬suffix_of (x :: l) l.
Proof. intros [??]. discriminate_list_equality. Qed. Proof. intros [??]. discriminate_list_equality. Qed.
Context `{ x y : A, Decision (x = y)}. Global Instance suffix_of_dec `{ x y : A, Decision (x = y)}
(l1 l2 : list A) : Decision (suffix_of l1 l2).
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. Proof.
refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2))); refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
abstract (by rewrite suffix_prefix_reverse). abstract (by rewrite suffix_prefix_reverse).
Defined. Defined.
Section max_suffix_of.
Context `{ x y : A, Decision (x = y)}.
Lemma max_suffix_of_fst (l1 l2 : list A) :
l1 = fst (fst (max_suffix_of l1 l2)) ++ snd (max_suffix_of l1 l2).
Proof.
rewrite <-(reverse_involutive l1) at 1.
rewrite (max_prefix_of_fst (reverse l1) (reverse l2)).