Require Import subsequences.
Require Import Sorting.Permutation.

Require Import Nat.
Require Import PeanoNat.
Require Import List.


Import ListNotations.



Definition permutation_mapping {X: Type} (u v base : list X) :=
  exists p l, Permutation base p
  /\ map Some u = map (nth_error base) l
  /\ map Some v = map (nth_error p) l.





(*

Definition incl_without_eq {X: Type} (u v : list X) :=
  exists l, map Some u = map (nth_error v) l.

Lemma incl_without_eq_incl {X: Type}:
  forall (u v : list X), incl_without_eq u v -> incl u v.
Proof.
  intro u. induction u; intro v; intro H. easy. destruct H.
  destruct x. symmetry in H. apply nil_cons in H. contradiction.
  inversion H. apply incl_cons.
  symmetry in H1. apply nth_error_In in H1. assumption.
  apply IHu. exists x. assumption.
Qed.


Lemma incl_incl_without_eq {X: Type}:
  forall (u v : list X), incl u v -> incl_without_eq u v.
Proof.
  intro u. induction u; intro v; intro H. exists nil. easy.
  apply incl_cons_inv in H. destruct H. apply IHu in H0. destruct H0.
  apply In_nth_error in H. destruct H. exists (x0 :: x).
  simpl. rewrite H. rewrite H0. reflexivity.
Qed.
 *)


Lemma permutation_mapping_self {X: Type} :
  forall (u base : list X), incl u base -> permutation_mapping u u base.
Proof.
  intro u. induction u; intro base; intro H; exists base.
  exists nil. split; easy. apply incl_cons_inv in H. destruct H.
  apply IHu in H0. destruct H0. destruct H0. destruct H0. destruct H1.
  apply In_nth_error in H. destruct H. exists (x1 :: x0).
  split. easy. split; simpl; rewrite H; rewrite H1; reflexivity.
Qed.


Lemma permutation_mapping_length {X: Type} :
  forall (u v base : list X),
  permutation_mapping u v base -> length u = length v.
Proof.
  intros u v base. intro H. destruct H. destruct H. destruct H. destruct H0.
  replace (length u) with (length (map Some u)). rewrite H0.
  replace (length v) with (length (map Some v)). rewrite H1.
  rewrite map_length. rewrite map_length. reflexivity.
  apply map_length. apply map_length.
Qed. 






(*
Lemma permutation_mapping_base {X: Type} :
  forall (u v base p: list X),
    Permutation base p -> permutation_mapping u v base
      -> permutation_mapping u v p.
Proof.
  intros u v base p.

  (* destruct u in order to get a value of type X when needed *)
  destruct u. intros I H. destruct H. destruct H. destruct H. destruct H0.
  symmetry in H0. apply map_eq_nil in H0. rewrite H0 in H1.
  exists base. exists nil. split. easy. rewrite H1. split; easy.

  intros H I. assert (K := H).

  destruct I as [p']. destruct H0 as [l]. destruct H0.
  destruct H1.

  rewrite Permutation_nth in H. destruct H.
  destruct H3 as [f]. destruct H3. destruct H4.
  apply FinFun.bInjective_bSurjective in H4.
  apply FinFun.bSurjective_bBijective in H4. destruct H4 as [g].
  destruct H4.



  exists base. exists (map g l). split.
  apply Permutation_trans with (l' := base). apply Permutation_sym.
  assumption. apply Permutation_refl. split.

  (* first case in split *)
  rewrite H1.

  assert (forall s, (forall y, In y s -> y < length base)
    -> map (nth_error base) s = map (nth_error p) (map g s)).
  intro s. induction s; intro L. reflexivity.
  assert (M: a < length base). apply L. apply in_eq.

  simpl. rewrite IHs.
  rewrite nth_error_nth' with (d := x).
  rewrite nth_error_nth' with (d := x).
  replace a with (f (g a)) at 1.
  rewrite <- H5. reflexivity.
  apply H4. assumption.
  apply H6 in M. destruct M. assumption.
  rewrite H. apply H4. assumption. assumption.
  intro y. intro N. apply L. apply in_cons. assumption.

  apply H7. intro y. intro N.

  assert (forall s z, In z s -> nth_error base z <> None -> z < length base).
  intros s z. intros M1 M2. apply nth_error_Some. assumption.
  apply H8 with (s := l). assumption.

  assert (forall s (t: list X),
    map Some t = map (nth_error base) s
    -> In y s -> nth_error base y <> None).
  intro s. induction s; intros t; intros M1 M2.
  apply in_nil in M2. contradiction.
  apply in_inv in M2. destruct M2. rewrite H9 in M1.
  destruct t. inversion M1. inversion M1. easy.
  destruct t. inversion M1. inversion M1.
  apply IHs with (t := t). assumption. assumption.
  generalize N. generalize H1. apply H9.

  (* second case in split *)
  rewrite H2.

  assert (forall s, (forall y, In y s -> y < length base)
    -> map (nth_error p') s = map (nth_error base) (map g s)).
  intro s. induction s; intro R. reflexivity.
  simpl. rewrite IHs.

  rewrite nth_error_nth' with (d := x).
  rewrite nth_error_nth' with (d := x).
  replace a with (g (f a)) at 1.
  rewrite <- H5. reflexivity.
  apply H4. assumption.
  apply H6 in M. destruct M. assumption.
  rewrite H. apply H4. assumption. assumption.
  intro y. intro N. apply L. apply in_cons. assumption.

  apply H7. intro y. intro N.

  assert (forall s z, In z s -> nth_error base z <> None -> z < length base).
  intros s z. intros M1 M2. apply nth_error_Some. assumption.
  apply H8 with (s := l). assumption.

  assert (forall s (t: list X),
    map Some t = map (nth_error base) s
    -> In y s -> nth_error base y <> None).
  intro s. induction s; intros t; intros M1 M2.
  apply in_nil in M2. contradiction.
  apply in_inv in M2. destruct M2. rewrite H9 in M1.
  destruct t. inversion M1. inversion M1. easy.
  destruct t. inversion M1. inversion M1.
  apply IHs with (t := t). assumption. assumption.
  generalize N. generalize H1. apply H9.




















  exists p'. exists (map g l). split.
  apply Permutation_trans with (l' := base). apply Permutation_sym.
  assumption. assumption. split.

  (* first case in split *)
  rewrite H1.

  assert (forall s, (forall y, In y s -> y < length base)
    -> map (nth_error base) s = map (nth_error p) (map g s)).
  intro s. induction s; intro L. reflexivity.
  assert (M: a < length base). apply L. apply in_eq.

  simpl. rewrite IHs.
  rewrite nth_error_nth' with (d := x).
  rewrite nth_error_nth' with (d := x).
  replace a with (f (g a)) at 1.
  rewrite <- H5. reflexivity.
  apply H4. assumption.
  apply H6 in M. destruct M. assumption.
  rewrite H. apply H4. assumption. assumption.
  intro y. intro N. apply L. apply in_cons. assumption.

  apply H7. intro y. intro N.

  assert (forall s z, In z s -> nth_error base z <> None -> z < length base).
  intros s z. intros M1 M2. apply nth_error_Some. assumption.
  apply H8 with (s := l). assumption.

  assert (forall s (t: list X),
    map Some t = map (nth_error base) s
    -> In y s -> nth_error base y <> None).
  intro s. induction s; intros t; intros M1 M2.
  apply in_nil in M2. contradiction.
  apply in_inv in M2. destruct M2. rewrite H9 in M1.
  destruct t. inversion M1. inversion M1. easy.
  destruct t. inversion M1. inversion M1.
  apply IHs with (t := t). assumption. assumption.
  generalize N. generalize H1. apply H9.

  (* second case in split *)
  rewrite H2.

  apply FinFun.bInjective_bSurjective in H3.
  apply FinFun.bSurjective_bBijective in H3. destruct H3 as [g].
  destruct H3.

  assert (forall s, (forall y, In y s -> y < length base)
    -> map (nth_error base) s = map (nth_error p) (map f s)).
  intro s. induction s; intro K. reflexivity.
  simpl. rewrite IHs.

  rewrite map_map.
  rewrite nth_error_nth' with (d := x).
  rewrite nth_error_nth' with (d := x).

  (*
  assert (a < length base). apply K. apply in_eq.
  assert (N := H6). apply H5 in N. destruct N.
   *)
  replace a with (f (g a)) at 1. rewrite H4.


  assert (exists b, b < length base /\ a = g b).
  exists (f a).



  rewrite <- H4. reflexivity. apply K.
  apply in_eq. apply H2. apply K.
  apply in_eq. rewrite H. apply K.
  apply in_eq. intro y. intro L. apply K. apply in_cons. assumption.
  apply H5. intro y. intro L.






 *)

Lemma permutation_mapping_swap {X: Type} :
  forall (u v base : list X),
  permutation_mapping u v base -> permutation_mapping v u base.
Proof.
  intros u v base.

  (* destruct u in order to get a value of type X when needed *)
  destruct u. intro H. destruct H. destruct H. destruct H. destruct H0.
  symmetry in H0. apply map_eq_nil in H0. rewrite H0 in H1.
  exists base. exists nil. split. easy. rewrite H1. split; easy.

  intro H. destruct H as [p]. destruct H as [l].
  destruct H. destruct H0. assert (I := H). rewrite Permutation_nth in H.
  destruct H. destruct H2 as [f]. destruct H2. destruct H3.
  apply FinFun.bInjective_bSurjective in H3.
  apply FinFun.bSurjective_bBijective in H3.
  destruct H3 as [g]. destruct H3.

  exists (map (fun e => nth e base x) (map g (seq 0 (length base)))).
  exists (map f l). split.

  replace base with (map (fun e => nth e base x) (seq 0 (length base))) at 1.
  apply Permutation_map. apply NoDup_Permutation_bis.
  apply seq_NoDup. rewrite map_length. rewrite seq_length. easy.
  intro a. intro J.

  assert (a < 0 + length base). apply in_seq. assumption.

  assert (forall x n h h', FinFun.bFun n h -> FinFun.bFun n h'
    -> (forall y, y < n -> h (h' y) = y /\ h' (h y) = y)
    -> x < n -> In x (map h (seq 0 n))).
  intros x' n h h'. intros J1 J2 J3 J4. replace x' with (h (h' x')) at 1.
  apply in_map. rewrite in_seq. split. apply le_0_n. apply J2. assumption.
  apply J3 in J4. destruct J4. assumption. apply H7 with (h' := f); assumption.

  assert (forall (b: list X),
    map (fun e : nat => nth e b x) (seq 0 (length b)) = b).
  intro b. induction b. reflexivity.
  
  replace (seq 0 (length (a :: b))) with (0:: map S (seq 0 (length b))).
  rewrite map_cons. rewrite map_map.

  assert (map (fun e : nat => nth e b x) (seq 0 (length b))
    = map (fun x0 : nat => nth (S x0) (a :: b) x) (seq 0 (length b))).
  destruct b. reflexivity. reflexivity.
  rewrite <- H6. rewrite IHb. reflexivity.
  rewrite seq_shift. rewrite cons_seq. reflexivity. apply H6.

  split.

  (* first case in split *)
  rewrite H1.

  assert (forall s, (forall y, In y s -> y < length base)
    -> map (nth_error p) s = map (nth_error base) (map f s)).
  intro s. induction s; intro K. reflexivity. simpl. rewrite IHs.
  rewrite nth_error_nth' with (d := x). rewrite nth_error_nth' with (d := x).
  rewrite <- H4. reflexivity. apply K. apply in_eq. apply H2. apply K.
  apply in_eq. rewrite H. apply K. apply in_eq. intro y. intro L. apply K.
  apply in_cons. assumption. apply H6. intro y. intro L.

  assert (forall s z, In z s -> nth_error base z <> None -> z < length base).
  intros s z. intros M1 M2. apply nth_error_Some. assumption.
  apply H7 with (s := l). assumption.

  assert (forall s (t: list X),
    map Some t = map (nth_error base) s -> In y s -> nth_error base y <> None).
  intro s. induction s; intros t; intros M1 M2.
  apply in_nil in M2. contradiction.
  apply in_inv in M2. destruct M2. rewrite H8 in M1.
  destruct t; inversion M1; easy.
  destruct t; inversion M1; apply IHs with (t := t); assumption.
  generalize L. generalize H0. apply H8.

  (* second case in split *)
  rewrite H0.

  (*
  apply FinFun.bInjective_bSurjective in H3.
  apply FinFun.bSurjective_bBijective in H3. destruct H3 as [g].
  destruct H3.
   *)

  assert (forall s, (forall y, In y s -> y < length base)
    -> map (nth_error base) s
      = map (nth_error (map (fun e => nth (g e) base x) (seq 0 (length base)))) (map f s)).
  intro s. rewrite map_map. induction s; intro K. reflexivity.
  simpl. rewrite IHs.

  rewrite nth_error_nth' with (d := x).
  replace (nth_error (map (fun e : nat => nth (g e) base x)
                          (seq 0 (length base))) (f a))
    with (Some ((fun e => nth (g e) base x)
                (nth (f a) (seq 0 (length base)) 0))).


  assert (forall m n f' g',
    FinFun.bFun m f' -> FinFun.bFun m g'
    -> (forall x : nat, x < m -> g' (f' x) = x /\ f' (g' x) = x)
    -> n < m -> g' (nth (f' n) (seq 0 m) 0) = n).
  intros m n f' g'. intros J J1 J2 J3.

  assert (forall q p, p < q -> nth p (seq 0 q) 0 = p).
  intro q. induction q; intro p'; intro J4.
  apply Nat.nlt_0_r in J4. contradiction.
  rewrite Nat.lt_succ_r in J4. rewrite Nat.le_lteq in J4. destruct J4.
  rewrite seq_S. rewrite app_nth1. apply IHq. assumption.
  rewrite seq_length. assumption. rewrite H6. rewrite seq_nth.
  reflexivity. apply Nat.lt_succ_diag_r. rewrite H6.
  apply J2 in J3. destruct J3. apply H7. apply J. assumption.

  rewrite H6. reflexivity. assumption. assumption. assumption.
  apply K. apply in_eq.
  rewrite nth_error_nth' with (d := x).

  replace (nth (f a) (ma
  rewrite <- map_nth at 1.









  assert (forall p q, p < q -> nth p (seq 0 q) 0 = p).
  intro p'. induction p'; intro q; intro J4.
  destruct q. apply Nat.nlt_0_r in J4. contradiction.
  reflexivity.


  intro m. induction m; intros n f' g'; intros J J1 J2 J3.
  apply Nat.nlt_0_r in J3. contradiction. simpl in J3.
  rewrite Nat.lt_succ_r in J3. rewrite Nat.le_lteq in J3. destruct J3.
  rewrite seq_S. rewrite app_nth1. apply IHm. assumption.
  rewrite seq_length. apply H2.

  replace (seq 0 (length (a0::b))) with (0 :: (seq 1 (length b))).
  rewrite cons_seq.



  prouver avec map_nth






  rewrite nth_error_nth' with (d := nth (g 0) base x).
  rewrite nth_error_nth' with (d := nth (g 0) base x).
  r
  replace (nth (g 0) base x) with ((fun e => nth (g e) base x) 0).
  rewrite nth_error_nth' with (d := (fun e => nth (g e) base x) 0).
  rewrite map_nth.
  rewrite nth_error_nth' with (d := x).

  rewrite nth_error_nth' with (d := (fun e => nth (g e) base x) 0).
  rewrite nth_error_nth' with (d := x).




  rewrite nth_error_nth' with (d := x).
  rewrite nth_error_nth' with (d := x).
  rewrite <- H4. reflexivity. apply K.
  apply in_eq. apply H2. apply K.
  apply in_eq. rewrite H. apply K.
  apply in_eq. intro y. intro L. apply K. apply in_cons. assumption.
  apply H6. intro y. intro L.

  assert (forall s z, In z s -> nth_error base z <> None -> z < length base).
  intros s z. intros M1 M2. apply nth_error_Some. assumption.
  apply H7 with (s := l). assumption.

  assert (forall s (t: list X),
    map Some t = map (nth_error base) s
    -> In y s -> nth_error base y <> None).
  intro s. induction s; intros t; intros M1 M2.
  apply in_nil in M2. contradiction.
  apply in_inv in M2. destruct M2. rewrite H8 in M1.
  destruct t. inversion M1. inversion M1. easy.
  destruct t. inversion M1. inversion M1.
  apply IHs with (t := t). assumption. assumption.
  generalize L. generalize H0. apply H8.






  assert (forall n, n < length base ->
    nth_error base n = nth_error (map (fun e => nth (g e) base x) (seq 0 (length base))) (f n)).
  intro n. induction n; intro M.
  destruct base. destruct (f 0); reflexivity.

  rewrite nth_error_nth' with (d := x).
  rewrite nth_error_nth' with (d := x).
  simpl.

  assert (forall b,
    nth_error (map (fun e => nth (g e) b x) (seq 0 (length b))) (f 0)
    = nth_error b 0).
  intro b. induction b. destruct (f 0); reflexivity.
  replace (seq 0 (length (a0::b))) with ((seq 0 (length b)) ++ [ length b ]).
  rewrite map_app.





  induction a. destruct base. destruct (f 0); reflexivity.
  destruct base. simpl.



  intro s. induction s; intro K. reflexivity.
  simpl. rewrite IHs.

  rewrite map_map.
  rewrite nth_error_nth' with (d := x).
  rewrite nth_error_nth' with (d := x).

  (*
  assert (a < length base). apply K. apply in_eq.
  assert (N := H6). apply H5 in N. destruct N.
   *)
  assert (a < length base). apply K. apply in_eq.
  replace a with (f (g a)) at 1. rewrite H4.


  assert (exists b, b < length base /\ a = g b).
  exists (f a). split. apply H2.
  assumption. apply H5 in H6. destruct H6. rewrite H6. reflexivity.










  base = [0,1,2,3]

  u = [0,1,2,3,0,1,2,3]   -->    l = [0,1,2,3,0,1,2,3]
  p = [2,3,1,0]
  v = [2,3,1,0,2,3,1,0]













  intro u. induction u; intros v base; intro H;
  destruct H; destruct H; destruct H; destruct H0.
  symmetry in H0. apply map_eq_nil in H0. rewrite H0 in H1.
  apply map_eq_nil in H1. rewrite H1. apply permutation_mapping_self. easy.
  rewrite Permutation_nth in H. destruct H. destruct H2 as [f].
  destruct H2. destruct H3.
  apply FinFun.bInjective_bSurjective in H3.
  apply FinFun.bSurjective_bBijective in H3. destruct H3 as [g].
  destruct H3.
  destruct v.
  symmetry in H1. apply map_eq_nil in H1. rewrite H1 in H0.
  apply map_eq_nil in H0. symmetry in H0. apply nil_cons in H0.
  contradiction.