Library prosa.util.list

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
Require Export mathcomp.zify.zify.

Require Import prosa.util.tactics.
Require Export prosa.util.supremum.

Maximum, First, and Last Element of Empty Lists

We define a few simple operations on lists that return zero for empty lists: max0, first0, and last0.
Definition max0 := foldl maxn 0.
Definition first0 := head 0.
Definition last0 := last 0.

Lemmas about last0.

Let xs be a non-empty sequence and x be an arbitrary element, then we prove that last0 (x::xs) = last0 xs.
Lemma last0_cons :
  ∀ x xs,
    xs ≠ [::] →
    last0 (x::xs) = last0 xs.
Proof. by move⇒ x; elim. Qed.

Similarly, let xs_r be a non-empty sequence and xs_l be any sequence, we prove that last0 (xs_l ++ xs_r) = last0 xs_r.
Lemma last0_cat :
  ∀ xs_l xs_r,
    xs_r ≠ [::] →
    last0 (xs_l ++ xs_r) = last0 xs_r.
Proof.
  elim⇒ [//|xs xs_l IHxs_l] n NEQ.
  simpl; rewrite last0_cons.
  - by apply IHxs_l.
  - by intros C; apply: NEQ; destruct xs_l.
Qed.

We also prove that last0 xs = xs [| size xs -1 |] .
Lemma last0_nth :
  ∀ xs,
    last0 xs = nth 0 xs (size xs).-1.
Proof. by intros; rewrite nth_last. Qed.

We prove that for any non-empty sequence xs there is a sequence xsh such that xsh ++ [::last0 x] = [xs].
Lemma last0_ex_cat :
  ∀ x xs,
    xs ≠ [::] →
    last0 xs = x →
    ∃ xsh, xsh ++ [::x] = xs.
Proof.
  move⇒ x; elim⇒ [//|a xs IHxs] NEQ LAST.
  destruct xs.
  - by ∃ [::]; move: LAST; rewrite /last0 /= ⇒ →.
  - feed_n 2 IHxs; try by done.
    destruct IHxs as [xsh EQ].
    by ∃ (a::xsh); rewrite //= EQ.
Qed.

We prove that if x is the last element of a sequence xs and x satisfies a predicate, then x remains the last element in the filtered sequence.
Lemma last0_filter :
  ∀ x xs (P : nat → bool),
    xs ≠ [::] →
    last0 xs = x →
    P x →
    last0 [seq x <- xs | P x] = x.
Proof.
  clear; intros x xs P NEQ LAST PX.
  destruct (last0_ex_cat x xs NEQ LAST) as [xsh EQ]; subst xs.
  rewrite filter_cat last0_cat.
  all:rewrite //= PX //=.
Qed.

Lemmas about max0.

First we prove that max0 (x::xs) is equal to max {x, max0 xs}.
Lemma max0_cons : ∀ x xs, max0 (x :: xs) = maxn x (max0 xs).
Proof. by move⇒ x xs; rewrite /max0 !foldlE /= !big_cons maxnCA. Qed.

Next, we prove that if all the numbers of a seq xs are equal to a constant k, then max0 xs = k.
Lemma max0_of_uniform_set :
  ∀ k xs,
    size xs > 0 →
    (∀ x, x \in xs → x = k) →
    max0 xs = k.
Proof.
  move⇒ k; elim⇒ [//|a xs IHxs] SIZE ALL.
  destruct xs as [|b xs].
  - rewrite /max0 //= max0n; apply ALL.
    by rewrite in_cons; apply/orP; left.
  - rewrite max0_cons IHxs; [ | by done | ].
    + by rewrite [a]ALL; [ rewrite maxnn | rewrite in_cons; apply/orP; left].
    + move⇒ x H; apply ALL.
      rewrite in_cons; move: H ⇒ /orP [/eqP EQ | IN].
      × by subst x; rewrite !in_cons; apply/orP; right; apply/orP; left.
      × by rewrite !in_cons; apply/orP; right; apply/orP; right.
Qed.

We prove that no element in a sequence xs is greater than max0 xs.
Lemma in_max0_le :
  ∀ xs x, x \in xs → x ≤ max0 xs.
Proof.
  elim⇒ [//|a xs IHxs] x.
  rewrite in_cons ⇒ /orP [/eqP EQ | IN]; subst.
  - by rewrite !max0_cons leq_maxl.
  - apply leq_trans with (max0 xs); first by eauto.
    by rewrite max0_cons; apply leq_maxr.
Qed.

We prove that for a non-empty sequence xs, max0 xs ∈ xs.
Lemma max0_in_seq :
  ∀ xs,
    xs ≠ [::] →
    max0 xs \in xs.
Proof.
  elim⇒ [//|a xs IHxs] _.
  destruct xs as [|n xs].
  - destruct a; simpl; first by done.
    by rewrite /max0 //= max0n in_cons eq_refl.
  - rewrite max0_cons.
    move: (leq_total a (max0 (n::xs))) ⇒ /orP [LE|LE].
    + by rewrite maxnE subnKC // in_cons; apply/orP; right; apply IHxs.
    + rewrite maxnE; move: LE; rewrite -subn_eq0 ⇒ /eqP EQ.
      by rewrite EQ addn0 in_cons; apply/orP; left.
Qed.

We prove a technical lemma stating that one can remove duplicating element from the head of a sequence.
Lemma max0_2cons_eq :
  ∀ x xs,
    max0 (x::x::xs) = max0 (x::xs).
Proof. by intros; rewrite !max0_cons maxnA maxnn. Qed.

Similarly, we prove that one can remove the first element of a sequence if it is not greater than the second element of this sequence.
Lemma max0_2cons_le :
  ∀ x1 x2 xs,
    x1 ≤ x2 →
    max0 (x1::x2::xs) = max0 (x2::xs).
Proof.
  by move⇒ x1 x2 ? ?; rewrite !max0_cons maxnA [maxn x1 x2]maxnE subnKC.
Qed.

We prove that max0 of a sequence xs is equal to max0 of sequence xs without 0s.
Lemma max0_rem0 :
  ∀ xs,
    max0 ([seq x <- xs | 0 < x]) = max0 xs.
Proof.
  elim⇒ [//|a xs IHxs].
  simpl; destruct a; simpl.
  - by rewrite max0_cons max0n.
  - by rewrite !max0_cons IHxs.
Qed.

Note that the last element is at most the max element.
Lemma last_of_seq_le_max_of_seq :
  ∀ xs, last0 xs ≤ max0 xs.
Proof.
  intros xs.
  have EX: ∃ len, size xs ≤ len.
  { by ∃ (size xs). }
  move: EX ⇒ [len LE].
  generalize dependent xs; elim: len ⇒ [|n IHlen] xs LE.
  - by intros; move: LE; rewrite leqn0 size_eq0 ⇒ /eqP EQ; subst.
  - move: LE; rewrite leq_eqVlt ⇒ /orP [/eqP EQ| LE]; last by apply IHlen.
    destruct xs as [ | x1 xs]; first by inversion EQ.
    destruct xs as [ | x2 xs]; first by rewrite /max leq_max; apply/orP; right.
    have ->: last0 [:: x1, x2 & xs] = last0 [:: x2 & xs] by done.
    rewrite max0_cons leq_max; apply/orP; right; apply IHlen.
    move: EQ ⇒ /eqP; simpl; rewrite eqSS ⇒ /eqP EQ.
    by subst.
Qed.

If any element of a sequence xs is less-than-or-equal-to the corresponding element of a sequence ys, then max0 of xs is less-than-or-equal-to max of ys.
Lemma max_of_dominating_seq :
  ∀ xs ys,
    (∀ n, (nth 0 xs n) ≤ (nth 0 ys n)) →
    max0 xs ≤ max0 ys.
Proof.
  intros xs ys.
  have EX: ∃ len, size xs ≤ len ∧ size ys ≤ len.
  { ∃ (maxn (size xs) (size ys)).
    by split; rewrite leq_max; apply/orP; [left | right].
  }
  move: EX ⇒ [len [LE1 LE2]].
  generalize dependent xs; generalize dependent ys.
  elim: len ⇒ [ | len IHlen] xs LE1 ys LE2.
  { by move: LE1 LE2; rewrite !leqn0 !size_eq0 ⇒ /eqP E1 /eqP E2; subst. }
  { move: xs ys LE1 LE2 ⇒ [ |x xs] [//|y ys] LE1 LE2 H.
    { have L: ∀ xs, (∀ n, (nth 0 xs n) = 0) → max0 xs = 0.
      { clear; elim⇒ [//|x xs IHxs] H.
        rewrite max0_cons.
        apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.
        rewrite geq_max; apply/andP; split.
        - by specialize (H 0); simpl in H; rewrite H.
        - rewrite leqn0; apply/eqP; apply: IHxs.
          by move⇒ n; specialize (H n.+1); simpl in H.
      }
      rewrite L; first by done.
      move⇒ n0; specialize (H n0).
      by destruct n0; simpl in *; apply/eqP; rewrite -leqn0.
    }
    { rewrite !max0_cons geq_max; apply/andP; split.
      + rewrite leq_max; apply/orP; left.
        by specialize (H 0); simpl in H.
      + rewrite leq_max; apply/orP; right.
        apply IHlen; try (by rewrite ltnS in LE1, LE2).
        by move⇒ n1; specialize (H n1.+1); simpl in H.
    }
  }
Qed.

Additional Lemmas about rem

We prove that if x lies in xs excluding y, then x also lies in xs.
Lemma rem_in :
  ∀ {X : eqType} (x y : X) (xs : seq X),
    x \in rem y xs → x \in xs.
Proof.
  move⇒ X x y; elim⇒ [|a xs IHxs] /= H.
  { by rewrite in_nil in H. }
  { rewrite in_cons; apply/orP.
    destruct (a == y) eqn:EQ.
    { by move: EQ ⇒ /eqP EQ; subst a; right. }
    { move: H; rewrite in_cons ⇒ /orP [/eqP H | H].
      - by subst a; left.
      - by right; apply IHxs.
    }
  }
Qed.

Similarly, we prove that if x ≠ y and x lies in xs, then x lies in xs excluding y.
Lemma in_neq_impl_rem_in :
  ∀ {X : eqType} (x y : X) (xs : seq X),
    x \in xs →
    x != y →
    x \in rem y xs.
Proof.
  move⇒ X x y; elim⇒ [//|a xs IHxs].
  rewrite in_cons ⇒ /orP [/eqP EQ | IN]; intros NEQ.
  { rewrite -EQ //=.
    move: NEQ; rewrite -eqbF_neg ⇒ /eqP →.
    by rewrite in_cons; apply/orP; left.
  }
  { simpl; destruct (a == y) eqn:AD; first by done.
    rewrite in_cons; apply/orP; right.
    by apply IHxs.
  }
Qed.

We prove that if we remove an element x for which P x from a filter, then the size of the filter decreases by 1.
Lemma filter_size_rem :
  ∀ {X : eqType} (x : X) (xs : seq X) (P : pred X),
    (x \in xs) →
    P x →
    size [seq y <- xs | P y] = size [seq y <- rem x xs | P y] + 1.
Proof.
  move⇒ X x + P + H0; elim⇒ [|a xs IHxs] H; first by inversion H.
  move: H; rewrite in_cons ⇒ /orP [/eqP H | H]; subst.
  { by simpl; rewrite H0 -[X in X = _]addn1 eq_refl. }
  { specialize (IHxs H); simpl in ×.
    case EQab: (a == x); simpl.
    { move: EQab ⇒ /eqP EQab; subst.
      by rewrite H0 addn1. }
    { case Pa: (P a); simpl.
      - by rewrite IHxs !addn1.
      - by rewrite IHxs.
    }
  }
Qed.

Misc. Additional Lemmas about Sequences

First, we show that a sequence xs contains the same elements as a sequence undup xs.
Lemma in_seq_equiv_undup :
  ∀ {X : eqType} (xs : seq X) (x : X),
    (x \in undup xs) = (x \in xs).
Proof.
  move⇒ X xs; induction xs as [ | x0 xs IHxs]; first by done.
  move⇒ x; rewrite in_cons //=; case IN: (x0 \in xs).
  - case EQ: (x == x0).
    + by move: EQ ⇒ /eqP EQ; subst; rewrite orTb IHxs.
    + by rewrite orFb; apply IHxs.
  - by rewrite in_cons IHxs.
Qed.

We show that if n > 0, then nth (x::xs) n = nth xs (n-1).
Lemma nth0_cons :
  ∀ x xs n,
    n > 0 →
    nth 0 (x :: xs) n = nth 0 xs n.-1.
Proof. by move⇒ ? ? []. Qed.

Equality of singleton lists is identical to equality of option types.
Lemma seq1_some {T : eqType} :
  ∀ (x y : T),
    ([:: x] == [:: y]) = (Some x == Some y).
Proof.
  move⇒ x y.
  case: (eqVneq x y) ⇒ [-> //=|/eqP NEQ]; first by rewrite !eq_refl.
  apply/eqP; rewrite ifF.
  - by move⇒ []EQ; apply: NEQ.
  - by apply/negbTE/eqP ⇒ -[].
Qed.

We prove that a sequence xs of size n.+1 can be destructed into a sequence xs_l of size n and an element x such that x = xs ++ [::x].
Lemma seq_elim_last :
  ∀ {X : Type} (n : nat) (xs : seq X),
    size xs = n.+1 →
    ∃ x xs__c, xs = xs__c ++ [:: x] ∧ size xs__c = n.
Proof.
  intros X n xs SIZE.
  elim: n xs SIZE ⇒ [|n IHn] xs SIZE.
  - destruct xs as [|x xs]; first by done.
    destruct xs; last by done.
    by ∃ x, [::]; split.
  - destruct xs as [|x xs]; first by done.
    specialize (IHn xs).
    feed IHn; first by simpl in SIZE; apply eq_add_S in SIZE.
    destruct IHn as [x__n [xs__n [EQ__n SIZE__n]]]; subst xs.
    ∃ x__n, (x :: xs__n); split; first by done.
    simpl in SIZE; apply eq_add_S in SIZE.
    rewrite size_cat //= in SIZE; rewrite addn1 in SIZE; apply eq_add_S in SIZE.
    by apply eq_S.
Qed.

Next, we prove that x ∈ xs implies that xs can be split into two parts such that xs = xsl ++ [::x] ++ [xsr].
Lemma in_cat :
  ∀ {X : eqType} (x : X) (xs : list X),
    x \in xs → ∃ xsl xsr, xs = xsl ++ [::x] ++ xsr.
Proof.
  move⇒ X x; elim⇒ [//|a xs IHxs] SUB.
  move: SUB; rewrite in_cons ⇒ /orP [/eqP EQ|IN].
  - by subst; ∃ [::], xs.
  - feed IHxs; first by done.
    clear IN; move: IHxs ⇒ [xsl [xsr EQ]].
    by subst; ∃ (a::xsl), xsr.
Qed.

We prove that for any two sequences xs and ys the fact that xs is a sub-sequence of ys implies that the size of xs is at most the size of ys.
Lemma subseq_leq_size :
  ∀ {X : eqType} (xs ys : seq X),
    uniq xs →
    (∀ x, x \in xs → x \in ys) →
    size xs ≤ size ys.
Proof.
  intros X xs ys UNIQ SUB.
  have EXm: ∃ m, size ys ≤ m; first by ∃ (size ys).
  move: EXm ⇒ [m SIZEm].
  move: xs ys SIZEm UNIQ SUB.
  elim: m ⇒ [|m IHm] xs ys SIZEm UNIQ SUB.
  { move: SIZEm; rewrite leqn0 size_eq0 ⇒ /eqP SIZEm; subst ys.
    destruct xs as [|s xs]; first by done.
    specialize (SUB s).
    by feed SUB; [rewrite in_cons; apply/orP; left | done].
  }
  { destruct xs as [ | x xs]; first by done.
    move: (@in_cat _ x ys) ⇒ Lem.
    feed Lem; first by apply SUB; rewrite in_cons; apply/orP; left.
    move: Lem ⇒ [ysl [ysr EQ]]; subst ys.
    rewrite !size_cat //= -addnC add1n addSn ltnS -size_cat; eapply IHm.
    - move: SIZEm; rewrite !size_cat //= ⇒ SIZE.
      by rewrite add1n addnS ltnS addnC in SIZE.
    - by move: UNIQ; rewrite cons_uniq ⇒ /andP [_ UNIQ].
    - intros a IN.
      destruct (a == x) eqn: EQ.
      { exfalso.
        move: EQ UNIQ; rewrite cons_uniq ⇒ /eqP EQ /andP [NIN UNIQ].
        by subst; move: NIN ⇒ /negP NIN; apply: NIN.
      }
      { specialize (SUB a).
        feed SUB; first by rewrite in_cons; apply/orP; right.
        clear IN; move: SUB; rewrite !mem_cat ⇒ /orP [IN| /orP [IN|IN]].
        - by apply/orP; right.
        - by exfalso; move: IN; rewrite in_cons ⇒ /orP [IN|IN]; [rewrite IN in EQ | ].
        - by apply/orP; left.
      }
  }
Qed.

Given two sequences xs and ys, two elements x and y, and an index idx such that nth xs idx = x, nth ys idx = y, we show that the pair (x, y) is in zip xs ys.
Lemma in_zip :
  ∀ {X Y : eqType} (xs : seq X) (ys : seq Y) (x x__d : X) (y y__d : Y),
    size xs = size ys →
    (∃ idx, idx < size xs ∧ nth x__d xs idx = x ∧ nth y__d ys idx = y) →
    (x, y) \in zip xs ys.
Proof.
  move⇒ X Y xs ys x x__d y y__d.
  elim: xs ys ⇒ [|x1 xs IHxs] ys EQ [idx [LT [NTHx NTHy]]] //.
  destruct ys as [ | y1 ys]; first by done.
  rewrite //= in_cons; apply/orP.
  destruct idx as [ | idx]; [left | right].
  { by simpl in NTHx, NTHy; subst. }
  { simpl in NTHx, NTHy, LT.
    eapply IHxs.
    - by apply eq_add_S.
    - by ∃ idx; repeat split; eauto.
  }
Qed.

We prove that if no element of a sequence xs satisfies a predicate P, then filter P xs is equal to an empty sequence.
Lemma filter_in_pred0 :
  ∀ {X : eqType} (xs : seq X) (P : pred X),
    (∀ x, x \in xs → ~~ P x) →
    filter P xs = [::].
Proof.
  move⇒ X xs P; elim: xs ⇒ [//|a xs IHxs] ALLF.
  rewrite //= IHxs; last first.
  + by intros; apply ALLF; rewrite in_cons; apply/orP; right.
  + destruct (P a) eqn:EQ; last by done.
    move: EQ ⇒ /eqP; rewrite eqb_id -[P a]Bool.negb_involutive ⇒ /negP T.
    exfalso; apply: T.
    by apply ALLF; apply/orP; left.
Qed.

We show that any two elements having the same index in a sequence must be equal.
Lemma eq_ind_in_seq :
  ∀ {X : eqType} (a b : X) (xs : seq X),
    index a xs = index b xs →
    a \in xs →
    b \in xs →
    a = b.
Proof.
  move⇒ X a b xs EQ IN_a IN_b.
  move: (nth_index a IN_a) ⇒ EQ_a.
  move: (nth_index a IN_b) ⇒ EQ_b.
  by rewrite -EQ_a -EQ_b EQ.
Qed.

We show that the nth element in a sequence is either in the sequence or is the default element.
Lemma default_or_in :
  ∀ {X : eqType} (n : nat) (d : X) (xs : seq X),
    nth d xs n = d ∨ nth d xs n \in xs.
Proof.
  move⇒ x n d xs; destruct (leqP (size xs) n).
  - by left; apply nth_default.
  - by right; apply mem_nth.
Qed.

We show that in a unique sequence of size greater than one there exist two unique elements.
Lemma exists_two :
  ∀ {X : eqType} (xs : seq X),
    size xs > 1 →
    uniq xs →
    ∃ a b, a ≠ b ∧ a \in xs ∧ b \in xs.
Proof.
  move⇒ T xs GT1 UNIQ.
  (* get an element of T so that we can use nth *)
  have HEAD: ∃ x, ohead xs = Some x by elim: xs GT1 UNIQ ⇒ // a l _ _ _; ∃ a ⇒ //.
  move: (HEAD) ⇒ [x0 _].
  have GT0 : 0 < size xs by exact: ltn_trans GT1.
  ∃ (nth x0 xs 0).
  ∃ (nth x0 xs 1).
  repeat split; try apply mem_nth ⇒ //.
  apply /eqP; apply contraNneq with (b := (0 == 1)) ⇒ // /eqP.
  by rewrite nth_uniq.
Qed.

The predicate all implies the predicate has, if the sequence is not empty.
Lemma has_all_nilp {T : eqType} :
  ∀ (s : seq T) (P : pred T),
    all P s →
    ~~ nilp s →
    has P s.
Proof.
  case ⇒ // a s P /allP ALL _.
  by apply /hasP; ∃ a; [|move: (ALL a); apply]; exact: mem_head.
Qed.

Additional Lemmas about sorted

We show that if [x | x ∈ xs : P x] is sorted with respect to values of some function f, then it can be split into two parts: [x | x ∈ xs : P x ∧ f x ≤ t] and [x | x ∈ xs : P x ∧ f x ≤ t].
Lemma sorted_split :
  ∀ {X : eqType} (xs : seq X) P f t,
    sorted (fun x y ⇒ f x ≤ f y) xs →
    [seq x <- xs | P x] = [seq x <- xs | P x & f x ≤ t] ++ [seq x <- xs | P x & f x > t].
Proof.
  clear; move⇒ X xs P f t; elim: xs ⇒ [//|a xs IHxs] /= SORT.
  have TR : transitive (T:=X) (fun x y : X ⇒ f x ≤ f y).
  { intros ? ? ? LE1 LE2; lia. }
  destruct (P a) eqn:Pa, (leqP (f a) t) as [R1 | R1]; simpl.
  { erewrite IHxs; first by reflexivity.
    by eapply path_sorted; eauto. }
  { erewrite IHxs; last by eapply path_sorted; eauto.
    replace ([seq x <- xs | P x & f x ≤ t]) with (@nil X); first by done.
    symmetry; move: SORT; rewrite path_sortedE // ⇒ /andP [ALL SORT].
    apply filter_in_pred0; intros ? IN; apply/negP; intros H; move: H ⇒ /andP [Px LEx].
    by move: ALL ⇒ /allP ALL; specialize (ALL _ IN); simpl in ALL; lia.
  }
  { by eapply IHxs, path_sorted; eauto. }
  { by eapply IHxs, path_sorted; eauto. }
Qed.

We show that if a sequence xs1 ++ xs2 is sorted, then both subsequences xs1 and xs2 are sorted as well.
Lemma sorted_cat :
  ∀ {X : eqType} {R : rel X} (xs1 xs2 : seq X),
    transitive R →
    sorted R (xs1 ++ xs2) → sorted R xs1 ∧ sorted R xs2.
Proof.
  move⇒ X R; elim⇒ [//|a xs1 IHxs1] xs2 TR SORT; split.
  { move: SORT; rewrite /= path_sortedE// all_cat ⇒ /andP[/andP[ALL1 ALL2] SORT].
    rewrite path_sortedE//; apply/andP; split⇒ //.
    exact: (proj1 (IHxs1 _ _ SORT)).
  }
  { simpl in *; move: SORT; rewrite //= path_sortedE // all_cat ⇒ /andP [/andP [ALL1 ALL2] SORT].
    by apply IHxs1.
  }
Qed.

Additional Lemmas about last

First, we show that the default element does not change the value of last for non-empty sequences.
Lemma nonnil_last :
  ∀ {X : eqType} (xs : seq X) (d1 d2 : X),
    xs != [::] →
    last d1 xs = last d2 xs.
Proof. by move⇒ X xs d1 d2; elim: xs ⇒ [//|a xs IHxs] _. Qed.

We show that if a sequence xs contains an element that satisfies a predicate P, then the last element of filter P xs is in xs.
Lemma filter_last_mem :
  ∀ {X : eqType} (xs : seq X) (d : X) (P : pred X),
    has P xs →
    last d (filter P xs) \in xs.
Proof.
  move⇒ X; elim⇒ [//|a xs IHxs] d P /hasP [x + Px].
  rewrite in_cons ⇒ /orP [/eqP EQ | IN].
  { simpl; subst a; rewrite Px; simpl.
    destruct (has P xs) eqn:HAS.
    { by rewrite in_cons; apply/orP; right; apply IHxs. }
    { replace (filter _ _) with (@nil X).
      - by simpl; rewrite in_cons; apply/orP; left.
      - symmetry; apply filter_in_pred0; intros y IN.
        by move: HAS ⇒ /negP/negP/hasPn ALLN; apply: ALLN.
    }
  }
  { rewrite in_cons; apply/orP; right.
    simpl; destruct (P a); simpl; apply IHxs.
    all: by apply/hasP; ∃ x.
  }
Qed.

Removing all Instances of a Given Value from a List

Function rem from ssreflect removes only the first occurrence of an element in a sequence. We define function rem_all which removes all occurrences of an element in a sequence.
Fixpoint rem_all {X : eqType} (x : X) (xs : seq X) :=
  match xs with
  | [::] ⇒ [::]
  | a :: xs ⇒
    if a == x then rem_all x xs else a :: rem_all x xs
  end.

First we prove that x ∉ rem_all x xs.
Lemma nin_rem_all :
  ∀ {X : eqType} (x : X) (xs : seq X),
    ¬ (x \in rem_all x xs).
Proof.
  move⇒ X x; elim⇒ [//|a xs IHxs] IN.
  apply: IHxs.
  simpl in IN; destruct (a == x) eqn:EQ; first by done.
  move: IN; rewrite in_cons ⇒ /orP [/eqP EQ2 | IN]; last by done.
  by subst; exfalso; rewrite eq_refl in EQ.
Qed.

Next we show that rem_all x xs ⊆ xs.
Lemma in_rem_all :
  ∀ {X : eqType} (a x : X) (xs : seq X),
    a \in rem_all x xs → a \in xs.
Proof.
  intros X a x; elim⇒ [//|a0 xs IHxs] /= IN.
  destruct (a0 == x) eqn:EQ.
  - by rewrite in_cons; apply/orP; right; eauto.
  - move: IN; rewrite in_cons ⇒ /orP [EQ2|IN].
    + by rewrite in_cons; apply/orP; left.
    + by rewrite in_cons; apply/orP; right; auto.
Qed.

If an element x is smaller than any element of a sequence xs, then rem_all x xs = xs.
Lemma rem_lt_id :
  ∀ x xs,
    (∀ y, y \in xs → x < y) →
    rem_all x xs = xs.
Proof.
  move⇒ x; elim⇒ [//|a xs IHxs] MIN /=.
  have → : (a == x) = false.
  { apply/eqP/eqP; rewrite neq_ltn; apply/orP; right.
    by apply MIN; rewrite in_cons; apply/orP; left.
  }
  rewrite IHxs //.
  intros; apply: MIN.
  by rewrite in_cons; apply/orP; right.
Qed.

Range of Indices

To have a more intuitive naming, we introduce the definition of range a b which is equal to index_iota a b.+1.
Definition range (a b : nat) := index_iota a b.+1.

In the following, we establish some lemmas about index_iota and range for lists.
First, we show that iota m n can be split into two parts iota m nle and iota (m + nle) (n - nle) for any nle ≤ n.
Lemma iotaD_impl :
  ∀ n_le m n,
    n_le ≤ n →
    iota m n = iota m n_le ++ iota (m + n_le) (n - n_le).
Proof.
  move⇒ n_le m n LE.
  interval_to_duration n_le n k.
  by rewrite iotaD; replace (_ + _ - _) with k; last lia.
Qed.

Next, we prove that index_iota a b = a :: index_iota a.+1 b for a < b.
Remark index_iota_lt_step :
  ∀ a b,
    a < b →
    index_iota a b = a :: index_iota a.+1 b.
Proof.
  move⇒ a b LT; unfold index_iota.
  destruct b; first by done.
  rewrite ltnS in LT.
  by rewrite subSn //.
Qed.

Splitting index_iota t1 t2 at t yields two concatenated iotas.
Lemma index_iota_cat :
  ∀ t t1 t2,
    t1 ≤ t ≤ t2 →
    index_iota t1 t2 = index_iota t1 t ++ index_iota t t2.
Proof.
  move⇒ t t1 t2 NEQ; rewrite /index_iota (iotaD_impl (t - t1)); last by lia.
  by f_equal; f_equal; lia.
Qed.

We prove that one can remove duplicating element from the head of a sequence by which range is filtered.
Lemma range_filter_2cons :
  ∀ x xs k,
    [seq ρ <- range 0 k | ρ \in x :: x :: xs]
    = [seq ρ <- range 0 k | ρ \in x :: xs].
Proof.
  move⇒ x xs k; apply: eq_filter ⇒ x0.
  by rewrite !in_cons; destruct (x0 == x), (x0 \in xs).
Qed.

Consider a, b, and x s.t. a ≤ x < b, then filter of iota_index a b with predicate (_ == x) yields ::x.
Lemma index_iota_filter_eqx :
  ∀ x a b,
    a ≤ x < b →
    [seq ρ <- index_iota a b | ρ == x] = [::x].
Proof.
  move⇒ x a b.
  have EX : ∃ k, b - a ≤ k.
  { ∃ (b-a); by simpl. }
  destruct EX as [k BO].
  revert x a b BO; elim: k ⇒ [|k IHk] ⇒ x a b BO /andP [GE LT].
  { by exfalso; move: BO; rewrite leqn0 subn_eq0 ⇒ BO; lia. }
  { destruct a as [|a].
    { destruct b; first by done.
      rewrite index_iota_lt_step //; simpl.
      destruct (0 == x) eqn:EQ.
      - move: EQ ⇒ /eqP EQ; subst x.
        rewrite filter_in_pred0 //.
        by intros x; rewrite mem_index_iota -lt0n ⇒ /andP [T1 _].
      - by apply IHk; lia.
    }
    rewrite index_iota_lt_step; last by lia.
    simpl; destruct (a.+1 == x) eqn:EQ.
    - move: EQ ⇒ /eqP EQ; subst x.
      rewrite filter_in_pred0 //.
      intros x; rewrite mem_index_iota ⇒ /andP [T1 _].
      by rewrite neq_ltn; apply/orP; right.
    - by rewrite IHk //; lia.
  }
Qed.

As a corollary we prove that filter of iota_index a b with predicate (_ ∈ [::x]) yields ::x.
Corollary index_iota_filter_singl :
  ∀ x a b,
    a ≤ x < b →
    [seq ρ <- index_iota a b | ρ \in [:: x]] = [::x].
Proof.
  move⇒ x a b NEQ.
  rewrite -{2}(index_iota_filter_eqx _ a b) //.
  apply eq_filter; intros ?.
  by repeat rewrite in_cons; rewrite in_nil Bool.orb_false_r.
Qed.

Next we prove that if an element x is not in a sequence xs, then iota_index a b filtered with predicate (_ ∈ xs) is equal to iota_index a b filtered with predicate (_ ∈ rem_all x xs).
Lemma index_iota_filter_inxs :
  ∀ a b x xs,
    x < a →
    [seq ρ <- index_iota a b | ρ \in xs]
    = [seq ρ <- index_iota a b | ρ \in rem_all x xs].
Proof.
  intros a b x xs LT.
  apply eq_in_filter.
  intros y; rewrite mem_index_iota ⇒ /andP [LE GT].
  elim: xs ⇒ [//|y' xs IHxs].
  rewrite in_cons IHxs; simpl; clear IHxs.
  destruct (y == y') eqn:EQ1, (y' == x) eqn:EQ2; auto.
  - by exfalso; move: EQ1 EQ2 ⇒ /eqP EQ1 /eqP EQ2; subst; lia.
  - by move: EQ1 ⇒ /eqP EQ1; subst; rewrite in_cons eq_refl.
  - by rewrite in_cons EQ1.
Qed.

We prove that if an element x is a min of a sequence xs, then iota_index a b filtered with predicate (_ ∈ x::xs) is equal to x :: iota_index a b filtered with predicate (_ ∈ rem_all x xs).
Lemma index_iota_filter_step :
  ∀ x xs a b,
    a ≤ x < b →
    (∀ y, y \in xs → x ≤ y) →
    [seq ρ <- index_iota a b | ρ \in x :: xs]
    = x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs].
Proof.
  intros x xs a b B MIN.
  have EX : ∃ k, b - a ≤ k.
  { ∃ (b-a); by simpl. } destruct EX as [k BO].
  revert x xs a b B MIN BO.
  elim: k ⇒ [ |k IHk] x xs a b /andP [LE GT] MIN BO.
  - by move_neq_down BO; lia.
  - move: LE; rewrite leq_eqVlt ⇒ /orP [/eqP EQ|LT].
    + subst.
      rewrite index_iota_lt_step //.
      replace ([seq ρ <- x :: index_iota x.+1 b | ρ \in x :: xs])
        with (x :: [seq ρ <- index_iota x.+1 b | ρ \in x :: xs]); last first.
      { by rewrite /= in_cons eqxx.
      }
      rewrite (index_iota_filter_inxs _ _ x) //; simpl.
      rewrite eq_refl.
      replace (@in_mem nat x (@mem nat (seq_predType _) (@rem_all _ x xs))) with false; first by reflexivity.
      apply/eqP; rewrite eq_sym eqbF_neg.
      apply/negP; apply nin_rem_all.
    + rewrite index_iota_lt_step //; last by lia.
      replace ([seq ρ <- a :: index_iota a.+1 b | ρ \in x :: xs])
        with ([seq ρ <- index_iota a.+1 b | ρ \in x :: xs]); last first.
      { simpl; replace (@in_mem nat a (@mem nat (seq_predType _) (@cons nat x xs))) with false; first by done.
        apply/eqP; rewrite eq_sym eqbF_neg.
        apply/negP; rewrite in_cons; intros C; move: C ⇒ /orP [/eqP C|C].
        - by subst; rewrite ltnn in LT.
        - by move_neq_down LT; apply MIN.
      }
      replace ([seq ρ <- a :: index_iota a.+1 b | ρ \in rem_all x xs])
        with ([seq ρ <- index_iota a.+1 b | ρ \in rem_all x xs]); last first.
      { simpl; replace (@in_mem nat a (@mem nat (seq_predType _) (@rem_all _ x xs))) with false; first by done.
        apply/eqP; rewrite eq_sym eqbF_neg; apply/negP; intros C.
        apply in_rem_all in C.
        by move_neq_down LT; apply MIN.
      }
      by rewrite IHk //; lia.
Qed.

For convenience, we define a special case of lemma index_iota_filter_step for a = 0 and b = k.+1.
Corollary range_iota_filter_step :
  ∀ x xs k,
    x ≤ k →
    (∀ y, y \in xs → x ≤ y) →
    [seq ρ <- range 0 k | ρ \in x :: xs]
    = x :: [seq ρ <- range 0 k | ρ \in rem_all x xs].
Proof.
  intros x xs k LE MIN.
    by apply index_iota_filter_step; auto.
Qed.

We prove that if x < a, then x < (filter P (index_iota a b))[idx] for any predicate P.
Lemma iota_filter_gt :
  ∀ x a b idx P,
    x < a →
    idx < size ([seq x <- index_iota a b | P x]) →
    x < nth 0 [seq x <- index_iota a b | P x] idx.
Proof.
  clear⇒ x a b idx P.
  have EX : ∃ k, b - a ≤ k.
  { ∃ (b-a); by simpl. } destruct EX as [k BO].
  revert x a b idx P BO; elim: k ⇒ [|k IHk].
  - move ⇒ x a b idx P BO LT1 LT2.
    move: BO; rewrite leqn0 ⇒ /eqP BO.
      by rewrite /index_iota BO in LT2; simpl in LT2.
  - move ⇒ x a b idx P BO LT1 LT2.
    case: (leqP b a) ⇒ [N|N].
    + move: N; rewrite -subn_eq0 ⇒ /eqP EQ.
        by rewrite /index_iota EQ //= in LT2.
    + rewrite index_iota_lt_step; last by done.
      simpl in *; destruct (P a) eqn:PA.
      × destruct idx; simpl; first by done.
        apply IHk; try lia.
          by rewrite index_iota_lt_step // //= PA //= in LT2.
      × apply IHk; try lia.
          by rewrite index_iota_lt_step // //= PA //= in LT2.
Qed.

Additional Lemmas about count

If f implies g for all elements in xs, then the number of elements in xs satisfying f is less than or equal to the number of elements satisfying g.
Lemma sub_count_seq :
  ∀ {X : eqType} (f g : pred X) (xs : seq X),
    {in xs, ∀ x, f x → g x} →
    count f xs ≤ count g xs.
Proof.
  move⇒ X f g xs LE; rewrite -!size_filter -!sum1_size !big_filter.
  rewrite big_seq_cond [leqRHS]big_seq_cond big_mkcond [leqRHS]big_mkcond.
  apply leq_sum ⇒ t _; destruct (_ \in _) eqn:IN, (f t) eqn:FT, (g t) eqn:GT ⇒ //.
  by move: (LE _ IN); rewrite FT GT ⇒ FA.
Qed.

We adapt ssreflect’s count_predUI lemma for easier rewriting: the count of elements satisfying P1 ∪ P2 equals the sum of counts for P1 and P2, minus the count of elements satisfying both.
Lemma count_predUI' :
  ∀ (P1 P2 : pred nat) (xs : seq nat),
    count (predU P1 P2) xs = count P1 xs + count P2 xs - count (predI P1 P2) xs.
Proof.
  by move⇒ P1 P2 xs; rewrite -(count_predUI P1 P2 xs) -addnBA // subnn addn0.
Qed.

Prefix Definitions

A sequence xs is a prefix of another sequence ys iff there exists a sequence xs_tail such that ys is a concatenation of xs and xs_tail.
Definition prefix_of {T : eqType} (xs ys : seq T) := ∃ xs_tail, xs ++ xs_tail = ys.

Furthermore, every prefix of a sequence is said to be strict if it is not equal to the sequence itself.
Definition strict_prefix_of {T : eqType} (xs ys : seq T) :=
  ∃ xs_tail, xs_tail ≠ [::] ∧ xs ++ xs_tail = ys.

Shifting Sequences of Natural Numbers

We define a helper function that shifts a sequence of numbers "forward" by a constant offset, and an analogous version that shifts them "backwards," removing any number that, in the absence of Coq' s saturating subtraction, would become negative. These functions are useful in transforming abstract RTA's search space.
Definition shift_points_pos (xs : seq nat) (s : nat) : seq nat :=
  map (addn s) xs.
Definition shift_points_neg (xs : seq nat) (s : nat) : seq nat :=
  let nonsmall := filter (fun x ⇒ x ≥ s) xs in
  map (fun x ⇒ x - s) nonsmall.