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

Re: Check the work please (Structural Induction)

It seems that whole proving stuff is a bit wrong I will have to re-do it...

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.