A03 Arytmetyka według Euklidesa (na komputerze)

 

1. Arytmetka Euklidesa

W księgach 7-9 “Elementów”Euklidesa znajdziemy wykład elementarnej teorii liczb. W księdze 7 Euklides wprowadza szereg definicji związanych z liczbami. Nam będzie potrzebna wyłącznie

Definicja 12. Dwie liczby są względnie pierwsze jeśli ich jedynymy wspólnym dzielnikiem jest $1$.

Przyjrzyjmy się dwóm pierwszym stwierdzeniom z księgi 7:

Dla danych dwóch różnych liczb $a,b$ kolejno od większej odejmujemy mniejszą. Wtedy liczby $a,b$ są względnie pierwsze, jeśli w ostatnim kroku algorytmu uzyskujemy jedność (liczbę 1).

Powyższy algorytm znajduje największy wspólny dzielnik $a$ i $b$.

Bardziej precyzyjne sformułowanie mogłoby wyglądać następująco

Stwierdzenie 1 i 2. Dane są dwie liczby $a,b$. Rozważmy następujący algorytm 1

defnwd(a,b):
whilea<>b:
c=max(a,b)
a=min(a,b)
b=c-a
returna

Liczba $nwd(a,b)$ to największy wspólny dzielnik liczb $a$ i $b$. W szczególności, $nwd(a,b)=1$ wtedy i tylko wtedy, gdy $a$ i $b$ są względnie pierwsze.

Proof. Postąpimy w duchu dowodów z księgi 7 i najpierw wykażemy, że jeśli $nwd(a,b)=1$ to $a$ i $b$ są względnie pierwsze. Bez straty ogólności możemy przypuścić, że $a<b$. Niech $c$ będzię wspólnym dzielnikiem $a$ i $b$, $c>1$. Zauważmy, że w każdym kroku algorytmu wewnątrz pętli while liczba $c$ dzieli zarówno $b$ jak i $a$. Istotnie, jeśli $c$ dzieli $a$ i $b$, to $c$ dzieli zarówno $min(a,b)$ jak i $c-a$, które w kolejnym wykonaniu pętli while grają rolę $a$ i $b$. W szczególności w ostatnim kroku pętli while liczba $c$ dzieli $a$, czyli każdy wspólny dzielnik $a$ i $b$ dzieli $nwd(a,b)$. Zatem jeśli $nwd(a,b)=1$, to $c$ dzieli $1$, czyli $c=1$, co oznacza, że $a$ i $b$ są względnie pierwsze.

Z powyższego rozumowania wynika także, że każdy wspólny dzielnik $a$ i $b$ dzieli $nwd(a,b)$. Wykażemy teraz, że liczba $nwd(a,b)$ sama jest dzielnikiem $a$ i $b$, co będzię dowodziło, że $nwd(a,b)$ jest największym dzielnikiem $a$ i $b$. TODO

Rekurencyjny sposób zapisania powyższego programu obliczającego nwd(a,b) mógłby wyglądać następująco

defnwd(a,b):
if(a==0):
returnb
returnnwd(min(a,b),max(a,b)-min(a,b))

Może też być dość wygodne zaangażowanie operacji modulo, czyli dzielenie z resztą. Przykładowo, $12 modulo 7$ daje $5$, podobnie $19 modulo 7$ także daje $5$. Widać zatem, że w algorytmie Euklidesa zamiast systematycznie odejmować liczbę $7$, moglibyśmy w jednym kroku policzyć $n modulo 7$. Wtedy algorytm Euklidesa przedstawiałby się następująco

defnwd(a,b):
if(a==0):
returnb
returnnwd(b%a,a)# % = modulo w Pythonie

Zauważmy, że na to, żeby $nwd(a,b)$ się zatrzymywał musimy coś jeszcze założyć o naszych liczbach naturalnych. Na przykład, że nia ma w nich nieskończonego zstępującego ciągu $a_0 > a_1 > a_2 > \ldots$. Tym samym pętla while/rekurencja nie może zostać wykonana nieskończenie wiele razy, bo liczba $min(a,b)$ w każdym przebiegu pętli się zmniejsza.

Te szczegóły dość dobrze uwidaczniają się w następującym (klikalnym) skrypcie zaczerpniętym zbibliotek języka Coq):

Require Import NPeano. Fixpoint nwd a b := match a with | O => b | S a1 => nwd (b mod (S a1)) (S a1) end. Eval compute in (nwd 10 15).

Proszę poeksperymentować trochę z tym kodem zmieniając liczby 10, 15 na inne. Powyższy formalizm pozwala też na udowodnienie twierdzenia Euklidesa w wersji zrozumiałej dla komputera. Tymczasem przyjrzymy się, jak by takie twierdzenie mogło wyglądać.

Require Import NPeano Lemma nwd_divide : forall a b, (nwd a b | a) /\ (nwd a b | b).

Powyższy lemat mówi, że nwd(a,b) dzieli zarówno a, jak i b. Poniżej sformułujemy analogiczny lemat, który stwierdza, że nwd(a,b) jest największym dzielnikiem.

Require Import NPeano. Lemma nwd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b).

2. Arytmetyka Peano

3. Dygresja- dowody w arytmetyce Peano na komputerze

Poniżej nie tylko formułujemy, ale także dowodzimy stwierdzeń 1 i 2 z siódmej księgi Euklidesa. TODO: wpisać drugie z powyższych stwierdzeń.

Require Import Bool Peano Peano_dec Compare_dec Plus Mult Minus Le Lt EqNat Div2 Wf_nat NAxioms NProperties. Fixpoint nwd a b := match a with | O => b | S a1 => nwd (b mod (S a1)) (S a1) end. Eval compute in (nwd 10 15).
Require Import Bool Peano Peano_dec Compare_dec Plus Mult Minus Le Lt EqNat Div2 Wf_nat NAxioms NProperties. Fixpoint divmod x y q u := match x with | 0 => (q,u) | S x1 => match u with | 0 => divmod x1 y (S q) y | S u1 => divmod x1 y q u1 end end. Definition modulo x y := match y with | 0 => y | S y1 => y1 - snd (divmod x y1 0 y1) end. Infix "mod" := modulo (at level 40, no associativity) : nat_scope. Fixpoint gcd a b := match a with | O => b | S a1 => gcd (b mod (S a1)) (S a1) end. Eval compute in (gcd 10 15). Definition divide x y := exists z, y=z*x. Notation "( x | y )" := (divide x y) (at level 0) : nat_scope. Definition div x y := match y with | 0 => y | S y' => fst (divmod x y' 0 y') end. Infix "/" := div : nat_scope. Infix "mod" := modulo (at level 40, no associativity) : nat_scope. Lemma divmod_spec : forall x y q u, u <= y -> let (q',u') := divmod x y q u in x + (S y)*q + (y-u) = (S y)*q' + (y-u') /\ u' <= y. Proof. induction x. simpl. intuition. intros y q u H. destruct u; simpl divmod. generalize (IHx y (S q) y (le_n y)). destruct divmod as (q',u'). intros (EQ,LE); split; trivial. rewrite <- EQ, <- minus_n_O, minus_diag, <- plus_n_O. now rewrite !plus_Sn_m, plus_n_Sm, <- plus_assoc, mult_n_Sm. generalize (IHx y q u (le_Sn_le _ _ H)). destruct divmod as (q',u'). intros (EQ,LE); split; trivial. rewrite <- EQ. rewrite !plus_Sn_m, plus_n_Sm. f_equal. now apply minus_Sn_m. Qed. Lemma div_mod : forall x y, y<>0 -> x = y*(x/y) + x mod y. Proof. intros x y Hy. destruct y; [ now elim Hy | clear Hy ]. unfold div, modulo. generalize (divmod_spec x y 0 y (le_n y)). destruct divmod as (q,u). intros (U,V). simpl in *. now rewrite <- mult_n_O, minus_diag, <- !plus_n_O in U. Qed. Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b). Proof. fix 1. intros [|a] b; simpl. split. now exists 0. exists 1. simpl. now rewrite <- plus_n_O. fold (b mod (S a)). destruct (gcd_divide (b mod (S a)) (S a)) as (H,H'). set (a':=S a) in *. split; auto. rewrite (div_mod b a') at 2 by discriminate. destruct H as (u,Hu), H' as (v,Hv). rewrite mult_comm. exists ((b/a')*v + u). rewrite mult_plus_distr_r. now rewrite <- mult_assoc, <- Hv, <- Hu. Qed.

Dziala, tylko wyglada okropnie :)

Created with Madoko.net.

1.uruchamialny, zapisany w Pythonie.