---
# System prepended metadata

title: Rose-Tree
tags: [MP]

---

---
title: Rose-Tree
---
```racket=


(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ć)


