---
# System prepended metadata

title: Zadanie 10
tags: [mp]

---

# Zadanie 10

## Część I
---
### Twierdzenie:
```racket
(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:
```racket
(list? ys) ≡ #t
```

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

Niech:
```racket
(P xs) ≔ (map f (append xs ys)) ≡ (append (map f xs) (map f ys))
```

#### 1° Dla $xs ≡ null$ mamy:
```racket
(map f (append null ys))

≡ (map f (if (null? null)
             ys
             (cons (car null) 
                   (append (cdr null) ys))))
                   
≡ (map f ys)
```
Ponieważ zachodzi:
```racket
(list? (map f ys)) ≡ #t
```
to:
```racket
(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:
```racket
(map f (append xs ys)) ≡ (append (map f xs) (map f ys))
```

Pokażmy, że własność $P$ zachodzi dla $x \space xs$:
```racket
(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:
```racket
≡ (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:
```racket
(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:
```racket
(list? ys) ≡ #t
```

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

Niech:
```racket
(P xs) ≔ (filter p? (append xs ys)) ≡ (append (filter p? xs) (filter p? ys))
```

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

```racket
(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:
```racket
(filter p? (append xs ys)) ≡ (append (filter p? xs) (filter p? ys))
```
Pokażmy, że własność $P$ zachodzi dla $x$ $xs$:
```racket 
(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
```racket
(p? x) ≡ #t
```
Wtedy
```racket
≡ (cons x
        (filter p? (append xs ys)))
```
Z założenia indukcyjnego:
```racket 
≡ (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
```racket
(p? x) ≡ #f
```

Wtedy
```racket
≡ (filter p? (append xs ys))
```

Z założenia indukcyjnego:
```racket 
≡ (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`