(* ---------- list lemmas ---------- *)
Lemma valid_gt s P : valid_from s P -> Forall (fun p => s < p) P.
Proof.
  revert s. induction P as [|p P IH]; intros s H; [constructor|].
  destruct H as [[t Ht] HP]. constructor; [lia|].
  specialize (IH p HP). eapply Forall_impl; [|exact IH]. intros x Hx; cbn in *; lia.
Qed.

Lemma cnt_cons_lt q Q n : q < n -> cnt (q :: Q) n = S (cnt Q n).
Proof. intros H. unfold cnt. cbn [filter]. rewrite (proj2 (Nat.ltb_lt q n) H). reflexivity. Qed.

Lemma cnt_cons_ge q Q n : n <= q -> cnt (q :: Q) n = cnt Q n.
Proof. intros H. unfold cnt. cbn [filter]. rewrite (proj2 (Nat.ltb_ge q n) H). reflexivity. Qed.

Lemma cnt_app X Y n : cnt (X ++ Y) n = cnt X n + cnt Y n.
Proof. unfold cnt. rewrite filter_app, length_app. reflexivity. Qed.

Lemma cnt_all_lt X n : Forall (fun q => q < n) X -> cnt X n = length X.
Proof.
  induction 1 as [|q X Hq HX IH]; [reflexivity|].
  rewrite cnt_cons_lt by exact Hq. cbn [length]. lia.
Qed.

Lemma cnt_all_ge X n : Forall (fun q => n <= q) X -> cnt X n = 0.
Proof.
  induction 1 as [|q X Hq HX IH]; [reflexivity|].
  rewrite cnt_cons_ge by exact Hq. exact IH.
Qed.

Lemma cnt_S_nin Q n : ~ In n Q -> cnt Q (S n) = cnt Q n.
Proof.
  induction Q as [|q Q IH]; intros H; [reflexivity|].
  assert (q <> n) by (intro; apply H; left; auto).
  assert (~ In n Q) by (intro; apply H; right; auto).
  destruct (Nat.lt_ge_cases q n).
  - rewrite !cnt_cons_lt by lia. f_equal. auto.
  - rewrite !cnt_cons_ge by lia. auto.
Qed.

Lemma cnt_S_in s Q n : valid_from s Q -> In n Q -> cnt Q (S n) = S (cnt Q n).
Proof.
  revert s. induction Q as [|q Q IH]; intros s HV H; [destruct H|].
  destruct HV as [_ HV]. pose proof (valid_gt _ _ HV) as Hg. rewrite Forall_forall in Hg.
  destruct H as [<- | H].
  - rewrite cnt_cons_lt by lia. rewrite cnt_cons_ge by lia. f_equal. apply cnt_S_nin.
    intro Hin. specialize (Hg _ Hin). lia.
  - pose proof (Hg _ H). rewrite !cnt_cons_lt by lia. f_equal. eapply IH; eauto.
Qed.

Lemma ind_in Q n : valid Q -> In n Q -> ind Q n = 1.
Proof. intros HV H. unfold ind. rewrite (cnt_S_in 0 Q n HV H). lia. Qed.

Lemma ind_nin Q n : ~ In n Q -> ind Q n = 0.
Proof. intros H. unfold ind. rewrite (cnt_S_nin Q n H). lia. Qed.

Lemma ind_iff P Q k k' : valid P -> valid Q -> (In k P <-> In k' Q) -> ind P k = ind Q k'.
Proof.
  intros HP HQ E. destruct (in_dec Nat.eq_dec k P) as [H|H].
  - rewrite (ind_in P k HP H), (ind_in Q k' HQ (proj1 E H)). reflexivity.
  - rewrite (ind_nin P k H), (ind_nin Q k'); [reflexivity|]. intro H'. apply H, E, H'.
Qed.

Lemma parity_in s P n : valid_from s P -> In n P -> exists u, n + cnt P n + s = 2 * u + 1.
Proof.
  revert s. induction P as [|p P IH]; intros s HV H; [destruct H|].
  destruct HV as [[t Ht] HV]. pose proof (valid_gt _ _ HV) as Hg. rewrite Forall_forall in Hg.
  destruct H as [<- | H].
  - rewrite cnt_cons_ge by lia. rewrite cnt_all_ge.
    + exists (s + t). lia.
    + apply Forall_forall. intros x Hx. specialize (Hg _ Hx). lia.
  - pose proof (Hg _ H). rewrite cnt_cons_lt by lia. destruct (IH p HV H) as [u Hu].
    exists (u - t). lia.
Qed.

Lemma filter_lt_app X Y k : Forall (fun q => q <= k) X ->
  filter (fun q => k <? q) (X ++ Y) = filter (fun q => k <? q) Y.
Proof.
  intros H. rewrite filter_app. replace (filter (fun q => k <? q) X) with (@nil nat); [reflexivity|].
  induction H as [|q X Hq HX IH]; cbn [filter]; [reflexivity|].
  rewrite (proj2 (Nat.ltb_ge k q) Hq). exact IH.
Qed.

Lemma filter_filter_lt P k k' : k <= k' ->
  filter (fun p => k' <? p) (filter (fun p => k <? p) P) = filter (fun p => k' <? p) P.
Proof.
  intros Hk. induction P as [|p P IH]; cbn [filter]; [reflexivity|].
  destruct (Nat.ltb_spec k p); cbn [filter]; destruct (Nat.ltb_spec k' p); try lia; rewrite IH; reflexivity.
Qed.

Lemma filter_all P k : Forall (fun p => k < p) P -> filter (fun p => k <? p) P = P.
Proof.
  induction 1 as [|p P Hp HP IH]; cbn [filter]; [reflexivity|].
  rewrite (proj2 (Nat.ltb_lt k p) Hp). rewrite IH. reflexivity.
Qed.

Lemma filter_gt P k p : In p (filter (fun p => k <? p) P) -> k < p.
Proof. intros Hp. apply filter_In in Hp. destruct Hp as [_ Hp]. apply Nat.ltb_lt. exact Hp. Qed.

Lemma filter_in P k p : k < p -> (In p (filter (fun p => k <? p) P) <-> In p P).
Proof.
  intros H. rewrite filter_In. split; [tauto|]. intros Hp. split; [exact Hp | apply Nat.ltb_lt; exact H].
Qed.

Lemma filter_cnt_len P n : length (filter (fun p => n <? p) P) + cnt P (S n) = length P.
Proof.
  induction P as [|p P IH]; [reflexivity|]. cbn [filter length].
  destruct (Nat.ltb_spec n p).
  - rewrite cnt_cons_ge by lia. cbn [length]. lia.
  - rewrite cnt_cons_lt by lia. lia.
Qed.

(* shifted copies of index lists *)
Definition Sh (u v : nat) (Q P : list nat) : Prop := Forall2 (fun q p => q + u = p + v) Q P.

Lemma Sh_len u v Q P : Sh u v Q P -> length Q = length P.
Proof. apply Forall2_length. Qed.

Lemma Sh_eq u v u' v' Q P : Sh u v Q P -> u = u' -> v = v' -> Sh u' v' Q P.
Proof. intros H -> ->. exact H. Qed.

Lemma Sh_filter u v Q P k k' : Sh u v Q P -> k + u = k' + v ->
  Sh u v (filter (fun q => k <? q) Q) (filter (fun p => k' <? p) P).
Proof.
  unfold Sh. induction 1 as [|q p Q P Hqp HQP IH]; intros Hk; cbn [filter]; [constructor|].
  destruct (Nat.ltb_spec k q), (Nat.ltb_spec k' p); try lia.
  - constructor; auto.
  - auto.
Qed.

Lemma Sh_in u v Q P k k' : Sh u v Q P -> k + u = k' + v -> (In k Q <-> In k' P).
Proof.
  unfold Sh. induction 1 as [|q p Q P Hqp HQP IH]; intros Hk; cbn [In]; [tauto|].
  specialize (IH Hk). split; (intros [H|H]; [left; lia | right; tauto]).
Qed.

Lemma Sh_trans u1 v1 u2 v2 u v w X Y Z : Sh u1 v1 X Y -> Sh u2 v2 Y Z ->
  u1 + u2 = u + w -> v1 + v2 = v + w -> Sh u v X Z.
Proof.
  unfold Sh. intros H1. revert Z. induction H1 as [|x y X Y Hxy HXY IH]; intros Z H2 E1 E2;
    inversion H2; subst; constructor; [lia | auto].
Qed.

Lemma Sh_map u v d Q P : Sh u v Q P -> Sh u (v + d) (map (fun q => q + d) Q) P.
Proof. unfold Sh. induction 1; cbn [map]; constructor; [lia | auto]. Qed.

Lemma Sh_unmap v k P : Forall (fun p => k <= p) P -> Sh (v + k) v (map (fun p => p - k) P) P.
Proof. unfold Sh. induction 1; cbn [map]; constructor; [lia | auto]. Qed.

Lemma Sh_ge u v Q P k k' : Sh u v Q P -> (forall p, In p P -> k' <= p) -> k + u <= k' + v ->
  Forall (fun q => k <= q) Q.
Proof.
  unfold Sh. induction 1 as [|q p Q P Hqp HQP IH]; intros Hp Hk; constructor.
  - specialize (Hp p (or_introl eq_refl)). lia.
  - apply IH; [intros x Hx; apply Hp; right; exact Hx | exact Hk].
Qed.

Lemma valid_shift s k P : valid_from s P -> valid_from (s + k) (map (fun p => p + k) P).
Proof.
  revert s. induction P as [|p P IH]; intros s H; [exact I|].
  destruct H as [[t Ht] H]. cbn [map valid_from]. split; [exists t; lia | apply IH; exact H].
Qed.

Lemma valid_map2 s P : valid_from s P -> valid_from s (map (fun p => p + 2) P).
Proof.
  destruct P as [|p P]; intros H; [exact I|]. destruct H as [[t Ht] H].
  cbn [map valid_from]. split; [exists (S t); lia | apply valid_shift; exact H].
Qed.

Lemma valid_cons1 Q : valid Q -> valid (1 :: map (fun q => q + 1) Q).
Proof. intros H. cbn [valid valid_from]. split; [exists 0; lia | apply (valid_shift 0 1 Q H)]. Qed.

Lemma valid_unshift s k P : valid_from (s + k) P -> valid_from s (map (fun p => p - k) P).
Proof.
  revert s. induction P as [|p P IH]; intros s H; [exact I|].
  destruct H as [[t Ht] H]. cbn [map valid_from]. split; [exists t; lia|].
  apply IH. replace (p - k + k) with p by lia. exact H.
Qed.

Lemma valid_app_l X Y : valid (X ++ Y) -> Forall (fun q => 1 <= q) X.
Proof.
  intros H. apply valid_gt in H. apply Forall_app in H. destruct H as [H _].
  eapply Forall_impl; [|exact H]. intros; lia.
Qed.

Lemma mwf_unshift s k P : k <= s -> Forall (fun p => k <= p) P ->
  mwf (s - k) (map (fun p => p - k) P) = mwf s P.
Proof.
  intros Hs H. revert s Hs. induction H as [|p P Hp HP IH]; intros s Hs; cbn [map mwf]; [reflexivity|].
  rewrite (IH p Hp). f_equal. lia.
Qed.

Lemma mw_cons1 Q : 2 :: 1 :: mw Q = mw (1 :: map (fun q => q + 1) Q).
Proof. unfold mw. cbn [mwf]. rewrite <- (mwf_shift 0 1 Q). reflexivity. Qed.