macOS Formal proofs

[Cromulent]

Okay so I started reading The Art of Computer Programming and have started doing the exercises but am having a bit of difficulty with formal proofs. I'm not that great with maths but would like to get better so this is my attempt.

One of the (supposed) easy exercises states:

Prove that m is always greater than n at the beginning of step E1. except possibly the first time the step occurs.

The algorithm is as follows:

E1 [Find the remainder] Divide m by n and let r be the remainder. (We will have 0 <= r < n).
E2 [Is it 0?] If r = 0, the algorithm terminates; n is the answer.
E3 [Reduce] Set m <- n, n <- r, and go back to step E1.

Okay so we do:

E1 m = 3 and n = 5.
3 / 5 = 0 r = 3.
E2 r = 3, continue
E3 m = 5, n = 3
E1 5 / 3 = 1 r = 2
E2 r = 2, continue
E3 m = 3, n = 2
E1 3 / 2 = 1 r = 1
E2 r = 1, continue
E3 m = 2, n = 1
E1 2 / 1 = 2 r = 0
E2 r = 0, terminate

If n > m then at step E3 m => n meaning that after one iteration n is always <= m.

How would I write this as a formal proof? Am I doing anything wrong?

 

[gnasher729]

The remainder of 3/5 is not 5.

 

[Cromulent]

The remainder of 3/5 is not 5.

Bah sorry I'm an idiot. Previous post fixed.

Heh, stupid brain farts .

 

[robbieduncan]

I would suggest you use Proof By Induction.

Looking at this reminds me of studying Computer Science at Uni!

 

[lee1210]

I am not sure what notation is being used, but:
r must be strictly less than n, as there cannot be a remainder greater than the divisor. This should be some sort of lemma that is already available. Since m is set to n at the end of the algorithm, and n is set to r, based on the prior assertion, at E1 n must be strictly less than m.
Q.E.D.
=)
-Lee

 

[robbieduncan]

I think that there must be some more assumptions that are not stated. For example if you start with m=1 and n=1 then m will never be larger than n.

 

[gnasher729]

I think that there must be some more assumptions that are not stated. For example if you start with m=1 and n=1 then m will never be larger than n.

If m = n = 1, the algorithm will terminate immediately in Step 2 and never return to Step 1. It is correct to say "m > n whenever the algorithm returns to Step 1" if it never returns to that step.

 

[robbieduncan]

If m = n = 1, the algorithm will terminate immediately in Step 2 and never return to Step 1. It is correct to say "m > n whenever the algorithm returns to Step 1" if it never returns to that step.

Yes, you are right. This might well be a useful base case for one of 2 (or maybe 3) inductive proofs that would prove this for all cases...

 

[Berlepsch]

For problems like this, it is often easiest if you sort all possible start conditions into relevant categories and look at them one by one. For your problem, consider

1) m = n , which implies r = 0
2) m > n with r > 0
3) m > n with r = 0
4) m < n with r > 0
5) m < n with r = 0 (only possible if m = 0 is allowed).

Cases 1, 3 and 5 can be dismissed because the algorithm stops in the first iteration. For case 2, lee has already given the answer: r < n by definition, therefore m' > n' in the second and all following iterations.

That leaves only case 4 to look at. The result is obvious, so I don't have to spell it out.

 

[Cromulent]

Cheers guys .

Looks like this book will be well worth persevering with. Does anyone have any useful maths website links at all for this kind of stuff? I looked at the wiki link provided earlier but was wondering if there was a slightly more general resource?