Please check my work: Structural Induction

Just want to confirm whether I've got this right or not.. (should be right tho)

(tip: ++ is concatenation therefore joining two lists [ ] [ ] or (x:xs))

1. Prove xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

Base case P( [ ] )

[ ] ++ (ys ++ zs) = ( [ ] ++ ys ) ++ zs

= ys ++ zs (RH)

= [ ] ++ (ys ++ zs)

= ys ++ zs (LH)

Step Case P (as)

Assume

as ++ (ys ++ zs) = (as ++ ys) ++ zs -- (IH)

Prove P (a:as)

(a:as) ++ (ys ++ zs) = ( (a:as) ++ ys) ++ zs

= ( (a:as) ++ ys) ++ zs --- (IH) (LH)

Theorem Proved. (I'm not too sure because it seems so simple though...something may be missing)

--------------------------------------------------------------------------------------------------------

revT :: Tree a -> Tree a

revT Nil = Nil -- (T1)

revT (Node x t1 t2) = Node x (revT t2) (revT t1) -- (T2)

2. Prove revT (revT t) = t

Base Case P(Nil)

revT (revT Nil) = Nil

= revT (Nil) - T1

= Nil -- T1 (LH)

Step Case ∀t1, ∀t2, P(t1) ^ P (t2) => (P (Node x t1 t2)

Assume P (u1) ^ P (u2)

revT (rev T u1) = u1 ---- IH1

revT (rev T u2) = u2 ---- IH2

Prove P(Node a u1 u2)

revT (revT (Node a u1 u2)) = Node a u1 u2

= revT ( Node a (revT u2) (revT u1) ) -- T2

= Node a (revT(revT u1)) (revT(revT u2)) -- T2

= Node a u1 u2 -- IH1, IH2 (LH)

Theorem Proved

3. (Extension work) Prove count(revT t) = count (t)

Base Case P (Nil)

count (rev T Nil) = count (Nil)

= count (rev T Nil) (LH)

= count (Nil) -- T1

Step Case Step Case ∀t1, ∀t2, P(t1) ^ P (t2) => (P (Node x t1 t2))

Assume P (u1) ^ P (u2)

count (rev T u1) = count (u1) -- IH1

count (rev T u2) = count (u2) -- IH2

Prove P (Node a u1 u2), that is

count (revT (Node a u1 u2)) = count (Node a u1 u2)

= count (Node a (revT u2) (revT u1)) -- T2

= Node (count a) (count(revT u2) (count (rev u1)) -

= Node (count a) (count u2) (count u1) -- IH1, IH2

= count (Node a u2 u1) (LH)

Well, looking at it, they are two different thing but if count function is merely counting number of nodes it should be the same.

4. Final question: natural deduction..

I thought I was able to solve all natural deduction questions but failed one.. which is:

(c V d) /\ ㄱc

----------------

d

(contradiction elimination rule can be used for this one)

Thank you (Fitch style please thank you)

It is a bit long but thank you very much!

Re: Please check my work: Structural Induction

It is not recommended to post more than two questions in one thread.

Quote:

Originally Posted by

**gomdohri** 1. Prove xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

Base case P( [ ] )

[ ] ++ (ys ++ zs) = ( [ ] ++ ys ) ++ zs

= ys ++ zs (RH)

= [ ] ++ (ys ++ zs)

= ys ++ zs (LH)

You did not define ++, LH, RH and P. You did not say on which of the three variables you do induction. I also don't understand the chain of equalities. Which side of the first equality do you rewrite on each line? In a mathematical proof, one does not write the target equality first. Rather, one writes the left-hand side of the target equality and then on each line one rewrites it according to some laws, writing comments on the right, until one comes to the right-hand side of the target equality. Of course, it's OK to prove an equality right-to-left.

Quote:

Originally Posted by

**gomdohri** Step Case P (as)

Assume

as ++ (ys ++ zs) = (as ++ ys) ++ zs -- (IH)

Prove P (a:as)

(a:as) ++ (ys ++ zs) = ( (a:as) ++ ys) ++ zs

= ( (a:as) ++ ys) ++ zs --- (IH) (LH)

I don't understand this. It needs to be written in more details with clear comments.

Re: Please check my work: Structural Induction

If you just say that ++ is concatenation, then the only thing that can be said about xs ++ (ys ++ zs) = (xs ++ ys) ++ zs is that it is obvious. To write a more precise proof you need a more precise definition. Here is how I would write the proof.

Let's assume that : binds stronger than ++, i.e., x : xs ++ ys means (x : xs) ++ ys and not x : (xs ++ ys).

Definition,

[] ++ ys = ys (D1)

x : xs ++ ys = x : (ys ++ zs) (D2)

Proving xs ++ (ys ++ zs) = (xs ++ ys) ++ zs by induction on xs.

Base case.

[] ++ (ys ++ zs) = ys ++ zs (D1)

= ([] ++ ys) ++ zs (D1)

Induction step.

Suppose xs ++ (ys ++ zs) = (xs ++ ys) ++ zs (IH).

Need to prove: x : xs ++ (ys ++ zs) = (x : xs ++ ys) ++ zs.

x : xs ++ (ys ++ zs) = x : (xs ++ (ys ++ zs)) (D2)

= x : ((xs ++ ys) ++ zs) (IH)

= x : (xs ++ ys) ++ zs (D2)

= (x : xs ++ ys) ++ zs (D2)

Re: Please check my work: Structural Induction

The proof of revT (revT t) = t make sense.

Quote:

Originally Posted by

**gomdohri** 3. (Extension work) Prove count(revT t) = count (t)

Base Case P (Nil)

count (rev T Nil) = count (Nil)

= count (rev T Nil) (LH)

= count (Nil) -- T1

Step Case Step Case ∀t1, ∀t2, P(t1) ^ P (t2) => (P (Node x t1 t2))

Assume P (u1) ^ P (u2)

count (rev T u1) = count (u1) -- IH1

count (rev T u2) = count (u2) -- IH2

Prove P (Node a u1 u2), that is

count (revT (Node a u1 u2)) = count (Node a u1 u2)

= count (Node a (revT u2) (revT u1)) -- T2

= Node (count a) (count(revT u2) (count (rev u1)) -

= Node (count a) (count u2) (count u1) -- IH1, IH2

= count (Node a u2 u1) (LH)

If count returns numbers, then the left- and right-hand sides are both numbers. However, your second and third line from the end start with Node, which returns a tree. The second last line should say 1 + (count u2) + (count u1).

Quote:

4. Final question: natural deduction..

I thought I was able to solve all natural deduction questions but failed one.. which is:

(c V d) /\ ㄱc

----------------

d

(contradiction elimination rule can be used for this one)

Break the assumption into c \/ d and ~c using conjunction elimination. Apply disjunction elimination to c \/ d. If c, then together with ~c you get a contradiction, from which d follows. If d, then you get d immediately. Thus, in both cases you get d.Look at examples of disjuntion elimination and try the outline above. If you need more help, let me know.

Re: Please check my work: Structural Induction

so for (c v d) /\ ㄱc

----------------

d

1 (c v d) /\ c

2 c v d ............ VI 1

3 ㄱc ........... VI 1

4 c Ass

5 d ㄱE 3-4

6 d Ass

7 d R6

8 d ... VE 2, 4-5, 6-7

(excuse my indentation)

Re: Please check my work: Structural Induction

Line 1 should say (c \/ d) /\ ~c. The rule in lines 2 and 3 is conjunction elimination /\E. It may not be necessary to repeat d in step 7. A single assumption is still a subderivation. Otherwise it seems OK.

Edit: You can use the [code] tag to preserve indentation.

Re: Please check my work: Structural Induction

Oh my mistake! Thank for the help!