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)…………………………….. 3 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!(Nicerproofstyle) ……………………………. 4 5.2 Doublingall! ……………………………………… 5 5.3 Reversing!……………………………………….. 6 5.4 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!
1
2 LaTeX Basics!
Overleaf is a great resource for learning LaTeX.
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:
1. ordered
2. lists!
3. Inlined Haskell formatting! something :: Int -> Int -> Int -> Int
module Tutorial 02 where main :: IO ()
main = putStrLn “Hello, world!”
doubleAll :: [Int ] → Int
doubleAll [ ] = 0
doubleAll (x : xs) = 2 ∗ x + doubleAll xs
— doubleAll.1 — doubleAll.2
2
3 Proof Styles!
3.1 Example 1 (Recommended)
Proof doubleAll [1,2,3] = 12
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
{ Reflexivity of = } true
3.2 Example 2 (Also recommended)
Proof. doubleAll [1,2,3] = 12
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
3
3.3 Example 3
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
∴ 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
doubleAll.2
doubleAll.2
doubleAll.2
doubleAll.1
doubleAll.2
doubleAll.2
doubleAll.1
∴ we have shown something!
4
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.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
sum′ ::[Int]→Int
sum′ []=0 –sum’.1 sum′ (x:xs)=x+sum′ xs –sum’.2
5.1 Doubling all! (Nicer proof style)
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
{ Reflexivity of = } 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!
5.2 Doubling all!
Let’s prove that doubleAll x = 2 * sum’ x Proof. doubleAll x = 2 * sum’ x
We will use induction! Base Case: []
LHS:
RHS:
doubleAll [] =0
2 * sum’ [] = 2 * 0 =0
by doubleAll.1
by sum’.1
Evaluation
∴ our base case holds!
Induction Step:
Recall our induction step: ∀ xs . doubleAll xs == 2 * sum’ xs LHS:
doubleAll (x:xs)
=2 * x + doubleAll xs
6
by doubleAll.2
RHS:
RHS:
reverse ([] ++ ys) = reverse ys
reverse ys ++ reverse [] = reverse ys ++ []
= reverse ys
by identity of ++
by reverse.1
by identity of ++
2 * sum’ (x:xs)
= 2 * (x + sum’ xs)
= 2 * x + 2 * sum’ xs =2 * x + doubleAll xs
by sum’.2
by Distr. of * over +
by Ind. Hyp.
∴ we have used the induction hypothesis to prove our inductive case, and hence our statement holds! 5.3 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:
∴ 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]
7
by ++.2
by reverse.2
by ind. hyp
by reverse.2
∴ we have shown through induction that this property holds!
5.4 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 Proof. Let’s use induction on xs!
Base Case: []
Our goal is length ([] ++ ys) == length [] ++ length ys.
LHS:
RHS:
length ([] ++ ys) = length ys
length [] + length ys = 0 + length ys
= length ys
by ++.1
by length.1
Evaluation
∴ our base case holds since our LHS = RHS! Induction Step: (x:xs)
Recall our induction hypothesis: ∀ xs, ys . length (xs ++ ys) == length xs + length ys Our goal is length (reverse (x:xs)) == length (x:xs)
LHS:
length ((x:xs) ++ ys)
= length (x:(xs ++ ys)) = length (xs ++ ys) + 1
8
by ++.2
by length.2
RHS:
length (x:xs) + length ys
= length xs + 1 + length ys = length xs + length ys + 1 = length (xs ++ ys) + 1
by length.2
by commutativity of +
by ind. hyp.
∴ we have shown LHS = RHS, and hence our inductive proof holds.
As such, we know that ∀ xs, ys . length (xs ++ ys) == length xs + length ys holds!
9