Induction on predicate with arity greater than 1

Stream: general

[rory]

This one is not really about math, but it's more about reasoning about program.

So, I am a tutor for computing students in my university. We were discussing about structual induction.

For simplicity, I will write the following content in terms of Haskell.

So say you have the following data type definition.

data A = Int | Some A

Suppose you have a statement P(a), where a :: A(i.e. a has type A). Then if you want to prove P(a) is true for all a, then you need to prove that P(a) is true when a = i, where i :: Int, and that P(a) is true implies that P(Some a) is true for all a::A.

Then my students ask:
"what if you have a statement like P(a, a)? So the predicate have arity 2.Is there a strategy for arbitrary arity? "

I wish to give them an answer in the next meeting.

Thanks.

[Mario Carneiro]

It depends on what the second a is.

• If it is literally P(a, a), then this is still a unary predicate, where the predicate is P'(a) := P(a, a), and you do induction on that.
• If it is some other type, like P(a, n), then you might want to hold it fixed by letting P'(a) := P(a, n), and then in the induction step you will have to prove P(a, n) implies P(Some a, n).
• Or maybe you want to generalize over values of n, in which case you let P'(a) := forall n, P(a, n) and then you have to prove forall n, P(a, n) implies P(Some a, n), which is to say, you can change the value of n when referencing the inductive hypothesis.
• In more complicated situations you may need to perform a nested induction, when you need to decrease either a or a' in P(a, a').

[Chris B]

I'm not sure whether this is a helpful supplement to Mario's answer; but the induction/recursion principles you get with the elements of A or data A don't change, but there's also no hard and fast rule for how best to use them to prove P. IE ∀ (a b : ℕ) : a + b = b + a only needs induction on one element. Sometimes you'll need to do induction on one and then cases on the other, etc.
To put it in prose like you did earlier, the proof obligations branch out with the constructors as you start destructuring :

To prove P a1 a2 is true for all (a1 a2 : Data A),
  branch 1 : show P (int) (a2)
     goal 1_1 : show P (int) (int)
     goal 1_2 : forall a_y, show P (int) (Some a_y)
  branch 2 : forall a_x, show P (Some a_x) (a2)
     goal 2_1 : show P (Some a_x) (int)
     goal 2_2 : forall a_y, show P (Some a_x) (Some a_y)

And you would have further branches for higher arities. If you had a recursive type you would get a nice induction hypothesis, but the one you gave isn't (unless I missed something).