kanak

 {- Discrete Mathematics with a Computer
   Chapter 01: Introduction
-}
module Introduction where
import Data.Maybe

--------------------------------------------------------------------------------
-- Ex 1 are the following true or false

ex11 = True && False  -- False

kanak

Chapter 02 Equational Reasoning
of Discrete Mathematics Using a Computer

--------------------------------------------------------------------------------
Theorem 1 (length (++))
Let xs, ys :: [a] be arbitrary lists. 
Then length (xs ++ ys) = length xs + length ys
- Proof is by Induction, chapter 4

--------------------------------------------------------------------------------

kanak

{- Discrete Mathematics Using a Computer
   Chapter 03 : Recursion
-}

-- ================================================================================
-- 3.1 Recursion over Lists
-- Ex 1: Write a function that copies its list argument. copy [2] -> [2]

copy :: [a] -> [a]
copy [] = []

kanak

#+TITLE: DiscreteMathComputer 04 - Induction
#+DATE:
#+LATEX_HEADER: \usepackage{fullpage}
#+LATEX_HEADER: \usepackage{tgschola}
#+OPTIONS: H:3 toc:nil

* Introduction
  - Want to prove that every element $x$ of a set $X$ has a property $P$
  - i.e. $\forall x \in X, P(x)$
  - Direct proof for each element doesn't work because we want finitely long proof even for an infinite set

kanak

{- Discrete Mathematics Using a Computer
   Chapter 05: Trees
-}

-- =============================================================================
-- 5.1 Components of a Tree

{-
Definition 1: A tree is either an empty tree or it is a node together with a sequence of trees.

kanak

#+TITLE: DiscreteMathComputer 06 - Propositional Logic
#+DATE:
#+LATEX_HEADER: \usepackage{fullpage}
#+LATEX_HEADER: \usepackage{tgschola}
#+OPTIONS: H:3 toc:nil

* Chapter Outline
  - Difficulties with informal logic
  - Propositional logic (one type of formal logic)
  - Three mathematical systems for reasoning about propositions:

kanak

{- Discrete Math Using a Computer
   Chapter 6: Propositional Logic
   Section 6.6 - Proof Checking by Computer

   In this section, STDM's proof checker is used to verify some proofs
-}

import Stdm
--------------------------------------------------------------------------------
-- Theorem 55: |- Q => ((P ^ R) => (R ^ Q))

kanak

{- Discrete Math Using a Computer
   Chapter 6: Propositional Logic
  Review Exercise
-}

import Stdm

--------------------------------------------------------------------------------
-- Exercise 34: Prove A ^ ~A |- False

kanak

#+TITLE: DiscreteMathComputer 07-Predicate Logic
#+DATE:
#+LATEX_HEADER: \usepackage{fullpage}
#+OPTIONS: H:3 toc:nil

* Introduction: Why Predicates Logic
  - Want to make the statement that everything has a certain property
    + e.g. "All men are mortal"
  - Propositional Logic doesn't provide us any structure to express this
    + e.g. could say "P = all men are mortal"

kanak

{- Discrete Mathematics Using a Computer
   Chapter 08: Sets
-}

module Sets where

type Set a = [a]
-- Note, this definition prevents us from having heterogeneous sets
-- TODO: use hlist (http://homepages.cwi.nl/~ralf/HList/) ?