Library probsa.util.seq

From mathcomp Require Export ssreflect ssrbool eqtype ssrnat seq.

Require Export prosa.util.list.

Lemma seq_split_take_drop :
  ∀ {X : eqType} (e : X) (xs : seq X),
    (e \in xs) →
    xs = take (index e xs) xs ++ [:: e] ++ drop (index e xs).+1 xs.
Proof.
  intros × IN.
  induction xs; first by done.
  simpl; destruct ( _ == _ ) eqn:EQ.
  { by rewrite //= drop0; move: EQ ⇒ /eqP EQ; subst. }
  { rewrite //= {1}IHxs //=.
    by move: IN; rewrite in_cons eq_sym EQ orFb. }
Qed.

Lemma seq_split :
  ∀ {X : eqType} (e : X) (xs : seq X),
    (e \in xs) →
    ∃ xs1 xs2,
      xs = xs1 ++ [::e] ++ xs2
      ∧ (e \notin xs1).
Proof.
  intros × IN.
  set (i := index e xs).
  ∃ (take i xs), (drop i.+1 xs).
  repeat split.
  { by apply seq_split_take_drop. }
  { apply/negP ⇒ INT; apply index_ltn in INT.
    by rewrite ltnn in INT.
  }
Qed.

Lemma choose_superior_default_or_in_seq :
  ∀ {X : eqType} (R : rel X) (a e : X) (ys : seq X),
    foldr (choose_superior R) (Some a) ys = Some e →
    a = e ∨ e \in ys.
Proof.
  intros; induction ys.
  { by inversion H; subst; left. }
  { simpl in H.
    destruct (foldr (choose_superior R) (Some a) ys) eqn:FLR.
    { unfold choose_superior in H; destruct (R a0 s) eqn:REL.
      { inversion H; subst; right.
        by rewrite in_cons eq_refl orTb. }
      { inversion H; subst; apply IHys in H.
        by destruct H; [subst; left | right; rewrite in_cons H orbT].
      }
    }
    { by inversion H; subst; right; rewrite in_cons eq_refl orTb. }
  }
Qed.

Lemma foldr_choose_superior_not_none :
  ∀ {X : eqType} (R : rel X) (e : X) (ys : seq X),
    ¬ foldr (choose_superior R) (Some e) ys = None.
Proof.
  intros; induction ys; first by simpl.
  simpl; intros ?; apply: IHys.
  destruct (foldr (choose_superior R) (Some e) ys).
  { by unfold choose_superior in H; destruct (R a s). }
  { by done. }
Qed.

Lemma foldr_choose_superior_in_seq :
  ∀ {X : eqType} (R : rel X) (ys : seq X) (y e : X),
    (y \in ys) →
    (R y e) →
    foldr (choose_superior R) (Some e) ys = Some e →
    e \in ys.
Proof.
  intros × IN Rye FL.
  have FF := seq_split _ _ IN.
  destruct FF as [xs1 [xs2 [EQ NIN]]].
  subst; rewrite !foldr_cat in FL.
  simpl in FL; clear IN.
  destruct (foldr (choose_superior R) (Some e) xs2) eqn:EQ.
  { simpl in FL; destruct (R y s) eqn: RR.
    { eapply choose_superior_default_or_in_seq in FL; destruct FL as []; subst.
      { by rewrite !mem_cat mem_seq1 eq_refl orbT. }
      { by rewrite !mem_cat H. }
    }
    { apply choose_superior_default_or_in_seq in FL.
      destruct FL as []; subst.
      { by rewrite RR in Rye. }
      { by rewrite !mem_cat H. }
    }
  }
  { by eapply foldr_choose_superior_not_none in EQ. }
Qed.

Lemma supremum_monotone_wrt_subset :
  ∀ {X : eqType} (R : rel X) (e : X) (xs ys : seq X),
    reflexive R →
    total R →
    transitive R →
    uniq ys →
    subseq xs ys →
    (e \in xs) →
    supremum R ys = Some e →
    supremum R xs = Some e.
Proof.
  intros × REF TOT TR UNIQ SUB IN SUP.
  have INy : e \in ys by apply: supremum_in; eassumption.
  move: (seq_split e ys INy) ⇒ [ys1 [ys2 [EQ NINy]]]; subst ys.
  have NR1 : ∀ y, y \in ys2 → R e y.
  { intros; apply supremum_spec with (y0 := y) in SUP ⇒ //.
    by rewrite mem_cat mem_cat H !orbT. }
  have NR2 : ∀ y, y \in ys1 → ~~ R y e.
  { intros; apply/negP ⇒ Rye; clear INy SUB IN.
    rewrite /supremum !foldr_cat in SUP.
    destruct (foldr (choose_superior R) None ys2) eqn:FLD2.
    { have EQ : foldr (choose_superior R) (Some s) [:: e] = Some e.
      { by rewrite //= NR1; [reflexivity | apply supremum_in in FLD2]. }
      rewrite EQ in SUP; clear EQ FLD2.
      eapply foldr_choose_superior_in_seq in SUP; eauto 1.
      by rewrite SUP in NINy.
    }
    { eapply foldr_choose_superior_in_seq in SUP; eauto 1.
      by rewrite SUP in NINy.
    }
  }
  have L2: ∃ xs1 xs2, xs = xs1 ++ [::e] ++ xs2 ∧ e \notin xs1.
  { set (i := index e xs).
    ∃ (take i xs), (drop i.+1 xs).
    repeat split.
    { by apply seq_split_take_drop. }
    { apply/negP ⇒ INT; apply index_ltn in INT.
      by rewrite ltnn in INT.
    }
  }
  clear IN; move: L2 ⇒ [xs1 [xs2 [EQ NINx]]]; subst xs.
  have L22: subseq xs1 ys1 ∧ subseq xs2 ys2.
  { apply/andP; erewrite <-uniq_subseq_pivot.
    { by instantiate (1 := e); apply SUB. }
    { by done. }
  }
  clear SUB; move: L22 ⇒ [SUB1 SUB2].
  have L3 : ∀ x : X, x \in xs1 → ~~ R x e.
  { by intros × IN; apply NR2; apply: mem_subseq; eauto 1. }
  have L4 : ∀ x : X, x \in xs2 → R e x.
  { by intros × IN; apply NR1; apply: mem_subseq; eauto 1. }
  rewrite /supremum foldr_cat foldr_cat.
  have FLEQ: foldr (choose_superior R) (Some e) xs1 = Some e.
  { clear SUB1 SUB2 NINy NINx.
    induction xs1; first by done.
    rewrite //= IHxs1.
    { simpl.
      have → : R a e = false.
      { apply/eqP; rewrite eqbF_neg; apply L3.
        by rewrite in_cons eq_refl orTb.
      }
      reflexivity.
    }
    { by intros; apply L3; rewrite in_cons H orbT. }
  }
  destruct (foldr _ None _) eqn:FL3; last by apply FLEQ.
  destruct (foldr _ (Some s) _) eqn:FLe.
  { simpl in FLe.
    rewrite L4 in FLe; last by apply: supremum_in; apply FL3.
    inversion FLe; subst s0; clear FLe.
    by apply FLEQ.
  }
  { by simpl in FLe; destruct (R e s). }
Qed.

Lemma subseq_filter :
  ∀ {X : eqType} (xs : seq X) (P1 P2 : pred X),
    (∀ x, x \in xs → P1 x → P2 x) →
    subseq [seq x <- xs | P1 x] [seq x <- xs | P2 x].
Proof.
  intros; rewrite subseq_filter; apply/andP; split.
  { by apply/allP ⇒ x; rewrite mem_filter ⇒ /andP [Px INx]; apply H. }
  { by apply filter_subseq. }
Qed.