Update

src/mapping.v

@@ -285,7 +285,73 @@ Proof.
   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.
-  exists p. exists (map f l). split. assumption. split.
+  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. (* rewrite <- IHb at 2. *)
+  
+  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.
+
+
+
+
+
+
+
+
+
+
+
+
+
+  exists (map (fun e => (nth (g e) base x)) (seq 0 (length base))).
+  exists (map f l). split.
+
+
+
+
+  apply Permutation_sym. apply nat_bijection_Permutation.
+
+
+  rewrite Permutation_image.
+
+  assert (forall (b: list X),
+    Permutation b (map (fun e => nth (g e) b x) (seq 0 (length b)))).
+  intro b. induction b. easy.
+  replace (seq 0 (length (a::b))) with ((seq 0 (length b)) ++ [ length b ]).
+  rewrite map_app.
+
+
+
+  admit. (* TODO *) (* easy. *)
+  split.
 
   (* first case in split *)
   rewrite H1.
@@ -300,32 +366,70 @@ Proof.
   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.
+  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 H6 with (s := l). 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 H7 in M1.
+  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 H7.
+  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 p) (map f s)).
+    -> 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.
+
+
+
+
+
+
+
+
+  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.
 
@@ -337,20 +441,16 @@ Proof.
   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).
+  exists (f a). split. apply H2.
+  assumption. apply H5 in H6. destruct H6. rewrite H6. reflexivity.
 
 
 
-  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.
-