Update

src/mapping.v

@@ -83,7 +83,65 @@ Proof.
 Qed.
 
 
+Lemma permutation_mapping_app {X: Type} :
+  forall (u1 u2 v1 v2 base : list X),
+    permutation_mapping (u1 ++ u2) (v1 ++ v2) base
+    -> length u1 = length v1 ->
+      permutation_mapping u1 v1 base /\ 
+      permutation_mapping u2 v2 base.
+Proof.
+  intros u1 u2 v1 v2 base. intros H I.
+  destruct H as [p]. destruct H as [l]. destruct H. destruct H0.
+  rewrite map_app in H0. rewrite map_app in H1.
 
+  assert (K: length u1 <= length (map (nth_error base) l)).
+  rewrite <- H0. rewrite app_length. rewrite map_length. apply Nat.le_add_r.
+  rewrite map_length in K.
+
+  rewrite <- firstn_skipn with (n := length u1) in H0.
+  rewrite <- firstn_skipn with (n := length u1) in H1.
+
+  assert (forall (a b c d: list (option X)),
+    a ++ b = c ++ d -> length a = length c -> a=c /\ b = d).
+  intro a. induction a; intros b c d; intros J1 J2. symmetry in J2.
+  rewrite length_zero_iff_nil in J2. rewrite J2. split. reflexivity.
+  rewrite J2 in J1. assumption.
+  destruct c. inversion J2.
+  split; inversion J1; apply IHa in H4; destruct H4.
+  rewrite H2. reflexivity. inversion J2. reflexivity.
+  assumption. inversion J2. reflexivity.
+    apply H2 in H0. apply H2 in H1.
+    destruct H0. destruct H1.
+
+  split; exists p.
+  - exists (firstn (length u1) l). split. assumption.
+    rewrite <- firstn_map. rewrite <- firstn_map.
+    split; assumption.
+  - exists (skipn (length u1) l). split. assumption.
+    rewrite <- skipn_map. rewrite <- skipn_map.
+    split; assumption.
+  - rewrite map_length. rewrite firstn_length_le. rewrite I. reflexivity.
+    rewrite map_length. assumption.
+  - rewrite map_length. rewrite firstn_length_le. rewrite I. reflexivity.
+    rewrite map_length. assumption.
+Qed.
+
+
+Lemma permutation_mapping_base_cons {X: Type} :
+  forall (u v base : list X) a,
+    permutation_mapping u v base -> permutation_mapping u v (a::base).
+Proof.
+  intros u v base a. intro H. destruct H as [p]. destruct H as [l].
+  destruct H. destruct H0. exists (a::p). exists (map S l).
+  split. apply perm_skip. assumption.
+
+  assert (forall x (y: list X),
+    map (nth_error (a :: y)) (map S x) = map (nth_error y) x).
+  intro x. induction x; intro y. reflexivity. simpl. rewrite IHx.
+  reflexivity.
+
+  split; rewrite H2; assumption.
+Qed.