# Metody Programowania | Lista 6

## Zadanie 1

Przypomnij sobie definicję funkcji map. Następnie pokaż, że dla dowolnych funkcji
`f` i `g` oraz listy `xs` zachodzi `(map f (map g xs))` ≡ `(map (lambda (x) (f (g x)))xs)`. Możesz założyć, że funkcje `f` i `g` poprawnie obliczają się do wartości dla
dowolnego argumentu.

### Dowód

#### Definicja funkcji map

(define (map f xs)
  (if (empty? xs)
      xs
      (cons (f (first xs)) (map f (rest xs)))))

Przeprowadźmy dowód indukcyjnie względem `xs`.
`P(xs)` := `(map f (map g xs))` ≡ `(map (lambda (x) (f (g x))) xs)`

1. Podstawa indukcji:
L = `(map f (map g xs))` ≡ `(map f (map g empty))` ≡ `(map f (map g empty))` ≡
`(map f empty)` ≡ `empty`

P = `(map (lambda (x) (f (g x))) xs)` ≡ `(map (lambda (x) (f (g x))) empty)` ≡ `empty'
2. Krok indukcyjny:
Załóżmy, że `(map f (map g xs))` ≡ `(map (lambda (x) (f (g x))) xs)`. Pokażemy
`(map f (map g (cons x xs)))` ≡ `(map (lambda (x) (f (g x))) (cons x xs))`.

L = `(map f (map g (cons x xs)))` ≡ `(map f (cons (g x) (map g xs)))` ≡
`(map f (cons (g x) (map g xs)))` ≡ `(cons (f (g x)) (map f ((map g xs)))` ≡
`(cons (f (g x)) (map (lambda (x) (f (g x))) xs))`

P = `(map (lambda (x) (f (g x))) (cons x xs))` ≡
`(cons (lambda (x) (f (g x)) x) (map (lambda (x) (f (g x))) xs))` ≡
`(cons (f (g x)) (map (lambda (x) (f (g x))) xs))` = L

Zatem dla dowolnej listy xs zachodzi P(xs).

## Zadanie 2

Pokaż, że funkcja `append` zawsze oblicza się do wartości, tzn. pokaż, że dla dowolnych list `xs` i `ys` istnieje lista `zs` taka, że `(append xs ys) ≡ zs`.

### Dowód

#### Definicja funkcji append

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

Weźmy dowolne listy `xs` i `ys`. Udowodnijmy przez indukcyję względem `xs`, że `(append xs ys)` oblicza się do wartości.

1. Baza indukcji
Jeśli `xs` jest `empty` to: `(append xs ys)` ≡ `(append empty ys)` ≡ (Lemat 1 z wykładu) ≡ `ys`, co jest wartością.

2. Krok indukcyjny
Załóżmy, że istnieje `zs` ≡ `(append xs ys)`, pokażemy, że istnieje `ts` ≡ `(append (cons x xs) ys)`.
`(append (cons x xs) ys)` ≡ `(cons x (append xs ys))` ≡ (zal. ind.) ≡ `(cons x zs)`. Skoro `(cons a as)` jest wartością to udowodniliśmy, że dla dowolonych `xs`, `ys` `(append xs ys)` oblicza się do wartości.

## Zadanie 3

Formuły w negacyjnej postaci normalnej to takie formuły rachunku zdań, w których wszystkie negacje znajdują się przy zmiennych zdaniowych. Dokładniej, formuły w negacyjnej postaci normalnej, składają się z koniunkcji, alternatywy i literałów, gdzie literały to zanegowane lub niezanegowane zmienne zdaniowe. Takie formuły można opisać następującym typem danych, sparametryzowanym typem opisującym zmienne.

( define-type ( NNF 'v )
    ( nnf-lit [ polarity : Boolean ] [ var : 'v ])
    ( nnf-conj [ l : ( NNF 'v ) ] [ r : ( NNF 'v ) ])
    ( nnf-disj [ l : ( NNF 'v ) ] [ r : ( NNF 'v ) ]) )

Flaga polarity w konstruktorze literału oznacza, czy zmienna jest zanegowana (wartość #f), czy nie (wartość #t). Sformułuj zasadę indukcji dla typu NNF.

### Zasada indukcji

Niech `nnf` będzie formułą w `NNF` i niech `P` będzie własnościa taką, że:
1. Dla każdego `var` zachodzi:
* `P((nnf #t var))`
* `P((nnf #f var))`
2. Dla każdego `l`, `r` (będących formułami nnf) jeśli `P(l)` i `P(r)` to `P((nnf-conj l r))`
3. Dla każdego `l`, `r` (będących formułami nnf) jeśli `P(l)` i `P(r)` to `P((nnf-disj l r))`

Wówczas dla każdej formuły `nnf` typu `NNF` zachodzi `P(nnf)`.

## Zadanie 4

Zdefiniuj funkcję `neg-nnf` typu `((NNF 'a) -> (NNF 'a))` negującą formułę w negacyjnej postaci normalnej. Następnie pokaż, że `(neg-nnf (neg-nnf φ))` ≡ `φ` dla dowolnej formuły `φ`.

### Dowód

#### Definicja funkcji neg-nnf

(define (neg-nnf formula)
  (cond
    [(nnf-lit? formula) (if (equal? (nnf-lit-polarity formula) #t)
                      (nnf-lit #f (nnf-lit-var formula))
                      (nnf-lit #t (nnf-lit-var formula)))]
    [(nnf-conj? formula) (nnf-disj (neg-nnf (nnf-conj-l formula))
                                   (neg-nnf (nnf-conj-r formula)))]
    [(nnf-disj? formula) (nnf-conj (neg-nnf (nnf-disj-l formula))
                                   (neg-nnf (nnf-disj-r formula)))]))

Przeprowadźmy dowód indukcyjnie względem `φ`.
`P(φ)` := `(neg-nnf (neg-nnf φ))` ≡ `φ`
1. Jeśli `φ` jest literałem:
* Jeśli istnieje takie `var`, że `φ` ≡ `(nnf-lit #t var)`
L = `(neg-nnf (neg-nnf φ))` ≡ `(neg-nnf (neg-nnf (nnf-lit #t var)))` ≡
`(neg-nnf (nnf-lit #f var))` ≡ `(nnf-lit #t var)` ≡ `φ` = P

* Jeśli istnieje takie `var`, że `φ` ≡ `(nnf-lit #f var)`
L = `(neg-nnf (neg-nnf φ))` ≡ `(neg-nnf (neg-nnf (nnf-lit #f var)))` ≡
`(neg-nnf (nnf-lit #t var))` ≡ `(nnf-lit #f var)` ≡ `φ` = P
2. Jeśli `φ` ≡ `(nnf-conj l r)` to:

Załóżmy, że `(neg-nnf (neg-nnf l))` ≡ `l` oraz `(neg-nnf (neg-nnf r))` ≡ `r`, pokażemy, że `(neg-nnf (neg-nnf φ))` ≡ `φ`.

L = `(neg-nnf (neg-nnf φ))` ≡ `(neg-nnf (neg-nnf (nnf-conj l r)))` ≡
`(neg-nnf (nnf-disj (neg-nnf l) (neg-nnf r)))` ≡
`(nnf-conj (neg-nnf (neg-nnf l)) (neg-nnf (neg-nnf r)))` ≡
`(nnf-conj l r)` ≡ `φ` = P
3. Jeśli `φ` ≡ `(nnf-disj l r)` to:

Załóżmy, że `(neg-nnf (neg-nnf l))` ≡ `l` oraz `(neg-nnf (neg-nnf r))` ≡ `r`, pokażemy, że `(neg-nnf (neg-nnf φ))` ≡ `φ`.

L = `(neg-nnf (neg-nnf φ))` ≡ `(neg-nnf (neg-nnf (nnf-disj l r)))` ≡
`(neg-nnf (nnf-conj (neg-nnf l) (neg-nnf r)))` ≡
`(nnf-disj (neg-nnf (neg-nnf l)) (neg-nnf (neg-nnf r)))` ≡
`(nnf-disj l r)` ≡ `φ` = P

Zatem `(neg-nnf (neg-nnf φ))` ≡ `φ`.

## Zadanie 5

Zdefiniuj funkcję eval-nnf typu `(('a -> Boolean) (NNF 'a) -> Boolean)` interpretującą formułę w negacyjnej postaci normalnej, przy zadanym wartościowaniu zmiennych (funkcji typu `('a -> Boolean)`). Następnie pokaż, że dla dowolnej formuły `φ` i wartościowania σ zachodzi `(eval-nnf σ (neg-nnf φ))` ≡ `(not (eval-nnf σ φ))`. Możesz założyć, że funkcja `σ` zawsze się zatrzymuje.

#### Definicja funkcji eval-nnf

(define (eval-nnf s formula)
  (cond [(nnf-lit? formula)
         (if (equal? (nnf-lit-polarity formula) #t) 
             (s (nnf-lit-var formula)
             (not (s (nnf-lit-var formula))))]
        [(nnf-conj? formula) (and (eval-nnf s (nnf-conj-l formula))
                                  (eval-nnf s (nnf-conj-r formula)))]
        [(nnf-disj? formula) (or (eval-nnf s (nnf-disj-l formula))
                                  (eval-nnf s (nnf-disj-r formula)))]))

### Lemat 5.1

Dla dowolnych `x`, `y`, zachodzi `(not (and x y))` ≡ `(or (not x) (not y))`, gdzie `x`, `y` są wartościami boolowskimi.

#### Dowód Lematu 5.1

Rozważmy 4 przypadki:
1. `x` ≡ `#f` oraz `y` ≡ `#f`
2. `x` ≡ `#f` oraz `y` ≡ `#t`
3. `x` ≡ `#t` oraz `y` ≡ `#f`
4. `x` ≡ `#t` oraz `y` ≡ `#t`
Zauważmy, że te przypadki są trywialne, więc Lemat jest prawdziwy dla dowolnych `x`, `y`.

### Lemat 5.2

Chcemy pokazać:
Dla dowolnych `x`, `y`, zachodzi `(not (or x y))` ~ `(and (not x) (not y))`, gdzie`x`, `y` są wartościami boolowskimi.

#### Dowód Lematu 5.2

Rozważmy 4 przypadki:
1. `x` ≡ `#f` oraz `y` ≡ `#f`
2. `x` ≡ `#f` oraz `y` ≡ `#t`
3. `x` ≡ `#t` oraz `y` ≡ `#f`
4. `x` ≡ `#t` oraz `y` ≡ `#t`
Zauważmy, że te przypadki są trywialne, więc Lemat 5.2 jest prawdziwy dla dowolnych`x`, `y`.

### Dowód:

Dowód indukcyjny po `φ`:
Chcemy pokazać, że `(eval-nnf σ (neg-nnf φ))` ≡ `(not (eval-nnf σ φ))`.

1. Jeśli `φ` jest literałem:
* Jeśli istnieje `var` takie, że `φ` ≡ `(nnf-lit #t v)`

L = `(eval-nnf σ (neg-nnf φ))` ≡ `(eval-nnf σ (neg-nnf (nnf-lit #t var)))` ≡
`(eval-nnf σ (nnf-lit #f var))` ≡ `(not (σ var))`

P = `(not (eval-nnf σ φ))` ≡ `(not (eval-nnf σ (nnf-lit #t var)))` ≡ `(not (σ var))` = L
* Jeśli istnieje `var` takie, że `φ` ≡ `(nnf-lit #f v)`

L = `(eval-nnf σ (neg-nnf φ))` ≡ `(eval-nnf σ (neg-nnf (nnf-lit #f var)))` ≡
`(eval-nnf σ (nnf-lit #t var))` ≡ `(σ var)`

P = `(not (eval-nnf σ φ))` ≡ `(not (eval-nnf σ (nnf-lit #t var)))` ≡ `(not (not (σ var))` ≡ `(s v)` = L
2. Jeśli `φ` ≡ `(nnf-conj l r)` to:

Załóżmy, że `(eval-nnf σ (neg-nnf l))` ≡ `(not (eval-nnf σ l))`
oraz `(eval-nnf σ (neg-nnf r))` ≡ `(not (eval-nnf σ r))`,
pokażemy, że `(eval-nnf σ (neg-nnf φ))` ≡ `(not (eval-nnf σ φ))`.

L = `(eval-nnf σ (neg-nnf φ))` ≡ `(eval-nnf σ (neg-nnf (nnf-conj l r)))` ≡
`(eval-nnf σ (nnf-disj (neg-nnf l) (neg-nnf r)))` ≡
`(or (eval-nnf σ (neg-nnf l)) (eval-nnf σ (neg-nnf r)))` ≡
`(or (not (eval-nnf σ l)) (not (eval-nnf σ r)))`

P = `(not (eval-nnf σ φ))` ≡ `(not (eval-nnf σ (nnf-conj l r)))` ≡
`(not (and (eval-nnf σ l)(eval-nnf σ r)))` ≡ (Lemat 5.1)
`(or (not (eval-nnf σ l)) (not (eval-nnf σ r)))` = L
3. Jeśli `φ` ≡ `(nnf-disj l r)` to:

Załóżmy, że `(eval-nnf σ (neg-nnf l))` ≡ `(not (eval-nnf σ l))`
oraz `(eval-nnf σ (neg-nnf r))` ≡ `(not (eval-nnf σ r))`,
pokażemy, że `(eval-nnf σ (neg-nnf φ))` ≡ `(not (eval-nnf σ φ))`.

L = `(eval-nnf σ (neg-nnf φ))` ≡ `(eval-nnf σ (neg-nnf (nnf-disj l r)))` ≡
`(eval-nnf σ (nnf-conj (neg-nnf l) (neg-nnf r)))` ≡
`(and (eval-nnf σ (neg-nnf l)) (eval-nnf σ (neg-nnf r)))` ≡
`(and (not (eval-nnf σ l)) (not (eval-nnf σ r)))`

P = `(not (eval-nnf σ φ))` ≡ `(not (eval-nnf σ (nnf-disj l r)))` ≡
`(not (or (eval-nnf σ l)(eval-nnf σ r)))` ≡ (Lemat 5.2)
`(and (not (eval-nnf σ l)) (not (eval-nnf σ r)))` = L

Zatem dla dowolnej formuły `φ` spełnione jest `(eval-nnf σ (neg-nnf φ))` ≡ `(not (eval-nnf σ φ))`.

## Zadanie 6

Formuły rachunku zdań możemy opisać następującym typem (definicja poniżej). Zdefiniuj funkcję `to-nnf` transformującą formułę do równoważnej formuły w negacyjnej postaci normalnej. Możesz definiować funkcję pomocnicze, ale wszystkie funkcje (wzajemnie) rekurencyjne powinny używać rekursji strukturalnej.

### Definicja typu:

( define-type ( Formula 'v )
    ( var [ var : 'v ])
    ( neg [ f : ( Formula 'v ) ])
    ( conj [ l : ( Formula 'v ) ] [ r : ( Formula 'v ) ])
    ( disj [ l : ( Formula 'v ) ] [ r : ( Formula 'v ) ]) )

### Definicja funkcji to-nnf

(define (to-nnf formula)
  (cond
    [(var? formula) (nnf-lit #t (var-var formula))]
    [(conj? formula) (nnf-conj (to-nnf (conj-l formula))
                               (to-nnf (conj-r formula)))]
    [(disj? formula) (nnf-disj (to-nnf (disj-l formula))
                               (to-nnd (disj-r formula)))]
    [(neg? formula) (to-nnf-neg (neg-f formula))]))

(define (to-nnf-neg formula)
  (cond
    [(var? formula) (nnf-lit #f (var-var formula))]
    [(conj? formula) (nnf-disj (to-nnf-neg (conj-l formula))
                               (to-nnf-neg (conj-r formula)))]
    [(disj? formula) (nnf-conj (to-nnf-neg (disj-l formula))
                               (to-nnf-neg (disj-r formula)))]
    [(neg? formula) (to-nnf (neg-f formula))]))

## Zadanie 7

Zdefiniuj funkcję eval-formula interpretującą formuły z poprzedniego zadania.
Następnie pokaż, że `(eval-nnf σ (to-nnf φ))` ≡ `(eval-formula σ φ)`. Możesz założyć, że funkcja `σ` zawsze się zatrzymuje.

### Lemat 7.1

Jeśli `(eval-nnf σ (to-nnf-neg φ))` ≡ `(not (eval-formula σ φ))` to `(eval-nnf σ (to-nnf (neg φ)))` ≡ `(eval-formula σ (neg φ))`

#### Dowód Lematu 7.1

L = `(eval-nnf σ (to-nnf (neg φ)))` ≡ `(eval-nnf σ (to-nnf-neg φ))` ≡ `(not (eval-formula σ φ))`
P = `(eval-formula σ (neg φ))` = `(not (eval-formula σ φ))` = L

### Dowód

#### Definicja funkcji:

(define (eval-formula s formula)
  (cond [(var? formula) (s (var-var formula))]
        [(conj? formula) (and (eval-formula s (conj-l formula))
                         (eval-formula s (conj-r formula)))]
        [(disj? formula) (or (eval-formula s (disj-l formula))
                            (eval-formula s (disj-r formula)))]
        [(neg? formula) (not (eval-formula s formula))]))

Dowód indukcyjny po `φ`:
Chcemy pokazać, że `(eval-nnf σ (to-nnf φ))` ≡ `(eval-formula σ φ)`.

1. `φ` ≡ `(var x)`:

L = `(eval-nnf σ (to-nnf φ))` ≡ `(eval-nnf σ (to-nnf (var x)))` ≡
`(eval-nnf σ (nnf-lit #t x))` ≡ `(σ x)`

P = `(eval-formula σ φ)` ≡ `(eval-formula σ (var x)))` ≡ `(σ x)` = L
2. `φ` ≡ `(conj l r)`
Załóżmy, że `(eval-nnf σ (to-nnf l))` ≡ `(eval-formula σ l)`
oraz `(eval-nnf σ (to-nnf r))` ≡ `(eval-formula σ r)`.

L = `(eval-nnf σ (to-nnf φ))` ≡ `(eval-nnf σ (to-nnf (conj l r)))` ≡
`(eval-nnf σ (nnf-conj (to-nnf l)(to-nnf r)))` ≡
`(and (eval-nnf σ (to-nnf l))(eval-nnf σ (to-nnf r))` ≡
`(and (eval-formula σ l)(eval-formula σ r)`

P = `(eval-formula σ φ)` ≡ `(eval-formula σ (conj l r))` ≡
`(and (eval-formula σ l)(eval-formula σ r))` = L
3. `φ` ≡ `(disj l r)`
Załóżmy, że `(eval-nnf σ (to-nnf l))` ≡ `(eval-formula σ l)` oraz `(eval-nnf σ (to-nnf r))` ≡ `(eval-formula σ r)`.

L = `(eval-nnf σ (to-nnf φ))` ≡
`(eval-nnf σ (to-nnf (disj l r)))` ≡
`(eval-nnf σ (nnf-disj (to-nnf l)(to-nnf r)))` ≡
`(or (eval-nnf σ (to-nnf l))(eval-nnf σ (to-nnf r))` ≡
`(or (eval-formula σ l)(eval-formula σ r)`

P = `(eval-formula σ φ)` ≡
`(eval-formula σ (disj l r))` ≡
`(or (eval-formula σ l)(eval-formula σ r))` = L
4. `φ` ≡ `(neg x)`
* `x` ≡ `(var v)`
L = `(eval-nnf σ (to-nnf φ))` ≡ `(eval-nnf σ (to-nnf (neg x)))` ≡
`(eval-nnf σ (to-nnf-neg x))` ≡ `(eval-nnf σ (to-nnf-neg (var v)))` ≡
`(eval-nnf σ (nnf-lit #f v)` ≡ `(not (σ v))`

P = `(eval-formula σ φ)` ≡ `(eval-formula σ (neg (var v)))` ≡
`(not (eval-formula σ v))` ≡ `(not (σ v))` = L
* `x` ≡ `(conj l r)`
Załóżmy, że `(eval-nnf σ (to-nnf-neg l))` ≡ `(not (eval-formula σ l))`
oraz `(eval-nnf σ (to-nnf-neg r))` ≡ `(not (eval-formula σ r))`.

L = `(eval-nnf σ (to-nnf φ))` ≡ `(eval-nnf σ (to-nnf (neg (conj l r))))` ≡
`(eval-nnf σ (to-nnf-neg (conj l r)))` ≡
`(eval-nnf σ (nnf-disj (to-nnf-neg l) (to-nnf-neg r)))` ≡
`(or (eval-nnf σ (to-nnf-neg l)) (eval-nnf σ (to-nnf-neg r)))` ≡
`(or (not (eval-formula σ l)) (not (eval-formula σ r)))`

P = `(eval-formula σ φ)` ≡ `(eval-formula σ (neg (conj l r)))` ≡
`(not (eval-formula σ (conj l r)))` ≡
`(not (and (eval-formula σ l)(eval-formula σ r)))` ≡
`(or (not (eval-formula σ l))(not (eval-formula σ r)))` = L

Udowodniliśmy, że
`(eval-nnf σ (to-nnf-neg (conj l r)))` ≡ `(not (eval-formula σ (conj l r)))`, ale z Lematu 7.1 otrzymujemy
`(eval-nnf σ (to-nnf (neg (conj l r))))` ≡ `(eval-formula σ (neg (conj l r)))`
* `x` ≡ `(disj l r)`
Załóżmy, że `(eval-nnf σ (to-nnf-neg l))` ≡ `(not (eval-formula σ l))`
oraz `(eval-nnf σ (to-nnf-neg r))` ≡ `(not (eval-formula σ r))`.

L = `(eval-nnf σ (to-nnf φ))` ≡ `(eval-nnf σ (to-nnf (neg (disj l r))))` ≡
`(eval-nnf σ (to-nnf-neg (disj l r)))` ≡
`(eval-nnf σ (nnf-conj (to-nnf-neg l) (to-nnf-neg r)))` ≡
`(and (eval-nnf σ (to-nnf-neg l)) (eval-nnf σ (to-nnf-neg r)))` ≡
`(and (not (eval-formula σ l)) (not (eval-formula σ r)))`

P = `(eval-formula σ φ)` ≡ `(eval-formula σ (neg (disj l r)))` ≡
`(not (eval-formula σ (disj l r)))` ≡
`(not (or (eval-formula σ l)(eval-formula σ r)))` ≡
`(and (not (eval-formula σ l))(not (eval-formula σ r)))` = L

Udowodniliśmy, że
`(eval-nnf σ (to-nnf-neg (disj l r)))` ≡ `(not (eval-formula σ (disj l r)))`, ale z Lematu 7.1 otrzymujemy
`(eval-nnf σ (to-nnf (neg (disj l r))))` ≡ `(eval-formula σ (neg (disj l r)))`
* `x` ≡ `(neg v)`
Zalozmy, ze `(eval-nnf σ (to-nnf v))` ≡ `(eval-formula σ v)`
oraz `(eval-nnf σ (to-nnf (neg v)))` ≡ `(eval-formula σ (neg v))`
L = `(eval-nnf σ (to-nnf φ))` ≡ `(eval-nnf σ (to-nnf (neg (neg v))))` ≡
`(eval-nnf σ (to-nnf-neg (neg v)))` ≡ `(eval-nnf σ (to-nnf v))`

P = `(eval-formula σ φ)` ≡ `(eval-formula σ (neg (neg v)))` ≡
`(not (eval-formula σ (neg v)))` ≡ `(not (not (eval-formula σ v)))` ≡
`(eval-formula σ v)` = L

Zatem `(eval-nnf σ (to-nnf φ))` ≡ `(eval-formula σ φ)`

## Zadanie 8.
Zdefiniuj predykat `sorted?` : `((Listof Number) -> Boolean)` sprawdzający czy lista jest posortowana oraz funkcję `insert` : `(Number (Listof Number) -> (Listof Number))` wstawiającą element do listy posortowanej. Następnie udowodnij, że jeśli `(sorted? xs)` ≡ `#t` to `(sorted? (insert x xs))` ≡ `#t`.

#### Definicja sorted?

(define (sorted? xs)
  (cond [(empty? xs) #t]
        [(empty? (rest xs)) #t]
        [else (if (<= (first xs) (second xs))
                  (sorted? (rest xs))
                  #f)]))

#### Definicja insert

(define (insert x xs)
  (if (empty? xs)
      (list x)
      (if (<= x (first xs))
          (cons x xs)
          (cons (first xs) (insert x (rest xs))))))

### Lemat 8.1
`(sorted? xs)` zwraca `#t` gdy lista `xs` jest posortowana, a `#f` w przeciwnym wypadku.

#### Dowód:
Pokażmy indukcyjnie:
1. Baza indukcji:
dla `xs` ≡ `empty` oczywiście jest dobrze
dla `xs` jednoelementowego też
2. Krok indukcyjny:
Weźmy takie `x`, `xrest`, że `xs` ≡ `(cons x xrest)`. Zakładamy, że `sorted` działa dla `xrest`, pokażemy że działa dla `(cons x xrest)`.
1. Jeśli `(sorted? xrest)` to `xrest` jest posortowana więc jeśli `x` jest mniejszy od `(first xrest)` to `(cons x xrest)` jest posortowane a `(sorted?)` zwróci prawdę, więc działa.
2. podobnie (jesli nie jest mniejszy to nie jest posortowane, jelsi wcześniej nieposortowane to całość też).
Stąd `sorted` działa.

### Lemat 8.2

Jeśli `x` < `y` oraz `(sorted? xs)` oraz `(sorted? (cons x xs))` to zachodzi:
`(sorted? (cons x (insert y xs))` ≡ `(sorted? (insert y xs))`.
1. Jeśli `(sorted? (insert y xs))` to: (l = (insert y xs))
* jeśli x <= (first l) to skoro l jest posortowana to (cons x l) także, zatem `(sorted? (cons x (insert y xs))` zwróci prawdę (zgadza się).
2. Jeśli nieprawda, że `(sorted? (insert y xs))` to `(sorted? (cons x (insert y xs))` nie może zwrócić prawdy, (bo prawda tylko jak x <= (first l) oraz `(sorted? (insert y xs))`), zatem się zgadza.
Stąd niezależnie, czy `(sorted? (insert y xs))` jest prawdą, czy nie mamy:
`(sorted? (cons x (insert y xs))` ≡ `(sorted? (insert y xs))`, co chceliśmy pokazać.

### Dowód

Pokażemy, że jeśli `(sorted? xs)` ≡ `#t` to `(sorted? (insert y xs))` ≡ `#t`.
Załóżmy, że `(sorted? xs)` ≡ `#t`.
1. Baza inducji:
Jeśli `xs` ≡ `empty` to:
`(sorted? (insert x xs))` ≡ `(sorted? (insert x empty))` ≡ `(sorted? (list x))` ≡ `(sorted? (cons x empty))` ≡ `#t`, cnd.
2. Krok indukcyjny:
Zakładamy, że:
* `(sorted? (cons x xs))` ≡ `#t`
* jeśli `(sorted? xs)` ≡ `#t` to `(sorted? (insert y xs))` ≡ `#t`
Pokażemy, że: `(sorted? (insert y (cons x xs)))` ≡ `#t`.
Zauważmy, że `(sorted? (cons x xs))` ≡
1. `xs` ≡ `empty`: `(sorted? (cons x xs))` ≡ `#t`
2. W pozostałych przypadkach:
a. jeśli `(<= x (second xs)` to `(sorted? (cons x xs))` ≡ `(sorted? xs)`
b. `#f`
Zatem skoro `(sorted? (cons x xs))` ≡ `#t` to `(sorted? xs)` ≡ `#t`. Zatem z założenia 2. mamy, że `(sorted? (insert y xs))` ≡ `#t`.
Mamy 2 przypadki:
1. `y` <= `x`, wtedy:
`(sorted? (insert y (cons x xs)))` ≡
`(sorted? (cons y (cons x xs)))` ≡ (skoro y <= x)
`(sorted? (cons x xs))` ≡ `#t` (z założeń).
2. `y` > `x`, wtedy:
`(sorted? (insert y (cons x xs)))` ≡
`(sorted? (cons x (insert y xs))` ≡ (skoro `(insert y xs)` jest pewną listą) i z L 8.2
`(sorted? (insert y xs))` ≡ `#t`, co należało pokazać.

## Zadanie 8.
Zdefiniuj predykat `sorted?` : `((Listof Number) -> Boolean)` sprawdzający czy lista jest posortowana oraz funkcję `insert` : `(Number (Listof Number) -> (Listof Number))` wstawiającą element do listy posortowanej. Następnie udowodnij, że jeśli `(sorted? xs)` ≡ `#t` to `(sorted? (insert x xs))` ≡ `#t`.

#### Definicja sorted?

(define (sorted? xs)
  (cond [(empty? xs) #t]
        [(empty? (rest xs)) #t]
        [else (if (<= (first xs) (second xs))
                  (sorted? (rest xs))
                  #f)]))

#### Definicja insert

(define (insert x xs)
  (if (empty? xs)
      (list x)
      (if (<= x (first xs))
          (cons x xs)
          (cons (first xs) (insert x (rest xs))))))

### Dowód

Pokażemy, że jeśli `(sorted? xs)` ≡ `#t` to `(sorted? (insert y xs))` ≡ `#t`.
Załóżmy, że `(sorted? xs)` ≡ `#t`.
1. Baza inducji:
Jeśli `xs` ≡ `empty` to:
`(sorted? (insert x xs))` ≡ `(sorted? (insert x empty))` ≡ `(sorted? (list x))` ≡ `(sorted? (cons x empty))` ≡ `#t`, cnd.
2. Krok indukcyjny:
Załóżmy, że `(sorted? xs)` ≡ `#t` to `(sorted? (insert y xs))` ≡ `#t`
Pokażemy, że `(sorted? (cons x xs)` ≡ `#t` to `(sorted? (insert y (cons x xs)))` ≡ `#t`
* `y` <= `x`:
Wtedy `(insert y (cons x xs))` ≡ `(cons y (cons x xs))`
`(sorted? (cons x xs) ≡ #t` oraz `y` <= `x`, więc
`(sorted? (insert y (cons x xs)))` ≡ `(sorted? (cons y (cons x xs)))` ≡ `#t`
* `x` < `y` <= `(first xs)`
`(sorted? (insert y (cons x xs)))` ≡ `(sorted? (cons x (insert y xs)))` ≡ `(sorted? (cons x (cons y xs)))` ≡ `#t`
* `x` < `(first xs)` < `y`
`(sorted? (insert y (cons x xs)))` ≡ `(sorted? (cons x (insert y xs)))` ≡ `(sorted? (cons x (insert y xs)))`
Skoro `(sorted? (insert y xs))` ≡ `#t` oraz `x` < `(first xs)` < `y` to `(sorted? (cons x (insert y xs)))` ≡ `#t`