Contents
This is a nice title!
My name!! January 28, 2021
1 Introduction 1
2 LaTeX Basics! 1
3 Proof Styles! 2
3.1 Example1(Recommended) ………………………………. 2 3.2 Example2(Alsorecommended)…………………………….. 2 3.3 Example3……………………………………….. 3 3.4 Example4……………………………………….. 3 3.5 Example5……………………………………….. 4
4 Induction 4
4.1 WeakvsStrong? ……………………………………. 4
5 Proofs 4
5.1 Doublingall! ……………………………………… 4 5.2 Reversing!……………………………………….. 6 5.3 Lengths!………………………………………… 7
1 Introduction
Overleaf is a great resource for learning LaTeX This is information related to my assignment! I might want to write some information here. It might be important!
2 LaTeX Basics!
Overleaf is a great resource for learning LaTeX.
1
1. 2. 3.
3
3.1
ordered
lists!
Inlined Haskell formatting! something :: Int -> Int -> Int -> Int
I like space between my lines. But they don’t appear!!!
I need to remember that if I want spaces between my words, that I need to double space!
But sometimes I need to use other methods (“\\” after my sentences) to get extra spacing!
Maybe I want to write a quote! ”Something” – Someone
…wait… something looks off about those quotes! “Something” – Someone (This looks better now!) I can make stuff bold!
I can make stuff large and bold!
I can make stuff HUGE and monospaced!
Some words: We
can
make
unordered
lists
Oh! We can also make:
module Tutorial 02 where main :: IO ()
main = putStrLn “Hello, world!”
Proof Styles!
Example 1 (Recommended)
Proof doubleAll [1,2,3] = 12
2
3.2 Example 2 (Also recommended)
Proof. doubleAll [1,2,3] = 12
∴ LHS = RHS!
3.3 Example 3
doubleAll [1, 2, 3] = 12 ≡ { doubleAll.2 }
2 * 1 + doubleAll [2, 3] = 12 ≡ { doubleAll.2 }
2 * 1 + 2 * 2 + doubleAll [3] = 12 ≡ { doubleAll.2 }
2 * 1 + 2 * 2 + 2 * 3 + doubleAll [] = 12
≡ ≡ ≡
{ doubleAll.1 }
2 * 1 + 2 * 2 + 2 * 3 + 0 = 12
{ Evaluation } 12 = 12
{ Evaluation } true
doubleAll [1, 2, 3] = { doubleAll.2 }
2 * 1 + doubleAll [2, 3] = { doubleAll.2 }
2 * 1 + 2 * 2 + doubleAll [3] = { doubleAll.2 }
2 * 1 + 2 * 2 + 2 * 3 + doubleAll []
= =
{ doubleAll.1 } 2*1+2*2+2*3+0
{ Evaluation } 12
doubleAll [1,2,3]
= { doubleAll.2 }
2∗1+doubleAll [2,3]
3
= { doubleAll.2 } 2∗1+2∗2+doubleAll [3]
= { doubleAll.2 } 2∗1+2∗2+2∗3+doubleAll []
= { doubleAll.1 } 2∗1+2∗2+2∗3+0
= { Evaluation } 12
∴ we have shown something! 3.4 Example 4
Proof. doubleAll [1,2,3] = 12
doubleAll [1,2,3] = 2 * 1 + doubleAll [2, 3]
=2 * 1 + 2 * 2 + doubleAll [3]
= 2 * 1 + 2 * 2 + 2 * 3 + doubleAll [] =2*1+2*2+2*3+0 Evaluation = 12
∴ we have shown something! 3.5 Example 5
Proof. doubleAll [1,2,3] = 12
doubleAll [1,2,3]
= 2 * 1 + doubleAll [2, 3]
=2 * 1 + 2 * 2 + doubleAll [3]
= 2 * 1 + 2 * 2 + 2 * 3 + doubleAll [] =2*1+2*2+2*3+0 Evaluation = 12
∴ we have shown something! 4 Induction
A mathematical technique for proving statements using inductive sets (e.g., the natural numbers!)! Induction is broken up into 2 steps; proving the base case(s), and proving the inductive cases. In the base case, we need to directly prove the statements for specific values, but in the inductive cases, we get to assume the statement holds for “previous” values!
4
doubleAll.2
doubleAll.2
doubleAll.1
doubleAll.2
doubleAll.2
doubleAll.2
doubleAll.1
4.1 Weak vs Strong?
With weak induction, we assume the statement holds for only the “n-th” and prove the statement holds for the “(n+1)-th” using the “n-th” (our inductive hypothesis). With strong induction, we assume the statement holds for all cases before the “(n+1)-th” hold and prove it using the previous ones (our inductive hypothesis ).
5 Proofs
5.1
doubleAll :: [Int ] → Int
doubleAll [ ] = 0
doubleAll (x : xs) = 2 ∗ x + doubleAll xs
sum′ ::[Int]→Int
sum′ []=0 –sum’.1 sum′ (x:xs)=x+sum′ xs –sum’.2
Doubling all!
— doubleAll.1 — doubleAll.2
Let’s prove that doubleAll x = 2 * sum’ x Proof. doubleAll x = 2 * sum’ x
We will use induction! Base Case: []
∴ our base case holds!!!!
Induction Case: We want to prove: (x:xs)
Weassume∀xs . doubleAll xs = 2 * sum’ xs
5
≡ ≡ ≡ ≡
doubleAll [] = 2 * sum’ [] { sum.1 }
doubleAll [] = 2 * 0 { doubleAll.1 }
0=2*0
{ Evaluation } 0=0
{ Evaluation } true
We want to prove is: ∀x.∀xs. doubleAll (x:xs) = 2 * sum’ (x:xs)
≡ ≡ ≡ ≡ ≡
doubleAll (x:xs) = 2 * sum’ (x:xs) { sum’.2 }
doubleAll (x:xs) = 2 * (x + sum’ xs) { doubleAll.2 }
2 * x + doubleAll xs = 2 * (x + sum’ xs)
{ Evaluate }
2 * x + doubleAll xs = 2 * x + 2 * sum’ xs
{ Ind. Hyp. }
2 * x + doubleAll xs = 2 * x + doubleAll xs
{ Reflexivity of = } true
∴ we have shown through induction that this statement holds!
6
5.2 Reversing!
Let’s prove that reverse (xs ++ ys) == reverse ys ++ reverse xs! where we define reverse as:
reverse :: [a] -> [a]
reverse [] = [] — reverse.1
reverse (x:xs) = reverse xs ++ [x] — reverse.2
Proof. Let’s use induction!
Base Case: []
Our Goal: reverse ([] ++ ys) == reverse ys ++ reverse [] LHS:
RHS:
reverse ([] ++ ys) = reverse ys
reverse ys ++ reverse [] = reverse ys ++ []
= reverse ys
by identity of ++
by reverse.1
by identity of ++
∴ our base case holds as the LHS = RHS.
Induction Step: (x:xs)
Note our induction hypothesis: ∀ xs ∀ ys . reverse (xs ++ ys) == reverse ys ++ reverse xs
Our goal: reverse ((x:xs) ++ ys) == reverse ys ++ reverse (x:xs) LHS:
RHS:
reverse ((x:xs) ++ ys)
= reverse (x:(xs ++ ys))
= reverse (xs ++ ys) ++ [x]
= reverse ys ++ reverse xs ++ [x]
reverse ys ++ reverse (x:xs)
= reverse ys ++ reverse xs ++ [x]
by ++.2
by reverse.2
by ind. hyp
by reverse.2
∴ we have shown through induction that this property holds!
7
5.3 Lengths!
First, let us define length!
length :: [a] -> Int
length [] = 0 — length.1
length (x:xs) = length xs + 1 — length.2
Now, let’s prove the following statement: ∀ xs, ys . length (xs ++ ys) == length xs + length ys
8