A02 Zrób własne liczby naturalne (na komputerze)

 

1. Formalizowanie arytmetyki

Współczesne systemy opisujące działania na liczbach naturalnych wywodzą się z prac Giuseppe Peano z drugiej połowy 19-tego wieku. Język arytmetyki docelowo powinien obejmować symbol reprezentujący zero oraz takie symbole jak $+$ (reprezentujący dodawanie) i $\cdot$ (reprezentujący mnożenie) z ich interpretacją znaną Państwu ze szkoły średniej. Zaczniemy jednak od nieco prostszego języka, gdzie do dyspozycji jest jedynie zero oraz symbol $S$ oznaczający następnik liczby naturanej, na przykład $S(5) = 6$.

System aksjomatów Peano można zdefiniować następująco:

  1. $0$ jest liczbą naturalną,
  2. dla każdych liczb $n,m$ zachodzi $n=m$ wtedy i tylko wtedy, gdy $S(n)=S(m)$,
  3. dla każdej liczby naturalnej $n$ zachodzi $S(n)\neq 0$,
  4. jeśli $\phi$ opisuje własność liczb naturalnych taką, że $\phi(0)$ oraz $\phi(n)\to \phi(n+1)$, to $\phi(n)$ zachodzi dla wszystkich liczb naturalnych.

Zależnie od przyjętych umów, ten prostszy system “arytmetyki z następnikiem”może pozwolić na wyrażenie $+$ i $\cdot$ i udowodnienie podstawowych twierdzeń arytmetycznych, jak na przykład

(1)
\[\forall_{a,b,c} a(b+c) = ab+ac.
\]

Posłużymy się jako ilustracją podejściem z książki “Software Foundations”

Inductive naturalne : Type := | O : naturalne | S : naturalne -> naturalne.

W tym ujęciu

  • $O$ (litera $O$, jak w imieniu Olgierd) jest liczbą naturalną i
  • $S$ jest “konstrukturem” liczb naturalnych, to znaczy $S$ zaaplikowane do liczby naturalnej daje liczbę naturalną.
  • gwarantowane jest istnienie nieskonczenie wielu liczby naturalnych; są to liczby postaci $O$, $S(O)$, $S(S(O))$ i tak dalej.

Innymi słowy, znane ze szkoły liczby naturalne identyfikujemy z coraz dłuższymi napisami złożonymi z odpowiednio dobranych nawiasów, liter $S$ i jednej litery $O$. Oczywiście można byłoby zacząć od innych liter, niż $S$ i $O$, także użyć nieco bardziej skompresowanych reprezentacji - powyżej używamy w przybliżeniu $2n$ znaków do zaprezentowania liczby $n$, natomiast pisanie w systemie dwójkowym lub dziesiętnym dawałoby logarytmiczną liczbę znaków względem $n$. Te ulepszenia liczb naturalnych zostawiamy sobie na przyszłość, gdyż w tym momencie stawiamy na to, żeby skonstruować arytmetykę od zera.

2. Funkcja $n-2$

Zdefiniujemy teraz funkcję odejmująca liczbę $S (S(O))$ (grająca rolę 2) od danej liczby naturalnej.

Inductive naturalne : Type := | O : naturalne | S : naturalne -> naturalne. (* poniższa definicja rozpatruje trzy przypadki - gdy n = O - wtedy odejmowanie zwraca O, gdyz nie mamy do dyspozycji liczb ujemnych - gdy n = S O - wtedy takze odejmowanie zwraca O, gdyz nie mamy liczb ujemnych *) Definition minusdwa (n : naturalne) : naturalne := match n with | O => O | S O => O | S (S n') => n' end. Check S (S O). Check S ( S (S O) ). Eval compute in (minusdwa ( S ( S (S O) ))).

Proszę zmienić linijkę z Eval i spróbować odjąć $2$ od innych liczb. Mam nadzieję, że widać na tym przykładzie, że $O, S(O), S(S(O)), \ldots$ zachowują się jak $0,1,2,\ldots$, przynajmniej w tym znaczeniu, że można na nich zdefiniować operacje $n\to n-2$. Przyjrzyjmy się teraz definicji dodawania.

3. Dodawanie na liczbach naturalnych

Inductive naturalne : Type := | O : naturalne | S : naturalne -> naturalne. Fixpoint plus (n : naturalne) (m : naturalne) : naturalne := match n with | O => m | S n' => S (plus n' m) end. Eval compute in (plus (S (S (S O))) (S (S O))).

W tym konkretnym przypadku dodajemy $S (S (S (O)))$ i $S (S (O))$, czyli $3$ i $2$ i istotnie wynik wygląda jak $5$.
Proszę trochę poeksperymentować z tą definicją i spróbować dodać do siebie inne liczby. Zarówno funkcja minusdwa jak i plus mają indukcyjne definicje. To jest ważne nie tylko w defijnicji, ale także będzie miało odzwierciedlenie w dowodach poniżej, które także odwołują się do indukcji.

Spróbujmy teraz udowodnić, że w naszym systemie liczb naturalnych $3+2 = 2+3$.

Inductive naturalne : Type := | O : naturalne | S : naturalne -> naturalne. Fixpoint plus (n : naturalne) (m : naturalne) : naturalne := match n with | O => m | S n' => S (plus n' m) end. Theorem trzy_plus_dwa: plus (S (S (S (O)))) (S (S (O))) = plus (S (S (O))) (S (S (S (O)))). Proof. (* zachecamy komputer, zeby rozwinal definicje funkcji plus *) unfold plus. (* korzystamy z faktu, ze w pojeciu komputera, jesli napis po lewej stronie jest dokladnie rowny napisowi po prawej, to istotnie mamy rownosc *) trivial. Qed. 

4. Dalsze własności dodawania

Dążymy do dowodu, że nasz plus jest przemienny, czyli $n+m = m+n$. W sformalizowanym języku będzie to wyglądało następująco:

Inductive naturalne : Type := | O : naturalne | S : naturalne -> naturalne. Fixpoint plus (n : naturalne) (m : naturalne) : naturalne := match n with | O => m | S n' => S (plus n' m) end. Theorem plus_przemienny: forall (n m:naturalne) plus n m = plus m n.

O dziwo, to twierdzenie wymaga pewnego wysiłku. Dowód rozbijemy na cztery kroki, z których dwa łatwiejsze zostaną wyodrębnione jako ćwiczenia.

Inductive naturalne : Type := | O : naturalne | S : naturalne -> naturalne. Fixpoint plus (n : naturalne) (m : naturalne) : naturalne := match n with | O => m | S n' => S (plus n' m) end. (* pierwszy lemat mówi o tym, że n = n + 0 *) Lemma plus_zero_prawy: forall (n : naturalne), n = plus n O. Proof. intros. induction n. unfold plus. reflexivity. (* krok indukcyjny - prosze zwrocic uwage na cwane wykorzystanie taktyki simpl *) simpl. (* uzywamy hipotezy indukcyjnej zeby nieco uproscic nasze wyrazenie *) rewrite <- IHn. reflexivity. Qed. (* okazuje się, że jest to trochę coś innego, niż n = n + 0 *) Lemma plus_zero_lewy: forall (n : naturalne), n = plus O n. Proof. intros. induction n. (* krok bazowy - do uzupełnienia w zadaniu domowym *) (* krok indukcyjny - do uzupełnienia w zadaniu domowym *) (* magiczne słowo Admitted oznacza, że komputer będzie od tej pory przyjmował ten lemat za udowodniony nawet jeśli na razie nie podaliśmy dowodu *) Admitted. Qed. (* potrzebujemy jeszcze jednego lematu mówiącego, że (n + m) + 1 = n + (m + 1) *) Lemma plus_n_Sm : forall n m : naturalne, S (plus n m) = plus n (S m). Proof. intros. induction n. (* krok bazowy *) unfold plus. reflexivity. (* krok bazowy *) simpl. rewrite <- IHn. reflexivity. Qed. (* w tym miejscu jesteśmy gotowi udowodnić twierdzenie, że n + m = m + n zostawiam to jako zadanie; w domyśle należy posłużyć się trzema powyższymi lematami, przykładowe użycie lematu to rewrite <- plus_zero_lewy. otrzymując takie polecenie komputer usiłuje zastosować równość udowodnioną w lemacie plus_zero_lewy do aktualnego równania; wystarczy posłużyć się simpl, rewrite, reflexivity oraz trzema lematami *) Theorem plus_przemienny: forall (n m:naturalne), plus n m = plus m n. Proof. intros. induction n. (* w tym miejscu komputer automatycznie rozbija dowod na dwa przypadki *) (* krok bazowy - do zrobienia w ramach pracy domowej *) (* krok indukcyjny - do zrobienia w ramach pracy domowej *) Qed. 
Created with Madoko.net.