coqbooks/src/mapping.v

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_swap {X: Type} :
  forall (u v base : list X),
  permutation_mapping u v base -> permutation_mapping v u base.
Proof.
  intro u. induction u; intros v base; intro H.