D1e: Podstawowe funkcje na listach [TODO]
Podstawowe funkcje na listach (TODO)
foldr, czyli standardowa reguła rekursji dla list (TODO)
From Typonomikon Require Import D5a.
Fixpoint foldr
{A B : Type} (f : A -> B -> B) (b : B) (l : list A) : B :=
match l with
| [] => b
| h :: t => f h (foldr f b t)
end.
Nie będę na razie tłumaczył, jaka ideologia stoi za
foldr i
foldl.
Napiszę o tym później, a na razie porcja zadań.
Zaimplementuj za pomocą
foldr następujące funkcje:
length,
app,
rev,
map,
join,
filter,
takeWhile,
dropWhile.
Udowodnij, że zdefiniowane przez ciebie funkcje pokrywają się ze
swoimi klasycznymi odpowiednikami.
Lemma lengthF_spec :
forall (A : Type) (l : list A),
lengthF l = length l.
Lemma snocF_spec :
forall (A : Type) (x : A) (l : list A),
snocF x l = snoc x l.
Lemma appF_spec :
forall (A : Type) (l1 l2 : list A),
appF l1 l2 = l1 ++ l2.
Lemma revF_spec :
forall (A : Type) (l : list A),
revF l = rev l.
Lemma mapF_spec :
forall (A B : Type) (f : A -> B) (l : list A),
mapF f l = map f l.
Lemma joinF_spec :
forall (A : Type) (l : list (list A)),
joinF l = join l.
Lemma allF_spec :
forall (A : Type) (p : A -> bool) (l : list A),
allF p l = all p l.
Lemma anyF_spec :
forall (A : Type) (p : A -> bool) (l : list A),
anyF p l = any p l.
Lemma findF_spec :
forall (A : Type) (p : A -> bool) (l : list A),
findF p l = find p l.
Lemma findIndexF_spec :
forall (A : Type) (p : A -> bool) (l : list A),
findIndexF p l = findIndex p l.
Lemma countF_spec :
forall (A : Type) (p : A -> bool) (l : list A),
countF p l = count p l.
Lemma filterF_spec :
forall (A : Type) (p : A -> bool) (l : list A),
filterF p l = filter p l.
Lemma takeWhileF_spec :
forall (A : Type) (p : A -> bool) (l : list A),
takeWhileF p l = takeWhile p l.
Lemma foldr_app :
forall (A B : Type) (f : A -> B -> B) (b : B) (l1 l2 : list A),
foldr f b (l1 ++ l2) = foldr f (foldr f b l2) l1.
Lemma foldr_map :
forall (A A' B : Type) (f : A' -> B -> B) (g : A -> A') (b : B) (l : list A),
foldr f b (map g l) = foldr (fun a x => f (g a) x) b l.