From Undecidability.Shared.Libs.PSL Require Export Prelim EqDec.

Export List.ListNotations.
Notation "x 'el' A" := (In x A) (at level 70).
Notation "A <<= B" := (incl A B) (at level 70).
Notation "| A |" := (length A) (at level 65).
Definition equi X (A B : list X) : Prop := incl A B /\ incl B A.
Notation "A === B" := (equi A B) (at level 70).
#[export] Hint Unfold equi : core.

#[export] Hint Extern 4 =>
match goal with
|[ H: ?x el nil |- _ ] => destruct H
end : core.


Global Hint Rewrite <- app_assoc : list.
Global Hint Rewrite rev_app_distr map_app prod_length : list.

Lemma list_cycle (X : Type) (A : list X) x :
  x::A <> A.
Proof.
  intros B.
  assert (C: |x::A| <> |A|) by (cbn; lia).
  apply C. now rewrite B.
Qed.


#[global]
Instance list_in_dec X (x : X) (A : list X) :
  eq_dec X -> dec (x el A).
Proof.
  intros D. apply in_dec. exact D.
Qed.


Lemma cfind X A (p: X -> Prop) (p_dec: forall x, dec (p x)) :
  {x | x el A /\ p x} + {forall x, x el A -> ~ p x}.
Proof.
  destruct (find (fun x => Dec (p x)) A) eqn:E.
  - apply find_some in E. firstorder.
  - right. intros. eapply find_none in E; eauto.
Qed.

Arguments cfind {X} A p {p_dec}.

#[global]
Instance list_forall_dec X A (p : X -> Prop) :
  (forall x, dec (p x)) -> dec (forall x, x el A -> p x).
Proof.
  intros p_dec.
  destruct (find (fun x => Dec (~ p x)) A) eqn:Eq.
  - apply find_some in Eq as [H1 H0 %Dec_true]; right; auto.
  - left. intros x E. apply find_none with (x := x) in Eq. apply dec_DN; auto. auto.
Qed.

#[global]
Instance list_exists_dec X A (p : X -> Prop) :
  (forall x, dec (p x)) -> dec (exists x, x el A /\ p x).
Proof.
  intros p_dec.
  destruct (find (fun x => Dec (p x)) A) eqn:Eq.   - apply find_some in Eq as [H0 H1 %Dec_true]. firstorder.   - right. intros [x [E F]]. apply find_none with (x := x) in Eq; auto. eauto. Qed.

Lemma list_exists_DM X A (p : X -> Prop) :
  (forall x, dec (p x)) ->
  ~ (forall x, x el A -> ~ p x) -> exists x, x el A /\ p x.
Proof.
  intros D E.
  destruct (find (fun x => Dec (p x)) A) eqn:Eq.
  + apply find_some in Eq as [? ?%Dec_true]. eauto.
  + exfalso. apply E. intros. apply find_none with (x := x) in Eq; eauto.
Qed.

Lemma list_exists_not_incl (X: eqType) (A B : list X) :
  ~ A <<= B -> exists x, x el A /\ ~ x el B.
Proof.
  intros E.
  apply list_exists_DM; auto.
  intros F. apply E. intros x G.
  apply dec_DN; auto.
Qed.

Lemma list_cc X (p : X -> Prop) A :
  (forall x, dec (p x)) ->
  (exists x, x el A /\ p x) -> {x | x el A /\ p x}.
Proof.
  intros D E.
  destruct (cfind A p) as [[x [F G]]|F].
  - eauto.
  - exfalso. destruct E as [x [G H]]. apply (F x); auto.
Qed.


#[export] Hint Resolve in_eq in_nil in_cons in_or_app : core.

Section Membership.
  Variable X : Type.
  Implicit Types (x y: X) (A B: list X).

  Lemma in_sing x y :
    x el [y] -> x = y.
  Proof.
    cbn. intros [[]|[]]. reflexivity.
  Qed.

  Lemma in_cons_neq x y A :
    x el y::A -> x <> y -> x el A.
  Proof.
    cbn. intros [[]|D] E; congruence.
  Qed.

  Lemma not_in_cons x y A :
    ~ x el y :: A -> x <> y /\ ~ x el A.
  Proof.
    intuition; subst; auto.
  Qed.


  Definition disjoint A B :=
    ~ exists x, x el A /\ x el B.

  Lemma disjoint_forall A B :
    disjoint A B <-> forall x, x el A -> ~ x el B.
  Proof.
    split.
    - intros D x E F. apply D. exists x. auto.
    - intros D [x [E F]]. exact (D x E F).
  Qed.

  Lemma disjoint_symm A B :
    disjoint A B -> disjoint B A.
  Proof.
    firstorder.
  Qed.

  Lemma disjoint_incl A B B' :
    B' <<= B -> disjoint A B -> disjoint A B'.
  Proof.
    firstorder.
  Qed.

  Lemma disjoint_nil B :
    disjoint nil B.
  Proof.
    firstorder.
  Qed.

  Lemma disjoint_nil' A :
    disjoint A nil.
  Proof.
    firstorder.
  Qed.

  Lemma disjoint_cons x A B :
    disjoint (x::A) B <-> ~ x el B /\ disjoint A B.
  Proof.
    split.
    - intros D. split.
      + intros E. apply D. eauto.
      + intros [y [E F]]. apply D. eauto.
    - intros [D E] [y [[F|F] G]].
      + congruence.
      + apply E. eauto.
  Qed.

  Lemma disjoint_app A B C :
    disjoint (A ++ B) C <-> disjoint A C /\ disjoint B C.
  Proof.
    split.
    - intros D. split.
      + intros [x [E F]]. eauto 6.
      + intros [x [E F]]. eauto 6.
    - intros [D E] [x [F G]].
      apply in_app_iff in F as [F|F]; eauto.
  Qed.

End Membership.

#[export] Hint Resolve disjoint_nil disjoint_nil' : core.


#[export] Hint Resolve incl_refl incl_tl incl_cons incl_appl incl_appr incl_app : core.

Lemma incl_nil X (A : list X) :
  nil <<= A.

Proof. intros x []. Qed.

#[export] Hint Resolve incl_nil : core.

Lemma incl_map X Y A B (f : X -> Y) :
  A <<= B -> map f A <<= map f B.

Proof.
  intros D y E. apply in_map_iff in E as [x [E E']].
  subst y. apply in_map_iff. eauto.
Qed.

Section Inclusion.
  Variable X : Type.
  Implicit Types A B : list X.

  Lemma incl_nil_eq A :
    A <<= nil -> A=nil.

  Proof.
    intros D. destruct A as [|x A].
    - reflexivity.
    - exfalso. apply (D x). auto.
  Qed.

  Lemma incl_shift x A B :
    A <<= B -> x::A <<= x::B.

  Proof. auto. Qed.

  Lemma incl_lcons x A B :
    x::A <<= B <-> x el B /\ A <<= B.
  Proof.
    split.
    - intros D. split; hnf; auto.
    - intros [D E] z [F|F]; subst; auto.
  Qed.

  Lemma incl_sing x A y :
    x::A <<= [y] -> x = y /\ A <<= [y].
  Proof.
    rewrite incl_lcons. intros [D E].
    apply in_sing in D. auto.
  Qed.

  Lemma incl_rcons x A B :
    A <<= x::B -> ~ x el A -> A <<= B.

  Proof. intros C D y E. destruct (C y E) as [F|F]. 1: congruence. assumption. Qed.

  Lemma incl_lrcons x A B :
    x::A <<= x::B -> ~ x el A -> A <<= B.

  Proof.
    intros C D y E.
    assert (F: y el x::B) by auto.
    destruct F as [F|F]; congruence.
  Qed.

  Lemma incl_app_left A B C :
    A ++ B <<= C -> A <<= C /\ B <<= C.
  Proof.
    firstorder.
  Qed.

End Inclusion.

Definition inclp (X : Type) (A : list X) (p : X -> Prop) : Prop :=
  forall x, x el A -> p x.


#[global]
Instance incl_preorder X :
  PreOrder (@incl X).
Proof.
  constructor; hnf; unfold incl; auto.
Qed.

#[global]
Instance equi_Equivalence X :
  Equivalence (@equi X).
Proof.
  constructor; hnf; firstorder.
Qed.

#[global]
Instance incl_equi_proper X :
  Proper (@equi X ==> @equi X ==> iff) (@incl X).
Proof.
  hnf. intros A B D. hnf. firstorder.
Qed.

#[global]
Instance cons_incl_proper X x :
  Proper (@incl X ==> @incl X) (@cons X x).
Proof.
  hnf. apply incl_shift.
Qed.

#[global]
Instance cons_equi_proper X x :
  Proper (@equi X ==> @equi X) (@cons X x).
Proof.
  hnf. firstorder.
Qed.

#[global]
Instance in_incl_proper X x :
  Proper (@incl X ==> Basics.impl) (@In X x).
Proof.
  intros A B D. hnf. auto.
Qed.

#[global]
Instance in_equi_proper X x :
  Proper (@equi X ==> iff) (@In X x).
Proof.
  intros A B D. firstorder.
Qed.

#[global]
Instance app_incl_proper X :
  Proper (@incl X ==> @incl X ==> @incl X) (@app X).
Proof.
  intros A B D A' B' E. auto.
Qed.

#[global]
Instance app_equi_proper X :
  Proper (@equi X ==> @equi X ==> @equi X) (@app X).
Proof.
  hnf. intros A B D. hnf. intros A' B' E.
  destruct D, E; auto.
Qed.

Section Equi.
  Variable X : Type.
  Implicit Types A B : list X.

  Lemma equi_push x A :
    x el A -> A === x::A.
  Proof.
    auto.
  Qed.

  Lemma equi_dup x A :
    x::A === x::x::A.

  Proof.
    auto.
  Qed.

  Lemma equi_swap x y A:
    x::y::A === y::x::A.
  Proof.
    split; intros z; cbn; tauto.
  Qed.

  Lemma equi_shift x A B :
    x::A++B === A++x::B.
  Proof.
    split; intros y.
    - intros [D|D].
      + subst; auto.
      + apply in_app_iff in D as [D|D]; auto.
    - intros D. apply in_app_iff in D as [D|D].
      + auto.
      + destruct D; subst; auto.
  Qed.

  Lemma equi_rotate x A :
    x::A === A++[x].
  Proof.
    split; intros y; cbn.
    - intros [D|D]; subst; auto.
    - intros D. apply in_app_iff in D as [D|D].
      + auto.
      + apply in_sing in D. auto.
  Qed.

End Equi.

Lemma in_concat_iff A l (a:A) : a el concat l <-> exists l', a el l' /\ l' el l.
Proof.
  induction l; cbn.
  - intuition. now destruct H.
  - rewrite in_app_iff, IHl. firstorder subst. auto.
Qed.

Lemma app_comm_cons' (A : Type) (x y : list A) (a : A) :
  x ++ a :: y = (x ++ [a]) ++ y.
Proof. rewrite <- app_assoc. cbn. trivial. Qed.


Lemma skipn_nil (X : Type) (n : nat) : skipn n nil = @nil X.
Proof. destruct n; cbn; auto. Qed.

Lemma skipn_app (X : Type) (xs ys : list X) (n : nat) :
  n = (| xs |) ->
  skipn n (xs ++ ys) = ys.
Proof.
  intros ->. revert ys. induction xs; cbn; auto.
Qed.

Lemma skipn_length (X : Type) (n : nat) (xs : list X) :
  length (skipn n xs) = length xs - n.
Proof.
  revert xs. induction n; intros; cbn.
  - lia.
  - destruct xs; cbn; auto.
Qed.


Lemma map_repeat (X Y : Type) (f : X -> Y) (n : nat) (a : X) :
  map f (repeat a n) = repeat (f a) n.
Proof. induction n; cbn in *; f_equal; auto. Qed.

Lemma repeat_add_app (X : Type) (m n : nat) (a : X) :
  repeat a (m + n) = repeat a m ++ repeat a n.
Proof. induction m; cbn; f_equal; auto. Qed.

Lemma repeat_S_cons (X : Type) (n : nat) (a : X) :
  a :: repeat a n = repeat a n ++ [a].
Proof.
  replace (a :: repeat a n) with (repeat a (S n)) by trivial. replace (S n) with (n+1) by lia.
  rewrite repeat_add_app. cbn. trivial.
Qed.

Lemma repeat_app_eq (X : Type) (m n : nat) (a : X) :
  repeat a n ++ repeat a m = repeat a m ++ repeat a n.
Proof. rewrite <- !repeat_add_app. f_equal. lia. Qed.

Lemma repeat_eq_iff (X : Type) (n : nat) (a : X) x :
  x = repeat a n <-> length x = n /\ forall y, y el x -> y = a.
Proof.
  split.
  {
    intros ->. split. apply repeat_length. apply repeat_spec.
  }
  {
    revert x. induction n; intros x (H1&H2); cbn in *.
    - destruct x; cbn in *; congruence.
    - destruct x; cbn in *; inv H1. f_equal.
      + apply H2. auto.
      + apply IHn. auto.
  }
Qed.

Lemma rev_repeat (X : Type) (n : nat) (a : X) :
  rev (repeat a n) = repeat a n.
Proof.
  apply repeat_eq_iff. split.
  - rewrite rev_length. rewrite repeat_length. auto.
  - intros y Hx % in_rev. eapply repeat_spec; eauto.
Qed.

Lemma concat_repeat_repeat (X : Type) (n m : nat) (a : X) :
  concat (repeat (repeat a n) m) = repeat a (m*n).
Proof.
  induction m as [ | m' IHm]; cbn.
  - auto.
  - rewrite repeat_add_app. f_equal. auto.
Qed.

Corollary skipn_repeat_add (X : Type) (n m : nat) (a : X) :
  skipn n (repeat a (n + m)) = repeat a m.
Proof.
  rewrite repeat_add_app. erewrite skipn_app; eauto. symmetry. apply repeat_length.
Qed.

Corollary skipn_repeat (X : Type) (n : nat) (a : X) :
  skipn n (repeat a n) = nil.
Proof.
  rewrite <- (app_nil_r (repeat a n)). erewrite skipn_app; eauto. symmetry. apply repeat_length.
Qed.

Lemma rev_eq_nil (Z: Type) (l: list Z) :
  rev l = nil -> l = nil.
Proof. intros. destruct l; cbn in *. reflexivity. symmetry in H. now apply app_cons_not_nil in H. Qed.

Lemma map_eq_nil (Y Z: Type) (f: Y->Z) (l: list Y) :
  map f l = nil -> l = nil.
Proof. intros. destruct l; cbn in *. reflexivity. congruence. Qed.

Lemma map_eq_nil' (Y Z: Type) (f: Y->Z) (l: list Y) :
  nil = map f l -> l = nil.
Proof. now intros H % eq_sym % map_eq_nil. Qed.

Lemma map_eq_cons (A B: Type) (f: A->B) (xs: list A) (y: B) (ys: list B) :
  map f xs = y :: ys ->
  exists x xs', xs = x :: xs' /\
          y = f x /\
          ys = map f xs'.
Proof. induction xs; intros H; cbn in *; inv H; eauto. Qed.

Lemma map_eq_cons' (A B: Type) (f: A -> B) (xs: list A) (y: B) (ys: list B) :
  y :: ys = map f xs ->
  exists x xs', xs = x :: xs' /\
          y = f x /\
          ys = map f xs'.
Proof. now intros H % eq_sym % map_eq_cons. Qed.

Lemma map_eq_app (A B: Type) (f: A -> B) (ls : list A) (xs ys : list B) :
  map f ls = xs ++ ys ->
  exists ls1 ls2, ls = ls1 ++ ls2 /\
             xs = map f ls1 /\
             ys = map f ls2.
Proof.
  revert xs ys. induction ls; intros; cbn in *.
  - symmetry in H. apply app_eq_nil in H as (->&->). exists nil, nil. cbn. tauto.
  - destruct xs; cbn in *.
    + exists nil. eexists. repeat split. cbn. now subst.
    + inv H. specialize IHls with (1 := H2) as (ls1&ls2&->&->&->).
      repeat econstructor. 2: instantiate (1 := a :: ls1). all: reflexivity.
Qed.

Lemma rev_eq_cons (A: Type) (ls: list A) (x : A) (xs: list A) :
  rev ls = x :: xs ->
  ls = rev xs ++ [x].
Proof. intros H. rewrite <- rev_involutive at 1. rewrite H. cbn. reflexivity. Qed.

Lemma map_injective (X Y: Type) (f: X -> Y) :
  (forall x y, f x = f y -> x = y) ->
  forall xs ys, map f xs = map f ys -> xs = ys.
Proof.
  intros HInj. hnf. intros x1. induction x1 as [ | x x1' IH]; intros; cbn in *.
  - now apply map_eq_nil' in H.
  - now apply map_eq_cons' in H as (l1&l2&->&->%HInj&->%IH).
Qed.

#[global]
Instance map_ext_proper A B: Proper (@ pointwise_relation A B (@eq B) ==> (@eq (list A)) ==> (@eq (list B))) (@map A B).
Proof.
  intros f f' Hf a ? <-. induction a;cbn;congruence.
Qed.


Lemma tl_map (A B: Type) (f: A -> B) (xs : list A) :
  tl (map f xs) = map f (tl xs).
Proof. now destruct xs; cbn. Qed.


Lemma tl_app (A: Type) (xs ys : list A) :
  xs <> nil ->
  tl (xs ++ ys) = tl xs ++ ys.
Proof. destruct xs; cbn; congruence. Qed.

Lemma tl_rev (A: Type) (xs : list A) :
  tl (rev xs) = rev (removelast xs).
Proof.
  induction xs; cbn; auto.
  destruct xs; cbn in *; auto.
  rewrite tl_app; cbn in *.
  - now rewrite IHxs.
  - intros (H1&H2) % app_eq_nil; inv H2.
Qed.

Lemma hd_map (A B: Type) (f: A -> B) (xs : list A) (a : A) :
  hd (f a) (map f xs) = f (hd a xs).
Proof. destruct xs; cbn; auto. Qed.

Lemma hd_app (A: Type) (xs ys : list A) a :
  xs <> nil ->
  hd a (xs ++ ys) = hd a xs.
Proof. intros H. destruct xs; auto. now contradiction H. Qed.

Lemma hd_rev (A: Type) (xs : list A) (a : A) :
  hd a (rev xs) = last xs a.
Proof.
  induction xs; cbn; auto.
  destruct xs; cbn; auto.
  rewrite hd_app. now apply IHxs.
  intros (H1&H2)%app_eq_nil; inv H2.
Qed.