\documentclass{article}
% Do you like comments?
% I like comments!
% Let’s change our page’s dimensions!!!
\usepackage[left=1in,right=1in]{geometry}
\usepackage{scrextend}
\usepackage{color}
\usepackage{hyperref}
\usepackage{url}
\usepackage{amsfonts}
\usepackage{amsmath,amssymb}
\usepackage{amsthm}
% If you don’t want to \usepackage{amsthm}, you can create your own proof macro!
%\newenvironment{proof}{\paragraph{Proof}}{\hfill$\square$}
%include polycode.fmt
%options ghci
%Credits to Musa Al-hassy for the below scripts!!!%
\def\stepWith#1#2{ \\ #1 & \quad \color{black}{\{\;\text{#2}\;\}} \\ & }
\def\step#1{ \stepWith{\equiv}{#1} }
\def\commentbegin{\quad\{\ }
\def\commentend{\}}
\def\stepEq#1{ \stepWith{=}{#1} }
\begin{document}
% Fill up some information for our title
\title{This is a nice title!}
\author{My name!!}
\date{\today}
% create our title
\maketitle
% generate a table of contents using the sections
\tableofcontents
% You can create new pages!
%\newpage
\section{Introduction}
% unordered list
\begin{itemize}
\item \href{https://www.overleaf.com/}{Overleaf} is a great resource for learning LaTeX
\item This is information related to my assignment!
\item I might want to write some information here.
\item It might be important!
\end{itemize}
\section{LaTeX Basics!}
\href{https://www.overleaf.com/}{Overleaf} is a great resource for learning LaTeX.\\
I like space between my lines.
But they don’t appear!!!
% double spacing
I need to remember that if I want spaces between my words, that I need to double space!\\
% include \\ in text-mode AND end sentences!
But sometimes I need to use other methods (“\textbackslash\textbackslash” after my sentences) to get extra spacing!\\ % e.g., \\
% italics
Maybe I want to write a quote! \textit{“Something” – Someone}\\
% quotes
…wait… something looks off about those quotes! \textit{“Something” – Someone} (This looks better now!)\\
% bold
\textbf{I can make stuff bold!}
% bold and large
{\Large\textbf{I can make stuff large and bold!}\par}
% monospace font and huge
{\Huge\texttt{I can make stuff HUGE and monospaced!}\par}
% unordered list
\textbf{Some words}:
\begin{itemize}
\item We
\item can
\item make
\item unordered
\item lists
\end{itemize}
% ordered list
\textbf{Oh! We can also make:}
\begin{enumerate}
\item ordered
\item lists!
% inlined haskell formatting
\item Inlined Haskell formatting! @something :: Int -> Int -> Int -> Int@
\end{enumerate}
% the haskell code!
% NOTE: We can place it anywhere we want! Doesn’t need to be at the top of the file!
\begin{code}
module Tutorial_02 where
main :: IO ()
main = putStrLn “Hello, world!”
\end{code}
\section{Proof Styles!}
\subsection{Example 1 (Recommended)}
\textbf{Proof} @doubleAll [1,2,3] = 12@
\begin{align*}&
@doubleAll [1, 2, 3] = 12@
\step{@doubleAll.2@}
@2 * 1 + doubleAll [2, 3] = 12@
\step{@doubleAll.2@}
@2 * 1 + 2 * 2 + doubleAll [3] = 12@
\step{@doubleAll.2@}
@2 * 1 + 2 * 2 + 2 * 3 + doubleAll [] = 12@
\step{@doubleAll.1@}
@2 * 1 + 2 * 2 + 2 * 3 + 0 = 12@
\step{Evaluation}
@12 = 12@
\step{Evaluation}
@true@
\end{align*}
\subsection{Example 2 (Also recommended)}
\begin{proof} @doubleAll [1,2,3] = 12@
\begin{align*}&
@doubleAll [1, 2, 3]@
\stepEq{@doubleAll.2@}
@2 * 1 + doubleAll [2, 3]@
\stepEq{@doubleAll.2@}
@2 * 1 + 2 * 2 + doubleAll [3]@
\stepEq{@doubleAll.2@}
@2 * 1 + 2 * 2 + 2 * 3 + doubleAll []@
\stepEq{@doubleAll.1@}
@2 * 1 + 2 * 2 + 2 * 3 + 0@
\stepEq{Evaluation}
@12@
\end{align*}
$\therefore$ LHS = RHS!
\end{proof}
\subsection{Example 3}
\begin{addmargin}[1.5em]{0em}
\begin{spec}
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
\end{spec}
\end{addmargin}
$\therefore$ we have shown something!
\subsection{Example 4}
\begin{proof} @doubleAll [1,2,3] = 12@
\begin{align*}
@doubleAll [1,2,3]@ &= @2 * 1 + doubleAll [2, 3]@ & \texttt{@doubleAll@.2}\\
&= @2 * 1 + 2 * 2 + doubleAll [3] @ & \texttt{@doubleAll@.2} \\
&= @2 * 1 + 2 * 2 + 2 * 3 + doubleAll [] @ & \texttt{@doubleAll@.1} \\
&= @2 * 1 + 2 * 2 + 2 * 3 + 0@ & \texttt{Evaluation} \\
&= @12@ & \\
\end{align*}
$\therefore$ we have shown something!
\end{proof}
\subsection{Example 5}
\begin{proof} @doubleAll [1,2,3] = 12@
\begin{align*}
&@doubleAll [1,2,3]@ & \texttt{@doubleAll@.2}\\
&= @2 * 1 + doubleAll [2, 3]@ & \texttt{@doubleAll@.2}\\
&= @2 * 1 + 2 * 2 + doubleAll [3] @ & \texttt{@doubleAll@.2} \\
&= @2 * 1 + 2 * 2 + 2 * 3 + doubleAll [] @ & \texttt{@doubleAll@.1} \\
&= @2 * 1 + 2 * 2 + 2 * 3 + 0@ & \texttt{Evaluation} \\
&= @12@ & \\
\end{align*}
$\therefore$ we have shown something!
\end{proof}
\section{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!
\subsection{Weak vs Strong?}
With \textbf{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 \textit{inductive hypothesis}).
With \textbf{strong induction}, we assume the statement holds for all cases before the “(n+1)-th” hold and prove it using the previous ones (our \textit{inductive hypothesis}).
\section{Proofs}
\begin{code}
doubleAll :: [Int] -> Int
doubleAll [] = 0 — doubleAll.1
doubleAll (x:xs) = 2 * x + doubleAll xs — doubleAll.2
\end{code}
\begin{code}
sum’ :: [Int] -> Int
sum’ [] = 0 –sum’.1
sum’ (x:xs) = x + sum’ xs –sum’.2
\end{code}
\subsection{Doubling all!}
Let’s prove that @doubleAll x = 2 * sum’ x@
\begin{proof} @doubleAll x = 2 * sum’ x@\\
We will use induction!
\textbf{Base Case}: @[]@
\begin{align*}&
@doubleAll [] = 2 * sum’ []@
\step{@sum.1@}
@doubleAll [] = 2 * 0@
\step{@doubleAll.1@}
@0 = 2 * 0@
\step{Evaluation}
@0 = 0@
\step{Evaluation}
@true@
\end{align*}
$\therefore$ our base case holds!!!!\\
\textbf{Induction Case}: We want to prove: @(x:xs)@
We assume $\forall $ @xs . doubleAll xs = 2 * sum’ xs@
We want to prove is: $\forall x . \forall xs . $ @doubleAll (x:xs) = 2 * sum’ (x:xs)@
\begin{align*}&
@doubleAll (x:xs) = 2 * sum’ (x:xs)@
\step{@sum’.2@}
@doubleAll (x:xs) = 2 * (x + sum’ xs)@
\step{@doubleAll.2@}
@2 * x + doubleAll xs = 2 * (x + sum’ xs)@
\step{Evaluate}
@2 * x + doubleAll xs = 2 * x + 2 * sum’ xs@
\step{Ind. Hyp.}
@2 * x + doubleAll xs = 2 * x + doubleAll xs@
\step{Reflexivity of =}
@true@
\end{align*}
$\therefore$ we have shown through induction that this statement holds!
\end{proof}
\newpage
\subsection{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@
\begin{proof}
Let’s use induction!
\textbf{Base Case}: @[]@
Our Goal: @reverse ([] ++ ys) == reverse ys ++ reverse []@
LHS:
\begin{align*}
&@reverse ([] ++ ys)@ & \texttt{by identity of @++@} \\
&= @reverse ys@ &
\end{align*}
RHS:
\begin{align*}
&@reverse ys ++ reverse []@ & \texttt{by @reverse.1@} \\
&= @reverse ys ++ []@ & \texttt{by identity of @++@} \\
&= @reverse ys@ &
\end{align*}
$\therefore$ our base case holds as the $LHS = RHS$.\\
\textbf{Induction Step}: @(x:xs)@\\
Note our induction hypothesis: $\forall$ @xs@ $\forall$ @ys . reverse (xs ++ ys) == reverse ys ++ reverse xs@ \\
Our goal: @reverse ((x:xs) ++ ys) == reverse ys ++ reverse (x:xs)@
LHS:
\begin{align*}
&@reverse ((x:xs) ++ ys)@ & \texttt{by @++.2@}\\
&= @reverse (x:(xs ++ ys))@ & \texttt{by @reverse.2@}\\
&= @reverse (xs ++ ys) ++ [x]@ & \texttt{by ind. hyp}\\
&= @reverse ys ++ reverse xs ++ [x]@ & \\
\end{align*}
RHS:
\begin{align*}
&@reverse ys ++ reverse (x:xs)@ & \texttt{by @reverse.2@} \\
&= @reverse ys ++ reverse xs ++ [x]@&
\end{align*}
$\therefore$ we have shown through induction that this property holds!
\end{proof}
\newpage
\subsection{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: $\forall$ @xs, ys . length (xs ++ ys) == length xs + length ys@
\end{document}