D5a: Proste funkcje na listach
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 Lia Arith Recdef Bool 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) ..).
Bardzo proste funkcje
isEmpty
Zdefiniuj funkcję
isEmpty, która sprawdza, czy lista jest pusta.
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.
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.
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.
Proste funkcje
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 head_snoc :
forall (A : Type) (x : A) (l : list A),
head (snoc x l) =
if isEmpty l then Some x else head l.
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 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 isEmpty_app :
forall (A : Type) (l1 l2 : list A),
isEmpty (l1 ++ l2) = andb (isEmpty l1) (isEmpty l2).
Lemma head_app :
forall (A : Type) (l1 l2 : list A),
head (l1 ++ l2) =
match l1 with
| [] => head l2
| h :: _ => Some h
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 app_assoc :
forall (A : Type) (l1 l2 l3 : list A),
l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.
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 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 no_infinite_app_l :
forall (A : Type) (l l' : list A),
l = l ++ l' -> l' = [].
Lemma no_infinite_app_r :
forall (A : Type) (l l' : list A),
l = l' ++ l -> l' = [].
Lemma no_infinite_app :
forall (A : Type) (l l' : list A),
l' <> [] -> l = l' ++ l -> False.
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) (l : list A) (x : 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_rev :
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 isEmpty_map :
forall (A B : Type) (f : A -> B) (l : list A),
isEmpty (map f l) = isEmpty l.
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 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 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 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.
Lemma bind_app :
forall {A B : Type} (f : A -> list B) (l1 l2 : list A),
bind f (l1 ++ l2) = bind f l1 ++ bind f l2.
Lemma rev_bind :
forall (A B : Type) (f : A -> list B) (l : list A),
rev (bind f l) = bind (fun x : A => rev (f x)) (rev l).
Lemma bind_bind :
forall {A B C : Type} (f : A -> list B) (g : B -> list C) (l : list A),
bind g (bind f l) = bind (fun x : A => bind g (f x)) l.
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 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 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 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_add_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 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.
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.
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),
snoc (iter f n x) (iterate 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 rev_iterate :
forall (A : Type) (f g : A -> A) (n : nat) (x : A),
(forall x : A, g (f x) = x) ->
rev (iterate f n x) = iterate g n (iter f (n - 1) 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.
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_None :
forall {A : Type} {l : list A},
last l = None -> l = [].
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.
Lemma rev_unsnoc :
forall (A : Type) (x : A) (l l' : list A),
unsnoc l = Some (x, l') -> Some (rev l') = tail (rev l).
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 rev_uncons :
forall (A : Type) (x : A) (l l' : list A),
uncons l = Some (x, l') -> Some (rev l') = init (rev l).
Lemma tail_decomposition :
forall (A : Type) (l : list A),
l = [] \/
exists (h : A) (t : list A),
tail l = Some t /\ head l = Some h /\ l = h :: t.
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_lt :
forall (A : Type) (n : nat) (x : A) (l : list A),
n < length l -> nth n (snoc x l) = nth n l.
Lemma nth_snoc_eq :
forall (A : Type) (n : nat) (x : A) (l : list A),
n = length l -> nth n (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_aux :
forall (A : Type) (n : nat) (l : list A),
n < length l -> nth n l = nth (length l - S n) (rev l).
Lemma nth_rev :
forall (A : Type) (n : nat) (l : list A),
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 (Nat.eqb 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 :
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 Nat.eqb 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 :
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) (l : list A) (n : nat),
drop n (rev l) = rev (take (length l - n) l).
Lemma rev_drop :
forall (A : Type) (l : list A) (n : nat),
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 Nat.eqb 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 Nat.eqb 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.
Lemma replace_rev :
forall (A : Type) (l : list A) (n : nat) (x : A),
n < length l ->
replace (rev l) n x = option_map 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).
Lemma rev_unzip :
forall (A B : Type) (l : list (A * B)) (la : list A) (lb : list B),
unzip l = (la, lb) -> unzip (rev l) = (rev la, rev 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.
Lemma zipWith_not_rev :
exists (A B C : Type) (f : A -> B -> C) (la : list A) (lb : list B),
zipWith f (rev la) (rev lb) <> rev (zipWith f la lb).
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.
Lemma rev_unzipWith :
forall (A B C : Type) (f : A -> B * C) (l : list A),
unzipWith f (rev l) =
let (la, lb) := unzipWith f l in (rev la, rev lb).
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 findLast_rev :
forall (A : Type) (p : A -> bool) (l : list A),
findLast p (rev l) = find p 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 (Nat.eqb (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.
Rozstrzyganie równości list (TODO)
Fixpoint list_eq_dec
{A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
match l1, l2 with
| [], [] => true
| [], _ => false
| _, [] => false
| h1 :: t1, h2 :: t2 => eq_dec h1 h2 && list_eq_dec eq_dec t1 t2
end.
Lemma list_eq_dec_spec :
forall
{A : Type} {eq_dec : A -> A -> bool}
(eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
(l1 l2 : list A),
reflect (l1 = l2) (list_eq_dec eq_dec l1 l2).