###### tags: `MP`
# MP wykład typy i dowodzenie (plait)

### w czym pomagają:
1. Wykrycie błędów

### Wnioskowanie o programach
Dowodzenie, że program spełnia pewne własności

1. na co dzień nieformalnie, ale na nieformalnym poziomie będzie się to regularnie robić
2. żeby robić to na nieformalnym poziomie trzeba być pewnym, że to wnioskowanie jest możliwe do przeprowadzenia formalnie

1. dane mają strukturę
2. programy mają strukturę
3. dowody mają strukturę 
4. najlepiej jak te struktury są takie same / połączone

Na logice używaliśmy przede wszystkim języka polskiego, ale było to "odpowiednikiem" FO.

#### Tutaj będziemy używać FO

1. Świat formuł (własności) : conj, disj, ...
2. Relacje (tutaj nasza relacja "równoważności")
3. Świat obiektów (termy): liczby, zbiory, programy, wyrażenia, wartości

Jakie chcemy mieć własności naszej relacji:
1. Relacja równoważności
* przechodnia
* symetryczna
* zwrotna
2. umożliwiająca przepisywanie równego na równe - kongruencja (tzn jak równe fragmenty podmienię to się nic nie zmienia)
* jeśli e1~e1' oraz e2~e2' to (e1e2)~(e1'e2')
* jeśli e1~e1' oraz e2~e2' oraz e3~e3'to (if e1 e2 e3) ~ (if e1' e2' e3')
* i inne podobne
3. zgodna z naszym modelem obliczeń (podstawowym)
* jak obliczymy fragment to wynik działania programu nie powinien zostać zmieniony
* np jeśli + jest normalny (nie jest zmieniony) to 4 ~ (+ 2 2)
* jeśli e1 oblicza się do e2 to e1 ~ e2
4. rozróżnia rzeczy które oczywiste że są różne
* true !~ false
* ciekawostka: jeśli true !~ false i cała reszta jest spełniona to już nam wystarcza do pokazania, że np 3 !~ 33 (z pzechodniości idzie)

Dlaczego chcemy z taką relacją pracować?
1. jest ogólna => można różne rzeczy robić

## Udowodnijmy coś:

(define (append xs ys)
    (if (empty? xs)
        ys
        (cons (first xs)
            (append (rest xs) ys))))

#### Zakładamy, że zmienne są wartością chyba że wyraźnie powiedziane inaczej

### Lemat 1.
Dla dowolnej listy xs (więc xs jest już wartością) `(append empty xs)` ~ `xs`

#### Dowód
`(append empty xs)` ~ `(if (empty? empty) xs (...))` ~ `(if #t xs (...))` ~ `xs` (to jedyny raz kiedy tak precyzyjnie to robimy)

### Lemat 2.
Dla dowolnej listy xs (więc xs jest już wartością) `(append xs empty)` ~ `xs`

#### Trochę do dowodu:
Tutaj nie jest tak prosto, bo nie wiemy czym jest lista xs i zależnie czy jest pusta czy nie to inne rzeczy się wykonają => INDUKCJA

5 to inaczej next -> N -> N -> N -> 0 czyli takie trochę drzewo

a lista to: val -> val -> val -> ... -> val -> null

Dowodu formalnego nie robimy ale skoro nie ma jakiś cyklicznych czy czegoś to działa indukcja i widzimy że da się dowód zrobić bo lista się kończy.

#### Zasada indukcji dla list:
Niech P będzię własnością list taką, że
1. P(empty)
2. dla każdego x, xs jeśli P(xs) to P((cons x xs))

Wtedy dla dowolnej listy xs zachodzi P(xs).

Na razie zasadę indukcji przyjmujemy trochę na wiarę ale generalnie wyprowadzamy ją zawsze z definicji typu (dla wszystkich konstruktorów co się dzieje).

! tak naprawdę to nie jest FO tylko MSO albo SO ale przypomina FO, więc nie myślmy o tym!

#### Dowód (z użyciem indukcji)
Przez indukcję względem xs:
Niech P(xs) := {(append xs empty) ~ xs}
1. Baza indukcji : P(empty)
(append empty empty) ~ empty z Lematu 1.

2. Krok indukcyjny
Weźmy dowolne x, xs takie, że P(xs), czyli (append xs empty) ~ xs. Pokażmy, że P((cons x xs)).
`tutaj wyliczamy z tego jak append wygląda i wychodzi, było na tablicy (korzystamy z tego, że ~ jest kongruencją)`

### Lemat 3
`(append xs (append ys zs))` ~ `(append (append xs ys) zs)`

#### Plan dowodu

! nie można tak po prostu bo mamy 3 listy i się robią problemy!

Dobimy indukcję po `xs`, ponieważ on jest zawsze w lewej części `append`, więc jesteśmy w stanie coś wtedy zrobić (`append` podąża po strukturze pierwszego argumentu).

Lubimy rekursję strukturalną bo się łatwo o niej wnioskuje (bo indukcja wtedy ładnie działa)

#### Dowód

Indukcja względem xs
1. `(append empty (append ys zs))` ~? `(append (append empty ys) zs)`
`(append empty (append ys zs))`
* Lemat pomocniczy: dla każdych ys, zs istnieje lista v (będąca wartością) taka, że (apppend ys zs) ~ v (nie dowodzimy, z indukcji by poszło)
Zatem z L1 mamy:
lewa strona = (append empty (append ys zs)) ~ (append empty v) ~ v ~ (append ys zs)
prawa strona = (append (append empty ys) zs) ~ (append ys zs)

Stąd P ~ L, co należało pokazać

2. Krok indukcyjny:
Załóżmy, że `(append xs (append ys zs)) `~` (append (append xs ys) zs)`, pokażemy że `(append (cons x xs) (append ys zs)) ~(append (append (cons x xs) ys) zs)`.
Lewa = `(append (cons x xs) (append ys zs))` ~ `(append (cons x xs) v)` ~ (z definicji append) ~`(cons x (append xs v))` ~ `(cons x (append xs (append ys zs)))` ~ (z zał ind) ~ `(cons x (append (append xs ys) zs)`]
Prawa = `(append (append (cons x xs) ys) zs)` ~ `(append (cons x (append xs ys) zs))` ~ `(cons x (append (append xs ys) zs))`, więc P ~ L , co należało pokazać.

#### komentarze:

Rekursja jest fajna bo po tym po czym robimy rekursję robimy dowód indukcyjny i wszystko ładnie działa.

### Reverse:

(define (rev1 xs)
    (if (empty? xs)
        xs
        (append (rev1 (rest xs))
        (cons (first xs) empty))))
 
;"lepsza implementacja":
(define (rev2 xs)
    (rev-app xs empty))
    
(define (rev-app xs ys)
    (if (empty? xs)
        ys
        (rev-app (first xs) ys))) ;coś tu chyba jest nie tak

Czy są równoważne?

#### Lemat 4:
`rev1` ~ `rev2`, czyli bardziej formalnie:
Dla dowolnej listy xs: `(rev1 xs)` ~ `(rev2 xs)`.

##### Próba dowodu:
Indukcyjny:

1. Baza indukcji:
`(rev1 empty)` ~ `(rev2 empty)`
oczywiste, dokładniej nie pokazujemy

2. Krok indukcyjny:
Zakładamy: `(rev1 xs)` ~ `(rev2 xs)`, dowodzimy `(rev1 (cons x xs))` ~ `(rev2 (cons x xs))`.
Wiemy, że:
L ~ `(append (rev1 xs) (cons x empty))` ~ `(append (rev2 xs) (cons x empty))`
P ~ `(rev-app (cons x xs) empty)` ~ `(rev-app xs (cons x epmty) empty)`

Nie wychodzi za bardzo... (da się ale bardzo długo i brzydko wychodzi)

Nie wychodzi ładnie bo o ile `rev1` jest ładnie rekursją zapisany o tyle `rev2` zupełnie nie i indukcja tu nam nic nie da.

Jak to zrobić łatwiej?

#### Lemat 5:

`(rev1 xs)` ~ `(revapp xs empty)`

##### Próba dowodu:

Możnaby to robić indukcyjnie, ale też by było brzydko (w revapp drugi argument się zmienia w każdym przejściu a w rev1 nie)

Może wzmocnijmy twierdzenie:

`(rev1 xs)` ~ `(revapp xs ys)`

Teraz jest problem taki, że to nie jest prawdziwe, zatem trzeba coś zmienić z prawą częścią:

`(append (rev1 xs) ys)` ~ `(revapp xs ys)`

To (jak za chwilę udowodnimy) działa, jak na to wpaść? `???`

#### Dowód:

P(xs) := `(append (rev1 xs) ys)` ~ `(revapp xs ys)`
1. Baza indukcji:
L ~ ys ~ P (triv)
2. Krok indukcyjny:
Zakładamy dla każdego x, xs, ys: `(append (rev1 xs) ys)` ~ `(revapp xs ys)`, pokażmy że
`(append (rev1 (cons x xs)) ys)` ~ `(revapp (cons x xs) ys)`.
L = `(append (rev1 (cons x xs)) ys)` ~ `(append (append (rev1 xs) (cons x empty)) ys)` ~ `(append (rev1 xs) (append (cons x empty) ys))` ~ `(append (rev1 xs) (cons x ys))` ~ (zał. ind) ~ `(revapp xs (cons x ys))` ~ (def. revapp) ~ `(revapp (cons x xs) ys)` = P, co mieliśmy pokazać.

#### Dowód L4: (krok indukcyjny)

Z lematu 5 mamy:

`(append (rev1 xs) (cons x empty))` ~ `(revapp xs (cons x empty))`

Zatem:

L = `(rev1 (cons x xs))` ~ (z def. rev1) ~ `(append (rev1 xs) (cons x empty))` ~ (L5) ~ `(revapp xs (cons x empty))`

P = `(rev2 (cons x xs))` ~ (z def. rev2) ~ `(revapp (cons x xs) empty)` ~
(z def. revapp) ~ `(rev-app x ys)`

Coś by się dało dalej, ale definicja funkcji coś się nie zgadza, więc no...

### Jak robić zasadę indukcji dla innych typów danych?

#### Bool

Myślimy o boolu jako typie algebraicznym z dwoma konstruktorami: `#t` i `#f`.

Zasada indukcji:
Niech P będzie własnością wartości boolowskich taką, że:
1. `P(#f)`
2. `P(#t)`

Wówczas dla każdego boola `b` zachodzi `P(b)`.

Stąd mamy, że dla booli, żeby coś udowodnić wystarczy rozpatrzeć 2 przypadki.

#### Drzewa binarne

Zasada indukcji:
Niech `P` będzie własnością taką, że:
1. `P((leaf))`
2. Dla każdego `l`, `x`, `r` jeśli `P(l)` i `P(r)` to `P((node l x p))`

Wówczas dla każdego drzewa binarnego `t` zachodzi `P(t)`.

#### Drzewa różane:

Nasza definicja:

(define-type (T 'a)
    (node (elem 'a)
        (children (Listof (T 'a)))))

Zasada indukcji:
Niech `P`, będzie własnością taką, że:
1. Dla każdego `x`, `ts` jeśli dla każdego `t` będącego elementem `(node-children ts)` zachodzi `P(t)` mamy `P(ts)`.

Driga wersja: (zasada wzajemnej indukcji)
Niech `P`, `Q`, będzie własnością taką, że:
1. Dla każdego `x`, `ts` jeśli `Q(ts)` to `P((node x ts))`.
2. dla każdego `t`, `ts` jeśli `P(t)` i `Q(ts)` to `Q((cons t, ts))`