2023-12-02 12:08:19 -05:00
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2023-12-02 12:25:32 -05:00
|
|
|
(*
|
2023-12-02 12:08:19 -05:00
|
|
|
|
|
|
|
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.
|
2023-12-02 12:25:32 -05:00
|
|
|
*)
|
2023-12-02 12:08:19 -05:00
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
2023-12-02 12:25:32 -05:00
|
|
|
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.
|
|
|
|
|
|
|
|
|
2023-12-02 17:13:03 -05:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(*
|
|
|
|
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. 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.
|
|
|
|
|
|
|
|
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).
|
|
|
|
replace a with (g (f 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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*)
|
|
|
|
|
2023-12-02 12:25:32 -05:00
|
|
|
Lemma permutation_mapping_swap {X: Type} :
|
|
|
|
forall (u v base : list X),
|
|
|
|
permutation_mapping u v base -> permutation_mapping v u base.
|
|
|
|
Proof.
|
2023-12-02 17:13:03 -05:00
|
|
|
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.
|
|
|
|
exists p. exists (map f l). split. assumption. 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 H5. 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.
|
|
|
|
|
|
|
|
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.
|
|
|
|
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.
|
|
|
|
|
|
|
|
(* 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)).
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
2023-12-02 12:25:32 -05:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|