# Zadanie 10

## Część I
---
### Twierdzenie:

(map f (append xs ys)) ≡ (append (map f xs) (map f ys))

### Dowód:
Niech $f$ - ustalona procedura jednoargumentowa.
Weźmy dowolne $ys$ takie, że:

(list? ys) ≡ #t

Dowód przeprowadzimy przez indukcję względem $xs$.

Niech:

(P xs) ≔ (map f (append xs ys)) ≡ (append (map f xs) (map f ys))

#### 1° Dla $xs ≡ null$ mamy:

(map f (append null ys))

≡ (map f (if (null? null)
             ys
             (cons (car null) 
                   (append (cdr null) ys))))
                   
≡ (map f ys)

Ponieważ zachodzi:

(list? (map f ys)) ≡ #t

to:

(map f ys)

≡ (if (null? null)
      (map f ys)
      (cons (car null) (append (cdr null) ys)))
      
≡ (append null (map f ys)

Zatem własność $P$ zachodzi dla $xs ≡ null$.

---

#### 2° Weżmy dowolne $x \space xs$ i załóżmy, że zachodzi:

(map f (append xs ys)) ≡ (append (map f xs) (map f ys))

Pokażmy, że własność $P$ zachodzi dla $x \space xs$:

(map f (append (cons x xs) ys))

≡ (map f (if (null? (cons x xs)
             ys
             (cons (car (cons x xs)) 
                   (append (cdr (cons x xs)) ys)))))
                   
≡ (map f (cons x (append xs ys)))
             
≡ (if (null? (cons x (append xs ys)))
       null
       (cons (f x)
             (map f (append xs ys))))
≡ (cons (f x)
        (map f (append xs ys))))

Z założenia indukcyjnego:

≡ (cons (f x)
        (append (map f xs) (map f ys)))
        
≡ (cons (car (cons (f x) (map f xs))) 
            (append (cdr (cons (f x) (map f xs))) (map f ys))
            
≡ (if (null? (cons (f x) (map f xs))
      (map f ys)
      (cons (car (cons (f x) (map f xs))) 
            (append (cdr (cons (f x) (map f xs))) (map f ys))))

≡ (append (cons (f x) (map f xs))
          (map f ys))
             
≡ (append (if (null? (cons x xs))
              null
              (cons (f (car (cons x xs)))
                    (map f (cdr (cons x xs)))))
          (map f ys))

≡ (append (map f (cons x xs)) (map f ys))

Zatem własność $P$ zachodzi dla dowolnego xs.

## Część II
---
### Twierdzenie:

(filter p? (append xs ys)) ≡ (append (filter p? xs) (filter p? ys))

### Dowód:
Niech $p?$ - ustalony predykat jednoargumentowy.

Weźmy dowolne $ys$ takie, że:

(list? ys) ≡ #t

Dowód przeprowadzimy przez indukcję względem $xs$.

Niech:

(P xs) ≔ (filter p? (append xs ys)) ≡ (append (filter p? xs) (filter p? ys))

#### 1° Dla $xs ≡ null$ mamy

(filter p? (append null ys))

≡ (filter p? ys)

≡ (append null (filter p? ys))

≡ (append (cond
              [(null? null) null]
              [(p? (car xs))
                (cons (car xs)
                      (filter p? (cdr xs)))]
              [else (filter p? (cdr xs))])
          (filter p? ys))
          
≡ (append (filter p? null) (filter p? ys))

Zatem własność $P$ zachodzi dla $xs ≡ null$.

#### 2° Weżmy dowolne $x$ $xs$ i załóżmy, że zachodzi:

(filter p? (append xs ys)) ≡ (append (filter p? xs) (filter p? ys))

Pokażmy, że własność $P$ zachodzi dla $x$ $xs$:

(filter p? (append (cons x xs) ys))

≡ (filter p? (if (null? (cons x xs)) 
                  ys 
                  (cons (car (cons x xs)) 
                        (append (cdr (cons x xs)) ys))))
                  
≡ (filter p? (cons x (append xs ys)))

≡ (cond
     [(null? (cons x (append xs ys))) null]
     [(p? x)
        (cons x
             (filter p? (append xs ys)))]
     [else (filter p? (append xs ys))])

Rozważmy dwa przypadki:
##### 2.1°
Załóżmy, że

(p? x) ≡ #t

Wtedy

≡ (cons x
        (filter p? (append xs ys)))

Z założenia indukcyjnego:

≡ (cons x
        (append (filter p? xs) (filter p? ys)))

≡ (if (null? (cons x (filter p? xs)) 
        ys 
        (cons x  
              (append (filter p? xs) (filter p? ys))))))
        
≡ (if (null? (cons x (filter p? xs)) 
        (filter p? ys) 
        (cons (car (cons x (filter p? xs)) 
              (append (cdr (cons x (filter p? xs))) 
                      (filter p? ys))))))

≡ (append (cons x (filter p? xs))
          (filter p? ys))

≡ (append (cond
            [(null? (cons x xs)) null]
            [(p? x)
                (cons x 
                      (filter p? xs))]
            [else (filter p? xs)])
          (filter p? ys))
          
≡ (append (cond
            [(null? (cons x xs)) null]
            [(p? (car (cons x xs)))
                (cons (car (cons x xs))
                      (filter p? (cdr (cons x xs))))]
            [else (filter p? (cdr (cons x xs)))])
          (filter p? ys))

≡ (append (filter p? (cons x xs)) (filter p? ys))

##### 2.2°
Załóżmy, że

(p? x) ≡ #f

Wtedy

≡ (filter p? (append xs ys))

Z założenia indukcyjnego:

≡ (append (filter p? xs) (filter p? ys))

≡ (append (cond
            [(null? (cons x xs)) null]
            [(p? x)
                (cons x
                      (filter p? xs))]
            [else (filter p? xs)]) 
          (filter p? ys))
          
≡ (append (cond
            [(null? (cons x xs)) null]
            [(p? (car (cons x xs)))
                (cons (car (cons x xs))
                      (filter p? (cdr (cons x xs))))]
            [else (filter p? (cdr (cons x xs)))]) 
          (filter p? ys))
          
≡ (append (filter p? (cons x xs)) (filter p? ys))

Zatem własność $P$ zachodzi dla dowolnego $xs$.

---
Autor: Wiktoria Kuna
(konsultując z Jakub Zając)

###### tags: `mp`