D1k: Arytmetyka Peano, część 2


Require Import Recdef.

From Typonomikon Require Import D1b.

Module MyNat.

Export D1b.MyNat.

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_l :
  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_add_l :
  forall a b c : nat,
    b <= c -> add a b <= add a c.

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

Lemma le_add :
  forall a b c d : nat,
    a <= b -> c <= d -> add a c <= add b d.

Lemma le_sub_S_S :
  forall n m : nat,
    sub n (S m) <= sub n m.

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

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

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

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

Lemma le_mul :
  forall a b c d : nat,
    a <= b -> c <= d -> mul a c <= mul b d.

Lemma le_add_exists :
  forall n m : nat,
    n <= m -> exists k : nat, add 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.

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 sub_le_0 :
  forall n m : nat,
    n <= m -> sub n m = 0.

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

Lemma sub_sub_r' :
  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.

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.


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

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

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

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

Lemma div2_mod2_spec :
  forall n : nat, add (mul 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.

Nieinduktywne predykaty i relacje (TODO)

Podzielność


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

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

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

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

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

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

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

Lemma divides_add :
  forall k n m : nat, divides k n -> divides k m -> divides k (add n m).

Lemma divides_mul_l :
  forall k n m : nat,
    divides k n -> divides k (mul n m).

Lemma divides_mul_r :
  forall k n m : nat,
    divides k m -> divides k (mul n m).

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

Liczby pierwsze (TODO)


Definition prime (p : nat) : Prop :=
  forall k : nat, divides k p -> k = 1 \/ k = p.

Lemma double_not_prime :
  forall n : nat,
    n <> 1 -> ~ prime (mul 2 n).

Definicje induktywne vs definicje nieinduktywne (TODO)


Definition le' (n m : nat) : Prop :=
  exists k : nat, add k n = m.

Lemma le'_le :
  forall n m : nat,
    n <= m -> le' n m.

Lemma le_le' :
  forall n m : nat,
    le' n m -> n <= m.

Inductive divides' (n : nat) : nat -> Prop :=
| divides'_0 : divides' n 0
| divides'_add : forall m : nat, divides' n m -> divides' n (add n m).

Lemma divides_divides' :
  forall n m : nat,
    divides' n m -> divides n m.

Lemma divides'_divides :
  forall n m : nat,
    divides n m -> divides' 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.

Silnia

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


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

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

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

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

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

End MyNat.

Dyskretny pierwiastek kwadratowy (TODO)

TODO: dyskretny pierwiastek kwadratowy

Require Import Lia Arith.

Fixpoint root (n : nat) :=
match n with
| 0 => 0
| S n' =>
    let r := root n' in
      if Nat.ltb n (S r * S r)
      then r
      else S r
end.

Compute root 50.

Lemma root_spec :
  forall (n : nat) (r := root n),
    r * r <= n < (S r) * (S r).
Proof.
  induction n as [| n']; [now cbn; lia |].
  destruct IHn' as [H1 H2].
  cbn [root].
  now destruct (Nat.ltb_spec (S n') (S (root n') * S (root n'))); lia.
Qed.

Lemma le_diag_inv :
  forall n m : nat,
    n * n <= m * m -> n <= m.
Proof.
  intros n m Hle.
  apply Decidable.not_not; [admit |].
  intros Hlt.
  rewrite <- Nat.lt_nge in Hlt.
  assert (m * m < n * n).
  {
    now apply Nat.square_lt_mono_nonneg; [lia |].
  }
  lia.
Admitted.

Lemma lt_diag_inv :
  forall n m : nat,
    n * n < m * m -> n < m.
Proof.
  intros n m Hlt.
  apply Decidable.not_not; [admit |].
  intros Hle.
  rewrite <- Nat.le_ngt in Hle.
  assert (m * m <= n * n).
  {
    now apply Nat.square_le_mono_nonneg; [lia |].
  }
  lia.
Admitted.

Lemma root_spec' :
  forall (n : nat) (r := root (n * n)),
    r = n.
Proof.
  intros n r.
  pose proof (Hspec := root_spec (n * n)).
  assert (Hle : r <= n) by apply le_diag_inv, Hspec.
  assert (Hlt : n < S r) by apply lt_diag_inv, Hspec.
  lia.
Qed.

Zadania

Ćwiczenie (przeszukiwanko)


Section reverse.

Context
  (f : nat -> nat)
  (Hzero : f 0 = 0)
  (Hincreasing : forall m n, m < n -> f m < f n).

Udowodnij, że przy powyższych założeniach dla każdego y : nat istnieje x : nat takie, że f x <= y <= f (S x). Zdefiniuj w tym celu funkcję g : nat -> nat i udowodnij, że spełnia ona specyfikację.


End reverse.