- #1

- 297

- 0

## 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.