# Check the work please (Structural Induction)

• Aug 24th 2012, 09:48 PM
gomdohri
Check the work please (Structural Induction)
I have completed the problem but I would like to know whether I did it correctly so please check my work to see whether everything went ok.

mult Nul = 1 ------ (M1)
mult (Node a t1 t2) = a * mult t1 * mult t2 ------ (M2)

multa t = multb t 1 ------ (MA)

multb Nul acc = acc --------- (MB1)
multb (Node a t1 t2) acc = multb t1 (a * (multb t2 acc)) ---- (MB2)

Prove mult t = multa t

By induction on t,

Base Case P(Nul)

mult Nul = multa Nul
RHS = multb Nul 1 ---by (MA)
= 1 --- by (MB1)
LHS = 1 --- by (M1)
= RHS

Step Case a. t1. t2. P(t1) ^ P(t2) P(Node a t1 t2)

Assume, P(u1) ^ P(u2)

mult u1 = multa u1 --- (IH1)
mult u2 = multa u2 --- (IH2)

Prove P(Node x u1 u2), that is,

mult (Node x u1 u2) = multa (Node x u1 u2)
LHS = x * mult u1 * mult u2 ---by (M2)
= x * multa u1 * multa u2 ---by(IH1,IH2)
RHS = multb (Node x u1 u2) 1 ---by (MA)
= multb u1 (x * (multb u2 acc)) ---by(MB2)
LHS

-- note: I have changed a to x to show specific instance.. right?

Although I have used the IH1 & IH2, both sides are not the same. Therefore, we need to prove a stronger property than the one we is given.

∀ acc. acc * mult t = multb t acc

By induction on t,

Base Case P(Nul)

∀ acc. acc * mult Nul = multb Nul acc
RHS = acc ---by (MB1)
LHS = acc * 1 ---by (M1)
= acc
= RHS

Step Case a. t1. t2. P(t1) ^ P(t2) P(Node a t1 t2)

Assume, P(u1) ^ P(u2)

∀ acc. acc * mult u1 = multb u1 acc --- (IH3)
∀ acc. acc * mult u2 = multb u2 acc --- (IH4)

Prove,
∀ acc. acc * mult (Node x u1 u2) = multb (Node x u1 u2) acc
RHS = multb u1 (x*(multb u2 acc)) -- by(MB2)
= multb u1 (x * acc * mult u2)-- by(IH4)
= (x * acc * mult u2)*mult u1 -- by(IH3)
LHS = acc * x * mult u1 * mult u2 -- by(M2)
= RHS
Then we need to generalise over acc by using →I.

We have now proved ∀ t. P(t), that is: [is this right? proved that for all t, P(t)? not too sure]

∀ t. ∀ acc. acc * mult t = multb t acc [is it okay to change Node a t1 t2 to t?]

Change the order of the quantifiers :

∀ acc. ∀ t. acc * mult t = multb t acc

Instantiate at (acc = 1),

∀ t. 1 * mult t = multb 1 acc by →E
∀ t. mult t = multb 1 acc by arithmetic
∀ t. mult t = multa t by MA

Which was the original property required. after instantiating the proof finishes right? not too sure about it.

Red texts are my questions... thank you
• Aug 25th 2012, 06:54 PM
gomdohri
Re: Check the work please (Structural Induction)
It seems that whole proving stuff is a bit wrong I will have to re-do it...
• Aug 27th 2012, 07:31 AM
emakarov
Re: Check the work please (Structural Induction)
Your proof is basically correct after you consider the more general induction hypothesis.

Quote:

Originally Posted by gomdohri
Therefore, we need to prove a stronger property than the one we is given.

∀ acc. acc * mult t = multb t acc

By induction on t,

Base Case P(Nul)

One flaw is that you don't define P. Often it is not defined explicitly (but then one is not supposed to use the letter P). However, your proof is very detailed (since you even mention the rules of universal introduction and elimination), so it's a good idea to define P explicitly. Moreover, this problem has an issue that often occurs in inductive proofs. The fact that we need to prove is ∀ t. ∀ acc. acc * mult t = multb t acc. There are two options. We can define P(t) as ∀ acc. acc * mult t = multb t acc. Alternatively, we can swap the quantifiers, fix some acc and define P(t) as acc * mult t = multb t acc for that particular acc. In other words, in the second option, acc would be the same throughout the proof. It turns out that the second option does not work.

Quote:

Originally Posted by gomdohri
∀ acc. acc * mult (Node x u1 u2) = multb (Node x u1 u2) acc
RHS = multb u1 (x*(multb u2 acc)) -- by(MB2)
= multb u1 (x * acc * mult u2)-- by(IH4)
= (x * acc * mult u2)*mult u1 -- by(IH3)
LHS = acc * x * mult u1 * mult u2 -- by(M2)
= RHS

The reason the second option does not work is that we apply IH4 for acc, but IH3 for x * acc * mult u2. Thus, we need P to be universally quantified over acc. This is an important distinction, which occurs when induction is studied seriously, e.g., in computational complexity and inductive types.

Quote:

Originally Posted by gomdohri
We have now proved ∀ t. P(t), that is: [is this right? proved that for all t, P(t)? not too sure]

Yes, you proved P(Nul) and ∀a. ∀t1. ∀t2. P(t1) ^ P(t2) → P(Node a t1 t2), so the induction principle gives you ∀ t. P(t).

Quote:

Originally Posted by gomdohri
∀ t. ∀ acc. acc * mult t = multb t acc [is it okay to change Node a t1 t2 to t?]

The definition of P does not use Node, so there is nothing to change.

Quote:

Originally Posted by gomdohri
Change the order of the quantifiers :

∀ acc. ∀ t. acc * mult t = multb t acc

Instantiate at (acc = 1),

∀ t. 1 * mult t = multb 1 acc by →E
∀ t. mult t = multb 1 acc by arithmetic
∀ t. mult t = multa t by MA

Which was the original property required. [COLOR=#ff0000]after instantiating the proof finishes right? not too sure about it.

Deducing ∀ t. mult t = multa t from ∀ t. ∀ acc. acc * mult t = multb t acc is trivial and does not really deserve a detailed explanation.