Zadania

Postanowiłem zrobić nowy rozdział, w którym będę trzymał same zadania. Każda sekcja z zadaniami będzie odpowiadać pewnemu podrozdziałowi. Polecam robić je na bieżąco. Niektóre zadania mogą pokrywać się z tymi z tekstu.
Zadania skądinąd (choćby z rozdziału 1) planuję w najbliższej przeszłości przerzucić tutaj.

R2

Enumeracje

Zadania z funkcji boolowskich, sprawdzające radzenie sobie w pracy z enumeracjami, definiowaniem funkcji przez pattern matching i dowodzeniem przez rozbicie na przypadki.
Chciałem, żeby nazwy twierdzeń odpowiadały tym z biblioteki standardowej, ale na razie nie mam siły tego ujednolicić.

Section boolean_functions.
Variables b b1 b2 b3 : bool.

Zdefiniuj następujące funkcje boolowskie:


Notation "b1 && b2" := (andb b1 b2).
Notation "b1 || b2" := (orb b1 b2).

Udowodnij następujące twierdzenia.


(* Właściwości negacji *)
Theorem negb_inv : negb (negb b) = b.

Theorem negb_ineq : negb b <> b.

(* Eliminacja *)
Theorem andb_elim_l : b1 && b2 = true -> b1 = true.

Theorem andb_elim_r : b1 && b2 = true -> b2 = true.

Theorem andb_elim : b1 && b2 = true -> b1 = true /\ b2 = true.

Theorem orb_elim : b1 || b2 = true -> b1 = true \/ b2 = true.

(* Elementy neutralne i anihilujące *)
Theorem andb_false_annihilation_l : false && b = false.

Theorem andb_false_annihilation_r : b && false = false.

Theorem andb_true_neutral_l : true && b = b.

Theorem andb_true_neutral_r : b && true = b.

Theorem orb_true_annihilation_l : true || b = true.

Theorem orb_true_annihilation_r : b || true = true.

Theorem orb_false_neutral_l : false || b = b.

Theorem orb_false_neutral_r : b || false = b.

(* Przemienność *)
Theorem andb_comm : b1 && b2 = b2 && b1.

Theorem orb_comm : b1 || b2 = b2 || b1.

(* Łączność *)
Theorem andb_assoc : b1 && (b2 && b3) = (b1 && b2) && b3.

Theorem orb_assoc : b1 || (b2 || b3) = (b1 || b2) || b3.

(* Rozdzielność *)
Theorem andb_dist_orb : b1 && (b2 || b3) = (b1 && b2) || (b1 && b3).

Theorem orb_dist_andb : b1 || (b2 && b3) = (b1 || b2) && (b1 || b3).

(* Negacja *)
Theorem andb_negb : b && negb b = false.

Theorem orb_negb : b || negb b = true.

(* de Morgan *)
Theorem negb_andb : negb (b1 && b2) = negb b1 || negb b2.

Theorem negb_orb : negb (b1 || b2) = negb b1 && negb b2.

(* eqb, xorb, norb, nandb *)
Theorem eqb_spec : eqb b1 b2 = true -> b1 = b2.

Theorem eqb_spec' : eqb b1 b2 = false -> b1 <> b2.

Theorem xorb_spec : xorb b1 b2 = negb (eqb b1 b2).

Theorem xorb_spec' : xorb b1 b2 = true -> b1 <> b2.

Theorem norb_spec : norb b1 b2 = negb (b1 || b2).

Theorem nandb_spec : nandb b1 b2 = negb (b1 && b2).

(* Różne *)
Theorem andb_eq_orb : b1 && b2 = b1 || b2 -> b1 = b2.

Theorem all3_spec : (b1 && b1) || (negb b1 || negb b2) = true.

Theorem noncontradiction_bool : negb (eqb b (negb b)) = true.

End boolean_functions.

Póki co bezimienny rozdział (alfa)

Injekcje, surjekcje, bijekcje (alfa)


Require Import Arith.

Definition injective {A B : Type} (f : A -> B) : Prop :=
    forall x x' : A, f x = f x' -> x = x'.

TODO: trzeba tu coś napisać, ale na razie nie mam czasu.

Definition injective' {A B : Type} (f : A -> B) : Prop :=
    forall x x' : A, x <> x' -> f x <> f x'.

Theorem injective_is_injective' : forall (A B : Type) (f : A -> B),
    injective f -> injective' f.

Theorem injective'_is_injective_classic : forall (A B : Type) (f : A -> B)
    (EM : forall P : Prop, P \/ ~ P), injective' f -> injective f.

Theorem id_injective : forall A : Type,
    injective (fun x : A => x).

Theorem S_injective : injective (fun n : nat => S n).

Theorem add_k_left_inj : forall k : nat,
    injective (fun n : nat => k + n).

Theorem mul_k_inj : forall k : nat, k <> 0 ->
    injective (fun n : nat => k * n).


Theorem pred_not_injective : ~ injective pred.

Definition surjective {A B : Type} (f : A -> B) : Prop :=
    forall b : B, exists a : A, f a = b.

Theorem S_not_surjective : ~ surjective S.

Definition bijective {A B : Type} (f : A -> B) : Prop :=
    injective f /\ surjective f.

Definition bijective' {A B : Type} (f : A -> B) : Prop :=
    forall b : B, exists! a : A, f a = b.

Theorem bijectives_equiv : forall (A B : Type) (f : A -> B),
    bijective f <-> bijective' f.

Require Import List.
Import ListNotations.

Fixpoint unary (n : nat) : list unit :=
match n with
    | 0 => []
    | S n' => tt :: unary n'
end.

Theorem unary_bij : bijective unary.

Wreszcie zadania z arytmetyki (alfa)

Poniższe zadania mają służyć utrwaleniu zdobytej dotychczas wiedzy na temat prostej rekursji i indukcji. Większość powinna być robialna po przeczytaniu rozdziału o konstruktorach rekurencyjnych, ale niczego nie gwarantuję.
Celem zadań jest rozwinięcie arytmetyki do takiego poziomu, żeby można było tego używać gdzie indziej w jakotakim stopniu. Niektóre zadania mogą pokrywać się z zadaniami obecnymi w tekście, a niektóre być może nawet z przykładami. Staraj się nie podglądać.
Nazwy twierdzeń nie muszą pokrywać się z tymi z biblioteki standardowej, choć starałem się, żeby tak było.

Module MyNat.

Zdefiniuj liczby naturalne.


Notation "0" := O.
Notation "1" := (S 0).

Udowodnij właściwości zera i następnika.

Theorem neq_0_Sn : forall n : nat, 0 <> S n.

Theorem neq_n_Sn : forall n : nat, n <> S n.

Theorem not_eq_S : forall n m : nat, n <> m -> S n <> S m.

Theorem S_injective : forall n m : nat, S n = S m -> n = m.

Zdefiniuj funkcję zwracającą poprzednik danej liczby naturalnej. Poprzednikiem 0 jest 0.


Theorem pred_0 : pred 0 = 0.

Theorem pred_Sn : forall n : nat, pred (S n) = n.

Zdefiniuj dodawanie (rekurencyjnie po pierwszym argumencie) i udowodnij jego właściwości.


Theorem plus_0_l : forall n : nat, plus 0 n = n.

Theorem plus_0_r : forall n : nat, plus n 0 = n.

Theorem plus_n_Sm : forall n m : nat, S (plus n m) = plus n (S m).

Theorem plus_Sn_m : forall n m : nat, plus (S n) m = S (plus n m).

Theorem plus_assoc : forall a b c : nat,
    plus a (plus b c) = plus (plus a b) c.

Theorem plus_comm : forall n m : nat, plus n m = plus m n.

Theorem no_annihilation_l :
    ~ exists a : nat, forall n : nat, plus a n = a.

Theorem no_annihilation_r :
    ~ exists a : nat, forall n : nat, plus n a = a.

Theorem no_inverse_l :
    ~ forall n : nat, exists i : nat, plus i n = 0.

Theorem no_inverse_r :
    ~ forall n : nat, exists i : nat, plus n i = 0.

Pokaż, że plus' n m = n + m

Fixpoint plus' (n m : nat) : nat :=
match m with
    | 0 => n
    | S m' => plus' (S n) m'
end.

Theorem plus'_0_r : forall n : nat, plus' n 0 = n.

Theorem plus'_S : forall n m : nat, plus' (S n) m = S (plus' n m).

Theorem plus'_0_l : forall n : nat, plus' 0 n = n.

Theorem plus'_comm : forall n m : nat, plus' n m = plus' m n.

Theorem plus'_is_plus : forall n m : nat, plus' n m = plus n m.

Udowodnij powyższe twierdzenie bez używania lematów pomocniczych.

Theorem plus'_is_plus_no_lemmas : forall n m : nat,
    plus' n m = plus n m.

Udowodnij analogiczne twierdzenia dla plus'' i plus'''

Fixpoint plus'' (n m : nat) : nat :=
match n with
    | 0 => m
    | S n' => plus'' n' (S m)
end.

Theorem plus''_is_plus : forall n m : nat, plus'' n m = plus n m.

Fixpoint plus''' (n m : nat) : nat :=
match m with
    | 0 => n
    | S m' => S (plus''' n m')
end.

Theorem plus'''_is_plus : forall n m : nat,
    plus''' n m = plus n m.

Zdefiniuj odejmowanie i udowodnij jego właściwości.


Theorem minus_pred : forall n : nat,
    minus n 1 = pred n.

Theorem minus_0_l : forall n : nat,
    minus 0 n = 0.

Theorem minus_0_r : forall n : nat,
    minus n 0 = n.

Theorem minus_S : forall n m : nat,
    minus (S n) (S m) = minus n m.

Theorem minus_n : forall n : nat, minus n n = 0.

Theorem minus_plus_l : forall n m : nat,
    minus (plus n m) n = m.

Theorem minus_plus_r : forall n m : nat,
    minus (plus n m) m = n.

Theorem minus_plus_distr : forall a b c : nat,
    minus a (plus b c) = minus (minus a b) c.

Theorem minus_exchange : forall a b c : nat,
    minus (minus a b) c = minus (minus a c) b.

Theorem minus_not_comm : ~ forall n m : nat,
    minus n m = minus m n.

Zdefiniuj mnożenie i udowodnij jego właściwości.


Theorem mult_0_l : forall n : nat, mult 0 n = 0.

Theorem mult_0_r : forall n : nat, mult n 0 = 0.

Theorem mult_1_l : forall n : nat, mult 1 n = n.

Theorem mult_1_r : forall n : nat, mult n 1 = n.

Theorem mult_comm : forall n m : nat,
    mult n m = mult m n.

Theorem mult_plus_distr_r : forall a b c : nat,
    mult (plus a b) c = plus (mult a c) (mult b c).

Theorem mult_minus_distr_l : forall a b c : nat,
    mult a (minus b c) = minus (mult a b) (mult a c).

Theorem mult_minus_distr_r : forall a b c : nat,
    mult (minus a b) c = minus (mult a c) (mult b c).

Theorem mult_assoc : forall a b c : nat,
    mult a (mult b c) = mult (mult a b) c.

Theorem mult_no_inverse_l :
    ~ forall n : nat, exists i : nat, mult i n = 1.

Theorem mult_no_inverse_r :
    ~ forall n : nat, exists i : nat, mult n i = 1.

Theorem mult_2_plus : forall n : nat, mult (S (S 0)) n = plus n n.

Zdefiniuj relację "mniejszy lub równy" i udowodnij jej właściwości.


Notation "n <= m" := (le n m).

Theorem le_0_n : forall n : nat, 0 <= n.

Theorem le_n_Sm : forall n m : nat, n <= m -> n <= S m.

Theorem le_Sn_m : forall n m : nat, S n <= m -> n <= m.

Theorem le_n_S : forall n m : nat, n <= m -> S n <= S m.

Theorem le_S_n : forall n m : nat, S n <= S m -> n <= m.

Theorem le_Sn_n : forall n : nat, ~ S n <= n.

Theorem le_refl : forall n : nat, n <= n.

Theorem le_trans : forall a b c : nat,
    a <= b -> b <= c -> a <= c.

Theorem le_antisym : forall n m : nat,
    n <= m -> m <= n -> n = m.

Theorem le_pred : forall n : nat, pred n <= n.

Theorem le_n_pred : forall n m : nat,
    n <= m -> pred n <= pred m.

Theorem no_le_pred_n : ~ forall n m : nat,
    pred n <= pred m -> n <= m.

Theorem le_plus_l : forall a b c : nat,
    b <= c -> plus a b <= plus a c.

Theorem le_plus_r : forall a b c : nat,
    a <= b -> plus a c <= plus b c.

Theorem le_plus : forall a b c d : nat,
    a <= b -> c <= d -> plus a c <= plus b d.

Theorem le_minus_S : forall n m : nat,
    minus n (S m) <= minus n m.

Theorem le_minus_l : forall a b c : nat,
    b <= c -> minus a c <= minus a b.

Theorem le_minus_r : forall a b c : nat,
    a <= b -> minus a c <= minus b c.

Theorem le_mult_l : forall a b c : nat,
    b <= c -> mult a b <= mult a c.

Theorem le_mult_r : forall a b c : nat,
    a <= b -> mult a c <= mult b c.

Theorem le_mult : forall a b c d : nat,
    a <= b -> c <= d -> mult a c <= mult b d.

Theorem le_plus_exists : forall n m : nat,
    n <= m -> exists k : nat, plus n k = m.

Zdefiniuj minimum i maksimum oraz udowodnij ich właściwości.


Theorem min_0_l : forall n : nat, min 0 n = 0.

Theorem min_0_r : forall n : nat, min n 0 = 0.

Theorem max_0_l : forall n : nat, max 0 n = n.

Theorem max_0_r : forall n : nat, max n 0 = n.

Theorem min_le : forall n m : nat, n <= m -> min n m = n.

Theorem max_le : forall n m : nat, n <= m -> max n m = m.

Theorem min_assoc : forall a b c : nat,
    min a (min b c) = min (min a b) c.

Theorem max_assoc : forall a b c : nat,
    max a (max b c) = max (max a b) c.

Theorem min_comm : forall n m : nat, min n m = min m n.

Theorem max_comm : forall n m : nat, max n m = max m n.

Theorem min_refl : forall n : nat, min n n = n.

Theorem max_refl : forall n : nat, max n n = n.

Theorem min_no_neutr_l :
    ~ exists e : nat, forall n : nat, min e n = n.

Theorem min_no_neutr_r :
    ~ exists e : nat, forall n : nat, min n e = n.

Theorem max_no_annihilator_l :
    ~ exists a : nat, forall n : nat, max a n = a.

Theorem max_no_annihilator_r :
    ~ exists a : nat, forall n : nat, max n a = a.

Theorem is_it_true :
    (forall n m : nat, min (S n) m = S (min n m)) \/
    (~ forall n m : nat, min (S n) m = S (min n m)).

Zdefiniuj potęgowanie i udowodnij jego właściwości.


Theorem pow_0_r : forall n : nat, pow n 0 = 1.

Theorem pow_1_l : forall n : nat, pow 1 n = 1.

Theorem pow_1_r : forall n : nat, pow n 1 = n.

Theorem pow_no_neutr_l :
    ~ exists e : nat, forall n : nat, pow e n = n.

Theorem pow_no_annihilator_r :
    ~ exists a : nat, forall n : nat, pow n a = a.

Theorem le_pow_l : forall a b c : nat,
    a <> 0 -> b <= c -> pow a b <= pow a c.

Theorem le_pow_r : forall a b c : nat,
    a <= b -> pow a c <= pow b c.

Theorem pow_mult : forall a b c : nat,
    pow (mult a b) c = mult (pow a c) (pow b c).

Theorem pow_plus : forall a b c : nat,
    pow a (plus b c) = mult (pow a b) (pow a c).

Theorem pow_pow : forall a b c : nat,
    pow (pow a b) c = pow a (mult b c).

Zdefiniuj funkcję leb, która sprawdza, czy n <= m.


Theorem leb_n : forall n : nat,
    leb n n = true.

Theorem leb_spec : forall n m : nat,
    n <= m <-> leb n m = true.

Zdefiniuj funkcję eqb, która sprawdza, czy n = m.


Theorem eqb_spec : forall n m : nat,
    n = m <-> eqb n m = true.

Pokaż, że indukcję na liczbach naturalnych można robić "co 2". Wskazówka: taktyk można używać nie tylko do dowodzenia. Przypomnij sobie, że taktyki to programy, które generują dowody, zaś dowody są programami. Dzięki temu nic nie stoi na przeszkodzie, aby taktyki interpretować jako programy, które piszą inne programy. I rzeczywiście — w Coqu możemy używać taktyk do definiowania dowolnych termów. W niektórych przypadkach jest to bardzo częsta praktyka.

Fixpoint ind_by_2 (P : nat -> Prop) (H0 : P 0) (H1 : P 1)
    (HSS : forall n : nat, P n -> P (S (S n))) (n : nat) : P n.

End MyNat.

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ę w bibliotece standardowej.
Zdefiniuj list (bez podglądania).


Arguments nil [A].
Arguments cons [A] _ _.

Notation "[]" := nil.
Notation "x :: y" := (cons x y) (at level 60, right associativity).
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

Zdefiniuj funkcję length, która oblicza długość listy.


Theorem length_nil : forall A : Type, length (@nil A) = 0.

Theorem length_cons : forall (A : Type) (h : A) (t : list A),
    exists n : nat, length (h :: t) = S n.

Theorem length_0 : forall (A : Type) (l : list A),
    length l = 0 -> l = [].

Zdefiniuj funkcję app, która skleja dwie listy.


Notation "l1 ++ l2" := (app l1 l2).

Theorem app_nil_l : forall (A : Type) (l : list A),
    [] ++ l = l.

Theorem app_nil_r : forall (A : Type) (l : list A),
    l ++ [] = l.

Theorem app_assoc : forall (A : Type) (l1 l2 l3 : list A),
    l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.

Theorem app_length : forall (A : Type) (l1 l2 : list A),
    length (l1 ++ l2) = length l1 + length l2.

Theorem app_cons : forall (A : Type) (x : A) (l1 l2 : list A),
    (x :: l1) ++ l2 = x :: (l1 ++ l2).

Theorem app_cons2 : forall (A : Type) (x : A) (l1 l2 : list A),
    l1 ++ x :: l2 = (l1 ++ [x]) ++ l2.

Theorem no_infinite_cons : forall (A : Type) (x : A) (l : list A),
    l = x :: l -> False.

Theorem no_infinite_app : forall (A : Type) (l l' : list A),
    l' <> [] -> l = l' ++ l -> False.

Theorem app_inv1 : forall (A : Type) (l l1 l2 : list A),
    l ++ l1 = l ++ l2 -> l1 = l2.

Theorem app_inv2 : forall (A : Type) (l l1 l2 : list A),
    l1 ++ l = l2 ++ l -> l1 = l2.

Theorem app_eq_nil : forall (A : Type) (l1 l2 : list A),
    l1 ++ l2 = [] -> l1 = [] /\ l2 = [].

Zdefiniuj funkcję rev, która odwraca listę.


Theorem rev_length : forall (A : Type) (l : list A),
    length (rev l) = length l.

Theorem rev_app : forall (A : Type) (l1 l2 : list A),
    rev (l1 ++ l2) = rev l2 ++ rev l1.

Theorem rev_inv : forall (A : Type) (l : list A),
    rev (rev l) = l.

Zdefiniuj induktywny predykat elem. elem x l jest spełniony, gdy x jest elementem listy l.


Theorem elem_nil : forall (A : Type) (x : A), ~ elem x [].

Theorem elem_inv_head : forall (A : Type) (x h : A) (t : list A),
    ~ elem x (h :: t) -> x <> h.

Theorem elem_inv_tail : forall (A : Type) (x h : A) (t : list A),
    ~ elem x (h :: t) -> ~ elem x t.

Lemma elem_app1 : forall (A : Type) (x : A) (l1 l2 : list A),
    elem x l2 -> elem x (l1 ++ l2).

Theorem elem_app2 : forall (A : Type) (x : A) (l1 l2 : list A),
    elem x l1 -> elem x (l1 ++ l2).

Theorem elem_app_or : forall (A : Type) (x : A) (l1 l2 : list A),
    elem x (l1 ++ l2) -> elem x l1 \/ elem x l2.

Theorem elem_or_app : forall (A : Type) (x : A) (l1 l2 : list A),
    elem x l1 \/ elem x l2 -> elem x (l1 ++ l2).

Theorem elem_rev : forall (A : Type) (x : A) (l : list A),
    elem x l -> elem x (rev l).

Theorem elem_split : forall (A : Type) (x : A) (l : list A),
    elem x l -> exists l1 l2 : list A, l = l1 ++ x :: l2.

Zdefiniuj funkcję map, która aplikuje funkcję f do każdego elementu listy.


Theorem map_id : forall (A : Type) (l : list A),
    map id l = l.

Theorem map_comp : 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.

Theorem map_length : forall (A B : Type) (f : A -> B) (l : list A),
    length (map f l) = length l.

Theorem map_app : forall (A B : Type) (f : A -> B) (l1 l2 : list A),
    map f (l1 ++ l2) = map f l1 ++ map f l2.

Theorem elem_map :
    forall (A B : Type) (f : A -> B) (l : list A) (x : A),
    elem x l -> elem (f x) (map f l).

Theorem 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.

Theorem map_rev : forall (A B : Type) (f : A -> B) (l : list A),
    map f (rev l) = rev (map f l).

Theorem 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.

Theorem 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.

Napisz funkcję join, która spłaszcza listę list.


Theorem join_app : forall (A : Type) (l1 l2 : list (list A)),
    join (l1 ++ l2) = join l1 ++ join l2.

Theorem join_map : forall (A B : Type) (f : A -> B) (l : list (list A)),
    map f (join l) = join (map (map f) l).

Zdefiniuj funkcję repeat, która zwraca listę n powtórzeń wartości x.


Theorem repeat_length : forall (A : Type) (n : nat) (x : A),
    length (repeat n x) = n.

Theorem repeat_elem : forall (A : Type) (n : nat) (x y : A),
    elem x (repeat n y) -> x = y.

Zdefiniuj funkcję nth, która zwraca n-ty element listy lub None, gdy nie ma n-tego elementu.


Theorem nth_length : forall (A : Type) (n : nat) (l : list A),
    n < length l -> exists x : A, nth n l = Some x.

Theorem nth_elem : forall (A : Type) (n : nat) (l : list A),
    n < length l -> exists x : A, nth n l = Some x /\ elem x l.

Theorem nth_elem_conv : forall (A : Type) (x : A) (l : list A),
    elem x l -> exists n : nat, nth n l = Some x.

Theorem nth_overflow : forall (A : Type) (n : nat) (l : list A),
    length l <= n -> ~ exists x : A, nth n l = Some x.

Theorem nth_app1 : forall (A : Type) (n : nat) (l1 l2 : list A),
    n < length l1 -> nth n (l1 ++ l2) = nth n l1.

Theorem nth_app2 : forall (A : Type) (n : nat) (l1 l2 : list A),
    length l1 <= n -> nth n (l1 ++ l2) = nth (n - length l1) l2.

Theorem nth_split : forall (A : Type) (n : nat) (l : list A) (x : A),
    nth n l = Some x -> exists l1 l2 : list A,
        l = l1 ++ x :: l2 /\ length l1 = n.

Theorem nth_None : forall (A : Type) (n : nat) (l : list A),
    nth n l = None -> length l <= n.

Theorem nth_Some : forall (A : Type) (n : nat) (l : list A) (x : A),
    nth n l = Some x -> n < length l.

Theorem map_nth :
    forall (A B : Type) (f : A -> B) (n : nat) (l : list A) (x : A),
        nth n l = Some x -> nth n (map f l) = Some (f x).

Zdefiniuj funkcje head i last, które zwracają odpowiednio pierwszy i ostatni element listy (lub None, jeżeli jest pusta).


Theorem head_nil : forall (A : Type),
    head [] = (@None A).

Theorem last_nil : forall (A : Type), last [] = (@None A).


Theorem head_nth: forall (A : Type) (l : list A),
    head l = nth 0 l.

Theorem last_nth : forall (A : Type) (l : list A),
    last l = nth (length l - 1) l.

Zdefiniuj funkcje tail i init, które zwracają odpowiednio ogon listy oraz wszystko poza jej ostatnim elementem (lub None, gdy lista jest pusta).


Zdefiniuj funkcje take i drop, które odpowiednio biorą lub odrzucają n pierwszych elementów listy.


Theorem take_nil : forall (A : Type) (n : nat),
    take n [] = @nil A.

Theorem drop_nil : forall (A : Type) (n : nat),
    drop n [] = @nil A.

Theorem take_cons : forall (A : Type) (n : nat) (h : A) (t : list A),
    take (S n) (h :: t) = h :: take n t.

Theorem drop_cons : forall (A : Type) (n : nat) (h : A) (t : list A),
    drop (S n) (h :: t) = drop n t.

Theorem take_0 : forall (A : Type) (l : list A),
    take 0 l = [].

Theorem drop_0 : forall (A : Type) (l : list A),
    drop 0 l = l.

Theorem take_length : forall (A : Type) (l : list A),
    take (length l) l = l.

Theorem drop_length : forall (A : Type) (l : list A),
    drop (length l) l = [].

Theorem take_length' : forall (A : Type) (n : nat) (l : list A),
    length l <= n -> take n l = l.

Theorem drop_length' : forall (A : Type) (n : nat) (l : list A),
    length l <= n -> drop n l = [].

Theorem length_take : forall (A : Type) (n : nat) (l : list A),
    n <= length l -> length (take n l) = n.

Theorem drop_map :
    forall (A B : Type) (f : A -> B) (n : nat) (l : list A),
        map f (drop n l) = drop n (map f l).

Theorem take_elem : forall (A : Type) (n : nat) (l : list A) (x : A),
    elem x (take n l) -> elem x l.

Theorem drop_elem : forall (A : Type) (n : nat) (l : list A) (x : A),
    elem x (drop n l) -> elem x l.

Theorem take_take : forall (A : Type) (n m : nat) (l : list A),
    take m (take n l) = take n (take m l).

Lemma drop_S : forall (A : Type) (n m : nat) (l : list A),
    drop (S m) (drop n l) = drop m (drop (S n) l).

Theorem drop_drop : forall (A : Type) (n m : nat) (l : list A),
    drop m (drop n l) = drop n (drop m l).


Theorem take_drop : forall (A : Type) (n m : nat) (l : list A),
    take m (drop n l) = drop n (take (n + m) l).

Napisz funkcję filter, która zostawia na liście elementy, dla których funkcja p zwraca true, a usuwa te, dla których zwraca false.


Theorem filter_false : forall (A : Type) (l : list A),
    filter (fun _ => false) l = [].

Theorem filter_true : forall (A : Type) (l : list A),
    filter (fun _ => true) l = l.

Theorem filter_spec :
    forall (A : Type) (p : A -> bool) (l : list A) (x : A),
        p x = false -> ~ elem x (filter p l).

Theorem filter_app :
    forall (A : Type) (p : A -> bool) (l1 l2 : list A),
        filter p (l1 ++ l2) = filter p l1 ++ filter p l2.

Theorem filter_rev :
    forall (A : Type) (p : A -> bool) (l : list A),
        filter p (rev l) = rev (filter p l).

Theorem filter_comm :
    forall (A : Type) (f g : A -> bool) (l : list A),
        filter f (filter g l) = filter g (filter f l).

Theorem filter_idempotent :
    forall (A : Type) (f : A -> bool) (l : list A),
        filter f (filter f l) = filter f l.

Theorem 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).

Theorem filter_repeat_false :
    forall (A : Type) (p : A -> bool) (n : nat) (x : A),
        p x = false -> filter p (repeat n x) = [].

Theorem filter_repeat_true :
    forall (A : Type) (p : A -> bool) (n : nat) (x : A),
        p x = true -> filter p (repeat n x) = repeat n x.

Theorem filter_length :
    forall (A : Type) (p : A -> bool) (l : list A),
        length (filter p l) <= length l.

Theorem filter_join :
    forall (A : Type) (p : A -> bool) (lla : list (list A)),
        join (map (filter p) lla) = filter p (join lla).

Zdefiniuj funkcje takeWhile oraz dropWhile, które, dopóki funkcja p zwraca true, odpowiednio biorą lub usuwają elementy z listy.


Theorem takeWhile_false : forall (A : Type) (l : list A),
    takeWhile (fun _ => false) l = [].

Theorem dropWhile_false : forall (A : Type) (l : list A),
    dropWhile (fun _ => false) l = l.

Theorem takeWhile_spec :
    forall (A : Type) (p : A -> bool) (l : list A) (x : A),
        elem x (takeWhile p l) -> p x = true.


Theorem dropWhile_spec :
    forall (A : Type) (p : A -> bool) (l : list A) (x : A),
        elem x l -> ~ elem x (dropWhile p l) -> p x = true.

Theorem takeWhile_idempotent :
    forall (A : Type) (p : A -> bool) (l : list A),
        takeWhile p (takeWhile p l) = takeWhile p l.

Theorem dropWhile_idempotent :
    forall (A : Type) (p : A -> bool) (l : list A),
        dropWhile p (dropWhile p l) = dropWhile p l.

Theorem takeWhile_repeat :
    forall (A : Type) (p : A -> bool) (n : nat) (x : A),
        p x = true -> takeWhile p (repeat n x) = repeat n x.

Theorem dropWhile_repeat :
    forall (A : Type) (p : A -> bool) (n : nat) (x : A),
        p x = true -> dropWhile p (repeat n x) = [].

Zwijanie


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.

Fixpoint foldl {A B : Type} (f : A -> B -> A) (a : A) (l : list B) : A :=
match l with
    | [] => a
    | h :: t => foldl f (f a h) 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 lub foldl następujące funkcje: length, app, rev, map, join, filter, takeWhile, dropWhile.
Udowodnij, że zdefiniowane przez ciebie funkcje pokrywają się ze swoimi klasycznymi odpowiednikami.


Theorem lengthF_spec : forall (A : Type) (l : list A),
    lengthF l = length l.

Theorem appF_spec : forall (A : Type) (l1 l2 : list A),
    appF l1 l2 = l1 ++ l2.

Theorem revF_spec : forall (A : Type) (l : list A),
    revF l = rev l.


Theorem mapF_spec : forall (A B : Type) (f : A -> B) (l : list A),
    mapF f l = map f l.

Theorem joinF_spec : forall (A : Type) (l : list (list A)),
    joinF l = join l.

Theorem filterF_spec : forall (A : Type) (p : A -> bool) (l : list A),
    filterF p l = filter p l.

Theorem takeWhileF_spec : forall (A : Type) (p : A -> bool) (l : list A),
    takeWhileF p l = takeWhile p l.


Napisz funkcję partition, która dzieli listę l na listy elementów spełniających i niespełniających pewnego warunku boolowskiego.


Theorem partition_spec : forall (A : Type) (p : A -> bool) (l : list A),
    partition p l = (filter p l, filter (fun x => negb (p x)) l).

Napisz funkcję zip : forall A B : Type, list A -> list B -> list (A * B), która spełnia poniższą specyfikację. Co robi ta funkcja?


Theorem zip_length : forall (A B : Type) (la : list A) (lb : list B),
    length (zip la lb) = min (length la) (length lb).

Theorem zip_head :
    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).


This page has been generated by coqdoc