D5d: Relacje między listami
From Typonomikon Require Export D5c.
Sublist: listy jako termy
Zdefiniuj relację
Sublist. Zdanie
Sublist l1 l2 zachodzi, gdy
l2 jest podtermem listy
l1, tzn. jej ogonem, ogonem ogona,
ogonem ogona ogona etc.
Przykład:
Sublist [4; 5] [1; 2; 3; 4; 5] zachodzi.
Sublist [3; 4] [1; 2; 3; 4; 5] nie zachodzi.
Lemma Sublist_length :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 -> length l1 < length l2.
Lemma Sublist_cons_l :
forall (A : Type) (x : A) (l : list A), ~ Sublist (x :: l) l.
Lemma Sublist_cons_l' :
forall (A : Type) (x : A) (l1 l2 : list A),
Sublist (x :: l1) l2 -> Sublist l1 l2.
Lemma Sublist_nil_cons :
forall (A : Type) (x : A) (l : list A), Sublist [] (x :: l).
Lemma Sublist_irrefl :
forall (A : Type) (l : list A), ~ Sublist l l.
Lemma Sublist_antisym :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 -> ~ Sublist l2 l1.
Lemma Sublist_trans :
forall (A : Type) (l1 l2 l3 : list A),
Sublist l1 l2 -> Sublist l2 l3 -> Sublist l1 l3.
Lemma Sublist_snoc :
forall (A : Type) (x : A) (l1 l2 : list A),
Sublist l1 l2 -> Sublist (snoc x l1) (snoc x l2).
Lemma Sublist_snoc_inv :
forall (A : Type) (x y : A) (l1 l2 : list A),
Sublist (snoc x l1) (snoc y l2) -> Sublist l1 l2 /\ x = y.
Lemma Sublist_app_l :
forall (A : Type) (l1 l2 : list A),
l1 <> [] -> Sublist l2 (l1 ++ l2).
Lemma Sublist_app_l' :
forall (A : Type) (l1 l2 l3 : list A),
Sublist l1 l2 -> Sublist l1 (l3 ++ l2).
Lemma Sublist_app_r :
forall (A : Type) (l1 l2 l3 : list A),
Sublist l1 l2 -> Sublist (l1 ++ l3) (l2 ++ l3).
Lemma Sublist_map :
forall (A B : Type) (f : A -> B) (l1 l2 : list A),
Sublist l1 l2 -> Sublist (map f l1) (map f l2).
Lemma Sublist_join :
forall (A : Type) (l1 l2 : list (list A)),
~ elem [] l2 -> Sublist l1 l2 -> Sublist (join l1) (join l2).
Lemma Sublist_replicate :
forall (A : Type) (n m : nat) (x : A),
Sublist (replicate n x) (replicate m x) <-> n < m.
Lemma Sublist_replicate' :
forall (A : Type) (n m : nat) (x y : A),
Sublist (replicate n x) (replicate m y) <->
n < m /\ (n <> 0 -> x = y).
Lemma Sublist_iterate :
forall (A : Type) (f : A -> A) (n m : nat) (x : A),
Sublist (iterate f n x) (iterate f m x) ->
n = 0 \/ n = m \/ (n <= m /\ f x = x).
Lemma Sublist_tail :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 ->
forall t1 t2 : list A, tail l1 = Some t1 -> tail l2 = Some t2 ->
Sublist t1 t2.
Lemma Sublist_last :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 -> l1 = [] \/ last l1 = last l2.
Lemma Sublist_spec :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 <->
exists n : nat,
n < length l2 /\ l1 = drop (S n) l2.
Lemma Sublist_drop_r :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 -> forall n : nat, Sublist (drop n l1) l2.
Lemma Sublist_drop :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 -> forall n : nat,
n < length l2 -> Sublist (drop n l1) (drop n l2).
Lemma Sublist_replace :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 -> forall (l1' l2' : list A) (n : nat) (x : A),
replace l1 n x = Some l1' -> replace l2 (n + length l1) x = Some l2' ->
Sublist l1' l2'.
Lemma Sublist_zip :
exists (A B : Type) (la1 la2 : list A) (lb1 lb2 : list A),
Sublist la1 la2 /\ Sublist lb1 lb2 /\
~ Sublist (zip la1 lb1) (zip la2 lb2).
Lemma Sublist_any_false :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Sublist l1 l2 -> any p l2 = false -> any p l1 = false.
Lemma Sublist_any_true :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Sublist l1 l2 -> any p l1 = true -> any p l2 = true.
Lemma Sublist_findLast :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Sublist l1 l2 -> forall x : A,
findLast p l1 = Some x -> findLast p l2 = Some x.
Lemma Sublist_removeLast :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Sublist l1 l2 ->
match removeLast p l1, removeLast p l2 with
| None, None => True
| None, Some (x, l2') => l1 = l2' \/ Sublist l1 l2'
| x, None => False
| Some (x, l1'), Some (y, l2') => x = y /\ Sublist l1' l2'
end.
Lemma Sublist_findIndex :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Sublist l1 l2 -> forall n : nat,
findIndex p l1 = Some n -> exists m : nat,
findIndex p l2 = Some m.
Lemma Sublist_filter :
exists (A : Type) (p : A -> bool) (l1 l2 : list A),
Sublist l1 l2 /\ ~ Sublist (filter p l1) (filter p l2).
Lemma Sublist_findIndices :
exists (A : Type) (p : A -> bool) (l1 l2 : list A),
Sublist l1 l2 /\ ~ Sublist (findIndices p l1) (findIndices p l2).
Lemma Sublist_takeWhile :
exists (A : Type) (p : A -> bool) (l1 l2 : list A),
Sublist l1 l2 /\ ~ Sublist (takeWhile p l1) (takeWhile p l2).
Lemma Sublist_dropWhile :
exists (A : Type) (p : A -> bool) (l1 l2 : list A),
Sublist l1 l2 /\ ~ Sublist (dropWhile p l1) (dropWhile p l2).
Lemma Sublist_pmap :
exists (A B : Type) (f : A -> option B) (l1 l2 : list A),
Sublist l1 l2 /\ ~ Sublist (pmap f l1) (pmap f l2).
Lemma Sublist_intersperse :
forall (A : Type) (x : A) (l1 l2 : list A),
Sublist l1 l2 -> Sublist (intersperse x l1) (intersperse x l2).
Lemma Sublist_elem :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 -> forall x : A, elem x l1 -> elem x l2.
Lemma Sublist_In :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 -> forall x : A, In x l1 -> In x l2.
Lemma Sublist_NoDup :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 -> NoDup l2 -> NoDup l1.
Lemma Sublist_Dup :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 -> Dup l1 -> Dup l2.
Lemma Sublist_Rep :
forall (A : Type) (x : A) (l1 l2 : list A),
Sublist l1 l2 -> forall n : nat, Rep x n l1 -> Rep x n l2.
Lemma Sublist_Exists :
forall (A : Type) (P : A -> Prop) (l1 l2 : list A),
Sublist l1 l2 -> Exists P l1 -> Exists P l2.
Lemma Sublist_Forall :
forall (A : Type) (P : A -> Prop) (l1 l2 : list A),
Sublist l1 l2 -> Forall P l2 -> Forall P l1.
Lemma Sublist_AtLeast :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 -> forall (P : A -> Prop) (n : nat),
AtLeast P n l1 -> AtLeast P n l2.
Lemma Sublist_AtMost :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 -> forall (P : A -> Prop) (n : nat),
AtMost P n l2 -> AtMost P n l1.
Prefiksy
Zdefiniuj induktywną relację
Prefix. Zdanie
Prefix l1 l2
zachodzi, gdy lista
l1 pokrywa się z początkowym fragmentem
listy
l2 o dowolnej długości.
Przykład:
Prefix [1; 2] [1; 2; 3; 4; 5] zachodzi.
Prefix [1; 2] [1; 1; 2; 3; 5] nie zachodzi.
Lemma Prefix_spec :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 <-> exists l3 : list A, l2 = l1 ++ l3.
Lemma Prefix_refl :
forall (A : Type) (l : list A), Prefix l l.
Lemma Prefix_trans :
forall (A : Type) (l1 l2 l3 : list A),
Prefix l1 l2 -> Prefix l2 l3 -> Prefix l1 l3.
Lemma Prefix_wasym :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 -> Prefix l2 l1 -> l1 = l2.
Lemma Prefix_length :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 -> length l1 <= length l2.
Lemma Prefix_snoc :
forall {A : Type} (l1 l2 : list A) (x : A),
Prefix l1 l2 -> Prefix l1 (snoc x l2).
Lemma Prefix_snoc' :
exists (A : Type) (l1 l2 : list A),
Prefix l1 l2 /\ exists x : A, ~ Prefix (snoc x l1) (snoc x l2).
Lemma Prefix_app :
forall (A : Type) (l1 l2 l3 : list A),
Prefix l1 l2 -> Prefix (l3 ++ l1) (l3 ++ l2).
Lemma Prefix_app_r :
forall (A : Type) (l1 l2 l3 : list A),
Prefix l1 l2 -> Prefix l1 (l2 ++ l3).
Lemma Prefix_rev_l :
forall (A : Type) (l : list A),
Prefix (rev l) l -> l = rev l.
Lemma Prefix_rev_r :
forall (A : Type) (l : list A),
Prefix l (rev l) -> l = rev l.
Lemma Prefix_map :
forall (A B : Type) (f : A -> B) (l1 l2 : list A),
Prefix l1 l2 -> Prefix (map f l1) (map f l2).
Lemma Prefix_join :
forall (A : Type) (l1 l2 : list (list A)),
Prefix l1 l2 -> Prefix (join l1) (join l2).
Lemma Prefix_replicate :
forall (A : Type) (n m : nat) (x : A),
Prefix (replicate n x) (replicate m x) <-> n <= m.
Lemma Prefix_replicate_inv_l :
forall (A : Type) (l : list A) (n : nat) (x : A),
Prefix l (replicate n x) ->
exists m : nat, m <= n /\ l = replicate m x.
Lemma Prefix_replicate_inv_r :
exists (A : Type) (l : list A) (n : nat) (x : A),
Prefix (replicate n x) l /\
~ exists m : nat, n <= m /\ l = replicate m x.
Lemma Prefix_replicate' :
forall (A : Type) (n : nat) (x y : A),
Prefix (replicate n x) (replicate n y) <-> n = 0 \/ x = y.
Lemma Prefix_replicate'' :
forall (A : Type) (n m : nat) (x y : A),
Prefix (replicate n x) (replicate m y) <->
n = 0 \/ n <= m /\ x = y.
Lemma Prefix_iterate :
forall (A : Type) (f : A -> A) (n m : nat) (x : A),
Prefix (iterate f n x) (iterate f m x) <-> n <= m.
Lemma Prefix_insert :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 -> forall (n : nat) (x : A),
n <= length l1 -> Prefix (insert l1 n x) (insert l2 n x).
Lemma Prefix_replace :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 -> forall (n : nat) (x : A),
match replace l1 n x, replace l2 n x with
| Some l1', Some l2' => Prefix l1' l2'
| _, _ => True
end.
Lemma insert_length_ge :
forall (A : Type) (l : list A) (n : nat) (x : A),
length l <= n -> insert l n x = snoc x l.
Lemma Prefix_insert' :
exists (A : Type) (l1 l2 : list A),
Prefix l1 l2 /\
exists (n : nat) (x : A),
length l1 < n /\ ~ Prefix (insert l1 n x) (insert l2 n x).
Lemma Prefix_take_l :
forall (A : Type) (l : list A) (n : nat), Prefix (take n l) l.
Lemma Prefix_take :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 -> forall n : nat, Prefix (take n l1) (take n l2).
Lemma Prefix_drop :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 -> forall n : nat, Prefix (drop n l1) (drop n l2).
Lemma Prefix_zip :
forall (A B : Type) (la1 la2 : list A) (lb1 lb2 : list B),
Prefix la1 la2 -> Prefix lb1 lb2 ->
Prefix (zip la1 lb1) (zip la2 lb2).
Lemma Prefix_any_false :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Prefix l1 l2 -> any p l2 = false -> any p l1 = false.
Lemma Prefix_any :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Prefix l1 l2 -> any p l1 = true -> any p l2 = true.
Lemma Prefix_all_false :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Prefix l1 l2 -> all p l1 = false -> all p l2 = false.
Lemma Prefix_all_true :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Prefix l1 l2 -> all p l2 = true -> all p l1 = true.
Lemma Prefix_find_None :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Prefix l1 l2 -> find p l2 = None -> find p l1 = None.
Lemma Prefix_find_Some :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Prefix l1 l2 -> forall x : A,
find p l1 = Some x -> find p l2 = Some x.
Lemma Prefix_findIndex_None :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Prefix l1 l2 -> findIndex p l2 = None -> findIndex p l1 = None.
Lemma Prefix_findIndex_Some :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Prefix l1 l2 -> forall i : nat,
findIndex p l1 = Some i -> findIndex p l2 = Some i.
Lemma Prefix_count :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Prefix l1 l2 -> count p l1 <= count p l2.
Lemma Prefix_filter :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Prefix l1 l2 -> Prefix (filter p l1) (filter p l2).
Lemma Prefix_findIndices :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Prefix l1 l2 -> Prefix (findIndices p l1) (findIndices p l2).
Lemma Prefix_takeWhile :
forall (A : Type) (p : A -> bool) (l : list A),
Prefix (takeWhile p l) l.
Lemma Prefix_takeWhile_pres :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Prefix l1 l2 -> Prefix (takeWhile p l1) (takeWhile p l2).
Lemma Prefix_dropWhile :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Prefix l1 l2 -> Prefix (dropWhile p l1) (dropWhile p l2).
Lemma Prefix_pmap :
forall (A B : Type) (f : A -> option B) (l1 l2 : list A),
Prefix l1 l2 -> Prefix (pmap f l1) (pmap f l2).
Lemma Prefix_intersperse :
forall (A : Type) (x : A) (l1 l2 : list A),
Prefix l1 l2 -> Prefix (intersperse x l1) (intersperse x l2).
Lemma Prefix_elem :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 -> forall x : A, elem x l1 -> elem x l2.
Lemma Prefix_elem_conv :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 -> forall x : A, ~ elem x l2 -> ~ elem x l1.
Lemma Prefix_NoDup :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 -> NoDup l2 -> NoDup l1.
Lemma Prefix_Dup :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 -> Dup l1 -> Dup l2.
Lemma Prefix_Exists :
forall (A : Type) (P : A -> Prop) (l1 l2 : list A),
Prefix l1 l2 -> Exists P l1 -> Exists P l2.
Lemma Prefix_Forall :
forall (A : Type) (P : A -> Prop) (l1 l2 : list A),
Prefix l1 l2 -> Forall P l2 -> Forall P l1.
Lemma Prefix_AtLeast :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 -> forall (P : A -> Prop) (n : nat),
AtLeast P n l1 -> AtLeast P n l2.
Lemma Prefix_AtMost :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 -> forall (P : A -> Prop) (n : nat),
AtMost P n l2 -> AtMost P n l1.
Lemma Sublist_Prefix :
exists (A : Type) (l1 l2 : list A),
Sublist l1 l2 /\ ~ Prefix l1 l2.
Lemma Prefix_spec' :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 <-> exists n : nat, l1 = take n l2.
Lemma Prefix_Palindrome :
forall (A : Type) (l : list A),
Prefix (rev l) l <-> Palindrome l.
Sufiksy
Zdefiniuj induktywną relację
Suffix. Zdanie
Suffix l1 l2
zachodzi, gdy
l1 pokrywa się z końcowym fragmentem listy
l2
o dowolnej długości.
Przykłady:
Suffix [4; 5] [1; 2; 3; 4; 5] zachodzi.
Suffix [3; 4] [1; 2; 3; 4; 5] nie zachodzi.
Lemma Suffix_spec :
forall (A : Type) (l1 l2 : list A),
Suffix l1 l2 <-> exists l3 : list A, l2 = l3 ++ l1.
Lemma Suffix_cons_inv :
forall (A : Type) (x : A) (l1 l2 : list A),
Suffix (x :: l1) l2 -> Suffix l1 l2.
Lemma Suffix_trans :
forall (A : Type) (l1 l2 l3 : list A),
Suffix l1 l2 -> Suffix l2 l3 -> Suffix l1 l3.
Lemma Suffix_wasym :
forall (A : Type) (l1 l2 : list A),
Suffix l1 l2 -> Suffix l2 l1 -> l1 = l2.
Lemma Suffix_nil_l :
forall (A : Type) (l : list A), Suffix [] l.
Lemma Suffix_snoc :
forall (A : Type) (x : A) (l1 l2 : list A),
Suffix l1 l2 -> Suffix (snoc x l1) (snoc x l2).
Lemma Suffix_Sublist :
forall (A : Type) (l1 l2 : list A),
Suffix l1 l2 <-> Sublist l1 l2 \/ l1 = l2.
Lemma Prefix_Suffix :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 <-> Suffix (rev l1) (rev l2).
Subseq: listy jako ciągi
Zdefiniuj relację
Subseq. Zdanie
Subseq l1 l2 zachodzi, gdy
lista
l2 zawiera wszystkie elementy listy
l1 w takiej samej
kolejności, w jakiej występują one w
l1, ale może też zawierać
inne elementy.
Przykłady:
Subseq [1; 3; 5] [0; 1; 5; 2; 3; 4; 5] zachodzi.
Subseq [1; 3; 5] [3; 1; 5; 3; 6] nie zachodzi.
Lemma Subseq_refl :
forall (A : Type) (l : list A), Subseq l l.
Lemma Subseq_cons_inv :
forall (A : Type) (x : A) (l1 l2 : list A),
Subseq (x :: l1) (x :: l2) -> Subseq l1 l2.
Lemma Subseq_cons_inv_l :
forall (A : Type) (x : A) (l1 l2 : list A),
Subseq (x :: l1) l2 -> Subseq l1 l2.
Lemma Subseq_isEmpty_l :
forall (A : Type) (l1 l2 : list A),
isEmpty l1 = true -> Subseq l1 l2.
Lemma Subseq_nil_r :
forall (A : Type) (l : list A),
Subseq l [] -> l = [].
Lemma Subseq_length :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 -> length l1 <= length l2.
Lemma Subseq_trans :
forall (A : Type) (l1 l2 l3 : list A),
Subseq l1 l2 -> Subseq l2 l3 -> Subseq l1 l3.
Lemma Subseq_cons_l_app :
forall (A : Type) (x : A) (l1 l2 : list A),
Subseq (x :: l1) l2 ->
exists l21 l22 : list A,
l2 = l21 ++ x :: l22 /\ Subseq l1 l22.
Lemma Subseq_wasym :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 -> Subseq l2 l1 -> l1 = l2.
Lemma Subseq_snoc :
forall (A : Type) (x : A) (l1 l2 : list A),
Subseq l1 l2 -> Subseq l1 (snoc x l2).
Lemma Subseq_snoc' :
forall (A : Type) (x : A) (l1 l2 : list A),
Subseq l1 l2 -> Subseq (snoc x l1) (snoc x l2).
Lemma Subseq_rev :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 -> Subseq (rev l1) (rev l2).
Lemma Subseq_rev' :
forall (A : Type) (l1 l2 : list A),
Subseq (rev l1) (rev l2) <-> Subseq l1 l2.
Lemma Subseq_snoc_inv :
forall (A : Type) (x : A) (l1 l2 : list A),
Subseq (snoc x l1) (snoc x l2) -> Subseq l1 l2.
Lemma Subseq_app_l :
forall (A : Type) (l1 l2 l3 : list A),
Subseq l1 l2 -> Subseq l1 (l3 ++ l2).
Lemma Subseq_app_r :
forall (A : Type) (l1 l2 l3 : list A),
Subseq l1 l2 -> Subseq l1 (l2 ++ l3).
Lemma Subseq_app_l' :
forall (A : Type) (l1 l2 l3 : list A),
Subseq l1 l2 -> Subseq (l3 ++ l1) (l3 ++ l2).
Lemma Subseq_app_r' :
forall (A : Type) (l1 l2 l3 : list A),
Subseq l1 l2 -> Subseq (l1 ++ l3) (l2 ++ l3).
Lemma Subseq_app_not_comm :
exists (A : Type) (l1 l2 l3 : list A),
Subseq l1 (l2 ++ l3) /\ ~ Subseq l1 (l3 ++ l2).
Lemma Subseq_map :
forall (A B : Type) (f : A -> B) (l1 l2 : list A),
Subseq l1 l2 -> Subseq (map f l1) (map f l2).
Lemma Subseq_join :
forall (A : Type) (l1 l2 : list (list A)),
Subseq l1 l2 -> Subseq (join l1) (join l2).
Lemma Subseq_replicate :
forall (A : Type) (n m : nat) (x : A),
Subseq (replicate n x) (replicate m x) <-> n <= m.
Lemma Subseq_iterate :
forall (A : Type) (f : A -> A) (n m : nat) (x : A),
Subseq (iterate f n x) (iterate f m x) <-> n <= m.
Lemma Subseq_tail :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 -> forall l1' l2' : list A,
tail l1 = Some l1' -> tail l2 = Some l2' -> Subseq l1' l2'.
Lemma Subseq_uncons :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 -> forall (h1 h2 : A) (t1 t2 : list A),
uncons l1 = Some (h1, t1) -> uncons l2 = Some (h2, t2) ->
h1 = h2 \/ Subseq l1 t2.
Lemma Subseq_init :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 -> forall l1' l2' : list A,
init l1 = Some l1' -> init l2 = Some l2' -> Subseq l1' l2'.
Lemma Subseq_unsnoc :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 -> forall (h1 h2 : A) (t1 t2 : list A),
unsnoc l1 = Some (h1, t1) -> unsnoc l2 = Some (h2, t2) ->
h1 = h2 \/ Subseq l1 t2.
Lemma Subseq_nth :
forall (A : Type) (l1 l2 : list A) (n : nat) (x : A),
Subseq l1 l2 -> nth n l1 = Some x ->
exists m : nat, nth m l2 = Some x /\ n <= m.
Lemma Subseq_insert :
forall (A : Type) (l1 l2 : list A) (n : nat) (x : A),
Subseq l1 l2 -> Subseq l1 (insert l2 n x).
Lemma Subseq_replace :
forall (A : Type) (l1 l1' l2 : list A) (n : nat) (x : A),
Subseq l1 l2 -> replace l1 n x = Some l1' ->
exists (m : nat) (l2' : list A),
replace l2 m x = Some l2' /\ Subseq l1' l2'.
Lemma Subseq_remove' :
forall (A : Type) (l1 l2 : list A) (n : nat),
Subseq l1 l2 -> Subseq (remove' n l1) l2.
Lemma Subseq_take :
forall (A : Type) (l : list A) (n : nat),
Subseq (take n l) l.
Lemma Subseq_drop :
forall (A : Type) (l : list A) (n : nat),
Subseq (drop n l) l.
Lemma Subseq_zip :
exists (A B : Type) (la1 la2 : list A) (lb1 lb2 : list B),
Subseq la1 la2 /\ Subseq lb1 lb2 /\
~ Subseq (zip la1 lb1) (zip la2 lb2).
Lemma Subseq_all :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Subseq l1 l2 -> bool_le (all p l2) (all p l1).
Lemma Subseq_any :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Subseq l1 l2 -> bool_le (any p l1) (any p l2).
Lemma Subseq_all' :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Subseq l1 l2 -> all p l2 = true -> all p l1 = true.
Lemma Subseq_any' :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Subseq l1 l2 -> any p l2 = false -> any p l1 = false.
Lemma Subseq_findIndex :
exists (A : Type) (p : A -> bool) (l1 l2 : list A) (n m : nat),
Subseq l1 l2 /\ findIndex p l1 = Some n /\
findIndex p l2 = Some m /\ m < n.
Lemma Subseq_count :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Subseq l1 l2 -> count p l1 <= count p l2.
Lemma Subseq_filter :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Subseq l1 l2 -> Subseq (filter p l1) (filter p l2).
Lemma Subseq_filter' :
forall (A : Type) (p : A -> bool) (l : list A),
Subseq (filter p l) l.
Lemma Subseq_takeWhile :
forall (A : Type) (p : A -> bool) (l : list A),
Subseq (takeWhile p l) l.
Lemma Subseq_takeWhile' :
exists (A : Type) (p : A -> bool) (l1 l2 : list A),
Subseq l1 l2 /\ ~ Subseq (takeWhile p l1) (takeWhile p l2).
Lemma Subseq_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A),
Subseq (dropWhile p l) l.
Lemma Subseq_dropWhile' :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Subseq l1 l2 -> Subseq (dropWhile p l1) (dropWhile p l2).
Lemma Subseq_pmap :
forall (A B : Type) (f : A -> option B) (l1 l2 : list A),
Subseq l1 l2 -> Subseq (pmap f l1) (pmap f l2).
Lemma Subseq_map_pmap :
forall (A B : Type) (f : A -> option B) (l1 l2 : list A),
Subseq l1 l2 -> Subseq (map Some (pmap f l1)) (map f l2).
Lemma Subseq_intersperse :
forall (A : Type) (x : A) (l1 l2 : list A),
Subseq l1 l2 -> Subseq (intersperse x l1) (intersperse x l2).
Lemma Subseq_elem :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 ->
forall x : A, elem x l1 -> elem x l2.
Lemma Subseq_In :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 ->
forall x : A, In x l1 -> In x l2.
Lemma Subseq_NoDup :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 -> NoDup l2 -> NoDup l1.
Lemma Subseq_Dup :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 -> Dup l1 -> Dup l2.
Lemma Subseq_Rep :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 -> forall (x : A) (n : nat),
Rep x n l1 -> Rep x n l2.
Lemma Subseq_Exists :
forall (A : Type) (P : A -> Prop) (l1 l2 : list A),
Subseq l1 l2 -> Exists P l1 -> Exists P l2.
Lemma Subseq_Forall :
forall (A : Type) (P : A -> Prop) (l1 l2 : list A),
Subseq l1 l2 -> Forall P l2 -> Forall P l1.
Lemma Subseq_AtLeast :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 -> forall (P : A -> Prop) (n : nat),
AtLeast P n l1 -> AtLeast P n l2.
Lemma Subseq_AtMost :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 -> forall (P : A -> Prop) (n : nat),
AtMost P n l2 -> AtMost P n l1.
Lemma Sublist_Subseq :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 -> Subseq l1 l2.
Lemma Subseq_Sublist :
exists (A : Type) (l1 l2 : list A),
Subseq l1 l2 /\ ~ Sublist l1 l2.
Lemma Prefix_Subseq :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 -> Subseq l1 l2.
Lemma Subseq_Prefix :
exists (A : Type) (l1 l2 : list A),
Subseq l1 l2 /\ ~ Prefix l1 l2.
Lemma Subseq_rev_l :
forall (A : Type) (l : list A),
Subseq (rev l) l <-> Palindrome l.
Lemma Subseq_rev_r :
forall (A : Type) (l : list A),
Subseq l (rev l) <-> Palindrome l.
Zawieranie
Zdefiniuj (niekoniecznie induktywnie) relację
Incl. Zdanie
Incl l1 l2 zachodzi, gdy lista
l2 zawiera wszystkie te
elementy, które zawiera lista
l1, ale nie musi koniecznie
zawierać tyle samo sztuk każdego elementu.
Przykłady:
Incl [1; 1; 2; 2; 3; 3] [3; 4; 5; 1; 9; 0; 2] zachodzi.
Incl [1; 1; 2; 2; 3; 3] [2; 3; 4; 5] nie zachodzi.
Lemma Incl_nil :
forall (A : Type) (l : list A), Incl [] l.
Lemma Incl_nil_inv :
forall (A : Type) (l : list A),
Incl l [] -> l = [].
Lemma Incl_cons :
forall (A : Type) (h : A) (t1 t2 : list A),
Incl t1 t2 -> Incl (h :: t1) (h :: t2).
Lemma Incl_cons' :
forall (A : Type) (h : A) (t : list A),
Incl t (h :: t).
Lemma Incl_cons'' :
forall (A : Type) (h : A) (t l : list A),
Incl l t -> Incl l (h :: t).
Lemma Incl_cons_conv :
exists (A : Type) (x : A) (l1 l2 : list A),
Incl (x :: l1) (x :: l2) /\ ~ Incl l1 l2.
Lemma Incl_refl :
forall (A : Type) (l : list A), Incl l l.
Lemma Incl_trans :
forall (A : Type) (l1 l2 l3 : list A),
Incl l1 l2 -> Incl l2 l3 -> Incl l1 l3.
Lemma Incl_length :
forall (A : Type) (l1 l2 : list A),
~ Dup l1 -> Incl l1 l2 -> length l1 <= length l2.
Lemma Incl_snoc :
forall (A : Type) (x : A) (l : list A),
Incl l (snoc x l).
Lemma Incl_singl_snoc :
forall (A : Type) (x : A) (l : list A),
Incl [x] (snoc x l).
Lemma Incl_snoc_snoc :
forall (A : Type) (x : A) (l1 l2 : list A),
Incl l1 l2 -> Incl (snoc x l1) (snoc x l2).
Lemma Incl_app_rl :
forall (A : Type) (l l1 l2 : list A),
Incl l l2 -> Incl l (l1 ++ l2).
Lemma Incl_app_rr :
forall (A : Type) (l l1 l2 : list A),
Incl l l1 -> Incl l (l1 ++ l2).
Lemma Incl_app_l :
forall (A : Type) (l1 l2 l3 : list A),
Incl (l1 ++ l2) l3 <-> Incl l1 l3 /\ Incl l2 l3.
Lemma Incl_app_sym :
forall (A : Type) (l1 l2 l : list A),
Incl (l1 ++ l2) l -> Incl (l2 ++ l1) l.
Lemma Incl_rev :
forall (A : Type) (l : list A), Incl (rev l) l.
Lemma Incl_map :
forall (A B : Type) (f : A -> B) (l1 l2 : list A),
Incl l1 l2 -> Incl (map f l1) (map f l2).
Lemma Incl_join :
forall (A : Type) (l1 l2 : list (list A)),
Incl l1 l2 -> Incl (join l1) (join l2).
Lemma Incl_elem_join :
forall (A : Type) (ll : list (list A)) (l : list A),
elem l ll -> Incl l (join ll).
Lemma Incl_replicate :
forall (A : Type) (n : nat) (x : A) (l : list A),
elem x l -> Incl (replicate n x) l.
Lemma Incl_replicate' :
forall (A : Type) (n m : nat) (x : A),
n <> 0 -> Incl (replicate m x) (replicate n x).
Lemma Incl_nth :
forall (A : Type) (l1 l2 : list A),
Incl l1 l2 <->
forall (n1 : nat) (x : A), nth n1 l1 = Some x ->
exists n2 : nat, nth n2 l2 = Some x.
Lemma Incl_remove :
forall (A : Type) (l : list A) (n : nat),
match remove n l with
| None => True
| Some (_, l') => Incl l' l
end.
Lemma Incl_take :
forall (A : Type) (l : list A) (n : nat),
Incl (take n l) l.
Lemma Incl_drop :
forall (A : Type) (l : list A) (n : nat),
Incl (drop n l) l.
Lemma Incl_insert :
forall (A : Type) (l1 l2 : list A) (n m : nat) (x : A),
Incl l1 l2 -> Incl (insert l1 n x) (insert l2 m x).
Lemma Incl_replace :
forall (A : Type) (l1 l1' l2 : list A) (n : nat) (x : A),
Incl l1 l2 -> replace l1 n x = Some l1' ->
exists (m : nat) (l2' : list A),
replace l2 m x = Some l2' /\ Incl l1' l2'.
Lemma Incl_splitAt :
forall (A : Type) (l : list A) (n : nat),
match splitAt n l with
| None => True
| Some (l1, _, l2) => Incl l1 l /\ Incl l2 l
end.
Lemma Incl_filter :
forall (A : Type) (p : A -> bool) (l : list A),
Incl (filter p l) l.
Lemma Incl_filter_conv :
forall (A : Type) (p : A -> bool) (l : list A),
Incl l (filter p l) <-> filter p l = l.
Lemma Incl_takeWhile :
forall (A : Type) (p : A -> bool) (l : list A),
Incl (takeWhile p l) l.
Lemma Incl_takeWhile_conv :
forall (A : Type) (p : A -> bool) (l : list A),
Incl l (takeWhile p l) <-> takeWhile p l = l.
Lemma Incl_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A),
Incl (dropWhile p l) l.
Lemma Incl_span :
forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
span p l = Some (b, x, e) ->
Incl b l /\ elem x l /\ Incl e l.
Lemma Incl_pmap :
forall (A B : Type) (f : A -> option B) (l : list A),
Incl (map Some (pmap f l)) (map f l).
Lemma Incl_intersperse :
forall (A : Type) (x : A) (l1 l2 : list A),
Incl l1 (intersperse x l2) -> Incl l1 (x :: l2).
Lemma Incl_intersperse_conv :
forall (A : Type) (x : A) (l1 l2 : list A),
2 <= length l2 -> Incl l1 (x :: l2) -> Incl l1 (intersperse x l2).
Lemma groupBy_elem_incl :
forall (A : Type) (p : A -> A -> bool) (l g : list A),
elem g (groupBy p l) -> Incl g l.
Lemma Incl_In :
forall (A : Type) (l1 l2 : list A),
Incl l1 l2 -> forall x : A, In x l1 -> In x l2.
Lemma Incl_NoDup :
exists (A : Type) (l1 l2 : list A),
Incl l1 l2 /\ NoDup l2 /\ ~ NoDup l1.
Lemma Incl_Dup :
exists (A : Type) (l1 l2 : list A),
Incl l1 l2 /\ Dup l1 /\ ~ Dup l2.
Lemma Incl_Rep :
exists (A : Type) (x : A) (n : nat) (l1 l2 : list A),
Incl l1 l2 /\ Rep x n l1 /\ ~ Rep x n l2.
Lemma Incl_Exists :
forall (A : Type) (l1 l2 : list A),
Incl l1 l2 -> forall P : A -> Prop,
Exists P l1 -> Exists P l2.
Lemma Incl_Forall :
forall (A : Type) (l1 l2 : list A),
Incl l1 l2 -> forall P : A -> Prop,
Forall P l2 -> Forall P l1.
Lemma Incl_AtLeast :
exists (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
Incl l1 l2 /\ AtLeast P n l1 /\ ~ AtLeast P n l2.
Lemma Incl_Exactly :
exists (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
Incl l1 l2 /\ Exactly P n l1 /\ ~ Exactly P n l2.
Lemma Incl_AtMost :
exists (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
Incl l1 l2 /\ AtMost P n l2 /\ ~ AtMost P n l1.
Lemma Sublist_Incl :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 -> Incl l1 l2.
Lemma Incl_Sublist :
exists (A : Type) (l1 l2 : list A),
Incl l1 l2 /\ ~ Sublist l1 l2.
Lemma Prefix_Incl :
forall (A : Type) (l1 l2 : list A),
Prefix l1 l2 -> Incl l1 l2.
Lemma Incl_Prefix :
exists (A : Type) (l1 l2 : list A),
Incl l1 l2 /\ ~ Prefix l1 l2.
Lemma Subseq_Incl :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 -> Incl l1 l2.
Lemma Incl_Subseq :
exists (A : Type) (l1 l2 : list A),
Incl l1 l2 /\ ~ Subseq l1 l2.
Listy jako zbiory
Zdefiniuj relację
SetEquiv. Zdanie
SetEquiv l1 l2 zachodzi,
gdy listy
l1 i
l2 mają te same elementy, choć niekoniecznie
w tej samej kolejności czy ilości.
Przykłady:
SetEquiv [1; 1; 2] [2; 2; 1] zachodzi.
SetEquiv [1; 2; 3; 3] [2; 2; 3; 3; 4] nie zachodzi.
Lemma SetEquiv_Incl :
forall (A : Type) (l1 l2 : list A),
SetEquiv l1 l2 <-> Incl l1 l2 /\ Incl l2 l1.
Lemma SetEquiv_refl :
forall (A : Type) (l : list A), SetEquiv l l.
Lemma SetEquiv_sym :
forall (A : Type) (l1 l2 : list A),
SetEquiv l1 l2 <-> SetEquiv l2 l1.
Lemma SetEquiv_trans :
forall (A : Type) (l1 l2 l3 : list A),
SetEquiv l1 l2 -> SetEquiv l2 l3 -> SetEquiv l1 l3.
Lemma SetEquiv_nil_l :
forall (A : Type) (l : list A),
SetEquiv [] l -> l = [].
Lemma SetEquiv_nil_r :
forall (A : Type) (l : list A),
SetEquiv l [] -> l = [].
Lemma SetEquiv_cons :
forall (A : Type) (x : A) (l1 l2 : list A),
SetEquiv l1 l2 -> SetEquiv (x :: l1) (x :: l2).
Lemma SetEquiv_cons_conv :
exists (A : Type) (x : A) (l1 l2 : list A),
SetEquiv (x :: l1) (x :: l2) /\ ~ SetEquiv l1 l2.
Lemma SetEquiv_cons' :
exists (A : Type) (x : A) (l : list A),
~ SetEquiv l (x :: l).
Lemma SetEquiv_snoc_cons :
forall (A : Type) (x : A) (l : list A),
SetEquiv (snoc x l) (x :: l).
Lemma SetEquiv_snoc :
forall (A : Type) (x : A) (l1 l2 : list A),
SetEquiv l1 l2 -> SetEquiv (snoc x l1) (snoc x l2).
Lemma SetEquiv_app_comm :
forall (A : Type) (l1 l2 : list A),
SetEquiv (l1 ++ l2) (l2 ++ l1).
Lemma SetEquiv_app_l :
forall (A : Type) (l1 l2 l : list A),
SetEquiv l1 l2 -> SetEquiv (l ++ l1) (l ++ l2).
Lemma SetEquiv_app_r :
forall (A : Type) (l1 l2 l : list A),
SetEquiv l1 l2 -> SetEquiv (l1 ++ l) (l2 ++ l).
Lemma SetEquiv_rev :
forall (A : Type) (l : list A), SetEquiv (rev l) l.
Lemma SetEquiv_map :
forall (A B : Type) (f : A -> B) (l1 l2 : list A),
SetEquiv l1 l2 -> SetEquiv (map f l1) (map f l2).
Lemma SetEquiv_join :
forall (A : Type) (l1 l2 : list (list A)),
SetEquiv l1 l2 -> SetEquiv (join l1) (join l2).
Lemma SetEquiv_replicate :
forall (A : Type) (n : nat) (x : A),
SetEquiv (replicate n x) (if isZero n then [] else [x]).
Lemma SetEquiv_replicate' :
forall (A : Type) (n m : nat) (x : A),
m <> 0 -> n <> 0 -> SetEquiv (replicate m x) (replicate n x).
Lemma SetEquiv_nth :
forall (A : Type) (l1 l2 : list A),
SetEquiv l1 l2 <->
(forall n : nat, exists m : nat, nth n l1 = nth m l2) /\
(forall n : nat, exists m : nat, nth m l1 = nth n l2).
Lemma SetEquiv_take :
forall (A : Type) (l : list A) (n : nat),
SetEquiv (take n l) l <-> Incl (drop n l) (take n l).
Lemma SetEquiv_drop :
forall (A : Type) (n : nat) (l : list A),
SetEquiv (drop n l) l <-> Incl (take n l) (drop n l).
Lemma SetEquiv_filter :
forall (A : Type) (p : A -> bool) (l : list A),
SetEquiv (filter p l) l <-> all p l = true.
Lemma SetEquiv_filter' :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
SetEquiv l1 l2 -> SetEquiv (filter p l1) (filter p l2).
Lemma SetEquiv_takeWhile :
forall (A : Type) (p : A -> bool) (l : list A),
SetEquiv (takeWhile p l) l <-> all p l = true.
Lemma SetEquiv_dropWhile :
exists (A : Type) (p : A -> bool) (l : list A),
SetEquiv (dropWhile p l) l /\ any p l = true.
Lemma SetEquiv_pmap :
exists (A B : Type) (f : A -> option B) (l : list A),
~ SetEquiv (map Some (pmap f l)) (map f l).
Lemma SetEquiv_intersperse :
forall (A : Type) (x : A) (l : list A),
2 <= length l -> SetEquiv (intersperse x l) (x :: l).
Lemma SetEquiv_intersperse_conv :
forall (A : Type) (x : A) (l : list A),
SetEquiv (intersperse x l) (x :: l) ->
elem x l \/ 2 <= length l.
Lemma SetEquiv_singl :
forall (A : Type) (l : list A) (x : A),
SetEquiv [x] l -> forall y : A, elem y l -> y = x.
Lemma SetEquiv_pres_intersperse :
exists (A : Type) (x : A) (l1 l2 : list A),
SetEquiv l1 l2 /\ ~ SetEquiv (intersperse x l1) (intersperse x l2).
Require Export Coq.Classes.SetoidClass.
Require Import Coq.Classes.RelationClasses.
Zdefiniuj induktywną relację
Permutation. Zdanie
Permutation l1 l2 zachodzi, gdy listy
l1 i
l2 mają te same
elementy w tej samej ilości sztuk, ale niekoniecznie w tej samej
kolejności.
Przykłady:
Permutation [1; 5; 1; 4; 3] [4; 1; 1; 5; 3] zachodzi.
Permutation [0; 0; 2; 6; 7] [7; 0; 2; 0; 6; 0] nie zachodzi.
Uwaga: to zadanie jest dużo trudniejsze od reszty zadań dotyczących
relacji między listami. Jeżeli masz problem z rozwiązaniem, spróbuj
poszukać gotowca w bibliotece standardowej Coqa.
Lemma Permutation_refl :
forall (A : Type) (l : list A),
Permutation l l.
Lemma Permutation_trans :
forall (A : Type) (l1 l2 l3 : list A),
Permutation l1 l2 -> Permutation l2 l3 -> Permutation l1 l3.
Lemma Permutation_sym :
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 -> Permutation l2 l1.
#[export]
Instance Permutation_Equivalence:
forall A : Type, RelationClasses.Equivalence (Permutation (A := A)).
Lemma Permutation_isEmpty :
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 -> isEmpty l1 = isEmpty l2.
Lemma Permutation_nil_l :
forall (A : Type) (l : list A),
Permutation [] l -> l = [].
Lemma Permutation_nil_r :
forall (A : Type) (l : list A),
Permutation l [] -> l = [].
Lemma Permutation_nil_cons_l :
forall (A : Type) (l : list A) (x : A),
~ Permutation [] (x :: l).
Lemma Permutation_nil_cons_r :
forall (A : Type) (l : list A) (x : A),
~ Permutation (x :: l) [].
Lemma Permutation_nil_app_cons_l :
forall (A : Type) (l l' : list A) (x : A),
~ Permutation [] (l ++ x :: l').
#[export]
Instance Permutation_cons :
forall A : Type,
Proper (eq ==> @Permutation A ==> @Permutation A) (@cons A).
Lemma Permutation_ind' :
forall (A : Type) (P : list A -> list A -> Prop),
P [] [] ->
(forall x l l', Permutation l l' -> P l l' -> P (x :: l) (x :: l')) ->
(forall x y l l', Permutation l l' -> P l l' ->
P (y :: x :: l) (x :: y :: l')) ->
(forall l l' l'', Permutation l l' -> P l l' -> Permutation l' l'' ->
P l' l'' -> P l l'') ->
forall l l', Permutation l l' -> P l l'.
Inductive Elem {A : Type} (x : A) : list A -> list A -> Prop :=
| es_here :
forall l : list A, Elem x l (x :: l)
| es_there :
forall (y : A) (l1 l2 : list A),
Elem x l1 l2 -> Elem x (y :: l1) (y :: l2).
Lemma Elem_spec :
forall (A : Type) (x : A) (l1 l2 : list A),
Elem x l1 l2 -> exists l21 l22 : list A,
l2 = l21 ++ x :: l22 /\ l1 = l21 ++ l22.
Lemma Permutation_Elem :
forall (A : Type) (x : A) (l l' : list A),
Elem x l l' -> Permutation l' (x :: l).
Lemma Elem_Permutation :
forall (A : Type) (x : A) (l1 l1' : list A),
Elem x l1 l1' -> forall l2' : list A,
Permutation l1' l2' -> exists l2 : list A, Elem x l2 l2'.
Lemma Permutation_Elems :
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 -> forall (x : A) (l1' l2' : list A),
Elem x l1' l1 -> Elem x l2' l2 ->
Permutation l1' l2'.
Lemma Permutation_cons_inv :
forall (A : Type) (l1 l2 : list A) (x : A),
Permutation (x :: l1) (x :: l2) -> Permutation l1 l2.
Lemma Permutation_length :
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 -> length l1 = length l2.
Lemma Permutation_length' :
forall A : Type,
Proper (@Permutation A ==> eq) (@length A).
Lemma Permutation_length_1:
forall (A : Type) (l1 l2 : list A),
length l1 = 1 -> Permutation l1 l2 -> l1 = l2.
Lemma Permutation_singl :
forall (A : Type) (a b : A),
Permutation [a] [b] -> a = b.
Lemma Permutation_length_1_inv:
forall (A : Type) (x : A) (l : list A),
Permutation [x] l -> l = [x].
Lemma Permutation_snoc :
forall (A : Type) (x : A) (l1 l2 : list A),
Permutation l1 l2 -> Permutation (snoc x l1) (snoc x l2).
Lemma Permutation_cons_snoc :
forall (A : Type) (l : list A) (x : A),
Permutation (x :: l) (snoc x l).
Lemma Permutation_cons_snoc' :
forall (A : Type) (l : list A) (x : A),
Permutation (x :: l) (l ++ [x]).
Lemma Permutation_app_l :
forall (A : Type) (l1 l2 l3 : list A),
Permutation l1 l2 -> Permutation (l3 ++ l1) (l3 ++ l2).
Lemma Permutation_app_r :
forall (A : Type) (l1 l2 l3 : list A),
Permutation l1 l2 -> Permutation (l1 ++ l3) (l2 ++ l3).
Lemma Permutation_app :
forall (A : Type) (l1 l1' l2 l2' : list A),
Permutation l1 l1' -> Permutation l2 l2' ->
Permutation (l1 ++ l2) (l1' ++ l2').
#[export]
Instance Permutation_app':
forall A : Type,
Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A).
Lemma Permutation_add_inside :
forall (A : Type) (x : A) (l1 l2 l1' l2' : list A),
Permutation l1 l1' -> Permutation l2 l2' ->
Permutation (l1 ++ x :: l2) (l1' ++ x :: l2').
Lemma Permutation_cons_middle :
forall (A : Type) (l1 l2 l3 : list A) (x : A),
Permutation l1 (l2 ++ l3) -> Permutation (x :: l1) (l2 ++ x :: l3).
Lemma Permutation_middle :
forall (A : Type) (l1 l2 : list A) (x : A),
Permutation (l1 ++ x :: l2) (x :: (l1 ++ l2)).
Lemma Permutation_app_comm :
forall (A : Type) (l1 l2 : list A),
Permutation (l1 ++ l2) (l2 ++ l1).
Lemma Permutation_app_inv_l :
forall (A : Type) (l1 l2 l3 : list A),
Permutation (l1 ++ l2) (l1 ++ l3) -> Permutation l2 l3.
Lemma Permutation_app_inv_r :
forall (A : Type) (l1 l2 l3 : list A),
Permutation (l1 ++ l3) (l2 ++ l3) -> Permutation l1 l2.
Lemma Permutation_rev :
forall (A : Type) (l : list A),
Permutation (rev l) l.
#[export]
Instance Permutation_rev' :
forall A : Type,
Proper (@Permutation A ==> @Permutation A) (@rev A).
Lemma Permutation_map:
forall (A B : Type) (f : A -> B) (l1 l2 : list A),
Permutation l1 l2 -> Permutation (map f l1) (map f l2).
Lemma Permutation_map':
forall (A B : Type) (f : A -> B),
Morphisms.Proper
(Morphisms.respectful (Permutation (A:=A)) (Permutation (A:=B)))
(map f).
Lemma Permutation_join :
forall (A : Type) (l1 l2 : list (list A)),
Permutation l1 l2 -> Permutation (join l1) (join l2).
Lemma Permutation_join_rev :
exists (A : Type) (l1 l2 : list (list A)),
Permutation (join l1) (join l2) /\ ~ Permutation l1 l2.
Lemma Permutation_replicate :
forall (A : Type) (n m : nat) (x : A),
Permutation (replicate n x) (replicate m x) <-> n = m.
Lemma Permutation_In :
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 -> (forall x : A, In x l1 <-> In x l2).
Lemma Permutation_in :
forall (A : Type) (l l' : list A) (x : A),
Permutation l l' -> In x l -> In x l'.
Lemma Permutation_in' :
forall A : Type,
Proper (eq ==> @Permutation A ==> iff) (@In A).
Lemma Permutation_replicate' :
forall (A : Type) (n : nat) (x y : A),
Permutation (replicate n x) (replicate n y) <-> n = 0 \/ x = y.
Lemma Permutation_iterate :
forall (A : Type) (f : A -> A) (n m : nat) (x : A),
Permutation (iterate f n x) (iterate f m x) <-> n = m.
Lemma Permutation_iterate' :
forall (A : Type) (f : A -> A) (n : nat) (x y : A),
Permutation (iterate f n x) (iterate f n y) ->
n = 0 \/ exists k : nat, k < n /\ iter f k y = x.
Lemma Permutation_insert :
forall (A : Type) (l : list A) (n : nat) (x : A),
Permutation (insert l n x) (x :: l).
Lemma Permutation_take :
exists (A : Type) (l1 l2 : list A),
Permutation l1 l2 /\
exists n : nat, ~ Permutation (take n l1) (take n l2).
Lemma Permutation_drop :
exists (A : Type) (l1 l2 : list A),
Permutation l1 l2 /\
exists n : nat, ~ Permutation (drop n l1) (drop n l2).
Lemma Permutation_cycle :
forall (A : Type) (n : nat) (l : list A),
Permutation (cycle n l) l.
Lemma Permutation_filter_cycle :
forall (A : Type) (p : A -> bool) (n : nat) (l : list A),
Permutation (filter p (cycle n l)) (filter p l).
Lemma Permutation_length_2_inv:
forall (A : Type) (x y : A) (l : list A),
Permutation [x; y] l -> l = [x; y] \/ l = [y; x].
Lemma Permutation_length_2:
forall (A : Type) (x1 x2 y1 y2 : A),
Permutation [x1; x2] [y1; y2] ->
x1 = y1 /\ x2 = y2 \/ x1 = y2 /\ x2 = y1.
Lemma Permutation_zip :
exists (A B : Type) (la1 la2 : list A) (lb1 lb2 : list B),
Permutation la1 la2 /\ Permutation lb1 lb2 /\
~ Permutation (zip la1 lb1) (zip la2 lb2).
Lemma Permutation_zipWith :
exists
(A B C : Type) (f : A -> B -> C)
(la1 la2 : list A) (lb1 lb2 : list B),
Permutation la1 la2 /\
Permutation lb1 lb2 /\
~ Permutation (zipWith f la1 lb1) (zipWith f la2 lb2).
Lemma Permutation_any :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Permutation l1 l2 -> any p l1 = any p l2.
Lemma Permutation_all :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Permutation l1 l2 -> all p l1 = all p l2.
Lemma Permutation_count :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Permutation l1 l2 -> count p l1 = count p l2.
Lemma Permutation_count_replicate_filter :
forall (A : Type) (p : A -> bool) (l b e : list A) (x : A),
span p l = Some (b, x, e) ->
Permutation l (replicate (count p l) x ++ b ++ e).
Lemma Permutation_count_conv :
forall (A : Type) (l1 l2 : list A),
(forall p : A -> bool, count p l1 = count p l2) -> Permutation l1 l2.
Lemma Permutation_filter :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Permutation l1 l2 -> Permutation (filter p l1) (filter p l2).
Lemma Permutation_takeWhile :
exists (A : Type) (p : A -> bool) (l1 l2 : list A),
Permutation l1 l2 /\
~ Permutation (takeWhile p l1) (takeWhile p l2).
Lemma Permutation_dropWhile :
exists (A : Type) (p : A -> bool) (l1 l2 : list A),
Permutation l1 l2 /\
~ Permutation (dropWhile p l1) (dropWhile p l2).
Lemma Permutation_span :
forall (A : Type) (p : A -> bool) (l b e : list A) (x : A),
span p l = Some (b, x, e) -> Permutation l (b ++ x :: e).
Lemma Permutation_removeFirst :
forall (A : Type) (p : A -> bool) (l l' : list A) (x : A),
removeFirst p l = Some (x, l') -> Permutation l (x :: l').
Lemma Permutation_intersperse_replicate :
forall (A : Type) (x : A) (l : list A),
Permutation (intersperse x l) (replicate (length l - 1) x ++ l).
Lemma Permutation_intersperse :
forall (A : Type) (x : A) (l1 l2 : list A),
Permutation (intersperse x l1) (intersperse x l2) <->
Permutation l1 l2.
Lemma Permutation_pmap :
forall (A B : Type) (f : A -> option B) (l1 l2 : list A),
Permutation l1 l2 -> Permutation (pmap f l1) (pmap f l2).
Lemma Permutation_elem :
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 ->
forall x : A, elem x l1 <-> elem x l2.
Lemma Permutation_replicate'' :
forall (A : Type) (n m : nat) (x y : A),
Permutation (replicate n x) (replicate m y) <->
n = m /\ (n <> 0 -> m <> 0 -> x = y).
Lemma NoDup_Permutation:
forall (A : Type) (l1 l2 : list A),
NoDup l1 -> NoDup l2 ->
(forall x : A, In x l1 <-> In x l2) -> Permutation l1 l2.
Lemma NoDup_Permutation_bis:
forall (A : Type) (l1 l2 : list A),
NoDup l1 -> NoDup l2 -> length l2 <= length l1 ->
Incl l1 l2 -> Permutation l1 l2.
Lemma Permutation_NoDup:
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 -> NoDup l1 -> NoDup l2.
Lemma Permutation_NoDup':
forall A : Type,
Morphisms.Proper
(Morphisms.respectful (Permutation (A:=A)) iff)
(NoDup (A:=A)).
Lemma Permutation_Dup :
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 -> Dup l1 <-> Dup l2.
Lemma Permutation_Rep :
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 ->
forall (x : A) (n : nat), Rep x n l1 <-> Rep x n l2.
Lemma Permutation_Exists :
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 ->
forall P : A -> Prop, Exists P l1 <-> Exists P l2.
Lemma Permutation_Exists_conv :
exists (A : Type) (l1 l2 : list A),
(forall P : A -> Prop, Exists P l1 <-> Exists P l2) /\
~ Permutation l1 l2.
Lemma Permutation_Forall :
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 ->
forall P : A -> Prop, Forall P l1 <-> Forall P l2.
Lemma Permutation_AtLeast :
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 ->
forall (P : A -> Prop) (n : nat), AtLeast P n l1 <-> AtLeast P n l2.
Lemma Permutation_Exactly :
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 ->
forall (P : A -> Prop) (n : nat), Exactly P n l1 <-> Exactly P n l2.
Lemma Permutation_AtMost :
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 ->
forall (P : A -> Prop) (n : nat), AtMost P n l1 <-> AtMost P n l2.
Lemma Permutation_Sublist :
exists (A : Type) (l1 l2 : list A),
Permutation l1 l2 /\ ~ Sublist l1 l2.
Lemma Sublist_Permutation :
exists (A : Type) (l1 l2 : list A),
Sublist l1 l2 /\ ~ Permutation l1 l2.
Lemma Permutation_Prefix :
exists (A : Type) (l1 l2 : list A),
Permutation l1 l2 /\ ~ Prefix l1 l2.
Lemma Prefix_Permutation :
exists (A : Type) (l1 l2 : list A),
Prefix l1 l2 /\ ~ Permutation l1 l2.
Lemma Permutation_Subseq :
exists (A : Type) (l1 l2 : list A),
Permutation l1 l2 /\ ~ Subseq l1 l2.
Lemma Subseq_Permutation :
exists (A : Type) (l1 l2 : list A),
Subseq l1 l2 /\ ~ Permutation l1 l2.
Lemma Permutation_Incl :
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 -> Incl l1 l2.
Lemma Permutation_SetEquiv :
forall (A : Type) (l1 l2 : list A),
Permutation l1 l2 -> SetEquiv l1 l2.
Listy jako cykle
Zdefiniuj induktywną relację
Cycle. Zdanie
Cycle l1 l2 zachodzi,
gdy listy
l1 i
l2 reprezentują ten sam cykl. Intuicyjnie możesz
sobie wyobrazić elementy
l1 ułożone po kolei wzdłuż okręgu tak, że
ostatni element sąsiaduje z pierwszym. Jeżeli da się teraz przekręcić
ten okrąg tak, żeby uzyskać listę
l2, to znaczy, że
Cycle l1 l2
zachodzi.
Przykłady:
Cycle [1; 2; 3; 4; 5] [4; 5; 1; 2; 3] zachodzi.
Cycle [1; 2; 3] [2; 1; 3] nie zachodzi.
Lemma lt_plus_S :
forall n m : nat,
n < m -> exists k : nat, m = S (n + k).
Lemma Cycle_spec :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 <->
exists n : nat, n <= length l1 /\ l1 = drop n l2 ++ take n l2.
Lemma Cycle_isEmpty :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> isEmpty l1 = isEmpty l2.
Lemma Cycle_nil_l :
forall (A : Type) (l : list A),
Cycle [] l -> l = [].
Lemma Cycle_nil_r :
forall (A : Type) (l : list A),
Cycle l [] -> l = [].
Lemma Cycle_length :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> length l1 = length l2.
Lemma Cycle_cons :
exists (A : Type) (x : A) (l1 l2 : list A),
Cycle l1 l2 /\ ~ Cycle (x :: l1) (x :: l2).
Lemma Cycle_cons_inv :
exists (A : Type) (x : A) (l1 l2 : list A),
Cycle (x :: l1) (x :: l2) /\ ~ Cycle l1 l2.
Lemma Cycle_snoc :
exists (A : Type) (x : A) (l1 l2 : list A),
Cycle l1 l2 /\ ~ Cycle (snoc x l1) (snoc x l2).
Lemma Cycle_sym :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> Cycle l2 l1.
Lemma Cycle_snoc_cons :
forall (A : Type) (x : A) (l : list A),
Cycle (snoc x l) (x :: l).
Lemma Cycle_cons_snoc :
forall (A : Type) (x : A) (l : list A),
Cycle (x :: l) (snoc x l).
Lemma Cycle_cons_snoc' :
forall (A : Type) (x : A) (l1 l2 : list A),
Cycle l1 (x :: l2) -> Cycle l1 (snoc x l2).
Lemma Cycle_trans :
forall (A : Type) (l1 l2 l3 : list A),
Cycle l1 l2 -> Cycle l2 l3 -> Cycle l1 l3.
Lemma Cycle_app :
forall (A : Type) (l1 l2 l3 : list A),
Cycle l1 (l2 ++ l3) -> Cycle l1 (l3 ++ l2).
Lemma Cycle_rev :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> Cycle (rev l1) (rev l2).
Lemma Cycle_map :
forall (A B : Type) (f : A -> B) (l1 l2 : list A),
Cycle l1 l2 -> Cycle (map f l1) (map f l2).
Lemma Cycle_join :
forall (A : Type) (l1 l2 : list (list A)),
Cycle l1 l2 -> Cycle (join l1) (join l2).
Lemma Cycle_replicate :
forall (A : Type) (n m : nat) (x : A),
Cycle (replicate n x) (replicate m x) <-> n = m.
Lemma Cycle_iterate :
forall (A : Type) (f : A -> A) (n m : nat) (x : A),
Cycle (iterate f n x) (iterate f m x) <-> n = m.
Lemma Cycle_iterate' :
forall (A : Type) (f : A -> A) (n m : nat) (x y : A),
Cycle (iterate f n x) (iterate f m y) <-> n = m.
Lemma Cycle_nth :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> forall (n : nat) (x : A),
nth n l1 = Some x -> exists m : nat, nth m l2 = Some x.
Lemma Cycle_cycle :
forall (A : Type) (n : nat) (l : list A),
Cycle (cycle n l) l.
Lemma cycle_Cycle :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> exists n : nat, cycle n l1 = l2.
Lemma Cycle_insert :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> forall (n : nat) (x : A),
exists m : nat, Cycle (insert l1 n x) (insert l2 m x) .
Lemma Cycle_zip :
exists (A B : Type) (la1 la2 : list A) (lb1 lb2 : list B),
Cycle la1 la2 /\ Cycle lb1 lb2 /\ ~ Cycle (zip la1 lb1) (zip la2 lb2).
Lemma Cycle_any :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Cycle l1 l2 -> any p l1 = any p l2.
Lemma Cycle_all :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Cycle l1 l2 -> all p l1 = all p l2.
Lemma Cycle_find :
exists (A : Type) (p : A -> bool) (l1 l2 : list A) (x : A),
Cycle l1 l2 /\ find p l1 = Some x /\ find p l2 <> Some x.
Lemma Cycle_findIndex :
exists (A : Type) (p : A -> bool) (l1 l2 : list A) (n : nat),
Cycle l1 l2 /\ findIndex p l1 = Some n /\ findIndex p l2 <> Some n.
Lemma Cycle_count :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Cycle l1 l2 -> count p l1 = count p l2.
Lemma Cycle_filter :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
Cycle l1 l2 -> Cycle (filter p l1) (filter p l2).
Lemma Cycle_takeWhile :
exists (A : Type) (p : A -> bool) (l1 l2 : list A),
Cycle l1 l2 /\ ~ Cycle (takeWhile p l1) (takeWhile p l2).
Lemma Cycle_dropWhile :
exists (A : Type) (p : A -> bool) (l1 l2 : list A),
Cycle l1 l2 /\ ~ Cycle (dropWhile p l1) (dropWhile p l2).
Lemma Cycle_pmap :
forall (A B : Type) (f : A -> option B) (l1 l2 : list A),
Cycle l1 l2 -> Cycle (pmap f l1) (pmap f l2).
Lemma Cycle_intersperse :
exists (A : Type) (x : A) (l1 l2 : list A),
Cycle l1 l2 /\ ~ Cycle (intersperse x l1) (intersperse x l2).
Lemma Cycle_Permutation :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> Permutation l1 l2.
Lemma Cycle_elem :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> forall x : A, elem x l1 <-> elem x l2.
Lemma Cycle_replicate' :
forall (A : Type) (n m : nat) (x y : A),
Cycle (replicate n x) (replicate m y) <->
n = m /\ (n <> 0 -> m <> 0 -> x = y).
Lemma Cycle_In :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> forall x : A, In x l1 <-> In x l2.
Lemma Cycle_NoDup :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> NoDup l1 -> NoDup l2.
Lemma Cycle_Dup :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> Dup l1 -> Dup l2.
Lemma Cycle_Rep :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> forall (x : A) (n : nat),
Rep x n l1 -> Rep x n l2.
Lemma Cycle_Exists :
forall (A : Type) (P : A -> Prop) (l1 l2 : list A),
Cycle l1 l2 -> Exists P l1 -> Exists P l2.
Lemma Cycle_Forall :
forall (A : Type) (P : A -> Prop) (l1 l2 : list A),
Cycle l1 l2 -> Forall P l1 -> Forall P l2.
Lemma Cycle_AtLeast :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> forall (P : A -> Prop) (n : nat),
AtLeast P n l1 -> AtLeast P n l2.
Lemma Cycle_Exactly :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> forall (P : A -> Prop) (n : nat),
Exactly P n l1 -> Exactly P n l2.
Lemma Cycle_AtMost :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> forall (P : A -> Prop) (n : nat),
AtMost P n l1 -> AtMost P n l2.
Lemma Cycle_Sublist :
exists (A : Type) (l1 l2 : list A),
Cycle l1 l2 /\ ~ Sublist l1 l2.
Lemma Sublist_Cycle :
exists (A : Type) (l1 l2 : list A),
Sublist l1 l2 /\ ~ Cycle l1 l2.
Lemma Cycle_Prefix :
exists (A : Type) (l1 l2 : list A),
Cycle l1 l2 /\ ~ Prefix l1 l2.
Lemma Prefix_Cycle :
exists (A : Type) (l1 l2 : list A),
Prefix l1 l2 /\ ~ Cycle l1 l2.
Lemma Cycle_Subseq :
exists (A : Type) (l1 l2 : list A),
Cycle l1 l2 /\ ~ Subseq l1 l2.
Lemma Subseq_Cycle :
exists (A : Type) (l1 l2 : list A),
Subseq l1 l2 /\ ~ Cycle l1 l2.
Lemma Cycle_Incl :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> Incl l1 l2.
Lemma Incl_Cycle :
exists (A : Type) (l1 l2 : list A),
Incl l1 l2 /\ ~ Cycle l1 l2.
Lemma Cycle_SetEquiv :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> SetEquiv l1 l2.
Lemma SetEquiv_Cycle :
exists (A : Type) (l1 l2 : list A),
SetEquiv l1 l2 /\ ~ Cycle l1 l2.
Module Partition.
Definition Partition
{A : Type} (ll : list (list A)) (l : list A) : Prop :=
Permutation (join ll) l.
Lemma Partition_rev :
forall {A : Type} (ll : list (list A)) (l : list A),
Partition ll l -> Partition (rev (map rev ll)) (rev l).
Proof.
unfold Partition. intros.
rewrite <- rev_join, !Permutation_rev.
assumption.
Qed.
End Partition.
Module OPartition.
Record OPartition
{A : Type} (ll : list (list A)) (l : list A) : Prop :=
{
nonempty : forall l' : list A, elem l' ll -> l' <> [];
all : join ll = l;
}.
End OPartition.
Module IPartition.
Inductive IPartition {A : Type} : list (list A) -> list A -> Prop :=
| IP_nil : IPartition [] []
| IP_cons :
forall {ll : list (list A)} {l1 l2 : list A},
l1 <> [] -> IPartition ll l2 ->
IPartition (l1 :: ll) (l1 ++ l2).
Lemma IPartition_spec :
forall {A : Type} {ll : list (list A)} {l : list A},
IPartition ll l -> join ll = l.
Proof.
induction 1; cbn.
reflexivity.
rewrite IHIPartition. reflexivity.
Qed.
Lemma IPartition_spec_conv :
forall {A : Type} (ll : list (list A)) (l : list A),
(forall l' : list A, elem l' ll -> l' <> []) ->
join ll = l -> IPartition ll l.
Proof.
induction ll as [| hh tt]; cbn; intros; subst.
constructor.
constructor.
apply H. constructor.
apply IHtt.
intros. apply H. constructor. assumption.
reflexivity.
Qed.
Lemma IPartition_app :
forall {A : Type} (ll1 ll2 : list (list A)) (l1 l2 : list A),
IPartition ll1 l1 -> IPartition ll2 l2 ->
IPartition (ll1 ++ ll2) (l1 ++ l2).
Proof.
intros until 1. revert ll2 l2.
induction H; cbn; intros.
assumption.
rewrite <- app_assoc. constructor.
assumption.
apply IHIPartition. assumption.
Qed.
Lemma IPartition_rev :
forall {A : Type} (ll : list (list A)) (l : list A),
IPartition ll l -> IPartition (map rev (rev ll)) (rev l).
Proof.
induction 1; cbn.
constructor.
rewrite map_snoc, rev_app, snoc_app_singl. apply IPartition_app.
assumption.
rewrite <- app_nil_r. constructor.
intro. apply H. destruct l1.
reflexivity.
apply (f_equal length) in H1. rewrite length_rev in H1.
cbn in H1. inv H1.
constructor.
Qed.
Lemma IPartition_map :
forall {A B : Type} {ll : list (list A)} {l : list A},
IPartition ll l ->
forall f : A -> B, IPartition (map (map f) ll) (map f l).
Proof.
induction 1; cbn; intros.
constructor.
rewrite map_app. constructor.
intro. apply H. destruct l1.
reflexivity.
inv H1.
apply IHIPartition.
Qed.
End IPartition.
Rozstrzyganie relacji na listach (TODO)
Fixpoint Sublist_dec
{A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
match l2 with
| [] => false
| h2 :: t2 =>
list_eq_dec eq_dec l1 t2 || Sublist_dec eq_dec l1 t2
end.
Lemma Sublist_dec_spec :
forall
(A : Type) (eq_dec : A -> A -> bool)
(eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
(l1 l2 : list A),
reflect (Sublist l1 l2) (Sublist_dec eq_dec l1 l2).
Fixpoint Prefix_dec
{A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
match l1, l2 with
| [], _ => true
| _, [] => false
| h1 :: t1, h2 :: t2 => eq_dec h1 h2 && Prefix_dec eq_dec t1 t2
end.
Lemma Prefix_dec_spec :
forall
{A : Type} {eq_dec : A -> A -> bool}
(eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
(l1 l2 : list A),
reflect (Prefix l1 l2) (Prefix_dec eq_dec l1 l2).
Definition Suffix_dec
{A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
Prefix_dec eq_dec (rev l1) (rev l2).
Lemma Suffix_dec_spec :
forall
{A : Type} {eq_dec : A -> A -> bool}
(eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
(l1 l2 : list A),
reflect (Suffix l1 l2) (Suffix_dec eq_dec l1 l2).
Fixpoint Subseq_dec
{A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
match l1, l2 with
| [], _ => true
| _, [] => false
| h1 :: t1, h2 :: t2 =>
(eq_dec h1 h2 && Subseq_dec eq_dec t1 t2) ||
Subseq_dec eq_dec l1 t2
end.
Lemma Subseq_dec_spec :
forall
{A : Type} {eq_dec : A -> A -> bool}
(eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
(l1 l2 : list A),
reflect (Subseq l1 l2) (Subseq_dec eq_dec l1 l2).
Fixpoint Incl_dec
{A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
match l1 with
| [] => true
| h :: t => elem_dec eq_dec h l2 && Incl_dec eq_dec t l2
end.
Lemma Incl_dec_spec :
forall
{A : Type} {eq_dec : A -> A -> bool}
(eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
(l1 l2 : list A),
reflect (Incl l1 l2) (Incl_dec eq_dec l1 l2).
Definition SetEquiv_dec
{A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
Incl_dec eq_dec l1 l2 && Incl_dec eq_dec l2 l1.
Lemma SetEquiv_dec_spec :
forall
{A : Type} {eq_dec : A -> A -> bool}
(eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
(l1 l2 : list A),
reflect (SetEquiv l1 l2) (SetEquiv_dec eq_dec l1 l2).
Fixpoint Permutation_dec
{A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
match l1 with
| [] => isEmpty l2
| h :: t =>
match removeFirst (eq_dec h) l2 with
| None => false
| Some (_, l2') => Permutation_dec eq_dec t l2'
end
end.
Lemma Permutation_dec_spec :
forall
{A : Type} {eq_dec : A -> A -> bool}
(eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
(l1 l2 : list A),
reflect (Permutation l1 l2) (Permutation_dec eq_dec l1 l2).
Fixpoint Cycle_dec_aux
{A : Type} (eq_dec : A -> A -> bool) (n : nat) (l1 l2 : list A) : bool :=
match n with
| 0 => list_eq_dec eq_dec l1 l2
| S n' =>
list_eq_dec eq_dec l1 (drop n l2 ++ take n l2) ||
Cycle_dec_aux eq_dec n' l1 l2
end.
Definition Cycle_dec
{A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
Cycle_dec_aux eq_dec (length l1) l1 l2.
Lemma Cycle_dec_aux_spec :
forall
{A : Type} {eq_dec : A -> A -> bool}
(eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
(m : nat) (l1 l2 : list A),
reflect
(exists n : nat, n <= m /\ l1 = drop n l2 ++ take n l2)
(Cycle_dec_aux eq_dec m l1 l2).
Lemma Cycle_dec_spec :
forall
{A : Type} {eq_dec : A -> A -> bool}
(eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
(m : nat) (l1 l2 : list A),
reflect (Cycle l1 l2) (Cycle_dec eq_dec l1 l2).
Definition Palindrome_dec
{A : Type} (eq_dec : A -> A -> bool) (l : list A) : bool :=
list_eq_dec eq_dec l (rev l).
Lemma Palindrome_dec_spec :
forall
{A : Type} {eq_dec : A -> A -> bool}
(eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
(l : list A),
reflect (Palindrome l) (Palindrome_dec eq_dec l).
Znajdowanie wszystkich podstruktur (TODO)
Podlisty/podtermy
Module sublists.
Fixpoint sublists {A : Type} (l : list A) : list (list A) :=
match l with
| [] => []
| h :: t => t :: sublists t
end.
Lemma sublists_spec :
forall {A : Type} (l1 l2 : list A),
Sublist l1 l2 -> elem l1 (sublists l2).
Lemma sublists_spec' :
forall {A : Type} (l1 l2 : list A),
elem l1 (sublists l2) -> Sublist l1 l2.
End sublists.
Module suffixes.
Fixpoint suffixes {A : Type} (l : list A) : list (list A) :=
l ::
match l with
| [] => []
| h :: t => suffixes t
end.
Lemma suffixes_spec :
forall {A : Type} (l1 l2 : list A),
Suffix l1 l2 -> elem l1 (suffixes l2).
Lemma suffixes_spec' :
forall {A : Type} (l1 l2 : list A),
elem l1 (suffixes l2) -> Suffix l1 l2.
End suffixes.
Module prefixes.
Import suffixes.
Fixpoint prefixes {A : Type} (l : list A) : list (list A) :=
[] ::
match l with
| [] => []
| h :: t => map (cons h) (prefixes t)
end.
Lemma prefixes_spec :
forall {A : Type} (l1 l2 : list A),
Prefix l1 l2 -> elem l1 (prefixes l2).
Lemma elem_map_cons :
forall {A : Type} (h1 h2 : A) (t1 : list A) (t2 : list (list A)),
elem (h1 :: t1) (map (cons h2) t2) -> h1 = h2.
Lemma prefixes_spec' :
forall {A : Type} (l1 l2 : list A),
elem l1 (prefixes l2) -> Prefix l1 l2.
End prefixes.
Module subseqs.
Fixpoint subseqs {A : Type} (l : list A) : list (list A) :=
match l with
| [] => [[]]
| h :: t => map (cons h) (subseqs t) ++ subseqs t
end.
Compute subseqs [1; 2; 3; 4; 5].
Lemma Subseq_subseqs :
forall (A : Type) (l1 l2 : list A),
Subseq l1 l2 -> elem l1 (subseqs l2).
Lemma subseqs_Subseq :
forall (A : Type) (l1 l2 : list A),
elem l1 (subseqs l2) -> Subseq l1 l2.
End subseqs.
Module subsets.
Fixpoint subsets {A : Type} (l : list A) : list (list A) :=
match l with
| [] => [[]]
| h :: t => subsets t ++ map (cons h) (subsets t)
end.
Import prefixes.
End subsets.
Module cycles.
Fixpoint cycles_aux {A : Type} (n : nat) (l : list A) : list (list A) :=
match n with
| 0 => []
| S n' => cycle n l :: cycles_aux n' l
end.
Compute cycles_aux 0 [1; 2; 3; 4; 5].
Compute cycles_aux 5 [1; 2; 3; 4; 5].
Definition cycles {A : Type} (l : list A) : list (list A) :=
match l with
| [] => [[]]
| _ => cycles_aux (length l) l
end.
Compute cycles [].
Compute cycles [1].
Compute cycles [1; 2; 3; 4; 5].
Lemma Cycle_cycles_aux :
forall (A : Type) (l1 l2 : list A),
Cycle l1 l2 -> forall n : nat,
elem l1 (cycles_aux (S (length l2) + n) l2).
End cycles.