From VLSM.Lib Require Import Itauto.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From stdpp Require Import prelude finite.
From Coq Require Import FinFun.
From VLSM.Lib Require Import Preamble.

Utility: Lemmas About Lists

A list is either empty or it can be decomposed into an initial prefix and the last element.

Lemma has_last_or_null :
  forall {A : Type} (l : list A),
    {l' : list A & {a : A | l = l' ++ (a :: nil)}} + {l = nil}.∀ (A : Type) (l : list A),
  {l' : list A & {a : A | l = l' ++ [a]}} + {l = []}
Proof.∀ (A : Type) (l : list A),
  {l' : list A & {a : A | l = l' ++ [a]}} + {l = []}
  destruct l.A: Type
{l' : list A & {a : A | [] = l' ++ [a]}} + {[] = []}
A: Type
a: A
l: list A
{l' : list A & {a0 : A | a :: l = l' ++ [a0]}} +
{a :: l = []}
  -A: Type
{l' : list A & {a : A | [] = l' ++ [a]}} + {[] = []} by right.
  -A: Type
a: A
l: list A
{l' : list A & {a0 : A | a :: l = l' ++ [a0]}} +
{a :: l = []} by left; apply exists_last.
Qed.

Decompose a list in into a prefix l' and the last element a with an equation Heq stating that l = l' ++ [a].

Ltac destruct_list_last l l' a Heq :=
 destruct (has_last_or_null l) as [[l' [a Heq]] | Heq]; rewrite Heq in *; swap 1 2.

Lemma last_not_null :
  forall {A : Type} (l : list A) (a : A),
    l ++ [a] <> [].∀ (A : Type) (l : list A) (a : A), l ++ [a] ≠ []
Proof.∀ (A : Type) (l : list A) (a : A), l ++ [a] ≠ []
  by destruct l.
Qed.

Return the last element of the list if it's present and None otherwise.

Definition last_error {A : Type} (l : list A) : option A :=
  match l with
  | [] => None
  | a :: t => Some (List.last t a)
  end.

Lemma unfold_last_hd :
  forall {A : Type} (random a b : A) (l : list A),
    List.last (a :: b :: l) random = List.last (b :: l) random.∀ (A : Type) (random a b : A) (l : list A),
  List.last (a :: b :: l) random =
  List.last (b :: l) random
Proof.∀ (A : Type) (random a b : A) (l : list A),
  List.last (a :: b :: l) random =
  List.last (b :: l) random done. Qed.

Lemma swap_head_last :
  forall {A : Type} (random a b c : A) (l : list A),
    List.last (a :: b :: c :: l) random = List.last (b :: a :: c :: l) random.∀ (A : Type) (random a b c : A) (l : list A),
  List.last (a :: b :: c :: l) random =
  List.last (b :: a :: c :: l) random
Proof.∀ (A : Type) (random a b c : A) (l : list A),
  List.last (a :: b :: c :: l) random =
  List.last (b :: a :: c :: l) random
  by induction l.
Qed.

Lemma remove_hd_last :
  forall {A : Type} (hd1 hd2 d1 d2 : A) (tl : list A),
    List.last (hd1 :: hd2 :: tl) d1 = List.last (hd2 :: tl) d2.∀ (A : Type) (hd1 hd2 d1 d2 : A) (tl : list A),
  List.last (hd1 :: hd2 :: tl) d1 =
  List.last (hd2 :: tl) d2
Proof.∀ (A : Type) (hd1 hd2 d1 d2 : A) (tl : list A),
  List.last (hd1 :: hd2 :: tl) d1 =
  List.last (hd2 :: tl) d2
  induction tl; cbn; [done |].A: Type
hd1, hd2, d1, d2, a: A
tl: list A
IHtl: List.last (hd1 :: hd2 :: tl) d1 =
List.last (hd2 :: tl) d2
match tl with
| [] => a
| _ :: _ => List.last tl d1
end =
match tl with
| [] => a
| _ :: _ => List.last tl d2
end
  by destruct tl.
Qed.

Lemma unroll_last :
  forall {A : Type} (random a : A) (l : list A),
    List.last (a :: l) random = List.last l a.∀ (A : Type) (random a : A) (l : list A),
  List.last (a :: l) random = List.last l a
Proof.∀ (A : Type) (random a : A) (l : list A),
  List.last (a :: l) random = List.last l a
  induction l as [| h [| h' t]]; [done.. |].A: Type
random, a, h, h': A
t: list A
IHl: List.last (a :: h' :: t) random =
List.last (h' :: t) a
List.last (a :: h :: h' :: t) random =
List.last (h :: h' :: t) a
  by rewrite swap_head_last, unfold_last_hd, IHl, unfold_last_hd.
Qed.

Lemma last_app :
  forall {A : Type} (l1 l2 : list A) (def : A),
    List.last (l1 ++ l2) def = List.last l2 (List.last l1 def).∀ (A : Type) (l1 l2 : list A) (def : A),
  List.last (l1 ++ l2) def =
  List.last l2 (List.last l1 def)
Proof.∀ (A : Type) (l1 l2 : list A) (def : A),
  List.last (l1 ++ l2) def =
  List.last l2 (List.last l1 def)
  induction l1; intros; [done |].A: Type
a: A
l1: list A
IHl1: ∀ (l2 : list A) (def : A),
  List.last (l1 ++ l2) def =
  List.last l2 (List.last l1 def)
l2: list A
def: A
List.last ((a :: l1) ++ l2) def =
List.last l2 (List.last (a :: l1) def)
  by rewrite <- !app_comm_cons, !unroll_last.
Qed.

Lemma last_map :
  forall {A B : Type} (f : A -> B) (t : list A) (h : A) (def : B),
    List.last (map f (h :: t)) def = f (List.last t h).∀ (A B : Type) (f : A → B) (t : list A) (h : A) (def : B),
  List.last (map f (h :: t)) def = f (List.last t h)
Proof.∀ (A B : Type) (f : A → B) (t : list A) (h : A) (def : B),
  List.last (map f (h :: t)) def = f (List.last t h)
  induction t; intros; [done |].A, B: Type
f: A → B
a: A
t: list A
IHt: ∀ (h : A) (def : B), List.last (map f (h :: t)) def = f (List.last t h)
h: A
def: B
List.last (map f (h :: a :: t)) def =
f (List.last (a :: t) h)
  by rewrite map_cons, !unroll_last.
Qed.

Lemma last_error_some :
  forall {A : Type} (l : list A) (s random : A) (Herr : last_error l = Some s),
    List.last l random = s.∀ (A : Type) (l : list A) (s random : A),
  last_error l = Some s → List.last l random = s
Proof.∀ (A : Type) (l : list A) (s random : A),
  last_error l = Some s → List.last l random = s
  by destruct l; [| inversion 1; apply unroll_last].
Qed.

Lemma incl_singleton :
  forall {A : Type} (l : list A) (a : A),
    l ⊆ [a] -> forall b : A, b ∈ l -> b = a.∀ (A : Type) (l : list A) (a : A),
  l ⊆ [a] → ∀ b : A, b ∈ l → b = a
Proof.∀ (A : Type) (l : list A) (a : A),
  l ⊆ [a] → ∀ b : A, b ∈ l → b = a
  intros * Hsub * Hin.A: Type
l: list A
a: A
Hsub: l ⊆ [a]
b: A
Hin: b ∈ l
b = a
  by apply elem_of_list_singleton, Hsub.
Qed.

Lemma Exists_first :
  forall {A : Type} (P : A -> Prop) (Pdec : forall a : A, Decision (P a)) (l : list A),
    Exists P l ->
    exists (prefix : list A) (suffix : list A) (first : A),
      P first /\
      l = prefix ++ [first] ++ suffix /\
      ~ Exists P prefix.∀ (A : Type) (P : A → Prop),
  (∀ a : A, Decision (P a))
  → ∀ l : list A,
      Exists P l
      → ∃ (prefix suffix : list A) (first : A),
          P first
          ∧ l = prefix ++ [first] ++ suffix
            ∧ ¬ Exists P prefix
Proof.∀ (A : Type) (P : A → Prop),
  (∀ a : A, Decision (P a))
  → ∀ l : list A,
      Exists P l
      → ∃ (prefix suffix : list A) (first : A),
          P first
          ∧ l = prefix ++ [first] ++ suffix
            ∧ ¬ Exists P prefix
  induction l as [| h t]; intros Hex; [by inversion Hex |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
t: list A
IHt: Exists P t
→ ∃ (prefix suffix : list A) (first : A),
    P first
    ∧ t = prefix ++ [first] ++ suffix
      ∧ ¬ Exists P prefix
Hex: Exists P (h :: t)
∃ (prefix suffix : list A) (first : A),
  P first
  ∧ h :: t = prefix ++ [first] ++ suffix
    ∧ ¬ Exists P prefix
  destruct (decide (P h)).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
t: list A
IHt: Exists P t
→ ∃ (prefix suffix : list A) (first : A),
    P first
    ∧ t = prefix ++ [first] ++ suffix
      ∧ ¬ Exists P prefix
Hex: Exists P (h :: t)
p: P h
∃ (prefix suffix : list A) (first : A),
  P first
  ∧ h :: t = prefix ++ [first] ++ suffix
    ∧ ¬ Exists P prefix
A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
t: list A
IHt: Exists P t
→ ∃ (prefix suffix : list A) (first : A),
    P first
    ∧ t = prefix ++ [first] ++ suffix
      ∧ ¬ Exists P prefix
Hex: Exists P (h :: t)
n: ¬ P h
∃ (prefix suffix : list A) (first : A),
  P first
  ∧ h :: t = prefix ++ [first] ++ suffix
    ∧ ¬ Exists P prefix
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
t: list A
IHt: Exists P t
→ ∃ (prefix suffix : list A) (first : A),
    P first
    ∧ t = prefix ++ [first] ++ suffix
      ∧ ¬ Exists P prefix
Hex: Exists P (h :: t)
p: P h
∃ (prefix suffix : list A) (first : A),
  P first
  ∧ h :: t = prefix ++ [first] ++ suffix
    ∧ ¬ Exists P prefix exists [], t, h.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
t: list A
IHt: Exists P t
→ ∃ (prefix suffix : list A) (first : A),
    P first
    ∧ t = prefix ++ [first] ++ suffix
      ∧ ¬ Exists P prefix
Hex: Exists P (h :: t)
p: P h
P h ∧ h :: t = [] ++ [h] ++ t ∧ ¬ Exists P []
    rewrite Exists_nil.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
t: list A
IHt: Exists P t
→ ∃ (prefix suffix : list A) (first : A),
    P first
    ∧ t = prefix ++ [first] ++ suffix
      ∧ ¬ Exists P prefix
Hex: Exists P (h :: t)
p: P h
P h ∧ h :: t = [] ++ [h] ++ t ∧ ¬ False
    by itauto.
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
t: list A
IHt: Exists P t
→ ∃ (prefix suffix : list A) (first : A),
    P first
    ∧ t = prefix ++ [first] ++ suffix
      ∧ ¬ Exists P prefix
Hex: Exists P (h :: t)
n: ¬ P h
∃ (prefix suffix : list A) (first : A),
  P first
  ∧ h :: t = prefix ++ [first] ++ suffix
    ∧ ¬ Exists P prefix apply Exists_cons in Hex as []; [done |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
t: list A
IHt: Exists P t
→ ∃ (prefix suffix : list A) (first : A),
    P first
    ∧ t = prefix ++ [first] ++ suffix
      ∧ ¬ Exists P prefix
H: Exists P t
n: ¬ P h
∃ (prefix suffix : list A) (first : A),
  P first
  ∧ h :: t = prefix ++ [first] ++ suffix
    ∧ ¬ Exists P prefix
    destruct (IHt H) as (prefix & suffix & first & p & -> & Hnex).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
prefix, suffix: list A
first: A
H: Exists P (prefix ++ [first] ++ suffix)
IHt: Exists P (prefix ++ [first] ++ suffix)
→ ∃ (prefix0 suffix0 : list A) (first0 : A),
    P first0
    ∧ prefix ++ [first] ++ suffix =
      prefix0 ++ [first0] ++ suffix0
      ∧ ¬ Exists P prefix0
n: ¬ P h
p: P first
Hnex: ¬ Exists P prefix
∃ (prefix0 suffix0 : list A) (first0 : A),
  P first0
  ∧ h :: prefix ++ [first] ++ suffix =
    prefix0 ++ [first0] ++ suffix0
    ∧ ¬ Exists P prefix0
    exists (h :: prefix), suffix, first.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
prefix, suffix: list A
first: A
H: Exists P (prefix ++ [first] ++ suffix)
IHt: Exists P (prefix ++ [first] ++ suffix)
→ ∃ (prefix0 suffix0 : list A) (first0 : A),
    P first0
    ∧ prefix ++ [first] ++ suffix =
      prefix0 ++ [first0] ++ suffix0
      ∧ ¬ Exists P prefix0
n: ¬ P h
p: P first
Hnex: ¬ Exists P prefix
P first
∧ h :: prefix ++ [first] ++ suffix =
  (h :: prefix) ++ [first] ++ suffix
  ∧ ¬ Exists P (h :: prefix)
    rewrite Exists_cons.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
prefix, suffix: list A
first: A
H: Exists P (prefix ++ [first] ++ suffix)
IHt: Exists P (prefix ++ [first] ++ suffix)
→ ∃ (prefix0 suffix0 : list A) (first0 : A),
    P first0
    ∧ prefix ++ [first] ++ suffix =
      prefix0 ++ [first0] ++ suffix0
      ∧ ¬ Exists P prefix0
n: ¬ P h
p: P first
Hnex: ¬ Exists P prefix
P first
∧ h :: prefix ++ [first] ++ suffix =
  (h :: prefix) ++ [first] ++ suffix
  ∧ ¬ (P h ∨ Exists P prefix)
    by itauto.
Qed.

Lemma map_list_subseteq :
  forall {A B : Type} (f : A -> B) (l1 l2 : list A),
    l1 ⊆ l2 -> map f l1 ⊆ map f l2.∀ (A B : Type) (f : A → B) (l1 l2 : list A),
  l1 ⊆ l2 → map f l1 ⊆ map f l2
Proof.∀ (A B : Type) (f : A → B) (l1 l2 : list A),
  l1 ⊆ l2 → map f l1 ⊆ map f l2
  unfold subseteq, list_subseteq.∀ (A B : Type) (f : A → B) (l1 l2 : list A),
  (∀ x : A, x ∈ l1 → x ∈ l2)
  → ∀ x : B, x ∈ map f l1 → x ∈ map f l2
  intros * Hsub b Hin.A, B: Type
f: A → B
l1, l2: list A
Hsub: ∀ x : A, x ∈ l1 → x ∈ l2
b: B
Hin: b ∈ map f l1
b ∈ map f l2
  rewrite elem_of_list_fmap in Hin |- *.A, B: Type
f: A → B
l1, l2: list A
Hsub: ∀ x : A, x ∈ l1 → x ∈ l2
b: B
Hin: ∃ y : A, b = f y ∧ y ∈ l1
∃ y : A, b = f y ∧ y ∈ l2
  destruct Hin as (x & -> & Hin').A, B: Type
f: A → B
l1, l2: list A
Hsub: ∀ x : A, x ∈ l1 → x ∈ l2
x: A
Hin': x ∈ l1
∃ y : A, f x = f y ∧ y ∈ l2
  exists x.A, B: Type
f: A → B
l1, l2: list A
Hsub: ∀ x : A, x ∈ l1 → x ∈ l2
x: A
Hin': x ∈ l1
f x = f x ∧ x ∈ l2
  by split; [| apply Hsub].
Qed.

Lemma app_cons {A} :
  forall (a : A) (l : list A),
    [a] ++ l = a :: l.A: Type
∀ (a : A) (l : list A), [a] ++ l = a :: l
Proof.A: Type
∀ (a : A) (l : list A), [a] ++ l = a :: l done. Qed.

Lemma last_error_is_last {A} :
  forall (l : list A) (x : A),
    last_error (l ++ [x]) = Some x.A: Type
∀ (l : list A) (x : A), last_error (l ++ [x]) = Some x
Proof.A: Type
∀ (l : list A) (x : A), last_error (l ++ [x]) = Some x
  intros [] x; cbn; [done |].A: Type
a: A
l: list A
x: A
Some (List.last (l ++ [x]) a) = Some x
  by rewrite last_app.
Qed.

Lemma nth_error_last :
  forall {A : Type} (n : nat) (l : list A) (Hlast : S n = length l) (_last : A),
    nth_error l n = Some (List.last l _last).∀ (A : Type) (n : nat) (l : list A),
  S n = length l
  → ∀ _last : A,
      nth_error l n = Some (List.last l _last)
Proof.∀ (A : Type) (n : nat) (l : list A),
  S n = length l
  → ∀ _last : A,
      nth_error l n = Some (List.last l _last)
  intros.A: Type
n: nat
l: list A
Hlast: S n = length l
_last: A
nth_error l n = Some (List.last l _last)
  destruct_list_last l h t Heq; [by destruct n |].A: Type
n: nat
l, h: list A
t: A
Hlast: S n = length (h ++ [t])
_last: A
Heq: l = h ++ [t]
nth_error (h ++ [t]) n =
Some (List.last (h ++ [t]) _last)
  rewrite app_length in Hlast; cbn in Hlast.A: Type
n: nat
l, h: list A
t: A
Hlast: S n = length h + 1
_last: A
Heq: l = h ++ [t]
nth_error (h ++ [t]) n =
Some (List.last (h ++ [t]) _last)
  rewrite nth_error_app2, last_app by lia; cbn.A: Type
n: nat
l, h: list A
t: A
Hlast: S n = length h + 1
_last: A
Heq: l = h ++ [t]
nth_error [t] (n - length h) = Some t
  by replace (n - length h) with 0 by lia.
Qed.

Lemma take_prefix :
  forall {A : Type} (l : list A) (n1 n2 : nat),
    n1 <= n2 -> take n1 (take n2 l) = take n1 l.∀ (A : Type) (l : list A) (n1 n2 : nat),
  n1 ≤ n2 → take n1 (take n2 l) = take n1 l
Proof.∀ (A : Type) (l : list A) (n1 n2 : nat),
  n1 ≤ n2 → take n1 (take n2 l) = take n1 l
  by intros; rewrite take_take, min_l.
Qed.

Lemma prefix_of_take :
  forall {A : Type} (l : list A) (n : nat),
    take n l `prefix_of` l.∀ (A : Type) (l : list A) (n : nat),
  take n l `prefix_of` l
Proof.∀ (A : Type) (l : list A) (n : nat),
  take n l `prefix_of` l by eexists; symmetry; apply take_drop. Qed.

Compute the sublist of list l which starts at index n1 and ends before index n2. For example, list_segment [0; 1; 2; 3; 4; 5] 2 4 = [2; 3].

Definition list_segment {A : Type} (l : list A) (n1 n2 : nat) : list A :=
  drop n1 (take n2 l).

Lemma take_segment_suffix :
  forall {A : Type} (l : list A) (n1 n2 : nat),
    n1 <= n2 -> take n1 l ++ list_segment l n1 n2 ++ drop n2 l = l.∀ (A : Type) (l : list A) (n1 n2 : nat),
  n1 ≤ n2
  → take n1 l ++ list_segment l n1 n2 ++ drop n2 l = l
Proof.∀ (A : Type) (l : list A) (n1 n2 : nat),
  n1 ≤ n2
  → take n1 l ++ list_segment l n1 n2 ++ drop n2 l = l
  intros.A: Type
l: list A
n1, n2: nat
H: n1 ≤ n2
take n1 l ++ list_segment l n1 n2 ++ drop n2 l = l
  unfold list_segment.A: Type
l: list A
n1, n2: nat
H: n1 ≤ n2
take n1 l ++ drop n1 (take n2 l) ++ drop n2 l = l
  rewrite <- (take_drop n2 l) at 4.A: Type
l: list A
n1, n2: nat
H: n1 ≤ n2
take n1 l ++ drop n1 (take n2 l) ++ drop n2 l =
take n2 l ++ drop n2 l
  rewrite <- (take_drop n1 (take n2 l)) at 2.A: Type
l: list A
n1, n2: nat
H: n1 ≤ n2
take n1 l ++ drop n1 (take n2 l) ++ drop n2 l =
(take n1 (take n2 l) ++ drop n1 (take n2 l)) ++
drop n2 l
  by rewrite <- app_assoc, take_prefix.
Qed.

Annotate each element of a list with the proof that it satisfies the given decidable predicate.

Fixpoint list_annotate
  {A : Type} {P : A -> Prop} {Pdec : forall a, Decision (P a)} {l : list A}
   : Forall P l -> list (dsig P) :=
  match l with
  | [] => fun _ => []
  | h :: t => fun Hs => dexist h (Forall_inv Hs) :: list_annotate (Forall_inv_tail Hs)
  end.

Section sec_list_annotate_props.

Context
  {A : Type}
  {P : A -> Prop}
  `{Pdec : forall a, Decision (P a)}
  .

Lemma list_annotate_length :
  forall (l : list A) (Hs : Forall P l),
    length (list_annotate Hs) = length l.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (l : list A) (Hs : Forall P l),
  length (list_annotate Hs) = length l
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (l : list A) (Hs : Forall P l),
  length (list_annotate Hs) = length l
  by induction l; cbn; intros; [| rewrite IHl].
Qed.

Lemma list_annotate_pi :
  forall (l : list A) (Hs : Forall P l) (Hs' : Forall P l),
    list_annotate Hs = list_annotate Hs'.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (l : list A) (Hs Hs' : Forall P l),
  list_annotate Hs = list_annotate Hs'
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (l : list A) (Hs Hs' : Forall P l),
  list_annotate Hs = list_annotate Hs'
  induction l; cbn; intros; [done |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a: A
l: list A
IHl: ∀ Hs Hs' : Forall P l,
  list_annotate Hs = list_annotate Hs'
Hs, Hs': Forall P (a :: l)
dexist a (Forall_inv Hs)
:: list_annotate (Forall_inv_tail Hs) =
dexist a (Forall_inv Hs')
:: list_annotate (Forall_inv_tail Hs')
  by f_equal; [apply dsig_eq | apply IHl].
Qed.

Lemma list_annotate_eq :
  forall (l1 l2 : list A) (Hl1 : Forall P l1) (Hl2 : Forall P l2),
    list_annotate Hl1 = list_annotate Hl2 <-> l1 = l2.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (l1 l2 : list A) (Hl1 : Forall P l1) (Hl2 : Forall P
                                                l2),
  list_annotate Hl1 = list_annotate Hl2 ↔ l1 = l2
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (l1 l2 : list A) (Hl1 : Forall P l1) (Hl2 : Forall P
                                                l2),
  list_annotate Hl1 = list_annotate Hl2 ↔ l1 = l2
  split; [| by intros ->; apply list_annotate_pi].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
l1, l2: list A
Hl1: Forall P l1
Hl2: Forall P l2
list_annotate Hl1 = list_annotate Hl2 → l1 = l2
  revert l2 Hl1 Hl2.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
l1: list A
∀ (l2 : list A) (Hl1 : Forall P l1) (Hl2 : Forall P l2),
  list_annotate Hl1 = list_annotate Hl2 → l1 = l2
  induction l1 as [| h1 t1]; intros [| h2 t2] * Heq; [done.. |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h1: A
t1: list A
IHt1: ∀ (l2 : list A) (Hl1 : Forall P t1) 
  (Hl2 : Forall P l2),
  list_annotate Hl1 = list_annotate Hl2
  → t1 = l2
h2: A
t2: list A
Hl1: Forall P (h1 :: t1)
Hl2: Forall P (h2 :: t2)
Heq: list_annotate Hl1 = list_annotate Hl2
h1 :: t1 = h2 :: t2
  inversion Heq; subst.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
t1: list A
IHt1: ∀ (l2 : list A) (Hl1 : Forall P t1) 
  (Hl2 : Forall P l2),
  list_annotate Hl1 = list_annotate Hl2
  → t1 = l2
h2: A
t2: list A
Hl1: Forall P (h2 :: t1)
Hl2: Forall P (h2 :: t2)
Heq: list_annotate Hl1 = list_annotate Hl2
H1: list_annotate (Forall_inv_tail Hl1) =
list_annotate (Forall_inv_tail Hl2)
h2 :: t1 = h2 :: t2
  by apply IHt1 in H1 as ->.
Qed.

Lemma list_annotate_app :
  forall (l1 l2 : list A) (Hs : Forall P (l1 ++ l2)),
    list_annotate Hs =
    list_annotate (proj1 (proj1 (@Forall_app _ P l1 l2) Hs)) ++
    list_annotate (proj2 (proj1 (@Forall_app _ P l1 l2) Hs)).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (l1 l2 : list A) (Hs : Forall P (l1 ++ l2)),
  list_annotate Hs =
  list_annotate
    (proj1 (proj1 (Forall_app P l1 l2) Hs)) ++
  list_annotate
    (proj2 (proj1 (Forall_app P l1 l2) Hs))
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (l1 l2 : list A) (Hs : Forall P (l1 ++ l2)),
  list_annotate Hs =
  list_annotate
    (proj1 (proj1 (Forall_app P l1 l2) Hs)) ++
  list_annotate
    (proj2 (proj1 (Forall_app P l1 l2) Hs))
  induction l1; cbn; intros; [by apply list_annotate_pi |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a: A
l1: list A
IHl1: ∀ (l2 : list A) (Hs : Forall P (l1 ++ l2)),
  list_annotate Hs =
  list_annotate
    (proj1 (proj1 (Forall_app P l1 l2) Hs)) ++
  list_annotate
    (proj2 (proj1 (Forall_app P l1 l2) Hs))
l2: list A
Hs: Forall P (a :: l1 ++ l2)
dexist a (Forall_inv Hs)
:: list_annotate (Forall_inv_tail Hs) =
dexist a
  (Forall_inv
     (proj1 (proj1 (Forall_app P (a :: l1) l2) Hs)))
:: list_annotate
     (Forall_inv_tail
        (proj1 (proj1 (Forall_app P (a :: l1) l2) Hs))) ++
   list_annotate
     (proj2 (proj1 (Forall_app P (a :: l1) l2) Hs))
  f_equal; [by apply dsig_eq |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a: A
l1: list A
IHl1: ∀ (l2 : list A) (Hs : Forall P (l1 ++ l2)),
  list_annotate Hs =
  list_annotate
    (proj1 (proj1 (Forall_app P l1 l2) Hs)) ++
  list_annotate
    (proj2 (proj1 (Forall_app P l1 l2) Hs))
l2: list A
Hs: Forall P (a :: l1 ++ l2)
list_annotate (Forall_inv_tail Hs) =
list_annotate
  (Forall_inv_tail
     (proj1 (proj1 (Forall_app P (a :: l1) l2) Hs))) ++
list_annotate
  (proj2 (proj1 (Forall_app P (a :: l1) l2) Hs))
  by rewrite IHl1; f_equal; apply list_annotate_pi.
Qed.

Lemma nth_error_list_annotate :
  forall (n : nat) (l : list A) (Hs : Forall P l),
    exists (oa : option (dsig P)),
      nth_error (list_annotate Hs) n = oa /\ option_map (@proj1_sig _ _) oa = nth_error l n.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (n : nat) (l : list A) (Hs : Forall P l),
  ∃ oa : option (dsig P),
    nth_error (list_annotate Hs) n = oa
    ∧ option_map proj1_sig oa = nth_error l n
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (n : nat) (l : list A) (Hs : Forall P l),
  ∃ oa : option (dsig P),
    nth_error (list_annotate Hs) n = oa
    ∧ option_map proj1_sig oa = nth_error l n
  induction n as [| n']; intros [| h t] Hs; cbn.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
Hs: Forall P []
∃ oa : option (dsig P),
  None = oa ∧ option_map proj1_sig oa = None
A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
t: list A
Hs: Forall P (h :: t)
∃ oa : option (dsig P),
  Some (dexist h (Forall_inv Hs)) = oa
  ∧ option_map proj1_sig oa = Some h
A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
n': nat
IHn': ∀ (l : list A) (Hs : Forall P l),
  ∃ oa : option (dsig P),
    nth_error (list_annotate Hs) n' = oa
    ∧ option_map proj1_sig oa = nth_error l n'
Hs: Forall P []
∃ oa : option (dsig P),
  None = oa ∧ option_map proj1_sig oa = None
A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
n': nat
IHn': ∀ (l : list A) (Hs : Forall P l),
  ∃ oa : option (dsig P),
    nth_error (list_annotate Hs) n' = oa
    ∧ option_map proj1_sig oa = nth_error l n'
h: A
t: list A
Hs: Forall P (h :: t)
∃ oa : option (dsig P),
  nth_error (list_annotate (Forall_inv_tail Hs)) n' =
  oa ∧ option_map proj1_sig oa = nth_error t n'
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
Hs: Forall P []
∃ oa : option (dsig P),
  None = oa ∧ option_map proj1_sig oa = None by exists None.
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
t: list A
Hs: Forall P (h :: t)
∃ oa : option (dsig P),
  Some (dexist h (Forall_inv Hs)) = oa
  ∧ option_map proj1_sig oa = Some h inversion Hs; subst.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
t: list A
Hs: Forall P (h :: t)
H1: P h
H2: Forall P t
∃ oa : option (dsig P),
  Some (dexist h (Forall_inv Hs)) = oa
  ∧ option_map proj1_sig oa = Some h
    by exists (Some (dexist h (Forall_inv Hs))).
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
n': nat
IHn': ∀ (l : list A) (Hs : Forall P l),
  ∃ oa : option (dsig P),
    nth_error (list_annotate Hs) n' = oa
    ∧ option_map proj1_sig oa = nth_error l n'
Hs: Forall P []
∃ oa : option (dsig P),
  None = oa ∧ option_map proj1_sig oa = None by exists None.
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
n': nat
IHn': ∀ (l : list A) (Hs : Forall P l),
  ∃ oa : option (dsig P),
    nth_error (list_annotate Hs) n' = oa
    ∧ option_map proj1_sig oa = nth_error l n'
h: A
t: list A
Hs: Forall P (h :: t)
∃ oa : option (dsig P),
  nth_error (list_annotate (Forall_inv_tail Hs)) n' =
  oa ∧ option_map proj1_sig oa = nth_error t n' by eauto.
Qed.

Lemma elem_of_list_annotate :
  forall (l : list A) (Hs : Forall P l) (a : {x : A | bool_decide (P x)}),
    a ∈ list_annotate Hs <-> `a ∈ l.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (l : list A) (Hs : Forall P l) (a : {x : A
                                      | bool_decide
                                          (P x)}),
  a ∈ list_annotate Hs ↔ `a ∈ l
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (l : list A) (Hs : Forall P l) (a : {x : A
                                      | bool_decide
                                          (P x)}),
  a ∈ list_annotate Hs ↔ `a ∈ l
  induction l; cbn; intros.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
Hs: Forall P []
a: {x : A | bool_decide (P x)}
a ∈ [] ↔ `a ∈ []
A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a: A
l: list A
IHl: ∀ (Hs : Forall P l) (a : 
                     {x : A | 
                     bool_decide (P x)}),
  a ∈ list_annotate Hs ↔ `a ∈ l
Hs: Forall P (a :: l)
a0: {x : A | bool_decide (P x)}
a0
∈ dexist a (Forall_inv Hs)
  :: list_annotate (Forall_inv_tail Hs) ↔ 
`a0 ∈ a :: l
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
Hs: Forall P []
a: {x : A | bool_decide (P x)}
a ∈ [] ↔ `a ∈ [] by rewrite !elem_of_nil.
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a: A
l: list A
IHl: ∀ (Hs : Forall P l) (a : 
                     {x : A | 
                     bool_decide (P x)}),
  a ∈ list_annotate Hs ↔ `a ∈ l
Hs: Forall P (a :: l)
a0: {x : A | bool_decide (P x)}
a0
∈ dexist a (Forall_inv Hs)
  :: list_annotate (Forall_inv_tail Hs) ↔ `a0 ∈ a :: l by rewrite !elem_of_cons, IHl, (dsig_eq P a0); cbn.
Qed.

Lemma list_annotate_NoDup :
  forall (l : list A) (Hs : Forall P l),
    NoDup l -> NoDup (list_annotate Hs).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (l : list A) (Hs : Forall P l),
  NoDup l → NoDup (list_annotate Hs)
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (l : list A) (Hs : Forall P l),
  NoDup l → NoDup (list_annotate Hs)
  induction 1; cbn; constructor; [| by apply IHNoDup].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
x: A
l: list A
Hs: Forall P (x :: l)
H: x ∉ l
H0: NoDup l
IHNoDup: ∀ Hs : Forall P l, NoDup (list_annotate Hs)
dexist x (Forall_inv Hs)
∉ list_annotate (Forall_inv_tail Hs)
  by rewrite elem_of_list_annotate.
Qed.

Lemma list_annotate_forget :
  forall (l : list A) (Hs : Forall P l),
    map proj1_sig (list_annotate Hs) = l.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (l : list A) (Hs : Forall P l),
  map proj1_sig (list_annotate Hs) = l
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (l : list A) (Hs : Forall P l),
  map proj1_sig (list_annotate Hs) = l
  by induction l; cbn; intros; [| rewrite IHl].
Qed.

End sec_list_annotate_props.

Compute the index of the n-th element of the list that satisfies the predicate P.

Fixpoint nth_error_filter_index
  {A : Type} (P : A -> Prop) `{forall (x : A), Decision (P x)}
  (l : list A) (n : nat) : option nat :=
  match l with
  | [] => None
  | h :: t =>
    if decide (P h) then
      match n with
      | 0 => Some 0
      | S n' => option_map S (nth_error_filter_index P t n')
      end
    else
      option_map S (nth_error_filter_index P t n)
  end.

Lemma nth_error_filter_index_le `{forall (x : A), Decision (P x)} :
  forall (l : list A) (n1 n2 in1 in2 : nat),
    n1 <= n2 ->
    nth_error_filter_index P l n1 = Some in1 ->
    nth_error_filter_index P l n2 = Some in2 ->
      in1 <= in2.A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
∀ (l : list A) (n1 n2 in1 in2 : nat),
  n1 ≤ n2
  → nth_error_filter_index P l n1 = Some in1
    → nth_error_filter_index P l n2 = Some in2
      → in1 ≤ in2
Proof.A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
∀ (l : list A) (n1 n2 in1 in2 : nat),
  n1 ≤ n2
  → nth_error_filter_index P l n1 = Some in1
    → nth_error_filter_index P l n2 = Some in2
      → in1 ≤ in2
  induction l; cbn; intros * Hle Hin1 Hin2; [by inversion Hin1 |].A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
n1 ≤ n2
→ nth_error_filter_index P l n1 = Some in1
→ nth_error_filter_index P l n2 = Some in2 → in1 ≤ in2
n1, n2, in1, in2: nat
Hle: n1 ≤ n2
Hin1: (if decide (P a)
 then
  match n1 with
  | 0 => Some 0
  | S n' =>
      option_map S
        (nth_error_filter_index P l n')
  end
 else
  option_map S (nth_error_filter_index P l n1)) =
Some in1
Hin2: (if decide (P a)
 then
  match n2 with
  | 0 => Some 0
  | S n' =>
      option_map S
        (nth_error_filter_index P l n')
  end
 else
  option_map S (nth_error_filter_index P l n2)) =
Some in2
in1 ≤ in2
  destruct (decide (P a)).A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
n1 ≤ n2
→ nth_error_filter_index P l n1 = Some in1
→ nth_error_filter_index P l n2 = Some in2 → in1 ≤ in2
n1, n2, in1, in2: nat
Hle: n1 ≤ n2
p: P a
Hin1: match n1 with
| 0 => Some 0
| S n' =>
    option_map S
      (nth_error_filter_index P l n')
end = Some in1
Hin2: match n2 with
| 0 => Some 0
| S n' =>
    option_map S
      (nth_error_filter_index P l n')
end = Some in2
in1 ≤ in2
A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
  n1 ≤ n2
  → nth_error_filter_index P l n1 = Some in1
    → nth_error_filter_index P l n2 = Some in2
      → in1 ≤ in2
n1, n2, in1, in2: nat
Hle: n1 ≤ n2
n: ¬ P a
Hin1: option_map S (nth_error_filter_index P l n1) =
Some in1
Hin2: option_map S (nth_error_filter_index P l n2) =
Some in2
in1 ≤ in2
  -A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
n1 ≤ n2
→ nth_error_filter_index P l n1 = Some in1
→ nth_error_filter_index P l n2 = Some in2 → in1 ≤ in2
n1, n2, in1, in2: nat
Hle: n1 ≤ n2
p: P a
Hin1: match n1 with
| 0 => Some 0
| S n' =>
    option_map S
      (nth_error_filter_index P l n')
end = Some in1
Hin2: match n2 with
| 0 => Some 0
| S n' =>
    option_map S
      (nth_error_filter_index P l n')
end = Some in2
in1 ≤ in2 destruct n1, n2.A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
n1 ≤ n2
→ nth_error_filter_index P l n1 = Some in1
→ nth_error_filter_index P l n2 = Some in2 → in1 ≤ in2
in1, in2: nat
Hle: 0 ≤ 0
p: P a
Hin1: Some 0 = Some in1
Hin2: Some 0 = Some in2
in1 ≤ in2
A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
  n1 ≤ n2
  → nth_error_filter_index P l n1 = Some in1
    → nth_error_filter_index P l n2 = Some in2
      → in1 ≤ in2
n2, in1, in2: nat
Hle: 0 ≤ S n2
p: P a
Hin1: Some 0 = Some in1
Hin2: option_map S (nth_error_filter_index P l n2) =
Some in2
in1 ≤ in2
A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
  n1 ≤ n2
  → nth_error_filter_index P l n1 = Some in1
    → nth_error_filter_index P l n2 = Some in2
      → in1 ≤ in2
n1, in1, in2: nat
Hle: S n1 ≤ 0
p: P a
Hin1: option_map S (nth_error_filter_index P l n1) =
Some in1
Hin2: Some 0 = Some in2
in1 ≤ in2
A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
  n1 ≤ n2
  → nth_error_filter_index P l n1 = Some in1
    → nth_error_filter_index P l n2 = Some in2
      → in1 ≤ in2
n1, n2, in1, in2: nat
Hle: S n1 ≤ S n2
p: P a
Hin1: option_map S (nth_error_filter_index P l n1) =
Some in1
Hin2: option_map S (nth_error_filter_index P l n2) =
Some in2
in1 ≤ in2
    +A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
n1 ≤ n2
→ nth_error_filter_index P l n1 = Some in1
→ nth_error_filter_index P l n2 = Some in2 → in1 ≤ in2
in1, in2: nat
Hle: 0 ≤ 0
p: P a
Hin1: Some 0 = Some in1
Hin2: Some 0 = Some in2
in1 ≤ in2 by congruence.
    +A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
n1 ≤ n2
→ nth_error_filter_index P l n1 = Some in1
→ nth_error_filter_index P l n2 = Some in2 → in1 ≤ in2
n2, in1, in2: nat
Hle: 0 ≤ S n2
p: P a
Hin1: Some 0 = Some in1
Hin2: option_map S (nth_error_filter_index P l n2) =
Some in2
in1 ≤ in2 by inversion Hin1; lia.
    +A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
n1 ≤ n2
→ nth_error_filter_index P l n1 = Some in1
→ nth_error_filter_index P l n2 = Some in2 → in1 ≤ in2
n1, in1, in2: nat
Hle: S n1 ≤ 0
p: P a
Hin1: option_map S (nth_error_filter_index P l n1) =
Some in1
Hin2: Some 0 = Some in2
in1 ≤ in2 by lia.
    +A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
n1 ≤ n2
→ nth_error_filter_index P l n1 = Some in1
→ nth_error_filter_index P l n2 = Some in2 → in1 ≤ in2
n1, n2, in1, in2: nat
Hle: S n1 ≤ S n2
p: P a
Hin1: option_map S (nth_error_filter_index P l n1) =
Some in1
Hin2: option_map S (nth_error_filter_index P l n2) =
Some in2
in1 ≤ in2 unfold option_map in Hin1, Hin2.A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
n1 ≤ n2
→ nth_error_filter_index P l n1 = Some in1
→ nth_error_filter_index P l n2 = Some in2 → in1 ≤ in2
n1, n2, in1, in2: nat
Hle: S n1 ≤ S n2
p: P a
Hin1: match nth_error_filter_index P l n1 with
| Some a => Some (S a)
| None => None
end = Some in1
Hin2: match nth_error_filter_index P l n2 with
| Some a => Some (S a)
| None => None
end = Some in2
in1 ≤ in2
      destruct (nth_error_filter_index P l n1) eqn: Hin1'; inversion Hin1;
        subst; clear Hin1.A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
n1 ≤ n2
→ nth_error_filter_index P l n1 = Some in1
→ nth_error_filter_index P l n2 = Some in2 → in1 ≤ in2
n1, n2, in2: nat
Hle: S n1 ≤ S n2
p: P a
n: nat
Hin1': nth_error_filter_index P l n1 = Some n
Hin2: match nth_error_filter_index P l n2 with
| Some a => Some (S a)
| None => None
end = Some in2
S n ≤ in2
      destruct (nth_error_filter_index P l n2) eqn: Hin2'; inversion Hin2;
        subst; clear Hin2.A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
n1 ≤ n2
→ nth_error_filter_index P l n1 = Some in1
→ nth_error_filter_index P l n2 = Some in2 → in1 ≤ in2
n1, n2: nat
Hle: S n1 ≤ S n2
p: P a
n: nat
Hin1': nth_error_filter_index P l n1 = Some n
n0: nat
Hin2': nth_error_filter_index P l n2 = Some n0
S n ≤ S n0
      by eapply le_n_S, IHl; cycle 1; [done.. | lia].
  -A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
n1 ≤ n2
→ nth_error_filter_index P l n1 = Some in1
→ nth_error_filter_index P l n2 = Some in2 → in1 ≤ in2
n1, n2, in1, in2: nat
Hle: n1 ≤ n2
n: ¬ P a
Hin1: option_map S (nth_error_filter_index P l n1) =
Some in1
Hin2: option_map S (nth_error_filter_index P l n2) =
Some in2
in1 ≤ in2 destruct (nth_error_filter_index P l n1) eqn: Hin1'; inversion Hin1;
      subst; clear Hin1.A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
n1 ≤ n2
→ nth_error_filter_index P l n1 = Some in1
→ nth_error_filter_index P l n2 = Some in2 → in1 ≤ in2
n1, n2, in2: nat
Hle: n1 ≤ n2
n: ¬ P a
n0: nat
Hin1': nth_error_filter_index P l n1 = Some n0
Hin2: option_map S (nth_error_filter_index P l n2) =
Some in2
S n0 ≤ in2
    destruct (nth_error_filter_index P l n2) eqn: Hin2'; inversion Hin2;
      subst; clear Hin2.A: Type
P: A → Prop
H: ∀ x : A, Decision (P x)
a: A
l: list A
IHl: ∀ n1 n2 in1 in2 : nat,
n1 ≤ n2
→ nth_error_filter_index P l n1 = Some in1
→ nth_error_filter_index P l n2 = Some in2 → in1 ≤ in2
n1, n2: nat
Hle: n1 ≤ n2
n: ¬ P a
n0: nat
Hin1': nth_error_filter_index P l n1 = Some n0
n3: nat
Hin2': nth_error_filter_index P l n2 = Some n3
S n0 ≤ S n3
    by eapply le_n_S, IHl.
Qed.

Lemma Forall_filter :
  forall {A : Type} (P : A -> Prop) {Pdec : forall a : A, Decision (P a)} (l : list A),
    Forall P (filter P l).∀ (A : Type) (P : A → Prop) (Pdec : ∀ a : A,
                                      Decision (P a)) 
  (l : list A), Forall P (filter P l)
Proof.∀ (A : Type) (P : A → Prop) (Pdec : ∀ a : A,
                                      Decision (P a)) 
  (l : list A), Forall P (filter P l)
  induction l as [| h t]; cbn; [by constructor |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
t: list A
IHt: Forall P (filter P t)
Forall P
  (if decide (P h)
   then h :: filter P t
   else filter P t)
  by case_decide; [constructor |].
Qed.

Compute the sublist of a list that contains only elements that satisfy the given decidable predicate. Each element of the resulting list is paired with the proof that it satisfies the predicate.

Fixpoint filter_annotate
  {A : Type} (P : A -> Prop) {Pdec : forall a : A, Decision (P a)}
  (l : list A) : list (dsig P) :=
  match l with
  | [] => []
  | h :: t =>
    match decide (P h) with
    | left p => dexist h p :: filter_annotate P t
    | right _ => filter_annotate P t
    end
  end.

Lemma filter_annotate_length :
  forall {A : Type} (P : A -> Prop) {Pdec : forall a : A, Decision (P a)} (l : list A),
    length (filter_annotate P l) = length (filter P l).∀ (A : Type) (P : A → Prop) (Pdec : ∀ a : A,
                                      Decision (P a)) 
  (l : list A),
  length (filter_annotate P l) = length (filter P l)
Proof.∀ (A : Type) (P : A → Prop) (Pdec : ∀ a : A,
                                      Decision (P a)) 
  (l : list A),
  length (filter_annotate P l) = length (filter P l)
  induction l as [| h t]; cbn; [done |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
t: list A
IHt: length (filter_annotate P t) =
length (filter P t)
length
  match decide (P h) with
  | left p => dexist h p :: filter_annotate P t
  | right _ => filter_annotate P t
  end =
length
  (if decide (P h)
   then h :: filter P t
   else filter P t)
  case_decide; cbn; [| done].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
h: A
t: list A
IHt: length (filter_annotate P t) =
length (filter P t)
H: P h
S (length (filter_annotate P t)) =
S (length (filter P t))
  by rewrite IHt.
Qed.

Lemma filter_annotate_unroll :
  forall {A : Type} (P : A -> Prop) {Pdec : forall a : A, Decision (P a)} (a : A) (l : list A),
    filter_annotate P (a :: l) =
    let fa := filter_annotate P l in
    match decide (P a) with
    | left pa => dexist _ pa :: fa
    | _ => fa
    end.∀ (A : Type) (P : A → Prop) (Pdec : ∀ a : A,
                                      Decision (P a)) 
  (a : A) (l : list A),
  filter_annotate P (a :: l) =
  (let fa := filter_annotate P l in
   match decide (P a) with
   | left pa => dexist a pa :: fa
   | right _ => fa
   end)
Proof.∀ (A : Type) (P : A → Prop) (Pdec : ∀ a : A,
                                      Decision (P a)) 
  (a : A) (l : list A),
  filter_annotate P (a :: l) =
  (let fa := filter_annotate P l in
   match decide (P a) with
   | left pa => dexist a pa :: fa
   | right _ => fa
   end) done. Qed.

Lemma filter_annotate_app :
  forall {A : Type} (P : A -> Prop) {Pdec : forall a : A, Decision (P a)} (l1 l2 : list A),
    filter_annotate P (l1 ++ l2) = filter_annotate P l1 ++ filter_annotate P l2.∀ (A : Type) (P : A → Prop) (Pdec : ∀ a : A,
                                      Decision (P a)) 
  (l1 l2 : list A),
  filter_annotate P (l1 ++ l2) =
  filter_annotate P l1 ++ filter_annotate P l2
Proof.∀ (A : Type) (P : A → Prop) (Pdec : ∀ a : A,
                                      Decision (P a)) 
  (l1 l2 : list A),
  filter_annotate P (l1 ++ l2) =
  filter_annotate P l1 ++ filter_annotate P l2
  induction l1; cbn; intros; [done |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a: A
l1: list A
IHl1: ∀ l2 : list A,
  filter_annotate P (l1 ++ l2) =
  filter_annotate P l1 ++ filter_annotate P l2
l2: list A
match decide (P a) with
| left p => dexist a p :: filter_annotate P (l1 ++ l2)
| right _ => filter_annotate P (l1 ++ l2)
end =
match decide (P a) with
| left p => dexist a p :: filter_annotate P l1
| right _ => filter_annotate P l1
end ++ filter_annotate P l2
  case_decide; cbn; [| done].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a: A
l1: list A
IHl1: ∀ l2 : list A,
  filter_annotate P (l1 ++ l2) =
  filter_annotate P l1 ++ filter_annotate P l2
l2: list A
H: P a
dexist a H :: filter_annotate P (l1 ++ l2) =
dexist a H
:: filter_annotate P l1 ++ filter_annotate P l2
  by rewrite IHl1.
Qed.

Filters a list through a predicate, then transforms each element using a function which depends on the fact that the predicate holds.

Definition list_filter_map
  {A B : Type} (P : A -> Prop) {Pdec : forall a, Decision (P a)}
  (f : dsig P -> B) (l : list A) : list B :=
    map f (filter_annotate P l).

Lemma list_filter_map_app :
  forall {A B : Type} (P : A -> Prop) {Pdec : forall a, Decision (P a)}
    (f : dsig P -> B) (l1 l2 : list A),
      list_filter_map P f (l1 ++ l2) = list_filter_map P f l1 ++ list_filter_map P f l2.∀ (A B : Type) (P : A → Prop) (Pdec : ∀ a : A,
                                        Decision (P a)) 
  (f : dsig P → B) (l1 l2 : list A),
  list_filter_map P f (l1 ++ l2) =
  list_filter_map P f l1 ++ list_filter_map P f l2
Proof.∀ (A B : Type) (P : A → Prop) (Pdec : ∀ a : A,
                                        Decision (P a)) 
  (f : dsig P → B) (l1 l2 : list A),
  list_filter_map P f (l1 ++ l2) =
  list_filter_map P f l1 ++ list_filter_map P f l2
  by intros; unfold list_filter_map; rewrite filter_annotate_app, map_app.
Qed.

Lemma take_nth :
  forall {A : Type} (i n : nat) (s : list A),
    i < n -> nth_error (take n s) i = nth_error s i.∀ (A : Type) (i n : nat) (s : list A),
  i < n → nth_error (take n s) i = nth_error s i
Proof.∀ (A : Type) (i n : nat) (s : list A),
  i < n → nth_error (take n s) i = nth_error s i
  induction i; intros n [| h t] []; cbn; [done.. | |].A: Type
i: nat
IHi: ∀ (n : nat) (s : list A), i < n → nth_error (take n s) i = nth_error s i
n: nat
h: A
t: list A
nth_error (take (S i) t) i = nth_error t i
A: Type
i: nat
IHi: ∀ (n : nat) (s : list A), i < n → nth_error (take n s) i = nth_error s i
n: nat
h: A
t: list A
m: nat
H: S (S i) ≤ m
nth_error (take m t) i = nth_error t i
  -A: Type
i: nat
IHi: ∀ (n : nat) (s : list A), i < n → nth_error (take n s) i = nth_error s i
n: nat
h: A
t: list A
nth_error (take (S i) t) i = nth_error t i by apply IHi; lia.
  -A: Type
i: nat
IHi: ∀ (n : nat) (s : list A), i < n → nth_error (take n s) i = nth_error s i
n: nat
h: A
t: list A
m: nat
H: S (S i) ≤ m
nth_error (take m t) i = nth_error t i by apply IHi; lia.
Qed.

Lemma nth_error_length :
  forall {A : Type} (n : nat) (l : list A) (a : A),
    nth_error l n = Some a -> S n <= length l.∀ (A : Type) (n : nat) (l : list A) (a : A),
  nth_error l n = Some a → S n ≤ length l
Proof.∀ (A : Type) (n : nat) (l : list A) (a : A),
  nth_error l n = Some a → S n ≤ length l
  induction n as [| n']; intros [| h t] a; inversion 1; cbn; [by lia |].A: Type
n': nat
IHn': ∀ (l : list A) (a : A),
  nth_error l n' = Some a → S n' ≤ length l
h: A
t: list A
a: A
H: nth_error (h :: t) (S n') = Some a
H1: nth_error t n' = Some a
S (S n') ≤ S (length t)
  by eapply le_n_S, IHn'.
Qed.

Lemma take_nth_last :
  forall {A : Type} (l : list A) (n : nat) (nth : A) (Hnth : nth_error l n = Some nth) (_last : A),
    nth = List.last (take (S n) l) _last.∀ (A : Type) (l : list A) (n : nat) (nth : A),
  nth_error l n = Some nth
  → ∀ _last : A, nth = List.last (take (S n) l) _last
Proof.∀ (A : Type) (l : list A) (n : nat) (nth : A),
  nth_error l n = Some nth
  → ∀ _last : A, nth = List.last (take (S n) l) _last
  intros.A: Type
l: list A
n: nat
nth: A
Hnth: nth_error l n = Some nth
_last: A
nth = List.last (take (S n) l) _last
  apply Some_inj.A: Type
l: list A
n: nat
nth: A
Hnth: nth_error l n = Some nth
_last: A
Some nth = Some (List.last (take (S n) l) _last)
  erewrite <- Hnth, <- nth_error_last.A: Type
l: list A
n: nat
nth: A
Hnth: nth_error l n = Some nth
_last: A
nth_error l n = nth_error (take (S n) l) ?n
A: Type
l: list A
n: nat
nth: A
Hnth: nth_error l n = Some nth
_last: A
S ?n = length (take (S n) l)
  -A: Type
l: list A
n: nat
nth: A
Hnth: nth_error l n = Some nth
_last: A
nth_error l n = nth_error (take (S n) l) ?n by rewrite take_nth; [done | lia].
  -A: Type
l: list A
n: nat
nth: A
Hnth: nth_error l n = Some nth
_last: A
S n = length (take (S n) l) rewrite take_length.A: Type
l: list A
n: nat
nth: A
Hnth: nth_error l n = Some nth
_last: A
S n = S n `min` length l
    by apply nth_error_length in Hnth; lia.
Qed.

Lemma drop_S_tail :
  forall {A : Type} (l : list A) (n : nat),
    drop (S n) l = drop n (tail l).∀ (A : Type) (l : list A) (n : nat),
  drop (S n) l = drop n (tail l)
Proof.∀ (A : Type) (l : list A) (n : nat),
  drop (S n) l = drop n (tail l)
  by intros A [] n; cbn; [rewrite drop_nil |].
Qed.

Lemma drop_tail_comm :
  forall {A : Type} (l : list A) (n : nat),
    drop n (tail l) = tail (drop n l).∀ (A : Type) (l : list A) (n : nat),
  drop n (tail l) = tail (drop n l)
Proof.∀ (A : Type) (l : list A) (n : nat),
  drop n (tail l) = tail (drop n l)
  intros A l n; revert l; induction n; intros l.A: Type
l: list A
drop 0 (tail l) = tail (drop 0 l)
A: Type
n: nat
IHn: ∀ l : list A, drop n (tail l) = tail (drop n l)
l: list A
drop (S n) (tail l) = tail (drop (S n) l)
  -A: Type
l: list A
drop 0 (tail l) = tail (drop 0 l) by rewrite !drop_0.
  -A: Type
n: nat
IHn: ∀ l : list A, drop n (tail l) = tail (drop n l)
l: list A
drop (S n) (tail l) = tail (drop (S n) l) by rewrite !drop_S_tail, IHn.
Qed.

Lemma drop_lookup :
  forall {A : Type} (s : list A) (n i : nat),
    n <= i -> drop n s !! (i - n) = s !! i.∀ (A : Type) (s : list A) (n i : nat),
  n ≤ i → drop n s !! (i - n) = s !! i
Proof.∀ (A : Type) (s : list A) (n i : nat),
  n ≤ i → drop n s !! (i - n) = s !! i
  intros.A: Type
s: list A
n, i: nat
H: n ≤ i
drop n s !! (i - n) = s !! i
  rewrite lookup_drop.A: Type
s: list A
n, i: nat
H: n ≤ i
s !! (n + (i - n)) = s !! i
  by replace (n + (i - n)) with i by lia.
Qed.

Lemma drop_nth :
  forall {A : Type} (i n : nat) (l : list A),
    n <= i -> nth_error (drop n l) (i - n) = nth_error l i.∀ (A : Type) (i n : nat) (l : list A),
  n ≤ i → nth_error (drop n l) (i - n) = nth_error l i
Proof.∀ (A : Type) (i n : nat) (l : list A),
  n ≤ i → nth_error (drop n l) (i - n) = nth_error l i
  induction i; intros [| n'] [| h t] Hi; cbn; try done.A: Type
n': nat
h: A
t: list A
Hi: S n' ≤ 0
match drop n' t with
| [] => None
| x :: _ => Some x
end = Some h
A: Type
i: nat
IHi: ∀ (n : nat) (l : list A),
n ≤ i → nth_error (drop n l) (i - n) = nth_error l i
n': nat
Hi: S n' ≤ S i
nth_error [] (i - n') = None
A: Type
i: nat
IHi: ∀ (n : nat) (l : list A),
n ≤ i → nth_error (drop n l) (i - n) = nth_error l i
n': nat
h: A
t: list A
Hi: S n' ≤ S i
nth_error (drop n' t) (i - n') = nth_error t i
  -A: Type
n': nat
h: A
t: list A
Hi: S n' ≤ 0
match drop n' t with
| [] => None
| x :: _ => Some x
end = Some h by inversion Hi.
  -A: Type
i: nat
IHi: ∀ (n : nat) (l : list A),
n ≤ i → nth_error (drop n l) (i - n) = nth_error l i
n': nat
Hi: S n' ≤ S i
nth_error [] (i - n') = None by apply nth_error_None; cbn; lia.
  -A: Type
i: nat
IHi: ∀ (n : nat) (l : list A),
n ≤ i → nth_error (drop n l) (i - n) = nth_error l i
n': nat
h: A
t: list A
Hi: S n' ≤ S i
nth_error (drop n' t) (i - n') = nth_error t i by apply IHi; lia.
Qed.

Lemma drop_last :
  forall {A : Type} (i : nat) (l : list A) (_default : A),
    i < length l -> List.last (drop i l) _default  = List.last l _default.∀ (A : Type) (i : nat) (l : list A) (_default : A),
  i < length l
  → List.last (drop i l) _default =
    List.last l _default
Proof.∀ (A : Type) (i : nat) (l : list A) (_default : A),
  i < length l
  → List.last (drop i l) _default =
    List.last l _default
  induction i; intros [| h t] * Hlt; cbn in *; [done.. |].A: Type
i: nat
IHi: ∀ (l : list A) (_default : A),
i < length l → List.last (drop i l) _default = List.last l _default
h: A
t: list A
_default: A
Hlt: S i < S (length t)
List.last (drop i t) _default =
match t with
| [] => h
| _ :: _ => List.last t _default
end
  rewrite IHi by lia.A: Type
i: nat
IHi: ∀ (l : list A) (_default : A),
i < length l → List.last (drop i l) _default = List.last l _default
h: A
t: list A
_default: A
Hlt: S i < S (length t)
List.last t _default =
match t with
| [] => h
| _ :: _ => List.last t _default
end
  destruct t; [| done].A: Type
i: nat
IHi: ∀ (l : list A) (_default : A),
i < length l → List.last (drop i l) _default = List.last l _default
h, _default: A
Hlt: S i < S (length [])
List.last [] _default = h
  by inversion Hlt; lia.
Qed.

Lemma list_segment_nth :
  forall {A : Type} (l : list A) (n1 n2 : nat) (i : nat),
    n1 <= n2 -> n1 <= i -> i < n2 ->
      nth_error (list_segment l n1 n2) (i - n1) = nth_error l i.∀ (A : Type) (l : list A) (n1 n2 i : nat),
  n1 ≤ n2
  → n1 ≤ i
    → i < n2
      → nth_error (list_segment l n1 n2) (i - n1) =
        nth_error l i
Proof.∀ (A : Type) (l : list A) (n1 n2 i : nat),
  n1 ≤ n2
  → n1 ≤ i
    → i < n2
      → nth_error (list_segment l n1 n2) (i - n1) =
        nth_error l i
  intros.A: Type
l: list A
n1, n2, i: nat
H: n1 ≤ n2
H0: n1 ≤ i
H1: i < n2
nth_error (list_segment l n1 n2) (i - n1) =
nth_error l i
  unfold list_segment.A: Type
l: list A
n1, n2, i: nat
H: n1 ≤ n2
H0: n1 ≤ i
H1: i < n2
nth_error (drop n1 (take n2 l)) (i - n1) =
nth_error l i
  rewrite drop_nth; [| done].A: Type
l: list A
n1, n2, i: nat
H: n1 ≤ n2
H0: n1 ≤ i
H1: i < n2
nth_error (take n2 l) i = nth_error l i
  by apply take_nth.
Qed.

Lemma list_segment_app :
  forall {A : Type} (l : list A) (n1 n2 n3 : nat),
    n1 <= n2 -> n2 <= n3 ->
      list_segment l n1 n2 ++ list_segment l n2 n3 = list_segment l n1 n3.∀ (A : Type) (l : list A) (n1 n2 n3 : nat),
  n1 ≤ n2
  → n2 ≤ n3
    → list_segment l n1 n2 ++ list_segment l n2 n3 =
      list_segment l n1 n3
Proof.∀ (A : Type) (l : list A) (n1 n2 n3 : nat),
  n1 ≤ n2
  → n2 ≤ n3
    → list_segment l n1 n2 ++ list_segment l n2 n3 =
      list_segment l n1 n3
  intros.A: Type
l: list A
n1, n2, n3: nat
H: n1 ≤ n2
H0: n2 ≤ n3
list_segment l n1 n2 ++ list_segment l n2 n3 =
list_segment l n1 n3
  unfold list_segment.A: Type
l: list A
n1, n2, n3: nat
H: n1 ≤ n2
H0: n2 ≤ n3
drop n1 (take n2 l) ++ drop n2 (take n3 l) =
drop n1 (take n3 l)
  assert (Hle : n1 <= n3) by lia.A: Type
l: list A
n1, n2, n3: nat
H: n1 ≤ n2
H0: n2 ≤ n3
Hle: n1 ≤ n3
drop n1 (take n2 l) ++ drop n2 (take n3 l) =
drop n1 (take n3 l)
  pose proof (Hl1 := take_segment_suffix l n1 n3 Hle).A: Type
l: list A
n1, n2, n3: nat
H: n1 ≤ n2
H0: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: take n1 l ++ list_segment l n1 n3 ++ drop n3 l = l
drop n1 (take n2 l) ++ drop n2 (take n3 l) =
drop n1 (take n3 l)
  rewrite <- (take_segment_suffix l n2 n3) in Hl1 at 4 by done.A: Type
l: list A
n1, n2, n3: nat
H: n1 ≤ n2
H0: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: take n1 l ++ list_segment l n1 n3 ++ drop n3 l =
take n2 l ++ list_segment l n2 n3 ++ drop n3 l
drop n1 (take n2 l) ++ drop n2 (take n3 l) =
drop n1 (take n3 l)
  rewrite !app_assoc in Hl1.A: Type
l: list A
n1, n2, n3: nat
H: n1 ≤ n2
H0: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: (take n1 l ++ list_segment l n1 n3) ++ drop n3 l =
(take n2 l ++ list_segment l n2 n3) ++ drop n3 l
drop n1 (take n2 l) ++ drop n2 (take n3 l) =
drop n1 (take n3 l)
  apply app_inv_tail in Hl1.A: Type
l: list A
n1, n2, n3: nat
H: n1 ≤ n2
H0: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: take n1 l ++ list_segment l n1 n3 = take n2 l ++ list_segment l n2 n3
drop n1 (take n2 l) ++ drop n2 (take n3 l) =
drop n1 (take n3 l)
  rewrite <- (take_drop n1 (take n2 l)), <- app_assoc, (take_prefix l n1 n2) in Hl1 by done.A: Type
l: list A
n1, n2, n3: nat
H: n1 ≤ n2
H0: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: take n1 l ++ list_segment l n1 n3 =
take n1 l ++ drop n1 (take n2 l) ++ list_segment l n2 n3
drop n1 (take n2 l) ++ drop n2 (take n3 l) =
drop n1 (take n3 l)
  by apply app_inv_head in Hl1.
Qed.

Lemma list_segment_singleton :
  forall {A : Type} (l : list A) (n : nat) (a : A),
    nth_error l n = Some a -> list_segment l n (S n) = [a].∀ (A : Type) (l : list A) (n : nat) (a : A),
  nth_error l n = Some a
  → list_segment l n (S n) = [a]
Proof.∀ (A : Type) (l : list A) (n : nat) (a : A),
  nth_error l n = Some a
  → list_segment l n (S n) = [a]
  intros * Hnth.A: Type
l: list A
n: nat
a: A
Hnth: nth_error l n = Some a
list_segment l n (S n) = [a]
  apply nth_error_split in Hnth as (l1 & l2 & -> & <-).A: Type
a: A
l1, l2: list A
list_segment (l1 ++ a :: l2) (length l1)
  (S (length l1)) = [a]
  unfold list_segment.A: Type
a: A
l1, l2: list A
drop (length l1)
  (take (S (length l1)) (l1 ++ a :: l2)) = [a]
  rewrite <- app_cons, app_assoc, take_app_length', drop_app_length; [done |].A: Type
a: A
l1, l2: list A
S (length l1) = length (l1 ++ [a])
  by rewrite app_length; cbn; lia.
Qed.

Lemma nth_error_map :
  forall {A B : Type} (f : A -> B) (l : list A) (n : nat),
    nth_error (List.map f l) n = option_map f (nth_error l n).∀ (A B : Type) (f : A → B) (l : list A) (n : nat),
  nth_error (map f l) n = option_map f (nth_error l n)
Proof.∀ (A B : Type) (f : A → B) (l : list A) (n : nat),
  nth_error (map f l) n = option_map f (nth_error l n)
  by induction l; intros [| n]; cbn; [.. | apply IHl].
Qed.

Lemma omap_app_rev :
  forall {A B : Type} (f : A -> option B) (l : list A) (l1' l2' : list B),
    omap f l = l1' ++ l2' ->
      exists l1 l2 : list A, l = l1 ++ l2 /\ omap f l1 = l1' /\ omap f l2 = l2'.∀ (A B : Type) (f : A → option B) (l : list A) (l1'
                                                l2' : 
                                                list B),
  omap f l = l1' ++ l2'
  → ∃ l1 l2 : list A,
      l = l1 ++ l2 ∧ omap f l1 = l1' ∧ omap f l2 = l2'
Proof.∀ (A B : Type) (f : A → option B) (l : list A) (l1'
                                                l2' : 
                                                list B),
  omap f l = l1' ++ l2'
  → ∃ l1 l2 : list A,
      l = l1 ++ l2 ∧ omap f l1 = l1' ∧ omap f l2 = l2'
  induction l; intros * Happ_rev.A, B: Type
f: A → option B
l1', l2': list B
Happ_rev: omap f [] = l1' ++ l2'
∃ l1 l2 : list A,
  [] = l1 ++ l2 ∧ omap f l1 = l1' ∧ omap f l2 = l2'
A, B: Type
f: A → option B
a: A
l: list A
IHl: ∀ l1' l2' : list B,
  omap f l = l1' ++ l2'
  → ∃ l1 l2 : list A,
      l = l1 ++ l2
      ∧ omap f l1 = l1' ∧ omap f l2 = l2'
l1', l2': list B
Happ_rev: omap f (a :: l) = l1' ++ l2'
∃ l1 l2 : list A,
  a :: l = l1 ++ l2
  ∧ omap f l1 = l1' ∧ omap f l2 = l2'
  -A, B: Type
f: A → option B
l1', l2': list B
Happ_rev: omap f [] = l1' ++ l2'
∃ l1 l2 : list A,
  [] = l1 ++ l2 ∧ omap f l1 = l1' ∧ omap f l2 = l2' symmetry in Happ_rev.A, B: Type
f: A → option B
l1', l2': list B
Happ_rev: l1' ++ l2' = omap f []
∃ l1 l2 : list A,
  [] = l1 ++ l2 ∧ omap f l1 = l1' ∧ omap f l2 = l2'
    apply app_eq_nil in Happ_rev as [Hl1' Hl2']; subst.A, B: Type
f: A → option B
∃ l1 l2 : list A,
  [] = l1 ++ l2 ∧ omap f l1 = [] ∧ omap f l2 = []
    by exists [], [].
  -A, B: Type
f: A → option B
a: A
l: list A
IHl: ∀ l1' l2' : list B,
omap f l = l1' ++ l2'
→ ∃ l1 l2 : list A, l = l1 ++ l2 ∧ omap f l1 = l1' ∧ omap f l2 = l2'
l1', l2': list B
Happ_rev: omap f (a :: l) = l1' ++ l2'
∃ l1 l2 : list A,
  a :: l = l1 ++ l2
  ∧ omap f l1 = l1' ∧ omap f l2 = l2' cbn in Happ_rev.A, B: Type
f: A → option B
a: A
l: list A
IHl: ∀ l1' l2' : list B,
omap f l = l1' ++ l2'
→ ∃ l1 l2 : list A, l = l1 ++ l2 ∧ omap f l1 = l1' ∧ omap f l2 = l2'
l1', l2': list B
Happ_rev: match f a with
| Some y => y :: omap f l
| None => omap f l
end = l1' ++ l2'
∃ l1 l2 : list A,
  a :: l = l1 ++ l2
  ∧ omap f l1 = l1' ∧ omap f l2 = l2'
    destruct (f a) eqn: Hfa; cycle 1.A, B: Type
f: A → option B
a: A
l: list A
IHl: ∀ l1' l2' : list B,
omap f l = l1' ++ l2'
→ ∃ l1 l2 : list A, l = l1 ++ l2 ∧ omap f l1 = l1' ∧ omap f l2 = l2'
l1', l2': list B
Hfa: f a = None
Happ_rev: omap f l = l1' ++ l2'
∃ l1 l2 : list A,
  a :: l = l1 ++ l2
  ∧ omap f l1 = l1' ∧ omap f l2 = l2'
A, B: Type
f: A → option B
a: A
l: list A
IHl: ∀ l1' l2' : list B,
  omap f l = l1' ++ l2'
  → ∃ l1 l2 : list A,
      l = l1 ++ l2
      ∧ omap f l1 = l1' ∧ omap f l2 = l2'
l1', l2': list B
b: B
Hfa: f a = Some b
Happ_rev: b :: omap f l = l1' ++ l2'
∃ l1 l2 : list A,
  a :: l = l1 ++ l2
  ∧ omap f l1 = l1' ∧ omap f l2 = l2'
    +A, B: Type
f: A → option B
a: A
l: list A
IHl: ∀ l1' l2' : list B,
omap f l = l1' ++ l2'
→ ∃ l1 l2 : list A, l = l1 ++ l2 ∧ omap f l1 = l1' ∧ omap f l2 = l2'
l1', l2': list B
Hfa: f a = None
Happ_rev: omap f l = l1' ++ l2'
∃ l1 l2 : list A,
  a :: l = l1 ++ l2
  ∧ omap f l1 = l1' ∧ omap f l2 = l2' destruct (IHl _ _ Happ_rev) as (_l1 & l2 & -> & <- & <-).A, B: Type
f: A → option B
a: A
_l1, l2: list A
IHl: ∀ l1' l2' : list B,
omap f (_l1 ++ l2) = l1' ++ l2'
→ ∃ l1 l3 : list A,
_l1 ++ l2 = l1 ++ l3 ∧ omap f l1 = l1' ∧ omap f l3 = l2'
Hfa: f a = None
Happ_rev: omap f (_l1 ++ l2) =
omap f _l1 ++ omap f l2
∃ l1 l3 : list A,
  a :: _l1 ++ l2 = l1 ++ l3
  ∧ omap f l1 = omap f _l1 ∧ omap f l3 = omap f l2
      by exists (a :: _l1), l2; cbn; rewrite Hfa.
    +A, B: Type
f: A → option B
a: A
l: list A
IHl: ∀ l1' l2' : list B,
omap f l = l1' ++ l2'
→ ∃ l1 l2 : list A, l = l1 ++ l2 ∧ omap f l1 = l1' ∧ omap f l2 = l2'
l1', l2': list B
b: B
Hfa: f a = Some b
Happ_rev: b :: omap f l = l1' ++ l2'
∃ l1 l2 : list A,
  a :: l = l1 ++ l2
  ∧ omap f l1 = l1' ∧ omap f l2 = l2' destruct l1' as [| _b l1']; cbn in Happ_rev; inversion Happ_rev; subst.A, B: Type
f: A → option B
a: A
l: list A
IHl: ∀ l1' l2' : list B,
omap f l = l1' ++ l2'
→ ∃ l1 l2 : list A, l = l1 ++ l2 ∧ omap f l1 = l1' ∧ omap f l2 = l2'
b: B
Hfa: f a = Some b
H: b :: omap f l = b :: omap f l
∃ l1 l2 : list A,
  a :: l = l1 ++ l2
  ∧ omap f l1 = [] ∧ omap f l2 = b :: omap f l
A, B: Type
f: A → option B
a: A
l: list A
IHl: ∀ l1' l2' : list B,
omap f l = l1' ++ l2'
→ ∃ l1 l2 : list A, l = l1 ++ l2 ∧ omap f l1 = l1' ∧ omap f l2 = l2'
_b: B
l1', l2': list B
Happ_rev: _b :: omap f l = _b :: l1' ++ l2'
Hfa: f a = Some _b
H1: omap f l = l1' ++ l2'
∃ l1 l2 : list A,
  a :: l = l1 ++ l2
  ∧ omap f l1 = _b :: l1' ∧ omap f l2 = l2'
      *A, B: Type
f: A → option B
a: A
l: list A
IHl: ∀ l1' l2' : list B,
omap f l = l1' ++ l2'
→ ∃ l1 l2 : list A, l = l1 ++ l2 ∧ omap f l1 = l1' ∧ omap f l2 = l2'
b: B
Hfa: f a = Some b
H: b :: omap f l = b :: omap f l
∃ l1 l2 : list A,
  a :: l = l1 ++ l2
  ∧ omap f l1 = [] ∧ omap f l2 = b :: omap f l by exists [], (a :: l); cbn; rewrite Hfa.
      *A, B: Type
f: A → option B
a: A
l: list A
IHl: ∀ l1' l2' : list B,
omap f l = l1' ++ l2'
→ ∃ l1 l2 : list A, l = l1 ++ l2 ∧ omap f l1 = l1' ∧ omap f l2 = l2'
_b: B
l1', l2': list B
Happ_rev: _b :: omap f l = _b :: l1' ++ l2'
Hfa: f a = Some _b
H1: omap f l = l1' ++ l2'
∃ l1 l2 : list A,
  a :: l = l1 ++ l2
  ∧ omap f l1 = _b :: l1' ∧ omap f l2 = l2' destruct (IHl _ _ H1) as (_l1 & l2 & -> & <- & <-).A, B: Type
f: A → option B
a: A
_l1, l2: list A
IHl: ∀ l1' l2' : list B,
omap f (_l1 ++ l2) = l1' ++ l2'
→ ∃ l1 l3 : list A,
_l1 ++ l2 = l1 ++ l3 ∧ omap f l1 = l1' ∧ omap f l3 = l2'
_b: B
Happ_rev: _b :: omap f (_l1 ++ l2) =
_b :: omap f _l1 ++ omap f l2
Hfa: f a = Some _b
H1: omap f (_l1 ++ l2) = omap f _l1 ++ omap f l2
∃ l1 l3 : list A,
  a :: _l1 ++ l2 = l1 ++ l3
  ∧ omap f l1 = _b :: omap f _l1
    ∧ omap f l3 = omap f l2
        by exists (a :: _l1), l2; cbn; rewrite Hfa.
Qed.

Lemma omap_length :
  forall {A B : Type} (f : A -> option B) (l : list A),
    Forall (fun a => f a <> None) l -> length (omap f l) = length l.∀ (A B : Type) (f : A → option B) (l : list A),
  Forall (λ a : A, f a ≠ None) l
  → length (omap f l) = length l
Proof.∀ (A B : Type) (f : A → option B) (l : list A),
  Forall (λ a : A, f a ≠ None) l
  → length (omap f l) = length l
  induction 1; cbn; [done |].A, B: Type
f: A → option B
x: A
l: list A
H: f x ≠ None
H0: Forall (λ a : A, f a ≠ None) l
IHForall: length (omap f l) = length l
length
  match f x with
  | Some y => y :: omap f l
  | None => omap f l
  end = S (length l)
  by case_match; cbn; congruence.
Qed.

Lemma omap_nth :
  forall {A B : Type} (f : A -> option B) (l : list A) (i : nat) (dummya : A) (dummyb : B),
    Forall (fun a => f a <> None) l -> i < length l ->
      Some (nth i (omap f l) dummyb) = f (nth i l dummya).∀ (A B : Type) (f : A → option B) (l : list A) (i : nat) 
  (dummya : A) (dummyb : B),
  Forall (λ a : A, f a ≠ None) l
  → i < length l
    → Some (nth i (omap f l) dummyb) =
      f (nth i l dummya)
Proof.∀ (A B : Type) (f : A → option B) (l : list A) (i : nat) 
  (dummya : A) (dummyb : B),
  Forall (λ a : A, f a ≠ None) l
  → i < length l
    → Some (nth i (omap f l) dummyb) =
      f (nth i l dummya)
  intros * Hall; revert i.A, B: Type
f: A → option B
l: list A
dummya: A
dummyb: B
Hall: Forall (λ a : A, f a ≠ None) l
∀ i : nat,
  i < length l
  → Some (nth i (omap f l) dummyb) =
    f (nth i l dummya)
  induction Hall; cbn; intros; [by lia |].A, B: Type
f: A → option B
dummya: A
dummyb: B
x: A
l: list A
H: f x ≠ None
Hall: Forall (λ a : A, f a ≠ None) l
IHHall: ∀ i : nat,
  i < length l
  → Some (nth i (omap f l) dummyb) =
    f (nth i l dummya)
i: nat
H0: i < S (length l)
Some
  (nth i
     match f x with
     | Some y => y :: omap f l
     | None => omap f l
     end dummyb) =
f match i with
  | 0 => x
  | S m => nth m l dummya
  end
  destruct i, (f x); cbn; [done.. | | done].A, B: Type
f: A → option B
dummya: A
dummyb: B
x: A
l: list A
b: B
H: Some b ≠ None
Hall: Forall (λ a : A, f a ≠ None) l
IHHall: ∀ i : nat,
  i < length l
  → Some (nth i (omap f l) dummyb) =
    f (nth i l dummya)
i: nat
H0: S i < S (length l)
Some (nth i (omap f l) dummyb) = f (nth i l dummya)
  by apply IHHall; lia.
Qed.

omap can be expressed as a list_filter_map.

Lemma omap_as_filter :
  forall {A B : Type} (f : A -> option B) (l : list A),
    omap f l = list_filter_map (is_Some ∘ f) (fun x => is_Some_proj (proj2_dsig x)) l.∀ (A B : Type) (f : A → option B) (l : list A),
  omap f l =
  list_filter_map (is_Some ∘ f)
    (λ x : dsig (is_Some ∘ f),
       is_Some_proj (proj2_dsig x)) l
Proof.∀ (A B : Type) (f : A → option B) (l : list A),
  omap f l =
  list_filter_map (is_Some ∘ f)
    (λ x : dsig (is_Some ∘ f),
       is_Some_proj (proj2_dsig x)) l
  induction l; cbn; [done |].A, B: Type
f: A → option B
a: A
l: list A
IHl: omap f l =
list_filter_map (is_Some ∘ f)
(λ x : dsig (is_Some ∘ f), is_Some_proj (proj2_dsig x)) l
match f a with
| Some y => y :: omap f l
| None => omap f l
end =
map
  (λ x : dsig (is_Some ∘ f),
     is_Some_proj (proj2_dsig x))
  match decide (is_Some (f a)) with
  | left p =>
      dexist a p :: filter_annotate (is_Some ∘ f) l
  | right _ => filter_annotate (is_Some ∘ f) l
  end
  case_decide; cbn.A, B: Type
f: A → option B
a: A
l: list A
IHl: omap f l =
list_filter_map (is_Some ∘ f)
(λ x : dsig (is_Some ∘ f), is_Some_proj (proj2_dsig x)) l
H: is_Some (f a)
match f a with
| Some y => y :: omap f l
| None => omap f l
end =
is_Some_proj (proj2_dsig (dexist a H))
:: map
     (λ x : dsig (is_Some ∘ f),
        is_Some_proj (proj2_dsig x))
     (filter_annotate (is_Some ∘ f) l)
A, B: Type
f: A → option B
a: A
l: list A
IHl: omap f l =
list_filter_map (is_Some ∘ f)
(λ x : dsig (is_Some ∘ f), is_Some_proj (proj2_dsig x)) l
H: ¬ is_Some (f a)
match f a with
| Some y => y :: omap f l
| None => omap f l
end =
map
  (λ x : dsig (is_Some ∘ f),
     is_Some_proj (proj2_dsig x))
  (filter_annotate (is_Some ∘ f) l)
  -A, B: Type
f: A → option B
a: A
l: list A
IHl: omap f l =
list_filter_map (is_Some ∘ f)
(λ x : dsig (is_Some ∘ f), is_Some_proj (proj2_dsig x)) l
H: is_Some (f a)
match f a with
| Some y => y :: omap f l
| None => omap f l
end =
is_Some_proj (proj2_dsig (dexist a H))
:: map
     (λ x : dsig (is_Some ∘ f),
        is_Some_proj (proj2_dsig x))
     (filter_annotate (is_Some ∘ f) l) by rewrite IHl; cbv; destruct H as [? ->].
  -A, B: Type
f: A → option B
a: A
l: list A
IHl: omap f l =
list_filter_map (is_Some ∘ f)
(λ x : dsig (is_Some ∘ f), is_Some_proj (proj2_dsig x)) l
H: ¬ is_Some (f a)
match f a with
| Some y => y :: omap f l
| None => omap f l
end =
map
  (λ x : dsig (is_Some ∘ f),
     is_Some_proj (proj2_dsig x))
  (filter_annotate (is_Some ∘ f) l) by destruct (f a); [contradict H |].
Qed.

Lemma omap_Forall :
  forall {A B : Type} (f : A -> option B) (l : list A),
    Forall (fun x => ~ is_Some (f x)) l ->
      omap f l = [].∀ (A B : Type) (f : A → option B) (l : list A),
  Forall (λ x : A, ¬ is_Some (f x)) l → omap f l = []
Proof.∀ (A B : Type) (f : A → option B) (l : list A),
  Forall (λ x : A, ¬ is_Some (f x)) l → omap f l = []
  induction 1 as [| ? ? H]; cbn; [done |].A, B: Type
f: A → option B
x: A
l: list A
H: ¬ is_Some (f x)
H0: Forall (λ x : A, ¬ is_Some (f x)) l
IHForall: omap f l = []
match f x with
| Some y => y :: omap f l
| None => omap f l
end = []
  by case_match; [contradict H |].
Qed.

Lemma NoDup_omap :
  forall {A B : Type} (f : A -> option B) (l : list A),
    (forall a1 a2 : A, is_Some (f a1) -> is_Some (f a2) -> f a1 = f a2 -> a1 = a2) ->
      NoDup l -> NoDup (omap f l).∀ (A B : Type) (f : A → option B) (l : list A),
  (∀ a1 a2 : A,
     is_Some (f a1)
     → is_Some (f a2) → f a1 = f a2 → a1 = a2)
  → NoDup l → NoDup (omap f l)
Proof.∀ (A B : Type) (f : A → option B) (l : list A),
  (∀ a1 a2 : A,
     is_Some (f a1)
     → is_Some (f a2) → f a1 = f a2 → a1 = a2)
  → NoDup l → NoDup (omap f l)
  intros A B f l Hinj Hnd.A, B: Type
f: A → option B
l: list A
Hinj: ∀ a1 a2 : A,
  is_Some (f a1)
  → is_Some (f a2) → f a1 = f a2 → a1 = a2
Hnd: NoDup l
NoDup (omap f l)
  induction Hnd as [| h t Hnin Hnd IH]; cbn; [by constructor |].A, B: Type
f: A → option B
Hinj: ∀ a1 a2 : A,
  is_Some (f a1)
  → is_Some (f a2) → f a1 = f a2 → a1 = a2
h: A
t: list A
Hnin: h ∉ t
Hnd: NoDup t
IH: NoDup (omap f t)
NoDup
  match f h with
  | Some y => y :: omap f t
  | None => omap f t
  end
  destruct (f h) eqn: Heq; [| by apply IH].A, B: Type
f: A → option B
Hinj: ∀ a1 a2 : A,
  is_Some (f a1)
  → is_Some (f a2) → f a1 = f a2 → a1 = a2
h: A
t: list A
Hnin: h ∉ t
Hnd: NoDup t
IH: NoDup (omap f t)
b: B
Heq: f h = Some b
NoDup (b :: omap f t)
  constructor; [| by apply IH].A, B: Type
f: A → option B
Hinj: ∀ a1 a2 : A,
  is_Some (f a1)
  → is_Some (f a2) → f a1 = f a2 → a1 = a2
h: A
t: list A
Hnin: h ∉ t
Hnd: NoDup t
IH: NoDup (omap f t)
b: B
Heq: f h = Some b
b ∉ omap f t
  intros Hin; apply elem_of_list_omap in Hin as (x & Hinx & Hfx).A, B: Type
f: A → option B
Hinj: ∀ a1 a2 : A,
  is_Some (f a1)
  → is_Some (f a2) → f a1 = f a2 → a1 = a2
h: A
t: list A
Hnin: h ∉ t
Hnd: NoDup t
IH: NoDup (omap f t)
b: B
Heq: f h = Some b
x: A
Hinx: x ∈ t
Hfx: f x = Some b
False
  assert (x = h) by (apply Hinj; [done.. | congruence]).A, B: Type
f: A → option B
Hinj: ∀ a1 a2 : A,
  is_Some (f a1)
  → is_Some (f a2) → f a1 = f a2 → a1 = a2
h: A
t: list A
Hnin: h ∉ t
Hnd: NoDup t
IH: NoDup (omap f t)
b: B
Heq: f h = Some b
x: A
Hinx: x ∈ t
Hfx: f x = Some b
H: x = h
False
  by congruence.
Qed.

Unpack list of option A into list of A.

Definition cat_option {A : Type} : list (option A) -> list A :=
  omap id.

Lemma cat_option_length :
  forall {A : Type} (l : list (option A)),
    Forall (fun a => a <> None) l -> length (cat_option l) = length l.∀ (A : Type) (l : list (option A)),
  Forall (λ a : option A, a ≠ None) l
  → length (cat_option l) = length l
Proof.∀ (A : Type) (l : list (option A)),
  Forall (λ a : option A, a ≠ None) l
  → length (cat_option l) = length l
  by intros; apply omap_length.
Qed.

Lemma cat_option_length_le :
  forall {A : Type} (l : list (option A)),
    length (cat_option l) <= length l.∀ (A : Type) (l : list (option A)),
  length (cat_option l) ≤ length l
Proof.∀ (A : Type) (l : list (option A)),
  length (cat_option l) ≤ length l
  by induction l as [| []]; cbn; [| lia..].
Qed.

Lemma cat_option_app :
  forall {A : Type} (l1 l2 : list (option A)),
    cat_option (l1 ++ l2) = cat_option l1 ++ cat_option l2.∀ (A : Type) (l1 l2 : list (option A)),
  cat_option (l1 ++ l2) =
  cat_option l1 ++ cat_option l2
Proof.∀ (A : Type) (l1 l2 : list (option A)),
  cat_option (l1 ++ l2) =
  cat_option l1 ++ cat_option l2
  by unfold cat_option; intros; rewrite omap_app.
Qed.

Lemma cat_option_nth :
  forall {A : Type} (l : list (option A)) (i : nat) (dummya : A),
    Forall (fun a => a <> None) l -> i < length l ->
      Some (nth i (cat_option l) dummya) = (nth i l (Some dummya)).∀ (A : Type) (l : list (option A)) (i : nat) (dummya : A),
  Forall (λ a : option A, a ≠ None) l
  → i < length l
    → Some (nth i (cat_option l) dummya) =
      nth i l (Some dummya)
Proof.∀ (A : Type) (l : list (option A)) (i : nat) (dummya : A),
  Forall (λ a : option A, a ≠ None) l
  → i < length l
    → Some (nth i (cat_option l) dummya) =
      nth i l (Some dummya)
  by unfold cat_option; intros; erewrite omap_nth.
Qed.

Lemma nth_error_eq :
  forall {A : Type} (l1 l2 : list A),
    (forall n : nat, nth_error l1 n = nth_error l2 n) -> l1 = l2.∀ (A : Type) (l1 l2 : list A),
  (∀ n : nat, nth_error l1 n = nth_error l2 n)
  → l1 = l2
Proof.∀ (A : Type) (l1 l2 : list A),
  (∀ n : nat, nth_error l1 n = nth_error l2 n)
  → l1 = l2
  induction l1; intros [| a2 l2] Hnth; [done | ..].A: Type
a2: A
l2: list A
Hnth: ∀ n : nat,
  nth_error [] n = nth_error (a2 :: l2) n
[] = a2 :: l2
A: Type
a: A
l1: list A
IHl1: ∀ l2 : list A,
  (∀ n : nat, nth_error l1 n = nth_error l2 n)
  → l1 = l2
Hnth: ∀ n : nat,
  nth_error (a :: l1) n = nth_error [] n
a :: l1 = []
A: Type
a: A
l1: list A
IHl1: ∀ l2 : list A,
  (∀ n : nat, nth_error l1 n = nth_error l2 n)
  → l1 = l2
a2: A
l2: list A
Hnth: ∀ n : nat,
  nth_error (a :: l1) n =
  nth_error (a2 :: l2) n
a :: l1 = a2 :: l2
  -A: Type
a2: A
l2: list A
Hnth: ∀ n : nat,
  nth_error [] n = nth_error (a2 :: l2) n
[] = a2 :: l2 by specialize (Hnth 0); inversion Hnth.
  -A: Type
a: A
l1: list A
IHl1: ∀ l2 : list A,
  (∀ n : nat, nth_error l1 n = nth_error l2 n)
  → l1 = l2
Hnth: ∀ n : nat,
  nth_error (a :: l1) n = nth_error [] n
a :: l1 = [] by specialize (Hnth 0); inversion Hnth.
  -A: Type
a: A
l1: list A
IHl1: ∀ l2 : list A,
  (∀ n : nat, nth_error l1 n = nth_error l2 n)
  → l1 = l2
a2: A
l2: list A
Hnth: ∀ n : nat,
  nth_error (a :: l1) n =
  nth_error (a2 :: l2) n
a :: l1 = a2 :: l2 f_equal.A: Type
a: A
l1: list A
IHl1: ∀ l2 : list A,
  (∀ n : nat, nth_error l1 n = nth_error l2 n)
  → l1 = l2
a2: A
l2: list A
Hnth: ∀ n : nat,
  nth_error (a :: l1) n =
  nth_error (a2 :: l2) n
a = a2
A: Type
a: A
l1: list A
IHl1: ∀ l2 : list A,
  (∀ n : nat, nth_error l1 n = nth_error l2 n)
  → l1 = l2
a2: A
l2: list A
Hnth: ∀ n : nat,
  nth_error (a :: l1) n =
  nth_error (a2 :: l2) n
l1 = l2
    +A: Type
a: A
l1: list A
IHl1: ∀ l2 : list A,
  (∀ n : nat, nth_error l1 n = nth_error l2 n)
  → l1 = l2
a2: A
l2: list A
Hnth: ∀ n : nat,
  nth_error (a :: l1) n =
  nth_error (a2 :: l2) n
a = a2 by specialize (Hnth 0); cbn in Hnth; congruence.
    +A: Type
a: A
l1: list A
IHl1: ∀ l2 : list A,
  (∀ n : nat, nth_error l1 n = nth_error l2 n)
  → l1 = l2
a2: A
l2: list A
Hnth: ∀ n : nat,
  nth_error (a :: l1) n =
  nth_error (a2 :: l2) n
l1 = l2 apply IHl1; intros n.A: Type
a: A
l1: list A
IHl1: ∀ l2 : list A,
  (∀ n : nat, nth_error l1 n = nth_error l2 n)
  → l1 = l2
a2: A
l2: list A
Hnth: ∀ n : nat,
  nth_error (a :: l1) n =
  nth_error (a2 :: l2) n
n: nat
nth_error l1 n = nth_error l2 n
      by specialize (Hnth (S n)); cbn in Hnth.
Qed.

Compute the list of all decompositions of the given list l into triples (l1, x, l2) such that l = l1 ++ x :: l2.

Fixpoint one_element_decompositions {A : Type} (l : list A) : list (list A * A * list A) :=
  match l with
  | [] => []
  | a :: l' =>
    ([], a, l')
    :: map
      (fun t => match t with (l1, b, l2) => (a :: l1, b, l2) end)
      (one_element_decompositions l')
  end.

Lemma elem_of_one_element_decompositions :
  forall {A : Type} (l pre suf : list A) (x : A),
    (pre, x, suf) ∈ one_element_decompositions l
      <->
    pre ++ [x] ++ suf = l.∀ (A : Type) (l pre suf : list A) (x : A),
  (pre, x, suf) ∈ one_element_decompositions l
  ↔ pre ++ [x] ++ suf = l
Proof.∀ (A : Type) (l pre suf : list A) (x : A),
  (pre, x, suf) ∈ one_element_decompositions l
  ↔ pre ++ [x] ++ suf = l
  induction l; split; cbn; intros Hin.A: Type
pre, suf: list A
x: A
Hin: (pre, x, suf) ∈ []
pre ++ x :: suf = []
A: Type
pre, suf: list A
x: A
Hin: pre ++ x :: suf = []
(pre, x, suf) ∈ []
A: Type
a: A
l: list A
IHl: ∀ (pre suf : list A) (x : A),
(pre, x, suf) ∈ one_element_decompositions l ↔ pre ++ [x] ++ suf = l
pre, suf: list A
x: A
Hin: (pre, x, suf)
∈ ([], a, l)
:: map
(λ t : list A * A * list A,
let (y, l2) := t in let (l1, b) := y in (a :: l1, b, l2))
(one_element_decompositions l)
pre ++ x :: suf = a :: l
A: Type
a: A
l: list A
IHl: ∀ (pre suf : list A) (x : A),
(pre, x, suf) ∈ one_element_decompositions l ↔ pre ++ [x] ++ suf = l
pre, suf: list A
x: A
Hin: pre ++ x :: suf = a :: l
(pre, x, suf)
∈ ([], a, l)
  :: map
       (λ t : list A * A * list A,
          let (y, l2) := t in
          let (l1, b) := y in (a :: l1, b, l2))
       (one_element_decompositions l)
  -A: Type
pre, suf: list A
x: A
Hin: (pre, x, suf) ∈ []
pre ++ x :: suf = [] by inversion Hin.
  -A: Type
pre, suf: list A
x: A
Hin: pre ++ x :: suf = []
(pre, x, suf) ∈ [] by destruct pre; inversion Hin.
  -A: Type
a: A
l: list A
IHl: ∀ (pre suf : list A) (x : A),
(pre, x, suf) ∈ one_element_decompositions l ↔ pre ++ [x] ++ suf = l
pre, suf: list A
x: A
Hin: (pre, x, suf)
∈ ([], a, l)
:: map
(λ t : list A * A * list A,
let (y, l2) := t in let (l1, b) := y in (a :: l1, b, l2))
(one_element_decompositions l)
pre ++ x :: suf = a :: l rewrite elem_of_cons, elem_of_list_fmap in Hin.A: Type
a: A
l: list A
IHl: ∀ (pre suf : list A) (x : A),
(pre, x, suf) ∈ one_element_decompositions l ↔ pre ++ [x] ++ suf = l
pre, suf: list A
x: A
Hin: (pre, x, suf) = ([], a, l)
∨ (∃ y : list A * A * list A,
(pre, x, suf) =
(let (y0, l2) := y in let (l1, b) := y0 in (a :: l1, b, l2))
∧ y ∈ one_element_decompositions l)
pre ++ x :: suf = a :: l
    destruct Hin as [[= -> -> ->] | (((pre', x'), suf') & [= -> -> ->] & Hin)]; [done |].A: Type
a: A
l: list A
IHl: ∀ (pre suf : list A) (x : A),
(pre, x, suf) ∈ one_element_decompositions l ↔ pre ++ [x] ++ suf = l
pre': list A
x': A
suf': list A
Hin: (pre', x', suf') ∈ one_element_decompositions l
(a :: pre') ++ x' :: suf' = a :: l
    by apply (IHl pre' suf' x') in Hin; subst.
  -A: Type
a: A
l: list A
IHl: ∀ (pre suf : list A) (x : A),
(pre, x, suf) ∈ one_element_decompositions l ↔ pre ++ [x] ++ suf = l
pre, suf: list A
x: A
Hin: pre ++ x :: suf = a :: l
(pre, x, suf)
∈ ([], a, l)
  :: map
       (λ t : list A * A * list A,
          let (y, l2) := t in
          let (l1, b) := y in (a :: l1, b, l2))
       (one_element_decompositions l) destruct pre; inversion Hin; subst; clear Hin; [by left |].A: Type
a: A
pre, suf: list A
x: A
IHl: ∀ (pre0 suf0 : list A) (x0 : A),
(pre0, x0, suf0) ∈ one_element_decompositions (pre ++ x :: suf)
↔ pre0 ++ [x0] ++ suf0 = pre ++ x :: suf
(a :: pre, x, suf)
∈ ([], a, pre ++ x :: suf)
  :: map
       (λ t : list A * A * list A,
          let (y, l2) := t in
          let (l1, b) := y in (a :: l1, b, l2))
       (one_element_decompositions (pre ++ x :: suf))
    right.A: Type
a: A
pre, suf: list A
x: A
IHl: ∀ (pre0 suf0 : list A) (x0 : A),
(pre0, x0, suf0) ∈ one_element_decompositions (pre ++ x :: suf)
↔ pre0 ++ [x0] ++ suf0 = pre ++ x :: suf
(a :: pre, x, suf)
∈ map
    (λ t : list A * A * list A,
       let (y, l2) := t in
       let (l1, b) := y in (a :: l1, b, l2))
    (one_element_decompositions (pre ++ x :: suf))
    apply elem_of_list_fmap.A: Type
a: A
pre, suf: list A
x: A
IHl: ∀ (pre0 suf0 : list A) (x0 : A),
(pre0, x0, suf0) ∈ one_element_decompositions (pre ++ x :: suf)
↔ pre0 ++ [x0] ++ suf0 = pre ++ x :: suf
∃ y : list A * A * list A,
  (a :: pre, x, suf) =
  (let (y0, l2) := y in
   let (l1, b) := y0 in (a :: l1, b, l2))
  ∧ y ∈ one_element_decompositions (pre ++ x :: suf)
    exists (pre, x, suf).A: Type
a: A
pre, suf: list A
x: A
IHl: ∀ (pre0 suf0 : list A) (x0 : A),
(pre0, x0, suf0) ∈ one_element_decompositions (pre ++ x :: suf)
↔ pre0 ++ [x0] ++ suf0 = pre ++ x :: suf
(a :: pre, x, suf) = (a :: pre, x, suf)
∧ (pre, x, suf)
  ∈ one_element_decompositions (pre ++ x :: suf)
    by rewrite IHl.
Qed.

Compute the list of all decompositions of the given list l into tuples (l1, x, l2, y, l3) such that l = l1 ++ x :: l2 ++ y :: l3.

Definition two_element_decompositions
  {A : Type} (l : list A) : list (list A * A * list A * A * list A) :=
  flat_map
    (fun t =>
      match t with
        (l1, e1, l2) =>
        map
          (fun t => match t with (l2', e2, l3) => (l1, e1, l2', e2, l3) end)
          (one_element_decompositions l2)
      end)
    (one_element_decompositions l).

Lemma elem_of_two_element_decompositions :
  forall {A : Type} (l pre mid suf : list A) (x y : A),
    (pre, x, mid, y, suf) ∈ two_element_decompositions l
      <->
    pre ++ [x] ++ mid ++ [y] ++ suf = l.∀ (A : Type) (l pre mid suf : list A) (x y : A),
  (pre, x, mid, y, suf) ∈ two_element_decompositions l
  ↔ pre ++ [x] ++ mid ++ [y] ++ suf = l
Proof.∀ (A : Type) (l pre mid suf : list A) (x y : A),
  (pre, x, mid, y, suf) ∈ two_element_decompositions l
  ↔ pre ++ [x] ++ mid ++ [y] ++ suf = l
  intros.A: Type
l, pre, mid, suf: list A
x, y: A
(pre, x, mid, y, suf) ∈ two_element_decompositions l
↔ pre ++ [x] ++ mid ++ [y] ++ suf = l
  unfold two_element_decompositions.A: Type
l, pre, mid, suf: list A
x, y: A
(pre, x, mid, y, suf)
∈ flat_map
    (λ t : list A * A * list A,
       let (y, l2) := t in
       let (l1, e1) := y in
       map
         (λ t0 : list A * A * list A,
            let (y0, l3) := t0 in
            let (l2', e2) := y0 in
            (l1, e1, l2', e2, l3))
         (one_element_decompositions l2))
    (one_element_decompositions l)
↔ pre ++ [x] ++ mid ++ [y] ++ suf = l
  rewrite elem_of_list_In, in_flat_map; setoid_rewrite <- elem_of_list_In.A: Type
l, pre, mid, suf: list A
x, y: A
(∃ x0 : list A * A * list A,
   x0 ∈ one_element_decompositions l
   ∧ (pre, x, mid, y, suf)
     ∈ (let (y, l2) := x0 in
        let (l1, e1) := y in
        map
          (λ t : list A * A * list A,
             let (y0, l3) := t in
             let (l2', e2) := y0 in
             (l1, e1, l2', e2, l3))
          (one_element_decompositions l2)))
↔ pre ++ [x] ++ mid ++ [y] ++ suf = l
  split.A: Type
l, pre, mid, suf: list A
x, y: A
(∃ x0 : list A * A * list A,
   x0 ∈ one_element_decompositions l
   ∧ (pre, x, mid, y, suf)
     ∈ (let (y, l2) := x0 in
        let (l1, e1) := y in
        map
          (λ t : list A * A * list A,
             let (y0, l3) := t in
             let (l2', e2) := y0 in
             (l1, e1, l2', e2, l3))
          (one_element_decompositions l2)))
→ pre ++ [x] ++ mid ++ [y] ++ suf = l
A: Type
l, pre, mid, suf: list A
x, y: A
pre ++ [x] ++ mid ++ [y] ++ suf = l
→ ∃ x0 : list A * A * list A,
    x0 ∈ one_element_decompositions l
    ∧ (pre, x, mid, y, suf)
      ∈ (let (y, l2) := x0 in
         let (l1, e1) := y in
         map
           (λ t : list A * A * list A,
              let (y0, l3) := t in
              let (l2', e2) := y0 in
              (l1, e1, l2', e2, l3))
           (one_element_decompositions l2))
  -A: Type
l, pre, mid, suf: list A
x, y: A
(∃ x0 : list A * A * list A,
   x0 ∈ one_element_decompositions l
   ∧ (pre, x, mid, y, suf)
     ∈ (let (y, l2) := x0 in
        let (l1, e1) := y in
        map
          (λ t : list A * A * list A,
             let (y0, l3) := t in
             let (l2', e2) := y0 in
             (l1, e1, l2', e2, l3))
          (one_element_decompositions l2)))
→ pre ++ [x] ++ mid ++ [y] ++ suf = l intros [((pre', x'), sufx) [Hdecx Hin]].A: Type
l, pre, mid, suf: list A
x, y: A
pre': list A
x': A
sufx: list A
Hdecx: (pre', x', sufx)
∈ one_element_decompositions l
Hin: (pre, x, mid, y, suf)
∈ map
    (λ t : list A * A * list A,
       let (y, l3) := t in
       let (l2', e2) := y in
       (pre', x', l2', e2, l3))
    (one_element_decompositions sufx)
pre ++ [x] ++ mid ++ [y] ++ suf = l
    apply elem_of_list_fmap in Hin as [[[mid' y'] suf'] [[= -> -> -> -> ->] Hin]].A: Type
l, pre': list A
x': A
sufx: list A
Hdecx: (pre', x', sufx)
∈ one_element_decompositions l
mid': list A
y': A
suf': list A
Hin: (mid', y', suf')
∈ one_element_decompositions sufx
pre' ++ [x'] ++ mid' ++ [y'] ++ suf' = l
    by apply elem_of_one_element_decompositions in Hdecx as <-, Hin as <-.
  -A: Type
l, pre, mid, suf: list A
x, y: A
pre ++ [x] ++ mid ++ [y] ++ suf = l
→ ∃ x0 : list A * A * list A,
    x0 ∈ one_element_decompositions l
    ∧ (pre, x, mid, y, suf)
      ∈ (let (y, l2) := x0 in
         let (l1, e1) := y in
         map
           (λ t : list A * A * list A,
              let (y0, l3) := t in
              let (l2', e2) := y0 in
              (l1, e1, l2', e2, l3))
           (one_element_decompositions l2)) intros H.A: Type
l, pre, mid, suf: list A
x, y: A
H: pre ++ [x] ++ mid ++ [y] ++ suf = l
∃ x0 : list A * A * list A,
  x0 ∈ one_element_decompositions l
  ∧ (pre, x, mid, y, suf)
    ∈ (let (y, l2) := x0 in
       let (l1, e1) := y in
       map
         (λ t : list A * A * list A,
            let (y0, l3) := t in
            let (l2', e2) := y0 in
            (l1, e1, l2', e2, l3))
         (one_element_decompositions l2))
    apply elem_of_one_element_decompositions in H.A: Type
l, pre, mid, suf: list A
x, y: A
H: (pre, x, mid ++ [y] ++ suf)
∈ one_element_decompositions l
∃ x0 : list A * A * list A,
  x0 ∈ one_element_decompositions l
  ∧ (pre, x, mid, y, suf)
    ∈ (let (y, l2) := x0 in
       let (l1, e1) := y in
       map
         (λ t : list A * A * list A,
            let (y0, l3) := t in
            let (l2', e2) := y0 in
            (l1, e1, l2', e2, l3))
         (one_element_decompositions l2))
    exists (pre, x, mid ++ [y] ++ suf).A: Type
l, pre, mid, suf: list A
x, y: A
H: (pre, x, mid ++ [y] ++ suf)
∈ one_element_decompositions l
(pre, x, mid ++ [y] ++ suf)
∈ one_element_decompositions l
∧ (pre, x, mid, y, suf)
  ∈ map
      (λ t : list A * A * list A,
         let (y, l3) := t in
         let (l2', e2) := y in (pre, x, l2', e2, l3))
      (one_element_decompositions (mid ++ [y] ++ suf))
    split; [done |].A: Type
l, pre, mid, suf: list A
x, y: A
H: (pre, x, mid ++ [y] ++ suf)
∈ one_element_decompositions l
(pre, x, mid, y, suf)
∈ map
    (λ t : list A * A * list A,
       let (y, l3) := t in
       let (l2', e2) := y in (pre, x, l2', e2, l3))
    (one_element_decompositions (mid ++ [y] ++ suf))
    apply elem_of_list_fmap.A: Type
l, pre, mid, suf: list A
x, y: A
H: (pre, x, mid ++ [y] ++ suf)
∈ one_element_decompositions l
∃ y0 : list A * A * list A,
  (pre, x, mid, y, suf) =
  (let (y, l3) := y0 in
   let (l2', e2) := y in (pre, x, l2', e2, l3))
  ∧ y0
    ∈ one_element_decompositions (mid ++ [y] ++ suf)
    exists (mid, y, suf).A: Type
l, pre, mid, suf: list A
x, y: A
H: (pre, x, mid ++ [y] ++ suf)
∈ one_element_decompositions l
(pre, x, mid, y, suf) = (pre, x, mid, y, suf)
∧ (mid, y, suf)
  ∈ one_element_decompositions (mid ++ [y] ++ suf)
    by rewrite elem_of_one_element_decompositions.
Qed.

Lemma order_decompositions :
  forall {A : Type} (pre1 suf1 pre2 suf2 : list A),
    pre1 ++ suf1 = pre2 ++ suf2 ->
    pre1 = pre2 \/ (exists suf1', pre1 = pre2 ++ suf1') \/ (exists suf2', pre2 = pre1 ++ suf2').∀ (A : Type) (pre1 suf1 pre2 suf2 : list A),
  pre1 ++ suf1 = pre2 ++ suf2
  → pre1 = pre2
    ∨ (∃ suf1' : list A, pre1 = pre2 ++ suf1')
      ∨ (∃ suf2' : list A, pre2 = pre1 ++ suf2')
Proof.∀ (A : Type) (pre1 suf1 pre2 suf2 : list A),
  pre1 ++ suf1 = pre2 ++ suf2
  → pre1 = pre2
    ∨ (∃ suf1' : list A, pre1 = pre2 ++ suf1')
      ∨ (∃ suf2' : list A, pre2 = pre1 ++ suf2')
  induction pre1; destruct pre2; cbn; [by eauto.. |].A: Type
a: A
pre1: list A
IHpre1: ∀ suf1 pre2 suf2 : list A,
  pre1 ++ suf1 = pre2 ++ suf2
  → pre1 = pre2
    ∨ (∃ suf1' : list A, pre1 = pre2 ++ suf1')
      ∨ (∃ suf2' : list A,
           pre2 = pre1 ++ suf2')
suf1: list A
a0: A
pre2: list A
∀ suf2 : list A,
  a :: pre1 ++ suf1 = a0 :: pre2 ++ suf2
  → a :: pre1 = a0 :: pre2
    ∨ (∃ suf1' : list A,
         a :: pre1 = a0 :: pre2 ++ suf1')
      ∨ (∃ suf2' : list A,
           a0 :: pre2 = a :: pre1 ++ suf2')
  inversion 1; subst.A: Type
pre1: list A
IHpre1: ∀ suf1 pre2 suf2 : list A,
  pre1 ++ suf1 = pre2 ++ suf2
  → pre1 = pre2
    ∨ (∃ suf1' : list A, pre1 = pre2 ++ suf1')
      ∨ (∃ suf2' : list A,
           pre2 = pre1 ++ suf2')
suf1: list A
a0: A
pre2, suf2: list A
H: a0 :: pre1 ++ suf1 = a0 :: pre2 ++ suf2
H2: pre1 ++ suf1 = pre2 ++ suf2
a0 :: pre1 = a0 :: pre2
∨ (∃ suf1' : list A, a0 :: pre1 = a0 :: pre2 ++ suf1')
  ∨ (∃ suf2' : list A,
       a0 :: pre2 = a0 :: pre1 ++ suf2')
  by edestruct IHpre1 as [| [[] | []]]; [done | subst; eauto..].
Qed.

Lemma list_max_exists :
  forall (l : list nat),
    l <> [] -> list_max l ∈ l.∀ l : list nat, l ≠ [] → list_max l ∈ l
Proof.∀ l : list nat, l ≠ [] → list_max l ∈ l
  induction l as [| h t]; cbn; intros; [done |].h: nat
t: list nat
IHt: t ≠ [] → list_max t ∈ t
H: h :: t ≠ []
h `max` foldr Init.Nat.max 0 t ∈ h :: t
  destruct (PeanoNat.Nat.max_spec h (foldr Init.Nat.max 0 t))
    as [[Hlt ->] | [Hle ->]]; [| by left].h: nat
t: list nat
IHt: t ≠ [] → list_max t ∈ t
H: h :: t ≠ []
Hlt: h < foldr Init.Nat.max 0 t
foldr Init.Nat.max 0 t ∈ h :: t
  right; apply IHt.h: nat
t: list nat
IHt: t ≠ [] → list_max t ∈ t
H: h :: t ≠ []
Hlt: h < foldr Init.Nat.max 0 t
t ≠ []
  by destruct t; [cbn in Hlt; lia |].
Qed.

Returns all values which occur with maximum frequency in the given list. Note that these values are returned with their original multiplicity.

Definition mode `{EqDecision A} (l : list A) : list A :=
  let mode_value := list_max (List.map (count_occ decide_eq l) l) in
    filter (fun a => (count_occ decide_eq l a) = mode_value) l.

Example mode1 : mode [1; 1; 2; 3; 3] = [1; 1; 3; 3].mode [1; 1; 2; 3; 3] = [1; 1; 3; 3]
Proof.mode [1; 1; 2; 3; 3] = [1; 1; 3; 3] by itauto. Qed.

Computes the list suff which satisfies pref ++ suff = l or reports that no such list exists.

Fixpoint complete_prefix `{EqDecision A} (l pref : list A) : option (list A) :=
  match l, pref with
  | l , [] => Some l
  | [], b :: pref' => None
  | a :: l', b :: pref' => if decide (a = b) then complete_prefix l' pref' else None
  end.

Example complete_prefix_some : complete_prefix [1; 2; 3; 4] [1; 2] = Some [3; 4].complete_prefix [1; 2; 3; 4] [1; 2] = Some [3; 4]
Proof.complete_prefix [1; 2; 3; 4] [1; 2] = Some [3; 4] by itauto. Qed.

Example complete_prefix_none : complete_prefix [1; 2; 3; 4] [1; 3] = None.complete_prefix [1; 2; 3; 4] [1; 3] = None
Proof.complete_prefix [1; 2; 3; 4] [1; 3] = None by itauto. Qed.

Lemma complete_prefix_empty `{EqDecision A} :
  forall (l : list A),
    complete_prefix l [] = Some l.A: Type
EqDecision0: EqDecision A
∀ l : list A, complete_prefix l [] = Some l
Proof.A: Type
EqDecision0: EqDecision A
∀ l : list A, complete_prefix l [] = Some l
  by induction l.
Qed.

Lemma complete_prefix_correct `{EqDecision A} :
  forall (l pref suff : list A),
    l = pref ++ suff <-> complete_prefix l pref = Some suff.A: Type
EqDecision0: EqDecision A
∀ l pref suff : list A,
  l = pref ++ suff
  ↔ complete_prefix l pref = Some suff
Proof.A: Type
EqDecision0: EqDecision A
∀ l pref suff : list A,
  l = pref ++ suff
  ↔ complete_prefix l pref = Some suff
  induction l; intros [] suff; cbn; [by itauto congruence.. |].A: Type
EqDecision0: EqDecision A
a: A
l: list A
IHl: ∀ pref suff : list A,
  l = pref ++ suff
  ↔ complete_prefix l pref = Some suff
a0: A
l0, suff: list A
a :: l = a0 :: l0 ++ suff
↔ (if decide (a = a0)
   then complete_prefix l l0
   else None) = Some suff
  case_decide; [| by itauto congruence].A: Type
EqDecision0: EqDecision A
a: A
l: list A
IHl: ∀ pref suff : list A,
  l = pref ++ suff
  ↔ complete_prefix l pref = Some suff
a0: A
l0, suff: list A
H: a = a0
a :: l = a0 :: l0 ++ suff
↔ complete_prefix l l0 = Some suff
  by rewrite <- IHl; itauto congruence.
Qed.

Computes the list pref which satisfies pref ++ suff = l or reports that no such list exists.

Definition complete_suffix `{EqDecision A} (l suff : list A) : option (list A) :=
  match complete_prefix (rev l) (rev suff) with
  | None => None
  | Some ls => Some (rev ls)
  end.

Example complete_suffix_some : complete_suffix [1; 2; 3; 4] [3; 4] = Some [1; 2].complete_suffix [1; 2; 3; 4] [3; 4] = Some [1; 2]
Proof.complete_suffix [1; 2; 3; 4] [3; 4] = Some [1; 2] by itauto. Qed.

Lemma complete_suffix_correct `{EqDecision A} :
  forall (l pref suff : list A),
    l = pref ++ suff <-> complete_suffix l suff = Some pref.A: Type
EqDecision0: EqDecision A
∀ l pref suff : list A,
  l = pref ++ suff
  ↔ complete_suffix l suff = Some pref
Proof.A: Type
EqDecision0: EqDecision A
∀ l pref suff : list A,
  l = pref ++ suff
  ↔ complete_suffix l suff = Some pref
  split; unfold complete_suffix.A: Type
EqDecision0: EqDecision A
l, pref, suff: list A
l = pref ++ suff
→ match complete_prefix (rev l) (rev suff) with
  | Some ls => Some (rev ls)
  | None => None
  end = Some pref
A: Type
EqDecision0: EqDecision A
l, pref, suff: list A
match complete_prefix (rev l) (rev suff) with
| Some ls => Some (rev ls)
| None => None
end = Some pref → l = pref ++ suff
  -A: Type
EqDecision0: EqDecision A
l, pref, suff: list A
l = pref ++ suff
→ match complete_prefix (rev l) (rev suff) with
  | Some ls => Some (rev ls)
  | None => None
  end = Some pref intros ->.A: Type
EqDecision0: EqDecision A
pref, suff: list A
match
  complete_prefix (rev (pref ++ suff)) (rev suff)
with
| Some ls => Some (rev ls)
| None => None
end = Some pref
    replace (complete_prefix _ _) with (Some (rev pref)).A: Type
EqDecision0: EqDecision A
pref, suff: list A
Some (rev (rev pref)) = Some pref
A: Type
EqDecision0: EqDecision A
pref, suff: list A
Some (rev pref) =
complete_prefix (rev (pref ++ suff)) (rev suff)
    +A: Type
EqDecision0: EqDecision A
pref, suff: list A
Some (rev (rev pref)) = Some pref by rewrite rev_involutive.
    +A: Type
EqDecision0: EqDecision A
pref, suff: list A
Some (rev pref) =
complete_prefix (rev (pref ++ suff)) (rev suff) symmetry; apply complete_prefix_correct.A: Type
EqDecision0: EqDecision A
pref, suff: list A
rev (pref ++ suff) = rev suff ++ rev pref
      by rewrite rev_app_distr.
  -A: Type
EqDecision0: EqDecision A
l, pref, suff: list A
match complete_prefix (rev l) (rev suff) with
| Some ls => Some (rev ls)
| None => None
end = Some pref → l = pref ++ suff destruct (complete_prefix (rev l) (rev suff)) eqn: Heq; intros [= <-].A: Type
EqDecision0: EqDecision A
l, suff, l0: list A
Heq: complete_prefix (rev l) (rev suff) = Some l0
l = rev l0 ++ suff
    apply complete_prefix_correct in Heq.A: Type
EqDecision0: EqDecision A
l, suff, l0: list A
Heq: rev l = rev suff ++ l0
l = rev l0 ++ suff
    apply rev_eq_app in Heq.A: Type
EqDecision0: EqDecision A
l, suff, l0: list A
Heq: l = rev l0 ++ rev (rev suff)
l = rev l0 ++ suff
    by rewrite rev_involutive in Heq.
Qed.

Lemma complete_suffix_empty `{EqDecision A} :
  forall (l : list A),
    complete_suffix l [] = Some l.A: Type
EqDecision0: EqDecision A
∀ l : list A, complete_suffix l [] = Some l
Proof.A: Type
EqDecision0: EqDecision A
∀ l : list A, complete_suffix l [] = Some l
  unfold complete_suffix; cbn; intros.A: Type
EqDecision0: EqDecision A
l: list A
match complete_prefix (rev l) [] with
| Some ls => Some (rev ls)
| None => None
end = Some l
  by rewrite complete_prefix_empty, rev_involutive.
Qed.

Keep elements which are inl but throw away those that are inr.

Definition list_sum_project_left {A B : Type} (x : list (A + B)) : list A :=
  omap sum_project_left x.

Keep elements which are inr but throw away those that are inl.

Definition list_sum_project_right {A B : Type} (x : list (A + B)) : list B :=
  omap sum_project_right x.

Lemma fold_right_andb_false :
  forall (l : list bool),
    fold_right andb false l = false.∀ l : list bool, foldr andb false l = false
Proof.∀ l : list bool, foldr andb false l = false
  induction l; cbn; [done |].a: bool
l: list bool
IHl: foldr andb false l = false
a && foldr andb false l = false
  by rewrite IHl, andb_false_r.
Qed.

Lemma sumbool_forall :
  forall {A : Type} {P Q : A -> Prop},
    (forall x : A, {P x} + {Q x}) ->
    forall l : list A, {Forall P l} + {Exists Q l}.∀ (A : Type) (P Q : A → Prop),
  (∀ x : A, {P x} + {Q x})
  → ∀ l : list A, {Forall P l} + {Exists Q l}
Proof.∀ (A : Type) (P Q : A → Prop),
  (∀ x : A, {P x} + {Q x})
  → ∀ l : list A, {Forall P l} + {Exists Q l}
  intros A P Q Hdec.A: Type
P, Q: A → Prop
Hdec: ∀ x : A, {P x} + {Q x}
∀ l : list A, {Forall P l} + {Exists Q l}
  induction l; [by left; constructor |].A: Type
P, Q: A → Prop
Hdec: ∀ x : A, {P x} + {Q x}
a: A
l: list A
IHl: {Forall P l} + {Exists Q l}
{Forall P (a :: l)} + {Exists Q (a :: l)}
  destruct (Hdec a); [| by right; constructor].A: Type
P, Q: A → Prop
Hdec: ∀ x : A, {P x} + {Q x}
a: A
l: list A
IHl: {Forall P l} + {Exists Q l}
p: P a
{Forall P (a :: l)} + {Exists Q (a :: l)}
  by destruct IHl; [left | right]; constructor.
Qed.

Lemma list_sum_map :
  forall {A : Type} (f g : A -> nat) (l : list A),
    (forall x : A, x ∈ l -> f x <= g x) ->
      list_sum (map f l) <= list_sum (map g l).∀ (A : Type) (f g : A → nat) (l : list A),
  (∀ x : A, x ∈ l → f x ≤ g x)
  → list_sum (map f l) ≤ list_sum (map g l)
Proof.∀ (A : Type) (f g : A → nat) (l : list A),
  (∀ x : A, x ∈ l → f x ≤ g x)
  → list_sum (map f l) ≤ list_sum (map g l)
  induction l as [| h t]; cbn; intros Hle; [done |].A: Type
f, g: A → nat
h: A
t: list A
IHt: (∀ x : A, x ∈ t → f x ≤ g x) → list_sum (map f t) ≤ list_sum (map g t)
Hle: ∀ x : A, x ∈ h :: t → f x ≤ g x
f h + foldr Init.Nat.add 0 (map f t)
≤ g h + foldr Init.Nat.add 0 (map g t)
  apply PeanoNat.Nat.add_le_mono.A: Type
f, g: A → nat
h: A
t: list A
IHt: (∀ x : A, x ∈ t → f x ≤ g x) → list_sum (map f t) ≤ list_sum (map g t)
Hle: ∀ x : A, x ∈ h :: t → f x ≤ g x
f h ≤ g h
A: Type
f, g: A → nat
h: A
t: list A
IHt: (∀ x : A, x ∈ t → f x ≤ g x) → list_sum (map f t) ≤ list_sum (map g t)
Hle: ∀ x : A, x ∈ h :: t → f x ≤ g x
foldr Init.Nat.add 0 (map f t)
≤ foldr Init.Nat.add 0 (map g t)
  -A: Type
f, g: A → nat
h: A
t: list A
IHt: (∀ x : A, x ∈ t → f x ≤ g x) → list_sum (map f t) ≤ list_sum (map g t)
Hle: ∀ x : A, x ∈ h :: t → f x ≤ g x
f h ≤ g h by apply Hle; left.
  -A: Type
f, g: A → nat
h: A
t: list A
IHt: (∀ x : A, x ∈ t → f x ≤ g x) → list_sum (map f t) ≤ list_sum (map g t)
Hle: ∀ x : A, x ∈ h :: t → f x ≤ g x
foldr Init.Nat.add 0 (map f t)
≤ foldr Init.Nat.add 0 (map g t) apply IHt; intros x Hin.A: Type
f, g: A → nat
h: A
t: list A
IHt: (∀ x : A, x ∈ t → f x ≤ g x) → list_sum (map f t) ≤ list_sum (map g t)
Hle: ∀ x : A, x ∈ h :: t → f x ≤ g x
x: A
Hin: x ∈ t
f x ≤ g x
    by apply Hle; right.
Qed.

Lemma list_sum_decrease :
  forall {A : Type} (f g : A -> nat) (l : list A),
    (forall a, a ∈ l -> f a <= g a) ->
    Exists (fun a => f a < g a) l ->
      list_sum (map f l) < list_sum (map g l).∀ (A : Type) (f g : A → nat) (l : list A),
  (∀ a : A, a ∈ l → f a ≤ g a)
  → Exists (λ a : A, f a < g a) l
    → list_sum (map f l) < list_sum (map g l)
Proof.∀ (A : Type) (f g : A → nat) (l : list A),
  (∀ a : A, a ∈ l → f a ≤ g a)
  → Exists (λ a : A, f a < g a) l
    → list_sum (map f l) < list_sum (map g l)
  intros A f g l Hall Hex.A: Type
f, g: A → nat
l: list A
Hall: ∀ a : A, a ∈ l → f a ≤ g a
Hex: Exists (λ a : A, f a < g a) l
list_sum (map f l) < list_sum (map g l)
  induction Hex; cbn.A: Type
f, g: A → nat
x: A
l: list A
Hall: ∀ a : A, a ∈ x :: l → f a ≤ g a
H: f x < g x
f x + foldr Init.Nat.add 0 (map f l) <
g x + foldr Init.Nat.add 0 (map g l)
A: Type
f, g: A → nat
x: A
l: list A
Hall: ∀ a : A, a ∈ x :: l → f a ≤ g a
Hex: Exists (λ a : A, f a < g a) l
IHHex: (∀ a : A, a ∈ l → f a ≤ g a)
→ list_sum (map f l) < list_sum (map g l)
f x + foldr Init.Nat.add 0 (map f l) <
g x + foldr Init.Nat.add 0 (map g l)
  -A: Type
f, g: A → nat
x: A
l: list A
Hall: ∀ a : A, a ∈ x :: l → f a ≤ g a
H: f x < g x
f x + foldr Init.Nat.add 0 (map f l) <
g x + foldr Init.Nat.add 0 (map g l) apply PeanoNat.Nat.add_lt_le_mono; [done |].A: Type
f, g: A → nat
x: A
l: list A
Hall: ∀ a : A, a ∈ x :: l → f a ≤ g a
H: f x < g x
foldr Init.Nat.add 0 (map f l)
≤ foldr Init.Nat.add 0 (map g l)
    apply list_sum_map.A: Type
f, g: A → nat
x: A
l: list A
Hall: ∀ a : A, a ∈ x :: l → f a ≤ g a
H: f x < g x
∀ x : A, x ∈ l → f x ≤ g x
    intros a' Hin.A: Type
f, g: A → nat
x: A
l: list A
Hall: ∀ a : A, a ∈ x :: l → f a ≤ g a
H: f x < g x
a': A
Hin: a' ∈ l
f a' ≤ g a'
    by apply Hall; right.
  -A: Type
f, g: A → nat
x: A
l: list A
Hall: ∀ a : A, a ∈ x :: l → f a ≤ g a
Hex: Exists (λ a : A, f a < g a) l
IHHex: (∀ a : A, a ∈ l → f a ≤ g a)
→ list_sum (map f l) < list_sum (map g l)
f x + foldr Init.Nat.add 0 (map f l) <
g x + foldr Init.Nat.add 0 (map g l) apply PeanoNat.Nat.add_le_lt_mono; [by apply Hall; left |].A: Type
f, g: A → nat
x: A
l: list A
Hall: ∀ a : A, a ∈ x :: l → f a ≤ g a
Hex: Exists (λ a : A, f a < g a) l
IHHex: (∀ a : A, a ∈ l → f a ≤ g a)
→ list_sum (map f l) < list_sum (map g l)
foldr Init.Nat.add 0 (map f l) <
foldr Init.Nat.add 0 (map g l)
    apply IHHex.A: Type
f, g: A → nat
x: A
l: list A
Hall: ∀ a : A, a ∈ x :: l → f a ≤ g a
Hex: Exists (λ a : A, f a < g a) l
IHHex: (∀ a : A, a ∈ l → f a ≤ g a)
→ list_sum (map f l) < list_sum (map g l)
∀ a : A, a ∈ l → f a ≤ g a
    intros a Hin.A: Type
f, g: A → nat
x: A
l: list A
Hall: ∀ a : A, a ∈ x :: l → f a ≤ g a
Hex: Exists (λ a : A, f a < g a) l
IHHex: (∀ a : A, a ∈ l → f a ≤ g a)
→ list_sum (map f l) < list_sum (map g l)
a: A
Hin: a ∈ l
f a ≤ g a
    by apply Hall; right.
Qed.

Nearly the natural induction principle for fold_left. Useful if you can think of fold_left f as transforming a list into a B → B function, and can describe the effect with a P : list A → relation B. The assumption Hstep could be weakened by replacing r with fold_left f l (f x a), but that isn't useful in natural examples.

Lemma fold_left_ind :
  forall {A B : Type} (f : B -> A -> B) (P : list A -> B -> B -> Prop)
    (Hstart : forall x, P nil x x)
    (Hstep : forall x a l r, P l (f x a) r -> P (a :: l) x r),
  forall l x, P l x (fold_left f l x).∀ (A B : Type) (f : B → A → B) (P : list A
                                    → B → B → Prop),
  (∀ x : B, P [] x x)
  → (∀ (x : B) (a : A) (l : list A) (r : B),
       P l (f x a) r → P (a :: l) x r)
    → ∀ (l : list A) (x : B), P l x (fold_left f l x)
Proof.∀ (A B : Type) (f : B → A → B) (P : list A
                                    → B → B → Prop),
  (∀ x : B, P [] x x)
  → (∀ (x : B) (a : A) (l : list A) (r : B),
       P l (f x a) r → P (a :: l) x r)
    → ∀ (l : list A) (x : B), P l x (fold_left f l x)
  induction l.A, B: Type
f: B → A → B
P: list A → B → B → Prop
Hstart: ∀ x : B, P [] x x
Hstep: ∀ (x : B) (a : A) (l : list A) (r : B),
  P l (f x a) r → P (a :: l) x r
∀ x : B, P [] x (fold_left f [] x)
A, B: Type
f: B → A → B
P: list A → B → B → Prop
Hstart: ∀ x : B, P [] x x
Hstep: ∀ (x : B) (a : A) (l : list A) (r : B),
  P l (f x a) r → P (a :: l) x r
a: A
l: list A
IHl: ∀ x : B, P l x (fold_left f l x)
∀ x : B, P (a :: l) x (fold_left f (a :: l) x)
  -A, B: Type
f: B → A → B
P: list A → B → B → Prop
Hstart: ∀ x : B, P [] x x
Hstep: ∀ (x : B) (a : A) (l : list A) (r : B),
  P l (f x a) r → P (a :: l) x r
∀ x : B, P [] x (fold_left f [] x) by apply Hstart.
  -A, B: Type
f: B → A → B
P: list A → B → B → Prop
Hstart: ∀ x : B, P [] x x
Hstep: ∀ (x : B) (a : A) (l : list A) (r : B),
  P l (f x a) r → P (a :: l) x r
a: A
l: list A
IHl: ∀ x : B, P l x (fold_left f l x)
∀ x : B, P (a :: l) x (fold_left f (a :: l) x) by intros x; apply Hstep, IHl.
Qed.

An induction principle for fold_left which decomposes the list from the right.

Lemma fold_left_ind_rev :
  forall {A B : Type} (f : B -> A -> B) (x0 : B) (P : list A -> B -> Prop)
    (Hstart : P nil x0)
    (Hstep : forall l a x, P l x -> P (l ++ [a]) (f x a)),
  forall l, P l (fold_left f l x0).∀ (A B : Type) (f : B → A → B) (x0 : B) (P : list A
                                             → B
                                               → Prop),
  P [] x0
  → (∀ (l : list A) (a : A) (x : B),
       P l x → P (l ++ [a]) (f x a))
    → ∀ l : list A, P l (fold_left f l x0)
Proof.∀ (A B : Type) (f : B → A → B) (x0 : B) (P : list A
                                             → B
                                               → Prop),
  P [] x0
  → (∀ (l : list A) (a : A) (x : B),
       P l x → P (l ++ [a]) (f x a))
    → ∀ l : list A, P l (fold_left f l x0)
  induction l using rev_ind.A, B: Type
f: B → A → B
x0: B
P: list A → B → Prop
Hstart: P [] x0
Hstep: ∀ (l : list A) (a : A) (x : B),
  P l x → P (l ++ [a]) (f x a)
P [] (fold_left f [] x0)
A, B: Type
f: B → A → B
x0: B
P: list A → B → Prop
Hstart: P [] x0
Hstep: ∀ (l : list A) (a : A) (x : B),
  P l x → P (l ++ [a]) (f x a)
x: A
l: list A
IHl: P l (fold_left f l x0)
P (l ++ [x]) (fold_left f (l ++ [x]) x0)
  -A, B: Type
f: B → A → B
x0: B
P: list A → B → Prop
Hstart: P [] x0
Hstep: ∀ (l : list A) (a : A) (x : B),
  P l x → P (l ++ [a]) (f x a)
P [] (fold_left f [] x0) by apply Hstart.
  -A, B: Type
f: B → A → B
x0: B
P: list A → B → Prop
Hstart: P [] x0
Hstep: ∀ (l : list A) (a : A) (x : B),
  P l x → P (l ++ [a]) (f x a)
x: A
l: list A
IHl: P l (fold_left f l x0)
P (l ++ [x]) (fold_left f (l ++ [x]) x0) by rewrite fold_left_app; apply Hstep.
Qed.

Section sec_suffix_quantifiers.

Quantifiers for all suffixes

In this section we define inductive quantifiers for lists that are concerned with predicates over the sublists of the list instead of the elements. They are analogous to Streams.ForAll and Streams.Exists. We prove several properties about them.

Among the definitions, the more useful are ForAllSuffix2 and ExistsSuffix2 as they allow us to quantify over relations between consecutive elements.

Context
  [A : Type]
  (P : list A -> Prop)
  .

Inductive ExistsSuffix : list A -> Prop :=
| SHere : forall l, P l -> ExistsSuffix l
| SFurther : forall a l, ExistsSuffix l -> ExistsSuffix (a :: l).

Inductive ForAllSuffix : list A -> Prop :=
| SNil : P [] -> ForAllSuffix []
| SHereAndFurther : forall a l, P (a :: l) -> ForAllSuffix l -> ForAllSuffix (a :: l).

Lemma fsHere :
  forall (l : list A),
    ForAllSuffix l -> P l.A: Type
P: list A → Prop
∀ l : list A, ForAllSuffix l → P l
Proof.A: Type
P: list A → Prop
∀ l : list A, ForAllSuffix l → P l by inversion 1. Qed.

Lemma fsFurther :
  forall (a : A) (l : list A),
    ForAllSuffix (a :: l) -> ForAllSuffix l.A: Type
P: list A → Prop
∀ (a : A) (l : list A),
  ForAllSuffix (a :: l) → ForAllSuffix l
Proof.A: Type
P: list A → Prop
∀ (a : A) (l : list A),
  ForAllSuffix (a :: l) → ForAllSuffix l by inversion 1. Qed.

Lemma ForAll_drop :
  forall (m : nat) (l : list A),
    ForAllSuffix l -> ForAllSuffix (drop m l).A: Type
P: list A → Prop
∀ (m : nat) (l : list A),
  ForAllSuffix l → ForAllSuffix (drop m l)
Proof.A: Type
P: list A → Prop
∀ (m : nat) (l : list A),
  ForAllSuffix l → ForAllSuffix (drop m l)
  induction m; intros [] Hall; cbn; [done.. |].A: Type
P: list A → Prop
m: nat
IHm: ∀ l : list A, ForAllSuffix l → ForAllSuffix (drop m l)
a: A
l: list A
Hall: ForAllSuffix (a :: l)
ForAllSuffix (drop m l)
  by apply fsFurther in Hall; apply IHm.
Qed.

Lemma ForAllSuffix_induction :
  forall (Inv : list A -> Prop)
    (InvThenP : forall l, Inv l -> P l)
    (InvIsStable : forall a l, Inv (a :: l) -> Inv l),
  forall l, Inv l -> ForAllSuffix l.A: Type
P: list A → Prop
∀ Inv : list A → Prop,
  (∀ l : list A, Inv l → P l)
  → (∀ (a : A) (l : list A), Inv (a :: l) → Inv l)
    → ∀ l : list A, Inv l → ForAllSuffix l
Proof.A: Type
P: list A → Prop
∀ Inv : list A → Prop,
  (∀ l : list A, Inv l → P l)
  → (∀ (a : A) (l : list A), Inv (a :: l) → Inv l)
    → ∀ l : list A, Inv l → ForAllSuffix l
  induction l; intros.A: Type
P, Inv: list A → Prop
InvThenP: ∀ l : list A, Inv l → P l
InvIsStable: ∀ (a : A) (l : list A),
  Inv (a :: l) → Inv l
H: Inv []
ForAllSuffix []
A: Type
P, Inv: list A → Prop
InvThenP: ∀ l : list A, Inv l → P l
InvIsStable: ∀ (a : A) (l : list A),
  Inv (a :: l) → Inv l
a: A
l: list A
IHl: Inv l → ForAllSuffix l
H: Inv (a :: l)
ForAllSuffix (a :: l)
  -A: Type
P, Inv: list A → Prop
InvThenP: ∀ l : list A, Inv l → P l
InvIsStable: ∀ (a : A) (l : list A),
  Inv (a :: l) → Inv l
H: Inv []
ForAllSuffix [] by constructor; apply InvThenP.
  -A: Type
P, Inv: list A → Prop
InvThenP: ∀ l : list A, Inv l → P l
InvIsStable: ∀ (a : A) (l : list A),
  Inv (a :: l) → Inv l
a: A
l: list A
IHl: Inv l → ForAllSuffix l
H: Inv (a :: l)
ForAllSuffix (a :: l) constructor.A: Type
P, Inv: list A → Prop
InvThenP: ∀ l : list A, Inv l → P l
InvIsStable: ∀ (a : A) (l : list A),
  Inv (a :: l) → Inv l
a: A
l: list A
IHl: Inv l → ForAllSuffix l
H: Inv (a :: l)
P (a :: l)
A: Type
P, Inv: list A → Prop
InvThenP: ∀ l : list A, Inv l → P l
InvIsStable: ∀ (a : A) (l : list A),
  Inv (a :: l) → Inv l
a: A
l: list A
IHl: Inv l → ForAllSuffix l
H: Inv (a :: l)
ForAllSuffix l
    +A: Type
P, Inv: list A → Prop
InvThenP: ∀ l : list A, Inv l → P l
InvIsStable: ∀ (a : A) (l : list A),
  Inv (a :: l) → Inv l
a: A
l: list A
IHl: Inv l → ForAllSuffix l
H: Inv (a :: l)
P (a :: l) by apply InvThenP.
    +A: Type
P, Inv: list A → Prop
InvThenP: ∀ l : list A, Inv l → P l
InvIsStable: ∀ (a : A) (l : list A),
  Inv (a :: l) → Inv l
a: A
l: list A
IHl: Inv l → ForAllSuffix l
H: Inv (a :: l)
ForAllSuffix l by eapply IHl, InvIsStable.
Qed.

End sec_suffix_quantifiers.

Lemma ForAllSuffix_subsumption :
  forall {A : Type} (P Q : list A -> Prop) (HPQ : forall l, P l -> Q l),
    forall (l : list A), ForAllSuffix P l -> ForAllSuffix Q l.∀ (A : Type) (P Q : list A → Prop),
  (∀ l : list A, P l → Q l)
  → ∀ l : list A, ForAllSuffix P l → ForAllSuffix Q l
Proof.∀ (A : Type) (P Q : list A → Prop),
  (∀ l : list A, P l → Q l)
  → ∀ l : list A, ForAllSuffix P l → ForAllSuffix Q l
  by induction 2; constructor; auto.
Qed.

Definition ForAllSuffix2 [A : Type] (R : A -> A -> Prop) : list A -> Prop :=
  ForAllSuffix (fun l => match l with | a :: b :: _ => R a b | _ => True end).

Lemma fsFurther2_transitive :
  forall {A : Type} (R : A -> A -> Prop) {HT : Transitive R} (a b : A) (l : list A),
    ForAllSuffix2 R (a :: b :: l) -> ForAllSuffix2 R (a :: l).∀ (A : Type) (R : A → A → Prop),
  Transitive R
  → ∀ (a b : A) (l : list A),
      ForAllSuffix2 R (a :: b :: l)
      → ForAllSuffix2 R (a :: l)
Proof.∀ (A : Type) (R : A → A → Prop),
  Transitive R
  → ∀ (a b : A) (l : list A),
      ForAllSuffix2 R (a :: b :: l)
      → ForAllSuffix2 R (a :: l)
  inversion 2; subst.A: Type
R: A → A → Prop
HT: Transitive R
a, b: A
l: list A
H: ForAllSuffix2 R (a :: b :: l)
H2: R a b
H3: ForAllSuffix
  (λ l : list A,
     match l with
     | [] => True
     | [a] => True
     | a :: b :: _ => R a b
     end) (b :: l)
ForAllSuffix2 R (a :: l)
  destruct l.A: Type
R: A → A → Prop
HT: Transitive R
a, b: A
H: ForAllSuffix2 R [a; b]
H2: R a b
H3: ForAllSuffix
  (λ l : list A,
     match l with
     | [] => True
     | [a] => True
     | a :: b :: _ => R a b
     end) [b]
ForAllSuffix2 R [a]
A: Type
R: A → A → Prop
HT: Transitive R
a, b, a0: A
l: list A
H: ForAllSuffix2 R (a :: b :: a0 :: l)
H2: R a b
H3: ForAllSuffix
  (λ l : list A,
     match l with
     | [] => True
     | [a] => True
     | a :: b :: _ => R a b
     end) (b :: a0 :: l)
ForAllSuffix2 R (a :: a0 :: l)
  -A: Type
R: A → A → Prop
HT: Transitive R
a, b: A
H: ForAllSuffix2 R [a; b]
H2: R a b
H3: ForAllSuffix
  (λ l : list A,
     match l with
     | [] => True
     | [a] => True
     | a :: b :: _ => R a b
     end) [b]
ForAllSuffix2 R [a] by repeat constructor.
  -A: Type
R: A → A → Prop
HT: Transitive R
a, b, a0: A
l: list A
H: ForAllSuffix2 R (a :: b :: a0 :: l)
H2: R a b
H3: ForAllSuffix
  (λ l : list A,
     match l with
     | [] => True
     | [a] => True
     | a :: b :: _ => R a b
     end) (b :: a0 :: l)
ForAllSuffix2 R (a :: a0 :: l) inversion H3; subst.A: Type
R: A → A → Prop
HT: Transitive R
a, b, a0: A
l: list A
H: ForAllSuffix2 R (a :: b :: a0 :: l)
H2: R a b
H3: ForAllSuffix
  (λ l : list A,
     match l with
     | [] => True
     | [a] => True
     | a :: b :: _ => R a b
     end) (b :: a0 :: l)
H4: R b a0
H5: ForAllSuffix
  (λ l : list A,
     match l with
     | [] => True
     | [a] => True
     | a :: b :: _ => R a b
     end) (a0 :: l)
ForAllSuffix2 R (a :: a0 :: l)
    by constructor; [transitivity b |].
Qed.

Lemma ForAllSuffix2_filter :
  forall {A : Type} (R : A -> A -> Prop) {HT : Transitive R}
    (P : A -> Prop) {Pdec : forall a, Decision (P a)},
  forall l, ForAllSuffix2 R l -> ForAllSuffix2 R (filter P l).∀ (A : Type) (R : A → A → Prop),
  Transitive R
  → ∀ (P : A → Prop) (Pdec : ∀ a : A, Decision (P a)) 
      (l : list A),
      ForAllSuffix2 R l → ForAllSuffix2 R (filter P l)
Proof.∀ (A : Type) (R : A → A → Prop),
  Transitive R
  → ∀ (P : A → Prop) (Pdec : ∀ a : A, Decision (P a)) 
      (l : list A),
      ForAllSuffix2 R l → ForAllSuffix2 R (filter P l)
  induction l; intros Hl; [done |].A: Type
R: A → A → Prop
HT: Transitive R
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a: A
l: list A
IHl: ForAllSuffix2 R l → ForAllSuffix2 R (filter P l)
Hl: ForAllSuffix2 R (a :: l)
ForAllSuffix2 R (filter P (a :: l))
  unfold filter; cbn.A: Type
R: A → A → Prop
HT: Transitive R
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a: A
l: list A
IHl: ForAllSuffix2 R l → ForAllSuffix2 R (filter P l)
Hl: ForAllSuffix2 R (a :: l)
ForAllSuffix2 R
  (if decide (P a)
   then a :: filter P l
   else filter P l)
  spec IHl; [by apply fsFurther in Hl |].A: Type
R: A → A → Prop
HT: Transitive R
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a: A
l: list A
Hl: ForAllSuffix2 R (a :: l)
IHl: ForAllSuffix2 R (filter P l)
ForAllSuffix2 R
  (if decide (P a)
   then a :: filter P l
   else filter P l)
  case_decide; [| done].A: Type
R: A → A → Prop
HT: Transitive R
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a: A
l: list A
Hl: ForAllSuffix2 R (a :: l)
IHl: ForAllSuffix2 R (filter P l)
H: P a
ForAllSuffix2 R (a :: filter P l)
  constructor; [| done].A: Type
R: A → A → Prop
HT: Transitive R
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a: A
l: list A
Hl: ForAllSuffix2 R (a :: l)
IHl: ForAllSuffix2 R (filter P l)
H: P a
match filter P l with
| [] => True
| b :: _ => R a b
end
  clear IHl H; induction l; cbn; [done |].A: Type
R: A → A → Prop
HT: Transitive R
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a, a0: A
l: list A
Hl: ForAllSuffix2 R (a :: a0 :: l)
IHl: ForAllSuffix2 R (a :: l)
→ match filter P l with
  | [] => True
  | b :: _ => R a b
  end
match
  (if decide (P a0)
   then a0 :: filter P l
   else filter P l)
with
| [] => True
| b :: _ => R a b
end
  case_decide.A: Type
R: A → A → Prop
HT: Transitive R
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a, a0: A
l: list A
Hl: ForAllSuffix2 R (a :: a0 :: l)
IHl: ForAllSuffix2 R (a :: l)
→ match filter P l with
  | [] => True
  | b :: _ => R a b
  end
H: P a0
R a a0
A: Type
R: A → A → Prop
HT: Transitive R
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a, a0: A
l: list A
Hl: ForAllSuffix2 R (a :: a0 :: l)
IHl: ForAllSuffix2 R (a :: l)
→ match filter P l with
  | [] => True
  | b :: _ => R a b
  end
H: ¬ P a0
match filter P l with
| [] => True
| b :: _ => R a b
end
  -A: Type
R: A → A → Prop
HT: Transitive R
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a, a0: A
l: list A
Hl: ForAllSuffix2 R (a :: a0 :: l)
IHl: ForAllSuffix2 R (a :: l)
→ match filter P l with
  | [] => True
  | b :: _ => R a b
  end
H: P a0
R a a0 by inversion Hl.
  -A: Type
R: A → A → Prop
HT: Transitive R
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
a, a0: A
l: list A
Hl: ForAllSuffix2 R (a :: a0 :: l)
IHl: ForAllSuffix2 R (a :: l)
→ match filter P l with
  | [] => True
  | b :: _ => R a b
  end
H: ¬ P a0
match filter P l with
| [] => True
| b :: _ => R a b
end by apply IHl; eapply fsFurther2_transitive.
Qed.

Lemma list_subseteq_tran :
  forall (A : Type) (l m n : list A),
    l ⊆ m -> m ⊆ n -> l ⊆ n.∀ (A : Type) (l m n : list A), l ⊆ m → m ⊆ n → l ⊆ n
Proof.∀ (A : Type) (l m n : list A), l ⊆ m → m ⊆ n → l ⊆ n
  intros A l m n Hlm Hmn x y.A: Type
l, m, n: list A
Hlm: l ⊆ m
Hmn: m ⊆ n
x: A
y: x ∈ l
x ∈ n
  by apply Hmn, Hlm.
Qed.

#[export] Instance list_subseteq_dec `{EqDecision A} : RelDecision (@subseteq (list A) _).A: Type
EqDecision0: EqDecision A
RelDecision subseteq
Proof.A: Type
EqDecision0: EqDecision A
RelDecision subseteq
  intros x; induction x.A: Type
EqDecision0: EqDecision A
∀ y : list A, Decision ([] ⊆ y)
A: Type
EqDecision0: EqDecision A
a: A
x: list A
IHx: ∀ y : list A, Decision (x ⊆ y)
∀ y : list A, Decision (a :: x ⊆ y)
  -A: Type
EqDecision0: EqDecision A
∀ y : list A, Decision ([] ⊆ y) by left; apply list_subseteq_nil.
  -A: Type
EqDecision0: EqDecision A
a: A
x: list A
IHx: ∀ y : list A, Decision (x ⊆ y)
∀ y : list A, Decision (a :: x ⊆ y) intros y; destruct (IHx y) as [Hsub | Hnsub].A: Type
EqDecision0: EqDecision A
a: A
x: list A
IHx: ∀ y : list A, Decision (x ⊆ y)
y: list A
Hsub: x ⊆ y
Decision (a :: x ⊆ y)
A: Type
EqDecision0: EqDecision A
a: A
x: list A
IHx: ∀ y : list A, Decision (x ⊆ y)
y: list A
Hnsub: x ⊈ y
Decision (a :: x ⊆ y)
    +A: Type
EqDecision0: EqDecision A
a: A
x: list A
IHx: ∀ y : list A, Decision (x ⊆ y)
y: list A
Hsub: x ⊆ y
Decision (a :: x ⊆ y) destruct (decide (a ∈ y)).A: Type
EqDecision0: EqDecision A
a: A
x: list A
IHx: ∀ y : list A, Decision (x ⊆ y)
y: list A
Hsub: x ⊆ y
e: a ∈ y
Decision (a :: x ⊆ y)
A: Type
EqDecision0: EqDecision A
a: A
x: list A
IHx: ∀ y : list A, Decision (x ⊆ y)
y: list A
Hsub: x ⊆ y
n: a ∉ y
Decision (a :: x ⊆ y)
      *A: Type
EqDecision0: EqDecision A
a: A
x: list A
IHx: ∀ y : list A, Decision (x ⊆ y)
y: list A
Hsub: x ⊆ y
e: a ∈ y
Decision (a :: x ⊆ y) by left; inversion 1; subst; [| apply Hsub].
      *A: Type
EqDecision0: EqDecision A
a: A
x: list A
IHx: ∀ y : list A, Decision (x ⊆ y)
y: list A
Hsub: x ⊆ y
n: a ∉ y
Decision (a :: x ⊆ y) by right; intros Hsub'; contradict n; apply Hsub'; left.
    +A: Type
EqDecision0: EqDecision A
a: A
x: list A
IHx: ∀ y : list A, Decision (x ⊆ y)
y: list A
Hnsub: x ⊈ y
Decision (a :: x ⊆ y) right; intros Hsub; contradict Hnsub.A: Type
EqDecision0: EqDecision A
a: A
x: list A
IHx: ∀ y : list A, Decision (x ⊆ y)
y: list A
Hsub: a :: x ⊆ y
x ⊆ y
      by intros b Hb; apply Hsub; right.
Qed.

Lemma nodup_append_left :
  forall {A : Type} (l1 l2 : list A),
    NoDup (l1 ++ l2) -> NoDup l1.∀ (A : Type) (l1 l2 : list A),
  NoDup (l1 ++ l2) → NoDup l1
Proof.∀ (A : Type) (l1 l2 : list A),
  NoDup (l1 ++ l2) → NoDup l1
  by intros * [? _]%NoDup_app.
Qed.

Lemma NoDup_subseteq_length :
  forall {A : Type} {l1 l2 : list A},
    NoDup l1 -> l1 ⊆ l2 -> length l1 <= length l2.∀ (A : Type) (l1 l2 : list A),
  NoDup l1 → l1 ⊆ l2 → length l1 ≤ length l2
Proof.∀ (A : Type) (l1 l2 : list A),
  NoDup l1 → l1 ⊆ l2 → length l1 ≤ length l2
  by intros; apply submseteq_length, NoDup_submseteq.
Qed.

Lemma submseteq_tail_l :
  forall {A : Type} (x : A) (l1 l2 : list A),
    x :: l1 ⊆+ l2 -> l1 ⊆+ l2.∀ (A : Type) (x : A) (l1 l2 : list A),
  x :: l1 ⊆+ l2 → l1 ⊆+ l2
Proof.∀ (A : Type) (x : A) (l1 l2 : list A),
  x :: l1 ⊆+ l2 → l1 ⊆+ l2
  by intros A x l1 l2; apply submseteq_trans, submseteq_cons.
Qed.

Lemma submseteq_list_subseteq :
  forall {A : Type} (l1 l2 : list A),
    l1 ⊆+ l2 -> l1 ⊆ l2.∀ (A : Type) (l1 l2 : list A), l1 ⊆+ l2 → l1 ⊆ l2
Proof.∀ (A : Type) (l1 l2 : list A), l1 ⊆+ l2 → l1 ⊆ l2
  by intros A l1 l2 H ? Hx; eapply elem_of_submseteq.
Qed.

Lemma take_app_inv :
  forall [A : Type] (n : nat) (l l' : list A) (x : A),
    take n l = l' ++ [x] -> exists n' : nat, n = S n'.∀ (A : Type) (n : nat) (l l' : list A) (x : A),
  take n l = l' ++ [x] → ∃ n' : nat, n = S n'
Proof.∀ (A : Type) (n : nat) (l l' : list A) (x : A),
  take n l = l' ++ [x] → ∃ n' : nat, n = S n'
  induction n as [| n']; intros l l' x H.A: Type
l, l': list A
x: A
H: take 0 l = l' ++ [x]
∃ n' : nat, 0 = S n'
A: Type
n': nat
IHn': ∀ (l l' : list A) (x : A),
  take n' l = l' ++ [x]
  → ∃ n'0 : nat, n' = S n'0
l, l': list A
x: A
H: take (S n') l = l' ++ [x]
∃ n'0 : nat, S n' = S n'0
  -A: Type
l, l': list A
x: A
H: take 0 l = l' ++ [x]
∃ n' : nat, 0 = S n' by rewrite take_0 in H; apply app_cons_not_nil in H.
  -A: Type
n': nat
IHn': ∀ (l l' : list A) (x : A),
  take n' l = l' ++ [x]
  → ∃ n'0 : nat, n' = S n'0
l, l': list A
x: A
H: take (S n') l = l' ++ [x]
∃ n'0 : nat, S n' = S n'0 by exists n'.
Qed.

Lemma elem_of_list_prod :
  forall [A B : Type] (x : A) (y : B) (la : list A) (lb : list B),
    (x, y) ∈ list_prod la lb <-> x ∈ la /\ y ∈ lb.∀ (A B : Type) (x : A) (y : B) (la : list A) (lb : 
                                              list B),
  (x, y) ∈ list_prod la lb ↔ x ∈ la ∧ y ∈ lb
Proof.∀ (A B : Type) (x : A) (y : B) (la : list A) (lb : 
                                              list B),
  (x, y) ∈ list_prod la lb ↔ x ∈ la ∧ y ∈ lb
  by intros; rewrite elem_of_list_In, in_prod_iff, <- !elem_of_list_In.
Qed.

The function lastn and its properties

lastn returns a suffix of length n from the list l.

Definition lastn {A : Type} (n : nat) (l : list A) : list A :=
  rev (take n (rev l)).

If the list is [], then the result of lastn is also [].

Lemma lastn_nil :
  forall {A : Type} (n : nat),
    lastn n (@nil A) = [].∀ (A : Type) (n : nat), lastn n [] = []
Proof.∀ (A : Type) (n : nat), lastn n [] = []
  by intros A n; unfold lastn; cbn; rewrite take_nil.
Qed.

If n is zero, then the result of lastn is [].

Lemma lastn_0 :
  forall {A : Type} (l : list A),
    lastn 0 l = [].∀ (A : Type) (l : list A), lastn 0 l = []
Proof.∀ (A : Type) (l : list A), lastn 0 l = []
  by intros A l; unfold lastn; rewrite take_0.
Qed.

If n is greater than the length of the list, lastn returns the whole list.

Lemma lastn_ge :
  forall {A : Type} (n : nat) (l : list A),
    length l <= n -> lastn n l = l.∀ (A : Type) (n : nat) (l : list A),
  length l ≤ n → lastn n l = l
Proof.∀ (A : Type) (n : nat) (l : list A),
  length l ≤ n → lastn n l = l
  intros A n l Hge.A: Type
n: nat
l: list A
Hge: length l ≤ n
lastn n l = l
  unfold lastn.A: Type
n: nat
l: list A
Hge: length l ≤ n
rev (take n (rev l)) = l
  rewrite take_ge.A: Type
n: nat
l: list A
Hge: length l ≤ n
rev (rev l) = l
A: Type
n: nat
l: list A
Hge: length l ≤ n
length (rev l) ≤ n
  -A: Type
n: nat
l: list A
Hge: length l ≤ n
rev (rev l) = l by rewrite rev_involutive.
  -A: Type
n: nat
l: list A
Hge: length l ≤ n
length (rev l) ≤ n by rewrite rev_length.
Qed.

lastn skips the prefix of the list as long as the suffix is long enough.

Lemma lastn_app_le :
  forall {A : Type} (n : nat) (l1 l2 : list A),
    n <= length l2 -> lastn n (l1 ++ l2) = lastn n l2.∀ (A : Type) (n : nat) (l1 l2 : list A),
  n ≤ length l2 → lastn n (l1 ++ l2) = lastn n l2
Proof.∀ (A : Type) (n : nat) (l1 l2 : list A),
  n ≤ length l2 → lastn n (l1 ++ l2) = lastn n l2
  intros A n l1 l2 Hlt.A: Type
n: nat
l1, l2: list A
Hlt: n ≤ length l2
lastn n (l1 ++ l2) = lastn n l2
  unfold lastn.A: Type
n: nat
l1, l2: list A
Hlt: n ≤ length l2
rev (take n (rev (l1 ++ l2))) = rev (take n (rev l2))
  rewrite rev_app_distr, take_app_le; [done |].A: Type
n: nat
l1, l2: list A
Hlt: n ≤ length l2
n ≤ length (rev l2)
  by rewrite rev_length; lia.
Qed.

lastn either skips the head of the list or not, depending on how big a suffix we want.

Lemma lastn_cons :
  forall {A : Type} (n : nat) (h : A) (t : list A),
    lastn n (h :: t) = if decide (S (length t) <= n) then h :: t else lastn n t.∀ (A : Type) (n : nat) (h : A) (t : list A),
  lastn n (h :: t) =
  (if decide (S (length t) ≤ n)
   then h :: t
   else lastn n t)
Proof.∀ (A : Type) (n : nat) (h : A) (t : list A),
  lastn n (h :: t) =
  (if decide (S (length t) ≤ n)
   then h :: t
   else lastn n t)
  intros A n h t.A: Type
n: nat
h: A
t: list A
lastn n (h :: t) =
(if decide (S (length t) ≤ n)
 then h :: t
 else lastn n t)
  case_decide; subst.A: Type
n: nat
h: A
t: list A
H: S (length t) ≤ n
lastn n (h :: t) = h :: t
A: Type
n: nat
h: A
t: list A
H: ¬ S (length t) ≤ n
lastn n (h :: t) = lastn n t
  -A: Type
n: nat
h: A
t: list A
H: S (length t) ≤ n
lastn n (h :: t) = h :: t by rewrite lastn_ge; cbn; [| lia].
  -A: Type
n: nat
h: A
t: list A
H: ¬ S (length t) ≤ n
lastn n (h :: t) = lastn n t by rewrite (lastn_app_le _ [h] t); [| lia].
Qed.

If l1 is a prefix of l2, then the reverse of l1 is a suffix of l2.

Lemma suffix_rev :
  forall {A : Type} (l1 l2 : list A),
    prefix l1 l2 -> suffix (rev l1) (rev l2).∀ (A : Type) (l1 l2 : list A),
  l1 `prefix_of` l2 → rev l1 `suffix_of` rev l2
Proof.∀ (A : Type) (l1 l2 : list A),
  l1 `prefix_of` l2 → rev l1 `suffix_of` rev l2
  intros A l1 l2 [l ->].A: Type
l1, l: list A
rev l1 `suffix_of` rev (l1 ++ l)
  rewrite rev_app_distr.A: Type
l1, l: list A
rev l1 `suffix_of` rev l ++ rev l1
  by exists (rev l).
Qed.

If n1 is less than (or equal to) n2, then lastn n1 l is shorter than lastn n2 l and therefore is its suffix.

Lemma suffix_lastn :
  forall {A : Type} (l : list A) (n1 n2 : nat),
    n1 <= n2 -> suffix (lastn n1 l) (lastn n2 l).∀ (A : Type) (l : list A) (n1 n2 : nat),
  n1 ≤ n2 → lastn n1 l `suffix_of` lastn n2 l
Proof.∀ (A : Type) (l : list A) (n1 n2 : nat),
  n1 ≤ n2 → lastn n1 l `suffix_of` lastn n2 l
  intros A l n1 n2 Hle.A: Type
l: list A
n1, n2: nat
Hle: n1 ≤ n2
lastn n1 l `suffix_of` lastn n2 l
  unfold lastn.A: Type
l: list A
n1, n2: nat
Hle: n1 ≤ n2
rev (take n1 (rev l))
`suffix_of` rev (take n2 (rev l))
  apply suffix_rev.A: Type
l: list A
n1, n2: nat
Hle: n1 ≤ n2
take n1 (rev l) `prefix_of` take n2 (rev l)
  exists (take (n2 - n1) (drop n1 (rev l))).A: Type
l: list A
n1, n2: nat
Hle: n1 ≤ n2
take n2 (rev l) =
take n1 (rev l) ++ take (n2 - n1) (drop n1 (rev l))
  rewrite take_take_drop.A: Type
l: list A
n1, n2: nat
Hle: n1 ≤ n2
take n2 (rev l) = take (n1 + (n2 - n1)) (rev l)
  by f_equal; lia.
Qed.

The length of lastn n l is the smaller of n and the length of l.

Lemma length_lastn :
  forall {A : Type} (n : nat) (l : list A),
    length (lastn n l) = min n (length l).∀ (A : Type) (n : nat) (l : list A),
  length (lastn n l) = n `min` length l
Proof.∀ (A : Type) (n : nat) (l : list A),
  length (lastn n l) = n `min` length l
  intros A n l.A: Type
n: nat
l: list A
length (lastn n l) = n `min` length l
  unfold lastn.A: Type
n: nat
l: list A
length (rev (take n (rev l))) = n `min` length l
  by rewrite rev_length, take_length, rev_length.
Qed.

Program Definition not_null_element
  `{EqDecision A} [l : list A] (Hl : l <> []) : dsig (fun i => i ∈ l) :=
    dexist (is_Some_proj (proj2 (head_is_Some l) Hl)) _.
Next Obligation.∀ A : Type,
  EqDecision A
  → ∀ (l : list A) (Hl : l ≠ []),
      (λ i : A, i ∈ l)
        (is_Some_proj (proj2 (head_is_Some l) Hl))
Proof.∀ A : Type,
  EqDecision A
  → ∀ (l : list A) (Hl : l ≠ []),
      (λ i : A, i ∈ l)
        (is_Some_proj (proj2 (head_is_Some l) Hl))
  by intros A ? [| h t] ?; [| left].
Qed.

Program Definition element_of_subseteq
  `{EqDecision A} [l1 l2 : list A] (Hsub : l1 ⊆ l2)
  (di : dsig (fun i => i ∈ l1)) : dsig (fun i => i ∈ l2) :=
    dexist (` di) _.
Next Obligation.∀ (A : Type) (EqDecision0 : EqDecision A) (l1
                                           l2 : list A),
  l1 ⊆ l2
  → ∀ di : dsig (λ i : A, i ∈ l1),
      (λ i : A, i ∈ l2) (`di)
Proof.∀ (A : Type) (EqDecision0 : EqDecision A) (l1
                                           l2 : list A),
  l1 ⊆ l2
  → ∀ di : dsig (λ i : A, i ∈ l1),
      (λ i : A, i ∈ l2) (`di)
  by intros; cbn; destruct_dec_sig di i Hi Heq; subst; apply Hsub.
Qed.

Definition element_of_filter
  `{EqDecision A} [P : A -> Prop] `{forall x, Decision (P x)} [l : list A]
  : dsig (fun i => i ∈ filter P l) -> dsig (fun i => i ∈ l) :=
  element_of_subseteq (list_filter_subseteq P l).

Computing longest common prefixes and suffixes

Longest common prefix

Section sec_max_prefix.

Context
  {A : Type}
  `{EqDecision A}
  .

Lemma max_prefix_nil_l :
  forall (l : list A),
    max_prefix [] l = ([], l, []).A: Type
EqDecision0: EqDecision A
∀ l : list A, max_prefix [] l = ([], l, [])
Proof.A: Type
EqDecision0: EqDecision A
∀ l : list A, max_prefix [] l = ([], l, []) done. Qed.

Lemma max_prefix_nil_r :
  forall (l : list A),
    max_prefix l [] = (l, [], []).A: Type
EqDecision0: EqDecision A
∀ l : list A, max_prefix l [] = (l, [], [])
Proof.A: Type
EqDecision0: EqDecision A
∀ l : list A, max_prefix l [] = (l, [], [])
  by destruct l.
Qed.

Lemma max_prefix_diag :
  forall (l : list A),
    max_prefix l l = ([], [], l).A: Type
EqDecision0: EqDecision A
∀ l : list A, max_prefix l l = ([], [], l)
Proof.A: Type
EqDecision0: EqDecision A
∀ l : list A, max_prefix l l = ([], [], l)
  induction l as [| h t]; cbn; [done |].A: Type
EqDecision0: EqDecision A
h: A
t: list A
IHt: max_prefix t t = ([], [], t)
(if decide_rel eq h h
 then prod_map id (cons h) (max_prefix t t)
 else (h :: t, h :: t, [])) = ([], [], h :: t)
  case_decide; [| done].A: Type
EqDecision0: EqDecision A
h: A
t: list A
IHt: max_prefix t t = ([], [], t)
H: h = h
prod_map id (cons h) (max_prefix t t) =
([], [], h :: t)
  by rewrite IHt; cbn.
Qed.

Lemma max_prefix_head :
  forall (l1 l2 : list A),
    head l1 <> head l2 -> max_prefix l1 l2 = (l1, l2, []).A: Type
EqDecision0: EqDecision A
∀ l1 l2 : list A,
  head l1 ≠ head l2 → max_prefix l1 l2 = (l1, l2, [])
Proof.A: Type
EqDecision0: EqDecision A
∀ l1 l2 : list A,
  head l1 ≠ head l2 → max_prefix l1 l2 = (l1, l2, [])
  intros [] [] Hneq; cbn in *; [done.. |].A: Type
EqDecision0: EqDecision A
a: A
l: list A
a0: A
l0: list A
Hneq: Some a ≠ Some a0
(if decide_rel eq a a0
 then prod_map id (cons a) (max_prefix l l0)
 else (a :: l, a0 :: l0, [])) = (a :: l, a0 :: l0, [])
  by case_decide; [congruence |].
Qed.

Lemma max_prefix_app :
  forall (l l1 l2 p r1 r2 : list A),
    max_prefix l1 l2 = (r1, r2, p) ->
      max_prefix (l ++ l1) (l ++ l2) = (r1, r2, l ++ p).A: Type
EqDecision0: EqDecision A
∀ l l1 l2 p r1 r2 : list A,
  max_prefix l1 l2 = (r1, r2, p)
  → max_prefix (l ++ l1) (l ++ l2) = (r1, r2, l ++ p)
Proof.A: Type
EqDecision0: EqDecision A
∀ l l1 l2 p r1 r2 : list A,
  max_prefix l1 l2 = (r1, r2, p)
  → max_prefix (l ++ l1) (l ++ l2) = (r1, r2, l ++ p)
  induction l as [| h t]; cbn; intros * Heq; [done |].A: Type
EqDecision0: EqDecision A
h: A
t: list A
IHt: ∀ l1 l2 p r1 r2 : list A,
  max_prefix l1 l2 = (r1, r2, p)
  → max_prefix (t ++ l1) (t ++ l2) =
    (r1, r2, t ++ p)
l1, l2, p, r1, r2: list A
Heq: max_prefix l1 l2 = (r1, r2, p)
(if decide_rel eq h h
 then
  prod_map id (cons h)
    (max_prefix (t ++ l1) (t ++ l2))
 else (h :: t ++ l1, h :: t ++ l2, [])) =
(r1, r2, h :: t ++ p)
  case_decide; [| done].A: Type
EqDecision0: EqDecision A
h: A
t: list A
IHt: ∀ l1 l2 p r1 r2 : list A,
  max_prefix l1 l2 = (r1, r2, p)
  → max_prefix (t ++ l1) (t ++ l2) =
    (r1, r2, t ++ p)
l1, l2, p, r1, r2: list A
Heq: max_prefix l1 l2 = (r1, r2, p)
H: h = h
prod_map id (cons h) (max_prefix (t ++ l1) (t ++ l2)) =
(r1, r2, h :: t ++ p)
  by apply IHt in Heq as ->; cbn.
Qed.

Lemma max_prefix_app_let :
  forall (l l1 l2 : list A),
    max_prefix (l ++ l1) (l ++ l2) =
      let '(r1, r2, p) := max_prefix l1 l2 in (r1, r2, l ++ p).A: Type
EqDecision0: EqDecision A
∀ l l1 l2 : list A,
  max_prefix (l ++ l1) (l ++ l2) =
  (let
   '(r1, r2, p) := max_prefix l1 l2 in
    (r1, r2, l ++ p))
Proof.A: Type
EqDecision0: EqDecision A
∀ l l1 l2 : list A,
  max_prefix (l ++ l1) (l ++ l2) =
  (let
   '(r1, r2, p) := max_prefix l1 l2 in
    (r1, r2, l ++ p))
  intros.A: Type
EqDecision0: EqDecision A
l, l1, l2: list A
max_prefix (l ++ l1) (l ++ l2) =
(let
 '(r1, r2, p) := max_prefix l1 l2 in (r1, r2, l ++ p))
  destruct (max_prefix l1 l2) as [[]] eqn: Heq.A: Type
EqDecision0: EqDecision A
l, l1, l2, l0, l3, l4: list A
Heq: max_prefix l1 l2 = (l0, l3, l4)
max_prefix (l ++ l1) (l ++ l2) = (l0, l3, l ++ l4)
  by eapply max_prefix_app in Heq.
Qed.

Lemma max_prefix_head_inv :
  forall (l1 l2 p r1 r2 : list A),
    max_prefix l1 l2 = (r1, r2, p) ->
      r1 = [] /\ r2 = [] \/ head r1 <> head r2.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_prefix l1 l2 = (r1, r2, p)
  → r1 = [] ∧ r2 = [] ∨ head r1 ≠ head r2
Proof.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_prefix l1 l2 = (r1, r2, p)
  → r1 = [] ∧ r2 = [] ∨ head r1 ≠ head r2
  intros l1 l2 p [] [] Heq; cbn; [by left | by right.. |].A: Type
EqDecision0: EqDecision A
l1, l2, p: list A
a: A
l: list A
a0: A
l0: list A
Heq: max_prefix l1 l2 = (a :: l, a0 :: l0, p)
a :: l = [] ∧ a0 :: l0 = [] ∨ Some a ≠ Some a0
  apply max_prefix_max_snoc in Heq.A: Type
EqDecision0: EqDecision A
l1, l2, p: list A
a: A
l: list A
a0: A
l0: list A
Heq: a ≠ a0
a :: l = [] ∧ a0 :: l0 = [] ∨ Some a ≠ Some a0
  by right; congruence.
Qed.

Lemma max_prefix_spec :
  forall (l1 l2 p r1 r2 : list A),
    max_prefix l1 l2 = (r1, r2, p)
      <->
    l1 = p ++ r1 /\ l2 = p ++ r2 /\ (r1 = [] /\ r2 = [] \/ head r1 <> head r2).A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_prefix l1 l2 = (r1, r2, p)
  ↔ l1 = p ++ r1
    ∧ l2 = p ++ r2
      ∧ (r1 = [] ∧ r2 = [] ∨ head r1 ≠ head r2)
Proof.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_prefix l1 l2 = (r1, r2, p)
  ↔ l1 = p ++ r1
    ∧ l2 = p ++ r2
      ∧ (r1 = [] ∧ r2 = [] ∨ head r1 ≠ head r2)
  split.A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
max_prefix l1 l2 = (r1, r2, p)
→ l1 = p ++ r1
  ∧ l2 = p ++ r2
    ∧ (r1 = [] ∧ r2 = [] ∨ head r1 ≠ head r2)
A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
l1 = p ++ r1
∧ l2 = p ++ r2
  ∧ (r1 = [] ∧ r2 = [] ∨ head r1 ≠ head r2)
→ max_prefix l1 l2 = (r1, r2, p)
  -A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
max_prefix l1 l2 = (r1, r2, p)
→ l1 = p ++ r1
  ∧ l2 = p ++ r2
    ∧ (r1 = [] ∧ r2 = [] ∨ head r1 ≠ head r2) split; [by eapply max_prefix_fst_alt |].A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
H: max_prefix l1 l2 = (r1, r2, p)
l2 = p ++ r2 ∧ (r1 = [] ∧ r2 = [] ∨ head r1 ≠ head r2)
    split; [by eapply max_prefix_snd_alt |].A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
H: max_prefix l1 l2 = (r1, r2, p)
r1 = [] ∧ r2 = [] ∨ head r1 ≠ head r2
    by eapply max_prefix_head_inv.
  -A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
l1 = p ++ r1
∧ l2 = p ++ r2
  ∧ (r1 = [] ∧ r2 = [] ∨ head r1 ≠ head r2)
→ max_prefix l1 l2 = (r1, r2, p) intros (-> & -> & [[-> ->] |]).A: Type
EqDecision0: EqDecision A
p: list A
max_prefix (p ++ []) (p ++ []) = ([], [], p)
A: Type
EqDecision0: EqDecision A
p, r1, r2: list A
H: head r1 ≠ head r2
max_prefix (p ++ r1) (p ++ r2) = (r1, r2, p)
    +A: Type
EqDecision0: EqDecision A
p: list A
max_prefix (p ++ []) (p ++ []) = ([], [], p) by rewrite app_nil_r, max_prefix_diag.
    +A: Type
EqDecision0: EqDecision A
p, r1, r2: list A
H: head r1 ≠ head r2
max_prefix (p ++ r1) (p ++ r2) = (r1, r2, p) by rewrite max_prefix_app_let, max_prefix_head, app_nil_r.
Qed.

Lemma max_prefix_comm :
  forall (l1 l2 p r1 r2 : list A),
    max_prefix l1 l2 = (r1, r2, p) ->
    max_prefix l2 l1 = (r2, r1, p).A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_prefix l1 l2 = (r1, r2, p)
  → max_prefix l2 l1 = (r2, r1, p)
Proof.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_prefix l1 l2 = (r1, r2, p)
  → max_prefix l2 l1 = (r2, r1, p)
  induction l1 as [| h1 t1]; destruct l2 as [| h2 t2]; cbn; [by itauto congruence.. |].A: Type
EqDecision0: EqDecision A
h1: A
t1: list A
IHt1: ∀ l2 p r1 r2 : list A,
  max_prefix t1 l2 = (r1, r2, p)
  → max_prefix l2 t1 = (r2, r1, p)
h2: A
t2: list A
∀ p r1 r2 : list A,
  (if decide_rel eq h1 h2
   then prod_map id (cons h1) (max_prefix t1 t2)
   else (h1 :: t1, h2 :: t2, [])) = (r1, r2, p)
  → (if decide_rel eq h2 h1
     then prod_map id (cons h2) (max_prefix t2 t1)
     else (h2 :: t2, h1 :: t1, [])) = (r2, r1, p)
  intros p r1 r2.A: Type
EqDecision0: EqDecision A
h1: A
t1: list A
IHt1: ∀ l2 p r1 r2 : list A,
  max_prefix t1 l2 = (r1, r2, p)
  → max_prefix l2 t1 = (r2, r1, p)
h2: A
t2, p, r1, r2: list A
(if decide_rel eq h1 h2
 then prod_map id (cons h1) (max_prefix t1 t2)
 else (h1 :: t1, h2 :: t2, [])) = (r1, r2, p)
→ (if decide_rel eq h2 h1
   then prod_map id (cons h2) (max_prefix t2 t1)
   else (h2 :: t2, h1 :: t1, [])) = (r2, r1, p)
  destruct (max_prefix t1 t2) as [[]] eqn: Heq.A: Type
EqDecision0: EqDecision A
h1: A
t1: list A
IHt1: ∀ l2 p r1 r2 : list A,
  max_prefix t1 l2 = (r1, r2, p)
  → max_prefix l2 t1 = (r2, r1, p)
h2: A
t2, p, r1, r2, l, l0, l1: list A
Heq: max_prefix t1 t2 = (l, l0, l1)
(if decide_rel eq h1 h2
 then prod_map id (cons h1) (l, l0, l1)
 else (h1 :: t1, h2 :: t2, [])) = (r1, r2, p)
→ (if decide_rel eq h2 h1
   then prod_map id (cons h2) (max_prefix t2 t1)
   else (h2 :: t2, h1 :: t1, [])) = (r2, r1, p)
  case_decide; subst; intros [= <- <- <-]; cbn; case_decide; [| done..].A: Type
EqDecision0: EqDecision A
t1: list A
IHt1: ∀ l2 p r1 r2 : list A,
  max_prefix t1 l2 = (r1, r2, p)
  → max_prefix l2 t1 = (r2, r1, p)
h2: A
t2, l, l0, l1: list A
Heq: max_prefix t1 t2 = (l, l0, l1)
H: h2 = h2
prod_map id (cons h2) (max_prefix t2 t1) =
(l0, l, h2 :: l1)
  by erewrite IHt1.
Qed.

Lemma max_prefix_comm_let :
  forall (l1 l2 : list A),
    max_prefix l2 l1 =
      let '(r1, r2, p) := max_prefix l1 l2 in (r2, r1, p).A: Type
EqDecision0: EqDecision A
∀ l1 l2 : list A,
  max_prefix l2 l1 =
  (let '(r1, r2, p) := max_prefix l1 l2 in (r2, r1, p))
Proof.A: Type
EqDecision0: EqDecision A
∀ l1 l2 : list A,
  max_prefix l2 l1 =
  (let '(r1, r2, p) := max_prefix l1 l2 in (r2, r1, p))
  intros.A: Type
EqDecision0: EqDecision A
l1, l2: list A
max_prefix l2 l1 =
(let '(r1, r2, p) := max_prefix l1 l2 in (r2, r1, p))
  destruct (max_prefix l1 l2) as [[]] eqn: Heq.A: Type
EqDecision0: EqDecision A
l1, l2, l, l0, l3: list A
Heq: max_prefix l1 l2 = (l, l0, l3)
max_prefix l2 l1 = (l0, l, l3)
  by apply max_prefix_comm in Heq.
Qed.

Lemma max_prefix_idem :
  forall (l1 l2 p r1 r2 : list A),
    max_prefix l1 l2 = (r1, r2, p) ->
    max_prefix r1 r2 = (r1, r2, []).A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_prefix l1 l2 = (r1, r2, p)
  → max_prefix r1 r2 = (r1, r2, [])
Proof.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_prefix l1 l2 = (r1, r2, p)
  → max_prefix r1 r2 = (r1, r2, [])
  induction l1 as [| h1 t1]; destruct l2 as [| h2 t2]; cbn;
    only 1-3: intros * [= <- <- <-]; cbn; [done.. |].A: Type
EqDecision0: EqDecision A
h1: A
t1: list A
IHt1: ∀ l2 p r1 r2 : list A,
  max_prefix t1 l2 = (r1, r2, p)
  → max_prefix r1 r2 = (r1, r2, [])
h2: A
t2: list A
∀ p r1 r2 : list A,
  (if decide_rel eq h1 h2
   then prod_map id (cons h1) (max_prefix t1 t2)
   else (h1 :: t1, h2 :: t2, [])) = (r1, r2, p)
  → max_prefix r1 r2 = (r1, r2, [])
  intros p r1 r2.A: Type
EqDecision0: EqDecision A
h1: A
t1: list A
IHt1: ∀ l2 p r1 r2 : list A,
  max_prefix t1 l2 = (r1, r2, p)
  → max_prefix r1 r2 = (r1, r2, [])
h2: A
t2, p, r1, r2: list A
(if decide_rel eq h1 h2
 then prod_map id (cons h1) (max_prefix t1 t2)
 else (h1 :: t1, h2 :: t2, [])) = (r1, r2, p)
→ max_prefix r1 r2 = (r1, r2, [])
  destruct (max_prefix t1 t2) as [[]] eqn: Heq.A: Type
EqDecision0: EqDecision A
h1: A
t1: list A
IHt1: ∀ l2 p r1 r2 : list A,
  max_prefix t1 l2 = (r1, r2, p)
  → max_prefix r1 r2 = (r1, r2, [])
h2: A
t2, p, r1, r2, l, l0, l1: list A
Heq: max_prefix t1 t2 = (l, l0, l1)
(if decide_rel eq h1 h2
 then prod_map id (cons h1) (l, l0, l1)
 else (h1 :: t1, h2 :: t2, [])) = (r1, r2, p)
→ max_prefix r1 r2 = (r1, r2, [])
  case_decide; subst; intros [= <- <- <-]; cbn.A: Type
EqDecision0: EqDecision A
t1: list A
IHt1: ∀ l2 p r1 r2 : list A,
  max_prefix t1 l2 = (r1, r2, p)
  → max_prefix r1 r2 = (r1, r2, [])
h2: A
t2, l, l0, l1: list A
Heq: max_prefix t1 t2 = (l, l0, l1)
max_prefix l l0 = (l, l0, [])
A: Type
EqDecision0: EqDecision A
h1: A
t1: list A
IHt1: ∀ l2 p r1 r2 : list A,
  max_prefix t1 l2 = (r1, r2, p)
  → max_prefix r1 r2 = (r1, r2, [])
h2: A
t2, l, l0, l1: list A
Heq: max_prefix t1 t2 = (l, l0, l1)
H: h1 ≠ h2
(if decide_rel eq h1 h2
 then prod_map id (cons h1) (max_prefix t1 t2)
 else (h1 :: t1, h2 :: t2, [])) =
(h1 :: t1, h2 :: t2, [])
  -A: Type
EqDecision0: EqDecision A
t1: list A
IHt1: ∀ l2 p r1 r2 : list A,
  max_prefix t1 l2 = (r1, r2, p)
  → max_prefix r1 r2 = (r1, r2, [])
h2: A
t2, l, l0, l1: list A
Heq: max_prefix t1 t2 = (l, l0, l1)
max_prefix l l0 = (l, l0, []) by apply IHt1 in Heq.
  -A: Type
EqDecision0: EqDecision A
h1: A
t1: list A
IHt1: ∀ l2 p r1 r2 : list A,
  max_prefix t1 l2 = (r1, r2, p)
  → max_prefix r1 r2 = (r1, r2, [])
h2: A
t2, l, l0, l1: list A
Heq: max_prefix t1 t2 = (l, l0, l1)
H: h1 ≠ h2
(if decide_rel eq h1 h2
 then prod_map id (cons h1) (max_prefix t1 t2)
 else (h1 :: t1, h2 :: t2, [])) =
(h1 :: t1, h2 :: t2, []) by case_decide.
Qed.

Lemma max_prefix_is_longest :
  forall (l1 l2 p r1 r2 p' : list A),
   max_prefix l1 l2 = (r1, r2, p) ->
   prefix p' l1 -> prefix p' l2 ->
   length p' <= length p.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 p' : list A,
  max_prefix l1 l2 = (r1, r2, p)
  → p' `prefix_of` l1
    → p' `prefix_of` l2 → length p' ≤ length p
Proof.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 p' : list A,
  max_prefix l1 l2 = (r1, r2, p)
  → p' `prefix_of` l1
    → p' `prefix_of` l2 → length p' ≤ length p
  intros l1 l2 p r1 r2 p' Hlc Hp1 Hp2.A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2, p': list A
Hlc: max_prefix l1 l2 = (r1, r2, p)
Hp1: p' `prefix_of` l1
Hp2: p' `prefix_of` l2
length p' ≤ length p
  inversion Hlc; subst; apply prefix_length.A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2, p': list A
Hlc: max_prefix l1 l2 = (r1, r2, p)
Hp1: p' `prefix_of` l1
Hp2: p' `prefix_of` l2
H0: max_prefix l1 l2 = (r1, r2, p)
p' `prefix_of` p
  by eapply max_prefix_max_alt.
Qed.

Lemma max_prefix_residual_suffix :
  forall (l1 l2 p r1 r2 : list A),
    max_prefix l1 l2 = (r1, r2, p) ->
      suffix r1 l1 /\ suffix r2 l2.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_prefix l1 l2 = (r1, r2, p)
  → r1 `suffix_of` l1 ∧ r2 `suffix_of` l2
Proof.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_prefix l1 l2 = (r1, r2, p)
  → r1 `suffix_of` l1 ∧ r2 `suffix_of` l2
  intros * Hprefix.A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
Hprefix: max_prefix l1 l2 = (r1, r2, p)
r1 `suffix_of` l1 ∧ r2 `suffix_of` l2
  apply max_prefix_spec in Hprefix as (-> & -> & _).A: Type
EqDecision0: EqDecision A
p, r1, r2: list A
r1 `suffix_of` p ++ r1 ∧ r2 `suffix_of` p ++ r2
  by split; apply suffix_app_r.
Qed.

End sec_max_prefix.

Longest common suffix

Section sec_max_suffix.

Context
  {A : Type}
  `{EqDecision A}
  .

Lemma max_suffix_diag :
  forall (l : list A),
    max_suffix l l = ([], [], l).A: Type
EqDecision0: EqDecision A
∀ l : list A, max_suffix l l = ([], [], l)
Proof.A: Type
EqDecision0: EqDecision A
∀ l : list A, max_suffix l l = ([], [], l)
  intros.A: Type
EqDecision0: EqDecision A
l: list A
max_suffix l l = ([], [], l)
  unfold max_suffix.A: Type
EqDecision0: EqDecision A
l: list A
(let (p, k3) := max_prefix (reverse l) (reverse l) in
 let (k1, k2) := p in
 (reverse k1, reverse k2, reverse k3)) = ([], [], l)
  by rewrite max_prefix_diag, reverse_involutive; cbn.
Qed.

Lemma max_suffix_app_let :
  forall (l l1 l2 : list A),
    max_suffix (l1 ++ l) (l2 ++ l) =
      let '(r1, r2, p) := max_suffix l1 l2 in (r1, r2, p ++ l).A: Type
EqDecision0: EqDecision A
∀ l l1 l2 : list A,
  max_suffix (l1 ++ l) (l2 ++ l) =
  (let
   '(r1, r2, p) := max_suffix l1 l2 in
    (r1, r2, p ++ l))
Proof.A: Type
EqDecision0: EqDecision A
∀ l l1 l2 : list A,
  max_suffix (l1 ++ l) (l2 ++ l) =
  (let
   '(r1, r2, p) := max_suffix l1 l2 in
    (r1, r2, p ++ l))
  intros.A: Type
EqDecision0: EqDecision A
l, l1, l2: list A
max_suffix (l1 ++ l) (l2 ++ l) =
(let
 '(r1, r2, p) := max_suffix l1 l2 in (r1, r2, p ++ l))
  unfold max_suffix.A: Type
EqDecision0: EqDecision A
l, l1, l2: list A
(let (p, k3) :=
   max_prefix (reverse (l1 ++ l)) (reverse (l2 ++ l)) in
 let (k1, k2) := p in
 (reverse k1, reverse k2, reverse k3)) =
(let
 '(r1, r2, p) :=
  let (p, k3) :=
    max_prefix (reverse l1) (reverse l2) in
  let (k1, k2) := p in
  (reverse k1, reverse k2, reverse k3) in
  (r1, r2, p ++ l))
  rewrite !reverse_app, max_prefix_app_let.A: Type
EqDecision0: EqDecision A
l, l1, l2: list A
(let (p, k3) :=
   let
   '(r1, r2, p) :=
    max_prefix (reverse l1) (reverse l2) in
    (r1, r2, reverse l ++ p) in
 let (k1, k2) := p in
 (reverse k1, reverse k2, reverse k3)) =
(let
 '(r1, r2, p) :=
  let (p, k3) :=
    max_prefix (reverse l1) (reverse l2) in
  let (k1, k2) := p in
  (reverse k1, reverse k2, reverse k3) in
  (r1, r2, p ++ l))
  destruct (max_prefix (reverse l1) (reverse l2)) as [[]] eqn: Heq.A: Type
EqDecision0: EqDecision A
l, l1, l2, l0, l3, l4: list A
Heq: max_prefix (reverse l1) (reverse l2) =
(l0, l3, l4)
(reverse l0, reverse l3, reverse (reverse l ++ l4)) =
(reverse l0, reverse l3, reverse l4 ++ l)
  by rewrite reverse_app, reverse_involutive.
Qed.

Lemma max_suffix_last :
  forall (l1 l2 : list A),
    last l1 <> last l2 -> max_suffix l1 l2 = (l1, l2, []).A: Type
EqDecision0: EqDecision A
∀ l1 l2 : list A,
  last l1 ≠ last l2 → max_suffix l1 l2 = (l1, l2, [])
Proof.A: Type
EqDecision0: EqDecision A
∀ l1 l2 : list A,
  last l1 ≠ last l2 → max_suffix l1 l2 = (l1, l2, [])
  intros * Hlast.A: Type
EqDecision0: EqDecision A
l1, l2: list A
Hlast: last l1 ≠ last l2
max_suffix l1 l2 = (l1, l2, [])
  unfold max_suffix.A: Type
EqDecision0: EqDecision A
l1, l2: list A
Hlast: last l1 ≠ last l2
(let (p, k3) :=
   max_prefix (reverse l1) (reverse l2) in
 let (k1, k2) := p in
 (reverse k1, reverse k2, reverse k3)) = (l1, l2, [])
  rewrite max_prefix_head.A: Type
EqDecision0: EqDecision A
l1, l2: list A
Hlast: last l1 ≠ last l2
(reverse (reverse l1), reverse (reverse l2),
 reverse []) = (l1, l2, [])
A: Type
EqDecision0: EqDecision A
l1, l2: list A
Hlast: last l1 ≠ last l2
head (reverse l1) ≠ head (reverse l2)
  -A: Type
EqDecision0: EqDecision A
l1, l2: list A
Hlast: last l1 ≠ last l2
(reverse (reverse l1), reverse (reverse l2),
 reverse []) = (l1, l2, []) by rewrite !reverse_involutive; cbn.
  -A: Type
EqDecision0: EqDecision A
l1, l2: list A
Hlast: last l1 ≠ last l2
head (reverse l1) ≠ head (reverse l2) by rewrite !head_reverse.
Qed.

Lemma max_suffix_last_inv :
  forall (l1 l2 p r1 r2 : list A),
    max_suffix l1 l2 = (r1, r2, p) ->
      r1 = [] /\ r2 = [] \/ last r1 <> last r2.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_suffix l1 l2 = (r1, r2, p)
  → r1 = [] ∧ r2 = [] ∨ last r1 ≠ last r2
Proof.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_suffix l1 l2 = (r1, r2, p)
  → r1 = [] ∧ r2 = [] ∨ last r1 ≠ last r2
  intros * Heq.A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
Heq: max_suffix l1 l2 = (r1, r2, p)
r1 = [] ∧ r2 = [] ∨ last r1 ≠ last r2
  destruct_list_last r1 r1' h1 Heq1; destruct_list_last r2 r2' h2 Heq2; cbn;
    rewrite ?last_snoc; [by left | by right.. |].A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2, r1': list A
h1: A
r2': list A
h2: A
Heq: max_suffix l1 l2 = (r1' ++ [h1], r2' ++ [h2], p)
Heq1: r1 = r1' ++ [h1]
Heq2: r2 = r2' ++ [h2]
r1' ++ [h1] = [] ∧ r2' ++ [h2] = []
∨ Some h1 ≠ Some h2
  right; intros [= ->].A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2, r1', r2': list A
h2: A
Heq1: r1 = r1' ++ [h2]
Heq: max_suffix l1 l2 = (r1' ++ [h2], r2' ++ [h2], p)
Heq2: r2 = r2' ++ [h2]
False
  by apply max_suffix_max_snoc in Heq.
Qed.

Lemma max_suffix_spec :
  forall (l1 l2 p r1 r2 : list A),
    max_suffix l1 l2 = (r1, r2, p)
      <->
    l1 = r1 ++ p /\ l2 = r2 ++ p /\ (r1 = [] /\ r2 = [] \/ last r1 <> last r2).A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_suffix l1 l2 = (r1, r2, p)
  ↔ l1 = r1 ++ p
    ∧ l2 = r2 ++ p
      ∧ (r1 = [] ∧ r2 = [] ∨ last r1 ≠ last r2)
Proof.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_suffix l1 l2 = (r1, r2, p)
  ↔ l1 = r1 ++ p
    ∧ l2 = r2 ++ p
      ∧ (r1 = [] ∧ r2 = [] ∨ last r1 ≠ last r2)
  split.A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
max_suffix l1 l2 = (r1, r2, p)
→ l1 = r1 ++ p
  ∧ l2 = r2 ++ p
    ∧ (r1 = [] ∧ r2 = [] ∨ last r1 ≠ last r2)
A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
l1 = r1 ++ p
∧ l2 = r2 ++ p
  ∧ (r1 = [] ∧ r2 = [] ∨ last r1 ≠ last r2)
→ max_suffix l1 l2 = (r1, r2, p)
  -A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
max_suffix l1 l2 = (r1, r2, p)
→ l1 = r1 ++ p
  ∧ l2 = r2 ++ p
    ∧ (r1 = [] ∧ r2 = [] ∨ last r1 ≠ last r2) split; [by eapply max_suffix_fst_alt |].A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
H: max_suffix l1 l2 = (r1, r2, p)
l2 = r2 ++ p ∧ (r1 = [] ∧ r2 = [] ∨ last r1 ≠ last r2)
    split; [by eapply max_suffix_snd_alt |].A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
H: max_suffix l1 l2 = (r1, r2, p)
r1 = [] ∧ r2 = [] ∨ last r1 ≠ last r2
    by eapply max_suffix_last_inv.
  -A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
l1 = r1 ++ p
∧ l2 = r2 ++ p
  ∧ (r1 = [] ∧ r2 = [] ∨ last r1 ≠ last r2)
→ max_suffix l1 l2 = (r1, r2, p) intros (-> & -> & [[-> ->] |]); cbn.A: Type
EqDecision0: EqDecision A
p: list A
max_suffix p p = ([], [], p)
A: Type
EqDecision0: EqDecision A
p, r1, r2: list A
H: last r1 ≠ last r2
max_suffix (r1 ++ p) (r2 ++ p) = (r1, r2, p)
    +A: Type
EqDecision0: EqDecision A
p: list A
max_suffix p p = ([], [], p) by rewrite max_suffix_diag.
    +A: Type
EqDecision0: EqDecision A
p, r1, r2: list A
H: last r1 ≠ last r2
max_suffix (r1 ++ p) (r2 ++ p) = (r1, r2, p) by rewrite max_suffix_app_let, max_suffix_last.
Qed.

Lemma max_suffix_comm_let :
  forall (l1 l2 : list A),
    max_suffix l2 l1 =
      let '(r1, r2, p) := max_suffix l1 l2 in (r2, r1, p).A: Type
EqDecision0: EqDecision A
∀ l1 l2 : list A,
  max_suffix l2 l1 =
  (let '(r1, r2, p) := max_suffix l1 l2 in (r2, r1, p))
Proof.A: Type
EqDecision0: EqDecision A
∀ l1 l2 : list A,
  max_suffix l2 l1 =
  (let '(r1, r2, p) := max_suffix l1 l2 in (r2, r1, p))
  intros.A: Type
EqDecision0: EqDecision A
l1, l2: list A
max_suffix l2 l1 =
(let '(r1, r2, p) := max_suffix l1 l2 in (r2, r1, p))
  unfold max_suffix.A: Type
EqDecision0: EqDecision A
l1, l2: list A
(let (p, k3) :=
   max_prefix (reverse l2) (reverse l1) in
 let (k1, k2) := p in
 (reverse k1, reverse k2, reverse k3)) =
(let
 '(r1, r2, p) :=
  let (p, k3) :=
    max_prefix (reverse l1) (reverse l2) in
  let (k1, k2) := p in
  (reverse k1, reverse k2, reverse k3) in (r2, r1, p))
  rewrite max_prefix_comm_let.A: Type
EqDecision0: EqDecision A
l1, l2: list A
(let (p, k3) :=
   let
   '(r1, r2, p) :=
    max_prefix (reverse l1) (reverse l2) in
    (r2, r1, p) in
 let (k1, k2) := p in
 (reverse k1, reverse k2, reverse k3)) =
(let
 '(r1, r2, p) :=
  let (p, k3) :=
    max_prefix (reverse l1) (reverse l2) in
  let (k1, k2) := p in
  (reverse k1, reverse k2, reverse k3) in (r2, r1, p))
  by destruct (max_prefix (reverse l1) (reverse l2)) as [[]].
Qed.

Lemma max_suffix_is_suffix :
  forall (l1 l2 p r1 r2 : list A),
    max_suffix l1 l2 = (r1, r2, p) ->
      suffix p l1 /\ suffix p l2.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_suffix l1 l2 = (r1, r2, p)
  → p `suffix_of` l1 ∧ p `suffix_of` l2
Proof.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_suffix l1 l2 = (r1, r2, p)
  → p `suffix_of` l1 ∧ p `suffix_of` l2
  intros * Hsuffix.A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
Hsuffix: max_suffix l1 l2 = (r1, r2, p)
p `suffix_of` l1 ∧ p `suffix_of` l2
  apply max_suffix_spec in Hsuffix as (-> & -> & _).A: Type
EqDecision0: EqDecision A
p, r1, r2: list A
p `suffix_of` r1 ++ p ∧ p `suffix_of` r2 ++ p
  by split; apply suffix_app_r.
Qed.

Lemma suffix_max_suffix :
  forall (l l1 l2 : list A),
    suffix l l1 -> suffix l l2 ->
      let '(r1, r2, p) := max_suffix l1 l2 in suffix l p.A: Type
EqDecision0: EqDecision A
∀ l l1 l2 : list A,
  l `suffix_of` l1
  → l `suffix_of` l2
    → let
      '(_, _, p) := max_suffix l1 l2 in
       l `suffix_of` p
Proof.A: Type
EqDecision0: EqDecision A
∀ l l1 l2 : list A,
  l `suffix_of` l1
  → l `suffix_of` l2
    → let
      '(_, _, p) := max_suffix l1 l2 in
       l `suffix_of` p
  intros.A: Type
EqDecision0: EqDecision A
l, l1, l2: list A
H: l `suffix_of` l1
H0: l `suffix_of` l2
let '(_, _, p) := max_suffix l1 l2 in l `suffix_of` p
  destruct (max_suffix l1 l2) as [[]] eqn: Heq.A: Type
EqDecision0: EqDecision A
l, l1, l2: list A
H: l `suffix_of` l1
H0: l `suffix_of` l2
l0, l3, l4: list A
Heq: max_suffix l1 l2 = (l0, l3, l4)
l `suffix_of` l4
  by eapply max_suffix_max_alt.
Qed.

Lemma max_suffix_is_longest :
  forall (l1 l2 p r1 r2 p' : list A),
   max_suffix l1 l2 = (r1, r2, p) ->
   suffix p' l1 -> suffix p' l2 ->
   length p' <= length p.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 p' : list A,
  max_suffix l1 l2 = (r1, r2, p)
  → p' `suffix_of` l1
    → p' `suffix_of` l2 → length p' ≤ length p
Proof.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 p' : list A,
  max_suffix l1 l2 = (r1, r2, p)
  → p' `suffix_of` l1
    → p' `suffix_of` l2 → length p' ≤ length p
  intros l1 l2 p r1 r2 p' Hlc Hp1 Hp2.A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2, p': list A
Hlc: max_suffix l1 l2 = (r1, r2, p)
Hp1: p' `suffix_of` l1
Hp2: p' `suffix_of` l2
length p' ≤ length p
  inversion Hlc; subst; apply suffix_length.A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2, p': list A
Hlc: max_suffix l1 l2 = (r1, r2, p)
Hp1: p' `suffix_of` l1
Hp2: p' `suffix_of` l2
H0: max_suffix l1 l2 = (r1, r2, p)
p' `suffix_of` p
  by eapply max_suffix_max_alt.
Qed.

Lemma max_suffix_residual_prefix :
  forall (l1 l2 p r1 r2 : list A),
    max_suffix l1 l2 = (r1, r2, p) ->
      prefix r1 l1 /\ prefix r2 l2.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_suffix l1 l2 = (r1, r2, p)
  → r1 `prefix_of` l1 ∧ r2 `prefix_of` l2
Proof.A: Type
EqDecision0: EqDecision A
∀ l1 l2 p r1 r2 : list A,
  max_suffix l1 l2 = (r1, r2, p)
  → r1 `prefix_of` l1 ∧ r2 `prefix_of` l2
  intros * Hsuffix.A: Type
EqDecision0: EqDecision A
l1, l2, p, r1, r2: list A
Hsuffix: max_suffix l1 l2 = (r1, r2, p)
r1 `prefix_of` l1 ∧ r2 `prefix_of` l2
  apply max_suffix_spec in Hsuffix as (-> & -> & _).A: Type
EqDecision0: EqDecision A
p, r1, r2: list A
r1 `prefix_of` r1 ++ p ∧ r2 `prefix_of` r2 ++ p
  by split; apply prefix_app_r.
Qed.

End sec_max_suffix.

Program Fixpoint Exists_choose_first
  `{P : A -> Prop} `{forall a, Decision (P a)} {l : list A} (Hl : Exists P l) {struct l} : A :=
  match l with
  | [] => _
  | a :: l => if decide (P a) then a else @Exists_choose_first A P _ l _
  end.
Next Obligation.∀ (A : Type) (P : A → Prop),
  (∀ a : A, Decision (P a))
  → ∀ l : list A, Exists P l → [] = l → A
Proof.∀ (A : Type) (P : A → Prop),
  (∀ a : A, Decision (P a))
  → ∀ l : list A, Exists P l → [] = l → A by intros; exfalso; subst; inversion Hl. Qed.
Next Obligation.∀ (A : Type) (P : A → Prop),
  (∀ a : A, Decision (P a))
  → ∀ l0 : list A,
      Exists P l0
      → ∀ (a : A) (l : list A),
          a :: l = l0 → ¬ P a → Exists P l
Proof.∀ (A : Type) (P : A → Prop),
  (∀ a : A, Decision (P a))
  → ∀ l0 : list A,
      Exists P l0
      → ∀ (a : A) (l : list A),
          a :: l = l0 → ¬ P a → Exists P l by intros; subst; apply Exists_cons in Hl as []. Qed.

Lemma Exists_choose_first_good :
  forall `(P : A -> Prop) `{forall a, Decision (P a)} (l : list A) (Hl : Exists P l),
    P (Exists_choose_first Hl).∀ (A : Type) (P : A → Prop) (H : ∀ a : A,
                                   Decision (P a)) 
  (l : list A) (Hl : Exists P l),
  P (Exists_choose_first Hl)
Proof.∀ (A : Type) (P : A → Prop) (H : ∀ a : A,
                                   Decision (P a)) 
  (l : list A) (Hl : Exists P l),
  P (Exists_choose_first Hl)
  induction l; cbn; intros; [by inversion Hl |].A: Type
P: A → Prop
H: ∀ a : A, Decision (P a)
a: A
l: list A
IHl: ∀ Hl : Exists P l, P (Exists_choose_first Hl)
Hl: Exists P (a :: l)
P
  match decide (P a) with
  | left _ => a
  | right x =>
      Exists_choose_first
        (Exists_choose_first_obligation_2 A P (a :: l)
           Hl a l eq_refl x)
  end
  by case_decide; [| apply IHl].
Qed.