---
title: Rose-Tree
---

(define-type (tree 'a)
  (leaf)
  (node [elem  : 'a]
        [left  : (tree 'a)]
        [right : (tree 'a)]))

(define (flatten-aux [t : (tree 'a)] [l : (Listof 'a)]) : (Listof 'a)
  (type-case (tree 'a) t
    [(leaf) l]
    [(node e t1 t2)
      (flatten-aux t1
                   (cons e (flatten-aux t2 l)))]))
  

(define (flatten [t : (tree 'a)])
  (flatten-aux t '[]))


(define-type (rose-tree 'a)
  (rose-node [elem     : 'a]
             [children : (Listof (rose-tree 'a))]))

1) Sformuluj zasade indukcji strukturalnej dla typu danych rose-tree
2) Udowodnij ze
(∀ T : Type),
(∀ t : tree T),
(∀ l : Listof T),
(flatten-aux t l) ≡ (append (flatten-aux t '[]) l)
3) Udowodnij prawo fuzji dla foldr'a tzn
(∀ A : Type),
(∀ B : Type),
(∀ C : Type),
(∀ f : B -> C),
(∀ g : A -> B -> B),
(∀ h : A -> C -> C),
(∀ b : B)
[(f (g x y)) ≡ (h x (f y))] =>
[(∀ xs : Listof A) (f (foldr g b xs)) ≡ (foldr h (f b) xs)]

1.
Niech P bedzie wlasnosc RoseTree, a Q wlasnoscia list drzew t.ze

- ∀ x mamy P((elem))
- ∀ wartosci xs, jesli zachodzi Q(xs) dla dowolnej listy xs ⟹ P((children xs))
- zachodzi Q(empty)
- Dla dowolnych t ts jesli P(t) ∧ Q(ts) ⟹ Q(cons t ts)

2. Udowodnij ze
(∀ T : Type),
(∀ t : tree T),
(∀ l : Listof T),
(flatten-aux t l) ≡ (append (flatten-aux t '[]) l)

#### P(t) := (flatten-aux t l) ≡ (append (flatten-aux t '[]) l)

Niech P bedzie dla typy Tree:
Niech P bedzie wlasnoscia drzew t.ze:
- P((leaf))
- Dla dowolnych wartosci l x r, jesli P(l) i P(r), to P((node l x r))

Wowczas zachodzi P(t) dla ∀ t

Baza:
P((leaf))
L = (flatten-aux (leaf) l) = l
P = (append (flatten-aux (leaf) '[]) l) = (append '() l) = l
L $\equiv$ P

Krok ind.
Zalozenie:
IHt1 : $\forall$ l : (flatten-aux t1 l) ≡ (append (flatten-aux t1 '[]) l)
IHt2 : $\forall$ l : (flatten-aux t2 l) ≡ (append (flatten-aux t2 '[]) l)

Teza: Dla każdej listy l: P((node t1 x t2))
D-d:
Biorę dowolną liste l
P((node t1 x t2)) = (flatten-aux (node t1 x t2) l) ≡ (append (flatten-aux (node t1 x t2) '[]) l)
L = (flatten-aux (node t1 x t2) l) ≡
≡ (flatten-aux t1 (cons x (flatten-aux t2 l))) ≡ IHt1
≡ (append (flatten-aux t1 null) (cons x (flatten-aux t2 l))) = IHt2
≡ (append (flatten-aux t1 null) (cons x (append (flatten-aux t2 null) l)))

P = (append (flatten-aux (node t1 x t2) '[]) l)
≡ (append (flatten-aux t1 (cons x (flatten-aux t2 '[]))) l) ≡ (z lematu Magic)
≡ (append (flatten-aux t1 null) (append (cons x (flatten-aux t2 null)) l)) (z def append'aa)
≡ (append (flatten-aux t1 null) (cons x (append (flatten-aux t2 null) l))) ≡ L

Lemat Magic:
H := (flatten-aux t1 (cons x (flatten-aux t2 '[])))
= (append (flatten-aux t1 null) (cons x (flatten-aux t2 null)))
Korzystając z IHt1 (widać)