Results 1 to 3 of 3

Math Help - Check the work please (Structural Induction)

  1. #1
    Newbie
    Joined
    Aug 2012
    From
    China
    Posts
    18

    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
    Follow Math Help Forum on Facebook and Google+

  2. #2
    Newbie
    Joined
    Aug 2012
    From
    China
    Posts
    18

    Re: Check the work please (Structural Induction)

    It seems that whole proving stuff is a bit wrong I will have to re-do it...
    Follow Math Help Forum on Facebook and Google+

  3. #3
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,535
    Thanks
    778

    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 View Post
    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 View Post
    ∀ 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 View Post
    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 View Post
    ∀ 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 View Post
    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.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Structural Induction problem
    Posted in the Discrete Math Forum
    Replies: 6
    Last Post: August 17th 2012, 09:47 PM
  2. Please check my work: Structural Induction
    Posted in the Discrete Math Forum
    Replies: 6
    Last Post: August 17th 2012, 11:16 AM
  3. help with structural induction
    Posted in the Discrete Math Forum
    Replies: 6
    Last Post: June 1st 2011, 04:09 PM
  4. Strong induction vs. structural induction?
    Posted in the Discrete Math Forum
    Replies: 13
    Last Post: April 21st 2011, 12:36 AM
  5. structural induction
    Posted in the Discrete Math Forum
    Replies: 0
    Last Post: October 19th 2009, 01:20 PM

Search Tags


/mathhelpforum @mathhelpforum