D5: Listy
Lista to najprostsza i najczęściej używana w programowaniu funkcyjnym
struktura danych. Czas więc przeżyć na własnej skórze ich implementację.
UWAGA: ten rozdział wyewoluował do stanu dość mocno odbiegającego od
tego, co jest w bibliotece standardowej — moim zdanem na korzyść.
Require Export Bool.
Require Export Nat.
W części dowodów przydadzą nam się fakty dotyczące arytmetyki liczb
naturalnych, które możemy znaleźć w module
Arith.
Zdefiniuj
list (bez podglądania).
Arguments nil {A}.
Arguments cons {A} _ _.
Notation "[ ]" := nil (format "[ ]").
Notation "x :: y" := (cons x y) (at level 60, right associativity).
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
Proste funkcje
isEmpty
Zdefiniuj funkcję
isEmpty, która sprawdza, czy lista jest pusta.
length
Zdefiniuj funkcję
length, która oblicza długość listy.
Przykład:
length [1; 2; 3] =
3
Lemma length_nil :
forall A : Type, length (@nil A) = 0.
Lemma length_cons :
forall (A : Type) (h : A) (t : list A),
exists n : nat, length (h :: t) = S n.
Lemma length_0 :
forall (A : Type) (l : list A),
length l = 0 -> l = [].
snoc
Zdefiniuj funkcję
snoc, która dokleja element
x na koniec listy
l.
Przykład:
snoc 42 [1; 2; 3] =
[1; 2; 3; 42]
Lemma snoc_isEmpty :
forall (A : Type) (x : A) (l : list A),
isEmpty l = true -> snoc x l = [x].
Lemma isEmpty_snoc :
forall (A : Type) (x : A) (l : list A),
isEmpty (snoc x l) = false.
Lemma length_snoc :
forall (A : Type) (x : A) (l : list A),
length (snoc x l) = S (length l).
Lemma snoc_inv :
forall (A : Type) (l1 l2 : list A) (x y : A),
snoc x l1 = snoc y l2 -> x = y /\ l1 = l2.
app
Zdefiniuj funkcję
app, która skleja dwie listy.
Przykład:
app [1; 2; 3] [4; 5; 6] =
[1; 2; 3; 4; 5; 6]
Notation "l1 ++ l2" := (app l1 l2).
Lemma app_nil_l :
forall (A : Type) (l : list A),
[] ++ l = l.
Lemma app_nil_r :
forall (A : Type) (l : list A),
l ++ [] = l.
Lemma app_assoc :
forall (A : Type) (l1 l2 l3 : list A),
l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.
Lemma isEmpty_app :
forall (A : Type) (l1 l2 : list A),
isEmpty (l1 ++ l2) = andb (isEmpty l1) (isEmpty l2).
Lemma length_app :
forall (A : Type) (l1 l2 : list A),
length (l1 ++ l2) = length l1 + length l2.
Lemma snoc_app :
forall (A : Type) (x : A) (l1 l2 : list A),
snoc x (l1 ++ l2) = l1 ++ snoc x l2.
Lemma app_snoc_l :
forall (A : Type) (x : A) (l1 l2 : list A),
snoc x l1 ++ l2 = l1 ++ x :: l2.
Lemma app_snoc_r :
forall (A : Type) (x : A) (l1 l2 : list A),
l1 ++ snoc x l2 = snoc x (l1 ++ l2).
Lemma snoc_app_singl :
forall (A : Type) (x : A) (l : list A),
snoc x l = l ++ [x].
Lemma app_cons_l :
forall (A : Type) (x : A) (l1 l2 : list A),
(x :: l1) ++ l2 = x :: (l1 ++ l2).
Lemma app_cons_r :
forall (A : Type) (x : A) (l1 l2 : list A),
l1 ++ x :: l2 = (l1 ++ [x]) ++ l2.
Lemma no_infinite_cons :
forall (A : Type) (x : A) (l : list A),
l = x :: l -> False.
Lemma no_infinite_app :
forall (A : Type) (l l' : list A),
l' <> [] -> l = l' ++ l -> False.
Lemma app_inv_l :
forall (A : Type) (l l1 l2 : list A),
l ++ l1 = l ++ l2 -> l1 = l2.
Lemma app_inv_r :
forall (A : Type) (l l1 l2 : list A),
l1 ++ l = l2 ++ l -> l1 = l2.
Lemma app_eq_nil :
forall (A : Type) (l1 l2 : list A),
l1 ++ l2 = [] -> l1 = [] /\ l2 = [].
rev
Zdefiniuj funkcję
rev, która odwraca listę.
Przykład:
rev [1; 2; 3] =
[3; 2; 1]
Lemma isEmpty_rev :
forall (A : Type) (l : list A),
isEmpty (rev l) = isEmpty l.
Lemma length_rev :
forall (A : Type) (l : list A),
length (rev l) = length l.
Lemma snoc_rev :
forall (A : Type) (x : A) (l : list A),
snoc x (rev l) = rev (x :: l).
Lemma rev_snoc :
forall (A : Type) (x : A) (l : list A),
rev (snoc x l) = x :: rev l.
Lemma rev_app :
forall (A : Type) (l1 l2 : list A),
rev (l1 ++ l2) = rev l2 ++ rev l1.
Lemma rev_inv :
forall (A : Type) (l : list A),
rev (rev l) = l.
map
Zdefiniuj funkcję
map, która aplikuje funkcję
f do każdego
elementu listy.
Przykład:
map isEmpty [[]; [1]; [2; 3]; []] =
[true; false; false; true]
Lemma map_id :
forall (A : Type) (l : list A),
map id l = l.
Lemma map_map :
forall (A B C : Type) (f : A -> B) (g : B -> C) (l : list A),
map g (map f l) = map (fun x : A => g (f x)) l.
Lemma isEmpty_map :
forall (A B : Type) (f : A -> B) (l : list A),
isEmpty (map f l) = isEmpty l.
Lemma length_map :
forall (A B : Type) (f : A -> B) (l : list A),
length (map f l) = length l.
Lemma map_snoc :
forall (A B : Type) (f : A -> B) (x : A) (l : list A),
map f (snoc x l) = snoc (f x) (map f l).
Lemma map_app :
forall (A B : Type) (f : A -> B) (l1 l2 : list A),
map f (l1 ++ l2) = map f l1 ++ map f l2.
Lemma map_rev :
forall (A B : Type) (f : A -> B) (l : list A),
map f (rev l) = rev (map f l).
Lemma map_ext :
forall (A B : Type) (f g : A -> B) (l : list A),
(forall x : A, f x = g x) -> map f l = map g l.
join
Zdefiniuj funkcję
join, która spłaszcza listę list.
Przykład:
join [[1; 2; 3]; [4; 5; 6]; [7]] =
[1; 2; 3; 4; 5; 6; 7]
Lemma join_snoc :
forall (A : Type) (x : list A) (l : list (list A)),
join (snoc x l) = join l ++ x.
Lemma join_app :
forall (A : Type) (l1 l2 : list (list A)),
join (l1 ++ l2) = join l1 ++ join l2.
Lemma rev_join :
forall (A : Type) (l : list (list A)),
rev (join l) = join (rev (map rev l)).
Lemma map_join :
forall (A B : Type) (f : A -> B) (l : list (list A)),
map f (join l) = join (map (map f) l).
bind
Zdefiniuj funkcję
bind, która spełnia specyfikację
bind_spec.
Użyj rekursji, ale nie używaj funkcji
join ani
map.
Lemma bind_spec :
forall (A B : Type) (f : A -> list B) (l : list A),
bind f l = join (map f l).
Lemma bind_snoc :
forall (A B : Type) (f : A -> list B) (x : A) (l : list A),
bind f (snoc x l) = bind f l ++ f x.
replicate
Zdefiniuj funkcję
replicate, która powiela dany element
n razy,
tworząc listę.
Przykład:
replicate 5 0 =
[0; 0; 0; 0; 0]
Definition isZero (n : nat) : bool :=
match n with
| 0 => true
| _ => false
end.
Lemma isEmpty_replicate :
forall (A : Type) (n : nat) (x : A),
isEmpty (replicate n x) = if isZero n then true else false.
Lemma length_replicate :
forall (A : Type) (n : nat) (x : A),
length (replicate n x) = n.
Lemma snoc_replicate :
forall (A : Type) (x : A) (n : nat),
snoc x (replicate n x) = replicate (S n) x.
Lemma replicate_plus :
forall (A : Type) (n m : nat) (x : A),
replicate (n + m) x = replicate n x ++ replicate m x.
Lemma replicate_plus_comm :
forall (A : Type) (n m : nat) (x : A),
replicate (n + m) x = replicate (m + n) x.
Lemma rev_replicate :
forall (A : Type) (n : nat) (x : A),
rev (replicate n x) = replicate n x.
Lemma map_replicate :
forall (A B : Type) (f : A -> B) (n : nat) (x : A),
map f (replicate n x) = replicate n (f x).
iterate i iter
Zdefiniuj funkcję
iterate.
iterate f n x to lista postaci
[x, f x, f (f x), ..., f (... (f x) ...)] o długości
n.
Przykład:
iterate S 5 0 =
[0; 1; 2; 3; 4]
Zdefiniuj też funkcję
iter, która przyda się do podania
charakteryzacji funkcji
iterate. Zgadnij, czym ma ona być.
Lemma isEmpty_iterate :
forall (A : Type) (f : A -> A) (n : nat) (x : A),
isEmpty (iterate f n x) =
match n with
| 0 => true
| _ => false
end.
Lemma length_iterate :
forall (A : Type) (f : A -> A) (n : nat) (x : A),
length (iterate f n x) = n.
Lemma snoc_iterate :
forall (A : Type) (f : A -> A) (n : nat) (x : A),
snoc (iter f n x) (iterate f n x) =
iterate f (S n) x.
Lemma iterate_plus :
forall (A : Type) (f : A -> A) (n m : nat) (x : A),
iterate f (n + m) x =
iterate f n x ++ iterate f m (iter f n x).
Lemma snoc_iterate_iter :
forall (A : Type) (f : A -> A) (n : nat) (x : A),
iterate f n x ++ [iter f n x] = iterate f (S n) x.
Lemma map_iterate :
forall (A : Type) (f : A -> A) (n : nat) (x : A),
map f (iterate f n x) = iterate f n (f x).
Lemma map_iter_iterate :
forall (A : Type) (f : A -> A) (n m : nat) (x : A),
map (iter f m) (iterate f n x) =
iterate f n (iter f m x).
Lemma iterate_replicate :
forall (A : Type) (n : nat) (x : A),
iterate id n x = replicate n x.
head, tail i uncons
head
Zdefiniuj funkcję
head, która zwraca głowę (pierwszy element)
listy lub
None, gdy lista jest pusta.
Przykład:
head [1; 2; 3] =
Some 1
Lemma head_nil :
forall (A : Type), head [] = (@None A).
Lemma head_cons :
forall (A : Type) (h : A) (t : list A),
head (h :: t) = Some h.
Lemma head_isEmpty_true :
forall (A : Type) (l : list A),
isEmpty l = true -> head l = None.
Lemma isEmpty_head_not_None :
forall (A : Type) (l : list A),
head l <> None -> isEmpty l = false.
Lemma head_snoc :
forall (A : Type) (x : A) (l : list A),
head (snoc x l) =
if isEmpty l then Some x else head l.
Lemma head_app :
forall (A : Type) (l1 l2 : list A),
head (l1 ++ l2) =
match l1 with
| [] => head l2
| h :: _ => Some h
end.
Lemma head_map :
forall (A B : Type) (f : A -> B) (l : list A),
head (map f l) =
match l with
| [] => None
| h :: _ => Some (f h)
end.
Lemma head_replicate_S :
forall (A : Type) (n : nat) (x : A),
head (replicate (S n) x) = Some x.
Lemma head_replicate :
forall (A : Type) (n : nat) (x : A),
head (replicate n x) =
match n with
| 0 => None
| _ => Some x
end.
Lemma head_iterate :
forall (A : Type) (f : A -> A) (n : nat) (x : A),
head (iterate f n x) =
match n with
| 0 => None
| S n' => Some x
end.
tail
Zdefiniuj funkcję
tail, która zwraca ogon listy (czyli wszystkie
jej elementy poza głową) lub
None, gdy lista jest pusta.
Przykład:
tail [1; 2; 3] =
Some [2; 3]
Lemma tail_nil :
forall A : Type, tail (@nil A) = None.
Lemma tail_cons :
forall (A : Type) (h : A) (t : list A),
tail (h :: t) = Some t.
Lemma tail_isEmpty_true :
forall (A : Type) (l : list A),
isEmpty l = true -> tail l = None.
Lemma isEmpty_tail_not_None :
forall (A : Type) (l : list A),
tail l <> None -> isEmpty l = false.
Lemma tail_snoc :
forall (A : Type) (x : A) (l : list A),
tail (snoc x l) =
match tail l with
| None => Some []
| Some t => Some (snoc x t)
end.
Lemma tail_app :
forall (A : Type) (l1 l2 : list A),
tail (l1 ++ l2) =
match l1 with
| [] => tail l2
| h :: t => Some (t ++ l2)
end.
Lemma tail_map :
forall (A B : Type) (f : A -> B) (l : list A),
tail (map f l) =
match l with
| [] => None
| _ :: t => Some (map f t)
end.
Lemma tail_replicate :
forall (A : Type) (n : nat) (x : A),
tail (replicate n x) =
match n with
| 0 => None
| S n' => Some (replicate n' x)
end.
Lemma tail_iterate :
forall (A : Type) (f : A -> A) (n : nat) (x : A),
tail (iterate f n x) =
match n with
| 0 => None
| S n' => Some (iterate f n' (f x))
end.
uncons
Zdefiniuj funkcję
uncons, która zwraca parę złożoną z głowy i ogona
listy lub
None, gdy lista jest pusta. Nie używaj funkcji
head
ani
tail. Udowodnij poniższą specyfikację.
Przykład:
uncons [1; 2; 3] =
Some (1, [2; 3])
Lemma uncons_spec :
forall (A : Type) (l : list A),
uncons l =
match head l, tail l with
| Some h, Some t => Some (h, t)
| _, _ => None
end.
last, init i unsnoc
last
Zdefiniuj funkcję
last, która zwraca ostatni element listy lub
None, gdy lista jest pusta.
Przykład:
last [1; 2; 3] =
Some 3
Lemma last_nil :
forall (A : Type), last [] = (@None A).
Lemma last_isEmpty_true :
forall (A : Type) (l : list A),
isEmpty l = true -> last l = None.
Lemma isEmpty_last_not_None :
forall (A : Type) (l : list A),
last l <> None -> isEmpty l = false.
Lemma last_snoc :
forall (A : Type) (x : A) (l : list A),
last (snoc x l) = Some x.
Lemma last_spec :
forall (A : Type) (l : list A) (x : A),
last (l ++ [x]) = Some x.
Lemma last_app :
forall (A : Type) (l1 l2 : list A),
last (l1 ++ l2) =
match l2 with
| [] => last l1
| _ => last l2
end.
Lemma last_replicate_S :
forall (A : Type) (n : nat) (x : A),
last (replicate (S n) x) = Some x.
Lemma last_replicate :
forall (A : Type) (n : nat) (x : A),
last (replicate n x) =
match n with
| 0 => None
| _ => Some x
end.
Lemma last_iterate :
forall (A : Type) (f : A -> A) (n : nat) (x : A),
last (iterate f n x) =
match n with
| 0 => None
| S n' => Some (iter f n' x)
end.
init
Zdefiniuj funkcję
init, która zwraca wszystkie elementy listy poza
ostatnim lub
None, gdy lista jest pusta.
Przykład:
init [1; 2; 3] =
Some [1; 2]
Lemma init_None :
forall (A : Type) (l : list A),
init l = None -> l = [].
Lemma init_snoc :
forall (A : Type) (x : A) (l : list A),
init (snoc x l) = Some l.
Lemma init_app :
forall (A : Type) (l1 l2 : list A),
init (l1 ++ l2) =
match init l2 with
| None => init l1
| Some i => Some (l1 ++ i)
end.
Lemma init_spec :
forall (A : Type) (l : list A) (x : A),
init (l ++ [x]) = Some l.
Lemma init_map :
forall (A B : Type) (f : A -> B) (l : list A),
init (map f l) =
match l with
| [] => None
| h :: t =>
match init t with
| None => Some []
| Some i => Some (map f (h :: i))
end
end.
Lemma init_replicate :
forall (A : Type) (n : nat) (x : A),
init (replicate n x) =
match n with
| 0 => None
| S n' => Some (replicate n' x)
end.
Lemma init_iterate :
forall (A : Type) (f : A -> A) (n : nat) (x : A),
init (iterate f n x) =
match n with
| 0 => None
| S n' => Some (iterate f n' x)
end.
Lemma init_last :
forall (A : Type) (l l' : list A) (x : A),
init l = Some l' -> last l = Some x -> l = l' ++ [x].
unsnoc
Zdefiniuj funkcję
unsnoc, która rozbija listę na parę złożoną z
ostatniego elementu oraz całej reszty lub zwraca
None gdy lista
jest pusta. Nie używaj funkcji
last ani
init. Udowodnij poniższą
specyfikację.
Przykład:
unsnoc [1; 2; 3] =
Some (3, [1; 2])
Lemma unsnoc_None :
forall (A : Type) (l : list A),
unsnoc l = None -> l = [].
Lemma unsnoc_spec :
forall (A : Type) (l : list A),
unsnoc l =
match last l, init l with
| Some x, Some l' => Some (x, l')
| _, _ => None
end.
Dualności head i last, tail i init oraz ciekawostki
Lemma last_rev :
forall (A : Type) (l : list A),
last (rev l) = head l.
Lemma head_rev :
forall (A : Type) (l : list A),
head (rev l) = last l.
Lemma tail_rev :
forall (A : Type) (l : list A),
tail (rev l) =
match init l with
| None => None
| Some t => Some (rev t)
end.
Lemma init_rev :
forall (A : Type) (l : list A),
init (rev l) =
match tail l with
| None => None
| Some t => Some (rev t)
end.
Lemma init_decomposition :
forall (A : Type) (l : list A),
l = [] \/
exists (h : A) (t : list A),
init l = Some t /\ last l = Some h /\ l = t ++ [h].
Lemma bilateral_decomposition :
forall (A : Type) (l : list A),
l = [] \/
(exists x : A, l = [x]) \/
exists (x y : A) (l' : list A), l = x :: l' ++ [y].
nth
Zdefiniuj funkcję
nth, która zwraca n-ty element listy lub
None,
gdy nie ma n-tego elementu.
Przykład:
nth 1 [1; 2; 3] =
Some 2
nth 42 [1; 2; 3] =
None
Lemma nth_nil :
forall (A : Type) (n : nat),
nth n (@nil A) = None.
Lemma nth_isEmpty_true :
forall (A : Type) (l : list A) (n : nat),
isEmpty l = true -> nth n l = None.
Lemma isEmpty_nth_not_None :
forall (A : Type) (l : list A) (n : nat),
nth n l <> None -> isEmpty l = false.
Lemma nth_length_lt :
forall (A : Type) (l : list A) (n : nat),
n < length l -> exists x : A, nth n l = Some x.
Lemma nth_length_ge :
forall (A : Type) (l : list A) (n : nat),
length l <= n -> nth n l = None.
Lemma nth_snoc_length_lt :
forall (A : Type) (x : A) (l : list A) (n : nat),
n < length l -> nth n (snoc x l) = nth n l.
Lemma nth_snoc_length_eq :
forall (A : Type) (x : A) (l : list A),
nth (length l) (snoc x l) = Some x.
Lemma nth_snoc :
forall (A : Type) (x : A) (l : list A) (n : nat),
nth n (snoc x l) =
if n <? length l then nth n l
else if n =? length l then Some x
else None.
Lemma nth_app :
forall (A : Type) (l1 l2 : list A) (n : nat),
nth n (l1 ++ l2) =
match nth n l1 with
| None => nth (n - length l1) l2
| Some x => Some x
end.
Lemma nth_app_l :
forall (A : Type) (l1 l2 : list A) (n : nat),
n < length l1 -> nth n (l1 ++ l2) = nth n l1.
Lemma nth_app_r :
forall (A : Type) (n : nat) (l1 l2 : list A),
length l1 <= n -> nth n (l1 ++ l2) = nth (n - length l1) l2.
Lemma nth_rev :
forall (A : Type) (l : list A) (n : nat),
n < length l -> nth n (rev l) = nth (length l - S n) l.
Lemma nth_None :
forall (A : Type) (l : list A) (n : nat),
nth n l = None -> length l <= n.
Lemma nth_Some :
forall (A : Type) (l : list A) (n : nat) (x : A),
nth n l = Some x -> n < length l.
Lemma nth_spec' :
forall (A : Type) (l : list A) (n : nat),
match nth n l with
| None => length l <= n
| Some x => exists l1 l2 : list A,
l = l1 ++ x :: l2 /\ length l1 = n
end.
Lemma nth_map_Some :
forall (A B : Type) (f : A -> B) (l : list A) (n : nat) (x : A),
nth n l = Some x -> nth n (map f l) = Some (f x).
Lemma nth_map :
forall (A B : Type) (f : A -> B) (l : list A) (n : nat),
nth n (map f l) =
match nth n l with
| None => None
| Some x => Some (f x)
end.
Lemma nth_replicate :
forall (A : Type) (n i : nat) (x : A),
i < n -> nth i (replicate n x) = Some x.
Lemma nth_iterate :
forall (A : Type) (f : A -> A) (n m : nat) (x : A),
nth m (iterate f n x) =
if leb n m then None else Some (iter f m x).
Lemma head_nth :
forall (A : Type) (l : list A),
nth 0 l = head l.
Lemma last_nth :
forall (A : Type) (l : list A),
last l = nth (length l - 1) l.
take
Zdefiniuj funkcję
take, która bierze z listy
n początkowych
elementów.
Przykład:
take 2 [1; 2; 3] =
[1; 2]
Lemma take_0 :
forall (A : Type) (l : list A),
take 0 l = [].
Lemma take_nil :
forall (A : Type) (n : nat),
take n [] = @nil A.
Lemma take_S_cons :
forall (A : Type) (n : nat) (h : A) (t : list A),
take (S n) (h :: t) = h :: take n t.
Lemma isEmpty_take :
forall (A : Type) (l : list A) (n : nat),
isEmpty (take n l) = orb (beq_nat 0 n) (isEmpty l).
Lemma take_length :
forall (A : Type) (l : list A),
take (length l) l = l.
Lemma take_length' :
forall (A : Type) (l : list A) (n : nat),
length l <= n -> take n l = l.
Lemma length_take :
forall (A : Type) (l : list A) (n : nat),
length (take n l) = min (length l) n.
Lemma take_snoc_lt :
forall (A : Type) (x : A) (l : list A) (n : nat),
n < length l -> take n (snoc x l) = take n l.
Lemma take_snoc_le :
forall (A : Type) (x : A) (l : list A) (n : nat),
n <= length l -> take n (snoc x l) = take n l.
Lemma take_app :
forall (A : Type) (l1 l2 : list A) (n : nat),
take n (l1 ++ l2) = take n l1 ++ take (n - length l1) l2.
Lemma take_app_l :
forall (A : Type) (l1 l2 : list A) (n : nat),
n <= length l1 -> take n (l1 ++ l2) = take n l1.
Lemma take_app_r :
forall (A : Type) (n : nat) (l1 l2 : list A),
length l1 < n ->
take n (l1 ++ l2) = l1 ++ take (n - length l1) l2.
Lemma take_map :
forall (A B : Type) (f : A -> B) (l : list A) (n : nat),
take n (map f l) = map f (take n l).
Lemma take_replicate :
forall (A : Type) (n m : nat) (x : A),
take m (replicate n x) = replicate (min n m) x.
Lemma take_iterate :
forall (A : Type) (f : A -> A) (n m : nat) (x : A),
take m (iterate f n x) = iterate f (min n m) x.
Lemma head_take :
forall (A : Type) (l : list A) (n : nat),
head (take n l) =
if beq_nat 0 n then None else head l.
Lemma last_take :
forall (A : Type) (l : list A) (n : nat),
last (take (S n) l) = nth (min (length l - 1) n) l.
Lemma tail_take :
forall (A : Type) (l : list A) (n : nat),
tail (take n l) =
match n, l with
| 0, _ => None
| _, [] => None
| S n', h :: t => Some (take n' t)
end.
Lemma init_take :
forall (A : Type) (l : list A) (n : nat),
init (take n l) =
match n, l with
| 0, _ => None
| _, [] => None
| S n', h :: t => Some (take (min n' (length l - 1)) l)
end.
Lemma nth_take :
forall (A : Type) (l : list A) (n m : nat),
nth m (take n l) =
if leb (S m) n then nth m l else None.
Lemma take_take :
forall (A : Type) (l : list A) (n m : nat),
take m (take n l) = take (min n m) l.
Lemma take_interesting :
forall (A : Type) (l1 l2 : list A),
(forall n : nat, take n l1 = take n l2) -> l1 = l2.
drop
Zdefiniuj funkcję
drop, która wyrzuca z listy
n początkowych
elementów i zwraca to, co zostało.
Przykład:
drop 2 [1; 2; 3] =
[3]
Lemma drop_0 :
forall (A : Type) (l : list A),
drop 0 l = l.
Lemma drop_nil :
forall (A : Type) (n : nat),
drop n [] = @nil A.
Lemma drop_S_cons :
forall (A : Type) (n : nat) (h : A) (t : list A),
drop (S n) (h :: t) = drop n t.
Lemma isEmpty_drop :
forall (A : Type) (l : list A) (n : nat),
isEmpty (drop n l) = leb (length l) n.
Lemma drop_length :
forall (A : Type) (l : list A),
drop (length l) l = [].
Lemma drop_length' :
forall (A : Type) (l : list A) (n : nat),
length l <= n -> drop n l = [].
Lemma length_drop :
forall (A : Type) (l : list A) (n : nat),
length (drop n l) = length l - n.
Lemma drop_snoc_le :
forall (A : Type) (x : A) (l : list A) (n : nat),
n <= length l -> drop n (snoc x l) = snoc x (drop n l).
Lemma drop_app :
forall (A : Type) (l1 l2 : list A) (n : nat),
drop n (l1 ++ l2) = drop n l1 ++ drop (n - length l1) l2.
Lemma drop_app_l :
forall (A : Type) (l1 l2 : list A) (n : nat),
n <= length l1 -> drop n (l1 ++ l2) = drop n l1 ++ l2.
Lemma drop_app_r :
forall (A : Type) (l1 l2 : list A) (n : nat),
length l1 < n -> drop n (l1 ++ l2) = drop (n - length l1) l2.
Lemma drop_map :
forall (A B : Type) (f : A -> B) (l : list A) (n : nat),
drop n (map f l) = map f (drop n l).
Lemma drop_replicate :
forall (A : Type) (n m : nat) (x : A),
drop m (replicate n x) = replicate (n - m) x.
Lemma drop_iterate :
forall (A : Type) (f : A -> A) (n m : nat) (x : A),
drop m (iterate f n x) =
iterate f (n - m) (iter f (min n m) x).
Lemma head_drop :
forall (A : Type) (l : list A) (n : nat),
head (drop n l) = nth n l.
Lemma last_drop :
forall (A : Type) (l : list A) (n : nat),
last (drop n l) = if leb (S n) (length l) then last l else None.
Lemma tail_drop :
forall (A : Type) (l : list A) (n : nat),
tail (drop n l) =
if leb (S n) (length l) then Some (drop (S n) l) else None.
Lemma init_drop :
forall (A : Type) (l : list A) (n : nat),
init (drop n l) =
if n <? length l
then
match init l with
| None => None
| Some l' => Some (drop n l')
end
else None.
Lemma nth_drop :
forall (A : Type) (l : list A) (n m : nat),
nth m (drop n l) = nth (n + m) l.
Lemma nth_spec_Some :
forall (A : Type) (l : list A) (n : nat) (x : A),
nth n l = Some x -> l = take n l ++ x :: drop (S n) l.
Lemma nth_spec :
forall (A : Type) (l : list A) (n : nat),
match nth n l with
| None => length l <= n
| Some x => l = take n l ++ x :: drop (S n) l
end.
Lemma drop_drop :
forall (A : Type) (l : list A) (n m : nat),
drop m (drop n l) = drop (n + m) l.
Lemma drop_not_so_interesting :
forall (A : Type) (l1 l2 : list A),
(forall n : nat, drop n l1 = drop n l2) -> l1 = l2.
Lemma take_rev :
forall (A : Type) (l : list A) (n : nat),
take n (rev l) = rev (drop (length l - n) l).
Lemma rev_take :
forall (A : Type) (l : list A) (n : nat),
rev (take n l) = drop (length l - n) (rev l).
Lemma drop_rev :
forall (A : Type) (n : nat) (l : list A),
drop n (rev l) = rev (take (length l - n) l).
Lemma take_drop :
forall (A : Type) (l : list A) (n m : nat),
take m (drop n l) = drop n (take (n + m) l).
Lemma drop_take :
forall (A : Type) (l : list A) (n m : nat),
drop m (take n l) = take (n - m) (drop m l).
Lemma app_take_drop :
forall (A : Type) (l : list A) (n : nat),
take n l ++ drop n l = l.
cycle
Zdefiniuj funkcję
cycle : forall A : Type, nat -> list A -> list A,
która obraca listę cyklicznie. Udowodnij jej właściwości.
Compute cycle 3 [1; 2; 3; 4; 5].
Compute cycle 6 [1; 2; 3; 4; 5].
Lemma cycle_0 :
forall (A : Type) (l : list A),
cycle 0 l = l.
Lemma cycle_nil :
forall (A : Type) (n : nat),
@cycle A n [] = [].
Lemma isEmpty_cycle :
forall (A : Type) (n : nat) (l : list A),
isEmpty (cycle n l) = isEmpty l.
Lemma length_cycle :
forall (A : Type) (n : nat) (l : list A),
length (cycle n l) = length l.
Lemma cycle_length_app :
forall (A : Type) (l1 l2 : list A) (n : nat),
cycle (length l1 + n) (l1 ++ l2) = cycle n (l2 ++ l1).
Lemma cycle_length :
forall (A : Type) (x : A) (l : list A),
cycle (length l) l = l.
Lemma cycle_plus_length :
forall (A : Type) (n : nat) (l : list A),
cycle (length l + n) l = cycle n l.
Łamigłówka: jaki jest związek cycle ze snoc, i rev?
Compute cycle 2 [1; 2; 3; 4; 5; 6].
Compute rev (cycle 4 (rev [1; 2; 3; 4; 5; 6])).
Lemma cycle_map :
forall (A B : Type) (f : A -> B) (n : nat) (l : list A),
cycle n (map f l) = map f (cycle n l).
A z join i bind?
Lemma cycle_replicate :
forall (A : Type) (n m : nat) (x : A),
cycle m (replicate n x) = replicate n x.
Lemma cycle_cycle :
forall (A : Type) (n m : nat) (l : list A),
cycle n (cycle m l) = cycle (m + n) l.
splitAt
Zdefiniuj funkcję
splitAt, która spełnia poniższą specyfikację.
Nie używaj take ani drop - użyj rekursji.
Przykład:
splitAt 2 [1; 2; 3; 4; 5] =
Some ([1; 2], 3, [4; 5])
Lemma splitAt_spec :
forall (A : Type) (l : list A) (n : nat),
match splitAt n l with
| None => length l <= n
| Some (l1, x, l2) => l = l1 ++ x :: l2
end.
Lemma splitAt_spec' :
forall (A : Type) (l l1 l2 : list A) (x : A) (n : nat),
splitAt n l = Some (l1, x, l2) ->
l1 = take n l /\ l2 = drop (S n) l.
Lemma splitAt_megaspec :
forall (A : Type) (l : list A) (n : nat),
match splitAt n l with
| None => length l <= n
| Some (l1, x, l2) =>
nth n l = Some x /\
l1 = take n l /\
l2 = drop (S n) l /\
l = l1 ++ x :: l2
end.
Lemma splitAt_isEmpty_true :
forall (A : Type) (l : list A),
isEmpty l = true -> forall n : nat, splitAt n l = None.
Lemma isEmpty_splitAt_false :
forall (A : Type) (l : list A) (n : nat),
splitAt n l <> None -> isEmpty l = false.
Lemma splitAt_length_inv :
forall (A : Type) (l : list A) (n : nat),
splitAt n l <> None <-> n < length l.
Lemma splitAt_Some_length :
forall (A : Type) (l l1 l2 : list A) (x : A) (n : nat),
splitAt n l = Some (l1, x, l2) -> n < length l.
Lemma splitAt_length_lt :
forall (A : Type) (l : list A) (n : nat),
n < length l -> exists x : A,
splitAt n l = Some (take n l, x, drop (S n) l).
Lemma splitAt_length_ge :
forall (A : Type) (l : list A) (n : nat),
length l <= n -> splitAt n l = None.
Lemma splitAt_snoc :
forall (A : Type) (l : list A) (n : nat) (x : A),
splitAt n (snoc x l) =
if n <? length l
then
match splitAt n l with
| None => None
| Some (b, y, e) => Some (b, y, snoc x e)
end
else
if beq_nat n (length l)
then Some (l, x, [])
else None.
Lemma splitAt_app :
forall (A : Type) (l1 l2 : list A) (n : nat),
splitAt n (l1 ++ l2) =
match splitAt n l1 with
| Some (l11, x, l12) => Some (l11, x, l12 ++ l2)
| None =>
match splitAt (n - length l1) l2 with
| Some (l21, x, l22) => Some (l1 ++ l21, x, l22)
| None => None
end
end.
Lemma splitAt_app_lt :
forall (A : Type) (l1 l2 : list A) (n : nat),
n < length l1 ->
splitAt n (l1 ++ l2) =
match splitAt n l1 with
| None => None
| Some (x, l11, l12) => Some (x, l11, l12 ++ l2)
end.
Lemma splitAt_app_ge :
forall (A : Type) (l1 l2 : list A) (n : nat),
length l1 <= n ->
splitAt n (l1 ++ l2) =
match splitAt (n - length l1) l2 with
| None => None
| Some (l21, x, l22) => Some (l1 ++ l21, x, l22)
end.
Lemma splitAt_rev_aux :
forall (A : Type) (l : list A) (n : nat),
n < length l ->
splitAt n l =
match splitAt (length l - S n) (rev l) with
| None => None
| Some (l1, x, l2) => Some (rev l2, x, rev l1)
end.
Lemma splitAt_rev :
forall (A : Type) (l : list A) (n : nat),
n < length l ->
splitAt n (rev l) =
match splitAt (length l - S n) l with
| None => None
| Some (l1, x, l2) => Some (rev l2, x, rev l1)
end.
Lemma splitAt_map :
forall (A B : Type) (f : A -> B) (l : list A) (n : nat),
splitAt n (map f l) =
match splitAt n l with
| None => None
| Some (l1, x, l2) => Some (map f l1, f x, map f l2)
end.
Lemma splitAt_replicate :
forall (A : Type) (n m : nat) (x : A),
splitAt m (replicate n x) =
if m <? n
then Some (replicate m x, x, replicate (n - S m) x)
else None.
Lemma splitAt_iterate :
forall (A : Type) (f : A -> A) (n m : nat) (x : A),
splitAt m (iterate f n x) =
if m <? n
then Some (iterate f m x, iter f m x, iterate f (n - S m) (iter f (S m) x))
else None.
Lemma splitAt_head_l :
forall (A : Type) (l l1 l2 : list A) (x : A) (n : nat),
splitAt n l = Some (l1, x, l2) ->
head l1 =
match n with
| 0 => None
| _ => head l
end.
Lemma splitAt_head_r :
forall (A : Type) (l l1 l2 : list A) (x : A) (n : nat),
splitAt n l = Some (l1, x, l2) ->
head l2 = nth (S n) l.
Lemma splitAt_last_l :
forall (A : Type) (l l1 l2 : list A) (x : A) (n : nat),
splitAt n l = Some (l1, x, l2) ->
last l1 =
match n with
| 0 => None
| S n' => nth n' l
end.
Lemma splitAt_last_r :
forall (A : Type) (l l1 l2 : list A) (x : A) (n : nat),
splitAt n l = Some (l1, x, l2) ->
last l2 =
if length l <=? S n
then None
else last l2.
Lemma take_splitAt :
forall (A : Type) (l l1 l2 : list A) (n m : nat) (x : A),
splitAt n l = Some (l1, x, l2) ->
take m l1 = take (min n m) l.
Lemma take_splitAt' :
forall (A : Type) (l l1 l2 : list A) (n m : nat) (x : A),
splitAt n l = Some (l1, x, l2) ->
take m l2 = take m (drop (S n) l).
Lemma drop_splitAt_l :
forall (A : Type) (l l1 l2 : list A) (n m : nat) (x : A),
splitAt n l = Some (l1, x, l2) ->
drop m l1 = take (n - m) (drop m l).
Lemma drop_splitAt_r :
forall (A : Type) (l l1 l2 : list A) (n m : nat) (x : A),
splitAt n l = Some (l1, x, l2) ->
drop m l2 = drop (S n + m) l.
insert
Zdefiniuj funkcję
insert, która wstawia do listy
l na
n-tą pozycję
element
x.
Przykład:
insert [1; 2; 3; 4; 5] 2 42 =
[1; 2; 42; 3; 4; 5]
Lemma insert_0 :
forall (A : Type) (l : list A) (x : A),
insert l 0 x = x :: l.
Lemma isEmpty_insert :
forall (A : Type) (l : list A) (n : nat) (x : A),
isEmpty (insert l n x) = false.
Lemma length_insert :
forall (A : Type) (l : list A) (n : nat) (x : A),
length (insert l n x) = S (length l).
Lemma insert_length :
forall (A : Type) (l : list A) (x : A),
insert l (length l) x = snoc x l.
Lemma insert_snoc :
forall (A : Type) (l : list A) (n : nat) (x y : A),
insert (snoc x l) n y =
if n <=? length l then snoc x (insert l n y) else snoc y (snoc x l).
Lemma insert_app :
forall (A : Type) (l1 l2 : list A) (n : nat) (x : A),
insert (l1 ++ l2) n x =
if leb n (length l1)
then insert l1 n x ++ l2
else l1 ++ insert l2 (n - length l1) x.
Lemma insert_rev :
forall (A : Type) (l : list A) (n : nat) (x : A),
insert (rev l) n x = rev (insert l (length l - n) x).
Lemma rev_insert :
forall (A : Type) (l : list A) (n : nat) (x : A),
rev (insert l n x) = insert (rev l) (length l - n) x.
Lemma map_insert :
forall (A B : Type) (f : A -> B) (l : list A) (n : nat) (x : A),
map f (insert l n x) = insert (map f l) n (f x).
Lemma insert_join :
forall (A : Type) (ll : list (list A)) (n : nat) (x : A) (l : list A),
join (insert ll n [x]) = l ->
exists m : nat, l = insert (join ll) m x.
Lemma insert_replicate :
forall (A : Type) (n m : nat) (x : A),
insert (replicate n x) m x = replicate (S n) x.
Lemma head_insert :
forall (A : Type) (l : list A) (n : nat) (x : A),
head (insert l n x) =
match l, n with
| [], _ => Some x
| _, 0 => Some x
| _, _ => head l
end.
Lemma tail_insert :
forall (A : Type) (l : list A) (n : nat) (x : A),
tail (insert l n x) =
match l, n with
| [], _ => Some []
| _, 0 => Some l
| h :: t, S n' => Some (insert t n' x)
end.
Lemma last_insert :
forall (A : Type) (l : list A) (n : nat) (x : A),
last (insert l n x) =
if isEmpty l
then Some x
else if leb (S n) (length l) then last l else Some x.
Lemma nth_insert :
forall (A : Type) (l : list A) (n : nat) (x : A),
n <= length l -> nth n (insert l n x) = Some x.
Lemma nth_insert' :
forall (A : Type) (l : list A) (n : nat) (x : A),
nth n (insert l n x) =
if leb n (length l) then Some x else None.
Lemma insert_spec :
forall (A : Type) (l : list A) (n : nat) (x : A),
insert l n x = take n l ++ x :: drop n l.
Lemma insert_take :
forall (A : Type) (l : list A) (n m : nat) (x : A),
insert (take n l) m x =
if leb m n
then take (S n) (insert l m x)
else snoc x (take n l).
Lemma take_S_insert :
forall (A : Type) (l : list A) (n : nat) (x : A),
take (S n) (insert l n x) = snoc x (take n l).
Lemma take_insert :
forall (A : Type) (l : list A) (n m : nat) (x : A),
take m (insert l n x) =
if m <=? n then take m l else snoc x l.
Lemma drop_S_insert :
forall (A : Type) (l : list A) (n : nat) (x : A),
drop (S n) (insert l n x) = drop n l.
Lemma insert_drop :
forall (A : Type) (l : list A) (n m : nat) (x : A),
insert (drop n l) m x =
drop (n - 1) (insert l (n + m) x).
replace
Zdefiniuj funkcję
replace, która na liście
l zastępuje element z
pozycji
n elementem
x.
Przykład:
replace [1; 2; 3; 4; 5] 2 42 =
[1; 2; 42; 4; 5]
Lemma isEmpty_replace :
forall (A : Type) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
isEmpty l' = isEmpty l.
Lemma length_replace :
forall (A : Type) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' -> length l' = length l.
Lemma replace_length_lt :
forall (A : Type) (l : list A) (n : nat) (x : A),
n < length l ->
exists l' : list A, replace l n x = Some l'.
Lemma replace_length_ge :
forall (A : Type) (l : list A) (n : nat) (x : A),
length l <= n -> replace l n x = None.
Lemma replace_snoc_eq :
forall (A : Type) (l : list A) (n : nat) (x y : A),
n = length l -> replace (snoc x l) n y = Some (snoc y l).
Lemma replace_snoc_neq :
forall (A : Type) (l : list A) (n : nat) (x y : A),
n <> length l ->
replace (snoc x l) n y =
match replace l n y with
| None => None
| Some l' => Some (snoc x l')
end.
Lemma replace_snoc :
forall (A : Type) (l : list A) (n : nat) (x y : A),
replace (snoc x l) n y =
if beq_nat n (length l)
then Some (snoc y l)
else
match replace l n y with
| None => None
| Some l' => Some (snoc x l')
end.
Lemma replace_app :
forall (A : Type) (l1 l2 : list A) (n : nat) (x : A),
replace (l1 ++ l2) n x =
match replace l1 n x, replace l2 (n - length l1) x with
| None, None => None
| Some l', _ => Some (l' ++ l2)
| _, Some l' => Some (l1 ++ l')
end.
Lemma replace_spec :
forall (A : Type) (l : list A) (n : nat) (x : A),
replace l n x =
if n <? length l
then Some (take n l ++ x :: drop (S n) l)
else None.
Lemma replace_spec' :
forall (A : Type) (l : list A) (n : nat) (x : A),
n < length l ->
replace l n x = Some (take n l ++ x :: drop (S n) l).
Lemma replace_spec'' :
forall (A : Type) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' -> l' = take n l ++ x :: drop (S n) l.
Lemma replace_rev_aux :
forall (A : Type) (l : list A) (n : nat) (x : A),
n < length l ->
replace l n x =
match replace (rev l) (length l - S n) x with
| None => None
| Some l' => Some (rev l')
end.
Definition omap {A B: Type} (f : A -> B) (oa : option A) : option B :=
match oa with
| None => None
| Some a => Some (f a)
end.
Lemma replace_rev :
forall (A : Type) (l : list A) (n : nat) (x : A),
n < length l ->
replace (rev l) n x = omap rev (replace l (length l - S n) x).
Lemma map_replace :
forall (A B : Type) (f : A -> B) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
Some (map f l') = replace (map f l) n (f x).
Lemma replace_join :
forall (A : Type) (ll : list (list A)) (n : nat) (x : A) (l : list A),
replace (join ll) n x = Some l ->
exists n m : nat,
match nth n ll with
| None => False
| Some l' =>
match replace l' m x with
| None => False
| Some l'' =>
match replace ll n l'' with
| None => False
| Some ll' => join ll' = l
end
end
end.
Lemma replace_replicate :
forall (A : Type) (l l' : list A) (n m : nat) (x y : A),
replace (replicate n x) m y =
if n <=? m
then None
else Some (replicate m x ++ y :: replicate (n - S m) x).
Lemma replace_iterate :
forall (A : Type) (f : A -> A) (l : list A) (n m : nat) (x y : A),
replace (iterate f n x) m y =
if n <=? m
then None
else Some (iterate f m x ++
y :: iterate f (n - S m) (iter f (S m) x)).
Lemma head_replace :
forall (A : Type) (l l' : list A) (n : nat) (x y : A),
replace l n x = Some l' ->
head l' =
match n with
| 0 => Some x
| _ => head l
end.
Lemma tail_replace :
forall (A : Type) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
tail l' =
match n with
| 0 => tail l
| S n' =>
match tail l with
| None => None
| Some t => replace t n' x
end
end.
Lemma replace_length_aux :
forall (A : Type) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' -> length l = length l'.
Lemma nth_replace :
forall (A : Type) (l l' : list A) (n m : nat) (x : A),
replace l n x = Some l' ->
nth m l' = if n =? m then Some x else nth m l.
Lemma replace_nth_eq :
forall (A : Type) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
l = l' <-> nth n l = Some x.
Lemma last_replace :
forall (A : Type) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
last l' =
if n =? length l - 1
then Some x
else last l.
Lemma init_replace :
forall (A : Type) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
init l' =
match init l with
| None => None
| Some i => if length i <=? n then Some i else replace i n x
end.
Lemma take_replace :
forall (A : Type) (l l' : list A) (n m : nat) (x : A),
replace l n x = Some l' ->
take m l' =
if m <=? n
then take m l
else take n l ++ x :: take (m - S n) (drop (S n) l).
Lemma drop_replace :
forall (A : Type) (l l' : list A) (n m : nat) (x : A),
replace l n x = Some l' ->
drop m l' =
if n <? m
then drop m l
else take (n - m) (drop m l) ++ x :: drop (S n) l.
Lemma replace_insert :
forall (A : Type) (l : list A) (n : nat) (x y : A),
n <= length l ->
replace (insert l n x) n y = Some (insert l n y).
Lemma replace_plus :
forall (A : Type) (l : list A) (n m : nat) (x : A),
replace l (n + m) x =
match replace (drop n l) m x with
| None => None
| Some l' => Some (take n l ++ l')
end.
remove
Zdefiniuj funkcję
remove, która bierze liczbę naturalną
n oraz listę
l i zwraca parę składającą się z
n-tego elementu listy
l oraz
tego, co pozostanie na liście po jego usunięciu. Jeżeli lista jest za
krótka, funkcja ma zwracać
None.
Przykład:
remove 2 [1; 2; 3; 4; 5] =
Some (3, [1; 2; 4; 5])
remove 42 [1; 2; 3; 4; 5] =
None
Uwaga TODO: w ćwiczeniach jest burdel.
Lemma remove'_S_cons :
forall (A : Type) (n : nat) (h : A) (t : list A),
remove' (S n) (h :: t) = h :: remove' n t.
Lemma remove_isEmpty_true :
forall (A : Type) (l : list A) (n : nat),
isEmpty l = true -> remove n l = None.
Lemma isEmpty_remove_not_None :
forall (A : Type) (l : list A) (n : nat),
remove n l <> None -> isEmpty l = false.
Lemma isEmpty_remove :
forall (A : Type) (l l' : list A) (n : nat) (x : A),
remove n l = Some (x, l') ->
isEmpty l' = isEmpty l || ((length l <=? 1) && isZero n).
Lemma length_remove :
forall (A : Type) (h : A) (l t : list A) (n : nat),
remove n l = Some (h, t) -> length l = S (length t).
Lemma remove_length_lt :
forall (A : Type) (l : list A) (n : nat),
n < length l ->
nth n l =
match remove n l with
| None => None
| Some (h, _) => Some h
end.
Lemma remove_length_lt' :
forall (A : Type) (l : list A) (n : nat),
n < length l -> remove n l <> None.
Lemma remove_length_ge :
forall (A : Type) (l : list A) (n : nat),
length l <= n -> remove n l = None.
Lemma remove_length_snoc :
forall (A : Type) (x : A) (l : list A),
remove (length l) (snoc x l) = Some (x, l).
Lemma remove_snoc_lt :
forall (A : Type) (x : A) (l : list A) (n : nat),
n < length l ->
remove n (snoc x l) =
match remove n l with
| None => None
| Some (h, t) => Some (h, snoc x t)
end.
Lemma remove_app :
forall (A : Type) (l1 l2 : list A) (n : nat),
remove n (l1 ++ l2) =
match remove n l1 with
| Some (h, t) => Some (h, t ++ l2)
| None =>
match remove (n - length l1) l2 with
| Some (h, t) => Some (h, l1 ++ t)
| None => None
end
end.
Lemma remove_app_lt :
forall (A : Type) (l1 l2 : list A) (n : nat),
n < length l1 ->
remove n (l1 ++ l2) =
match remove n l1 with
| None => None
| Some (h, t) => Some (h, t ++ l2)
end.
Lemma remove_app_ge :
forall (A : Type) (l1 l2 : list A) (n : nat),
length l1 <= n ->
remove n (l1 ++ l2) =
match remove (n - length l1) l2 with
| None => None
| Some (h, t) => Some (h, l1 ++ t)
end.
Lemma remove'_app :
forall (A : Type) (n : nat) (l1 l2 : list A),
n < length l1 ->
remove' n (l1 ++ l2) = remove' n l1 ++ l2.
Lemma remove_app' :
forall (A : Type) (n : nat) (l1 l2 : list A),
length l1 <= n ->
remove' n (l1 ++ l2) = l1 ++ remove' (n - length l1) l2.
Lemma remove_rev_aux :
forall (A : Type) (l : list A) (n : nat),
n < length l ->
remove n l =
match remove (length l - S n) (rev l) with
| None => None
| Some (h, t) => Some (h, rev t)
end.
Lemma remove_rev :
forall (A : Type) (l : list A) (n : nat),
n < length l ->
remove n (rev l) =
match remove (length l - S n) l with
| None => None
| Some (h, t) => Some (h, rev t)
end.
Lemma remove_map :
forall (A B : Type) (f : A -> B) (l : list A) (n : nat),
remove n (map f l) =
match remove n l with
| None => None
| Some (x, l') => Some (f x, map f l')
end.
Lemma remove_replicate :
forall (A : Type) (n m : nat) (x : A),
m < n -> remove m (replicate n x) = Some (x, replicate (n - 1) x).
Lemma remove_iterate :
forall (A : Type) (f : A -> A) (n m : nat) (x : A),
m < n ->
remove m (iterate f n x) =
Some (iter f m x,
iterate f m x ++
(iterate f (n - S m) (iter f (S m) x))).
Lemma remove_nth_take_drop :
forall (A : Type) (l : list A) (n : nat) (x : A),
nth n l = Some x <->
remove n l = Some (x, take n l ++ drop (S n) l).
Lemma remove_insert :
forall (A : Type) (l : list A) (n : nat) (x : A),
n < length l ->
remove n (insert l n x) = Some (x, l).
Lemma remove'_replace :
forall (A : Type) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
remove' n l' = remove' n l.
zip
Zdefiniuj funkcję
zip, która bierze dwie listy i skleja je w listę par.
Wywnioskuj z poniższej specyfikacji, jak dokładnie ma się zachowywać
ta funkcja.
Przykład:
zip [1; 3; 5; 7] [2; 4; 6] =
[(1, 2); (3, 4); (5, 6)]
Lemma zip_nil_l :
forall (A B : Type) (l : list B), zip (@nil A) l = [].
Lemma zip_nil_r :
forall (A B : Type) (l : list A), zip l (@nil B) = [].
Lemma isEmpty_zip :
forall (A B : Type) (la : list A) (lb : list B),
isEmpty (zip la lb) = orb (isEmpty la) (isEmpty lb).
Lemma length_zip :
forall (A B : Type) (la : list A) (lb : list B),
length (zip la lb) = min (length la) (length lb).
Lemma zip_not_rev :
exists (A B : Type) (la : list A) (lb : list B),
zip (rev la) (rev lb) <> rev (zip la lb).
Lemma head_zip :
forall (A B : Type) (la : list A) (lb : list B) (a : A) (b : B),
head la = Some a -> head lb = Some b ->
head (zip la lb) = Some (a, b).
Lemma tail_zip :
forall (A B : Type) (la ta : list A) (lb tb : list B),
tail la = Some ta -> tail lb = Some tb ->
tail (zip la lb) = Some (zip ta tb).
Lemma zip_not_app :
exists (A B : Type) (la la' : list A) (lb lb' : list B),
zip (la ++ la') (lb ++ lb') <> zip la lb ++ zip la' lb'.
Lemma zip_map :
forall (A B A' B' : Type) (f : A -> A') (g : B -> B')
(la : list A) (lb : list B),
zip (map f la) (map g lb) =
map (fun x => (f (fst x), g (snd x))) (zip la lb).
Lemma zip_replicate :
forall (A B : Type) (n m : nat) (a : A) (b : B),
zip (replicate n a) (replicate m b) =
replicate (min n m) (a, b).
Lemma zip_iterate :
forall
(A B : Type) (fa : A -> A) (fb : B -> B) (na nb : nat) (a : A) (b : B),
zip (iterate fa na a) (iterate fb nb b) =
iterate (fun '(a, b) => (fa a, fb b)) (min na nb) (a, b).
Lemma nth_zip :
forall (A B : Type) (la : list A) (lb : list B) (n : nat),
nth n (zip la lb) =
if n <=? min (length la) (length lb)
then
match nth n la, nth n lb with
| Some a, Some b => Some (a, b)
| _, _ => None
end
else None.
Lemma nth_zip' :
forall (A B : Type) (la : list A) (lb : list B) (n : nat),
nth n (zip la lb) =
match nth n la, nth n lb with
| Some a, Some b => Some (a, b)
| _, _ => None
end.
Lemma zip_take :
forall (A B : Type) (la : list A) (lb : list B) (n : nat),
zip (take n la) (take n lb) = take n (zip la lb).
Lemma zip_drop :
forall (A B : Type) (la: list A) (lb : list B) (n : nat),
zip (drop n la) (drop n lb) = drop n (zip la lb).
Lemma splitAt_zip :
forall (A B : Type) (la : list A) (lb : list B) (n : nat),
splitAt n (zip la lb) =
match splitAt n la, splitAt n lb with
| Some (la1, a, la2), Some (lb1, b, lb2) =>
Some (zip la1 lb1, (a, b), zip la2 lb2)
| _, _ => None
end.
Lemma insert_zip :
forall (A B : Type) (la : list A) (lb : list B) (a : A) (b : B) (n : nat),
insert (zip la lb) n (a, b) =
if n <=? min (length la) (length lb)
then zip (insert la n a) (insert lb n b)
else snoc (a, b) (zip la lb).
Lemma replace_zip :
forall
(A B : Type) (la la' : list A) (lb lb' : list B)
(n : nat) (a : A) (b : B),
replace la n a = Some la' ->
replace lb n b = Some lb' ->
replace (zip la lb) n (a, b) = Some (zip la' lb').
Lemma replace_zip' :
forall
(A B : Type) (la : list A) (lb : list B) (n : nat) (a : A) (b : B),
replace (zip la lb) n (a, b) =
match replace la n a, replace lb n b with
| Some la', Some lb' => Some (zip la' lb')
| _, _ => None
end.
Lemma remove_zip :
forall (A B : Type) (la : list A) (lb : list B) (n : nat),
remove n (zip la lb) =
match remove n la, remove n lb with
| Some (a, la'), Some (b, lb') => Some ((a, b), zip la' lb')
| _, _ => None
end.
unzip
Zdefiniuj funkcję
unzip, która rozdziela listę par na dwie listy:
lewa lista zawiera lewe komponenty par, a prawa lista - prawe
komponenty par.
Przykład:
unzip [(1, 2); (3, 4); (5, 6)] =
([1; 3; 5], [2; 4; 6])
Lemma zip_unzip :
forall (A B : Type) (l : list (A * B)),
zip (fst (unzip l)) (snd (unzip l)) = l.
Lemma unzip_zip :
exists (A B : Type) (la : list A) (lb : list B),
unzip (zip la lb) <> (la, lb).
Lemma isEmpty_unzip :
forall (A B : Type) (l : list (A * B)) (la : list A) (lb : list B),
unzip l = (la, lb) -> isEmpty l = orb (isEmpty la) (isEmpty lb).
Lemma unzip_snoc :
forall (A B : Type) (x : A * B) (l : list (A * B)),
unzip (snoc x l) =
let (la, lb) := unzip l in (snoc (fst x) la, snoc (snd x) lb).
zipWith
Zdefiniuj funkcję
zipWith, która zachowuje się jak połączenie
zip
i
map. Nie używaj
zip ani
map - użyj rekursji.
Przykład:
zipWith plus [1; 2; 3] [4; 5; 6] =
[5; 7; 9]
Lemma zipWith_spec :
forall (A B C : Type) (f : A -> B -> C)
(la : list A) (lb : list B),
zipWith f la lb =
map (fun '(a, b) => f a b) (zip la lb).
Lemma zipWith_pair :
forall (A B : Type) (la : list A) (lb : list B),
zipWith pair la lb = zip la lb.
Lemma isEmpty_zipWith :
forall (A B C : Type) (f : A -> B -> C) (la : list A) (lb : list B),
isEmpty (zipWith f la lb) = orb (isEmpty la) (isEmpty lb).
Lemma zipWith_snoc :
forall
(A B C : Type) (f : A -> B -> C)
(a : A) (b : B) (la : list A) (lb : list B),
length la = length lb ->
zipWith f (snoc a la) (snoc b lb) =
snoc (f a b) (zipWith f la lb).
Lemma zipWith_iterate :
forall
(A B C: Type) (fa : A -> A) (fb : B -> B) (g : A -> B -> C)
(na nb : nat) (a : A) (b : B),
zipWith g (iterate fa na a) (iterate fb nb b) =
map (fun '(a, b) => g a b)
(iterate (fun '(a, b) => (fa a, fb b)) (min na nb) (a, b)).
Lemma take_zipWith :
forall
(A B C : Type) (f : A -> B -> C) (la : list A) (lb : list B) (n : nat),
take n (zipWith f la lb) = zipWith f (take n la) (take n lb).
Lemma drop_zipWith :
forall
(A B C : Type) (f : A -> B -> C) (la : list A) (lb : list B) (n : nat),
drop n (zipWith f la lb) = zipWith f (drop n la) (drop n lb).
Lemma splitAt_zipWith :
forall (A B C : Type) (f : A -> B -> C)
(la : list A) (lb : list B) (n : nat),
splitAt n (zipWith f la lb) =
match splitAt n la, splitAt n lb with
| Some (la1, a, la2), Some (lb1, b, lb2) =>
Some (zipWith f la1 lb1, f a b, zipWith f la2 lb2)
| _, _ => None
end.
Lemma replace_zipWith :
forall
(A B C : Type) (f : A -> B -> C) (la la' : list A) (lb lb' : list B)
(n : nat) (a : A) (b : B),
replace la n a = Some la' ->
replace lb n b = Some lb' ->
replace (zipWith f la lb) n (f a b) = Some (zipWith f la' lb').
Lemma remove_zipWith :
forall (A B C : Type) (f : A -> B -> C)
(la : list A) (lb : list B) (n : nat),
remove n (zipWith f la lb) =
match remove n la, remove n lb with
| Some (a, la'), Some (b, lb') =>
Some (f a b, zipWith f la' lb')
| _, _ => None
end.
unzipWith
Zdefiniuj funkcję
unzipWith, która ma się tak do
zipWith, jak
unzip do
zip. Oczywiście użyj rekursji i nie używaj żadnych
funkcji pomocniczych.
Lemma isEmpty_unzipWith :
forall (A B C : Type) (f : A -> B * C) (l : list A)
(lb : list B) (lc : list C),
unzipWith f l = (lb, lc) ->
isEmpty l = orb (isEmpty lb) (isEmpty lc).
Lemma unzipWith_spec :
forall (A B C : Type) (f : A -> B * C) (l : list A),
unzipWith f l = unzip (map f l).
Lemma unzipWith_id :
forall (A B : Type) (l : list (A * B)),
unzipWith id l = unzip l.
Funkcje z predykatem boolowskim
any
Zdefiniuj funkcję
any, która sprawdza, czy lista
l zawiera jakiś
element, który spełnia predykat boolowski
p.
Przykład:
any even [3; 5; 7; 11] =
false
Lemma any_isEmpty_true :
forall (A : Type) (p : A -> bool) (l : list A),
isEmpty l = true -> any p l = false.
Lemma isEmpty_any_true :
forall (A : Type) (p : A -> bool) (l : list A),
any p l = true -> isEmpty l = false.
Lemma any_length :
forall (A : Type) (p : A -> bool) (l : list A),
any p l = true -> 1 <= length l.
Lemma any_snoc :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
any p (snoc x l) = orb (any p l) (p x).
Lemma any_app :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
any p (l1 ++ l2) = orb (any p l1) (any p l2).
Lemma any_rev :
forall (A : Type) (p : A -> bool) (l : list A),
any p (rev l) = any p l.
Lemma any_map :
forall (A B : Type) (f : A -> B) (p : B -> bool) (l : list A),
any p (map f l) = any (fun x : A => p (f x)) l.
Lemma any_join :
forall (A : Type) (p : A -> bool) (l : list (list A)),
any p (join l) = any (any p) l.
Lemma any_replicate :
forall (A : Type) (p : A -> bool) (n : nat) (x : A),
any p (replicate n x) = andb (leb 1 n) (p x).
Lemma any_iterate :
forall (A : Type) (p : A -> bool) (f : A -> A) (n : nat) (x : A),
(forall x : A, p (f x) = p x) ->
any p (iterate f n x) =
match n with
| 0 => false
| _ => p x
end.
Lemma any_nth :
forall (A : Type) (p : A -> bool) (l : list A),
any p l = true <->
exists (n : nat) (x : A), nth n l = Some x /\ p x = true.
Lemma any_take :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
any p (take n l) = true -> any p l = true.
Lemma any_take_conv :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
any p l = false -> any p (take n l) = false.
Lemma any_drop :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
any p (drop n l) = true -> any p l = true.
Lemma any_drop_conv :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
any p l = false -> any p (drop n l) = false.
Lemma any_cycle :
forall (A : Type) (p : A -> bool) (n : nat) (l : list A),
any p (cycle n l) = any p l.
Lemma any_insert :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat) (x : A),
any p (insert l n x) = orb (p x) (any p l).
Lemma any_replace :
forall (A : Type) (p : A -> bool) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
any p l' = any p (take n l) || p x || any p (drop (S n) l).
Lemma any_replace' :
forall (A : Type) (p : A -> bool) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
any p l = true -> p x = true -> any p l' = true.
Lemma any_true :
forall (A : Type) (l : list A),
any (fun _ => true) l = negb (isEmpty l).
Lemma any_false :
forall (A : Type) (l : list A),
any (fun _ => false) l = false.
Lemma any_orb :
forall (A : Type) (p q : A -> bool) (l : list A),
any (fun x : A => orb (p x) (q x)) l =
orb (any p l) (any q l).
Lemma any_andb :
forall (A : Type) (p q : A -> bool) (l : list A),
any (fun x : A => andb (p x) (q x)) l = true ->
any p l = true /\ any q l = true.
all
Zdefiniuj funkcję
all, która sprawdza, czy wszystkie wartości na liście
l spełniają predykat boolowski
p.
Przykład:
all even [2; 4; 6] =
true
Lemma all_isEmpty_true :
forall (A : Type) (p : A -> bool) (l : list A),
isEmpty l = true -> all p l = true.
Lemma isEmpty_all_false :
forall (A : Type) (p : A -> bool) (l : list A),
all p l = false -> isEmpty l = false.
Lemma all_length :
forall (A : Type) (p : A -> bool) (l : list A),
all p l = false -> 1 <= length l.
Lemma all_snoc :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
all p (snoc x l) = andb (all p l) (p x).
Lemma all_app :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
all p (l1 ++ l2) = andb (all p l1) (all p l2).
Lemma all_rev :
forall (A : Type) (p : A -> bool) (l : list A),
all p (rev l) = all p l.
Lemma all_map :
forall (A B : Type) (f : A -> B) (p : B -> bool) (l : list A),
all p (map f l) = all (fun x : A => p (f x)) l.
Lemma all_join :
forall (A : Type) (p : A -> bool) (l : list (list A)),
all p (join l) = all (all p) l.
Lemma all_replicate :
forall (A : Type) (p : A -> bool) (n : nat) (x : A),
all p (replicate n x) = orb (n <=? 0) (p x).
Lemma all_iterate :
forall (A : Type) (p : A -> bool) (f : A -> A) (n : nat) (x : A),
(forall x : A, p (f x) = p x) ->
all p (iterate f n x) = orb (isZero n) (p x).
Lemma all_nth :
forall (A : Type) (p : A -> bool) (l : list A),
all p l = true <->
forall n : nat, n < length l -> exists x : A,
nth n l = Some x /\ p x = true.
Lemma all_take :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
all p (take n l) = false -> all p l = false.
Lemma all_take_conv :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
all p l = true -> all p (take n l) = true.
Lemma all_drop :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
all p (drop n l) = false -> all p l = false.
Lemma all_drop_conv :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
all p l = true -> all p (drop n l) = true.
Lemma all_insert :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat) (x : A),
all p (insert l n x) = andb (p x) (all p l).
Lemma all_replace :
forall (A : Type) (p : A -> bool) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
all p l' = all p (take n l) && p x && all p (drop (S n) l).
Lemma all_replace' :
forall (A : Type) (p : A -> bool) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
all p l = true -> p x = true -> all p l' = true.
Lemma all_true :
forall (A : Type) (l : list A),
all (fun _ => true) l = true.
Lemma all_false :
forall (A : Type) (l : list A),
all (fun _ => false) l = isEmpty l.
Lemma all_orb :
forall (A : Type) (p q : A -> bool) (l : list A),
orb (all p l) (all q l) = true ->
all (fun x : A => orb (p x) (q x)) l = true.
Lemma all_andb :
forall (A : Type) (p q : A -> bool) (l : list A),
all (fun x : A => andb (p x) (q x)) l =
andb (all p l) (all q l).
Lemma any_all :
forall (A : Type) (p : A -> bool) (l : list A),
any p l = negb (all (fun x : A => negb (p x)) l).
Lemma all_any :
forall (A : Type) (p : A -> bool) (l : list A),
all p l = negb (any (fun x : A => negb (p x)) l).
Lemma all_cycle :
forall (A : Type) (p : A -> bool) (n : nat) (l : list A),
all p (cycle n l) = all p l.
Lemma isEmpty_join :
forall (A : Type) (l : list (list A)),
isEmpty (join l) = all isEmpty l.
find i findLast
Zdefiniuj funkcję
find, która znajduje pierwszy element na liście,
który spełnia podany predykat boolowski.
Przykład:
find even [1; 2; 3; 4] =
Some 2
Zdefiniuj też funkcję
findLast, która znajduje ostatni element na
liście, który spełnia podany predykat boolowski.
Przykład:
findLast even [1; 2; 3; 4] =
Some 4
Lemma find_false :
forall (A : Type) (l : list A),
find (fun _ => false) l = None.
Lemma find_true :
forall (A : Type) (l : list A),
find (fun _ => true) l = head l.
Lemma find_isEmpty_true :
forall (A : Type) (p : A -> bool) (l : list A),
isEmpty l = true -> find p l = None.
Lemma isEmpty_find_not_None :
forall (A : Type) (p : A -> bool) (l : list A),
find p l <> None -> isEmpty l = false.
Lemma find_length :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
find p l = Some x -> 1 <= length l.
Lemma find_snoc :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
find p (snoc x l) =
match find p l with
| None => if p x then Some x else None
| Some y => Some y
end.
Lemma findLast_snoc :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
findLast p (snoc x l) =
if p x then Some x else findLast p l.
Lemma find_app :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
find p (l1 ++ l2) =
match find p l1 with
| Some x => Some x
| None => find p l2
end.
Lemma find_rev :
forall (A : Type) (p : A -> bool) (l : list A),
find p (rev l) = findLast p l.
Lemma find_findLast :
forall (A : Type) (p : A -> bool) (l : list A),
find p l = findLast p (rev l).
Lemma find_map :
forall (A B : Type) (f : A -> B) (p : B -> bool) (l : list A),
find p (map f l) =
match find (fun x : A => p (f x)) l with
| None => None
| Some a => Some (f a)
end.
Lemma find_join :
forall (A : Type) (p : A -> bool) (l : list (list A)),
find p (join l) =
(fix aux (l : list (list A)) : option A :=
match l with
| [] => None
| h :: t =>
match find p h with
| None => aux t
| Some x => Some x
end
end) l.
Lemma find_replicate :
forall (A : Type) (p : A -> bool) (n : nat) (x : A),
find p (replicate n x) =
match n, p x with
| 0, _ => None
| _, false => None
| _, true => Some x
end.
Lemma find_iterate :
forall (A : Type) (p : A -> bool) (f : A -> A) (n : nat) (x : A),
(forall x : A, p (f x) = p x) ->
find p (iterate f n x) =
if isZero n then None else if p x then Some x else None.
Lemma findLast_iterate :
forall (A : Type) (p : A -> bool) (f : A -> A) (n : nat) (x : A),
(forall x : A, p (f x) = p x) ->
findLast p (iterate f n x) =
match n with
| 0 => None
| S n' => if p x then Some (iter f n' x) else None
end.
Lemma find_nth :
forall (A : Type) (p : A -> bool) (l : list A),
(exists (n : nat) (x : A), nth n l = Some x /\ p x = true) <->
find p l <> None.
Lemma find_tail :
forall (A : Type) (p : A -> bool) (l t : list A),
tail l = Some t -> find p t <> None -> find p l <> None.
Lemma find_init :
forall (A : Type) (p : A -> bool) (l t : list A),
init l = Some t -> find p t <> None -> find p l <> None.
Lemma find_take_Some :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat) (x : A),
find p (take n l) = Some x -> find p l = Some x.
Lemma find_take_None :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
find p l = None -> find p (take n l) = None.
Lemma find_drop_not_None :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
find p (drop n l) <> None -> find p l <> None.
Lemma find_drop_None :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
find p l = None -> find p (drop n l) = None.
Lemma findLast_take :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
findLast p (take n l) <> None -> findLast p l <> None.
Lemma findLast_drop :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat) (x : A),
findLast p (drop n l) = Some x -> findLast p l = Some x.
Lemma find_replace :
forall (A : Type) (p : A -> bool) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
find p l' =
match find p (take n l), p x with
| Some y, _ => Some y
| _, true => Some x
| _, _ => find p (drop (S n) l)
end.
Lemma replace_findLast :
forall (A : Type) (p : A -> bool) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
findLast p l' =
match findLast p (drop (S n) l), p x with
| Some y, _ => Some y
| _, true => Some x
| _, _ => findLast p (take n l)
end.
removeFirst i removeLast
Zdefiniuj funkcje
removeFirst i
removeLast o sygnaturach,
które zwracają pierwszy/ostatni element z listy spełniający
predykat boolowski
p oraz resztę listy bez tego elementu.
Przykład:
removeFirst even [1; 2; 3; 4] =
Some (2, [1; 3; 4])
removeLast even [1; 2; 3; 4] =
Some (4, [1; 2; 3])
Lemma removeFirst_isEmpty_true :
forall (A : Type) (p : A -> bool) (l : list A),
isEmpty l = true -> removeFirst p l = None.
Lemma isEmpty_removeFirst_not_None :
forall (A : Type) (p : A -> bool) (l : list A),
removeFirst p l <> None -> isEmpty l = false.
Lemma removeFirst_satisfies :
forall (A : Type) (p : A -> bool) (l l' : list A) (x : A),
removeFirst p l = Some (x, l') -> p x = true.
Lemma removeFirst_length :
forall (A : Type) (p : A -> bool) (l : list A),
length l = 0 -> removeFirst p l = None.
Lemma removeFirst_snoc :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
removeFirst p (snoc x l) =
match removeFirst p l with
| None => if p x then Some (x, l) else None
| Some (h, t) => Some (h, snoc x t)
end.
Lemma removeLast_snoc :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
removeLast p (snoc x l) =
if p x
then Some (x, l)
else
match removeLast p l with
| None => None
| Some (h, t) => Some (h, snoc x t)
end.
Lemma removeFirst_app :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
removeFirst p (l1 ++ l2) =
match removeFirst p l1, removeFirst p l2 with
| Some (h, t), _ => Some (h, t ++ l2)
| _, Some (h, t) => Some (h, l1 ++ t)
| _, _ => None
end.
Lemma removeLast_app :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
removeLast p (l1 ++ l2) =
match removeLast p l2, removeLast p l1 with
| Some (y, l'), _ => Some (y, l1 ++ l')
| _, Some (y, l') => Some (y, l' ++ l2)
| _, _ => None
end.
Lemma removeFirst_rev :
forall (A : Type) (p : A -> bool) (l : list A),
removeFirst p (rev l) =
match removeLast p l with
| Some (x, l) => Some (x, rev l)
| None => None
end.
Lemma removeLast_rev :
forall (A : Type) (p : A -> bool) (l : list A),
removeLast p (rev l) =
match removeFirst p l with
| None => None
| Some (x, l) => Some (x, rev l)
end.
Lemma removeFirst_map :
forall (A B : Type) (p : B -> bool) (f : A -> B) (l : list A),
removeFirst p (map f l) =
match removeFirst (fun x => p (f x)) l with
| Some (x, l) => Some (f x, map f l)
| None => None
end.
Lemma removeFirst_join :
forall (A : Type) (p : A -> bool) (l : list (list A)),
removeFirst p (join l) =
(fix f (l : list (list A)) : option (A * list A) :=
match l with
| [] => None
| hl :: tl =>
match removeFirst p hl with
| Some (x, l') => Some (x, join (l' :: tl))
| None =>
match f tl with
| Some (x, l) => Some (x, hl ++ l)
| None => None
end
end
end) l.
Lemma removeFirst_replicate :
forall (A : Type) (p : A -> bool) (n : nat) (x : A),
removeFirst p (replicate n x) =
if p x
then
match n with
| 0 => None
| S n' => Some (x, replicate n' x)
end
else None.
Lemma removeFirst_nth_None :
forall (A : Type) (p : A -> bool) (l : list A),
removeFirst p l = None <->
forall (n : nat) (x : A), nth n l = Some x -> p x = false.
Lemma removeFirst_nth_Some :
forall (A : Type) (p : A -> bool) (x : A) (l l' : list A),
removeFirst p l = Some (x, l') ->
exists n : nat, nth n l = Some x /\ p x = true.
Lemma removeFirst_nth_Some' :
exists (A : Type) (p : A -> bool) (n : nat) (x y : A) (l l' : list A),
removeFirst p l = Some (x, l') /\
nth n l = Some y /\ p y = true.
Lemma head_removeFirst :
forall (A : Type) (p : A -> bool) (x : A) (l l' : list A),
removeFirst p l = Some (x, l') ->
head l' =
match l with
| [] => None
| h :: t => if p h then head t else Some h
end.
Lemma removeFirst_take_None :
forall (A : Type) (p : A -> bool) (n : nat) (l : list A),
removeFirst p l = None -> removeFirst p (take n l) = None.
Lemma removeFirst_take :
forall (A : Type) (p : A -> bool) (n : nat) (x : A) (l l' : list A),
removeFirst p (take n l) = Some (x, l') ->
removeFirst p l = Some (x, l' ++ drop n l).
Lemma removeLast_drop :
forall (A : Type) (p : A -> bool) (n : nat) (x : A) (l l' : list A),
removeLast p (drop n l) = Some (x, l') ->
removeLast p l = Some (x, take n l ++ l').
Lemma removeFirst_replace :
forall (A : Type) (p : A -> bool) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
removeFirst p l' =
match removeFirst p (take n l), p x, removeFirst p (drop (S n) l) with
| Some (y, l''), _, _ => Some (y, l'' ++ x :: drop (S n) l)
| _, true, _ => Some (x, take n l ++ drop (S n) l)
| _, _, Some (y, l'') => Some (y, take n l ++ x :: l'')
| _, _, _ => None
end.
Lemma removeLast_replace :
forall (A : Type) (p : A -> bool) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
removeLast p l' =
match removeLast p (drop (S n) l), p x, removeLast p (take n l) with
| Some (y, l''), _ , _ => Some (y, take n l ++ x :: l'')
| _, true, _ => Some (x, take n l ++ drop (S n) l)
| _, _, Some (y, l'') => Some (y, l'' ++ x :: drop (S n) l)
| _, _, _ => None
end.
Lemma removeFirst_any_None :
forall (A : Type) (p : A -> bool) (l : list A),
removeFirst p l = None <-> any p l = false.
Lemma removeFirst_not_None_any :
forall (A : Type) (p : A -> bool) (l : list A),
removeFirst p l <> None <-> any p l = true.
Lemma removeFirst_None_iff_all :
forall (A : Type) (p : A -> bool) (l : list A),
removeFirst p l = None <->
all (fun x : A => negb (p x)) l = true.
findIndex
Zdefiniuj funkcję
findIndex, która znajduje indeks pierwszego elementu,
który spełnia predykat boolowski
p. Pamiętaj, że indeksy liczone są
od 0.
Przykład:
findIndex even [1; 3; 4; 5; 7] =
2
Lemma findIndex_false :
forall (A : Type) (l : list A),
findIndex (fun _ => false) l = None.
Lemma findIndex_true :
forall (A : Type) (l : list A),
findIndex (fun _ => true) l =
match l with
| [] => None
| _ => Some 0
end.
Lemma findIndex_orb :
forall (A : Type) (p q : A -> bool) (l : list A),
findIndex (fun x : A => orb (p x) (q x)) l =
match findIndex p l, findIndex q l with
| Some n, Some m => Some (min n m)
| Some n, None => Some n
| None, Some m => Some m
| _, _ => None
end.
Lemma findIndex_isEmpty_true :
forall (A : Type) (p : A -> bool) (l : list A),
isEmpty l = true -> findIndex p l = None.
Lemma isEmpty_findIndex_not_None :
forall (A : Type) (p : A -> bool) (l : list A),
findIndex p l <> None -> isEmpty l = false.
Lemma findIndex_length :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
findIndex p l = Some n -> n < length l.
Lemma findIndex_snoc :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
findIndex p (snoc x l) =
match findIndex p l with
| None => if p x then Some (length l) else None
| Some n => Some n
end.
Lemma findIndex_app_l :
forall (A : Type) (p : A -> bool) (l1 l2 : list A) (n : nat),
findIndex p l1 = Some n -> findIndex p (l1 ++ l2) = Some n.
Lemma findIndex_app_r :
forall (A : Type) (p : A -> bool) (l1 l2 : list A) (n : nat),
findIndex p l1 = None -> findIndex p l2 = Some n ->
findIndex p (l1 ++ l2) = Some (length l1 + n).
Lemma findIndex_app_None :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
findIndex p l1 = None -> findIndex p l2 = None ->
findIndex p (l1 ++ l2) = None.
Lemma findIndex_app :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
findIndex p (l1 ++ l2) =
match findIndex p l1, findIndex p l2 with
| Some n, _ => Some n
| _, Some n => Some (length l1 + n)
| _, _ => None
end.
Lemma findIndex_map :
forall (A B : Type) (p : B -> bool) (f : A -> B) (l : list A) (n : nat),
findIndex (fun x : A => p (f x)) l = Some n ->
findIndex p (map f l) = Some n.
Lemma findIndex_map_conv :
forall (A B : Type) (p : B -> bool) (f : A -> B) (l : list A) (n : nat),
(forall x y : A, f x = f y -> x = y) ->
findIndex p (map f l) = Some n ->
findIndex (fun x : A => p (f x)) l = Some n.
Lemma findIndex_join :
forall (A : Type) (p : A -> bool) (ll : list (list A)),
findIndex p (join ll) =
match ll with
| [] => None
| h :: t =>
match findIndex p h, findIndex p (join t) with
| Some n, _ => Some n
| _, Some n => Some (length h + n)
| _, _ => None
end
end.
Lemma findIndex_replicate :
forall (A : Type) (p : A -> bool) (n : nat) (x : A),
findIndex p (replicate n x) =
match n with
| 0 => None
| _ => if p x then Some 0 else None
end.
Lemma findIndex_nth :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
findIndex p l = Some n ->
exists x : A, nth n l = Some x /\ p x = true.
Lemma findIndex_nth_conv :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat) (x : A),
nth n l = Some x -> p x = true ->
exists m : nat, findIndex p l = Some m /\ m <= n.
Lemma findIndex_nth' :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
findIndex p l = Some n -> find p l = nth n l.
Lemma findIndex_head :
forall (A : Type) (p : A -> bool) (l : list A),
findIndex p l = Some 0 <->
exists x : A, head l = Some x /\ p x = true.
Lemma findIndex_last :
forall (A : Type) (p : A -> bool) (l : list A),
findIndex p l = Some (length l - 1) <->
exists x : A,
last l = Some x /\
p x = true /\
forall (n : nat) (y : A),
n < length l - 1 -> nth n l = Some y -> p y = false.
Lemma findIndex_spec :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
findIndex p l = Some n ->
forall m : nat, m < n ->
exists x : A, nth m l = Some x /\ p x = false.
Lemma findIndex_take :
forall (A : Type) (p : A -> bool) (l : list A) (n m : nat),
findIndex p (take n l) = Some m ->
findIndex p l = Some m /\ m <= n.
Lemma findIndex_drop :
forall (A : Type) (p : A -> bool) (l : list A) (n m : nat),
findIndex p l = Some m -> n <= m ->
findIndex p (drop n l) = Some (m - n).
Lemma findIndex_zip :
forall (A B : Type) (pa : A -> bool) (pb : B -> bool)
(la : list A) (lb : list B) (n : nat),
findIndex pa la = Some n -> findIndex pb lb = Some n ->
findIndex (fun '(a, b) => andb (pa a) (pb b)) (zip la lb) = Some n.
Lemma findIndex_zip_conv :
forall (A B : Type) (pa : A -> bool) (pb : B -> bool)
(la : list A) (lb : list B) (n : nat),
findIndex (fun '(a, b) => andb (pa a) (pb b)) (zip la lb) = Some n ->
exists na nb : nat,
findIndex pa la = Some na /\
findIndex pb lb = Some nb /\
na <= n /\
nb <= n.
count
Zdefiniuj funkcję
count, która liczy, ile jest na liście
l elementów
spełniających predykat boolowski
p.
Przykład:
count even [1; 2; 3; 4] =
2
Lemma count_isEmpty :
forall (A : Type) (p : A -> bool) (l : list A),
isEmpty l = true -> count p l = 0.
Lemma isEmpty_count_not_0 :
forall (A : Type) (p : A -> bool) (l : list A),
count p l <> 0 -> isEmpty l = false.
Lemma count_length :
forall (A : Type) (p : A -> bool) (l : list A),
count p l <= length l.
Lemma count_snoc :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
count p (snoc x l) = count p l + if p x then 1 else 0.
Lemma count_app :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
count p (l1 ++ l2) = count p l1 + count p l2.
Lemma count_rev :
forall (A : Type) (p : A -> bool) (l : list A),
count p (rev l) = count p l.
Lemma count_map :
forall (A B : Type) (f : A -> B) (p : B -> bool) (l : list A),
count p (map f l) = count (fun x : A => p (f x)) l.
Lemma count_replicate :
forall (A : Type) (p : A -> bool) (n : nat) (x : A),
count p (replicate n x) =
if p x then n else 0.
Lemma count_insert :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat) (x : A),
count p (insert l n x) =
(if p x then 1 else 0) + count p l.
Lemma count_replace :
forall (A : Type) (p : A -> bool) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
count p l' = count p (take n l) + count p [x] + count p (drop (S n) l).
Lemma count_remove :
forall (A : Type) (p : A -> bool) (l l' : list A) (n : nat) (x : A),
remove n l = Some (x, l') ->
S (count p l') = if p x then count p l else S (count p l).
Lemma count_take :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
count p (take n l) <= n.
Lemma count_take' :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
count p (take n l) <= min n (count p l).
Lemma count_drop :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
count p (drop n l) <= length l - n.
Lemma count_cycle :
forall (A : Type) (p : A -> bool) (n : nat) (l : list A),
count p (cycle n l) = count p l.
Lemma count_splitAt :
forall (A : Type) (p : A -> bool) (l l1 l2 : list A) (n : nat) (x : A),
splitAt n l = Some (l1, x, l2) ->
count p l = (if p x then 1 else 0) + count p l1 + count p l2.
Lemma count_false :
forall (A : Type) (l : list A),
count (fun _ => false) l = 0.
Lemma count_true :
forall (A : Type) (l : list A),
count (fun _ => true) l = length l.
Lemma count_negb :
forall (A : Type) (p : A -> bool) (l : list A),
count (fun x : A => negb (p x)) l = length l - count p l.
Lemma count_andb_le_l :
forall (A : Type) (p q : A -> bool) (l : list A),
count (fun x : A => andb (p x) (q x)) l <= count p l.
Lemma count_andb_le_r :
forall (A : Type) (p q : A -> bool) (l : list A),
count (fun x : A => andb (p x) (q x)) l <= count q l.
Lemma count_orb :
forall (A : Type) (p q : A -> bool) (l : list A),
count (fun x : A => orb (p x) (q x)) l =
(count p l + count q l) - count (fun x : A => andb (p x) (q x)) l.
Lemma count_orb_le :
forall (A : Type) (p q : A -> bool) (l : list A),
count (fun x : A => orb (p x) (q x)) l <=
count p l + count q l.
Lemma count_andb :
forall (A : Type) (p q : A -> bool) (l : list A),
count (fun x : A => andb (p x) (q x)) l =
count p l + count q l - count (fun x : A => orb (p x) (q x)) l.
filter
Zdefiniuj funkcję
filter, która zostawia na liście elementy, dla których
funkcja
p zwraca
true, a usuwa te, dla których zwraca
false.
Przykład:
filter even [1; 2; 3; 4] =
[2; 4]
Lemma filter_false :
forall (A : Type) (l : list A),
filter (fun _ => false) l = [].
Lemma filter_true :
forall (A : Type) (l : list A),
filter (fun _ => true) l = l.
Lemma filter_andb :
forall (A : Type) (f g : A -> bool) (l : list A),
filter (fun x : A => andb (f x) (g x)) l =
filter f (filter g l).
Lemma isEmpty_filter :
forall (A : Type) (p : A -> bool) (l : list A),
isEmpty (filter p l) = all (fun x : A => negb (p x)) l.
Lemma length_filter :
forall (A : Type) (p : A -> bool) (l : list A),
length (filter p l) <= length l.
Lemma filter_snoc :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
filter p (snoc x l) =
if p x then snoc x (filter p l) else filter p l.
Lemma filter_app :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
filter p (l1 ++ l2) = filter p l1 ++ filter p l2.
Lemma filter_rev :
forall (A : Type) (p : A -> bool) (l : list A),
filter p (rev l) = rev (filter p l).
Lemma filter_map :
forall (A B : Type) (f : A -> B) (p : B -> bool) (l : list A),
filter p (map f l) = map f (filter (fun x : A => p (f x)) l).
Lemma filter_join :
forall (A : Type) (p : A -> bool) (lla : list (list A)),
filter p (join lla) = join (map (filter p) lla).
Lemma filter_replicate :
forall (A : Type) (p : A -> bool) (n : nat) (x : A),
filter p (replicate n x) =
if p x then replicate n x else [].
Lemma filter_iterate :
forall (A : Type) (p : A -> bool) (f : A -> A) (n : nat) (x : A),
(forall x : A, p (f x) = p x) ->
filter p (iterate f n x) =
if p x then iterate f n x else [].
Lemma head_filter :
forall (A : Type) (p : A -> bool) (l : list A),
head (filter p l) = find p l.
Lemma last_filter :
forall (A : Type) (p : A -> bool) (l : list A),
last (filter p l) = findLast p l.
Lemma filter_nth :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat) (x : A),
nth n l = Some x -> p x = true ->
exists m : nat, m <= n /\ nth m (filter p l) = Some x.
Lemma splitAt_filter :
forall (A : Type) (p : A -> bool) (l l1 l2 : list A) (x : A) (n : nat),
splitAt n (filter p l) = Some (l1, x, l2) ->
exists m : nat,
match splitAt m l with
| None => False
| Some (l1', y, l2') =>
x = y /\ l1 = filter p l1' /\ l2 = filter p l2'
end.
Lemma filter_insert :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat) (x : A),
filter p (insert l n x) =
filter p (take n l) ++
(if p x then [x] else []) ++
filter p (drop n l).
Lemma replace_filter :
forall (A : Type) (p : A -> bool) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
filter p l' =
filter p (take n l) ++ filter p [x] ++ filter p (drop (S n) l).
Lemma remove_filter :
forall (A : Type) (p : A -> bool) (l l' : list A) (x : A) (n : nat),
remove n (filter p l) = Some (x, l') ->
exists m : nat,
match remove m l with
| None => False
| Some (y, l'') => x = y /\ l' = filter p l''
end.
Lemma filter_idempotent :
forall (A : Type) (f : A -> bool) (l : list A),
filter f (filter f l) = filter f l.
Lemma filter_comm :
forall (A : Type) (f g : A -> bool) (l : list A),
filter f (filter g l) = filter g (filter f l).
Lemma zip_not_filter :
exists (A B : Type) (pa : A -> bool) (pb : B -> bool)
(la : list A) (lb : list B),
zip (filter pa la) (filter pb lb) <>
filter (fun x => andb (pa (fst x)) (pb (snd x))) (zip la lb).
Lemma any_filter :
forall (A : Type) (p : A -> bool) (l : list A),
any p l = negb (isEmpty (filter p l)).
Lemma all_filter :
forall (A : Type) (p : A -> bool) (l : list A),
all p (filter p l) = true.
Lemma all_filter' :
forall (A : Type) (p : A -> bool) (l : list A),
all p l = isEmpty (filter (fun x : A => negb (p x)) l).
Lemma filter_all :
forall (A : Type) (p : A -> bool) (l : list A),
all p l = true -> filter p l = l.
Lemma removeFirst_filter :
forall (A : Type) (p : A -> bool) (l : list A),
removeFirst p (filter p l) =
match filter p l with
| [] => None
| h :: t => Some (h, t)
end.
Lemma removeFirst_negb_filter :
forall (A : Type) (p : A -> bool) (l : list A),
removeFirst (fun x : A => negb (p x)) (filter p l) = None.
Lemma findIndex_filter :
forall (A : Type) (p : A -> bool) (l : list A),
findIndex p (filter p l) = None \/
findIndex p (filter p l) = Some 0.
Lemma count_filter :
forall (A : Type) (p : A -> bool) (l : list A),
count p (filter p l) = length (filter p l).
Lemma count_filter' :
forall (A : Type) (p : A -> bool) (l : list A),
count p (filter p l) = count p l.
partition
Zdefiniuj funkcję
partition, która dzieli listę
l na listy
elementów spełniających i niespełniających pewnego warunku
boolowskiego.
Przykład:
partition even [1; 2; 3; 4] =
([2; 4], [1; 3])
Lemma partition_spec :
forall (A : Type) (p : A -> bool) (l : list A),
partition p l = (filter p l, filter (fun x => negb (p x)) l).
Lemma partition_true :
forall (A : Type) (p : A -> bool) (l : list A),
partition (fun _ => true) l = (l, []).
Lemma partition_false :
forall (A : Type) (p : A -> bool) (l : list A),
partition (fun _ => false) l = ([], l).
Lemma partition_cons_true :
forall (A : Type) (p : A -> bool) (h : A) (t l1 l2 : list A),
p h = true -> partition p t = (l1, l2) ->
partition p (h :: t) = (h :: l1, l2).
Lemma partition_cons_false :
forall (A : Type) (p : A -> bool) (h : A) (t l1 l2 : list A),
p h = false -> partition p t = (l1, l2) ->
partition p (h :: t) = (l1, h :: l2).
findIndices
Zdefiniuj funkcję
findIndices, która znajduje indeksy wszystkich
elementów listy, które spełniają predykat boolowski
p.
Przykład:
findIndices even [1; 1; 2; 3; 5; 8; 13; 21; 34] =
[2; 5; 8]
Lemma findIndices_false :
forall (A : Type) (l : list A),
findIndices (fun _ => false) l = [].
Lemma findIndices_true :
forall (A : Type) (l : list A),
findIndices (fun _ => true) l =
if isEmpty l then [] else iterate S (length l) 0.
Lemma findIndices_isEmpty_true :
forall (A : Type) (p : A -> bool) (l : list A),
isEmpty l = true -> findIndices p l = [].
Lemma isEmpty_findIndices_not_nil :
forall (A : Type) (p : A -> bool) (l : list A),
findIndices p l <> [] -> isEmpty l = false.
Lemma length_findIndices :
forall (A : Type) (p : A -> bool) (l : list A),
length (findIndices p l) = count p l.
Lemma findIndices_snoc :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
findIndices p (snoc x l) =
if p x
then snoc (length l) (findIndices p l)
else findIndices p l.
Lemma findIndices_app :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
findIndices p (l1 ++ l2) =
findIndices p l1 ++ map (plus (length l1)) (findIndices p l2).
Lemma findIndices_rev_aux :
forall (A : Type) (p : A -> bool) (l : list A),
rev (findIndices p (rev l)) =
map (fun n : nat => length l - S n) (findIndices p l).
Lemma findIndices_rev :
forall (A : Type) (p : A -> bool) (l : list A),
findIndices p (rev l) =
rev (map (fun n : nat => length l - S n) (findIndices p l)).
Lemma rev_findIndices :
forall (A : Type) (p : A -> bool) (l : list A),
rev (findIndices p l) =
map (fun n : nat => length l - S n) (findIndices p (rev l)).
Lemma findIndices_map :
forall (A B : Type) (f : A -> B) (p : B -> bool) (l : list A),
findIndices p (map f l) =
findIndices (fun x : A => p (f x)) l.
Lemma findIndices_replicate :
forall (A : Type) (p : A -> bool) (n : nat) (x : A),
findIndices p (replicate n x) =
match n with
| 0 => []
| S n' => if p x then iterate S n 0 else []
end.
Lemma map_nth_findIndices :
forall (A : Type) (p : A -> bool) (l : list A),
map (fun n : nat => nth n l) (findIndices p l) =
map Some (filter p l).
Lemma head_findIndices :
forall (A : Type) (p : A -> bool) (l : list A),
head (findIndices p l) = findIndex p l.
Lemma tail_findIndices :
forall (A : Type) (p : A -> bool) (l : list A),
tail (findIndices p l) =
match removeFirst p l with
| None => None
| Some (_, l') => Some (map S (findIndices p l'))
end.
Lemma last_findIndices :
forall (A : Type) (p : A -> bool) (l : list A),
last (findIndices p l) =
match findIndex p (rev l) with
| None => None
| Some n => Some (length l - S n)
end.
Lemma init_findIndices :
forall (A : Type) (p : A -> bool) (l : list A),
init (findIndices p l) =
match removeLast p l with
| None => None
| Some (_, l') => Some (findIndices p l')
end.
Lemma findIndices_take :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
findIndices p (take n l) =
take (count p (take n l)) (findIndices p l).
Lemma findIndices_insert :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat) (x : A),
findIndices p (insert l n x) =
findIndices p (take n l) ++
(if p x then [min (length l) n] else []) ++
map (plus (S n)) (findIndices p (drop n l)).
Lemma findIndices_replace :
forall (A : Type) (p : A -> bool) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
findIndices p l' =
findIndices p (take n l) ++
map (plus n) (findIndices p [x]) ++
map (plus (S n)) (findIndices p (drop (S n) l)).
takeWhile i dropWhile
Zdefiniuj funkcje
takeWhile oraz
dropWhile, które, dopóki
funkcja
p zwraca
true, odpowiednio biorą lub usuwają elementy
z listy.
Przykład:
takeWhile even [2; 4; 6; 1; 8; 10; 12] =
[2; 4; 6]
dropWhile even [2; 4; 6; 1; 8; 10; 12] =
[1; 8; 10; 12]
Lemma takeWhile_dropWhile_spec :
forall (A : Type) (p : A -> bool) (l : list A),
takeWhile p l ++ dropWhile p l = l.
Lemma takeWhile_false :
forall (A : Type) (l : list A),
takeWhile (fun _ => false) l = [].
Lemma dropWhile_false :
forall (A : Type) (l : list A),
dropWhile (fun _ => false) l = l.
Lemma takeWhile_andb :
forall (A : Type) (p q : A -> bool) (l : list A),
takeWhile (fun x : A => andb (p x) (q x)) l =
takeWhile p (takeWhile q l).
Lemma isEmpty_takeWhile :
forall (A : Type) (p : A -> bool) (l : list A),
isEmpty (takeWhile p l) =
match l with
| [] => true
| h :: t => negb (p h)
end.
Lemma isEmpty_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A),
isEmpty (dropWhile p l) = all p l.
Lemma takeWhile_snoc_all :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
all p l = true ->
takeWhile p (snoc x l) = if p x then snoc x l else l.
Lemma takeWhile_idempotent :
forall (A : Type) (p : A -> bool) (l : list A),
takeWhile p (takeWhile p l) = takeWhile p l.
Lemma dropWhile_idempotent :
forall (A : Type) (p : A -> bool) (l : list A),
dropWhile p (dropWhile p l) = dropWhile p l.
Lemma takeWhile_replicate :
forall (A : Type) (p : A -> bool) (n : nat) (x : A),
takeWhile p (replicate n x) =
if p x then replicate n x else [].
Lemma takeWhile_iterate :
forall (A : Type) (p : A -> bool) (f : A -> A) (n : nat) (x : A),
(forall x : A, p (f x) = p x) ->
takeWhile p (iterate f n x) =
if p x then iterate f n x else [].
Lemma dropWhile_replicate :
forall (A : Type) (p : A -> bool) (n : nat) (x : A),
dropWhile p (replicate n x) =
if p x then [] else replicate n x.
Lemma dropWhile_iterate :
forall (A : Type) (p : A -> bool) (f : A -> A) (n : nat) (x : A),
(forall x : A, p (f x) = p x) ->
dropWhile p (iterate f n x) =
if p x then [] else iterate f n x.
Lemma any_takeWhile :
forall (A : Type) (p : A -> bool) (l : list A),
any p (takeWhile p l) = negb (isEmpty (takeWhile p l)).
Lemma any_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A),
any (fun x : A => negb (p x)) (dropWhile p l) =
negb (isEmpty (dropWhile p l)).
Lemma any_takeWhile_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A),
any p l = orb (any p (takeWhile p l)) (any p (dropWhile p l)).
Lemma all_takeWhile :
forall (A : Type) (p : A -> bool) (l : list A),
all p (takeWhile p l) = true.
Lemma all_takeWhile' :
forall (A : Type) (p : A -> bool) (l : list A),
all p l = true -> takeWhile p l = l.
Lemma all_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A),
all p (dropWhile p l) = all p l.
Lemma takeWhile_app_all :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
all p l1 = true -> takeWhile p (l1 ++ l2) = l1 ++ takeWhile p l2.
Lemma removeFirst_takeWhile :
forall (A : Type) (p : A -> bool) (l : list A),
removeFirst p (takeWhile p l) =
match takeWhile p l with
| [] => None
| h :: t => Some (h, t)
end.
Lemma removeLast_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A),
removeFirst p (dropWhile (fun x : A => negb (p x)) l) =
match dropWhile (fun x : A => negb (p x)) l with
| [] => None
| h :: t => Some (h, t)
end.
Lemma findIndex_takeWhile :
forall (A : Type) (p : A -> bool) (l : list A) (n m : nat),
findIndex p (takeWhile p l) = Some n ->
findIndex p l = Some n -> n <= m.
Lemma findIndex_spec' :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
findIndex p l = Some n ->
takeWhile (fun x : A => negb (p x)) l = take n l.
Lemma findIndex_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A) (n m : nat),
findIndex p (dropWhile p l) = Some m ->
findIndex p l = Some n -> n <= m.
Lemma count_takeWhile :
forall (A : Type) (p : A -> bool) (l : list A),
count p (takeWhile p l) = length (takeWhile p l).
Lemma count_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A),
count p (dropWhile p l) <= count p l.
Lemma count_takeWhile_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A),
count p (takeWhile p l) + count p (dropWhile p l) = count p l.
span
Zdefiniuj funkcję
span, która dzieli listę
l na listę
b, której
elementy nie spełniają predykatu
p, element
x, który spełnia
p
oraz listę
e zawierającą resztę elementów
l. Jeżeli na liście nie
ma elementu spełniającego
p, funkcja zwraca
None.
Przykład:
span even [1; 1; 2; 3; 5; 8] =
Some ([1; 1], 2, [3; 5; 8])
span even [1; 3; 5] =
None
Lemma isEmpty_span :
forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
span p l = Some (b, x, e) ->
isEmpty l = false.
Lemma length_span :
forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
span p l = Some (b, x, e) -> length b + length e < length l.
Lemma length_span' :
forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
span p l = Some (b, x, e) ->
length b < length l /\
length e < length l.
Lemma span_snoc :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
span p (snoc x l) =
match span p l with
| None => if p x then Some (l, x, []) else None
| Some (b, y, e) => Some (b, y, snoc x e)
end.
Lemma span_app :
forall (A : Type) (p : A -> bool) (l1 l2 : list A),
span p (l1 ++ l2) =
match span p l1, span p l2 with
| Some (b, x, e), _ => Some (b, x, e ++ l2)
| _, Some (b, x, e) => Some (l1 ++ b, x, e)
| _, _ => None
end.
Lemma span_map :
forall (A B : Type) (f : A -> B) (p : B -> bool) (l : list A),
span p (map f l) =
match span (fun x : A => p (f x)) l with
| None => None
| Some (b, x, e) => Some (map f b, f x, map f e)
end.
Lemma span_join :
forall (A : Type) (p : A -> bool) (lla : list (list A)),
span p (join lla) =
match span (any p) lla with
| None => None
| Some (bl, l, el) =>
match span p l with
| None => None
| Some (b, x, e) => Some (join bl ++ b, x, e ++ join el)
end
end.
Lemma span_replicate :
forall (A : Type) (p : A -> bool) (n : nat) (x : A),
span p (replicate n x) =
if andb (1 <=? n) (p x)
then Some ([], x, replicate (n - 1) x)
else None.
Lemma span_any :
forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
span p l = Some (b, x, e) -> any p l = true.
Lemma span_all :
forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
span p l = Some (b, x, e) ->
all p l = andb (beq_nat (length b) 0) (all p e).
Lemma span_find :
forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
span p l = Some (b, x, e) -> find p l = Some x.
Lemma span_removeFirst :
forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
span p l = Some (b, x, e) ->
removeFirst p l = Some (x, b ++ e).
Lemma count_span_l :
forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
span p l = Some (b, x, e) -> count p b = 0.
Lemma count_span_r :
forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
span p l = Some (b, x, e) ->
count p e < length l - length b.
Lemma span_filter :
forall (A : Type) (p : A -> bool) (l : list A),
span p (filter p l) =
match filter p l with
| [] => None
| h :: t => Some ([], h, t)
end.
Lemma filter_span_l :
forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
span p l = Some (b, x, e) -> filter p b = [].
Lemma takeWhile_span :
forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
span p l = Some (b, x, e) ->
takeWhile (fun x : A => negb (p x)) l = b.
Lemma dropWhile_span :
forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
span p l = Some (b, x, e) ->
dropWhile (fun x : A => negb (p x)) l = x :: e.
Związki span i rev
Zdefiniuj funkcję
naps, która działa tak jak
span, tyle że
"od tyłu". Udowodnij twierdzenie
span_rev.
Lemma span_rev_aux :
forall (A : Type) (p : A -> bool) (l : list A),
span p l =
match naps p (rev l) with
| None => None
| Some (b, x, e) => Some (rev e, x, rev b)
end.
Lemma span_rev :
forall (A : Type) (p : A -> bool) (l : list A),
span p (rev l) =
match naps p l with
| None => None
| Some (b, x, e) => Some (rev e, x, rev b)
end.
Sekcja mocno ad hoc
pmap
Zdefiniuj funkcję
pmap, która mapuje funkcję
f : A -> option B
po liście
l, ale odpakowuje wyniki zawinięte w
Some, a wyniki
równe
None usuwa.
Przykład:
pmap (fun n : nat => if even n then None else Some (n + 42)) [1; 2; 3]
=
[43; 45]
Lemma isEmpty_pmap_false :
forall (A B : Type) (f : A -> option B) (l : list A),
isEmpty (pmap f l) = false -> isEmpty l = false.
Lemma isEmpty_pmap_true :
forall (A B : Type) (f : A -> option B) (l : list A),
isEmpty l = true -> isEmpty (pmap f l) = true.
Lemma length_pmap :
forall (A B : Type) (f : A -> option B) (l : list A),
length (pmap f l) <= length l.
Lemma pmap_snoc :
forall (A B : Type) (f : A -> option B) (a : A) (l : list A),
pmap f (snoc a l) =
match f a with
| None => pmap f l
| Some b => snoc b (pmap f l)
end.
Lemma pmap_app :
forall (A B : Type) (f : A -> option B) (l1 l2 : list A),
pmap f (l1 ++ l2) = pmap f l1 ++ pmap f l2.
Lemma pmap_rev :
forall (A B : Type) (f : A -> option B) (l : list A),
pmap f (rev l) = rev (pmap f l).
Lemma pmap_map :
forall (A B C : Type) (f : A -> B) (g : B -> option C) (l : list A),
pmap g (map f l) = pmap (fun x : A => g (f x)) l.
Lemma pmap_join :
forall (A B : Type) (f : A -> option B) (l : list (list A)),
pmap f (join l) = join (map (pmap f) l).
Lemma pmap_bind :
forall (A B C : Type) (f : A -> list B) (g : B -> option C) (l : list A),
pmap g (bind f l) = bind (fun x : A => pmap g (f x)) l.
Lemma pmap_replicate :
forall (A B : Type) (f : A -> option B) (n : nat) (x : A),
pmap f (replicate n x) =
match f x with
| None => []
| Some y => replicate n y
end.
Definition isSome {A : Type} (x : option A) : bool :=
match x with
| None => false
| _ => true
end.
Lemma head_pmap :
forall (A B : Type) (f : A -> option B) (l : list A),
head (pmap f l) =
match find isSome (map f l) with
| None => None
| Some x => x
end.
Lemma pmap_zip :
exists
(A B C : Type)
(fa : A -> option C) (fb : B -> option C)
(la : list A) (lb : list B),
pmap
(fun '(a, b) =>
match fa a, fb b with
| Some a', Some b' => Some (a', b')
| _, _ => None
end)
(zip la lb) <>
zip (pmap fa la) (pmap fb lb).
Lemma any_pmap :
forall (A B : Type) (f : A -> option B) (p : B -> bool) (l : list A),
any p (pmap f l) =
any
(fun x : A =>
match f x with
| Some b => p b
| None => false
end)
l.
Lemma all_pmap :
forall (A B : Type) (f : A -> option B) (p : B -> bool) (l : list A),
all p (pmap f l) =
all
(fun x : A =>
match f x with
| Some b => p b
| None => true
end)
l.
Lemma find_pmap :
forall (A B : Type) (f : A -> option B) (p : B -> bool) (l : list A),
find p (pmap f l) =
let oa :=
find (fun x : A => match f x with Some b => p b | _ => false end) l
in
match oa with
| Some a => f a
| None => None
end.
Lemma findLast_pmap :
forall (A B : Type) (f : A -> option B) (p : B -> bool) (l : list A),
findLast p (pmap f l) =
let oa :=
findLast
(fun x : A => match f x with Some b => p b | _ => false end) l
in
match oa with
| Some a => f a
| None => None
end.
Lemma count_pmap :
forall (A B : Type) (f : A -> option B) (p : B -> bool) (l : list A),
count p (pmap f l) =
count
(fun x : A =>
match f x with
| Some b => p b
| None => false
end)
l.
Definition aux {A B : Type} (p : B -> bool) (f : A -> option B)
(dflt : bool) (x : A) : bool :=
match f x with
| Some b => p b
| None => dflt
end.
Lemma pmap_filter :
forall (A B : Type) (p : B -> bool) (f : A -> option B) (l : list A),
filter p (pmap f l) =
pmap f (filter (aux p f false) l).
Lemma pmap_takeWhile :
forall (A B : Type) (p : B -> bool) (f : A -> option B) (l : list A),
takeWhile p (pmap f l) =
pmap f
(takeWhile
(fun x : A => match f x with | Some b => p b | _ => true end)
l).
Lemma pmap_dropWhile :
forall (A B : Type) (p : B -> bool) (f : A -> option B) (l : list A),
dropWhile p (pmap f l) =
pmap f
(dropWhile
(fun x : A => match f x with | Some b => p b | _ => true end)
l).
Lemma pmap_span :
forall (A B : Type) (f : A -> option B) (p : B -> bool) (l : list A),
match
span
(fun x : A => match f x with None => false | Some b => p b end)
l
with
| None => True
| Some (b, x, e) =>
exists y : B, f x = Some y /\
span p (pmap f l) = Some (pmap f b, y, pmap f e)
end.
Lemma pmap_nth_findIndices :
forall (A : Type) (p : A -> bool) (l : list A),
pmap (fun n : nat => nth n l) (findIndices p l) =
filter p l.
Bardziej skomplikowane funkcje
intersperse
Zdefiniuj funkcję
intersperse, który wstawia element
x : A między
każde dwa elementy z listy
l : list A. Zastanów się dobrze nad
przypadkami bazowymi.
Przykład:
intersperse 42 [1; 2; 3] =
[1; 42; 2; 42; 3]
Lemma isEmpty_intersperse :
forall (A : Type) (x : A) (l : list A),
isEmpty (intersperse x l) = isEmpty l.
Lemma length_intersperse :
forall (A : Type) (x : A) (l : list A),
length (intersperse x l) = 2 * length l - 1.
Lemma intersperse_snoc :
forall (A : Type) (x y : A) (l : list A),
intersperse x (snoc y l) =
if isEmpty l then [y] else snoc y (snoc x (intersperse x l)).
Lemma intersperse_app :
forall (A : Type) (x : A) (l1 l2 : list A),
intersperse x (l1 ++ l2) =
match l1, l2 with
| [], _ => intersperse x l2
| _, [] => intersperse x l1
| h1 :: t1, h2 :: t2 =>
intersperse x l1 ++ x :: intersperse x l2
end.
Lemma intersperse_app_cons :
forall (A : Type) (x : A) (l1 l2 : list A),
l1 <> [] -> l2 <> [] ->
intersperse x (l1 ++ l2) = intersperse x l1 ++ x :: intersperse x l2.
Lemma intersperse_rev :
forall (A : Type) (x : A) (l : list A),
intersperse x (rev l) = rev (intersperse x l).
Lemma intersperse_map :
forall (A B : Type) (f : A -> B) (l : list A) (a : A) (b : B),
f a = b -> intersperse b (map f l) = map f (intersperse a l).
Lemma head_intersperse :
forall (A : Type) (x : A) (l : list A),
head (intersperse x l) = head l.
Lemma last_intersperse :
forall (A : Type) (x : A) (l : list A),
last (intersperse x l) = last l.
Lemma tail_intersperse :
forall (A : Type) (x : A) (l : list A),
tail (intersperse x l) =
match tail l with
| None => None
| Some [] => Some []
| Some (h :: t) => tail (intersperse x l)
end.
Lemma nth_intersperse_even :
forall (A : Type) (x : A) (l : list A) (n : nat),
n < length l ->
nth (2 * n) (intersperse x l) = nth n l.
Lemma nth_intersperse_odd :
forall (A : Type) (x : A) (l : list A) (n : nat),
0 < n -> n < length l ->
nth (2 * n - 1) (intersperse x l) = Some x.
Lemma intersperse_take :
forall (A : Type) (x : A) (l : list A) (n : nat),
intersperse x (take n l) =
take (2 * n - 1) (intersperse x l).
Lemma any_intersperse :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
any p (intersperse x l) =
orb (any p l) (andb (2 <=? length l) (p x)).
Lemma all_intersperse :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
all p (intersperse x l) =
all p l && ((length l <=? 1) || p x).
Lemma findIndex_intersperse :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
findIndex p (intersperse x l) =
if p x
then
match l with
| [] => None
| [h] => if p h then Some 0 else None
| h :: t => if p h then Some 0 else Some 1
end
else
match findIndex p l with
| None => None
| Some n => Some (2 * n)
end.
Lemma count_intersperse :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
count p (intersperse x l) =
count p l + if p x then length l - 1 else 0.
Lemma filter_intersperse_false :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
p x = false -> filter p (intersperse x l) = filter p l.
Lemma pmap_intersperse :
forall (A B : Type) (f : A -> option B) (x : A) (l : list A),
f x = None -> pmap f (intersperse x l) = pmap f l.
Proste predykaty
elem
Zdefiniuj induktywny predykat
elem.
elem x l jest spełniony, gdy
x jest elementem listy
l.
Lemma elem_not_nil :
forall (A : Type) (x : A), ~ elem x [].
Lemma elem_not_cons :
forall (A : Type) (x h : A) (t : list A),
~ elem x (h :: t) -> x <> h /\ ~ elem x t.
Lemma elem_cons' :
forall (A : Type) (x h : A) (t : list A),
elem x (h :: t) <-> x = h \/ elem x t.
Lemma elem_snoc :
forall (A : Type) (x y : A) (l : list A),
elem x (snoc y l) <-> elem x l \/ x = y.
Lemma elem_app_l :
forall (A : Type) (x : A) (l1 l2 : list A),
elem x l1 -> elem x (l1 ++ l2).
Lemma elem_app_r :
forall (A : Type) (x : A) (l1 l2 : list A),
elem x l2 -> elem x (l1 ++ l2).
Lemma elem_or_app :
forall (A : Type) (x : A) (l1 l2 : list A),
elem x l1 \/ elem x l2 -> elem x (l1 ++ l2).
Lemma elem_app_or :
forall (A : Type) (x : A) (l1 l2 : list A),
elem x (l1 ++ l2) -> elem x l1 \/ elem x l2.
Lemma elem_app :
forall (A : Type) (x : A) (l1 l2 : list A),
elem x (l1 ++ l2) <-> elem x l1 \/ elem x l2.
Lemma elem_spec :
forall (A : Type) (x : A) (l : list A),
elem x l <-> exists l1 l2 : list A, l = l1 ++ x :: l2.
Lemma elem_map :
forall (A B : Type) (f : A -> B) (l : list A) (x : A),
elem x l -> elem (f x) (map f l).
Lemma elem_map_conv :
forall (A B : Type) (f : A -> B) (l : list A) (y : B),
elem y (map f l) <-> exists x : A, f x = y /\ elem x l.
Lemma elem_map_conv' :
forall (A B : Type) (f : A -> B) (l : list A) (x : A),
(forall x y : A, f x = f y -> x = y) ->
elem (f x) (map f l) -> elem x l.
Lemma map_ext_elem :
forall (A B : Type) (f g : A -> B) (l : list A),
(forall x : A, elem x l -> f x = g x) -> map f l = map g l.
Lemma elem_join :
forall (A : Type) (x : A) (ll : list (list A)),
elem x (join ll) <-> exists l : list A, elem x l /\ elem l ll.
Lemma elem_replicate :
forall (A : Type) (n : nat) (x y : A),
elem y (replicate n x) <-> n <> 0 /\ x = y.
Lemma nth_elem :
forall (A : Type) (l : list A) (n : nat),
n < length l -> exists x : A, nth n l = Some x /\ elem x l.
Lemma iff_elem_nth :
forall (A : Type) (x : A) (l : list A),
elem x l <-> exists n : nat, nth n l = Some x.
Lemma elem_rev_aux :
forall (A : Type) (x : A) (l : list A),
elem x l -> elem x (rev l).
Lemma elem_rev :
forall (A : Type) (x : A) (l : list A),
elem x (rev l) <-> elem x l.
Lemma elem_remove_nth :
forall (A : Type) (x : A) (l : list A) (n : nat),
elem x l -> nth n l <> Some x ->
match remove n l with
| None => True
| Some (_, l') => elem x l'
end.
Lemma elem_take :
forall (A : Type) (l : list A) (n : nat) (x : A),
elem x (take n l) -> elem x l.
Lemma elem_drop :
forall (A : Type) (l : list A) (n : nat) (x : A),
elem x (drop n l) -> elem x l.
Lemma elem_splitAt' :
forall (A : Type) (l l1 l2 : list A) (n : nat) (x y : A),
splitAt n l = Some (l1, y, l2) ->
elem x l <-> x = y \/ elem x l1 \/ elem x l2.
Lemma elem_insert :
forall (A : Type) (l : list A) (n : nat) (x y : A),
elem y (insert l n x) <-> x = y \/ elem y l.
Lemma elem_replace :
forall (A : Type) (l l' : list A) (n : nat) (x y : A),
replace l n x = Some l' ->
elem y l' <-> elem y (take n l) \/ x = y \/ elem y (drop (S n) l).
Lemma elem_filter :
forall (A : Type) (p : A -> bool) (l : list A) (x : A),
elem x (filter p l) <-> p x = true /\ elem x l.
Lemma elem_filter_conv :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
elem x l <->
elem x (filter p l) /\ p x = true \/
elem x (filter (fun x : A => negb (p x)) l) /\ p x = false.
Lemma elem_partition :
forall (A : Type) (p : A -> bool) (x : A) (l l1 l2 : list A),
partition p l = (l1, l2) ->
elem x l <->
(elem x l1 /\ p x = true) \/ (elem x l2 /\ p x = false).
Lemma elem_takeWhile :
forall (A : Type) (p : A -> bool) (l : list A) (x : A),
elem x (takeWhile p l) -> elem x l /\ p x = true.
Lemma elem_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A) (x : A),
elem x (dropWhile p l) -> elem x l.
Lemma elem_takeWhile_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A) (x : A),
elem x l <-> elem x (takeWhile p l) \/ elem x (dropWhile p l).
Lemma elem_dropWhile_conv :
forall (A : Type) (p : A -> bool) (l : list A) (x : A),
elem x l -> ~ elem x (dropWhile p l) -> p x = true.
Lemma span_spec' :
forall (A : Type) (p : A -> bool) (l : list A),
match span p l with
| None => forall x : A, elem x l -> p x = false
| Some (b, x, e) =>
b = takeWhile (fun x : A => negb (p x)) l /\
Some x = find p l /\
x :: e = dropWhile (fun x : A => negb (p x)) l /\
Some (x, b ++ e) = removeFirst p l
end.
Lemma elem_span_None :
forall (A : Type) (p : A -> bool) (l : list A),
span p l = None -> forall x : A, elem x l -> p x = false.
Lemma elem_span_Some :
forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
span p l = Some (b, x, e) ->
forall y : A, elem y l <-> elem y b \/ y = x \/ elem y e.
Lemma elem_span :
forall (A : Type) (p : A -> bool) (l : list A),
match span p l with
| None => forall x : A, elem x l -> p x = false
| Some (b, x, e) =>
forall y : A, elem y l <-> elem y b \/ y = x \/ elem y e
end.
Lemma elem_removeFirst_None :
forall (A : Type) (p : A -> bool) (l : list A),
removeFirst p l = None ->
forall x : A, elem x l -> p x = false.
Lemma elem_zip :
forall (A B : Type) (a : A) (b : B) (la : list A) (lb : list B),
elem (a, b) (zip la lb) -> elem a la /\ elem b lb.
Lemma zip_not_elem :
exists (A B : Type) (a : A) (b : B) (la : list A) (lb : list B),
elem a la /\ elem b lb /\ ~ elem (a, b) (zip la lb).
Lemma elem_findIndices :
forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
elem n (findIndices p l) ->
exists x : A, nth n l = Some x /\ p x = true.
Lemma isEmpty_bind :
forall (A B : Type) (f : A -> list B) (l : list A),
isEmpty (bind f l) = true <->
l = [] \/ l <> [] /\ forall x : A, elem x l -> f x = [].
Lemma elem_pmap :
forall (A B : Type) (f : A -> option B) (l : list A) (a : A) (b : B),
f a = Some b -> elem a l -> elem b (pmap f l).
Lemma elem_pmap' :
forall (A B : Type) (f : A -> option B) (l : list A) (b : B),
(exists a : A, elem a l /\ f a = Some b) -> elem b (pmap f l).
Lemma elem_pmap_conv :
forall (A B : Type) (f : A -> option B) (l : list A) (b : B),
elem b (pmap f l) -> exists a : A, elem a l /\ f a = Some b.
Lemma elem_intersperse :
forall (A : Type) (x y : A) (l : list A),
elem x (intersperse y l) <-> elem x l \/ (x = y /\ 2 <= length l).
In
Gratuluję, udało ci się zdefiniować predykat
elem i dowieść wszystkich
jego właściwości. To jednak nie koniec zabawy, gdyż predykaty możemy
definiować nie tylko przez indukcję, ale także przez rekursję. Być może
taki sposób definiowania jest nawet lepszy? Przyjrzyjmy się poniższej
definicji — tak właśnie "bycie elementem" jest zdefiniowane w bibliotece
standardowej.
Fixpoint In {A : Type} (x : A) (l : list A) : Prop :=
match l with
| [] => False
| h :: t => x = h \/ In x t
end.
Powyższa definicja jest bardzo podobna do tej induktywnej.
In x
dla listy pustej redukuje się do
False, co oznacza, że w pustej
liście nic nie ma, zaś dla listy mającej głowę i ogon redukuje się do
zdania "
x jest głową lub jest elementem ogona".
Definicja taka ma swoje wady i zalety. Największą moim zdaniem wadą jest
to, że nie możemy robić indukcji po dowodzie, gdyż dowód faktu
In x l
nie jest induktywny. Największą zaletą zaś jest fakt, że nie możemy robić
indukcji po dowodzie — im mniej potencjalnych rzeczy, po których można
robić indukcję, tym mniej zastanawiania się. Przekonajmy się zatem na
własnej skórze, która definicja jest "lepsza".
Lemma In_elem :
forall (A : Type) (x : A) (l : list A),
In x l <-> elem x l.
Lemma In_not_nil :
forall (A : Type) (x : A), ~ In x [].
Lemma In_not_cons :
forall (A : Type) (x h : A) (t : list A),
~ In x (h :: t) -> x <> h /\ ~ In x t.
Lemma In_cons :
forall (A : Type) (x h : A) (t : list A),
In x (h :: t) <-> x = h \/ In x t.
Lemma In_snoc :
forall (A : Type) (x y : A) (l : list A),
In x (snoc y l) <-> In x l \/ x = y.
Lemma In_app_l :
forall (A : Type) (x : A) (l1 l2 : list A),
In x l1 -> In x (l1 ++ l2).
Lemma In_app_r :
forall (A : Type) (x : A) (l1 l2 : list A),
In x l2 -> In x (l1 ++ l2).
Lemma In_or_app :
forall (A : Type) (x : A) (l1 l2 : list A),
In x l1 \/ In x l2 -> In x (l1 ++ l2).
Lemma In_app_or :
forall (A : Type) (x : A) (l1 l2 : list A),
In x (l1 ++ l2) -> In x l1 \/ In x l2.
Lemma In_app :
forall (A : Type) (x : A) (l1 l2 : list A),
In x (l1 ++ l2) <-> In x l1 \/ In x l2.
Lemma In_spec :
forall (A : Type) (x : A) (l : list A),
In x l <-> exists l1 l2 : list A, l = l1 ++ x :: l2.
Lemma In_map :
forall (A B : Type) (f : A -> B) (l : list A) (x : A),
In x l -> In (f x) (map f l).
Lemma In_map_conv :
forall (A B : Type) (f : A -> B) (l : list A) (y : B),
In y (map f l) <-> exists x : A, f x = y /\ In x l.
Lemma In_map_conv' :
forall (A B : Type) (f : A -> B) (l : list A) (x : A),
(forall x y : A, f x = f y -> x = y) ->
In (f x) (map f l) -> In x l.
Lemma map_ext_In :
forall (A B : Type) (f g : A -> B) (l : list A),
(forall x : A, In x l -> f x = g x) -> map f l = map g l.
Lemma In_join :
forall (A : Type) (x : A) (ll : list (list A)),
In x (join ll) <->
exists l : list A, In x l /\ In l ll.
Lemma In_replicate :
forall (A : Type) (n : nat) (x y : A),
In y (replicate n x) <-> n <> 0 /\ x = y.
Lemma In_iterate :
forall (A : Type) (f : A -> A) (n : nat) (x y : A),
In y (iterate f n x) <-> exists k : nat, k < n /\ y = iter f k x.
Lemma nth_In :
forall (A : Type) (l : list A) (n : nat),
n < length l -> exists x : A, nth n l = Some x /\ In x l.
Lemma iff_In_nth :
forall (A : Type) (x : A) (l : list A),
In x l <-> exists n : nat, nth n l = Some x.
Lemma In_rev_aux :
forall (A : Type) (x : A) (l : list A),
In x l -> In x (rev l).
Lemma In_rev :
forall (A : Type) (x : A) (l : list A),
In x (rev l) <-> In x l.
Lemma In_take :
forall (A : Type) (l : list A) (n : nat) (x : A),
In x (take n l) -> In x l.
Lemma In_drop :
forall (A : Type) (l : list A) (n : nat) (x : A),
In x (drop n l) -> In x l.
Lemma In_splitAt :
forall (A : Type) (l b e : list A) (n : nat) (x y : A),
splitAt n l = Some (b, x, e) ->
In y l <-> In y b \/ x = y \/ In y e.
Lemma In_insert :
forall (A : Type) (l : list A) (n : nat) (x y : A),
In y (insert l n x) <-> x = y \/ In y l.
Lemma In_replace :
forall (A : Type) (l l' : list A) (n : nat) (x y : A),
replace l n x = Some l' ->
In y l' <-> In y (take n l) \/ x = y \/ In y (drop (S n) l).
Lemma In_filter :
forall (A : Type) (p : A -> bool) (l : list A) (x : A),
In x (filter p l) <-> p x = true /\ In x l.
Lemma In_filter_conv :
forall (A : Type) (p : A -> bool) (x : A) (l : list A),
In x l <->
In x (filter p l) /\ p x = true \/
In x (filter (fun x : A => negb (p x)) l) /\ p x = false.
Lemma In_partition :
forall (A : Type) (p : A -> bool) (x : A) (l l1 l2 : list A),
partition p l = (l1, l2) ->
In x l <->
(In x l1 /\ p x = true) \/ (In x l2 /\ p x = false).
Lemma In_takeWhile :
forall (A : Type) (p : A -> bool) (l : list A) (x : A),
In x (takeWhile p l) -> In x l /\ p x = true.
Lemma In_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A) (x : A),
In x (dropWhile p l) -> In x l.
Lemma In_takeWhile_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A) (x : A),
In x l ->
In x (takeWhile p l) \/
In x (dropWhile p l).
Lemma In_dropWhile_conv :
forall (A : Type) (p : A -> bool) (l : list A) (x : A),
In x l -> ~ In x (dropWhile p l) -> p x = true.
Lemma In_span :
forall (A : Type) (p : A -> bool) (x y : A) (l b e : list A),
span p l = Some (b, x, e) ->
In y l <-> In y b \/ y = x \/ In y e.
Lemma In_zip :
forall (A B : Type) (a : A) (b : B) (la : list A) (lb : list B),
In (a, b) (zip la lb) -> In a la /\ In b lb.
Lemma zip_not_In :
exists (A B : Type) (a : A) (b : B) (la : list A) (lb : list B),
In a la /\ In b lb /\ ~ In (a, b) (zip la lb).
Lemma In_intersperse :
forall (A : Type) (x y : A) (l : list A),
In x (intersperse y l) <->
In x l \/ (x = y /\ 2 <= length l).
NoDup
Zdefiniuj induktywny predykat
NoDup. Zdanie
NoDup l jest prawdziwe,
gdy w
l nie ma powtarzających się elementów. Udowodnij, że zdefiniowany
przez ciebie predykat posiada pożądane właściwości.
Lemma NoDup_singl :
forall (A : Type) (x : A), NoDup [x].
Lemma NoDup_cons_inv :
forall (A : Type) (h : A) (t : list A),
NoDup (h :: t) -> NoDup t.
Lemma NoDup_length :
forall (A : Type) (l : list A),
~ NoDup l -> 2 <= length l.
Lemma NoDup_snoc :
forall (A : Type) (x : A) (l : list A),
NoDup (snoc x l) <-> NoDup l /\ ~ elem x l.
Lemma NoDup_app :
forall (A : Type) (l1 l2 : list A),
NoDup (l1 ++ l2) <->
NoDup l1 /\
NoDup l2 /\
(forall x : A, elem x l1 -> ~ elem x l2) /\
(forall x : A, elem x l2 -> ~ elem x l1).
Lemma NoDup_app_comm :
forall (A : Type) (l1 l2 : list A),
NoDup (l1 ++ l2) <-> NoDup (l2 ++ l1).
Lemma NoDup_rev :
forall (A : Type) (l : list A),
NoDup (rev l) <-> NoDup l.
Lemma NoDup_map :
forall (A B : Type) (f : A -> B) (l : list A),
NoDup (map f l) -> NoDup l.
Lemma NoDup_map_inj :
forall (A B : Type) (f : A -> B) (l : list A),
(forall x y : A, f x = f y -> x = y) ->
NoDup l -> NoDup (map f l).
Lemma NoDup_replicate :
forall (A : Type) (n : nat) (x : A),
NoDup (replicate n x) <-> n = 0 \/ n = 1.
Lemma NoDup_take :
forall (A : Type) (l : list A) (n : nat),
NoDup l -> NoDup (take n l).
Lemma NoDup_drop :
forall (A : Type) (l : list A) (n : nat),
NoDup l -> NoDup (drop n l).
Lemma NoDup_filter :
forall (A : Type) (p : A -> bool) (l : list A),
NoDup l -> NoDup (filter p l).
Lemma NoDup_partition :
forall (A : Type) (p : A -> bool) (l l1 l2 : list A),
partition p l = (l1, l2) -> NoDup l <-> NoDup l1 /\ NoDup l2.
Lemma NoDup_takeWhile :
forall (A : Type) (p : A -> bool) (l : list A),
NoDup l -> NoDup (takeWhile p l).
Lemma NoDup_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A),
NoDup l -> NoDup (dropWhile p l).
Lemma NoDup_zip :
forall (A B : Type) (la : list A) (lb : list B),
NoDup la /\ NoDup lb -> NoDup (zip la lb).
Lemma NoDup_zip_conv :
exists (A B : Type) (la : list A) (lb : list B),
NoDup (zip la lb) /\ ~ NoDup la /\ ~ NoDup lb.
Lemma NoDup_pmap :
exists (A B : Type) (f : A -> option B) (l : list A),
NoDup l /\ ~ NoDup (pmap f l).
Lemma NoDup_intersperse :
forall (A : Type) (x : A) (l : list A),
NoDup (intersperse x l) -> length l <= 2.
Lemma NoDup_spec :
forall (A : Type) (l : list A),
~ NoDup l <->
exists (x : A) (l1 l2 l3 : list A),
l = l1 ++ x :: l2 ++ x :: l3.
Dup
Powodem problemów z predykatem
NoDup jest fakt, że jest on w pewnym
sensie niekonstruktywny. Wynika to wprost z jego definicji:
NoDup l
zachodzi, gdy w
l nie ma duplikatów. Parafrazując:
NoDup l zachodzi,
gdy
nieprawda, że w
l są duplikaty.
Jak widać, w naszej definicji implicite występuje negacja. Wobec tego
jeżeli spróbujemy za pomocą
NoDup wyrazić zdanie "na liście
l są
duplikaty", to tak naprawdę dostaniemy zdanie "nieprawda, że nieprawda,
że
l ma duplikaty".
Dostaliśmy więc po głowie nagłym atakiem podwójnej negacji. Nie ma się
co dziwić w takiej sytuacji, że nasza "negatywna" definicja predykatu
NoDup jest nazbyt klasyczna. Możemy jednak uratować sytuację, jeżeli
zdefiniujemy predykat
Dup i zanegujemy go.
Zdefiniuj predykat
Dup, który jest spełniony, gdy na liście występują
duplikaty.
Lemma Dup_nil :
forall A : Type, ~ Dup (@nil A).
Lemma Dup_cons :
forall (A : Type) (x : A) (l : list A),
Dup (x :: l) <-> elem x l \/ Dup l.
Lemma Dup_singl :
forall (A : Type) (x : A), ~ Dup [x].
Lemma Dup_cons_inv :
forall (A : Type) (h : A) (t : list A),
~ Dup (h :: t) -> ~ elem h t /\ ~ Dup t.
Lemma Dup_spec :
forall (A : Type) (l : list A),
Dup l <->
exists (x : A) (l1 l2 l3 : list A),
l = l1 ++ x :: l2 ++ x :: l3.
Lemma Dup_NoDup :
forall (A : Type) (l : list A),
~ Dup l <-> NoDup l.
Lemma Dup_length :
forall (A : Type) (l : list A),
Dup l -> 2 <= length l.
Lemma Dup_snoc :
forall (A : Type) (x : A) (l : list A),
Dup (snoc x l) <-> Dup l \/ elem x l.
Lemma Dup_app_l :
forall (A : Type) (l1 l2 : list A),
Dup l1 -> Dup (l1 ++ l2).
Lemma Dup_app_r :
forall (A : Type) (l1 l2 : list A),
Dup l2 -> Dup (l1 ++ l2).
Lemma Dup_app_both :
forall (A : Type) (x : A) (l1 l2 : list A),
elem x l1 -> elem x l2 -> Dup (l1 ++ l2).
Lemma Dup_app :
forall (A : Type) (l1 l2 : list A),
Dup (l1 ++ l2) <->
Dup l1 \/ Dup l2 \/ exists x : A, elem x l1 /\ elem x l2.
Lemma Dup_rev :
forall (A : Type) (l : list A),
Dup (rev l) <-> Dup l.
Lemma Dup_map :
forall (A B : Type) (f : A -> B) (l : list A),
Dup l -> Dup (map f l).
Lemma Dup_map_conv :
forall (A B : Type) (f : A -> B) (l : list A),
(forall x y : A, f x = f y -> x = y) ->
Dup (map f l) -> Dup l.
Lemma Dup_join :
forall (A : Type) (ll : list (list A)),
Dup (join ll) ->
(exists l : list A, elem l ll /\ Dup l) \/
(exists (x : A) (l1 l2 : list A),
elem x l1 /\ elem x l2 /\ elem l1 ll /\ elem l2 ll).
Lemma Dup_replicate :
forall (A : Type) (n : nat) (x : A),
Dup (replicate n x) -> 2 <= n.
Lemma Dup_nth :
forall (A : Type) (l : list A),
Dup l <->
exists (x : A) (n1 n2 : nat),
n1 < n2 /\ nth n1 l = Some x /\ nth n2 l = Some x.
Lemma Dup_take :
forall (A : Type) (l : list A) (n : nat),
Dup (take n l) -> Dup l.
Lemma Dup_drop :
forall (A : Type) (l : list A) (n : nat),
Dup (drop n l) -> Dup l.
Lemma Dup_filter :
forall (A : Type) (p : A -> bool) (l : list A),
Dup (filter p l) -> Dup l.
Lemma Dup_filter_conv :
forall (A : Type) (p : A -> bool) (l : list A),
Dup l ->
Dup (filter p l) \/
Dup (filter (fun x : A => negb (p x)) l).
Lemma Dup_partition :
forall (A : Type) (p : A -> bool) (l l1 l2 : list A),
partition p l = (l1, l2) -> Dup l <-> Dup l1 \/ Dup l2.
Lemma Dup_takeWhile :
forall (A : Type) (p : A -> bool) (l : list A),
Dup (takeWhile p l) -> Dup l.
Lemma Dup_dropWhile :
forall (A : Type) (p : A -> bool) (l : list A),
Dup (dropWhile p l) -> Dup l.
Lemma Dup_takeWhile_dropWhile_conv :
forall (A : Type) (p : A -> bool) (l : list A),
Dup l ->
Dup (takeWhile p l) \/
Dup (dropWhile p l) \/
exists x : A,
elem x (takeWhile p l) /\ elem x (dropWhile p l).
Lemma Dup_span :
forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
span p l = Some (b, x, e) ->
Dup l <-> Dup b \/ Dup e \/ elem x b \/ elem x e \/
exists y : A, elem y b /\ elem y e.
Lemma Dup_zip :
forall (A B : Type) (la : list A) (lb : list B),
Dup (zip la lb) -> Dup la /\ Dup lb.
Lemma Dup_zip_conv :
forall (A B : Type) (la : list A) (lb : list B),
~ Dup la /\ ~ Dup lb -> ~ Dup (zip la lb).
Lemma Dup_pmap :
exists (A B : Type) (f : A -> option B) (l : list A),
Dup l /\ ~ Dup (pmap f l).
Lemma Dup_intersperse :
forall (A : Type) (x : A) (l : list A),
Dup (intersperse x l) -> 2 <= length l.
Rep
Jeżeli zastanowimy się chwilę, to dojdziemy do wniosku, że
Dup l
znaczy "istnieje x, który występuje na liście l co najmniej dwa
razy". Widać więc, że
Dup jest jedynie specjalnym przypadkiem
pewngo bardziej ogólnego predykatu
Rep x n dla dowolnego
x oraz
n = 2. Zdefiniuj relację
Rep. Zdanie
Rep x n l zachodzi, gdy
element
x występuje na liście
l co najmnej
n razy.
Zastanów się, czy lepsza będzie definicja induktywna, czy rekurencyjna.
Jeżeli nie masz nic lepszego do roboty, zaimplementuj obie wersje i
porównaj je pod względem łatwości w użyciu.
Lemma Rep_S_cons :
forall (A : Type) (x y : A) (n : nat) (l : list A),
Rep x (S n) (y :: l) <-> (x = y /\ Rep x n l) \/ Rep x (S n) l.
Lemma Rep_cons :
forall (A : Type) (x y : A) (n : nat) (l : list A),
Rep x n (y :: l) <-> (x = y /\ Rep x (n - 1) l) \/ Rep x n l.
Lemma elem_Rep :
forall (A : Type) (x : A) (l : list A),
elem x l -> Rep x 1 l.
Lemma Rep_elem :
forall (A : Type) (x : A) (n : nat) (l : list A),
1 <= n -> Rep x n l -> elem x l.
Lemma Dup_Rep :
forall (A : Type) (l : list A),
Dup l -> exists x : A, Rep x 2 l.
Lemma Rep_Dup :
forall (A : Type) (x : A) (n : nat) (l : list A),
2 <= n -> Rep x n l -> Dup l.
Lemma Rep_le :
forall (A : Type) (x : A) (n m : nat) (l : list A),
n <= m -> Rep x m l -> Rep x n l.
Lemma Rep_S_inv :
forall (A : Type) (x : A) (n : nat) (l : list A),
Rep x (S n) l -> Rep x n l.
Lemma Rep_length :
forall (A : Type) (x : A) (n : nat) (l : list A),
Rep x n l -> n <= length l.
Lemma Rep_S_snoc :
forall (A : Type) (x : A) (n : nat) (l : list A),
Rep x n l -> Rep x (S n) (snoc x l).
Lemma Rep_snoc :
forall (A : Type) (x y : A) (n : nat) (l : list A),
Rep x n l -> Rep x n (snoc y l).
Lemma Rep_app_l :
forall (A : Type) (x : A) (n : nat) (l1 l2 : list A),
Rep x n l1 -> Rep x n (l1 ++ l2).
Lemma Rep_app_r :
forall (A : Type) (x : A) (n : nat) (l1 l2 : list A),
Rep x n l2 -> Rep x n (l1 ++ l2).
Lemma Rep_app :
forall (A : Type) (x : A) (n1 n2 : nat) (l1 l2 : list A),
Rep x n1 l1 -> Rep x n2 l2 -> Rep x (n1 + n2) (l1 ++ l2).
Lemma Rep_app_conv :
forall (A : Type) (x : A) (n : nat) (l1 l2 : list A),
Rep x n (l1 ++ l2) <->
exists n1 n2 : nat,
Rep x n1 l1 /\ Rep x n2 l2 /\ n = n1 + n2.
Lemma Rep_rev :
forall (A : Type) (x : A) (n : nat) (l : list A),
Rep x n (rev l) <-> Rep x n l.
Lemma Rep_map :
forall (A B : Type) (f : A -> B) (x : A) (n : nat) (l : list A),
Rep x n l -> Rep (f x) n (map f l).
Lemma Rep_map_conv :
forall (A B : Type) (f : A -> B) (x : A) (n : nat) (l : list A),
(forall x y : A, f x = f y -> x = y) ->
Rep (f x) n (map f l) -> Rep x n l.
Lemma Rep_replicate :
forall (A : Type) (x : A) (n : nat),
Rep x n (replicate n x).
Lemma Rep_replicate_general :
forall (A : Type) (x : A) (n m : nat),
n <= m -> Rep x n (replicate m x).
Lemma Rep_take :
forall (A : Type) (x : A) (l : list A) (n m : nat),
Rep x n (take m l) -> Rep x n l.
Lemma Rep_drop :
forall (A : Type) (x : A) (l : list A) (n m : nat),
Rep x n (drop m l) -> Rep x n l.
Lemma Rep_filter :
forall (A : Type) (p : A -> bool) (x : A) (n : nat) (l : list A),
Rep x n (filter p l) -> Rep x n l.
Lemma Rep_filter_true :
forall (A : Type) (p : A -> bool) (x : A) (n : nat) (l : list A),
p x = true -> Rep x n l -> Rep x n (filter p l).
Lemma Rep_filter_false :
forall (A : Type) (p : A -> bool) (x : A) (l : list A) (n : nat),
p x = false -> Rep x n (filter p l) -> n = 0.
Lemma Rep_takeWhile :
forall (A : Type) (p : A -> bool) (x : A) (l : list A) (n : nat),
Rep x n (takeWhile p l) -> Rep x n l.
Lemma Rep_dropWhile :
forall (A : Type) (p : A -> bool) (x : A) (l : list A) (n : nat),
Rep x n (dropWhile p l) -> Rep x n l.
Lemma Rep_zip :
forall (A B : Type) (a : A) (b : B) (la : list A) (lb : list B) (n : nat),
Rep (a, b) n (zip la lb) -> Rep a n la /\ Rep b n lb.
Lemma Rep_intersperse :
forall (A : Type) (x y : A) (n : nat) (l : list A),
Rep x n (intersperse y l) <->
Rep x n l \/ x = y /\ Rep x (S n - length l) l.
Exists
Zaimplementuj induktywny predykat
Exists.
Exists P l zachodzi, gdy
lista
l zawiera taki element, który spełnia predykat
P.
Lemma Exists_spec :
forall (A : Type) (P : A -> Prop) (l : list A),
Exists P l <-> exists x : A, elem x l /\ P x.
Lemma Exists_nil :
forall (A : Type) (P : A -> Prop),
Exists P [] <-> False.
Lemma Exists_cons :
forall (A : Type) (P : A -> Prop) (h : A) (t : list A),
Exists P (h :: t) <-> P h \/ Exists P t.
Lemma Exists_length :
forall (A : Type) (P : A -> Prop) (l : list A),
Exists P l -> 1 <= length l.
Lemma Exists_snoc :
forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
Exists P (snoc x l) <-> Exists P l \/ P x.
Lemma Exists_app :
forall (A : Type) (P : A -> Prop) (l1 l2 : list A),
Exists P (l1 ++ l2) <-> Exists P l1 \/ Exists P l2.
Lemma Exists_rev :
forall (A : Type) (P : A -> Prop) (l : list A),
Exists P (rev l) <-> Exists P l.
Lemma Exists_map :
forall (A B : Type) (P : B -> Prop) (f : A -> B) (l : list A),
Exists P (map f l) -> Exists (fun x : A => P (f x)) l.
Lemma Exists_join :
forall (A : Type) (P : A -> Prop) (ll : list (list A)),
Exists P (join ll) <->
Exists (fun l : list A => Exists P l) ll.
Lemma Exists_replicate :
forall (A : Type) (P : A -> Prop) (n : nat) (x : A),
Exists P (replicate n x) <-> 1 <= n /\ P x.
Lemma Exists_nth :
forall (A : Type) (P : A -> Prop) (l : list A),
Exists P l <->
exists (n : nat) (x : A), nth n l = Some x /\ P x.
Lemma Exists_remove :
forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
Exists P l ->
match remove n l with
| None => True
| Some (x, l') => ~ P x -> Exists P l'
end.
Lemma Exists_take :
forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
Exists P (take n l) -> Exists P l.
Lemma Exists_drop :
forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
Exists P (drop n l) -> Exists P l.
Lemma Exists_take_drop :
forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
Exists P l -> Exists P (take n l) \/ Exists P (drop n l).
Lemma Exists_cycle :
forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
Exists P (cycle n l) <-> Exists P l.
Lemma Exists_splitAt :
forall (A : Type) (P : A -> Prop) (l l1 l2 : list A) (n : nat) (x : A),
splitAt n l = Some (l1, x, l2) ->
Exists P l <-> P x \/ Exists P l1 \/ Exists P l2.
Lemma Exists_insert :
forall (A : Type) (P : A -> Prop) (l : list A) (n : nat) (x : A),
Exists P (insert l n x) <-> P x \/ Exists P l.
Lemma Exists_replace :
forall (A : Type) (P : A -> Prop) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
Exists P l' <->
Exists P (take n l) \/ P x \/ Exists P (drop (S n) l).
Lemma Exists_filter :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
Exists P (filter p l) -> Exists P l.
Lemma Exists_filter_conv :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
Exists P l ->
Exists P (filter p l) \/
Exists P (filter (fun x : A => negb (p x)) l).
Lemma Exists_filter_compat :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
(forall x : A, P x <-> p x = false) -> ~ Exists P (filter p l).
Lemma Exists_partition :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l l1 l2 : list A),
partition p l = (l1, l2) ->
Exists P l <-> Exists P l1 \/ Exists P l2.
Lemma Exists_takeWhile :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
Exists P (takeWhile p l) -> Exists P l.
Lemma Exists_takeWhile_compat :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
(forall x : A, P x <-> p x = false) -> ~ Exists P (takeWhile p l).
Lemma Exists_dropWhile :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
Exists P (dropWhile p l) -> Exists P l.
Lemma Exists_takeWhile_dropWhile :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
Exists P l -> Exists P (takeWhile p l) \/ Exists P (dropWhile p l).
Lemma Exists_span :
forall
(A : Type) (P : A -> Prop) (p : A -> bool) (x : A) (l b e : list A),
(forall x : A, P x <-> p x = true) ->
span p l = Some (b, x, e) ->
Exists P l <-> Exists P b \/ P x \/ Exists P e.
Lemma Exists_interesting :
forall (A B : Type) (P : A * B -> Prop) (la : list A) (hb : B) (tb : list B),
Exists (fun a : A => Exists (fun b : B => P (a, b)) tb) la ->
Exists (fun a : A => Exists (fun b : B => P (a, b)) (hb :: tb)) la.
Lemma Exists_zip :
forall (A B : Type) (P : A * B -> Prop) (la : list A) (lb : list B),
Exists P (zip la lb) ->
Exists (fun a : A => Exists (fun b : B => P (a, b)) lb) la.
Lemma Exists_pmap :
forall (A B : Type) (f : A -> option B) (P : B -> Prop) (l : list A),
Exists P (pmap f l) <->
Exists (fun x : A => match f x with | Some b => P b | _ => False end) l.
Lemma Exists_intersperse :
forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
Exists P (intersperse x l) <->
Exists P l \/ (P x /\ 2 <= length l).
Forall
Zaimplementuj induktywny predykat
Forall.
Forall P l jest
spełniony, gdy każdy element listy
l spełnia predykat
P.
Lemma Forall_spec :
forall (A : Type) (P : A -> Prop) (l : list A),
Forall P l <-> forall x : A, elem x l -> P x.
Lemma Forall_nil :
forall (A : Type) (P : A -> Prop),
Forall P [] <-> True.
Lemma Forall_cons :
forall (A : Type) (P : A -> Prop) (h : A) (t : list A),
Forall P (h :: t) <-> P h /\ Forall P t.
Lemma Forall_snoc :
forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
Forall P (snoc x l) <-> Forall P l /\ P x.
Lemma Forall_app :
forall (A : Type) (P : A -> Prop) (l1 l2 : list A),
Forall P (l1 ++ l2) <-> Forall P l1 /\ Forall P l2.
Lemma Forall_rev :
forall (A : Type) (P : A -> Prop) (l : list A),
Forall P (rev l) <-> Forall P l.
Lemma Forall_map :
forall (A B : Type) (P : B -> Prop) (f : A -> B) (l : list A),
Forall P (map f l) -> Forall (fun x : A => P (f x)) l.
Lemma Forall_join :
forall (A : Type) (P : A -> Prop) (ll : list (list A)),
Forall P (join ll) <-> Forall (fun l : list A => Forall P l) ll.
Lemma Forall_replicate :
forall (A : Type) (P : A -> Prop) (n : nat) (x : A),
Forall P (replicate n x) <-> n = 0 \/ P x.
Lemma Forall_nth :
forall (A : Type) (P : A -> Prop) (l : list A),
Forall P l <-> forall n : nat, n < length l ->
exists x : A, nth n l = Some x /\ P x.
Lemma Forall_remove :
forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
Forall P l ->
match remove n l with
| None => True
| Some (x, l') => Forall P l'
end.
Lemma Forall_take :
forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
Forall P l -> Forall P (take n l).
Lemma Forall_drop :
forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
Forall P l -> Forall P (drop n l).
Lemma Forall_take_drop :
forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
Forall P (take n l) -> Forall P (drop n l) -> Forall P l.
Lemma Forall_splitAt :
forall (A : Type) (P : A -> Prop) (l l1 l2 : list A) (n : nat) (x : A),
splitAt n l = Some (l1, x, l2) ->
Forall P l <-> P x /\ Forall P l1 /\ Forall P l2.
Lemma Forall_insert :
forall (A : Type) (P : A -> Prop) (l : list A) (n : nat) (x : A),
Forall P (insert l n x) <-> P x /\ Forall P l.
Lemma Forall_replace :
forall (A : Type) (P : A -> Prop) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' ->
Forall P l' <->
Forall P (take n l) /\ P x /\ Forall P (drop (S n) l).
Lemma Forall_filter :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
Forall P l -> Forall P (filter p l).
Lemma Forall_filter_conv :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
Forall P (filter p l) ->
Forall P (filter (fun x : A => negb (p x)) l) ->
Forall P l.
Lemma Forall_filter_compat :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
(forall x : A, P x <-> p x = true) -> Forall P (filter p l).
Lemma Forall_partition :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l l1 l2 : list A),
partition p l = (l1, l2) ->
Forall P l <-> Forall P l1 /\ Forall P l2.
Lemma Forall_takeWhile :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
Forall P l -> Forall P (takeWhile p l).
Lemma Forall_takeWhile_compat :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
(forall x : A, P x <-> p x = true) -> Forall P (takeWhile p l).
Lemma Forall_dropWhile :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
Forall P l -> Forall P (dropWhile p l).
Lemma Forall_takeWhile_dropWhile :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
Forall P (takeWhile p l) -> Forall P (dropWhile p l) -> Forall P l.
Lemma Forall_span :
forall
(A : Type) (P : A -> Prop) (p : A -> bool) (x : A) (l b e : list A),
(forall x : A, P x <-> p x = true) ->
span p l = Some (b, x, e) ->
Forall P l <-> Forall P b /\ P x /\ Forall P e.
Lemma Forall_zip :
forall (A B : Type) (PA : A -> Prop) (PB : B -> Prop)
(la : list A) (lb : list B),
Forall PA la -> Forall PB lb ->
Forall (fun '(a, b) => PA a /\ PB b) (zip la lb).
Lemma Forall_pmap :
forall (A B : Type) (f : A -> option B) (P : B -> Prop) (l : list A),
Forall (fun x : A => match f x with | Some b => P b | _ => False end) l ->
Forall P (pmap f l).
Lemma Forall_intersperse :
forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
Forall P (intersperse x l) <->
Forall P l /\ (2 <= length l -> P x).
Lemma Forall_impl :
forall (A : Type) (P Q : A -> Prop) (l : list A),
(forall x : A , P x -> Q x) ->
Forall P l -> Forall Q l.
Lemma Forall_Exists :
forall (A : Type) (P : A -> Prop) (l : list A),
Forall P l -> ~ Exists (fun x : A => ~ P x) l.
Lemma Exists_Forall :
forall (A : Type) (P : A -> Prop) (l : list A),
Exists P l -> ~ Forall (fun x : A => ~ P x) l.
AtLeast
Czas uogólnić relację
Rep oraz predykaty
Exists i
Forall. Zdefiniuj
w tym celu relację
AtLeast. Zdanie
AtLeast P n l zachodzi, gdy na
liście
l jest co najmniej
n elementów spełniających predykat
P.
Lemma AtLeast_cons :
forall (A : Type) (P : A -> Prop) (n : nat) (h : A) (t : list A),
AtLeast P n (h :: t) <->
AtLeast P n t \/ P h /\ AtLeast P (n - 1) t.
Lemma AtLeast_cons' :
forall (A : Type) (P : A -> Prop) (n : nat) (h : A) (t : list A),
AtLeast P (S n) (h :: t) -> AtLeast P n t.
Lemma AtLeast_length :
forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
AtLeast P n l -> n <= length l.
Lemma AtLeast_snoc :
forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
AtLeast P n l -> AtLeast P n (snoc x l).
Lemma AtLeast_S_snoc :
forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
AtLeast P n l -> P x -> AtLeast P (S n) (snoc x l).
Lemma AtLeast_Exists :
forall (A : Type) (P : A -> Prop) (l : list A),
AtLeast P 1 l <-> Exists P l.
Lemma AtLeast_Forall :
forall (A : Type) (P : A -> Prop) (l : list A),
AtLeast P (length l) l <-> Forall P l.
Lemma AtLeast_Rep :
forall (A : Type) (x : A) (n : nat) (l : list A),
AtLeast (fun y : A => x = y) n l <-> Rep x n l.
Lemma AtLeast_app_l :
forall (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
AtLeast P n l1 -> AtLeast P n (l1 ++ l2).
Lemma AtLeast_app_r :
forall (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
AtLeast P n l2 -> AtLeast P n (l1 ++ l2).
Lemma AtLeast_plus_app :
forall (A : Type) (P : A -> Prop) (n1 n2 : nat) (l1 l2 : list A),
AtLeast P n1 l1 -> AtLeast P n2 l2 ->
AtLeast P (n1 + n2) (l1 ++ l2).
Lemma AtLeast_app_conv :
forall (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
AtLeast P n (l1 ++ l2) ->
exists n1 n2 : nat, AtLeast P n1 l1 /\ AtLeast P n2 l2 /\ n = n1 + n2.
Lemma AtLeast_app :
forall (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
AtLeast P n (l1 ++ l2) <->
exists n1 n2 : nat,
AtLeast P n1 l1 /\ AtLeast P n2 l2 /\ n = n1 + n2.
Lemma AtLeast_app_comm :
forall (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
AtLeast P n (l1 ++ l2) -> AtLeast P n (l2 ++ l1).
Lemma AtLeast_rev :
forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
AtLeast P n (rev l) <-> AtLeast P n l.
Lemma AtLeast_map :
forall (A B : Type) (P : B -> Prop) (f : A -> B) (n : nat) (l : list A),
AtLeast (fun x : A => P (f x)) n l ->
AtLeast P n (map f l).
Lemma AtLeast_map_conv :
forall (A B : Type) (P : B -> Prop) (f : A -> B) (n : nat) (l : list A),
(forall x y : A, f x = f y -> x = y) -> AtLeast P n (map f l) ->
AtLeast (fun x : A => P (f x)) n l.
Lemma AtLeast_replicate :
forall (A : Type) (P : A -> Prop) (n : nat) (x : A),
n <> 0 -> P x -> AtLeast P n (replicate n x).
Lemma AtLeast_replicate_conv :
forall (A : Type) (P : A -> Prop) (n m : nat) (x : A),
AtLeast P m (replicate n x) -> m = 0 \/ m <= n /\ P x.
Lemma AtLeast_remove :
forall (A : Type) (P : A -> Prop) (l : list A) (m : nat),
AtLeast P m l -> forall n : nat,
match remove n l with
| None => True
| Some (_, l') => AtLeast P (m - 1) l'
end.
Lemma AtLeast_take :
forall (A : Type) (P : A -> Prop) (l : list A) (n m : nat),
AtLeast P m (take n l) -> AtLeast P m l.
Lemma AtLeast_drop :
forall (A : Type) (P : A -> Prop) (l : list A) (n m : nat),
AtLeast P m (drop n l) -> AtLeast P m l.
Lemma AtLeast_take_drop :
forall (A : Type) (P : A -> Prop) (n m : nat) (l : list A),
AtLeast P n l ->
exists n1 n2 : nat,
AtLeast P n1 (take m l) /\ AtLeast P n2 (drop m l) /\ n = n1 + n2.
Lemma AtLeast_splitAt :
forall (A : Type) (P : A -> Prop) (l l1 l2 : list A) (n : nat) (x : A),
splitAt n l = Some (l1, x, l2) ->
forall m : nat,
AtLeast P m l ->
exists m1 mx m2 : nat,
AtLeast P m1 l1 /\ AtLeast P mx [x] /\ AtLeast P m2 l2 /\
m1 + mx + m2 = m.
Lemma AtLeast_insert :
forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
AtLeast P n l -> forall (m : nat) (x : A),
AtLeast P n (insert l m x).
Lemma AtLeast_replace :
forall (A : Type) (P : A -> Prop) (l l' : list A) (n m : nat) (x : A),
replace l n x = Some l' -> AtLeast P m l ->
AtLeast P (m - 1) l'.
Lemma AtLeast_replace' :
forall (A : Type) (P : A -> Prop) (l l' : list A) (n m : nat) (x : A),
replace l n x = Some l' -> AtLeast P m l -> P x ->
AtLeast P m l'.
Lemma AtLeast_replace_conv :
forall (A : Type) (P : A -> Prop) (l l' : list A) (n m : nat) (x : A),
replace l n x = Some l' -> AtLeast P m l' -> AtLeast P (m - 1) l.
Lemma AtLeast_replace_conv' :
forall (A : Type) (P : A -> Prop) (l l' : list A) (n m : nat) (x y : A),
replace l n x = Some l' -> nth n l = Some y -> P y ->
AtLeast P m l' -> AtLeast P m l.
Lemma AtLeast_filter :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (n : nat) (l : list A),
AtLeast P n (filter p l) -> AtLeast P n l.
Lemma AtLeast_filter_compat_true :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
(forall x : A, P x <-> p x = true) ->
AtLeast P (length (filter p l)) (filter p l).
Lemma AtLeast_filter_compat_false :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (n : nat) (l : list A),
(forall x : A, P x <-> p x = false) ->
AtLeast P n (filter p l) -> n = 0.
Lemma AtLeast_takeWhile :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (n : nat) (l : list A),
AtLeast P n (takeWhile p l) -> AtLeast P n l.
Lemma AtLeast_dropWhile :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (n : nat) (l : list A),
AtLeast P n (dropWhile p l) -> AtLeast P n l.
Lemma AtLeast_takeWhile_true :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
(forall x : A, P x <-> p x = true) ->
AtLeast P (length (takeWhile p l)) (takeWhile p l).
Lemma AtLeast_takeWhile_false :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (n : nat) (l : list A),
(forall x : A, P x <-> p x = false) ->
AtLeast P n (takeWhile p l) -> n = 0.
Lemma AtLeast_dropWhile_true :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A) (n : nat),
(forall x : A, P x <-> p x = true) ->
AtLeast P n l -> AtLeast P (n - length (takeWhile p l)) (dropWhile p l).
Lemma AtLeast_dropWhile_false :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A) (n : nat),
(forall x : A, P x <-> p x = false) ->
AtLeast P n l -> AtLeast P n (dropWhile p l).
Lemma AtLeast_zip :
forall (A B : Type) (PA : A -> Prop) (PB : B -> Prop)
(la : list A) (lb : list B) (n : nat),
AtLeast (fun '(a, b) => PA a /\ PB b) n (zip la lb) ->
AtLeast PA n la /\ AtLeast PB n lb.
Lemma AtLeast_findIndices :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A) (n : nat),
(forall x : A, P x <-> p x = true) ->
AtLeast P n l -> n <= length (findIndices p l).
Lemma AtLeast_1_elem :
forall (A : Type) (P : A -> Prop) (l : list A),
AtLeast P 1 l <-> exists x : A, elem x l /\ P x.
Lemma AtLeast_intersperse :
forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
P x -> AtLeast P (length l - 1) (intersperse x l).
Lemma AtLeast_intersperse' :
forall (A : Type) (P : A -> Prop) (x : A) (n : nat) (l : list A),
AtLeast P n l -> P x ->
AtLeast P (n + (length l - 1)) (intersperse x l).
Lemma AtLeast_intersperse'' :
forall (A : Type) (P : A -> Prop) (x : A) (n : nat) (l : list A),
AtLeast P n l -> ~ P x -> AtLeast P n (intersperse x l).
Exactly
Zdefiniuj predykat
Exactly. Zdanie
Exactly P n l zachodzi, gdy
na liście
l występuje dokładnie
n elementów spełniających predykat
P.
Lemma Exactly_0_cons :
forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
Exactly P 0 (x :: l) <-> ~ P x /\ Exactly P 0 l.
Lemma Exactly_S_cons :
forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
Exactly P (S n) (x :: l) <->
P x /\ Exactly P n l \/ ~ P x /\ Exactly P (S n) l.
Lemma Exactly_AtLeast :
forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
Exactly P n l -> AtLeast P n l.
Lemma Exactly_eq :
forall (A : Type) (P : A -> Prop) (n m : nat) (l : list A),
Exactly P n l -> Exactly P m l -> n = m.
Lemma Exactly_length :
forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
Exactly P n l -> n <= length l.
Lemma Exactly_snoc :
forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
Exactly P n l -> ~ P x -> Exactly P n (snoc x l).
Lemma Exactly_S_snoc :
forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
Exactly P n l -> P x -> Exactly P (S n) (snoc x l).
Lemma Exactly_app :
forall (A : Type) (P : A -> Prop) (n1 n2 : nat) (l1 l2 : list A),
Exactly P n1 l1 -> Exactly P n2 l2 -> Exactly P (n1 + n2) (l1 ++ l2).
Lemma Exactly_app_conv :
forall (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
Exactly P n (l1 ++ l2) ->
exists n1 n2 : nat,
Exactly P n1 l1 /\ Exactly P n2 l2 /\ n = n1 + n2.
Lemma Exactly_app_comm :
forall (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
Exactly P n (l1 ++ l2) -> Exactly P n (l2 ++ l1).
Lemma Exactly_rev :
forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
Exactly P n (rev l) <-> Exactly P n l.
Lemma Exactly_map :
forall (A B : Type) (P : B -> Prop) (f : A -> B) (n : nat) (l : list A),
(forall x y : A, f x = f y -> x = y) ->
Exactly (fun x : A => P (f x)) n l <->
Exactly P n (map f l).
Lemma Exactly_replicate :
forall (A : Type) (P : A -> Prop) (n : nat) (x : A),
P x -> Exactly P n (replicate n x).
Lemma Exactly_replicate_conv :
forall (A : Type) (P : A -> Prop) (n : nat) (x : A),
Exactly P n (replicate n x) -> n = 0 \/ P x.
Lemma Exactly_replicate' :
forall (A : Type) (P : A -> Prop) (n m : nat) (x : A),
Exactly P n (replicate m x) <->
n = 0 /\ m = 0 \/
n = 0 /\ ~ P x \/
n = m /\ P x.
Lemma Exactly_take :
forall (A : Type) (P : A -> Prop) (l : list A) (n m1 m2 : nat),
Exactly P m1 (take n l) -> Exactly P m2 l -> m1 <= m2.
Lemma Exactly_drop :
forall (A : Type) (P : A -> Prop) (l : list A) (n m1 m2 : nat),
Exactly P m1 (drop n l) -> Exactly P m2 l -> m1 <= m2.
Lemma Exactly_take_drop :
forall (A : Type) (P : A -> Prop) (l : list A) (n m : nat),
Exactly P n l -> exists n1 n2 : nat,
n = n1 + n2 /\ Exactly P n1 (take m l) /\ Exactly P n2 (drop m l).
Lemma Exactly_splitAt :
forall (A : Type) (P : A -> Prop) (l l1 l2 : list A) (n : nat) (x : A),
splitAt n l = Some (l1, x, l2) ->
forall m : nat,
Exactly P m l <->
exists m1 mx m2 : nat,
Exactly P m1 l1 /\ Exactly P mx [x] /\ Exactly P m2 l2 /\
m1 + mx + m2 = m.
Lemma Exactly_filter :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
(forall x : A, P x <-> p x = true) ->
Exactly P (length (filter p l)) (filter p l).
Lemma Exactly_takeWhile :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
(forall x : A, P x <-> p x = true) ->
Exactly P (length (takeWhile p l)) (takeWhile p l).
Lemma Exactly_dropWhile :
forall (A : Type) (P : A -> Prop) (p : A -> bool) (n : nat) (l : list A),
(forall x : A, P x <-> p x = true) ->
Exactly P n l ->
Exactly P (n - length (takeWhile p l)) (dropWhile p l).
Lemma Exactly_span :
forall
(A : Type) (P : A -> Prop) (p : A -> bool)
(n : nat)(x : A) (l b e : list A),
(forall x : A, P x <-> p x = true) ->
span p l = Some (b, x, e) ->
Exactly P n l <->
exists n1 n2 : nat,
Exactly P n1 b /\ Exactly P n2 e /\
if p x then S (n1 + n2) = n else n1 + n2 = n.
Lemma Exactly_intersperse :
forall (A : Type) (P : A -> Prop) (x : A) (n : nat) (l : list A),
Exactly P n l -> P x ->
Exactly P (n + (length l - 1)) (intersperse x l).
Lemma Exactly_intersperse' :
forall (A : Type) (P : A -> Prop) (x : A) (n : nat) (l : list A),
Exactly P n l -> ~ P x ->
Exactly P n (intersperse x l).
AtMost
Zdefiniuj relację
AtMost. Zdanie
AtMost P n l zachodzi, gdy
na liście
l występuje co najwyżej
n elementów spełniających
predykat
P.
Przykład:
AtMost (fun n => n = 0) 3 [0; 1; 2; 3; 0] zachodzi.
AtMost (fun n => n < 5) 5 [1; 2; 3; 4; 5; 6; 7] nie zachodzi.
Lemma AtMost_0 :
forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
AtMost P 0 (x :: l) <-> ~ P x /\ AtMost P 0 l.
Lemma AtMost_nil :
forall (A : Type) (P : A -> Prop) (n : nat),
AtMost P n [] <-> True.
Lemma AtMost_le :
forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
AtMost P n l -> forall m : nat, n <= m -> AtMost P m l.
Lemma AtMost_S_cons :
forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
AtMost P (S n) (x :: l) <->
(~ P x /\ AtMost P (S n) l) \/ AtMost P n l.
Lemma AtMost_S_snoc :
forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
AtMost P n l -> AtMost P (S n) (snoc x l).
Lemma AtMost_snoc :
forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
AtMost P n l -> ~ P x -> AtMost P n (snoc x l).
Lemma AtMost_S :
forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
AtMost P n l -> AtMost P (S n) l.
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 :
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.
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).
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_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.
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 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.
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').
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').
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.
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_app, rev_app. cbn. 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.
Niestandardowe reguły indukcyjne (TODO)
Wyjaśnienia nadejdą już wkrótce.
Fixpoint list_ind_2
(A : Type) (P : list A -> Prop)
(H0 : P [])
(H1 : forall x : A, P [x])
(H2 : forall (x y : A) (l : list A), P l -> P (x :: y :: l))
(l : list A) : P l.
Lemma list_ind_rev :
forall (A : Type) (P : list A -> Prop)
(Hnil : P [])
(Hsnoc : forall (h : A) (t : list A), P t -> P (t ++ [h]))
(l : list A), P l.
Lemma list_ind_app_l :
forall (A : Type) (P : list A -> Prop)
(Hnil : P []) (IH : forall l l' : list A, P l -> P (l' ++ l))
(l : list A), P l.
Lemma list_ind_app_r :
forall (A : Type) (P : list A -> Prop)
(Hnil : P []) (IH : forall l l' : list A, P l -> P (l ++ l'))
(l : list A), P l.
Lemma list_ind_app :
forall (A : Type) (P : list A -> Prop)
(Hnil : P []) (Hsingl : forall x : A, P [x])
(IH : forall l l' : list A, P l -> P l' -> P (l ++ l'))
(l : list A), P l.
Lemma list_app_ind :
forall (A : Type) (P : list A -> Prop),
P [] ->
(forall (l l1 l2 : list A), P l -> P (l1 ++ l ++ l2)) ->
forall l : list A, P l.
Palindromy
Palindrom to słowo, które czyta się tak samo od przodu jak i od tyłu.
Zdefiniuj induktywny predykat
Palindrome, które odpowiada powyższemu
pojęciu palindromu, ale dla list elementów dowolnego typu, a nie tylko
słów.
Lemma Palindrome_inv_2 :
forall (A : Type) (x y : A),
Palindrome [x; y] -> x = y.
Lemma Palindrome_inv_3 :
forall (A : Type) (x y : A) (l : list A),
Palindrome (x :: l ++ [y]) -> x = y.
Lemma nat_ind_2 :
forall P : nat -> Prop,
P 0 -> P 1 -> (forall n : nat, P n -> P (S (S n))) ->
forall n : nat, P n.
Lemma Palindrome_length :
forall (A : Type) (x : A) (n : nat),
exists l : list A, Palindrome l /\ n <= length l.
Lemma Palindrome_cons_snoc :
forall (A : Type) (x : A) (l : list A),
Palindrome l -> Palindrome (x :: snoc x l).
Lemma Palindrome_app :
forall (A : Type) (l1 l2 : list A),
Palindrome l1 -> Palindrome l2 -> Palindrome (l1 ++ l2 ++ rev l1).
Lemma Palindrome_app' :
forall (A : Type) (l1 l2 : list A),
Palindrome l2 -> Palindrome (l1 ++ l2 ++ rev l1).
Lemma Palindrome_rev :
forall (A : Type) (l : list A),
Palindrome l <-> Palindrome (rev l).
Definition lengthOrder {A : Type} (l1 l2 : list A) : Prop :=
length l1 < length l2.
Lemma lengthOrder_wf :
forall A : Type, well_founded (@lengthOrder A).
Lemma Palindrome_spec :
forall (A : Type) (l : list A),
Palindrome l <-> l = rev l.
Lemma Palindrome_spec' :
forall (A : Type) (l : list A),
Palindrome l -> exists l1 l2 : list A,
l = l1 ++ l2 ++ rev l1 /\ length l2 <= 1.
Lemma Palindrome_map :
forall (A B : Type) (f : A -> B) (l : list A),
Palindrome l -> Palindrome (map f l).
Lemma replicate_S :
forall (A : Type) (n : nat) (x : A),
replicate (S n) x = x :: replicate n x.
Lemma Palindrome_replicate :
forall (A : Type) (n : nat) (x : A),
Palindrome (replicate n x).
Lemma Palindrome_cons_replicate :
forall (A : Type) (n : nat) (x y : A),
Palindrome (x :: replicate n y) -> n = 0 \/ x = y.
Lemma Palindrome_iterate :
forall (A : Type) (f : A -> A),
(forall (n : nat) (x : A), Palindrome (iterate f n x)) ->
forall x : A, f x = x.
Lemma Palindrome_nth :
forall (A : Type) (l : list A),
Palindrome l -> forall n : nat,
n < length l -> nth n l = nth (length l - S n) l.
Lemma Palindrome_drop :
forall (A : Type) (l : list A),
(forall n : nat, Palindrome (drop n l)) ->
l = [] \/ exists (n : nat) (x : A), l = replicate n x.
Lemma Palindrome_take :
forall (A : Type) (l : list A),
(forall n : nat, Palindrome (take n l)) ->
l = [] \/ exists (n : nat) (x : A), l = replicate n x.
Lemma replace_Palindrome :
forall (A : Type) (l l' : list A) (n : nat) (x : A),
replace l n x = Some l' -> Palindrome l ->
Palindrome l' <-> length l = 1 /\ n = 0 \/ nth n l = Some x.
Lemma Palindrome_zip :
exists (A B : Type) (la : list A) (lb : list B),
Palindrome la /\ Palindrome lb /\ ~ Palindrome (zip la lb).
Lemma Palindrome_find_findLast :
forall (A : Type) (p : A -> bool) (l : list A),
Palindrome l -> find p l = findLast p l.
Lemma Palindrome_pmap :
forall (A B : Type) (f : A -> option B) (l : list A),
Palindrome l -> Palindrome (pmap f l).
Lemma Palindrome_intersperse :
forall (A : Type) (x : A) (l : list A),
Palindrome l -> Palindrome (intersperse x l).
Lemma Palindrome_Dup :
forall (A : Type) (l : list A),
Palindrome l -> length l <= 1 \/ Dup l.
Lemma Sublist_Palindrome :
forall (A : Type) (l1 l2 : list A),
Sublist l1 l2 -> Palindrome l1 -> Palindrome l2 -> l1 = [].
Lemma Prefix_Palindrome :
forall (A : Type) (l : list A),
Prefix (rev l) l <-> Palindrome l.
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.