> (∀ 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

Thank you, Rustom Mody, that's it, reordering of universal quantifiers.
By the way, I'm searching for a 'good' book about predicate logic for quite some time now.
One with a strong link to mathematics and the quantification style
that is used there would be nice. By chance, is there a reference (script/paper/book )
you would recommend?

I have rewritten my first proof a little. It mentions the other variables now explicitly.
This way it should be cleaner:

--  1. Induction Hypothesis (1. I.H.):
--  ----------------------------------
--
--    For an arbitrary but fixed list "ys", for all lists "zs" and for all functions f the statement ...
--
--      map f (ys ++ zs)  =  map f ys ++ map f zs
--
--    ... holds.



When proving the proposition the first time I've used a different approach
(the chapter heavily promoted generalization and because I tried to get around
the dilemma that I wasn't sure if I understood 'simultaneous induction' correctly):


-- ---------------
-- 1. Proposition:
-- ---------------
--
--   map f (ys ++ zs)  =  map f ys ++ map f zs
--
--
--
-- Proof By Generalization:
-- ------------------------
--
--
-- ------------------------------
-- 1. Specialization Proposition:
-- ------------------------------
--
--   map f (ys ++ zs)  =  map f ys ++ map f zs
--
--
-- ------------------------------
-- 1. Generalization Proposition:
-- ------------------------------
--
--    map f (foldr (++) [] ls)  =  foldr ( (++) . (f `map`) ) [] ls
--
--
-- Proof By Structural Induction:
-- ------------------------------
--
--
--   1. Induction Beginning (1. I.B.):
--   ---------------------------------
--
--
--     (Base case 1.)  :<=>  ls := []
--    
--       =>  (left)  :=  map f (foldr (++) [] ls)
--                                                  | (Base case 1.)
--                    =  map f (foldr (++) [] [])
--                                                  | foldr
--                    =  map f []
--                                                  | map
--                    =  []
--
--
--          (right)  :=  foldr ( (++) . (f `map`) ) [] ls
--                                                          | (Base case 1.)
--                    =  foldr ( (++) . (f `map`) ) [] []
--                                                          | foldr
--                    =  []
--
--
--       => (left)  =  (right)
--
--       ✔
--
--
--  1. Induction Hypothesis (1. I.H.):
--  ----------------------------------
--
--    For an arbitrary but fixed (list-of-)lists "ls" and ∀ functions f, the statement ...
--
--      map f ( foldr (++) [] ls )  =  foldr ( (++) . (f `map`) ) [] ls
--
--    ... holds.
--
--
--  1. Induction Step (1. I.S.):
--  ----------------------------
--
--
--     (left)  :=  map f ( foldr (++) [] (l : ls) )
--                                                                      | foldr
--              =  map f ( l ++ foldr (++) [] ls )
--                                                                      | (Specialized 1. I.H.)
--              =  map f l ++ map f ( foldr (++) [] ls )
--                                                                      | (1. I.H.)
--              =  map f l ++ (  foldr ( (++) . (f `map`) ) [] ls  )
--
--
--    (right)  :=  foldr ( (++) . (f `map`) ) [] (l : ls)
--                                                                                  | foldr
--              =  ( (++) . (f `map`) ) l foldr ( (++) . (f `map`) ) [] ls
--                                                                                  | General rule of function application (left associativity)
--              =  (  ( (++) . (f `map`) ) l  ) foldr ( (++) . (f `map`) ) [] ls
--                                                                                  | (.)
--              =  (  (++) ( (f `map`) l )  ) foldr ( (++) . (f `map`) ) [] ls
--                                                                                  | (f `map`)
--              =  (  (++) (map f l)  ) foldr ( (++) . (f `map`) ) [] ls
--                                                                                  | General rule of function application (left associativity)
--              =  (++) (map f l) ( foldr ( (++) . (f `map`) ) [] ls )
--                                                                                  | ++
--              =  map f l ++ (  foldr ( (++) . (f `map`) ) [] ls  )
--
--
--    =>  (left)  =  (right)
--
--
--    ?■?  (1. Generalization Proof)
--
--
--           (Generalization)
--
--    :<=>   map f ( foldr (++) [] ls )  =  foldr ( (++) . (f `map`) ) [] ls
--                                                                                            | ls := [ys , zs]
--     |=>   map f ( foldr (++) [] [ys , zs] )  =  foldr ( (++) . (f `map`) ) [] [ys , zs]
--
--     <=>   map f (ys ++ zs)  =  map f ys ++ map f zs
--
--     <=>:  (Specialization)
--
--
--    ■  (1. Specialization Proof)


Is this also possible? Is it allowed to use a specialized induction hypothesis like that ( see '| (Specialized 1. I.H.)' above )?

Pascal





On Mon, Dec 15, 2014 at 7:12 AM, Pascal Knodel <pascal.knodel@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@haskell.org
http://www.haskell.org/mailman/listinfo/beginners


--
http://www.the-magus.in
http://blog.languager.org



_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://www.haskell.org/mailman/listinfo/beginners