Consider adding proof requirement to some currently easy exercises

[keiravillekode]

Would it reasonable to ask students to prove one or two properties of their solutions, for some of the simplest exercises? We would increase their difficulty rating at the same time.

Possible examples:

reverse-string
length A <= 1 implies reverse A = A
reverse (A ++ B) = (reverse B) ++ (reverse A)

difference-of-squares
difference 0 = 0
difference (n+1) = difference n + n (n+1)^2

hamming
(length A = length C and length B = length D) implies hamming (A ++ B) (C ++ D) = (hamming A C) + (hamming B D)

matching-brackets
matching-brackets A implies matching-brackets '(' A ')'
(matching-brackets A and matching-brackets B) implies matching-brackets (A ++ B)

[oxe-i]

I spent some time today thinking about this. I believe that we should have some exercises with both computations and proofs, some with only computations (which is the current default) and some with only proofs.

We might perhaps create a "clone" of a few exercises so that we have a full-computational version and an equivalent (generally harder) proof-only version. I think that zebra-puzzle is particularly well-suited to this, considering it is a logic puzzle. We might encode the rules as axioms and require a proof of the result. But creating this exercise is currently above my skill level, I'd have to do some research on the topic.