Library rt.util.list

Require Import rt.util.tactics.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

(* Lemmas about lists without duplicates. *)
Section UniqList.

  Lemma idx_lt_rcons :
     {T: eqType} (l: seq T) i x0,
      uniq l
      i < size l
      [seq x <- l | index x l < i.+1] =
        rcons [seq x <- l | index x l < i] (nth x0 l i).
  Proof.
    intros T l i x0 UNIQ LT.
    generalize dependent i.
    induction l as [| l' x] using last_ind; first by ins; rewrite ltn0 in LT.
    {
      intros i LT.
      rewrite size_rcons in LT.
      rewrite filter_rcons.
      rewrite -cats1 index_cat; desf; simpl in *;
        try (by rewrite rcons_uniq in UNIQ; move: UNIQ ⇒ /andP [NOTIN _]; rewrite Heq0 in NOTIN).
      {
        rewrite eq_refl addn0 in Heq.
        rewrite filter_cat /=.
        assert (EQ: i = size l'); first by apply/eqP; rewrite eqn_leq; apply/andP; split.
        rewrite index_cat Heq0 /= eq_refl addn0 EQ ltnn cats0.
        rewrite nth_cat ltnn subnn /=.
        f_equal; apply eq_in_filter; red; intros y INy.
        by rewrite index_cat INy ltnS index_size index_mem INy.
      }
      {
        rewrite rcons_uniq in UNIQ; move: UNIQ ⇒ /andP [NOTIN UNIQ].
        rewrite eq_refl addn0 in Heq.
        apply negbT in Heq; rewrite -leqNgt in Heq.
        rewrite nth_cat Heq.
        rewrite filter_cat /= index_cat Heq0 /= eq_refl addn0.
        rewrite ltnS in LT; rewrite ltnNge LT /= cats0 cats1.
        apply eq_trans with (y := [seq x1 <- l' | index x1 l' < i.+1]);
          first by apply eq_in_filter; red; intros y INy; rewrite -cats1 index_cat INy.
        rewrite IHl //; f_equal; apply eq_in_filter; intros y INy.
        by rewrite -cats1 index_cat INy.
      }
    }
  Qed.

  Lemma filter_idx_lt_take :
     {T: eqType} (l: seq T) i,
      uniq l
      i < size l
      [seq x <- l | index x l < i] = take i l.
  Proof.
    intros T l i UNIQ LT.
    generalize dependent l.
    induction i.
    {
      intros l UNIQ LT; destruct l as [| x0 l']; first by done.
      by apply eq_trans with (filter pred0 (x0 :: l'));
        [by apply eq_filter | by rewrite filter_pred0].
    }
    {
      intros l UNIQ LT.
      destruct (lastP l) as [| l' x]; first by rewrite ltn0 in LT.
      rewrite size_rcons ltnS in LT.
      rewrite (take_nth x); last by rewrite size_rcons; apply (leq_trans LT).
      rewriteidx_lt_rcons with (x0 := x); try (by done);
        last by rewrite size_rcons; apply (leq_trans LT).
      by f_equal; apply IHi; last by rewrite size_rcons; apply (leq_trans LT).
    }
  Qed.

  Lemma filter_idx_le_takeS :
     {T: eqType} (l: seq T) i,
      uniq l
      i < size l
      [seq x <- l | index x l i] = take i.+1 l.
  Proof.
    intros T l i UNIQ LT.
    induction l as [| x0 l]; first by done.
    simpl; rewrite eq_refl leq0n; f_equal.
    apply eq_trans with (y := [seq x <- l | index x l < i]).
    {
      apply eq_in_filter; red; intros x IN.
      desf; subst; last by done.
      by simpl in *; rewrite IN andFb in UNIQ.
    }
    simpl in *; desf.
    rewrite /= ltnS in LT.
    rewrite leq_eqVlt in LT; desf.
    {
      rewrite take_size.
      apply eq_trans with (y := filter predT l); last by rewrite filter_predT.
      by apply eq_in_filter; red; ins; rewrite index_mem.
    }
    by apply filter_idx_lt_take.
  Qed.

End UniqList.

(* Additional lemmas about list zip. *)
Section Zip.

  Lemma zipP {T: eqType} (x0: T) (P: _ _ bool) (X Y: seq T):
    size X = size Y
    reflect ( i, i < size (zip X Y) P (nth x0 X i) (nth x0 Y i))
            (all (fun pP (fst p) (snd p)) (zip X Y)).
  Proof.
    intro SIZE; apply/introP.
    {
      move ⇒ /allP ALL i LT.
      apply (ALL (nth x0 X i,nth x0 Y i)).
      by rewrite -nth_zip; [by apply mem_nth | by done].
    }
    {
      rewrite -has_predC; unfold predC.
      move ⇒ /hasP HAS; simpl in *; destruct HAS as [x IN NOT].
      unfold not; intro BUG.
      exploit (BUG (index x (zip X Y))).
        by rewrite index_mem.
      have NTH := @nth_zip _ _ x0 x0 X Y (index x (zip X Y)) SIZE.
      destruct x as [x1 x2].
      rewrite {1}nth_index in NTH; last by done.
      clear BUG; intros BUG.
      inversion NTH as [[NTH0 NTH1]]; rewrite -NTH0 in NTH1.
      by rewrite -NTH0 -NTH1 in BUG; rewrite BUG in NOT.
    }
  Qed.

  Lemma mem_zip_exists :
     (T T': eqType) (x1: T) (x2: T') l1 l2 elem elem',
      size l1 = size l2
      (x1, x2) zip l1 l2
       idx,
        idx < size l1
        idx < size l2
        x1 = nth elem l1 idx
        x2 = nth elem' l2 idx.
  Proof.
    intros T T' x1 x2 l1 l2 elem elem' SIZE IN.
    assert (LT: index (x1, x2) (zip l1 l2) < size l1).
    {
      apply leq_trans with (n := size (zip l1 l2)); first by rewrite index_mem.
      by rewrite size_zip; apply geq_minl.
    }
    have NTH := @nth_index _ (elem,elem') (x1, x2) (zip l1 l2) IN.
    rewrite nth_zip in NTH; last by done.
    inversion NTH; rewrite H1 H0; rewrite H0 in H1.
    by (index (x1, x2) (zip l1 l2)); repeat split; try (by done); rewrite -?SIZE.
  Qed.

  Lemma mem_zip :
     (T T': eqType) (x1: T) (x2: T') l1 l2,
      size l1 = size l2
      (x1, x2) zip l1 l2
      x1 l1 x2 l2.
  Proof.
    intros T T' x1 x2 l1 l2 SIZE IN.
    split.
    {
      rewrite -[l1](@unzip1_zip _ _ l1 l2); last by rewrite SIZE.
      by apply/mapP; (x1, x2).
    }
    {
      rewrite -[l2](@unzip2_zip _ _ l1 l2); last by rewrite SIZE.
      by apply/mapP; (x1, x2).
    }
  Qed.

  Lemma mem_zip_nseq_r :
     {T1 T2:eqType} (x: T1) (y: T2) n l,
      size l = n
      ((x, y) zip l (nseq n y)) = (x l).
  Proof.
    intros T1 T2 x y n l SIZE.
    apply/idP/idP.
    {
      intros IN.
      generalize dependent n.
      induction l.
      {
        intros n SIZE IN.
        by destruct n; simpl in IN; rewrite in_nil in IN.
      }
      {
        intros n SIZE; destruct n; first by ins.
        by intros MEM; apply mem_zip in MEM; [des | by rewrite size_nseq].
      }
    }
    {
      intros IN; generalize dependent n.
      induction l; first by rewrite in_nil in IN.
      intros n SIZE; destruct n; first by ins.
      rewrite in_cons in IN; move: IN ⇒ /orP [/eqP EQ | IN];
        first by rewrite in_cons; apply/orP; left; apply/eqP; f_equal.
      simpl in *; apply eq_add_S in SIZE.
      by rewrite in_cons; apply/orP; right; apply IHl.
    }
  Qed.

  Lemma mem_zip_nseq_l :
     {T1 T2:eqType} (x: T1) (y: T2) n l,
      size l = n
      ((x, y) zip (nseq n x) l) = (y l).
  Proof.
    intros T1 T2 x y n l SIZE.
    apply/idP/idP.
    {
      intros IN.
      generalize dependent n.
      induction l.
      {
        intros n SIZE IN.
        by destruct n; simpl in IN; rewrite in_nil in IN.
      }
      {
        intros n SIZE; destruct n; first by ins.
        by intros MEM; apply mem_zip in MEM; [des | by rewrite size_nseq].
      }
    }
    {
      intros IN; generalize dependent n.
      induction l; first by rewrite in_nil in IN.
      intros n SIZE; destruct n; first by ins.
      rewrite in_cons in IN; move: IN ⇒ /orP [/eqP EQ | IN];
        first by rewrite in_cons; apply/orP; left; apply/eqP; f_equal.
      simpl in *; apply eq_add_S in SIZE.
      by rewrite in_cons; apply/orP; right; apply IHl.
    }
  Qed.

End Zip.

(* Restate nth_error function from Coq library. *)
Fixpoint nth_or_none {T: Type} (l: seq T) (n:nat) {struct n} : option T :=
  match n, l with
  | 0, x :: _Some x
  | n.+1, _ :: lnth_or_none l n
  | _, _None
end.

(* Lemmas about nth. *)
Section Nth.

  Context {T: eqType}.

  Lemma nth_in_or_default:
     (l: seq T) x0 i,
      (nth x0 l i) l (nth x0 l i) = x0.
  Proof.
    intros l x0 i.
    generalize dependent i.
    induction l;
      first by right; destruct i.
    destruct i; simpl in *;
      first by left; rewrite in_cons eq_refl.
    by destruct (IHl i) as [IN | DEF];
      [by left; rewrite in_cons IN orbT | by rewrite DEF; right].
  Qed.

  Lemma nth_neq_default :
     (l: seq T) x0 i y,
      nth x0 l i = y
      y x0
      y l.
  Proof.
    intros l x0 i y NTH NEQ.
    by destruct (nth_in_or_default l x0 i) as [IN | DEF];
      [by rewrite -NTH | by rewrite -NTH DEF in NEQ].
  Qed.

  Lemma nth_or_none_mem :
     (l: seq T) n x, nth_or_none l n = Some x x l.
  Proof.
    induction l; first by unfold nth_or_none; ins; destruct n; ins.
    {
      ins; destruct n.
      {
        inversion H; subst.
        by rewrite in_cons eq_refl orTb.
      }
      simpl in H; rewrite in_cons; apply/orP; right.
      by apply IHl with (n := n).
    }
  Qed.

  Lemma nth_or_none_mem_exists :
     (l: seq T) x, x l n, nth_or_none l n = Some x.
  Proof.
    induction l; first by intros x IN; rewrite in_nil in IN.
    {
      intros x IN; rewrite in_cons in IN.
      move: IN ⇒ /orP [/eqP EQ | IN]; first by subst; 0.
      specialize (IHl x IN); des.
      by n.+1.
    }
  Qed.

  Lemma nth_or_none_size_none :
     (l: seq T) n,
      nth_or_none l n = None n size l.
  Proof.
    induction l; first by split; destruct n.
    by destruct n; simpl; [by split; last by rewrite ltn0 | by rewrite ltnS].
  Qed.

  Lemma nth_or_none_size_some :
     (l: seq T) n x,
      nth_or_none l n = Some x n < size l.
  Proof.
    induction l; first by destruct n.
    by intros n x; destruct n; simpl; last by rewrite ltnS; apply IHl.
  Qed.

  Lemma nth_or_none_uniq :
     (l: seq T) i j x,
      uniq l
      nth_or_none l i = Some x
      nth_or_none l j = Some x
      i = j.
  Proof.
    intros l i j x UNIQ SOMEi SOMEj.
    {
      generalize dependent j.
      generalize dependent i.
      induction l;
        first by ins; destruct i, j; simpl in *; inversion SOMEi.
      intros i SOMEi j SOMEj.
      simpl in UNIQ; move: UNIQ ⇒ /andP [NOTIN UNIQ].
      feed IHl; first by done.
      destruct i, j; simpl in *; first by done.
      - by inversion SOMEi; subst; apply nth_or_none_mem in SOMEj; rewrite SOMEj in NOTIN.
      - by inversion SOMEj; subst; apply nth_or_none_mem in SOMEi; rewrite SOMEi in NOTIN.
      - by f_equal; apply IHl.
    }
  Qed.

  Lemma nth_or_none_nth :
     (l: seq T) n x x0,
      nth_or_none l n = Some x
      nth x0 l n = x.
  Proof.
    induction l; first by destruct n.
    by intros n x x0 SOME; destruct n; simpl in *; [by inversion SOME | by apply IHl].
  Qed.

End Nth.

Section PartialMap.

  Lemma pmap_inj_in_uniq {T T': eqType} (s: seq T) (f: T option T') :
    {in s &, ssrfun.injective f}
    uniq s
    uniq (pmap f s).
  Proof.
    intros INJ UNIQ; red in INJ.
    induction s; first by done.
    simpl in *; unfold ssrfun.Option.apply.
    move: UNIQ ⇒ /andP [NOTIN UNIQ].
    feed IHs.
      by ins; apply INJ; try (by rewrite in_cons; apply/orP; right).
    specialize (IHs UNIQ).
    destruct (f a) eqn:F; simpl; last by done.
    rewrite IHs andbT mem_pmap -F.
    apply/mapP; move ⇒ [a' IN' EQ].
    exploit (INJ a a'); try (by done).
      by rewrite in_cons; apply/orP; left.
      by rewrite in_cons; apply/orP; right.
    by intros EQ'; subst; rewrite IN' in NOTIN.
  Qed.

  Lemma pmap_inj_uniq {T T': eqType} (s: seq T) (f: T option T') :
    ssrfun.injective f
    uniq s
    uniq (pmap f s).
  Proof.
    intros INJ UNIQ.
    apply pmap_inj_in_uniq; last by done.
    by red; ins; apply INJ.
  Qed.

End PartialMap.

(* Define a set_nth that does not grow the vector. *)
Program Definition set_nth_if_exists {T: Type} (l: seq T) n y :=
  if n < size l then
    set_nth _ l n y
  else l.

(* Define a function that replaces the first element that satisfies
   some predicate with using a mapping function f. *)

Fixpoint replace_first {T: Type} P f (l: seq T) :=
  if l is x0 :: l' then
    if P x0 then
      f x0 :: l'
    else x0 :: replace_first P f l'
  else [::].

(* Define a function that replaces the first element that satisfies
   some predicate with a constant. *)

Definition replace_first_const {T: Type} P y (l: seq T) :=
  replace_first P (fun xy) l.

Definition set_pair_1nd {T1: Type} {T2: Type} (y: T2) (p: T1 × T2) :=
  (fst p, y).

Definition set_pair_2nd {T1: Type} {T2: Type} (y: T2) (p: T1 × T2) :=
  (fst p, y).

Section Replace.

  Context {T: eqType}.

  Lemma replace_first_size P f (l: seq T) :
    size (replace_first P f l) = size l.
  Proof.
    induction l; simpl; first by done.
    by destruct (P a); rewrite // /= IHl.
  Qed.

  Lemma replace_first_cases {P} {f} {l: seq T} {x}:
    x replace_first P f l
    x l ( y, x = f y P y y l).
  Proof.
    intros IN.
    induction l; simpl in *; first by rewrite IN; left.
    destruct (P a) eqn:HOLDS.
    {
      rewrite in_cons in IN; des;
        last by left; rewrite in_cons IN orbT.
      right; a; split; first by done.
      by split; last by rewrite in_cons eq_refl orTb.
    }
    {
      rewrite in_cons in IN; des;
        first by left; rewrite in_cons IN eq_refl orTb.
      specialize (IHl IN); des;
        first by left; rewrite in_cons IHl orbT.
      right; y; split; first by done.
      by split; last by rewrite in_cons IHl1 orbT.
    }
  Qed.

  Lemma replace_first_no_change {P} {f} {l: seq T} {x}:
    x l
    ¬ P x
    x replace_first P f l.
  Proof.
    intros IN NOT.
    induction l; simpl in *; first by rewrite in_nil in IN.
    destruct (P a) eqn:HOLDS.
    {
      rewrite in_cons in IN; des; last by rewrite in_cons IN orbT.
      by rewrite IN HOLDS in NOT.
    }
    {
      rewrite in_cons in IN; des; first by rewrite IN in_cons eq_refl orTb.
      by rewrite in_cons; apply/orP; right; apply IHl.
    }
  Qed.

  Lemma replace_first_idempotent {P} {f} {l: seq T} {x}:
    x l
    f x = x
    x replace_first P f l.
  Proof.
    intros IN IDEMP.
    induction l; simpl in *; first by rewrite in_nil in IN.
    destruct (P a) eqn:HOLDS.
    {
      rewrite in_cons in IN; des; last by rewrite in_cons IN orbT.
      by rewrite -IN -{1}IDEMP; rewrite in_cons eq_refl orTb.

    }
    {
      rewrite in_cons in IN; des; first by rewrite IN in_cons eq_refl orTb.
      by rewrite in_cons; apply/orP; right; apply IHl.
    }
  Qed.

  Lemma replace_first_new :
     P f (l: seq T) x1 x2,
    x1 l
    x2 l
    x1 replace_first P f l
    x2 replace_first P f l
    x1 = x2.
  Proof.
    intros P f l x1 x2 NOT1 NOT2 IN1 IN2.
    induction l; simpl in *; first by rewrite in_nil in IN1.
    {
      destruct (P a) eqn:HOLDS.
      {
        rewrite 2!in_cons in IN1 IN2.
        rewrite 2!in_cons 2!negb_or in NOT1 NOT2.
        move: NOT1 NOT2 ⇒ /andP [NEQ1 NOT1] /andP [NEQ2 NOT2].
        move: IN1 ⇒ /orP [/eqP F1 | IN1]; last by rewrite IN1 in NOT1.
        move: IN2 ⇒ /orP [/eqP F2 | IN2]; last by rewrite IN2 in NOT2.
        by rewrite F1 F2.
      }
      {
        rewrite 2!in_cons in IN1 IN2.
        rewrite 2!in_cons 2!negb_or in NOT1 NOT2.
        move: NOT1 NOT2 ⇒ /andP [NEQ1 NOT1] /andP [NEQ2 NOT2].
        move: IN1 ⇒ /orP [/eqP A1 | IN1]; first by rewrite A1 eq_refl in NEQ1.
        move: IN2 ⇒ /orP [/eqP A2 | IN2]; first by rewrite A2 eq_refl in NEQ2.
        by apply IHl.
      }
    }
  Qed.

  Lemma replace_first_previous P f {l: seq T} {x}:
    x l
      (x replace_first P f l)
      (P x f x replace_first P f l).
  Proof.
    intros IN; induction l; simpl in *; first by rewrite in_nil in IN.
    destruct (P a) eqn:HOLDS.
    {
      rewrite in_cons in IN; des; subst.
      {
        right; rewrite HOLDS; split; first by done.
        by rewrite in_cons; apply/orP; left.
      }
      by rewrite in_cons IN; left; apply/orP; right.
    }
    {
      rewrite in_cons in IN; des; subst;
        first by left; rewrite in_cons eq_refl orTb.
      specialize (IHl IN); des;
        first by left; rewrite in_cons IHl orbT.
      right; rewrite IHl; split; first by done.
      by rewrite in_cons IHl0 orbT.
    }
  Qed.

  Lemma replace_first_failed P f {l: seq T}:
    ( x, x l f x replace_first P f l)
    ( x, x l ¬ P x).
  Proof.
    intros NOTIN.
    induction l as [| a l']; simpl in *;
      first by intros x IN; rewrite in_nil in IN.
    intros x IN.
    destruct (P a) eqn:HOLDS.
    {
      exploit (NOTIN a); first by rewrite in_cons eq_refl orTb.
      by rewrite in_cons eq_refl orTb.
    }
    {
      rewrite in_cons in IN; move: IN ⇒ /orP [/eqP EQ | IN];
        first by subst; rewrite HOLDS.
      apply IHl'; last by done.
      intros y INy.
      exploit (NOTIN y); first by rewrite in_cons INy orbT.
      intros NOTINy.
      rewrite in_cons negb_or in NOTINy.
      by move: NOTINy ⇒ /andP [_ NOTINy].
    }
  Qed.

End Replace.

Definition pairs_to_function {T1: eqType} {T2: Type} y0 (l: seq (T1×T2)) :=
  fun xnth y0 (unzip2 l) (index x (unzip1 l)).

Section Pairs.

  Lemma pairs_to_function_neq_default {T1: eqType} {T2: eqType} y0 (l: seq (T1×T2)) x y :
    pairs_to_function y0 l x = y
    y y0
    (x,y) l.
  Proof.
    unfold pairs_to_function, unzip1, unzip2; intros PAIR NEQ.
    induction l; simpl in *; first by subst.
    destruct (fst a = x) eqn:FST; simpl in ×.
    {
      move: FST ⇒ /eqP FST; subst.
      by rewrite in_cons; apply/orP; left; destruct a.
    }
    {
      by specialize (IHl PAIR); rewrite in_cons; apply/orP; right.
    }
  Qed.

  Lemma pairs_to_function_mem {T1: eqType} {T2: eqType} y0 (l: seq (T1×T2)) x y :
    uniq (unzip1 l)
    (x,y) l
    pairs_to_function y0 l x = y.
  Proof.
    unfold pairs_to_function, unzip1, unzip2; intros UNIQ IN.
    induction l as [| [x' y'] l']; simpl in *; first by rewrite in_nil in IN.
    {
      move: UNIQ ⇒ /andP [NOTIN UNIQ]; specialize (IHl' UNIQ).
      destruct (x' = x) eqn:FST; simpl in ×.
      {
        move: FST ⇒ /eqP FST; subst.
        rewrite in_cons /= in IN.
        move: IN ⇒ /orP [/eqP EQ | IN];
          first by case: EQ ⇒ →.
        exfalso; move: NOTIN ⇒ /negP NOTIN; apply NOTIN.
        by apply/mapP; (x,y).
      }
      {
        rewrite in_cons /= in IN.
        move: IN ⇒ /orP [/eqP EQ | IN];
          first by case: EQEQ1 EQ2; subst; rewrite eq_refl in FST.
        by apply IHl'.
      }
    }
  Qed.

End Pairs.

Section Order.

  Context {T: eqType}.
  Variable rel: T T bool.
  Variable l: seq T.

  Definition total_over_list :=
     x1 x2,
      x1 l
      x2 l
      (rel x1 x2 rel x2 x1).

  Definition antisymmetric_over_list :=
     x1 x2,
      x1 l
      x2 l
      rel x1 x2
      rel x2 x1
      x1 = x2.

End Order.