* Sheet 2 - Natural Deduction

Important points:
  - parenthesize correctly: quantifiers extend as far to the right as
    possible; i.e. up to the enclosing parenthesis, if there is any, and
    fully to the right, otherwise.

  - be explicit about all reasoning steps; i.e. no logical transformations
    and all steps must be justified by one of the rules.

  - Be precise when matching rules:
    * operators must match (outermost operators)
    * CHECK side conditions on all-I, ex-E

Many of you got 3.b wrong:
You did not check the side-conditions on ∃-E,
i.e., ∃-I and ∃-E were done in the wrong order.

* Sheet 2 - Natural Deduction

  Obviously wrong:  ∃ x. P(x) ⊢ P(t)
       also wrong:  ∃ x. P(x) ⊢ P(x)

  Obviously right:   ∃ x. P(x) ∧ Q ⊢ Ex y. P(y)

   Wrong proof: The rule ∃-E does NOT SATISFY its SIDE CONDITION!

   Let Γ :=  ∃ x. P(x) ∧ Q

                                         ====================== Ax
                           [  WRONG:  ]  Γ,P(y) ∧ Q ⊢ P(y) ∧ Q
   ================== Ax   [x NOT ARB.]  ====================== ∧-EL
   Γ ⊢ ∃ y. P(y) ∧ Q           \====>    Γ,P(y) ∧ Q ⊢ P(x)     
   ============================================================ ∃-E
   Γ ⊢ P(x)
   ========================= ∃-I
   ∃ x. P(x) ∧ Q ⊢ ∃ y. P(y)

* Sheet 2 - Natural Deduction

  Formulas that you can prove valid by violating the side condition:
  Obviously wrong:  ∃ x. P(x) ⊢ P(t)   
       also wrong:  ∃ x. P(x) ⊢ P(x)

  Obiously right:   ∃ x. P(x) ∧ Q ⊢ Ex y. P(y)

    Correct proof:
    Let Γ :=  ∃ x. P(x) ∧ Q
         
                             ======================= Ax
                             Γ, P(x) ∧ Q ⊢ P(x) ∧ Q
                             ======================= ∧-EL
                             Γ, P(x) ∧ Q ⊢ P(x)
      ================= Ax   ======================== ∃-I
      Γ ⊢ ∃ x. P(x) /\ Q      Γ, P(x) ∧ Q ⊢ ∃ y. P(y)
      ==================================================== ∃-E**
      ∃ x. P(x) ∧ Q ⊢ ∃ y. P(y)

* Sheet 2 - Exercise 4
    Haskell style suggestions:
    
    if x==0 then True else False => x==0
    foo x | <expr> = True        => foo x = <expr>
          | otherwise = False

* Sheet 3

** Induction over Nat
** Recursive functions on lists
** foldr
** Induction over lists

* Induction I

  *Example*: sum n computes Σ^ⁿ_i=1 i

  sum 0 = 0                      —- sum.1
  sum n = sum (n-1) + n          —- sum.2

  *Lemma*: ∀ n∈Nat. sum n = n*(n+1)/2

Prove the Lemma by induction.

* Induction II

  *Example*: sum n computes Σ^ⁿ_i=1 i

  sum 0     = 0                  —- sum.1
  sum n     = sum (n-1) + n      —- sum.2  n /= 0

  *Lemma*: ∀ n∈Nat. sum n = n*(n+1)/2

  *Proof*:
  Let P(n) ≡ (sum n = n*(n+1)/2).
  We prove ∀ n∈Nat. P(n) by induction.

  _Base Case_: We first prove P(0).

    sum 0
  = 0          —- sum.1
  = 0*(0+1)/2  –- arith

  _Step Case_:
  Let n∈Nat be arbitrary and assume that P(n) holds.
  Show P(n+1):

    sum (n+1)
  = sum (n+1-1) + (n+1)      —- sum.2
  = sum n       + (n+1)      —- arith
  = n*(n+1)/2 + (n+1)        —- P(n)
  = (n+2)*(n+1)/2            —- arith
  = (n+1)*((n+1) + 1)/2      —- arith

* List Functions I: Basic List Functions

Many list functions predefined in Prelude and the Data.List module

  -- test if list is equal to the empty list ([])
  null :: [a] -> Bool
  null [] = True
  null _  = False
  
  -- return head of the list
  head :: [a] -> a
  head []    = error "head: not defined on empty list"
  head (x:_) = x

  tail :: [a] -> [a]
  tail []    = error "tail: not defined on empty list"
  tail (_:xs) = xs

  (:) :: a -> [a] -> [a]
  
  -- return the last element of the list
  last :: [a] -> a

  -- return all elements of the list except the last one
  init :: [a] -> [a]


  (++) :: [a] -> [a] -> [a]
  length :: [a] -> Int
  reverse :: [a] -> [a]
  (!!) :: Int -> [a] -> a -- zero-based

  Exercise: Implement 3 of the functions listed above. E.g., last, init, ...

* List Functions I: Basic List Functions

> last' :: [a] -> a
> last' [] = error "last': not defined on empty list"
> last' (x:[]) = x
> last' (_:xs) = last' xs

(.) :: (b -> c) -> (a -> b) -> (a -> c)


> last'' = head . reverse

Evaluation example:
  last'' [1,2] = (head.reverse) [1,2] = head (reverse [1,2]) ... = 
  head [2,1] = 2

> init' :: [a] -> [a]
> init' [] = error "init': not defined on empty lists"
> init' [a] = []
> init' (y:x:xs) = y:init' (x:xs)

> init'' :: [a] -> [a]
> init'' = (reverse . tail . reverse)

> init''' :: [a] -> [a]
> init''' x = (reverse . tail . reverse) x

add1 x = x + 1
map add1 [1,2,3]

eqComma ',' = True
eqComma _ = False
break eqComma "asdasdfas"

Infix: +, ++, :
to use infix as prefix: (+)
Prefix: map, elem
to use prefix as infix: `map`, `elem`

breakComma = break (==',')

* List Functions: Misc

| reverse :: [a] -> [a]               | reverse [1,2,3] = [3,2,1]                    |
| map :: (a -> b) -> [a] -> [b]       | map (+1) [1,2,3] = [2,3,4]                   |
| intersperse :: a -> [a] -> [a]      | intersperse ',' "123" ="1,2,3"               |
| intercalate :: [a] -> [ [a] ]-> [a] | intercalate ", " ["Haskell", "C#", "Java"] = |
|                                     | "Haskell, C#, Java"                          |
| take :: Int -> [a] -> [a]           | take 3 [1..] = [1,2,3]                       |
| drop :: Int -> [a] -> [a]           | drop 7 [1..10] =  [8,9,10]                   |
| splitAt :: Int -> [a] -> ([a], [a]) | splitAt 3 "FOO,BAR" = ("FOO",",BAR")         |
| break ::                            | break (==',') "FOO,BAR" = ("FOO",",BAR")     |
| (a -> Bool) -> ([a] -> ([a], [a]))  |                                              |
| elem :: Eq a => a -> [a] -> Bool    | 1 `elem` [2,3,1] = True                      |
| concat :: [ [a] ]-> [a]             | concat [[1],[2,3]] = [1,2,3]                 |

Exercise: Implement 2 of the functions listed above.

* List Functions: Misc

> splitAt :: Int -> [a] -> ([a], [a])
> splitAt n xs =  (take n xs, drop n xs)

> elem' :: Eq a => a -> [a] -> Bool
> elem' _ [] = False
> elem' y (x:xs) = x == y || elem y xs

> concat' :: [ [a] ] -> [a]
> concat' [] = []
> concat' (x:xs) = x ++ concat xs







































* List Functions: Higher-Order Functions

  map :: (a -> b) -> [a] -> [b]

  takeWhile :: (a -> Bool) -> [a] -> [a]

  dropWhile :: (a -> Bool) -> [a] -> [a]

  filter :: (a -> Bool) -> [a] -> [a]

  partition :: (a -> Bool) -> [a] -> ([a], [a])

  concatMap :: (a -> [b]) -> [a]  -> [b]