Require Import Arith Lia List Permutation Relations.

From Undecidability.Shared.Libs.DLW.Utils
  Require Import utils_tac utils_list.

Set Implicit Arguments.

Local Infix "~p" := (@Permutation _) (at level 70, no associativity).

Section incl.

  Variable X : Type.

  Implicit Type l : list X.

  Fact incl_cons_linv l m x : incl (x::m) l In x l incl m l.
  Proof.
    intros H; split.
    + apply H; left; auto.
    + intros ? ?; apply H; right; auto.
  Qed.


  Fact incl_app_rinv l m p : incl m (lp) m1 m2, m p incl l incl p.
  Proof.
    induction m as [ | x m IHm ].
    + exists nil, nil; simpl; repeat split; auto; intros ? [].
    + intros H.
      apply incl_cons_linv in H.
      destruct H as ( & ).
      destruct (IHm ) as ( & & & & ).
      apply in_app_or in ; destruct .
      * exists (x::), ; repeat split; auto.
        - constructor 2; auto.
        - intros ? [|]; subst; auto.
      * exists , (x::); repeat split; auto.
        - apply Permutation_cons_app; auto.
        - intros ? [|]; subst; auto.
  Qed.


  Fact incl_cons_rinv x l m : incl m (x::l) m1 m2, m p Forall (eq x) incl l.
  Proof.
    intros H.
    apply (@incl_app_rinv (x::nil) _ l) in H.
    destruct H as ( & & & & ).
    exists , ; repeat split; auto.
    rewrite Forall_forall.
    intros a Ha; apply in Ha; destruct Ha as [ | [] ]; auto.
  Qed.


  Fact incl_right_cons_choose x l m : incl m (x::l) In x m incl m l.
  Proof.
    intros H.
    apply incl_cons_rinv in H.
    destruct H as ( & & & & ); simpl in .
    destruct as [ | y ].
    + right.
      intros u H; apply ; revert H.
      apply Permutation_in; auto.
    + left.
      apply Permutation_in with (1 := Permutation_sym ).
      rewrite Forall_forall in .
      rewrite ( y); left; auto.
  Qed.


  Fact incl_left_right_cons x l y m : incl (x::l) (y::m) y = x In y l
                                                          y = x incl l m
                                                          In x m incl l (y::m).
  Proof.
    intros H; apply incl_cons_linv in H.
    destruct H as [ [|] ]; auto.
    apply incl_right_cons_choose in ; tauto.
  Qed.


  Fact perm_incl_left m1 m2 l: p incl l incl l.
  Proof. intros ? H. apply ; revert H; apply Permutation_in; auto. Qed.

  Fact perm_incl_right m l1 l2: p incl m incl m .
  Proof.
    intros ? ?; apply Permutation_in with (1 := ), ; auto.
  Qed.


End incl.

Section Permutation_tools.

  Variable X : Type.

  Implicit Types (l : list X).

  Theorem Permutation_In_inv l1 l2: p x, In x l, r, = lx::r.
  Proof. intros H ? ?; apply in_split, Permutation_in with (1 := H); auto. Qed.

  Fact perm_in_head x l : In x l m, l p x::m.
  Proof.
    induction l as [ | y l IHl ].
    + destruct 1.
    + intros [ ? | H ]; subst.
      * exists l; apply Permutation_refl.
      * destruct (IHl H) as (m & Hm).
        exists (y::m).
        apply Permutation_trans with (2 := perm_swap _ _ _).
        constructor 2; auto.
  Qed.


End Permutation_tools.

Section pigeon_list.

  Variable (X : Type).

  Implicit Types (l m : list X).

  Inductive list_has_dup : list X Prop :=
    | in_list_hd0 : l x, In x l list_has_dup (x::l)
    | in_list_hd1 : l x, list_has_dup l list_has_dup (x::l).

  Fact list_hd_cons_inv x l : list_has_dup (x::l) In x l list_has_dup l.
  Proof. inversion 1; subst; auto. Qed.

  Definition list_has_dup_cons_inv := list_hd_cons_inv.

  Fact list_has_dup_app_left l m : list_has_dup m list_has_dup (lm).
  Proof. induction l; simpl; auto; constructor 2; auto. Qed.

  Fact list_has_dup_app_right l m : list_has_dup l list_has_dup (lm).
  Proof.
    induction 1; simpl.
    + constructor 1; apply in_or_app; left; auto.
    + constructor 2; auto.
  Qed.


  Fact perm_list_has_dup l m : l p m list_has_dup l list_has_dup m.
  Proof.
    induction 1 as [ | x l m | x y l | ]; auto;
      intros H; apply list_hd_cons_inv in H.
    + destruct H as [ H | H ].
      * apply Permutation_in with (1 := ) in H.
        apply in_list_hd0; auto.
      * apply in_list_hd1; auto.
    + destruct H as [ [ H | H ] | H ]; subst.
      * apply in_list_hd0; left; auto.
      * apply in_list_hd1, in_list_hd0; auto.
      * apply list_hd_cons_inv in H.
        destruct H as [ H | H ].
        - apply in_list_hd0; right; auto.
        - do 2 apply in_list_hd1; auto.
  Qed.


  Fact list_has_dup_app_inv l m : list_has_dup (lm) list_has_dup l
                                                       list_has_dup m
                                                       x, In x l In x m.
  Proof.
    induction l as [ | x l IHl ]; simpl; intros H; auto.
    apply list_hd_cons_inv in H.
    + destruct H as [ H | H ].
      * apply in_app_or in H; destruct H as [ H | H ].
        - left; constructor; auto.
        - do 2 right; exists x; simpl; auto.
      * destruct (IHl H) as [ | [ | (y & & ) ] ]; auto.
        - left; constructor 2; auto.
        - do 2 right; exists y; simpl; auto.
  Qed.


  Fact list_has_dup_eq_duplicates m: list_has_dup m x aa bb cc, m = aax::bbx::cc.
  Proof.
    split.
    + induction 1 as [ m x Hm | m x _ IHm ].
      - apply in_split in Hm.
        destruct Hm as (bb & cc & Hm).
        exists x, nil, bb, cc; subst; auto.
      - destruct IHm as (y & aa & bb & cc & IHm).
        exists y, (x::aa), bb, cc; subst; auto.
    + intros (x & aa & bb & cc & Hm).
      subst m.
      apply list_has_dup_app_left.
      constructor 1; apply in_or_app; right.
      constructor 1; reflexivity.
  Qed.


  Definition list_has_dup_equiv := list_has_dup_eq_duplicates.

  Fact repeat_choice_two x m : Forall (eq x) m ( m', m = x::x::m') m = nil m = x::nil.
  Proof.
    intros H.
    destruct m as [ | a [ | b m ] ]; auto.
    + inversion H; subst; auto.
    + rewrite Forall_forall in H.
      rewrite (H a), (H b); simpl; auto; left; exists m; auto.
  Qed.



  Fact incl_right_cons_incl_or_lhd_or_perm m x l :
       incl m (x::l) incl m l
                      list_has_dup m
                      m', m p x::m' incl m' l.
  Proof.
    intros H.
    apply incl_cons_rinv in H.
    destruct H as ( & & & & ).
    destruct (repeat_choice_two ) as [ (?&?) | [|] ];
      subst ; simpl in ; clear .
    + right; left; apply perm_list_has_dup with (1 := Permutation_sym ), in_list_hd0; left; auto.
    + left; revert ; apply perm_incl_left.
    + firstorder.
  Qed.


  Fact incl_left_right_php x l y m : incl (y::m) (x::l) list_has_dup (y::m)
                                                         x = y incl m l
                                                         In y l incl m l
                                                         In y l m', m p x::m' incl m' l.
  Proof.
    intros H; apply incl_left_right_cons in H.
    destruct H as [ (? & ?) | [ (? & ?) | ( & ) ] ]; subst; auto.
    + left; apply in_list_hd0; auto.
    + apply incl_right_cons_incl_or_lhd_or_perm in ; firstorder.
      left; apply in_list_hd1; auto.
  Qed.




  Lemma length_le_and_incl_implies_dup_or_perm l m :
            length l length m
          incl m l
          list_has_dup m m p l.
  Proof.
    revert m; induction l as [ | x l IHl ]; intros m; simpl; intros ; auto.
    + destruct m as [ | y ]; auto; destruct ( y); simpl; auto.
    + destruct incl_right_cons_incl_or_lhd_or_perm with (1 := )
        as [ | [ | (m' & & ) ] ]; auto.
      * destruct IHl with (2 := ) as [ | H ]; try ; auto.
        apply Permutation_length in H; .
      * destruct IHl with (2 := ) as [ H | H ]; try (simpl; ).
        - apply Permutation_length in ; simpl in ; .
        - left; apply perm_list_has_dup with (1 := Permutation_sym ).
          constructor 2; auto.
        - right; apply perm_trans with (1 := ); auto.
  Qed.



  Theorem finite_php_dup l m : length l < length m
                             incl m l
                             list_has_dup m.
  Proof.
    intros .
    destruct (@length_le_and_incl_implies_dup_or_perm l m) as [ | ]; auto; try .
    apply Permutation_length in ; .
  Qed.



  Theorem finite_pigeon_hole l m :
         length l < length m
       incl m l
       x aa bb cc, m = aax::bbx::cc.
  Proof.
    intros; apply list_has_dup_eq_duplicates, finite_php_dup with l; auto.
  Qed.


  Theorem partition_intersection l m k :
           length k < length (lm)
         incl (lm) k
         list_has_dup l
         list_has_dup m
         x, In x l In x m.
  Proof.
    intros .
    apply list_has_dup_app_inv, list_has_dup_eq_duplicates.
    revert ; apply finite_pigeon_hole.
  Qed.


End pigeon_list.

Fact not_list_has_dup_an a n : list_has_dup (list_an a n).
Proof.
  revert a; induction n as [ | n IHn ]; simpl; intros a H.
  + inversion H.
  + apply list_hd_cons_inv in H.
    rewrite list_an_spec in H.
    destruct H as [ | H ]; try .
    revert H; apply IHn.
Qed.


Fact list_has_dup_map_inv X Y (f : X Y) l :
           ( x y, In x l In y l f x = f y x = y)
         list_has_dup (map f l)
         list_has_dup l.
Proof.
  intros H; do 2 rewrite list_has_dup_eq_duplicates.
  intros (y & & & & E).
  apply map_app_inv in E; destruct E as ( & & & & ); symmetry in .
  apply map_cons_inv in ; destruct as ( & & & & ).
  apply map_app_inv in ; destruct as ( & & & & ); symmetry in .
  apply map_cons_inv in ; destruct as ( & & & & ); subst.
  apply H in ; subst.
  + exists , , , ; auto.
  + apply in_or_app; right; right; simpl.
    apply in_or_app; simpl; auto.
  + apply in_or_app; simpl; auto.
Qed.


Fact not_list_an_has_dup a n : list_has_dup (list_an a n).
Proof.
  revert a; induction n as [ | n IHn ]; simpl; intros a H.
  + inversion H.
  + apply list_hd_cons_inv in H.
    rewrite list_an_spec in H.
    destruct H as [ | H ]; try .
    revert H; apply IHn.
Qed.


Fact list_exists X Y (R : X Y Prop) l : ( x, In x l y, R x y) ll, R l ll.
Proof.
  induction l as [ | x l IHl ]; intros Hl.
  exists nil; constructor.
  destruct (Hl x) as (y & Hy).
  left; auto.
  destruct IHl as (ll & Hll).
  intros; apply Hl; right; auto.
  exists (y::ll); constructor; auto.
Qed.


Fact Forall2_conj X Y (R S : X Y Prop) ll mm : ( x y R x y S x y) ll mm R ll mm S ll mm.
Proof.
  split.
  induction 1; split; constructor; tauto.
  intros [ ]; revert .
  induction 1 as [ | x ll y mm IH ]; intros H; auto.
  apply Forall2_cons_inv in H; constructor; tauto.
Qed.


Fact Forall2_length X Y (R : X Y Prop) l m : R l m length l = length m.
Proof. induction 1; simpl; f_equal; auto. Qed.

Fact Forall2_impl X Y (R S : X Y Prop) :
     ( x y, R x y S x y) l m, R l m S l m.
Proof. induction 2; constructor; auto. Qed.

Fact Forall2_right_Forall X Y (P : Y Prop) lx ly : ( (_ : X) y P y) lx ly Forall P ly length lx = length ly.
Proof.
  split.
  intros H; split.
  induction H; constructor; auto.
  revert H; apply Forall2_length.
  intros ( & ); revert lx .
  induction ; intros [ | ] ; try discriminate ; constructor; auto.
Qed.


Fact Forall2_app_inv_r X Y R l m1 m2 :
       @ X Y R l ()
     { l1 : _ & { l2 | R R l = } }.
Proof.
  revert l;
  induction as [ | y IH ]; simpl; intros l H.
  exists nil, l; repeat split; auto.
  destruct l as [ | x l ].
  apply Forall2_nil_inv_l in H; discriminate H.
  apply Forall2_cons_inv in H; destruct H as [ ].
  apply IH in .
  destruct as ( & & & & ); subst l.
  exists (x::), ; repeat split; auto.
Qed.


Section PHP_rel.

  Variable (U V : Type) (R : U V Prop) (l : list U) (m : list V)
                        (HR : x, In x l y, In y m R x y).

  Let image_R_l : Rl, incl Rl m R l Rl.
  Proof.
    destruct (list_exists _ l HR) as (Rl & HRl).
    exists Rl; split.
    + clear HR.
      rewrite Forall2_conj in HRl.
      apply proj1, Forall2_right_Forall, proj1 in HRl.
      rewrite Forall_forall in HRl; auto.
    + revert HRl; apply Forall2_impl; tauto.
  Qed.


  Hypothesis (Hlm : length m < length l).


  Theorem PHP_rel : a x b y c v, l = ax::by::c
                                        In v m R x v R y v.
  Proof.
    destruct image_R_l as (Rl & & ).
    destruct finite_pigeon_hole with (2 := ) as (v & x & y & z & H).
    + apply Forall2_length in ; .
    + subst Rl.
      apply Forall2_app_inv_r in ; destruct as (x' & & & & ?); subst.
      apply Forall2_cons_inv_r in ; destruct as (v' & & & ? & ); subst.
      apply Forall2_app_inv_r in ; destruct as (y' & & & & ?); subst.
      apply Forall2_cons_inv_r in ; destruct as (v'' & & & ? & ); subst.
      exists x', v', y', v'', , v; repeat (split; auto).
      apply , in_or_app; simpl; auto.
  Qed.


End PHP_rel.

Section php_upto.


  Theorem php_upto X (R : X X Prop) (l m : list X) :
            symmetric _ R transitive _ R
          ( x, In x l y, In y m R x y)
          length m < length l
          a x b y c, l = ax::by::c R x y.   Proof.
    intros .
    destruct PHP_rel with (R := R) (2 := )
      as (a & x & b & y & c & z & & & & ); auto.
    exists a, x, b, y, c; split; auto.
    apply ( _ z); auto.
  Qed.


End php_upto.