Solution: proofs about adding even and odd numbers

This page is part of the introduction to proving metatheorems with STELF.

Exercise 4 from the part 1 exercises: Prove remaining properties of how evenness and oddness interacts with addition:

• State and prove the theorem sum-even-odd that shows that the sum of an even and an odd number results in an odd number
• State and prove a theorem sum-odd-even that shows that the sum of an odd plus an even number produces an odd number
• Finally, state and prove a theorem sum-odds that shows that the sum of two odd numbers produces an even number

Starting with the preliminaries, including the definition of odd from exercise 2:

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort plus {_ nat} {_ nat} {_ nat} %.
%term plus-z plus z N2 N2 %.
%term plus-s %pi (plus (s N1) N2 (s N3)) %<- (plus N1 N2 N3) %.
%sort even {_ nat} %.
%term even-z even z %.
%term even-s %pi (even (s (s N))) %<- (even N) %.
%sort odd {_ nat} %.
%term odd-1 odd (s z) %.
%term odd-s %pi (odd N) %-> (odd (s (s N))) %.

The sum of an even and odd number is odd

%sort sum-even-odd {_ even N1} {_ odd N2} {_ plus N1 N2 N3} {_ odd N3} %.
%mode sum-even-odd %in %in %in %out %.
%term seoz sum-even-odd even-z OddN2 plus-z OddN2 %.
%term seos
  %pi (sum-even-odd (even-s EvenN1) OddN2 (plus-s (plus-s PlusN1N2N3)) (odd-s OddN3))
  %<- (sum-even-odd EvenN1 OddN2 PlusN1N2N3 OddN3) %.
%worlds () (sum-even-odd _ _ _ _) %.
%total D (sum-even-odd D _ _ _) %.

The sum of an odd and an even number is odd

Unlike the previous proof that the sum of an even number and on odd, the base case of this proof is easiest to prove by reusing one of the lemmas a previous exercise.

Neither answer is better than the other! It’s valuable to think through the answer that you didn’t select, as it’s important to be able to think through multiple ways of proving the same theorem.

Likely proof, reusing succ-even

If you’ve just written sum-even-odd, and try to adapt the structure of that proof, the easiest approach is to reuse succ-even from Exercise 3, the proof that the successor of an even number is odd.

We’ll first repeat that proof:

%sort succ-even {_ even N} {_ odd (s N)} %.
%mode succ-even %in %out %.
%term sez succ-even even-z odd-1 %.
%term ses %pi (succ-even (even-s EvenA) (odd-s OddA)) %<- (succ-even EvenA OddA) %.
%worlds () (succ-even _ _) %.
%total D (succ-even D _) %.

With succ-even in hand, the proof of sum-odd-even has the same structure as the proof of sum-even-odd:

%sort sum-odd-even {_ odd N1} {_ even N2} {_ plus N1 N2 N3} {_ odd N3} %.
%mode sum-odd-even %in %in %in %out %.
%term soe1 %pi (sum-odd-even odd-1 EvenN2 _ OddN3) %<- (succ-even EvenN2 OddN3) %.
%term soes
  %pi (sum-odd-even (odd-s OddN1) EvenN2 (plus-s (plus-s PlusN1N2N3)) (odd-s OddN3))
  %<- (sum-odd-even OddN1 EvenN2 PlusN1N2N3 OddN3) %.
%worlds () (sum-odd-even _ _ _ _) %.
%total D (sum-odd-even D _ _ _) %.

Alternative solution, reusing succ-even-odd and plus-commutes

Another proof of sum-odd-even uses the previously proved sum-even-odd along with the proof of the proof of the commutativity of plus from Exercise 1. The sum-even-odd proof is a bit involved:

%sort plus-zero-id {N1 nat} {_ plus N1 z N1} %.
%mode plus-zero-id %in %out %.
%term pzidz plus-zero-id z plus-z %.
%term pzids
  %pi (plus-zero-id (s N) (%the (plus (s N) z (s N)) (plus-s D)))
  %<- (plus-zero-id N D) %.
%worlds () (plus-zero-id _ _) %.
%total N (plus-zero-id N _) %.
%sort plus-flip {_ plus N1 N2 N3} {_ plus N1 (s N2) (s N3)} %.
%mode plus-flip %in %out %.
%term pfz plus-flip _ plus-z %.
%term pfs
  %pi (plus-flip (%the (plus (s N1) N2 (s N3)) (plus-s Dplus)) (%the (plus (s N1) (s N2) (s (s N3))) (plus-s DIH)))
  %<- (plus-flip Dplus DIH) %.
%worlds () (plus-flip _ _) %.
%total D (plus-flip D _) %.
%sort plus-commutes {_ plus N1 N2 N3} {_ plus N2 N1 N3} %.
%mode plus-commutes %in %out %.
%term pcz %pi (plus-commutes _ D) %<- (plus-zero-id N1 D) %.
%term pcs
  %pi (plus-commutes (%the (plus (s N1') N2 (s N3')) (plus-s Dplus)) D)
  %<- (plus-commutes Dplus DIH)
  %<- (plus-flip DIH D) %.
%worlds () (plus-commutes _ _) %.
%total D (plus-commutes D _) %.

Once that proof is available, the proof of sum-odd-even requires no additional induction:

%sort sum-odd-even {_ odd M} {_ even N} {_ plus M N P} {_ odd P} %.
%mode sum-odd-even %in %in %in %out %.
%term soe
  %pi (sum-odd-even (%the (odd M) O) (%the (even N) E) (%the (plus M N P) A) (%the (odd P) O0))
  %<- (plus-commutes A A0)
  %<- (sum-even-odd E O A0 O0) %.
%worlds () (sum-odd-even _ _ _ _) %.
%total [] (sum-odd-even D _ _ _) %.

The sum of two odd numbers is even

The most straightforward approach here reuses succ-odd from Exercise 3 in exactly the same way as the “expected” solution to the previous theorem reused succ-even.

First, we’ll repeat the proof of succ-odd from Exercise 3:

%sort succ-odd {_ odd N} {_ even (s N)} %.
%mode succ-odd %in %out %.
%term so1 succ-odd odd-1 (even-s even-z) %.
%term sos %pi (succ-odd (odd-s OddA) (even-s EvenA)) %<- (succ-odd OddA EvenA) %.
%worlds () (succ-odd _ _) %.
%total D (succ-odd D _) %.

With that out of the way, the proof of sum-odds has the same structure as the previous solutions:

%sort sum-odds {_ odd N1} {_ odd N2} {_ plus N1 N2 N3} {_ even N3} %.
%mode sum-odds %in %in %in %out %.
%term soz %pi (sum-odds odd-1 OddN2 _ EvenN3) %<- (succ-odd OddN2 EvenN3) %.
%term sos
  %pi (sum-odds (odd-s OddN1) OddN2 (plus-s (plus-s PlusN1N2N3)) (even-s EvenN3))
  %<- (sum-odds OddN1 OddN2 PlusN1N2N3 EvenN3) %.
%worlds () (sum-odds _ _ _ _) %.
%total D (sum-odds D _ _ _) %.