diff --git a/src/mapping.v b/src/mapping.v index da4c729..73647bb 100644 --- a/src/mapping.v +++ b/src/mapping.v @@ -326,8 +326,46 @@ Proof. 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. + 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). rewrite nth_error_nth' with (d := x). rewrite <- H4. reflexivity. apply K. @@ -351,23 +389,6 @@ Proof. apply IHs with (t := t). assumption. 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. - - -