D4: Arytmetyka



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.

Podstawy

Definicja i notacje

Zdefiniuj liczby naturalne.


Notation "0" := O.
Notation "1" := (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_Sn :
  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 plus_0_l :
  forall n : nat, plus 0 n = n.

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

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

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

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

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

Lemma plus_no_annihilation_l :
  ~ exists a : nat, forall n : nat, plus a n = a.

Lemma plus_no_annihilation_r :
  ~ exists a : nat, forall n : nat, plus n a = a.

Lemma plus_no_inverse_l :
  ~ forall n : nat, exists i : nat, plus i n = 0.

Lemma plus_no_inverse_r :
  ~ forall n : nat, exists i : nat, plus n i = 0.

Lemma plus_no_inverse_l_strong :
  forall n i : nat, n <> 0 -> plus i n <> 0.

Lemma plus_no_inverse_r_strong :
  forall n i : nat, n <> 0 -> plus n i <> 0.

Alternatywne definicje dodawania

Udowodnij, że poniższe alternatywne metody zdefiniowania dodawania rzeczywiście definiują dodawanie.

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

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

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

Lemma 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' => plus''' (S n) m'
end.

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

Odejmowanie

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


Lemma minus_1_r :
  forall n : nat, minus n 1 = pred n.

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

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

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

Lemma minus_diag:
  forall n : nat, minus n n = 0.

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

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

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

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

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

Odejmowanie v2


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_pred_r :
  forall n m : nat,
    sub n (pred m) = sub n m.
(* begin hide *)
Proof.
  intros n m. revert n.
  induction m as | m'; cbn; intros.
    reflexivity.
    rewrite <- IHm' at 2.
    inducti
    rewrite <- sub_pred_l.
    rewrite IHm'. reflexivity.
Qed.
(* end hide *)
 *)

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_plus_l :
  forall n m : nat,
    sub (plus n m) n = m.

Lemma sub_plus_r :
  forall n m : nat,
    sub (plus n m) m = n.

Lemma sub_plus_distr :
  forall a b c : nat,
    sub a (plus 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.

Mnożenie

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


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

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

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

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

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

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

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

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

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

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

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

Lemma mult_no_inverse_l_strong :
  forall n i : nat, n <> 1 -> mult i n <> 1.

Lemma mult_no_inverse_r_strong :
  forall n i : nat, n <> 1 -> mult n i <> 1.

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

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_annihilator_r :
  ~ exists a : nat, forall n : nat, pow n a = a.

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

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

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

Porządek

Porządek <=

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lemma sub_0 :
  forall n m : nat,
    sub n m = 0 -> n <= m.

Lemma sub_S_l :
  forall n m : nat,
    m <= n -> sub (S n) m = S (sub n m).

Lemma le_sub_l :
  forall n m : nat,
    sub n m <= n.

Lemma sub_inv :
  forall n m : nat,
    m <= n -> sub n (sub n m) = m.

Porządek <


Definition lt (n m : nat) : Prop := S n <= m.

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

Lemma lt_irrefl :
  forall n : nat, ~ n < n.

Lemma lt_trans :
  forall a b c : nat, a < b -> b < c -> a < c.

Lemma lt_asym :
  forall n m : nat, n < m -> ~ m < n.

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_le :
  forall n m : nat, n <= m -> min n m = n.

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

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_annihilator_l :
  ~ exists a : nat, forall n : nat, max a n = a.

Lemma max_no_annihilator_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)).

Rozstrzygalność

Rozstrzygalność porządku

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


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

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

Rozstrzygalność równości

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


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

Dzielenie i podzielność

Dzielenie przez 2

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 nat_ind_2
  (P : nat -> Prop) (H0 : P 0) (H1 : P 1)
  (HSS : forall n : nat, P n -> P (S (S n))) (n : nat) : P n.

Zdefiniuj dzielenie całkowitoliczbowe przez 2 oraz funkcję obliczającą resztę z dzielenia przez 2.


Notation "2" := (S (S 0)).

Lemma div2_even :
  forall n : nat, div2 (mult 2 n) = n.

Lemma div2_odd :
  forall n : nat, div2 (S (mult 2 n)) = n.

Lemma mod2_even :
  forall n : nat, mod2 (mult 2 n) = 0.

Lemma mod2_odd :
  forall n : nat, mod2 (S (mult 2 n)) = 1.

Lemma div2_mod2_spec :
  forall n : nat, plus (mult 2 (div2 n)) (mod2 n) = n.

Lemma div2_le :
  forall n : nat, div2 n <= n.

Lemma div2_pres_le :
  forall n m : nat, n <= m -> div2 n <= div2 m.

Lemma mod2_le :
  forall n : nat, mod2 n <= n.

Lemma mod2_not_pres_e :
  exists n m : nat, n <= m /\ mod2 m <= mod2 n.

Lemma div2_lt :
  forall n : nat,
    0 <> n -> div2 n < n.

Podzielność


Module divides.

Definition divides (k n : nat) : Prop :=
  exists m : nat, mult k m = n.

Notation "k | n" := (divides k n) (at level 40).

k dzieli n jeżeli n jest wielokrotnością k. Udowodnij podstawowe właściwości tej relacji.

Lemma divides_0 :
  forall n : nat, n | 0.

Lemma not_divides_0 :
  forall n : nat, n <> 0 -> ~ 0 | n.

Lemma divides_1 :
  forall n : nat, 1 | n.

Lemma divides_refl :
  forall n : nat, n | n.

Lemma divides_trans :
  forall k n m : nat, k | n -> n | m -> k | m.

Lemma divides_plus :
  forall k n m : nat, k | n -> k | m -> k | plus n m.

Lemma divides_mult_l :
  forall k n m : nat, k | n -> k | mult n m.

Lemma divides_mult_r :
  forall k n m : nat, k | m -> k | mult n m.

Lemma divides_le :
  ~ forall k n : nat, k | n -> k <= n.


End divides.

Silnia

Zdefiniuj silnię.
Przykład: fac 5 = 1 * 2 * 3 * 4 * 5 = 120


Lemma le_1_fac :
  forall n : nat, 1 <= fac n.

Require Import Setoid.

Lemma le_lin_fac :
  forall n : nat, n <= fac n.

Fixpoint pow2 (n : nat) : nat :=
match n with
    | 0 => 1
    | S n' => mult 2 (pow2 n')
end.

Notation "4" := (S (S (S (S 0)))).

Lemma le_exp_fac :
  forall n : nat, 4 <= n -> pow2 n <= fac n.

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.

Require Import Recdef.


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

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_gt :
  forall n k : nat, n < k -> binom n k = 0.

Lemma binom_diag :
  forall n : nat, binom n n = 1.

Lemma binom_sym :
  forall n k : nat,
    k <= n -> binom n k = binom n (sub n k).

Lemma minus_sub :
  forall n m : nat,
    minus n m = sub n m.

Lemma binom_sym' :
  forall n k : nat,
    k <= n -> binom n k = binom n (minus n k).

Function binom' (n k : nat) : nat :=
match k with
    | 0 => 1
    | S k' =>
        match n with
            | 0 => 0
            | S n' => plus (binom' n' k') (binom' n' k)
        end
end.

Lemma binom_S_S :
  forall n k : nat,
    mult (S k) (binom (S n) (S k)) = mult (S n) (binom n k).

Lemma binom_spec :
  forall n k : nat,
    k <= n -> mult (fac k) (mult (fac (sub n k)) (binom n k)) = fac n.


Wzory rekurencyjne (TODO)

Sumy szeregów (TODO)

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 = minus (pow2 (S n)) 1.


End MyNat.

Dyskretny pierwiastek kwadratowy (TODO)