Update
This commit is contained in:
Thomas Baruchel
parent
bf9517f266
commit
55bb6b865b
495
src/mapping.v
495
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.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue