haskellfoldproof# substitution in proofs with recursive formulas

The following problem and partial solution are from Richard Bird's *Thinking Functionally with Haskell* (pp 132-133, 139)

given

```
foldl f e (x:xs) = foldl f (f e x) xs
foldl f e [] = e
```

Prove `foldl (@) e xs = foldr (<>) e xs`

for all finite lists xs provided that

`(x <> y) @ z = x <> (y @ z)`

`e @ x = x <> e`

induction case (left-hand side):

`foldl (@) e (x:xs)`

= {def foldl}

`foldl (@) (e @ x) xs`

= {proviso 2}

`foldl (@) (x <> e) xs`

This is obviously not the last step of the proof, but it's the source of my question: Because `e`

is expanded recursively by `foldl`

, it seems like its definition depends on the stage of the recursion, and therefore it's not clear to me that `e @ x = x <> e`

is always a valid substitution. Above in `foldl (@) (e @ x) xs`

, argument `e`

of `foldl`

takes on the value of `e @ x`

, so I would think that proviso 2 can't be applied -- to make the substitution it would need to be `(e @ x) @ x`

EDIT

Here's the complete proof

left hand | right hand |
---|---|

foldl (@) e (x:xs) = {def foldl} | foldr (<>) e (x:xs) = {def foldr} |

foldl (@) (e @ x) xs = {proviso 2} | x <> foldr (<>) e xs = {induction} |

foldl (@) (x <> e) xs | x <> foldl (@) e xs |

The two sides have simplified to different results. We need another induction hypothesis:

`foldl (@) (x <> y) xs = x <> foldl (@) y xs`

The base case is trivial. For the inductive case

left hand | right hand |
---|---|

foldl (@) (x <> y) (z:zs) = {def foldl} | x <> foldl (@) y (z:zs) = {def foldl} |

foldl (@) ((x <> y) @ z) zs = {proviso 1} | x <> foldl (@) (y @ z) zs |

foldl (@) (x <> (y @ z)) zs = {induction} | |

x <> foldl (@) (y @ z) zs |

Solution

This can be proved for `e`

fixed in the statement of the theorem (i.e., with the identity `e @ x = x <> e`

holding for all `x`

but only a specific `e`

), but it's quite a bit more complicated than the part of the proof you've shown. I don't have a copy of the original source, so I don't know how much additional guidance the solution gives.

Anyway, I found it helpful to first prove an intermediate result:

```
forall y, z, xs: foldl (@) (y <> z) xs = y <> foldl (@) z xs -- (A)
```

This can be proved inductively on `xs`

. The base case is:

```
foldl (@) (y <> z) []
= y <> z -- foldl definition
= y <> foldl (@) z [] -- foldl definition
```

The inductive case is:

```
foldl (@) (y <> z) (x:xs)
= foldl (@) ((y <> z) @ x) xs -- foldl definition
= foldl (@) (y <> (z @ x)) xs -- assumption #1
= y <> foldl (@) (z @ x) xs -- inductive assumption for z: = z @ x
= y <> foldl (@) z (x:xs) -- foldl definition
```

So, (A) is established.

Now, we can turn to the desired result:

```
forall xs. foldl (@) e xs = foldr (<>) e xs -- (B)
```

which can also be proved inductively.

The base case is:

```
foldl (@) e []
= e -- foldl definition
= foldr (<>) e [] -- foldr definition
```

The inductive step is:

```
foldl (@) e (x:xs)
= foldl (@) (e @ x) xs -- foldl definition
= foldl (@) (x <> e) xs -- assumption #2 for fixed e only
= x <> foldl (@) e xs -- intermediate result (A) specialized to z := e
= x <> foldr (<>) e xs -- inductive assumption
= foldr (<>) e (x:xs) -- definition of foldr
```

- How can I refactor from error to an ExceptT?
- How can I generate a random sequence of elements from a list in Haskell?
- Problem with quantified types and pattern matching
- Why is the `unicode-show` package necessary?
- Get sum of int or integer in Haskell
- Java 8: streams and the Sieve of Eratosthenes
- Can iterate be written with a fold?
- Haskell function with data pattern match and second argument gives Equations have different numbers of arguments
- How to use (->) instances of Monad and confusion about (->)
- Trouble understanding Haskell type unification with a nested `fmap`
- why ghc does not support PIE and Full RelRO in linux?
- Controlling Wai logger messages
- How do Haskell compilers decide whether to allocate on the heap or the stack?
- How can date/time format of Yesod logger be configured?
- In Haskell's Turtle library, how to copy a file, but preserve the file date
- Could not deduce (Semigroup (TimedEvents a))
- Instance of class with Data family yielding error "Couldn't match expected type"
- Is there a way to get a Haskell setup on Windows without an installation? (Copy + paste)
- Haskell parse error on input `<-'
- Inline assembly in Haskell
- How do I deal with arbitrary length tuple to build up a complex SQL query for Haskell's postgresql-simple's query function?
- Extract liftIO and runSql in separate function (Haskell)
- How to query NodeJS stream 'meta data'?
- Building multiple executables in the default Haskell Stack project
- Take elements of a list up to and including the first value that satisfies some predicate in Haskell
- How are Hackage package names mapped to 'cabal install' names?
- Insert entity into DB with manually created foreign key in Persistent library (Haskell)
- couldn´t match type 'IO´ with ´[]` inside a do
- Why doesn't contravariance apply in certain cases like [b] → Int < a → Int
- How does the Haskell compiler handle the 'where' statement?