How is it obvious that that (foldr Cons Nil) just copies a list?

Question

I am currently reading Why Functional Programming Matters by John Hughes.

In the "Gluing Functions Together" section, after having explained that (foldr f a) is a function that replaces all occurrences of Cons in a list by f, and all occurrences of Nil by a (which I understand), the author writes: "Now it’s obvious that (foldr Cons Nil) just copies a list" and gives this example to illustrate the point:

append [1, 2] [3, 4] = foldr Cons [3, 4] [1, 2]
                     = foldr Cons [3, 4] (Cons 1 (Cons 2 Nil))
                     = Cons 1 (Cons 2 [3, 4]))
                     = [1, 2, 3, 4]

I do not understand why on the third line of the given example, (Cons 1 (Cons 2 Nil)) is suddenly at the front and consequently why the list does not end up being [3, 4, 1, 2]. Is the Nil in (Cons 1 (Cons 2 Nil)) a and is Cons [3, 4] f if foldr's definition is foldr f a?

In which way is it obvious that foldr Cons Nil just copies a list?

Answer 1

We've got to substitute 3 times to get from line 2 to line 3. Using the definition of foldr given on page 5:

(foldr f x) Nil = x
(foldr f x) (Cons a l) = f a ((foldr f x) l)

taking the second line of the given example, and substituting using the 2nd line of the foldr defn, I'll write the variable matching under each argument:

                 = foldr Cons [3, 4] (Cons 1 (Cons 2 Nil))
defn:             (foldr  f     x)   (Cons a      l   )     = f a ((foldr f x) l)

gives:             Cons 1 ((foldr Cons [3,4]) (Cons 2 Nil) )

substituting again for this ..........^ occurrence of foldr gives:

                   Cons 1 (Cons 2 ((foldr Cons [3,4] Nil)

and again, but this time taking the 1st line of the foldr defn:

                   Cons 1 (Cons 2 (Cons [3,4])

Answer 2

Replacing Cons by Cons and Nil by Nil keeps things the same!

In the given append example, [3, 4] is what replaces Nil.