Notes for Lecture 14 (Fall 2022 week 6, part 3):
Proofs about programs
Copyright By PowCoder代写 加微信 powcoder
October 20, 2022
Reporter: What kind of proof do you need?
́tien: I don’t know. A proof is a proof. What kind of a proof? It’s a proof. A
proof is a proof, and when you have a good proof, it’s because it’s proven.
Reporter: But what kind of proof do you want?
Chrétien: Thank you very much.
September 2002
https://www.cbc.ca/player/play/2647901981
(starts around 3:26)
1 Stepping proofs
A proof is evidence of something—but that definition is barely more useful than ́tien’s.
There are many kinds of evidence, and many kinds of things.
We will consider one kind of thing: the behaviour of Haskell expressions. Because we have
defined stepping, by “behaviour” we mean “stepping”, and by “evidence” we mean, primarily, a
sequence of steps.
To prove that the Haskell expression (\x -> (\y -> y – x)) 1 6 produces the result 5, we
use stepping rules and write out the steps:
(\x -> (\y -> y – x)) 1 6⇒ (\y -> y – 1) 6 by function application, with substitution 1 for x⇒ 6 – 1 by function application, with substitution 6 for y⇒ 5 by arithmetic
So we have been doing proofs in CISC 360 already. You might think these proofs are “not
interesting”:
(1) if we want to know the result—the value produced at the end of the sequence of steps—we
could enter the expression into GHCi, and see what it produces;
(2) we might not think the intermediate results, like (\y -> y – 1) 6 and 6 – 1, are interesting.
Regarding (1), this is a fair point for many programs (including the example above). But recall
that GHCi will not print functions, so if we have the program
(\x -> (\y -> y – x)) 1
it will step to (\y -> y – 1), which is a lambda, so GHCi will not print it.
Regarding (2), maybe we want to understand how the expression works, or how many steps it
lec14, , CISC 360, F. 2022 1 2022/10/20
https://www.cbc.ca/player/play/2647901981
But I think most mathematicians would consider the stepping proofs we have done to be “triv-
ial”. An interesting proof should make a general statement, like “any integer greater than 1 is equal
to the product of prime numbers” or “for all a and b, if a and b are the lengths of the sides of a
right triangle, the length of the diagonal is
a2 + b2”. Our stepping proofs are more like proofs of
“the integer 6 is equal to the product of 3 and 2” or “if 2 and 5 are the lengths of the sides of a right
triangle, then the length of the diagonal is
The purpose of this lecture is to make our stepping proofs “interesting”, or at least “nontrivial”,
by adding quantifiers.
lec14, , CISC 360, F. 2022 2 2022/10/20
2 Doing “for all” in stepping proofs
Recall our old friend (?) diag:
diag m = if m == 0 then 0 else m + diag (m – 1)
(I changed n to m for reasons that may become clear.) If we try calling diag with various natural
numbers, we can guess there is a relationship between the input and output:
diag 1 ⇒∗ 1
diag 2 ⇒∗ 3
diag 3 ⇒∗ 6
diag 4 ⇒∗ 10
diag 5 ⇒∗ 15
(The symbol ⇒∗ means takes zero or more steps. For example, (\x -> (\y -> y – x)) 1 ⇒∗ 5.)
There is a relationship between diag n and (approximately) n
. To be exact, the result of diag n
is n·(n+1)
. For example, diag 5 produces 15, and 5·(5+1)
With the stepping proofs we have used before, we are limited to verifying the relationship
diag n ⇒∗ n · (n+ 1)
only for specific n, such as 15.
Let’s prove a general statement:
For all n ≥ 0,
diag n ⇒∗ n·(n+1)
Some might regard this as sloppy, because my intent is that n is an integer. So it might be better to
write it as
For all natural numbers n,
diag n ⇒∗ n·(n+1)
or, with more symbols:
For all n ∈ N,
diag n ⇒∗ n·(n+1)
For those who like such things, we could also write “for all” using symbols:
∀(n | n ≥ 0)
diag n ⇒∗ n · (n+ 1)
∀(n ∈ Z | n ≥ 0)
diag n ⇒∗ n · (n+ 1)
diag n ⇒∗ n · (n+ 1)
lec14, , CISC 360, F. 2022 3 2022/10/20
(n ∈ N) → (diag n ⇒∗ n · (n+ 1)
(n ∈ Z)∧ (n ≥ 0)
) → (diag n ⇒∗ n · (n+ 1)
(The last two are fairly close to CISC 204’s notation.)
We’ll stick to the “less symbols” version:
For all natural numbers n,
diag n ⇒∗ n·(n+1)
2.1 A simpler proof
Doing this proof about diag will require using induction, so we’ll build up to that by first doing a
proof that doesn’t need induction:
For all natural numbers n,
(\y -> y – 0) n ⇒∗ n.
How do we prove this statement?
To prove a “for all”, we assume that we have some natural number n.
We’ll try to use our usual stepping rules.
First, write the expression that we want to step. We can use the usual stepping rule for function
application:
(\y -> y – 0) n⇒ n – 0 by function application, with substitution n for y
Applying the rule works the same way it always has, even though we are substituting n rather
than a single, known number like 6.
(\y -> y – 0) n⇒ n – 0 by function application, with substitution n for y⇒ n by arithmetic
We have shown that (\y -> y – 0) n takes two steps to n.
Therefore, it takes zero or more steps to n, which we can write as:
(\y -> y – 0) n ⇒∗ n
which was to be proved.
2.2 The proof about diag
Let’s return to the statement about diag.
For all natural numbers n,
diag n ⇒∗ n·(n+1)
We are proving a “for all” statement, so we first assume that we have some natural number n.
lec14, , CISC 360, F. 2022 4 2022/10/20
Now we will do a proof by induction. There are (perhaps unfortunately) many ways to “phrase”
inductive proofs, so the one I use probably doesn’t look exactly like what you’ve seen in other
courses. In particular, you may have been told that in a proof by induction on natural numbers,
you must have “a base case” and “an inductive case” (or “an inductive step”), perhaps something
To prove ‘For all natural numbers n, we have Prop(n)’ by induction, where Prop is some
proposition involving n, thou shalt write the following:
• Base case (n = 0):
[prove that Prop(0) holds]
• Inductive step:
Assume Prop(k) holds.
[prove that Prop(k+ 1) holds]
However, the above is just one way of structuring an inductive proof. It has one advantage that
I know of: it looks like an inductive definition of the natural numbers, which may make it easier to
accept that proof by induction makes sense.
(Aside: An inductive definition of the natural numbers looks like this:
1. 0 is a natural number.
2. If k is a natural number then k+ 1 is a natural number.
I have no problem with this kind of definition, but I don’t like insisting that an inductive proof
has to have the same structure as the definition.)
The above approach, with an explicit “base case” and an explicit “inductive step”, has several
disadvantages:
• It forces you to structure your proof by considering cases of n. This is not always necessary
or desirable. Sometimes the proof is easier if you structure it in some other way.
• It is not very general. We can do proofs by induction on things that aren’t natural numbers,
including:
– pairs of natural numbers
– other data structures
– measures of data structures
We can also do “complete induction” on natural numbers, which is more powerful than “sim-
ple induction” on natural numbers.
For this lecture, though, we’ll stick to simple induction—but presented differently from what
you’re (probably) used to.
In an inductive proof, we assume the inductive hypothesis (IH). The IH, in English, will say:
lec14, , CISC 360, F. 2022 5 2022/10/20
If I am proving Prop(n) for n > 0, I can assume Prop(n− 1).
For the result about diag, that means:
If n > 0 then
diag (n− 1) ⇒∗ (n − 1) ·( (n − 1)+1)
(If you’re interested, I got this by taking the statement we’re trying to prove, replacing n with n−1,
and adding the condition that n is strictly greater than zero: otherwise n−1 would not be a natural
Because we are assuming the IH, we can “use” it at any time.
What we have to prove will be different, depending on whether n is 0 or greater than 0. So I
will begin the proof by “case analysis”:
Either n = 0, or n > 0.
1. First case: n = 0.
(In this case, we are assuming n = 0, in addition to the IH.)
Our goal is to prove
diag n ⇒∗ n · (n+ 1)
(Do not confuse the goal with the IH. The IH cannot change what you are trying to prove: it
is an “extra” assumption that will be very handy later, but we need to prove the statement
about diag n, not the IH which is about diag (n− 1).)
Since we are assuming n = 0, we actually need to prove
diag 0 ⇒∗ 0 · (0 + 1)
This has eliminated the variable n, so we can further simplify our goal by observing that
diag 0 ⇒∗ 0
Proving this doesn’t require anything new! This is a stepping problem with no n, so we can
solve it using techniques from weeks ago:
diag 0⇒ if 0 == 0 then 0 else 0 + diag (0 – 1) by function application, with subst. 0 for m⇒ if True then 0 else 0 + diag (0 – 1) by equality rule⇒ 0 by if-then-else rule
Since diag 0 takes zero or more steps to 0, we have proved
diag 0 ⇒∗ 0
which is our goal.
(This is the end of the first case, for when n = 0.)
lec14, , CISC 360, F. 2022 6 2022/10/20
2. Second case: n > 0.
(In this case, we are assuming n > 0, in addition to the IH.)
(It’s very easy to get lost in the details. While doing a proof, keep asking yourself two ques-
• What do I know?
• What am I trying to prove?
Right now, we know that n is a natural number (assumption from “for all” introduction), the
IH, and that n > 0.
We are trying to prove diag n ⇒∗ n·(n+1)
diag n⇒ if n == 0 then 0 else n + diag (n – 1) by function application, with subst. n for m
At this point, we might have a problem: don’t the rules for stepping n == 0 need two actual
integers? Not really: there is one rule for when the two integers are equal, and one for when
they aren’t equal. We have the assumption n > 0. If n > 0, then n ̸= 0. Therefore, n == 0
must step to False. After we take that step, we can take another step, using the if-then-else
diag n⇒ if n == 0 then 0 else n + diag (n – 1) by function application, with subst. n for m⇒ if False then 0 else n + diag (n – 1) by equality rule⇒ n + diag (n – 1) by if-then-else rule
What do we do now?
We could use the rule for stepping function application. (Exercise: Try that.) However, we
would find ourselves in a situation where we would need to know whether n − 1 > 0. We
don’t know that—we know that n > 0, but that means n could be 1, and 1 − 1 ̸> 0. If we
split into two cases, one for n− 1 = 0 and one for n− 1 > 0, we would go through the same
process we went through to get here, and would then have to consider cases n − 2 = 0 and
n − 2 > 0. That process would never end! (It’s somewhat similar to what happens in Prolog
if it starts trying to prove a subgoal that is identical to the original goal.)
So, again: what do we know, and what are we trying to prove? We know that n is a natural
number, that n > 0, and that the IH is true. We haven’t used the IH yet. So let’s try to use the
IH and see where that goes.
The IH is:
diag (n− 1) ⇒∗ (n − 1) ·( (n − 1)+1)
This looks promising, because we also have the assumption n > 0. Therefore, we actually
know (by modus ponens, if you care about that sort of thing)
diag (n− 1) ⇒∗ (n− 1) · ((n− 1) + 1)
lec14, , CISC 360, F. 2022 7 2022/10/20
Now this looks very promising: we got stuck on the expression n + diag (n – 1), and the
IH is telling us what diag (n – 1) steps to! So we can make some progress.
…⇒ n + diag (n – 1) by not-equals rule
⇒∗ n + (n− 1) · ((n− 1) + 1)
What are we trying to prove? That diag n ⇒∗ n·(n+1)
. Time to do arithmetic. This will look
a little strange, because I will only replace a + with a +. These are in different fonts: the + is
the Haskell addition operator, and the + is the mathematical addition operator.
⇒∗ n + (n− 1) · ((n− 1) + 1)
⇒ n+ (n− 1) · ((n− 1) + 1)
by arithmetic
Now we have a plain algebraic expression, which we need to show is equal to n·(n+1)
(n− 1) · ((n− 1) + 1)
(n− 1) · n
(n− 1) · n
2 · n+ (n− 1) · n
2 · n+ n · n− 1 · n
2 · n+ n2 − n
n · (n+ 1)
⇒∗ n+ (n− 1) · ((n− 1) + 1)
n · (n+ 1)
by above equations
Therefore, diag n ⇒∗ n·(n+1)
, which is our goal.
(This is the end of the second case, for when n > 0.)
lec14, , CISC 360, F. 2022 8 2022/10/20
2.3 The proof about diag, without explanations
I’m including this to help you understand what I think counts as a complete and correct proof.
Theorem 1. For all natural numbers n, diag n ⇒∗ n·(n+1)
Proof. By induction on n.
Assume the IH: If n > 0 then diag (n− 1) ⇒∗ (n − 1) ·( (n − 1)+1)
Either n = 0, or n > 0.
• First case: n = 0
diag 0⇒ if 0 == 0 then 0 else 0 + diag (0 – 1) by function application, with subst. 0 for m⇒ if True then 0 else 0 + diag (0 – 1) by equality rule⇒ 0 by if-then-else rule
by algebra
by assumption n = 0
• Second case: n > 0
diag n⇒ if n == 0 then 0 else n + diag (n – 1) by function application, with subst. n for m⇒ if False then 0 else n + diag (n – 1) by equality rule, using assumption n > 0⇒ n + diag (n – 1) by if-then-else rule
s ⇒∗ n + (n− 1) · ((n− 1) + 1)
⇒∗ n + (n− 1) · ((n− 1) + 1)
⇒ n+ (n− 1) · ((n− 1) + 1)
by arithmetic
by algebra. . .
2·n+(n−1)·n
= 2·n+n·n−1·n
lec14, , CISC 360, F. 2022 9 2022/10/20
A simpler proof
The proof about diag
The proof about diag, without explanations
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com