It seems that whole proving stuff is a bit wrong I will have to re-do it...
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
Your proof is basically correct after you consider the more general induction hypothesis.
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.
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.
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).
The definition of P does not use Node, so there is nothing to change.
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.