module Exercise_10 (module Join, module SafeMap) where

{- Library DO NOT CHANGE -}
import SafeMap (SafeMap, empty, update, lookup)
import Join (Field, doJoin, doJoinFormat, parseFormat)
{- End Library -}


{---------------------------------------------------------------------}
{- Aufgabe G10.1 -}

{-
\alpha ist wie in den Folien definiert:
alpha [] = {}
alpha (y:ys) = {y} union (alpha ys)

Simulationseigenschaften:

R_empty: \alpha empty = {}
       : a      empty = {}
empty = []

a empty
== a []                                 -- by def of empty
== {}                                   -- by def of alpha


R_insert: \alpha (insert x xs) = {x} \union \alpha xs
        : a      (insert x xs) = {x}  union a      xs
insert x xs = (x : xs)

a (insert x xs)
== a (x : xs)                           -- by def of insert
== {x} union (a xs)                     -- by def of alpha

R_isin: isin x xs = x \in \alpha xs
      : isin x xs = x \in a      xs
isin x xs = elem x xs

isin x xs
== elem x xs                            -- by implementation
== x \in (a xs)                         -- by L_elem

R_size: size xs = |\alpha xs|
      : size xs = | a     xs|
size xs = length (nub xs)

size xs
== length (nub xs)                      -- by implementation
== |a xs|                               -- by L_length


Hilfslemmata:

Funktionen:

elem x [] = False                               -- elem_Empty
elem x (y:ys) = x == y || elem x ys             -- elem_Cons

nub [] = []                                     -- nub_Empty
nub (y:ys) =                                    -- nub_Cons
        if y `elem` ys then nub ys
        else {- not elem -} y : (nub ys)

---

L_elem(xs): elem x xs = x \in a xs
Proof by structural induction on xs

Base case: L_elem([])
To show: elem x [] = x \in a []
elem x []
== False                                        -- by elem_Empty

x \in a []
== x \in {}                                     -- by alpha
== False                                        -- by {}

Induction step: L_elem(ys) => L_elem(y : ys)
IH: elem x ys = x \in (a ys)
To show: elem x (y:ys) = x \in a (y:ys)
elem x (y:ys)
== x == y || elem x ys                          -- by elem_Cons
== x == y || x \in (a ys)                       -- by IH

x \in a (y:ys)
== x \in ({y} union (a ys))                     -- alpha_Cons
== x \in {y} || x \in (a ys)                    -- by union
== x == y || x \in (a ys)                       -- by basic property

qed

---


L_length(xs): length (nub xs) = |a xs|
Proof by structural induction on xs

Base case: L_length([])
To show: length (nub []) = |a []|
length (nub [])
== length []                                    -- by nub_Empty
== 0                                            -- by def of length

|a []|
== |{}|                                         -- by alpha
== 0                                            -- by def of ||

Induction step: L_length(ys) => L_length(y : ys)
IH: length (nub ys) = |a ys|
To show: length (nub (y:ys)) = |a (y:ys)|
Proof by cases
case: y `elem` ys
        length (nub (y:ys))
        == length (nub ys)                      -- by nub_Cons
        == |a ys|                               -- IH

        |a (y:ys)|
        == |{y} union a ys|                     -- alpha_Cons
        == |(a ys)|                             -- by basic property

case: not (y `elem` ys)
        length (nub (y:ys))
        == length (y : (nub ys))                -- by nub_Cons
        == 1 + length [] + length (nub ys)      -- by length_Cons
        == 1 + length (nub ys)                  -- by length_Empty
        == 1 + |a ys|                           -- IH

        |a (y:ys)|
        == |{y} union a ys|                     -- alpha_Cons
        == |{y}| + |a ys|                       -- by def of union, case
        == 1 + |a ys|                           -- by def of ||

qed

-}



{---------------------------------------------------------------------}
{- Aufgabe G10.2 -}

{- siehe SetPairList.hs -}



{---------------------------------------------------------------------}
{- Aufgabe G10.3 -}

{- siehe Queue.hs und SuperQueue.hs -}

{-
Simulationseigenschaften zu beweisen:

    \alpha empty = []
    isEmpty q = \alpha q == []
    \alpha (enqueue x q) = \alpha q ++ [x]
    ~ isEmpty q ==> \alpha (dequeue q) = (head (\alpha q), tail (\alpha q))
    q == q' = \alpha q == \alpha q'

Definition von \alpha:

    \alpha (Queue front kcab) = front ++ reverse kcab

Beweis fuer "empty":

    \alpha empty
      = \alpha (Queue [] [])                -- by def of empty
      = [] ++ reverse []                    -- by def of \alpha
      = []                                  -- by def of reverse, ++

Beweis fuer "isEmpty":

    Hilfssatz: q == Queue [] [] = \alpha q == []

    isEmpty q
      = q == Queue [] []                    -- by def of isEmpty
      = \alpha q == []                      -- by lemma

Beweis fuer "enqueue":

    Sei q = Queue front kcab                -- by exhaustivity of constructor

    \alpha (enqueue x q)
      = \alpha (enqueue x (Queue front kcab))
                                            -- by def of q
      = \alpha (Queue (front (x : kcab)))   -- by def of enqueue
      = front ++ reverse (x : kcab)         -- by def of \alpha
      = front ++ (reverse kcab ++ [x])      -- by def of reverse
      = (front ++ reverse kcab) ++ [x]      -- by commutativity of ++
      = \alpha (Queue front kcab) ++ [x]    -- by def of \alpha
      = \alpha q ++ [x]                     -- by def of q

Hilfslemma L:

    Zu beweisen: \alpha (Queue [] kcab) = \alpha (Queue (reverse kcab) [])

    \alpha (Queue [] kcab)
      = [] ++ reverse kcab                  -- by def of \alpha
      = reverse kcab                        -- by def of ++

    \alpha (Queue (reverse kcab) [])
      = reverse kcab ++ []                  -- by def of \alpha
      = reverse kcab                        -- by def of ++

Beweis fuer "dequeue":

    Annahme: ~ isEmpty q

    Sei q = Queue front kcab

    Fallunterscheidung auf front und kcab:

    Fall front = [], kcab = []:
      ~ isEmpty (Queue front kcab)
        = ~ isEmpty (Queue [] [])
        = False
      Nichts mehr zu beweisen, weil die Annahme nicht erfuellt ist.

    Fall front /= []:
      \alpha (dequeue q)
        = \alpha (dequeue (Queue front kcab))
                                            -- def of q
        = \alpha (head front, Queue (tail front) kcab)
                                            -- def of dequeue (2nd equation)
        = (head front, \alpha (Queue (tail front) kcab))
                                            -- \alpha is an homomorphism

      Es bleibt zu beweisen, dass

        head front = head (\alpha q)
        \alpha (Queue (tail front) kcab) = tail (\alpha q)

        head (\alpha q)
          = head (\alpha (Queue front kcab))  -- def of q
          = head (front ++ reverse kcab)      -- def of \alpha
          = head front                        -- basic prop of head, front /= []

        \alpha (Queue (tail front) kcab)
          = tail front ++ reverse kcab        -- def of \alpha

        tail (\alpha q)
          = tail (\alpha (Queue front kcab))  -- def of q
          = tail (front ++ reverse kcab)      -- def of \alpha
          = tail front ++ reverse kcab        -- basic prop of tail, front /= []

    Fall front = [], kcab /= []:
      \alpha (dequeue q)
        = \alpha (dequeue (Queue front kcab)) -- def of q
        = \alpha (dequeue (Queue [] kcab))    -- assumption front = []
        = \alpha (dequeue (Queue (reverse kcab) []))
                                              -- def of dequeue (1st equation)
        = (head (\alpha (Queue (reverse kcab) [])),
           tail (\alpha (Queue (reverse kcab) [])))
                                              -- by reduction to already proved
                                              -- case, reverse kcab /= []
        = (head (\alpha (Queue [] kcab)), tail (\alpha (Queue [] kcab)))
                                              -- by lemma L (twice)
        = (head (\alpha q), tail (\alpha q))  -- by def of q (twice)

Beweis fuer ==:

    Zu beweisen: q == q' = \alpha q == \alpha q'

    Seien q = Queue (front kcab)
          q' = Queue (front' kcab')

    q == q'
      = Queue (front kcab) == Queue (front' kcab')
                                              -- by def of q, q'
      = toList (Queue (front kcab)) == toList (Queue (front' kcab'))
                                              -- by def of ==
      = front ++ reverse kcab == front' ++ reverse kcab'
                                              -- by def of toList

    \alpha q == \alpha q'
      = \alpha (Queue (front kcab)) == \alpha (Queue (front' kcab'))
                                              -- by def of ==
      = front ++ reverse kcab == front' ++ reverse kcab'
                                              -- by def of \alpha

-}



{---------------------------------------------------------------------}
{- Aufgabe H10.1 -}

{- siehe SafeMap.hs -}



{---------------------------------------------------------------------}
{- Aufgabe H10.2 -}

{- siehe Join.hs -}



{---------------------------------------------------------------------}
{- Aufgabe H10.3 -}

{- siehe Morsi.hs -}