diff --git a/src/mapping.v b/src/mapping.v index 48a53ca..be78184 100644 --- a/src/mapping.v +++ b/src/mapping.v @@ -69,6 +69,142 @@ Proof. Qed. +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. + + 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. + + 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. + + assert (N: In a (a::s)). apply in_eq. apply K in N. assert (M := N). + apply H5 in N. destruct N. + + 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. + + rewrite H6. apply J2 in J3. destruct J3. apply H9. apply J. assumption. + + rewrite H6. rewrite H7. reflexivity. apply H2. assumption. rewrite H6. + + symmetry. rewrite map_nth_error with (d := f a). reflexivity. + + rewrite nth_error_nth' with (d := 0). rewrite H6. reflexivity. + apply H2. assumption. rewrite seq_length. apply H2. assumption. + apply H2. assumption. assumption. intro y. intro G. apply K. + apply in_cons. assumption. + + replace (map (fun e : nat => nth e base x) (map g (seq 0 (length base)))) + with (map (fun z => (fun e => nth e base x) (g z)) (seq 0 (length base))). + apply H6. + + assert (forall w (u v: list X), + map Some u = map (nth_error v) w -> (forall y, In y w -> y < length v)). + intro w; induction w; intros u0 v0; intro J; intro y; intro J1. + contradiction. destruct u0. inversion J. + + apply in_inv in J1. destruct J1. rewrite <- H7. + inversion J. apply nth_error_Some. rewrite <- H9. easy. + apply IHw with (u := u0). inversion J. reflexivity. assumption. + apply H7 with (u := x::u). assumption. + + rewrite map_map. reflexivity. assumption. assumption. +Qed. + + @@ -270,362 +406,3 @@ Proof. *) - -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. - - 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. - - 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. - - assert (N: In a (a::s)). apply in_eq. apply K in N. assert (M := N). - apply H5 in N. destruct N. - - 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. - - rewrite H6. apply J2 in J3. destruct J3. apply H9. apply J. assumption. - - rewrite H6. rewrite H7. reflexivity. apply H2. assumption. rewrite H6. - - symmetry. rewrite map_nth_error with (d := f a). reflexivity. - - rewrite nth_error_nth' with (d := 0). rewrite H6. reflexivity. - apply H2. assumption. rewrite seq_length. apply H2. assumption. - apply H2. assumption. assumption. intro y. intro G. apply K. - apply in_cons. assumption. - - replace (map (fun e : nat => nth e base x) (map g (seq 0 (length base)))) - with (map (fun z => (fun e => nth e base x) (g z)) (seq 0 (length base))). - apply H6. - - assert (forall w (u v: list X), - map Some u = map (nth_error v) w -> (forall y, In y w -> y < length v)). - intro w; induction w; intros u0 v0; intro J; intro y; intro J1. - contradiction. destruct u0. inversion J. - - apply in_inv in J1. destruct J1. rewrite <- H7. - inversion J. apply nth_error_Some. rewrite <- H9. easy. - apply IHw with (u := u0). inversion J. reflexivity. assumption. - apply H7 with (u := x::u). assumption. - - - - - - - - - - - - - - - - - - - - - - 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). - - - - (* aboutit à -Some (nth (g (nth (f a) (seq 0 (length base)) 0)) base x) = -Some - (nth (f a) (map (fun e : nat => nth (g e) base x) (seq 0 (length base))) 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. - - - - - - - - -