Induction proof on list

[l46kok]

Homework Statement

Prove by finite list induction

∀xs:: [a]. map (\x -> x) xs = xs

Homework Equations

map f [ ] = [ ]
map f (x : xs) = (f x) : map f xs

The Attempt at a Solution

The list induction principle to prove a finite lists of type a is

[P([ ])^
∀x :: a. ∀xs :: [a]. P(xs) => P(x : xs)
=> ∀ys :: [a].P(ys)

So, to show ∀ys :: [a]. P(ys) we need to show two things
i.) P([ ])
ii.) ∀x :: a. ∀xs :: [a]. P(xs) => P(x : xs)


the i) part is really easy, it's just a base case but I am totally stomped on how to even go about proving the ii) part. I would like a guidance on this. Do I assume an arbitrary k of a newly list (that is previously constructed) and try to do an inductive proof? I don't know, I'm really lost.

 

[l46kok]

Bump :(

 

[l46kok]

Did I finally break the experts here with an unsolvable question?

Bump

 

[Dick]

Did I finally break the experts here with an unsolvable question?

Bump

Probably not unsolvable, but I can't make heads or tails of your notation. I was hoping somebody would come along who could. So you probably have succeeded in writing something nobody understands. Is this some kind of formal logic course?? Or abstract computer science?

 

[l46kok]

The class is known as Advanced Discrete Structures, crosslisted with Mathematics and Computer Science. Apparently we cover topics of both formal logic and abstract computer science.

This is the notes we got from the professor. Maybe this would be of help?

http://www.mediafire.com/?jasbcwfxycy5hmk [Broken]

 

[lpjhjdh]

You might consider taking a look at the Haskell community or other language theoretic sites like lambda the ultimate as this is really more of a computer science/type theory question.

The following might help, you already have some of these steps but just to be explicit:
1) Write out exactly what your predicate is (P = ?).
2) Show "P []" holds.
3) Assume "$\forall$ xs . P xs" and show "$\forall$ x . P (x :: xs)".
Does this help at all?

@Dick:
My category theory is not great by any measure but List is an endofunctor over the category of sets. To my knowledge :: is a Haskellism for type-of (presumably because they used up : for the list construction function) but I imagine it could have roots that go further back.
Again I'm no expert but I think for notation "∀xs:: [a]" is universal quantification over the set produced from the functor List applied to the object "a" in the category of sets. The "map" is Haskell-lingo for a functor's action on arrows. The "(\x -> x)" is Haskell-lingo for a lambda term.

 

[Dick]

Y
@Dick:
My category theory is not great by any measure but List is an endofunctor over the category of sets. To my knowledge :: is a Haskellism for type-of (presumably because they used up : for the list construction function) but I imagine it could have roots that go further back.
Again I'm no expert but I think for notation "∀xs:: [a]" is universal quantification over the set produced from the functor List applied to the object "a" in the category of sets. The "map" is Haskell-lingo for a functor's action on arrows. The "(\x -> x)" is Haskell-lingo for a lambda term.

I am more than willing to take your word for it. This is definitely not my field.

 

[lpjhjdh]

Looking over what I've said I'm not sure I really addressed your question very well so I'll be a bit more specific.

All you know about the term "xs" is that it's a list of a's. We could perform case analysis and then have the two cases x:[] and x:x':xs', however we're stuck in the same situation with xs' as we were with xs. This is the intuition behind our use of induction to solve the problem. Our induction hypothesis tells us something about xs, can you state what that is?

It will also be helpful to write out what you're trying to prove in its full form. What is P (x:xs)?