[Haskell-beginners] structural induction, two lists, simultaneous

[Rustom Mody]

On Mon, Dec 15, 2014 at 7:12 AM, Pascal Knodel <pascal.knodel at mail.com>
wrote:
>
> Hi list,
>
>
> Proposition:
>
> map f (ys ++ zs)  =  map f ys ++ map f zs
>
> (Haskell, the craft of functional programming, exercise 11.31)
>
>
> Almost every time I'm asked to do (structural) induction over multiple
> 'things', in this example lists, I don't know how to do it.
> (I encountered similar difficulties when I worked through chapter 9, see
> https://github.com/pascal-knodel/haskell-craft/tree/master/Chapter%209 ,
> ex. 9.5 , https://github.com/pascal-knodel/haskell-craft/blob/
> master/Chapter%209/E%279%27%275.hs).
> I think my proof in this case isn't formally correct. It feels like it
> isn't.
>
> I would like to do the example with your help, so that I feel a
> little bit safer.
>
> Let's start with the base case. If I have two lists, do I select
> one, say  ys := [] . Only one or one after another? Or both 'parallel'?
> I could state  ys ++ zs := []  too, does it help?
>
> I could imagine that the proposition could be expanded to something like
>
>     map f (l1 ++ l2 ++ ... ++ lN) = map f ys ++ map f zs
>  =  map f l1 ++ map f l2 ++ ... ++ map f lN
>
> And I could imagine that it is possible to do induction over more than two
> lists too.
>
> What is the reason why we can do it over two 'objects' at the same time?
> How do I start? Can you explain this to me?
>
>

This is a right question

It is somewhat a proof-version of currying

What you want to prove is

(∀ f,ys,zs • map f (ys ++ zs)  =  map f ys ++ map f zs)

= "reorder the variables"

(∀ ys,f,zs • map f (ys ++ zs)  =  map f ys ++ map f zs)

= "(∀ x,y • ...) = (∀x • (∀ y • ...))"

(∀ ys • (∀ f,zs • map f (ys ++ zs)  =  map f ys ++ map f zs))

And now you can see that you want a proof of a one-variable theorem

Of course at this stage you might ask "Why did you choose to pull ys out
and not zs (or f for that matter)?"

One possible answer: Experience!

Another: Recursion in definitions and induction in proofs go hand in hand.
Clearly the recursion is happening on the first list. So we may expect the
induction to focus there



>
> Attempt:
>
> -- ---------------
> -- 1. Proposition:
> -- ---------------
> --
> --   map f (ys ++ zs)  =  map f ys ++ map f zs
> --
> --
> -- Proof By Structural Induction:
> -- ------------------------------
> --
> --
> --   1. Induction Beginning (1. I.B.):
> --   ---------------------------------
> --
> --
> --     (Base case 1.)  :<=>  ys := []
> --
> --       =>  (left)  :=  map f (ys ++ zs)
> --                                          | (Base case 1.)
> --                    =  map f ([] ++ zs)
> --                                          | ++
> --                    =  map f zs
> --
> --
> --          (right)  :=  map f ys ++ map f zs
> --                                               | (Base case 1.)
> --                    =  map f [] ++ map f zs
> --                                               | map
> --                    =  map f zs
> --
> --
> --       => (left)  =  (right)
> --
> --       ✔
> --
> --
> --  1. Induction Hypothesis (1. I.H.):
> --  ----------------------------------
> --
> --    For an arbitrary, but fixed list "ys", the statement ...
> --
> --      map f (ys ++ zs)  =  map f ys ++ map f zs
> --
> --    ... holds.
> --
> --
> --  1. Induction Step (1. I.S.):
> --  ----------------------------
> --
> --
> --     (left)  :=  map f ( (y : ys) ++ zs )
> --                                                      | ++
> --              =  map f (  y : ( ys ++ zs )  )
> --                                                      | map
> --              =  f y : map f ( ys ++ zs )
> --                                                      | (1. I.H.)
> --              =  f y : map f ys ++ map f zs
> --                                                      | map
> --              =  map f (y : ys) ++ map f zs
> --
> --
> --    (right)  :=  map f (y : ys) ++ map f zs
> --
> --
> --    =>  (left)  =  (right)
> --
> --
> --    ?■?  (1. Proof)
>
>
> But in this 'proof attempt' only "ys" was considered (1. I.H.).
> What do I miss?
>
> Pascal
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://www.haskell.org/mailman/listinfo/beginners
>


-- 
http://www.the-magus.in
http://blog.languager.org
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20141215/298e9ee6/attachment.html>