---
# System prepended metadata

title: Zadania z indukcji (dodatkowe)
tags: [MP]

---

---
title: Zadania z indukcji (dodatkowe)
---
1. (append (map f xs) (map f ys)) = (map f (append xs ys))
2. (length (append xs ys)) = (+ (length xs) (length ys))
3. (filter p (map f xs)) = (map f (filter (lambda (x) (p (f x))) xs)
4. niech ns będzie lista liczb całkowitych.
   (foldr + 0 ns) = (foldl + 0 ns)

1) Dla każdej listy ys:
 P(xs) := (append (map f xs) (map f ys)) = (map f (append xs ys))

```racket=
(define (append xs ys)
    (if (null? xs)
        ys
        (append (cdr xs) (cons (car xs) ys))))
        
(define (map f xs)
    (if (null? xs)
        null
        (cons (f (car xs)) (map f (cdr xs)))))
        
```

Baza:
xs=null
P(null) 
L = (append (map f null) (map f ys)) = (append null (map f ys)) = (map f ys)
P = (map f ys)
Krok ind.
Zal: P(xs)
Teza: P((cons x xs))
P((cons x xs)):
L = (append (map f (cons x xs)) (map f ys)) = (def map)
= (append (cons (f x) (map f xs)) (map f ys)) = (def append)
= (append (map f xs) (cons (f x) (map f ys))


##### Zadanie 3


```racket!
(define (filter p xs)
    (if (null? xs)
        null
        (if (p (car xs))
            (cons (car xs) (filter p (cdr xs)))
            (filter p (cdr xs)))))
            
(define (map f xs)
    (if (null? xs)
        null
        (cons (f (car xs)) 
            (map f (cdr xs)))))
```
P(xs) := (filter p (map f xs)) = (map f (filter (lambda (x) (p (f x))) xs)
**Baza indukcji:**
P(null)
L = (filter p (map f null)) = (filter p null) = null
P = (map f (filter (lambda(x) p (f x)) null)) = (map f null) = null
$L=P$
**Krok indukcyjny**
Zal.ind P(xs)
Pokażemy, dla P((cons x xs))
P((cons x xs)):
$L$ = (filter p (map f (cons x xs))) = 
    (filter p (cons (f x) (map f xs))) =
1. (p (f x)) = #t
(cons (f x) (filter p (map f xs))) = (z zal. ind) = 
(cons (f x) (map f (filter (lambda (x) (p (f x))) xs))
2. (p (f x)) = #f
(filter p (map f xs)) = **(map f (filter (lambda (x) (p (f x))) xs) = P**

$P$ = (map f (filter (lambda (x) (p (f x))) (cons x xs))) = 
1. ((lambda (x) (p (f x))) x) = #t -> (p (f x)) = #t
(map f (cons x (filter (lambda (x) (p (f x))) xs))) = (def map'a)
(cons (f x) (map f (filter (lambda (x) (p (f x))) xs))) = L
2. ((lambda (x) (p (f x))) x) = #f -> (p (f x)) = #f
(map f (filter (lambda (x) (p (f x))) xs)) = **(filter p (map f xs)) = L** 
*Lemat pomocniczy*
(filter p (map f x)) $\equiv$ (map f (filter (lambda (x) (p (f x))) xs))


#### Niech ns będzie lista liczb całkowitych.
   Pokaż, (foldr + 0 ns) = (foldl + 0 ns)
```racket!

(define (foldr f x xs)
  (if (empty? xs)
      x
      (f (first xs) (foldr f x (rest xs)))))

(define (foldl f x xs)
  (if (empty? xs)
      x
      (foldl f (f (first xs) x) (rest xs))))
```
(foldr f x (cons A (cons B (cons C (cons D null)))))
NALEŻY ODCZYTYWAĆ JAKO
(f A (f B (f C (f D x))))

(foldl f x (cons A (cons B (cons C (cons D null)))))
ODCZYTUJ JAKO
(f D (f C (f B (f A x))))

P(ns) := (foldr + 0 ns) = (foldl + 0 ns)
**Baza indukcji:**
P(null) := 
L = (foldr + 0 null) = 0
P = (foldl + 0 null) = 0
$L = P$
**Krok indukcyjny:**
Zał.ind: P(ns)
Teza: (P (cons n ns)), gdie $n\in \mathbb{N}$ i ns - dowolna lista liczba naturalnych
P(xs) -> P((cons x xs))
zał. dla dowolnego y i z    (+ y (foldl + z xs)) = (foldl + (+ y z) xs)
teza:  (+ y (foldl + z (cons x xs))) = (foldl + (+ y z) (cons x xs))

L = (+ y (foldl + z (cons x xs))) =
(+ y (foldl + (+ x z) xs)) = z zał
(foldl + (+ y (+ x z)) xs) 

P = (foldl + (+ y z) (cons x xs)) =
(foldl + (+ x (+ y z)) xs) = przemienności dodawania
(foldl + (+ y (+ x z)) xs)


### Drzewa

Zadanie z indukcji:

przypomnijmy definicję drzewa z wykładu 4:

(define-struct leaf () #:transparent)
(define-struct node (l elem r) #:transparent)

 drzewo to:
 - albo (leaf)
 - albo (node l elem r), gdzie l i r to drzewa
```racket!


(define (tree? x)
  (cond [(leaf? x) #t]
        [(node? x) (and (tree? (node-l x))
                        (tree? (node-r x)))]
        [else #f]))


;i zdefiniujmy lustrzane odbicie drzewa:

(define (mirror t)
 (if ( leaf? t )
  (leaf)
  (node (mirror (node-r t))
             (node-elem t )
             (mirror (node-l t)))))


```

---
**Zasada indukcji:**
Jeśli P jest własnością drzew oraz
- P((leaf))
- dla wszystkich drzew l i r oraz dla wszystkich elementów x, jeśli P(l) i P(r) to P((node l x r))
Wtedy P zachodzi dla wszystkich drzew
---

Udowodnić, że (mirror (mirror t)) ≡ t dla wszystkich drzew t.
P(t) := (mirror (mirror t)) ≡ t
**Baza indukcji:**
P((leaf)) = (mirror (mirror (leaf))) = (mirror (leaf)) = (leaf)
**Krok indukcyjny:**

Założenia (zachodzi dla dowolnego lewego i prawego poddrzewa)
H1: P(l)= (mirror (mirror l)) ≡ l
H2: P(r )= (mirror (mirror r)) ≡ r

Pokażemy,dla dowolnego x, że P((node l x r ))
P((node l x r )) = (mirror (mirror (node l x r))) = (z def mirror)
                   (mirror (node (mirror r) x (mirror l)) = (z def mirror)
                   (node (mirror (mirror l)) x (mirror (mirror r)) = (z zal.ind)
                   (node l x r) 

Zadanie 2: to samo, ale dla drzew, które przechowują elementy w liściach a nie
w wierzchołkach wewnętrznych.

**Zasada indukcji**
- dla wszystkich elementów x, jeśli P((x leaf))
- dla wszystkich drzew l i r  jeśli P(l) i P(r) to P((node l x r))
Wtedy P zachodzi dla wszystkich drzew- P((leaf))
- dla wszystkich drzew l i r oraz dla wszystkich elementów x, jeśli P(l) i P(r ) to P((node l r))
Wtedy P zachodzi dla wszystkich drzew

Ciekawsze zadanie: udowodnić, że dwie implementacje flatten z listy 4 liczą to
samo.

```racket!
(define (flatten t)
    (if (leaf? t)
        null
        (append (flatten (node-l t))
                (cons (node-elem t)
                    (flatten (node-r t))))))
                
(define (flat-append t xs)
  (if (leaf? t)
      xs
      (flat-append (node-l t) (cons (node-elem t) (flat-append (node-r t) xs)))))

(define (flatten2 t)
  (flat-append t '()))
  
 (define (append xs ys)
    (if (null? xs)
        ys
        (cons (car xs) (append (cdr xs) ys))
```

**P(t) := (flatten t) = (flatten2 t)**
        ekwiwalentnie
        (flatten t) = (flat-append t '())
        
**Baza indukcji:**
P((leaf)):
L = (flatten (leaf)) = null
P = (flatten2 (leaf)) = (flat-append (leaf) null) = null

Spróbujemy najpierw przeprowadzić dowód mechanicznie
**Krok indukcyjny:**
Założenia (zachodzi dla lewego i prawego poddrzewa)
Dla dowolnego drzewa l i r oraz dowolnego elementu x
IH1: P(l) := (flatten l) = (flatten2 l)
IH2: P(r ) := (flatten r) = (flatten2 r)

**Lemat pomocniczy:**
Dla dowolnego drzewa t, i dla dowolnej listy xs
Q(t) := (append (flatten t) xs) = (flat-append t xs)
Dowód:
Dla dowolnej listy xs
Q((leaf)) :
L = (append (flatten (leaf)) xs) = (append null xs) = xs
P = (flat-append (leaf)) = xs

Krok indukcyjny:
Dla dowolnej listy xs
Q((node l x r)):

L = (append (flatten (node l x r)) xs) = (z def flatten)
= (append (append (flatten l) (cons x (flatten r))) xs) = (z zał ind)
  (append (flat-append l (cons x (flatten r))) xs) = (z def. flat-append)
  (append)
  
L = (append (flatten (node l x r)) xs)
= (append (append (flatten l) (cons x (flatten r))) xs) (z definicji flatten)

= (append (flat-append l (cons x (flatten r))) xs) (z ZI)
= (flat-append l (append (cons x (flatten r)) xs)) (z definicji flat-append)
  
  
P = (flat-append (node l x r) xs) = 
    (flat-append l (cons x (flat-append r xs)))
    

  