D1b: Arytmetyka Peano
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.
Require Import Setoid.
Require ZArith.
Module MyNat.
Podstawy
Definicja i notacje
Zdefiniuj liczby naturalne.
Notation "0" := O.
Notation "1" := (S 0).
Notation "2" := (S (S 0)).
0 i S
Udowodnij właściwości zera i następnika.
Lemma neq_0_Sn :
forall n : nat, 0 <> S n.
Lemma neq_n_Sn :
forall n : nat, n <> S n.
Lemma not_eq_S :
forall n m : nat, n <> m -> S n <> S m.
Lemma S_injective :
forall n m : nat, S n = S m -> n = m.
Poprzednik
Zdefiniuj funkcję zwracającą poprzednik danej liczby naturalnej.
Poprzednikiem
0 jest
0.
Lemma pred_0 : pred 0 = 0.
Lemma pred_S :
forall n : nat, pred (S n) = n.
Proste działania
Dodawanie
Zdefiniuj dodawanie (rekurencyjnie po pierwszym argumencie) i
udowodnij jego właściwości.
Lemma add_0_l :
forall n : nat, add 0 n = n.
Lemma add_0_r :
forall n : nat, add n 0 = n.
Lemma add_S_l :
forall n m : nat, add (S n) m = S (add n m).
Lemma add_S_r :
forall n m : nat, add n (S m) = S (add n m).
Lemma add_assoc :
forall a b c : nat,
add a (add b c) = add (add a b) c.
Lemma add_comm :
forall n m : nat, add n m = add m n.
Lemma add_no_absorbing_l :
~ exists a : nat, forall n : nat, add a n = a.
Lemma add_no_absorbing_r :
~ exists a : nat, forall n : nat, add n a = a.
Lemma add_no_inverse_l :
~ forall n : nat, exists i : nat, add i n = 0.
Lemma add_no_inverse_r :
~ forall n : nat, exists i : nat, add n i = 0.
Lemma add_no_inverse_l_strong :
forall n i : nat, n <> 0 -> add i n <> 0.
Lemma add_no_inverse_r_strong :
forall n i : nat, n <> 0 -> add n i <> 0.
Alternatywne definicje dodawania
Udowodnij, że poniższe alternatywne metody zdefiniowania dodawania
rzeczywiście definiują dodawanie.
Fixpoint add' (n m : nat) : nat :=
match m with
| 0 => n
| S m' => S (add' n m')
end.
Lemma add'_is_add :
forall n m : nat, add' n m = add n m.
Fixpoint add'' (n m : nat) : nat :=
match n with
| 0 => m
| S n' => add'' n' (S m)
end.
Lemma add''_is_add :
forall n m : nat, add'' n m = add n m.
Fixpoint add''' (n m : nat) : nat :=
match m with
| 0 => n
| S m' => add''' (S n) m'
end.
Lemma add'''_is_add :
forall n m : nat, add''' n m = add n m.
Odejmowanie
Zdefiniuj odejmowanie i udowodnij jego właściwości.
Lemma sub_1_r :
forall n : nat, sub n 1 = pred n.
Lemma sub_0_l :
forall n : nat, sub 0 n = 0.
Lemma sub_0_r :
forall n : nat, sub n 0 = n.
Lemma sub_S_S :
forall n m : nat,
sub (S n) (S m) = sub n m.
Lemma sub_diag:
forall n : nat, sub n n = 0.
Lemma sub_add_l :
forall n m : nat,
sub (add n m) n = m.
Lemma sub_add_l' :
forall n m : nat,
sub (add n m) m = n.
Lemma sub_add_r :
forall a b c : nat,
sub a (add b c) = sub (sub a b) c.
Lemma sub_exchange :
forall a b c : nat,
sub (sub a b) c = sub (sub a c) b.
Lemma sub_not_assoc :
~ forall a b c : nat,
sub a (sub b c) = sub (sub a b) c.
Lemma sub_not_comm :
~ forall n m : nat,
sub n m = sub m n.
Lemma sub_comm_char :
forall n m : nat,
sub n m = sub m n -> n = m.
Alternatywna definicja odejmowania
Fixpoint sub' (n m : nat) : nat :=
match m with
| 0 => n
| S m' => pred (sub' n m')
end.
Lemma sub'_1_r :
forall n : nat, sub' n 1 = pred n.
Lemma sub'_pred_l :
forall n m : nat,
sub' (pred n) m = pred (sub' n m).
Lemma sub'_0_l :
forall n : nat,
sub' 0 n = 0.
Lemma sub'_0_r :
forall n : nat,
sub' n 0 = n.
Lemma sub'_S_S :
forall n m : nat,
sub' (S n) (S m) = sub' n m.
Lemma pred_sub'_S :
forall n m : nat,
pred (sub' (S n) m) = sub' n m.
Lemma sub'_diag :
forall n : nat,
sub' n n = 0.
Lemma sub'_add_l :
forall n m : nat,
sub' (add n m) n = m.
Lemma sub'_add_l' :
forall n m : nat,
sub' (add n m) m = n.
Lemma sub'_add_r :
forall a b c : nat,
sub' a (add b c) = sub' (sub' a b) c.
Lemma sub'_exchange :
forall a b c : nat,
sub' (sub' a b) c = sub' (sub' a c) b.
Lemma sub'_not_assoc :
~ forall a b c : nat,
sub' a (sub' b c) = sub' (sub' a b) c.
Lemma sub'_not_comm :
~ forall n m : nat,
sub' n m = sub' m n.
Lemma sub_sub' :
forall n m : nat,
sub n m = sub' n m.
Mnożenie
Zdefiniuj mnożenie i udowodnij jego właściwości.
Lemma mul_0_l :
forall n : nat,
mul 0 n = 0.
Lemma mul_0_r :
forall n : nat,
mul n 0 = 0.
Lemma mul_1_l :
forall n : nat,
mul 1 n = n.
Lemma mul_1_r :
forall n : nat,
mul n 1 = n.
Lemma mul_comm :
forall n m : nat,
mul n m = mul m n.
Lemma mul_add_l :
forall a b c : nat,
mul (add a b) c = add (mul a c) (mul b c).
Lemma mul_sub_r :
forall a b c : nat,
mul a (sub b c) = sub (mul a b) (mul a c).
Lemma mul_sub_l :
forall a b c : nat,
mul (sub a b) c = sub (mul a c) (mul b c).
Lemma mul_assoc :
forall a b c : nat,
mul a (mul b c) = mul (mul a b) c.
Lemma mul_no_inverse_l :
~ forall n : nat, exists i : nat, mul i n = 1.
Lemma mul_no_inverse_r :
~ forall n : nat, exists i : nat, mul n i = 1.
Lemma mul_no_inverse_l_strong :
forall n i : nat, n <> 1 -> mul i n <> 1.
Lemma mul_no_inverse_r_strong :
forall n i : nat, n <> 1 -> mul n i <> 1.
Lemma mul_1_inv :
forall n m : nat,
mul n m = 1 -> n = 1 /\ m = 1.
Lemma mul_2_l :
forall n : nat, mul 2 n = add n n.
Alternatywna definicja mnożenia
Fixpoint mul' (n m : nat) : nat :=
match n with
| 0 => 0
| S n' => add (mul' n' m) m
end.
Ta definicja ma tę przyjemną właściwość, że lewostronne mnożenie przez 1
oblicza się do n, a nie do n + 0.
Lemma mul'_1_l :
forall n : nat, mul' 1 n = n.
Proof.
reflexivity.
Qed.
Lemma mul'_spec :
forall n m : nat,
mul' n m = mul n m.
Proof.
induction n as [| n']; cbn; intros; [easy |].
now rewrite IHn', add_comm.
Qed.
Potęgowanie
Zdefiniuj potęgowanie i udowodnij jego właściwości.
Lemma pow_0_r :
forall n : nat,
pow n 0 = 1.
Lemma pow_0_l :
forall n : nat,
pow 0 (S n) = 0.
Lemma pow_1_l :
forall n : nat,
pow 1 n = 1.
Lemma pow_1_r :
forall n : nat,
pow n 1 = n.
Lemma pow_no_neutr_l :
~ exists e : nat, forall n : nat, pow e n = n.
Lemma pow_no_absorbing_r :
~ exists a : nat, forall n : nat, pow n a = a.
Lemma pow_add :
forall a b c : nat,
pow a (add b c) = mul (pow a b) (pow a c).
Lemma pow_mul_l :
forall a b c : nat,
pow (mul a b) c = mul (pow a c) (pow b c).
Lemma pow_pow_l :
forall a b c : nat,
pow (pow a b) c = pow a (mul b c).
Minimum i maksimum
Zdefiniuj operacje brania minimum i maksimum z dwóch liczb naturalnych
oraz udowodnij ich właściwości.
Lemma min_0_l :
forall n : nat, min 0 n = 0.
Lemma min_0_r :
forall n : nat, min n 0 = 0.
Lemma max_0_l :
forall n : nat, max 0 n = n.
Lemma max_0_r :
forall n : nat, max n 0 = n.
Lemma min_assoc :
forall a b c : nat,
min a (min b c) = min (min a b) c.
Lemma max_assoc :
forall a b c : nat,
max a (max b c) = max (max a b) c.
Lemma min_comm :
forall n m : nat, min n m = min m n.
Lemma max_comm :
forall n m : nat, max n m = max m n.
Lemma min_refl :
forall n : nat, min n n = n.
Lemma max_refl :
forall n : nat, max n n = n.
Lemma min_no_neutr_l :
~ exists e : nat, forall n : nat, min e n = n.
Lemma min_no_neutr_r :
~ exists e : nat, forall n : nat, min n e = n.
Lemma max_no_absorbing_l :
~ exists a : nat, forall n : nat, max a n = a.
Lemma max_no_absorbing_r :
~ exists a : nat, forall n : nat, max n a = a.
Lemma 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)).
Współczynnik dwumianowy (TODO)
Zdefiniuj współczynnik dwumianowy. Jeżeli nie wiesz co to, to dobrze:
będziesz miał więcej zabawy. W skrócie
binom n k to ilość podzbiorów
zbioru
n elementowego, którego mają
k elementów.
Lemma binom_0_r :
forall n : nat,
binom n 0 = 1.
Lemma binom_0_l :
forall n : nat,
binom 0 (S n) = 0.
Lemma binom_1_r :
forall n : nat,
binom n 1 = n.
Lemma binom_eq_SS :
forall n k : nat,
binom (S n) (S k) = add (binom n k) (binom n (S k)).
Lemma binom_add_r :
forall n k : nat,
binom n (add (S n) k) = 0.
Lemma binom_diag :
forall n : nat,
binom n n = 1.
Lemma binom_sym :
forall n k : nat,
binom (add n k) n = binom (add n k) k.
Lemma binom_S_S :
forall n k : nat,
mul (S k) (binom (S n) (S k)) = mul (S n) (binom n k).
Wzory rekurencyjne (TODO)
Sumy szeregów (TODO)
Ćwiczenie
Udowodnij, że
2^0 + 2^1 + 2^2 + ... + 2^n = 2^(n + 1) - 1.
Zaimplementuj w tym celu celu funkcję
f, która oblicza lewą
stronę tego równania, a następnie pokaż, że
f n = 2^(n + 1) - 1
dla dowolnego
n : nat.
Lemma twos_spec :
forall n : nat, twos n = sub (pow 2 (S n)) 1.
Ćwiczenie
Udowodnij, że
2 * (1 + 2 + 3 + ... + n) = n * (n + 1).
Zaimplementuj w tym celu funkcję
sum_first.
Lemma sum_first_spec :
forall n : nat,
mul 2 (sum_first n) = mul n (S n).
End MyNat.