593 lines
19 KiB
Coq
593 lines
19 KiB
Coq
Require Import subsequences.
|
|
Require Import Sorting.Permutation.
|
|
|
|
Require Import Nat.
|
|
Require Import PeanoNat.
|
|
Require Import List.
|
|
|
|
|
|
Import ListNotations.
|
|
|
|
|
|
|
|
Definition Permutation_mapping {X: Type} (u v base : list X) :=
|
|
exists p l, Permutation base p
|
|
/\ map Some u = map (nth_error base) l
|
|
/\ map Some v = map (nth_error p) l.
|
|
|
|
|
|
(* TODO : ajouter un truc avec Add pour la base *)
|
|
|
|
|
|
|
|
(*
|
|
|
|
Definition incl_without_eq {X: Type} (u v : list X) :=
|
|
exists l, map Some u = map (nth_error v) l.
|
|
|
|
Lemma incl_without_eq_incl {X: Type}:
|
|
forall (u v : list X), incl_without_eq u v -> incl u v.
|
|
Proof.
|
|
intro u. induction u; intro v; intro H. easy. destruct H.
|
|
destruct x. symmetry in H. apply nil_cons in H. contradiction.
|
|
inversion H. apply incl_cons.
|
|
symmetry in H1. apply nth_error_In in H1. assumption.
|
|
apply IHu. exists x. assumption.
|
|
Qed.
|
|
|
|
|
|
Lemma incl_incl_without_eq {X: Type}:
|
|
forall (u v : list X), incl u v -> incl_without_eq u v.
|
|
Proof.
|
|
intro u. induction u; intro v; intro H. exists nil. easy.
|
|
apply incl_cons_inv in H. destruct H. apply IHu in H0. destruct H0.
|
|
apply In_nth_error in H. destruct H. exists (x0 :: x).
|
|
simpl. rewrite H. rewrite H0. reflexivity.
|
|
Qed.
|
|
*)
|
|
|
|
|
|
Lemma Permutation_mapping_nil {X: Type} :
|
|
forall (base : list X), Permutation_mapping nil nil base.
|
|
Proof.
|
|
intro base. exists base. exists nil. split; easy.
|
|
Qed.
|
|
|
|
|
|
Lemma Permutation_mapping_nil_l {X: Type} :
|
|
forall (u base : list X), Permutation_mapping nil u base -> u = nil.
|
|
Proof.
|
|
intro u. induction u; intro base; intro H. reflexivity.
|
|
destruct H as [p]. destruct H as [l]. destruct H. destruct H0.
|
|
inversion H1. symmetry in H0. apply map_eq_nil in H0. rewrite H0 in H3.
|
|
inversion H3.
|
|
Qed.
|
|
|
|
|
|
Lemma Permutation_mapping_nil_r {X: Type} :
|
|
forall (u base : list X), Permutation_mapping u nil base -> u = nil.
|
|
Proof.
|
|
intro u. induction u; intro base; intro H. reflexivity.
|
|
destruct H as [p]. destruct H as [l]. destruct H. destruct H0.
|
|
inversion H1. symmetry in H3. apply map_eq_nil in H3. rewrite H3 in H0.
|
|
inversion H0.
|
|
Qed.
|
|
|
|
|
|
Lemma Permutation_mapping_cons {X: Type} :
|
|
forall (u v base : list X) a b,
|
|
Permutation_mapping (a::u) (b::v) base -> Permutation_mapping u v base.
|
|
Proof.
|
|
intros u v base a b. intro H. destruct H as [p]. destruct H as [l].
|
|
destruct H. destruct H0. exists p. destruct l. inversion H0. exists l.
|
|
split. assumption. split; [ inversion H0 | inversion H1]; reflexivity.
|
|
Qed.
|
|
|
|
|
|
Lemma Permutation_mapping_cons3 {X: Type} :
|
|
forall (u v base: list X) a,
|
|
Permutation_mapping u v base
|
|
-> Permutation_mapping (a::u) (a::v) (a::base).
|
|
Proof.
|
|
intros u v base a. intros H.
|
|
destruct H as [p]. destruct H as [l].
|
|
destruct H. destruct H0. exists (a::p). exists (0::(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; simpl; rewrite H2; [ rewrite H0 | rewrite H1]; reflexivity.
|
|
Qed.
|
|
|
|
|
|
Lemma Permutation_mapping_swap_first {X: Type} :
|
|
forall (u v base: list X) a1 a2 b1 b2,
|
|
Permutation_mapping (a1::a2::u) (b1::b2::v) base
|
|
-> Permutation_mapping (a2::a1::u) (b2::b1::v) base.
|
|
Proof.
|
|
intros u v base a1 a2 b1 b2. intros H.
|
|
destruct H as [p]. destruct H as [l].
|
|
destruct H. destruct H0. exists p.
|
|
destruct l. inversion H0. destruct l. inversion H0. exists (n0::n::l).
|
|
split. assumption. inversion H0. inversion H1.
|
|
split; simpl; [ rewrite H3 | rewrite H6]; [ rewrite H4 | rewrite H7];
|
|
[ rewrite H5 | rewrite H8]; reflexivity.
|
|
Qed.
|
|
|
|
|
|
Lemma Permutation_mapping_repeat_first {X: Type} :
|
|
forall (u v base: list X) a b,
|
|
Permutation_mapping (a::u) (b::v) base
|
|
-> Permutation_mapping (a::a::u) (b::b::v) base.
|
|
Proof.
|
|
intros u v base a b. intros H.
|
|
destruct H as [p]. destruct H as [l].
|
|
destruct H. destruct H0. exists p.
|
|
destruct l. inversion H0. exists (n::n::l).
|
|
split. assumption. simpl. simpl in H0. simpl in H1.
|
|
rewrite H0. rewrite H1.
|
|
|
|
assert (forall (l: list (option X)) x y z,
|
|
x::l = z::l -> x::y::l = z::y::l).
|
|
intros. inversion H2. reflexivity.
|
|
|
|
split. apply H2. inversion H0. reflexivity.
|
|
apply H2. inversion H1. reflexivity.
|
|
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.
|
|
|
|
|
|
Lemma Permutation_mapping_self {X: Type} :
|
|
forall (u base : list X), incl u base -> Permutation_mapping u u base.
|
|
Proof.
|
|
intro u. induction u; intro base; intro H; exists base.
|
|
exists nil. split; easy. apply incl_cons_inv in H. destruct H.
|
|
apply IHu in H0. destruct H0. destruct H0. destruct H0. destruct H1.
|
|
apply In_nth_error in H. destruct H. exists (x1 :: x0).
|
|
split. easy. split; simpl; rewrite H; rewrite H1; reflexivity.
|
|
Qed.
|
|
|
|
|
|
Lemma Permutation_mapping_length {X: Type} :
|
|
forall (u v base : list X),
|
|
Permutation_mapping u v base -> length u = length v.
|
|
Proof.
|
|
intros u v base. intro H. destruct H. destruct H. destruct H. destruct H0.
|
|
replace (length u) with (length (map Some u)). rewrite H0.
|
|
replace (length v) with (length (map Some v)). rewrite H1.
|
|
rewrite map_length. rewrite map_length. reflexivity.
|
|
apply map_length. apply map_length.
|
|
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.
|
|
|
|
|
|
Lemma Permutation_mapping_subset {X: Type} :
|
|
forall (u v base u': list X),
|
|
Permutation_mapping u v base
|
|
-> incl u' u -> (exists v', incl v' v /\ Permutation_mapping u' v' base).
|
|
Proof.
|
|
intros u v base u'. intros H I. destruct H as [p]. destruct H as [l].
|
|
destruct H. destruct H0.
|
|
assert (exists l', map Some u' = map (nth_error base) l').
|
|
Admitted.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lemma Permutation_mapping_base {X: Type} :
|
|
forall (u v base p: list X),
|
|
Permutation base p -> Permutation_mapping u v base
|
|
-> Permutation_mapping u v p.
|
|
Proof.
|
|
intros u v base p.
|
|
|
|
(* destruct u in order to get a value of type X when needed *)
|
|
destruct u. intros I 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.
|
|
|
|
intros H I. assert (K := H).
|
|
|
|
destruct I as [p']. destruct H0 as [l]. destruct H0.
|
|
destruct H1.
|
|
|
|
rewrite Permutation_nth in H. destruct H.
|
|
destruct H3 as [f]. destruct H3. destruct H4.
|
|
apply FinFun.bInjective_bSurjective in H4.
|
|
apply FinFun.bSurjective_bBijective in H4. destruct H4 as [g].
|
|
destruct H4.
|
|
|
|
exists base. exists (map g l). split.
|
|
apply Permutation_trans with (l' := base). apply Permutation_sym.
|
|
assumption. apply Permutation_refl. split.
|
|
|
|
(* first case in split *)
|
|
rewrite H1.
|
|
|
|
assert (forall s, (forall y, In y s -> y < length base)
|
|
-> map (nth_error base) s = map (nth_error p) (map g s)).
|
|
intro s. induction s; intro L. reflexivity.
|
|
assert (M: a < length base). apply L. apply in_eq.
|
|
|
|
simpl. rewrite IHs.
|
|
rewrite nth_error_nth' with (d := x).
|
|
rewrite nth_error_nth' with (d := x).
|
|
replace a with (f (g a)) at 1.
|
|
rewrite <- H5. reflexivity.
|
|
apply H4. assumption.
|
|
apply H6 in M. destruct M. assumption.
|
|
rewrite H. apply H4. assumption. assumption.
|
|
intro y. intro N. apply L. apply in_cons. assumption.
|
|
|
|
apply H7. intro y. intro N.
|
|
|
|
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 H8 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 H9 in M1.
|
|
destruct t; inversion M1. easy.
|
|
destruct t; inversion M1.
|
|
apply IHs with (t := t); assumption.
|
|
generalize N. generalize H1. apply H9.
|
|
|
|
(* second case in split *)
|
|
rewrite H2.
|
|
|
|
assert (forall s, (forall y, In y s -> y < length base)
|
|
-> map (nth_error p') s = map (nth_error base) (map g s)).
|
|
intro s. induction s; intro R. reflexivity.
|
|
simpl. rewrite IHs.
|
|
|
|
rewrite nth_error_nth' with (d := x).
|
|
rewrite nth_error_nth' with (d := x).
|
|
|
|
rewrite Permutation_nth in H0. destruct H0. destruct H7 as [h].
|
|
destruct H7. destruct H8.
|
|
apply FinFun.bInjective_bSurjective in H8.
|
|
apply FinFun.bSurjective_bBijective in H8. destruct H8 as [h'].
|
|
destruct H8.
|
|
|
|
rewrite H9.
|
|
|
|
assert (forall n, n < length base -> h n = g n).
|
|
intro n. intro J.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
replace a with (f (g a)) at 1.
|
|
rewrite <- H5. reflexivity.
|
|
apply H4. assumption.
|
|
apply H6 in M. destruct M. assumption.
|
|
rewrite H. apply H4. assumption. assumption.
|
|
intro y. intro N. apply L. apply in_cons. assumption.
|
|
|
|
apply H7. intro y. intro N.
|
|
|
|
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 H8 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 H9 in M1.
|
|
destruct t. inversion M1. inversion M1. easy.
|
|
destruct t. inversion M1. inversion M1.
|
|
apply IHs with (t := t). assumption. assumption.
|
|
generalize N. generalize H1. apply H9.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
exists p'. exists (map g l). split.
|
|
apply Permutation_trans with (l' := base). apply Permutation_sym.
|
|
assumption. assumption. split.
|
|
|
|
(* first case in split *)
|
|
rewrite H1.
|
|
|
|
assert (forall s, (forall y, In y s -> y < length base)
|
|
-> map (nth_error base) s = map (nth_error p) (map g s)).
|
|
intro s. induction s; intro L. reflexivity.
|
|
assert (M: a < length base). apply L. apply in_eq.
|
|
|
|
simpl. rewrite IHs.
|
|
rewrite nth_error_nth' with (d := x).
|
|
rewrite nth_error_nth' with (d := x).
|
|
replace a with (f (g a)) at 1.
|
|
rewrite <- H5. reflexivity.
|
|
apply H4. assumption.
|
|
apply H6 in M. destruct M. assumption.
|
|
rewrite H. apply H4. assumption. assumption.
|
|
intro y. intro N. apply L. apply in_cons. assumption.
|
|
|
|
apply H7. intro y. intro N.
|
|
|
|
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 H8 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 H9 in M1.
|
|
destruct t. inversion M1. inversion M1. easy.
|
|
destruct t. inversion M1. inversion M1.
|
|
apply IHs with (t := t). assumption. assumption.
|
|
generalize N. generalize H1. apply H9.
|
|
|
|
(* second case in split *)
|
|
rewrite H2.
|
|
|
|
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)).
|
|
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.
|
|
*)
|
|
replace a with (f (g a)) at 1. rewrite H4.
|
|
|
|
|
|
assert (exists b, b < length base /\ a = g b).
|
|
exists (f a).
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*)
|