# FLP -- Důkazy
## Návod
Ne všechno je definované v zadání. Například foldr, foldl a podobné definice je potřeba znát z paměti.
- vždy číslujte ake pravidla (rovnice) použivate
- všetko krokujte postupne nespajajte kroky
- zatvorkovanie spravte ako samostatny krok
- https://haskellhero.grifart.cz/index.php?page=lessons&lesson=56
Pamatať si:
- foldr(hlavne)
```haskell
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f z [] = z
foldr f z (x:xs) = f x (foldr f z xs)
```
```haskell
foldl :: (a -> b -> a) -> a -> [b] -> a
foldl f z [] = z
foldl f z (x:xs) = foldl f (f z x) xs
```
```haskell
map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = f x : map f xs
```
```haskell
len [] = 0
len (x:xs) = 1 + len xs
```
```haskell
rev [] = []
rev (x:xs) = rev xs ++ [x]
```
```haskell
concat :: [[a]] -> [a]
concat [] = []
concat (x:xs) = x ++ concat xs
```
```haskell
-- Pozn.: nefunguje ako filter, ale and pre Bool zoznam
-- [True, True] vrati True
-- [True False] vrati False
all [] = True
all (x:xs) = x && all xs
```
```haskell
any [] = False
any (x:xs) = x || any xs
```
```haskell
sum [] = 0
sum (x:xs) = x + sum xs
```
```haskell
[] ++ ys = ys
(x:xs) ++ ys = x:(xs ++ ys)
(xs ++ ys) ++ zs = xs ++ (ys ++ zs)
```
- úprava prefix na infix
```haskell
(++) a (foldr (++) [] as) = a ++ (foldr (++) [] as)
```
- aplikacia beta-redukcie
```haskell
-- _ sa nahradi a
(\_ n -> 1+n) a (foldr (\_ n -> 1+n) 0 as) = |beta-reduction
-- n sa nahradi (foldr (\_ n -> 1+n) 0 as)
(\n-> 1+n) (foldr (\_ n -> 1+n) 0 as) = |beta-reduction
1 + (foldr (\_ n -> 1+n) 0 as)
```
```haskell
take n _ | n <= 0 = []
take _ [] = []
take n (x:xs) = x : take (n-1) xs
```
```haskell
drop n xs | n <= 0 = xs
drop _ [] = []
drop n (x:xs) = drop (n-1) xs
```
------
je treba dokazať L=P pre
- ak je v zadaní len xs:
· xs = []
· xs = (a:as)
- ak je v zadaní xs aj ys:
· xs = [] (ľubovolné ys - pozn. zostáva také isté)
· ys = [] (ľubovolné xs - pozn. zostáva také isté)
· xs = (a:as), ys = (b:bs)
I.P./I.H. je same shit indukčný predpoklad/hypotéza (je to v podstate odpisane len dokazovane zadanie)
## 2023/2024
### 1. Opravný termín
2. /12b/ Mějme definováno (ve dvou sloupcích):
```haskell
take 0 = [] drop 0 x = x
take _ [] = [] drop _ [] = []
take n (x:xs) = x : take (n-1) xs drop n (x:xs) = drop (n-1) xs
```
Dokažte, že `take n xs ++ drop n xs = xs` pro všechny konečné seznamy `xs` a pro všechna nezáporná celá čísla `n`.
```haskell
tak_ 0 x = [] -- 1
tak_ _ [] = [] -- 2
tak_ n (x:xs) = x : tak_ (n-1) xs -- 3
dro_ 0 x = x -- 4
dro_ _ [] = [] -- 5
dro_ n (x:xs) = dro_ (n-1) xs -- 6
[] ++ ys = ys -- 7
(x:xs) ++ ys = x : (xs ++ ys) -- 8
take n xs ++ drop n xs = xs
1) xs = [], n>0
L = take n [] ++ drop n [] =|2
[] ++ drop n [] =|7
drop n [] =|5
[] = P
2) n=0, for all xs
n==0
L = take 0 xs ++ drop 0 xs =|1
[] ++ drop 0 xs =|4
[] ++ xs =|7
xs = P
3)
xs = (a:as), n=k+1, k>=0
I.P.
take n xs ++ drop n xs = xs
L = take (k+1) (a:as) ++ drop (k+1) (a:as) =|3
(a : take k as) ++ drop (k+1) (a:as) =|6
(a : take k as) ++ drop k as =|8
a : (take k as ++ drop k as) =|I.P.
a : (as) = a:as = P
Q.E.D.
```
### Řádný termín
/14b/ Je dáno:
```haskell
minl v [] = v -- 1
minl v (x:xs) = if x<v then minl x xs else minl v xs -- 2
foldl_ f z [] = z -- 3
foldl_ f z (x:xs) = foldl_ f (f z x) xs -- 4
minf v l = foldl_ (\ b a -> if a<b then a else b) v l -- 5
```
Dokazte: `minl v xs = minf v xs` (pozor: druha cast dukazu `xs = (a:as)` se jeste musi rozdelit na dve vetvy)
```haskell
minl v xs = minf v xs
1) xs=[], for all v
L = minl v [] =|1
= v
P = minf v [] =|5
= foldl_ (\ b a -> if a<b then a else b) v [] =|3
= v
L=P
I.H.
for all v: minl v xs = minf v xs
2) xs = (a:as)
L = minl v (a:as) =|2
= if a<v then minl a as else v as
I] a<v && if True then else
minl a as =|I.H. minf a as
II] a>=v && if False then else
minl v as =|I.H. minf v as
P
= minf v (a:as) =|5
= foldl_ (\ b a -> if a<b then a else b) v (a:as) =|4
= foldl_ (\ b a -> if a<b then a else b) ((\ b a -> if a<b then a else b) v a) as =|2xBeta
= foldl_ (\ b a -> if a<b then a else b) (if a<v then a else v) as
i] a<v && if True then else
foldl_ (\ b a -> if a<b then a else b) a as =|5 minf a as = L[I]
ii] a>=v && if False then else
foldl_ (\ b a -> if a<b then a else b) v as =|5 minf v as = L[II]
Q.E.D.
```
## 2022/2023
### Předtermín
V haskellu je dano
- `suma a [] = a`
- `suma a (x:xs) = suma (a + x) xs`
Dokazte, ze `suma 0 xs = foldl (+) 0 xs`. Byla tam poznamka, ze mame vhodne zvolit indukcni hypotezu (8b)
Pozor na fold**l** a ne fold**r**
## 2021/2022
### termin
- concat = foldr (:) pro konečné xs a ys
`concat xs ++ ys = foldr (:) ys xs`
```haskell
concat [] ++ ys = ys
concat (x:xs) ++ ys = x : (concat xs ++ ys)
```
### 1. opravný
(14b alebo 16b)
Axiomy:
```haskell
uncurry f (x,y) = f x y (1)
zip [] _ = [] (3)
zip _ [] = [] (4)
zip (x:xs) (y:ys) = (x,y) : zip xs ys (5)
map f [] = [] (6)
map f (x:xs) = f x : map f xs (7)
zipWith f [] _ = [] (8)
zipWith f _ [] = [] (9)
zipWith f (x:xs) (y:ys) = f x y : zipWith f xs ys (10)
```
Dokazujeme pomocí strukturální indukce s indukční proměnnou xs:
`map (uncurry f) (zip xs ys) = zipWith f xs ys`
```haskell
1) xs = [], ys je libovolné
L = map (uncurry f) (zip [] ys) =|3
= map (uncurry f) ([]) =|závorky
= map (uncurry f) [] =|6
= []
P = zipWith f [] ys =|8
= []
L=P
2) xs je libovolné, ys = []
L = map (uncurry f) (zip xs []) =|4
= map (uncurry f) ([]) =|závorky
= map (uncurry f) [] =|6
= []
P = zipWith f xs [] =|9
= []
L=P
3) I.H.: map (uncurry f) (zip xs ys) = zipWith f xs ys
xs = (a:as), ys=(b:bs)
L = map (uncurry f) (zip (a:as) (b:bs)) =|5
= map (uncurry f) ((a,b) : zip as bs) =|7
= (uncurry f) (a,b) : map (uncurry f) (zip as bs) =|závorky
= uncurry f (a,b) : map (uncurry f) (zip as bs) =|1
= f a b : map (uncurry f) (zip as bs)
P = zipWith f (a:as) (b:bs) =|10
= f a b : zipWith f as bs =|I.H.
= f a b : map (uncurry f) (zip as bs)
L = P
Q.E.D
```
<!-- ### 2. opravný -->
## 2020/2021
### riadny
Zadanie: `all xs = foldr (&&) True xs`
```haskell
all' [] = True -- 1
all' (x:xs) = x && all' xs -- 2
```
Dôkaz:
```haskell
foldr' f a [] = a -- 3
foldr' f a (x:xs) = f x (foldr' f a xs) -- 4
foldr (&&) True xs = all xs -- dokazat
1)
xs = []
L = foldr (&&) True [] =|3
= True
P = all [] =|1
= True
L = P
2)
I.H.: foldr (&&) True as = all as
xs = (a:as)
L = foldr (&&) True (a:as) =|4
= (&&) a (foldr (&&) True as) =|IH
= (&&) a (all as) =|prefix->infix
= a && (all as) =|priorita
= a && all as
P = all (a:as) =|2
= a && all as
L = P
Q.E.D.
```
### 2. opravný termín
Zadané:
```haskell
df [] ys = ys -- 1
df xs [] = xs -- 2
df (x:xs) (y:ys) = x:y:df xs ys -- 3
zp _ [] ys = ys -- 4
zp _ xs [] = xs -- 5
zp f (x:xs) (y:ys) = f x y (zp f xs ys) -- 6
```
Dodefinujte funkciu `f` tak, aby platilo `zp f xs ys = df xs ys` a dokážte to pre všetky konečné `xs` a `ys`.
```haskell
f a b l = a:b:l -- 7
zp f xs ys = df xs ys -- dokazat
1)
xs = []
L = zp f [] ys =|4
= ys
P = df [] ys =|1
= ys
L = P
2)
ys = []
L = zp f xs p[] =|5
= xs
P = df xs p[] =|2
= xs
L = P
3)
xs=(a:as)
ys=(b:bs)
I.P.
zp f as bs = df as bs
L = zp f (a:as) (b:bs) =|6
= f a b (zp f as bs) =|7
= a:b:(zp f as bs) =|zbytecne zavorky
= a:b:zp f as bs =|I.P.
= a:b:df as bs
P = df (a:as) (b:bs) =|3
= a:b:df as bs
L=P
Q.E.D.
```
## 2019/2020
### předtermín
Dokázat, že `concat xs = foldr (++) [] xs`, když:
```haskell
concat [] = [] -- 1
concat (x:xs) = x ++ concat xs -- 2
```
Definiční rovnice pro foldr bylo potřeba si nadefinovat.
```haskell
foldr f z [] = z -- 3
foldr f z (x:xs) = f x (foldr f z xs) -- 4
-------
1:
xs = []
L = concat [] =|1
= []
P = foldr (++) [] [] =|3
= []
L=P
-------
2:
I.P.: concat xs = foldr (++) [] xs
xs = (a:as)
L = concat (a:as) =|2
= a ++ concat as =|I.P.
= a ++ foldr (++) [] as
P = foldr (++) [] (a:as) =|4
= (++) a (foldr (++) [] as) =|prefix -> infix
= a ++ (foldr (++) [] as) =|zavorky zbytecne, priorita
= a ++ foldr (++) [] as
L=P
Q.E.D.
```
### riadny
Pre `len xs = foldr (\_ n-> 1+n) 0 xs`
```haskell
len [] = 0 -- 1
len (x:s) = 1 + len xs -- 2
```
Postup:
```haskell
foldr f z [] = z -- 3
foldr f z (x:xs) = f x (foldr f z xs) -- 4
1)
xs = []
L = len [] =|1
= 0
P = foldr (\_ n-> 1+n) 0 [] =|3
= 0
L = P
2)
I.H.: len as = foldr (\_ n-> 1+n) 0 as
xs = (a:as)
L = len (a:as) =|2
= 1 + len as =|I.H.
= 1 + foldr (\_ n -> 1+n) 0 as
P = foldr (\_ n -> 1+n) 0 (a:as) =|4
= (\_ n -> 1+n) a (foldr (\_ n -> 1+n) 0 as) =|beta-reduction
= (\n-> 1+n) (foldr (\_ n -> 1+n) 0 as) =|beta-reduction
= 1 + (foldr (\_ n -> 1+n) 0 as) =|remove-brackets-unnecessary
= 1 + foldr (\_ n -> 1+n) 0 as
L = P
```
### 1. opravny
Pre `map (+1) xs = inc xs`
```haskell
inc [] = [] -- 1
inc (x:xs) = x+1 : inc xs -- 2
```
Postup:
```haskell
map f [] = [] -- 3
map f (x:xs) = f x : map f xs -- 4
1) xs = []
L = map (+1) [] =|3
= []
P = inc [] =|1
= []
L = P
2)
I.H.: map (+1) as = inc as
xs = (a:as)
L = map (+1) (a:as) =|4
= (+1) a : map f as =|I.H.
= (+1) a : inc as =|Haskell notation
= (a+1) : inc as =| priority
= a+1 : inc as
P = inc (a:as) =|2
= a+1 : inc as
L = P
Q,E.D.
```
## 2018/2019
### riadny
Dokážte, že platí `any xs = foldr (||) False xs` když:
```haskell
any [] = False -- 1
any (x:xs) = x || any xs -- 2
```
```haskell
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f z [] = z -- 3
foldr f z (x:xs) = f x (foldr f z xs) -- 4
any xs = foldr (||) False xs
1) xs = []
L = any [] =|1
= False
P = foldr (||) False [] =|3
= False
L = P
I.H.: any xs = foldr (||) False xs
2) xs = (a:as)
L = any (a:as) =|2
= a || any as
P = foldr (||) False (a:as) =| 4
= (||) a (foldr (||) False as) =|I.H.
= (||) a (any as) =|prefix->infi
= a || (any as) =|priorita
= a || any as
L=P
Q.E.D.
```
### 1. opravny
Dokážte, že platí `[] ++ as = as ++ [] = as` když:
```haskell
[] ++ ys = ys -- 1
(x:xs) ++ ys = x:(xs++ys) -- 2
```
Postup:
```haskell
[] ++ as = as ++ [] = as
1)
as = []
L = [] ++ [] =|1
= []
M = [] ++ [] =|2
= []
P = []
L=P=M
2)
I.P. : []++as = as++[] = []
as = (x:xs)
L = [] ++ (x:xs) =|1
= (x:xs)
M = (x:xs) ++ [] =|2
= x:(xs++[]) =|I.P.
= x:([]++xs) =|1
= x:(xs) =|zbytecne zavorky pryc
= x:xs =|zavorky kolem pridat
= (x:xs)
P = (x:xs)
L=P=M
Q.E.D.
```
## 2017/2018
### Radny
```haskell
all' [] = True -- 1
all' (x:xs) = x && all' xs -- 2
foldr' f a [] = a -- 3
foldr' f a (x:xs) = f x (foldr' f a xs) -- 4
Ukazat:
foldr (&&) True xs = all xs
1)
xs = []
L = foldr (&&) True [] =|3
= True
P = all [] =|1
= True
L = P
2)
I.H.: foldr (&&) True as = all as
xs = (a:as)
L = foldr (&&) True (a:as) =|4
= (&&) a (foldr (&&) True as) =|IH
= (&&) a (all as) =|prefix->infix
= a && (all as) =|priorita
= a && all as
P = all (a:as) =|2
= a && all as
L = P
Q.E.D.
```
### Opravny
```haskell
length' a [] = a -- 1
length' a (_:xs) = length' (a+1) xs -- 2
foldl' f a [] = a -- 3
foldl' f a (x:xs) = foldl' f (f a x) xs -- 4
length 0 xs = foldl (\ a _ -> a+1) 0 xs
1)
xs = []
L = length 0 [] =|1
= 0
P = foldl (\ a -> a+1) 0 [] =|3
= 0
L = P
2)
I.P.
forall k in N: length k as = foldl (\ a _ -> a+1) k as
xs = (a:as)
L = length 0 (a:as) =|2
= length (0+1) as =|soucet
= length (1) as =|prebytecne zavorky
= length 1 as =|I.P.
= foldl (\ a _ -> a+1) 1 as
P = foldl (\ a _ -> a+1) 0 (a:as) =|4
= foldl (\ a _ -> a+1) ((\ a _ -> a+1) 0 a) as =|beta_redukce
= foldl (\ a _ -> a+1) ((\ _ -> 0+1) a) as =|beta_redukce
= foldl (\ a _ -> a+1) (0+1) as =|soucet
= foldl (\ a _ -> a+1) (1) as =|prebytecne zavorky
= foldl (\ a _ -> a+1) 1 as
L = P
Q.E.D.
```
## 2016/2017
```haskell
-- apostrofy pouze pro akceptaci v ghci
sum' [] = 0 -- 1
sum' (x:xs) = x + sum' xs -- 2
foldr' f a [] = a -- 3
foldr' f a (x:xs) = f x (foldr' f a xs) -- 4
sum xs = foldr (+) 0 xs
(1) xs = []
L = sum [] =|1
= 0
P = foldr (+) 0 [] =|3
= 0
L=P
2) xs = (a:as)
I.H.
sum as = foldr (+) 0 as
L = sum (a:as) =|2
= a + sum as
P = foldr (+) 0 (a:as) =|4
= (+) a (foldr (+) 0 as) =|I.H.
= (+) a (sum as) =|prefix->infix
= a + (sum as) =|priorita aplikace nejvyssi -> eliminace zavorek
= a + sum as
L = P
Q.E.D.
```
## staršie
1.
Zadanie: `take n as ++ drop n as = as`
riešenie:
```haskell
take :: Int -> [a] -> [a]
take n _ | n <= 0 = [] (1.)
take _ [] = [] (2.)
take n (x:xs) = x : take (n-1) xs (3.)
drop :: Int -> [a] -> [a]
drop n xs | n <= 0 = xs (4.)
drop _ [] = [] (5.)
drop n (x:xs) = drop (n-1) xs (6.)
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys (7.)
(x:xs) ++ ys = x : (xs ++ ys) (8.)
Pro xs = []:
dokazuji: take n [] ++ drop n [] = []
L = take n [] ++ drop n []
= [] ++ drop n [] // použito 2. zleva doprava
= [] ++ [] // použito 5. zleva doprava
= [] // použito 7. zleva doprava
L = P
Předpoklad:
take n as ++ drop n as = as
Pro xs = (a:as):
dokazuji: take n (a:as) ++ drop n (a:as) = (a:as)
L = take n (a:as) ++ drop n (a:as)
= a:(take (n-1) as) ++ drop n (a:as) // použito 3. zleva doprava
= a:(take (n-1) as ++ drop n (a:as) ) // použito 8. zleva doprava
= a:(take (n-1) as ++ drop (n-1) as) // použito 6. zleva doprava
= (a:as) // použit předpoklad
L = P
```
2. Zadanie: `length (xs ++ ys) = length xs + length ys`
<!-- [fituska link](https://fituska.eu/download/file.php?id=11612)
 -->
```haskell
-- Axiomy:
length [] = 0 (1)
length (x:xs) = 1 + length xs (2)
[] ++ ys = ys (3)
(x:xs) ++ ys = x:(xs ++ ys) (4)
-- 1. xs = []
L:
= length ([] ++ ys) = // 3
= length ys
P:
= length [] + length ys = // 1
= 0 + length ys =
= length ys
L = P
-- 2. xs = (a:as)
IH: length (xs ++ ys) = length xs + length ys
L:
= length ((a:as) ++ ys) // 4
= length (a:(as ++ ys)) // 2
= 1 + length (as ++ ys) // IH
= 1 + length as + length ys
P:
= length (a:as) + length ys // 2
= 1 + length as + length ys
L = P
```
3. Zadanie `map f (xs ++ ys) = map f xs ++ map f ys`
[fituska link](https://fituska.eu/download/file.php?id=11651)
4. Zadanie `rev xs = reverse xs`
```haskell
rev [ ] = [ ] (1)
rev (x:xs) = rev xs ++ [x] (2)
reverse xs = rev’ xs [] (3)
rev’ [ ] ys = ys (4)
rev’ (x:xs) ys = rev’ xs (x:ys) (5)
1) xs = []
L = rev xs
= rev [] // 1
= []
P = reverse xs
= reverse [] // 3
= rev’ [] [] // 4
= []
L == P
2) xs = (a:as)
IP : rev as = reverse as
L = rev xs
= rev (a:as) // 2
= rev as ++ [a] // IP
= reverse as ++ [a] // 3
= rev’ as [] ++ [a]
= rev’ as [a]
= rev’ as (a:[])
= rev’ (a:as) []
= reverse (a:as)
= reverse xs = P
```
5. Zadanie `foldr (++) [] xs = ccat xs`
```haskell
(1) foldr f zs [] = zs
(2) foldr f zs (xs:xss) = f xs (foldr f zs xss)
(3) ccat [] = []
(4) ccat (xs:xss) = (++) xs (ccat xss)
----
1. xs = []
L = foldr (++) [] []
= []
P = ccat []
= []
L = P
2. xs = (a:as)
IP/IH: foldr (++) [] xs = ccat xs
L = foldr (++) [] (a:as)
= (++) a (foldr (++) [] (as))
= a:(foldr (++) [] (as))
P = ccat (a:as)
-- TODO
L = P
```
6. Zadanie `map f (xs ++ ys) = (map f xs) ++ (map f ys)`
7. Zadanie `sum (xs ++ ys) == sum xs + sum ys`
```haskell
1: sum [] = 0
2: sum (x:xs) = x + sum xs
3: (++) a b = a ++ b
4: (++) [] ys = ys
5: (++) (x:xs) ys = x:((++) xs ys)
6: 0 + x = x
```
```haskell
1.: xs = []
L = sum ([] ++ ys) // axiom 3 zprava doleva
= sum ((++) [] ys) // axiom 4 zleva doprava
= sum (ys) // odstranění závorek kolem samostatného členu
= sum ys
P = sum [] + sum ys // axiom 1 zleva doprava
= 0 + sum ys // axiom 6 zleva doprava
= sum ys
2.: xs = (a:as)
Indukční předpoklad: sum (as ++ ys) == sum as + sum ys
Dokazujeme: sum ((a:as) ++ ys) == sum (a:as) + sum ys
L = sum ((a:as) ++ ys) // axiom 3 zprava doleva
= sum ((++) (a:as) ys) // axiom 5 zleva doprava
= sum (a:((++) as ys)) // axiom 2 zleva doprava
= a + sum((++) as ys) // axiom 3 zleva doprava
= a + sum(as ++ ys) // indukční předpoklad zleva doprava
= a + sum as + sum ys
P = sum (a:as) + sum ys // axiom 2 zleva doprava
= a + sum as + sum ys
L = P
Q.E.D.
```
8. Zadanie `length (xs ++ ys) == length xs + length ys`
```haskell
1: length [] = 0
2: length (x:xs) = 1 + length xs
3: (++) a b = a ++ b
4. (++) [] ys = ys
5. (++) (x:xs) ys = x:((++) xs ys)
6. 0 + x = x
```
Dokazujeme pomocí strukturální indukce nad proměnnou xs.
První krok: `xs = []`
```haskell
L = length ([] ++ ys) // axiom 3 zprava doleva
= length ((++) [] ys) // axiom 4 zleva doprava
= length (ys) // odstranění závorek kolem samostatného členu
= length ys
P = length [] + length ys // axiom 1 zleva doprava
= 0 + length ys // axiom 6 zleva doprava
= length ys
L = P
```
Druhý krok: `xs = (a:as)`
Indukční předpoklad: `length (as ++ ys) == length as + length ys`
Dokazujeme: `length ((a:as) ++ ys) == length (a:as) + length ys`
```haskell
L = length ((a:as) ++ ys) // axiom 3 zprava doleva
= length ((++) (a:as) ys) // axiom 5 zleva doprava
= length (a:((++) as ys)) // axiom 2 zleva doprava
= 1 + length ((++) as ys) // axiom 3 zleva doprava
= 1 + length (as ++ ys) // indukční předpoklad zleva doprava
= 1 + length as + length ys
P = length (a:as) + length ys // axiom 2 zleva doprava
= 1 + length as + length ys
L = P
Q.E.D.
```
9.
V jazyku Haskell, necht je operátor
```
(++) : [a]-> [a]-> [a]
[] ++ ys = ys
(x:xs) ++ ys = x : (xs++ys)
```
Ukažte, že `xs ++ ys = foldr (:) ys xs` pro danou definici ++ a všechna konečná xs a ys.
Axiomy:
```haskell
1 - [] ++ ys = ys
2 - (x:xs) ++ ys = x : ( xs ++ ys)
3 - foldr f a [] = a
4 - foldr f a (x:xs) = f x (foldr f a xs)
```
Postup:
```haskell
1, ak xs = []
L: [] ++ ys = ys –axiom1 zlava do prava
P: foldr (:) ys [] = ys –axiom 3 zlava do prava
L=P
2, ak xs = (a:as) IP: as ++ ys = foldr (:) ys as
L: (a:as) ++ ys = a : (as ++ ys) –axiom 2 zlava do prava
P: foldr (:) ys (a:as) = – axiom 4 zlava do prava
= (:) a (foldr (:) ys as) = – IP zprava do lava
= (:) a (as ++ ys) = – prepis prefix na infix
= a : (as ++ ys)
L = P
Q.E.D
```
Sign in with Wallet
Connect another wallet