Reordering of lists
Inductive list_reorder : list A → list A → Prop :=
| list_reorder_nil : list_reorder [] []
| list_reorder_cons : ∀(a : A)(l1 l2 : list A)(n : nat),
list_reorder l1 l2 →
list_reorder (a :: l1) ((firstn n l2) ++ a :: (skipn n l2)).
Lemma list_reorder_cons_parts : ∀(l1 l2l l2r : list A)(a : A),
list_reorder l1 (l2l ++ l2r) →
list_reorder (a :: l1) (l2l ++ a :: l2r).
Lemma list_reorder_cons_head : ∀(l1 l2 : list A)(a : A),
list_reorder l1 l2 →
list_reorder (a :: l1) (a :: l2).
Lemma list_reorder_refl : ∀(l : list A), list_reorder l l.
Lemma list_reorder_length : ∀(l1 l2 : list A),
list_reorder l1 l2 → length l1 = length l2.
Lemma list_reorder_symm :
∀(l1 l2 : list A), list_reorder l1 l2 → list_reorder l2 l1.
Lemma list_reorder_occurence_full :
∀(l1 l2 : list A)(n1 : nat)(n1_less : n1 < length l1),
list_reorder l1 l2 →
∃(n2 : nat),
n2_less # n2 < length l2 /#\
nth l1 n1 n1_less = nth l2 n2 n2_less ∧
list_reorder (cutout_nth l1 n1) (cutout_nth l2 n2).
Lemma list_reorder_occurence :
∀(l1 l2 : list A)(n1 : nat)(n1_less : n1 < length l1),
list_reorder l1 l2 →
∃(n2 : nat),
n2_less # n2 < length l2 /#\
nth l1 n1 n1_less = nth l2 n2 n2_less.
Lemma list_reorder_trans :
∀(l1 l2 l3 : list A),
list_reorder l1 l2 → list_reorder l2 l3 → list_reorder l1 l3.
Lemma list_reorder_trans_rev :
∀(l1 l2 l3 : list A),
list_reorder l2 l3 → list_reorder l1 l2 → list_reorder l1 l3.
Lemma every_nth_list_reorder :
∀(P : A → Prop)(l1 l2 : list A),
list_reorder l1 l2 →
(every_nth P l1 ↔ every_nth P l2).
Lemma list_reorder_insert : ∀(l1l l1r l2l l2r : list A)(a1 a2 : A),
list_reorder (l1l ++ l1r) (l2l ++ l2r) →
a1 = a2 →
list_reorder (l1l ++ a1 :: l1r) (l2l ++ a2 :: l2r).
Lemma list_reorder_insert_list : ∀(l1l l1r l2l l2r lm1 lm2 : list A),
list_reorder (l1l ++ l1r) (l2l ++ l2r) →
list_reorder lm1 lm2 →
list_reorder (l1l ++ lm1 ++ l1r) (l2l ++ lm2 ++ l2r).
Lemma list_reorder_tail : ∀(l1 l2l l2r : list A)(a : A),
list_reorder (a :: l1) (l2l ++ a :: l2r) →
list_reorder l1 (l2l ++ l2r).
Lemma list_reorder_tail_head : ∀(l1 l2 : list A)(a : A),
list_reorder (a :: l1) (a :: l2) →
list_reorder l1 l2.
Lemma list_reorder_inserted_2 :
∀(l1l l1m l1r l2 : list A)(a1l a1r : A),
list_reorder (l1l ++ a1l :: l1m ++ a1r :: l1r) l2 →
∃(l2l l2m l2r : list A)(a2l a2r : A),
l2 = l2l ++ a2l :: l2m ++ a2r :: l2r ∧
list_reorder (l1l ++ l1m ++ l1r) (l2l ++ l2m ++ l2r) ∧
((a1l = a2l ∧ a1r = a2r) ∨
(a1l = a2r ∧ a1r = a2l)).
Lemma list_reorder_partition : ∀(f : A → bool)(l : list A),
list_reorder l ((fst (partition f l)) ++ (snd (partition f l))).
Lemma list_reorder_single_append :
∀(a : A)(l rl rr : list A),
list_reorder (a :: l) (rl ++ rr) →
(∃(rlt : list A), list_reorder (a :: rlt) rl) ∨
(∃(rrt : list A), list_reorder (a :: rrt) rr).
Lemma list_reorder_In : ∀(a : A)(l1 l2 : list A),
list_reorder l1 l2 →
In a l1 →
In a l2.
Lemma list_reorder_nil_is_nil : ∀(l : list A),
list_reorder [] l → l = [].
Lemma list_reorder_singleton : ∀(a : A)(l : list A),
list_reorder [a] l → l = [a].
Lemma list_reorder_nonempty : ∀(l1 l2 : list A),
l1 ≠ [] →
list_reorder l1 l2 →
l2 ≠ [].
Lemma list_reorder_first_occurence :
∀(a : A)(l1 l2 : list A),
list_reorder (a :: l1) l2 →
∃(n : nat),
n_less # n < length l2 /#\
nth l2 n n_less = a ∧ list_reorder l1 (cutout_nth l2 n).
Lemma list_reorder_swap_head : ∀(a b : A)(l : list A),
list_reorder (a :: b :: l) (b :: a :: l).
Lemma list_reorder_rot_3 : ∀(a b c : A)(l : list A),
list_reorder (a :: b :: c :: l) (b :: c :: a :: l).
Lemma list_reorder_move_append : ∀(a : A)(ll lr : list A),
list_reorder (a :: ll ++ lr) (ll ++ a :: lr).
Lemma list_reorder_append_3_middle : ∀(l1 l2 l3 : list A),
list_reorder (l2 ++ l1 ++ l3) (l1 ++ l2 ++ l3).
Lemma list_reorder_append_swap : ∀(l1 l2 : list A),
list_reorder (l1 ++ l2) (l2 ++ l1).
Lemma list_reorder_append_both : ∀(l1 l2 l3 l4 : list A),
list_reorder l1 l3 →
list_reorder l2 l4 →
list_reorder (l1 ++ l2) (l3 ++ l4).
Lemma list_reorder_append_right : ∀(l1 l2 l3 : list A),
list_reorder l1 l2 → list_reorder (l1 ++ l3) (l2 ++ l3).
Lemma list_reorder_append_left : ∀(l1 l2 l3 : list A),
list_reorder l1 l2 → list_reorder (l3 ++ l1) (l3 ++ l2).
Lemma list_reorder_In_split : ∀(l : list A)(a : A),
In a l →
∃(ll lr : list A),
list_reorder l (a :: ll ++ lr).
Lemma list_reorder_2_char : ∀(a1 a2 : A)(l : list A),
list_reorder [a1; a2] l →
l = [a1; a2] ∨ l = [a2; a1].
Lemma list_reorder_double_append :
∀(a : A)(l rl rr : list A),
list_reorder (a :: a :: l) (rl ++ rr) →
(∃(rlt : list A), list_reorder (a :: a :: rlt) rl) ∨
(∃(rlt rrt : list A),
list_reorder (a :: rlt) rl ∧ list_reorder (a :: rrt) rr) ∨
(∃(rrt : list A), list_reorder (a :: a :: rrt) rr).
End Reorder.
Implicit Arguments list_reorder [A].
Implicit Arguments list_reorder_length [A].
Implicit Arguments list_reorder_occurence_full [A].
Implicit Arguments list_reorder_occurence [A].
Implicit Arguments every_nth_list_reorder [A P].
Implicit Arguments list_reorder_insert [A].
Implicit Arguments list_reorder_insert_list [A].
Implicit Arguments list_reorder_tail [A].
Implicit Arguments list_reorder_inserted_2 [A].
Implicit Arguments list_reorder_single_append [A].
Implicit Arguments list_reorder_nonempty [A].
Implicit Arguments list_reorder_first_occurence [A].
Implicit Arguments list_reorder_move_append [A].
Implicit Arguments list_reorder_append_3_middle [A].
Implicit Arguments list_reorder_double_append [A].
Lemma list_reorder_map :
∀{A B : Type}{f : A → B}(l1 l2 : list A),
list_reorder l1 l2 →
list_reorder (map f l1) (map f l2).
Lemma list_reorder_left_map :
∀{A B : Type}(f : A → B)(l1 : list A)(l2 : list B),
list_reorder (map f l1) l2 →
∃(l2_pre : list A),
l2 = map f l2_pre ∧
list_reorder l1 l2_pre.
Lemma list_reorder_right_map :
∀{A B : Type}(f : A → B)(l1 : list B)(l2 : list A),
list_reorder l1 (map f l2) →
∃(l1_pre : list A),
l1 = map f l1_pre ∧
list_reorder l1_pre l2.